Prohibition and detecting its violation

Intention

I want to distinguish a prohibition of an action from a detected violation of that prohibition.

A prohibition executes as a negative maintenance condition.

Correct formFrozen execution sceneBoundary

Incorrect form and why it stays silent

Incorrect form

// Отсутствие performed(p) после окна означает SATISFIED.

Absence of information about the action does not prove that the prohibition was observed over the whole window. Satisfaction requires completeness of observations; otherwise after the window the status is UNDETERMINED.

Correct form

Arxo Law

language "law.core" version "0.2";
package recipes.a.r03 version "0.1.0";
namespace "urn:recipe:a-positions:03";

entity Person;
relation registered(p: Person);
relation done(p: Person);
relation performed(p: Person);
rule BanRule strict { for p: Person; when registered(p);
    then prohibition Ban { bearer p; action performed(p); window [@2026-09-01, @2026-09-10]; };
}
rule GuardRule strict { for p: Person; when registered(p);
    then duty Guard { bearer p; maintain not performed(p) during [@2026-09-01, @2026-09-10]; };
}

Frozen execution scene

Facts and snapshot	Question	Answer
no action; 2026-09-05	positions()	position(Ban, ACTIVE); expect position(Guard, ACTIVE); / COMPUTED
action performed; 2026-09-05	positions()	position(Ban, VIOLATED); expect position(Guard, VIOLATED); / COMPUTED
action established; after the window, 2026-09-13	positions()	position(Ban, VIOLATED); / COMPUTED

no action keeps ban active

Arxo Law

test "no action keeps ban active" {
    given {
        context {
            legal_time @2026-09-05;
            decision_time @2026-09-05T09:00:00+05:00;
            knowledge_time @2026-09-30T09:00:00+05:00;
            timezone "Asia/Almaty";
        }
        assert registered(entity_ref("urn:recipe:a-positions:03:p"));
    }
    evaluate positions();
    expect position(Ban, ACTIVE); expect position(Guard, ACTIVE);
    expect evaluation_status == COMPUTED;

}

performed action violates ban

Arxo Law

test "performed action violates ban" {
    given {
        context {
            legal_time @2026-09-05;
            decision_time @2026-09-05T09:00:00+05:00;
            knowledge_time @2026-09-30T09:00:00+05:00;
            timezone "Asia/Almaty";
        }
        assert registered(entity_ref("urn:recipe:a-positions:03:p")); assert performed(entity_ref("urn:recipe:a-positions:03:p"));
    }
    evaluate positions();
    expect position(Ban, VIOLATED); expect position(Guard, VIOLATED);
    expect evaluation_status == COMPUTED;

}

violation persists after window

Arxo Law

test "violation persists after window" {
    given {
        context {
            legal_time @2026-09-13;
            decision_time @2026-09-13T09:00:00+05:00;
            knowledge_time @2026-09-30T09:00:00+05:00;
            timezone "Asia/Almaty";
        }
        assert registered(entity_ref("urn:recipe:a-positions:03:p")); assert performed(entity_ref("urn:recipe:a-positions:03:p"));
    }
    evaluate positions();
    expect position(Ban, VIOLATED);
    expect evaluation_status == COMPUTED;

}

Counterfactual

Mutation: action performed(p); → “; rejection LDC-E1305. Additional counterfactuals are shown as separate scenes.

Boundary

Ban and Guard yield the same status. The example uses accepted facts of the current case; a separate search of historical events over the whole window is not performed here. An unestablished action is not treated as performed; an explicit negation in one snapshot does not replace completeness of observations over the whole window.