Maintain a state

Intention

I want to check that a state holds throughout an interval.

A one-off fact must be distinguished from complete monitoring.

Correct formFrozen execution sceneBoundary

Incorrect form and why it stays silent

Incorrect form

achieve done(p) during [@2026-09-01, @2026-09-10];

A one-off fact is enough for achievement, but does not certify maintenance over the whole window. The counterexample already breaks maintenance inside the window.

Correct form

Arxo Law

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

entity Person;
relation registered(p: Person);
relation done(p: Person);
rule R strict { for p: Person; when registered(p);
    then duty Keep { bearer p; maintain done(p) during [@2026-09-01, @2026-09-10]; };
}

Frozen execution scene

Facts and snapshot	Question	Answer
positive fact in the window; 2026-09-05	positions()	position(Keep, ACTIVE); / COMPUTED
counterexample in the window; 2026-09-05	positions()	position(Keep, VIOLATED); / COMPUTED
end without a certificate; 2026-09-13	positions()	position(Keep, UNDETERMINED); / COMPUTED

active with supporting fact in window

Arxo Law

test "active with supporting fact in window" {
    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:02:p")); assert done(entity_ref("urn:recipe:a-positions:02:p"));
    }
    evaluate positions();
    expect position(Keep, ACTIVE);
    expect evaluation_status == COMPUTED;

}

violated by counterexample in window

Arxo Law

test "violated by counterexample in window" {
    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:02:p")); assert not done(entity_ref("urn:recipe:a-positions:02:p"));
    }
    evaluate positions();
    expect position(Keep, VIOLATED);
    expect evaluation_status == COMPUTED;

}

undetermined at end without certificate

Arxo Law

test "undetermined at end without certificate" {
    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:02:p")); assert done(entity_ref("urn:recipe:a-positions:02:p"));
    }
    evaluate positions();
    expect position(Keep, UNDETERMINED);
    expect evaluation_status == COMPUTED;

}

The incorrect-form variant is executed as a separate package: maintain is replaced with achieve; one positive fact already yields SATISFIED.

achieve variant satisfied by single fact

Arxo Law

test "achieve variant satisfied by single fact" {
    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:02:p")); assert done(entity_ref("urn:recipe:a-positions:02:p"));
    }
    evaluate positions();
    expect position(Keep, SATISFIED);
    expect evaluation_status == COMPUTED;

}

Python

>>> import runpy
>>> check = runpy.run_path("docs/recipes/a-positions/resources/check.py")
>>> check["check_variant"](https://github.com/arxohq/law/blob/master/docs/recipes/a-positions/2)
'А2: контрфактуал подтверждён; lawc = lawref'

Counterfactual

Mutation: maintain done(p) during [@2026-09-01, @2026-09-10]; → maintain done(p);; rejection LDC-E0201. Additional counterfactuals are shown as separate scenes.

Boundary

A duty without a stated term is not always automatically maintenance: the goal kind is chosen from the content of the rule. Completeness of observations is needed for SATISFIED after the window.