LDC-E1348 — Transition guard reads above the fold

What it means

A transition guard runs inside the history fold, and it may only read what the fold can see: norms, powers, and rules that themselves read the fold all execute above it, and their inferences stay invisible to the guard under every phase order. A guard that reads such a predicate waits on an answer that never arrives, so the compiler stops at the guard.

The repair is to read downward: guard on case facts and empirical predicates the fold already holds, and move the derived reasoning out of the guard. A guard that reads the fold fires exactly when its history says so.

Example

Arxo Law

language "law.core" version "0.2";
package demo.diagnostics version "0.1.0";
namespace "urn:law:demo:diagnostics";

entity Tenant;
event Filed {
    tenant: Tenant;
}
relation seen_once(t: Tenant) kind institutional;
relation ready(t: Tenant) kind institutional;
procedure App(t: Tenant) {
    state Draft initial;
    state Done terminal;
    transition Go {
        from Draft;
        to Done;
        on Filed;
        when ready(t);
    }
}
rule Seen strict {
    for x: Tenant;
    when current_state(x, Done);
    then seen_once(x);
}
rule Ready strict {
    for x: Tenant;
    when seen_once(x);
    then ready(x);
}

Fix

Arxo Law

language "law.core" version "0.2";
package demo.diagnostics version "0.1.0";
namespace "urn:law:demo:diagnostics";

entity Tenant;
event Filed {
    tenant: Tenant;
}
relation team(t: Tenant) kind empirical;
procedure App(t: Tenant) {
    state Draft initial;
    state Done terminal;
    transition Go {
        from Draft;
        to Done;
        on Filed;
        when team(t);
    }
}

Engine message

The engine reports this in its own wording:

Output

example.law:14:16: error LDC-E1348: transition guard `urn:law:demo:diagnostics#App/Go` reads predicate `urn:law:demo:diagnostics#ready`, produced by rule `urn:law:demo:diagnostics#Ready`, which itself depends on the history fold: such a rule's inference is invisible to the guard under any phase order, and the rule cannot be moved down — it reads the fold (§161.2)

Related

• Procedures — transitions, guards, and what fires them.
• Strict rules — rules and the fold their inferences join.