Check event type and transition conditions

Intent

I want to move an application only by a suitable event when the conditions hold.

Correct formFrozen execution sceneBoundary

Wrong form and why it stays silent

Incorrect form

// on Filed считают необязательным описанием; либо один when заменяет requires.

Carrier type, when, and requires are checked independently. ElectronicFiled is a subtype of Filed; Other does not fit even with all facts. Missing approved is not treated as satisfied.

Correct form

Arxo Law

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

entity Application;
event Filed { }
event ElectronicFiled: Filed { }
event Other { }
relation ready(app: Application);
relation approved(app: Application);
procedure Filing(app: Application) {
    state Draft initial;
    state Done terminal;
    transition Submit { from Draft; to Done; on Filed; when ready(app); requires approved(app); }
}

Frozen execution scene

P and Q in the table are different instances; E1/E2/E3 are carriers with an explicitly given time. All identifiers and instants are pinned in the scenes.

Events and facts	Question	Answer
all conditions	truth(current_state(P,Done))	truth_status == TRUE_ONLY; / COMPUTED
event subtype	truth(current_state(P,Done))	truth_status == TRUE_ONLY; / COMPUTED
required condition missing	truth(current_state(P,Done))	truth_status == NEITHER; / COMPUTED
false guard	truth(current_state(P,Done))	truth_status == NEITHER; / COMPUTED
foreign type	truth(current_state(P,Done))	truth_status == NEITHER; / COMPUTED
without requires	truth(current_state(P,Done))	truth_status == TRUE_ONLY; / COMPUTED

matching carrier and conditions transition

Arxo Law

test "matching carrier and conditions transition" {
    given {
        context {
            legal_time @2026-09-13T09:00:00Z;
            decision_time @2026-09-13T09:00:00Z;
            knowledge_time @2026-09-13T09:00:00Z;
            timezone "UTC";
        }
        assert procedure_instance(entity_ref("urn:recipe:k-procedures:02:p"));assert ready(entity_ref("urn:recipe:k-procedures:02:p")); assert approved(entity_ref("urn:recipe:k-procedures:02:p"));assert attempted_transition(entity_ref("urn:recipe:k-procedures:02:p"), Submit, Filed { id: "urn:recipe:k-procedures:02:E1", time: @2026-09-02T09:00:00Z });
    }
    evaluate truth(current_state(entity_ref("urn:recipe:k-procedures:02:p"),Done));
    expect truth_status == TRUE_ONLY;
    expect evaluation_status == COMPUTED;

}

event subtype transitions

Arxo Law

test "event subtype transitions" {
    given {
        context {
            legal_time @2026-09-13T09:00:00Z;
            decision_time @2026-09-13T09:00:00Z;
            knowledge_time @2026-09-13T09:00:00Z;
            timezone "UTC";
        }
        assert procedure_instance(entity_ref("urn:recipe:k-procedures:02:p"));assert ready(entity_ref("urn:recipe:k-procedures:02:p")); assert approved(entity_ref("urn:recipe:k-procedures:02:p"));assert attempted_transition(entity_ref("urn:recipe:k-procedures:02:p"), Submit, ElectronicFiled { id: "urn:recipe:k-procedures:02:E1", time: @2026-09-02T09:00:00Z });
    }
    evaluate truth(current_state(entity_ref("urn:recipe:k-procedures:02:p"),Done));
    expect truth_status == TRUE_ONLY;
    expect evaluation_status == COMPUTED;

}

missing approval blocks silently

Arxo Law

test "missing approval blocks silently" {
    given {
        context {
            legal_time @2026-09-13T09:00:00Z;
            decision_time @2026-09-13T09:00:00Z;
            knowledge_time @2026-09-13T09:00:00Z;
            timezone "UTC";
        }
        assert procedure_instance(entity_ref("urn:recipe:k-procedures:02:p"));assert ready(entity_ref("urn:recipe:k-procedures:02:p"));assert attempted_transition(entity_ref("urn:recipe:k-procedures:02:p"), Submit, Filed { id: "urn:recipe:k-procedures:02:E1", time: @2026-09-02T09:00:00Z });
    }
    evaluate truth(current_state(entity_ref("urn:recipe:k-procedures:02:p"),Done));
    expect truth_status == NEITHER;
    expect evaluation_status == COMPUTED;

}

