language "law.core" version "0.1";
package de.hilbert.grundlagen version "0.1.0";
namespace "urn:de:hilbert:clir:grundlagen";

// §93.2 ГЛАЗАМИ ОДНОГО ОТВЕТА. Треугольник ABC: три точки, три прямые. На
// вопрос «лежит ли C на прямой ab» открытый мир ответил бы NEITHER, и
// аксиома Паша не имела бы посылки «прямая не проходит через вершину».
// Замыкание §70 конечной модели делает ответ FALSE_ONLY. Снимите
// `InzidenzAbschluss` — и этот тест упадёт первым.
test "urn:query:hilb-test-01" {
    given {
        context {
            decision_time @0001-01-01T12:00:00Z;
            knowledge_time @0001-01-01T12:00:00Z;
            legal_time @0001-01-01;
            timezone "UTC";
        }
        assert "hilb-t01-1": punkt_der_figur(entity_ref("urn:de:hilbert:case:point:A")) { origin case_input; }
        assert "hilb-t01-2": punktname(entity_ref("urn:de:hilbert:case:point:A"), "A") { origin case_input; }
        assert "hilb-t01-3": punkt_der_figur(entity_ref("urn:de:hilbert:case:point:B")) { origin case_input; }
        assert "hilb-t01-4": punktname(entity_ref("urn:de:hilbert:case:point:B"), "B") { origin case_input; }
        assert "hilb-t01-5": punkt_der_figur(entity_ref("urn:de:hilbert:case:point:C")) { origin case_input; }
        assert "hilb-t01-6": punktname(entity_ref("urn:de:hilbert:case:point:C"), "C") { origin case_input; }
        assert "hilb-t01-7": gerade_der_figur(entity_ref("urn:de:hilbert:case:line:ab")) { origin case_input; }
        assert "hilb-t01-8": geradenname(entity_ref("urn:de:hilbert:case:line:ab"), "ab") { origin case_input; }
        assert "hilb-t01-9": gerade_der_figur(entity_ref("urn:de:hilbert:case:line:bc")) { origin case_input; }
        assert "hilb-t01-10": geradenname(entity_ref("urn:de:hilbert:case:line:bc"), "bc") { origin case_input; }
        assert "hilb-t01-11": gerade_der_figur(entity_ref("urn:de:hilbert:case:line:ac")) { origin case_input; }
        assert "hilb-t01-12": geradenname(entity_ref("urn:de:hilbert:case:line:ac"), "ac") { origin case_input; }
        assert "hilb-t01-13": liegt_auf(entity_ref("urn:de:hilbert:case:point:A"), entity_ref("urn:de:hilbert:case:line:ab")) { origin case_input; }
        assert "hilb-t01-14": liegt_auf(entity_ref("urn:de:hilbert:case:point:B"), entity_ref("urn:de:hilbert:case:line:ab")) { origin case_input; }
        assert "hilb-t01-15": liegt_auf(entity_ref("urn:de:hilbert:case:point:B"), entity_ref("urn:de:hilbert:case:line:bc")) { origin case_input; }
        assert "hilb-t01-16": liegt_auf(entity_ref("urn:de:hilbert:case:point:C"), entity_ref("urn:de:hilbert:case:line:bc")) { origin case_input; }
        assert "hilb-t01-17": liegt_auf(entity_ref("urn:de:hilbert:case:point:A"), entity_ref("urn:de:hilbert:case:line:ac")) { origin case_input; }
        assert "hilb-t01-18": liegt_auf(entity_ref("urn:de:hilbert:case:point:C"), entity_ref("urn:de:hilbert:case:line:ac")) { origin case_input; }
    }
    evaluate truth(liegt_auf(entity_ref("urn:de:hilbert:case:point:C"), entity_ref("urn:de:hilbert:case:line:ab")));
    expect result_kind == PROPOSITION;
    expect truth_status == FALSE_ONLY;
    // ПОЧЕМУ ДОКУМЕНТ `NON_EXECUTABLE`, А НЕ `COMPUTED`. Ответ на сам вопрос
    // вычислен и равен `FALSE_ONLY`; статус документа говорит о ДРУГОМ — о том,
    // что предъявленный чертёж моделью аксиом I—II не является. Errata 0.2-05
    // (§175) запрещает `COMPUTED` рядом с issue строгости `error`, а
    // `CONSTRAINT_VIOLATED` §93.1 несёт строгость, объявленную у инварианта, —
    // здесь `error`. На треугольнике ABC нарушены три инварианта: `AxiomI3`
    // (тройка не лежит на одной прямой и не принадлежит ни одной плоскости —
    // плоскостей в чертеже нет вовсе), `AxiomII2Innen` и `AxiomII2Fortsetzung`
    // (граница 1 разбора: II 2 нарушена на КАЖДОЙ конечной конфигурации).
    // Поэтому `COMPUTED` в этом пакете не даёт и не может дать ни одна конечная
    // фигура, и разделение миров тут не помогает — чинится ожидание, а не
    // данные. Ожидание стережёт границу ПАДЕНИЕМ: снимут блокирующий исход у
    // `CONSTRAINT_VIOLATED` — тест упадёт, а не промолчит; `issues_within`
    // держит второе — иных диагностик выше `info` в документе нет.
    expect evaluation_status == NON_EXECUTABLE;
    expect issue(CONSTRAINT_VIOLATED);
    expect issues_within(info, CONSTRAINT_VIOLATED);
}