How to read and resolve an algebraic cycle¶

Audience: engineer whose block was refused because two values depend on each other within one scan.\ Prerequisites: definitions (:=), registers and PRE from the Introduction by Example.\ Design decision: ADR CYC-1.

Two signals that read each other in the same scan form an algebraic cycle. LoLa does not forbid such a cycle outright — it asks whether the cycle has a unique meaning. For every admissible input and previous state the compiler counts the solutions of the cycle's equations:

solutions	verdict	diagnosis
exactly one	admitted — the cycle is well defined	(compiles)
none	the rules contradict each other	`cycle-no-solution`
more than one	the specification does not pin the behaviour down	`cycle-underdetermined`

One solution — the cycle is fine¶

FUNCTION_BLOCK Enableable
VAR_INPUT a : BOOL; END_VAR
VAR_OUTPUT q1 : BOOL; q2 : BOOL; END_VAR
IMPLEMENTATION
    q1 := a AND q2;
    q2 := a OR q1;
END_IMPLEMENTATION
END_FUNCTION_BLOCK

q1 reads q2 and q2 reads q1, yet for each value of a exactly one assignment satisfies both equations. The compiler proves that, extracts the explicit form and emits it:

q1 := a;
q2 := a;

The cycle exists in your specification, never in the generated code — no loop, no runtime iteration, unchanged scan time.

No solution — the rules contradict each other¶

FUNCTION_BLOCK Contradiction
VAR_INPUT a : BOOL; END_VAR
VAR_OUTPUT x : BOOL; END_VAR
IMPLEMENTATION
    x := NOT x;
END_IMPLEMENTATION
END_FUNCTION_BLOCK

[cycle-no-solution] the cycle x has no solution for (no free inputs): the
rules cannot all hold, so the specification is inconsistent (CYC-1.1)

No value of x satisfies x = NOT x. This is a specification defect, and the message says so rather than blaming the cycle.

More than one solution — the interesting case¶

FUNCTION_BLOCK MutualStart
VAR_INPUT StartA : BOOL; StartB : BOOL; END_VAR
VAR_OUTPUT RunA : BOOL; RunB : BOOL; END_VAR
IMPLEMENTATION
    RunA := StartA AND NOT RunB;
    RunB := StartB AND NOT RunA;
END_IMPLEMENTATION
END_FUNCTION_BLOCK

[cycle-underdetermined] the cycle RunA -> RunB has more than one solution
for StartA=1, StartB=1: both (RunA=0, RunB=1) and (RunA=1, RunB=0) satisfy
the rules, so the specification does not pin down the behaviour (CYC-1.1)

This mutual interlock looks correct and is correct for every input except one: when both start buttons are pressed in the same scan, the rules permit either drive to win. That is a physical race, and the diagnosis names it — with the witness and both solutions — instead of reporting "cycle".

How to fix it: decide who wins. Any arbitration works; the point is that the decision now lives in the model instead of in the electrical timing.

FUNCTION_BLOCK ArbitratedStart
VAR_INPUT StartA : BOOL; StartB : BOOL; END_VAR
VAR_OUTPUT RunA : BOOL; RunB : BOOL; END_VAR
IMPLEMENTATION
    RunA := StartA AND NOT RunB;
    RunB := StartB AND NOT StartA;      (* A wins a simultaneous press *)
END_IMPLEMENTATION
END_FUNCTION_BLOCK

Uniqueness, not constructibility¶

One case separates LoLa from synchronous languages such as Esterel:

    x := x AND NOT x;

This is accepted. No value other than FALSE satisfies it, so the meaning is unique — even though no forward evaluation starting from "unknown" ever reaches it. Esterel rejects exactly this as non-constructive.

The admission rule here is about meaning, not about how a fixpoint iteration would behave: if the equations determine one answer, that answer is the definition, and the solver finds it whether or not a propagation order would.

What `PRE` is for — and what it is not¶

PRE(x) states a deliberate dependency on the previous scan. It is not a tool for silencing a cycle. Reaching for it here would turn a race into a one-scan delay that nobody asked for, and the arbitration question would stay unanswered — just invisible.

Limits (v1)¶

Cycles over BOOL values are admitted, up to an extraction budget. A cycle carrying INT/REAL values, or one larger than the budget, is refused with its own diagnosis (cycle-non-bool, cycle-budget-exceeded) — fail-closed, never a silent approximation.