docs← Back to article

Markdown for LLMs

Explain an unreached state

The source Markdown for this article. Copy it into your assistant or download it as a text file.

Download this articlePlain text ↗
# Explain an unreached state

## Intent

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

## Wrong form and why it stays silent

```text title="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

```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` |

```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;

}
```

```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;

}
```

```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;

}
```

```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);
}
```

```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:

```law
relation ready(app: Application);
```

Replacement:

```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.