refuted guard blocks transition

Arxo Law

test "refuted guard blocks transition" {
    given {
        context {
            legal_time @2026-09-13T09:00:00Z;
            decision_time @2026-09-13T09:00:00Z;
            knowledge_time @2026-09-13T09:00:00Z;
            timezone "UTC";
        }
        assert procedure_instance(entity_ref("urn:recipe:k-procedures:02:p"));assert not ready(entity_ref("urn:recipe:k-procedures:02:p")); assert approved(entity_ref("urn:recipe:k-procedures:02:p"));assert attempted_transition(entity_ref("urn:recipe:k-procedures:02:p"), Submit, Filed { id: "urn:recipe:k-procedures:02:E1", time: @2026-09-02T09:00:00Z });
    }
    evaluate truth(current_state(entity_ref("urn:recipe:k-procedures:02:p"),Done));
    expect truth_status == NEITHER;
    expect evaluation_status == COMPUTED;

}

foreign carrier type mismatches

Arxo Law

test "foreign carrier type mismatches" {
    given {
        context {
            legal_time @2026-09-13T09:00:00Z;
            decision_time @2026-09-13T09:00:00Z;
            knowledge_time @2026-09-13T09:00:00Z;
            timezone "UTC";
        }
        assert procedure_instance(entity_ref("urn:recipe:k-procedures:02:p"));assert ready(entity_ref("urn:recipe:k-procedures:02:p")); assert approved(entity_ref("urn:recipe:k-procedures:02:p"));assert attempted_transition(entity_ref("urn:recipe:k-procedures:02:p"), Submit, Other { id: "urn:recipe:k-procedures:02:E1", time: @2026-09-02T09:00:00Z });
    }
    evaluate truth(current_state(entity_ref("urn:recipe:k-procedures:02:p"),Done));
    expect truth_status == NEITHER;
    expect evaluation_status == COMPUTED;
    expect issue(TRANSITION_CARRIER_TYPE_MISMATCH);
}

transition passes without requires

Arxo Law

test "transition passes without requires" {
    given {
        context {
            legal_time @2026-09-13T09:00:00Z;
            decision_time @2026-09-13T09:00:00Z;
            knowledge_time @2026-09-13T09:00:00Z;
            timezone "UTC";
        }
        assert procedure_instance(entity_ref("urn:recipe:k-procedures:02:p"));assert ready(entity_ref("urn:recipe:k-procedures:02:p"));assert attempted_transition(entity_ref("urn:recipe:k-procedures:02:p"), Submit, Filed { id: "urn:recipe:k-procedures:02:E1", time: @2026-09-02T09:00:00Z });
    }
    evaluate truth(current_state(entity_ref("urn:recipe:k-procedures:02:p"),Done));
    expect truth_status == TRUE_ONLY;
    expect evaluation_status == COMPUTED;

}

Python

>>> import runpy
>>> check = runpy.run_path("docs/recipes/k-procedures/resources/check.py")
>>> check["check_steps"](https://github.com/arxohq/law/blob/master/docs/recipes/k-procedures/2)
'К2: причины шагов и отсутствие лишних предупреждений проверены; lawc = lawref'

Counterfactual

Mutation check — LDC-E1344.

Original fragment:

Output

on Filed;

Replacement:

Output

on ready;

Scenes with a condition removed are marked separately; the same inputs get a different outcome.

Boundary

requires here reads empirical approved. Cross-procedure completed(P,y) needs a concrete instance and reads only a strict temporal prefix. A guard must not depend on a rule over the fold result (E1348); the witness is Explain an unreached state.