Take an application through stages

Intent

I want to distinguish a filed application from completed consideration.

Correct formFrozen execution sceneBoundary

Wrong form and why it stays silent

Incorrect form

procedure Other(app: Application) { state Draft initial; }

A state, transition, or region name is unique in the whole package. Another procedure’s name does not create a separate resolution scope for a bare Draft.

Correct form

Arxo Law

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

entity Application;
event Tick { }
procedure Filing(app: Application) {
    state Draft initial;
    state Submitted;
    state Done terminal;
    transition Submit { from Draft; to Submitted; on Tick; }
    transition Decide { from Submitted; to Done; on Tick; }
}

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
instance with no attempts	truth(current_state(P,Draft))	truth_status == TRUE_ONLY; / COMPUTED
only filed	truth(current_state(P,Submitted))	truth_status == TRUE_ONLY; / COMPUTED
full chain	truth(current_state(P,Done))	truth_status == TRUE_ONLY; / COMPUTED
decision without filing	truth(current_state(P,Done))	truth_status == NEITHER; / COMPUTED
draft already left	truth(current_state(P,Draft))	truth_status == NEITHER; / COMPUTED

initial state holds without attempts

Arxo Law

test "initial state holds without attempts" {
    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:01:p"));
    }
    evaluate truth(current_state(entity_ref("urn:recipe:k-procedures:01:p"),Draft));
    expect truth_status == TRUE_ONLY;
    expect evaluation_status == COMPUTED;

}

submitted state after filing

Arxo Law

test "submitted state after filing" {
    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:01:p"));
assert attempted_transition(entity_ref("urn:recipe:k-procedures:01:p"), Submit, Tick { id: "urn:recipe:k-procedures:01:E1", time: @2026-09-02T09:00:00Z });
    }
    evaluate truth(current_state(entity_ref("urn:recipe:k-procedures:01:p"),Submitted));
    expect truth_status == TRUE_ONLY;
    expect evaluation_status == COMPUTED;

}

full chain reaches done

Arxo Law

test "full chain reaches done" {
    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:01:p"));
assert attempted_transition(entity_ref("urn:recipe:k-procedures:01:p"), Submit, Tick { id: "urn:recipe:k-procedures:01:E1", time: @2026-09-02T09:00:00Z });
assert attempted_transition(entity_ref("urn:recipe:k-procedures:01:p"), Decide, Tick { id: "urn:recipe:k-procedures:01:E2", time: @2026-09-03T09:00:00Z });
    }
    evaluate truth(current_state(entity_ref("urn:recipe:k-procedures:01:p"),Done));
    expect truth_status == TRUE_ONLY;
    expect evaluation_status == COMPUTED;

}

decision without submission stays neither

Arxo Law

test "decision without submission stays neither" {
    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:01:p"));
assert attempted_transition(entity_ref("urn:recipe:k-procedures:01:p"), Decide, Tick { id: "urn:recipe:k-procedures:01:E1", time: @2026-09-02T09:00:00Z });
    }
    evaluate truth(current_state(entity_ref("urn:recipe:k-procedures:01:p"),Done));
    expect truth_status == NEITHER;
    expect evaluation_status == COMPUTED;

}

abandoned draft no longer holds

Arxo Law

test "abandoned draft no longer holds" {
    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:01:p"));
assert attempted_transition(entity_ref("urn:recipe:k-procedures:01:p"), Submit, Tick { id: "urn:recipe:k-procedures:01:E1", time: @2026-09-02T09:00:00Z });
assert attempted_transition(entity_ref("urn:recipe:k-procedures:01:p"), Decide, Tick { id: "urn:recipe:k-procedures:01:E2", time: @2026-09-03T09:00:00Z });
    }
    evaluate truth(current_state(entity_ref("urn:recipe:k-procedures:01:p"),Draft));
    expect truth_status == NEITHER;
    expect evaluation_status == COMPUTED;

}

Counterfactual

Mutation check — LDC-E1351.

Original fragment:

Output

state Submitted;

Replacement:

Output

state Submitted;
    state Draft;

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

Boundary

A duplicate name is rejected statically with E1351.

An empty history has initial_state, but not entered_state with a fictional carrier. One legal_time date selects the law for the whole presented history; temporal frames by editions are a separate instrument.