Explain an unreached state

Intent

I want to know which transition attempt did not bring the case into the needed state.

Correct formFrozen execution sceneBoundary

Wrong form and why it stays silent

Incorrect form

// Ищу правило, выводящее current_state: такого правила в CLIR нет.

The why_not candidate is transition Submit. For a missing attempt the attempt itself is unknown; for a presented invalid attempt procedure_step names on, guard, or requires.

Correct form

Arxo Law

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

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
no attempt	why_not(current_state(P,Done))	blocked_by("urn:recipe:k-procedures:05#Filing/Submit"); expect blockers(1); / COMPUTED
guard refuted	why_not(current_state(P,Done))	blocked_by("urn:recipe:k-procedures:05#Filing/Submit","guard"); / COMPUTED
requires not established	why_not(current_state(P,Done))	blocked_by("urn:recipe:k-procedures:05#Filing/Submit","requires"); / COMPUTED
type mismatch	why_not(current_state(P,Done))	blocked_by("urn:recipe:k-procedures:05#Filing/Submit","on"); / COMPUTED
state reached	why_not(current_state(P,Done))	truth_status == TRUE_ONLY; / COMPUTED

missing attempt names candidate transition

Arxo Law

test "missing attempt names candidate 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:05:p"));
    }
    evaluate why_not(current_state(entity_ref("urn:recipe:k-procedures:05:p"),Done));
    expect blocked_by("urn:recipe:k-procedures:05#Filing/Submit"); expect blockers(1);
    expect evaluation_status == COMPUTED;

}

refuted guard names guard reason

Arxo Law

test "refuted guard names guard reason" {
    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:05:p"));assert not ready(entity_ref("urn:recipe:k-procedures:05:p")); assert approved(entity_ref("urn:recipe:k-procedures:05:p"));assert attempted_transition(entity_ref("urn:recipe:k-procedures:05:p"), Submit, Filed { id: "urn:recipe:k-procedures:05:E1", time: @2026-09-02T09:00:00Z });
    }
    evaluate why_not(current_state(entity_ref("urn:recipe:k-procedures:05:p"),Done));
    expect blocked_by("urn:recipe:k-procedures:05#Filing/Submit","guard");
    expect evaluation_status == COMPUTED;

}

missing approval names requires reason

Arxo Law

test "missing approval names requires reason" {
    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:05:p"));assert ready(entity_ref("urn:recipe:k-procedures:05:p"));assert attempted_transition(entity_ref("urn:recipe:k-procedures:05:p"), Submit, Filed { id: "urn:recipe:k-procedures:05:E1", time: @2026-09-02T09:00:00Z });
    }
    evaluate why_not(current_state(entity_ref("urn:recipe:k-procedures:05:p"),Done));
    expect blocked_by("urn:recipe:k-procedures:05#Filing/Submit","requires");
    expect evaluation_status == COMPUTED;

}

carrier mismatch names on reason

Arxo Law

test "carrier mismatch names on reason" {
    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:05:p"));assert ready(entity_ref("urn:recipe:k-procedures:05:p")); assert approved(entity_ref("urn:recipe:k-procedures:05:p"));assert attempted_transition(entity_ref("urn:recipe:k-procedures:05:p"), Submit, Other { id: "urn:recipe:k-procedures:05:E1", time: @2026-09-02T09:00:00Z });
    }
    evaluate why_not(current_state(entity_ref("urn:recipe:k-procedures:05:p"),Done));
    expect blocked_by("urn:recipe:k-procedures:05#Filing/Submit","on");
    expect evaluation_status == COMPUTED;
    expect issue(TRANSITION_CARRIER_TYPE_MISMATCH);
}

reached state answers true

Arxo Law

test "reached state answers true" {
    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:05:p"));assert ready(entity_ref("urn:recipe:k-procedures:05:p")); assert approved(entity_ref("urn:recipe:k-procedures:05:p"));assert attempted_transition(entity_ref("urn:recipe:k-procedures:05:p"), Submit, Filed { id: "urn:recipe:k-procedures:05:E1", time: @2026-09-02T09:00:00Z });
    }
    evaluate why_not(current_state(entity_ref("urn:recipe:k-procedures:05: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_blockers"](https://github.com/arxohq/law/blob/master/docs/recipes/k-procedures/5)
'К5: переходы и причины проверены; on воспроизводит дефект байтового паритета'

Counterfactual

Mutation check — LDC-E1348.

Original fragment:

Arxo Law

relation ready(app: Application);

Replacement:

Arxo Law

relation ready(app: Application);
rule Feedback strict { for app: Application; when current_state(app,Done); then ready(app); }

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

Boundary

The explanation reads a finished step and does not repeat the fold. why_not conjuncts are read from the final store; when another instance is read the summary may remain UNDETERMINED. A missing attempt is not declared a false fact.

For blocked_by here the transition StableId urn:recipe:k-procedures:05#Filing/Submit is needed. A bare Submit in this observation lowers as …#Submit and does not name the blocker; the formal member in attempted_transition resolves differently.