LDC-E1205 — Counterfactual with the wrong shape

What it means

A counterfactual block is a fixed-shape what-if: exactly one target being rewritten, exactly one cost function, and at least one mutable reference the analysis may vary. The same strictness covers the sibling name checks — an interpretation may only cite readings and names that exist, and a context profile may only extend a profile that is declared. A block that breaks the shape, or a reference that points at nothing declared, stops the compiler at the offending line.

The repair is to restore the shape: one target, one cost, at least one mutable entry, and references that name things the package declares.

Example

Arxo Law

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

entity Offence;
const Theft: Offence = Offence { };
relation listed(o: Offence) kind institutional;
function EditCost(cost: Decimal) -> Decimal = cost;
counterfactual IfX {
    target listed(Theft);
    target listed(Theft);
    mutable listed;
    cost EditCost;
}

Fix

Arxo Law

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

entity Offence;
const Theft: Offence = Offence { };
relation listed(o: Offence) kind institutional;
function EditCost(cost: Decimal) -> Decimal = cost;
counterfactual IfX {
    target listed(Theft);
    mutable listed;
    cost EditCost;
}

Engine message

The engine reports this in its own wording:

Output

example.law:9:16: error LDC-E1205: counterfactual "IfX": exactly one `target` is required (§186)

Related

• Interpretations — readings and the names they may cite.
• LDC-E1201 — the companion check for doubly declared names.