Skip to content

Synchronous semantics — how LoLa programmes run

Audience: developer who wants to understand why LoLa behaves the way it does, not just what the rules say.\ Language Reference: §15 Dynamic/synchronous semantics, §7 State transitions.

The scan-cycle model

A LoLa FUNCTION_BLOCK is a synchronous reactive component: it runs in a loop, one scan at a time. Each scan has exactly three phases:

  1. Read all inputs — every input variable is latched at its current value.
  2. Compute — evaluate rules, derived assignments, and proof obligations, using the start-of-scan values of all registers and inputs.
  3. Commit — all new register values are written simultaneously.

The loop repeats forever. No scan overlaps another. No output changes while a scan is running.

This is the same model as a PLC's scan cycle. LoLa makes it the formal execution model, not an implementation detail.

Pre-state semantics — why rules read old values

Inside a rule block, every reference to a register reads its start-of-scan value — the value it held before the current scan began. This is called the pre-state.

Why? Consider an edge detector:

Q:  SET CLK AND NOT M OTHERWISE;   -- CLK is new; M is the OLD previous CLK
M:  SET CLK OTHERWISE;              -- remember this scan's CLK for next scan

Q must detect a change: "CLK is high now and was low before." To detect a change you need two time-points, and the only way to read the past is to hold it in a register. M holds the previous CLK; the M that Q's rule reads is the old M — from the start of this scan — not the M that is being written in this same scan.

If rules read new values, an edge detector would collapse: M would already be the new CLK when Q reads it, and CLK AND NOT M would always be false.

Pre-state semantics is therefore not an arbitrary restriction. It is what makes state machines possible without requiring explicit latches.

The rule is simple: inside a rule block (output: rule list), a reference to any register reads the pre-state value. The compiler enforces this by computing all new values first, then committing them — the _next staging in the generated ST.

Derived values — the other reading time

A derived assignment (:=) reads a different time:

y := some_register + 1;

Inside :=, some_register reads the new (post-commit) value just computed for this scan, not the pre-state. This is what makes derived values combinational: they are recomputed from the latest results every scan, with no memory of their own.

The pattern:

Where you reference a register What you get
Inside a rule block (reg:) old (pre-state, start of scan)
Inside a derived assignment (:=) new (post-compute, this scan)

This distinction is the mechanism behind the counter/hold/edge patterns in the tutorial. If you get an unexpected counterexample that seems to show the invariant violated "in the same step it was set", check whether you are accidentally reading a new value where a pre-state read was intended.

Atomic commit — all outputs update simultaneously

The commit phase writes all new register values at once, in an undefined order. No output update is visible to another output's computation in the same scan. This is the meaning of "atomic" in the scan model.

The generated ST _next staging makes this concrete: every new value is computed into a temporary (_Q_next, _M_next, …), and only after all temporaries are computed are the registers assigned. A straightforward sequential assignment would not be equivalent — earlier assignments would be visible to later ones.

Atomic commit is why LoLa's semantics are deterministic even when multiple rules reference each other's outputs.

Priority resolution — explicit conflict semantics

When multiple rules for the same output are active at the same time, the rule with the highest PRIO value wins. The rule order in the source is irrelevant.

This is a deliberate design choice. Ordered if/else chains in Structured Text encode priority implicitly — first branch wins — and that implicit priority is invisible to reviewers and invisible to the proof system. Two developers may disagree about what "first branch wins" means after a refactor.

In LoLa: - Priority is declared, not implied by position. - Conflicts between equal-priority rules that can produce different results are ambiguous-priority compile errors, not silent bugs. - Dead rules (always beaten by a higher-priority rule) are unreachable-rule warnings — visible, not silently compiled away.

The compiler reduces the priority stack to a single logical formula (nested Ites) and proves properties about that formula. The proof is about the formula, not about the source text order.

Timers as declarations, not state machines

IEC 61131-3 timers (TON, TOFF) are explicit state machines you must wire and reset. LoLa's HELD(cond, PT) and ELAPSED(cond, PT) are declarations:

  • HELD(cond, PT) is TRUE if cond has been continuously true for at least PT.
  • ELAPSED(cond, PT) is the elapsed time since cond became true, capped at PT.

In the verifier, time is symbolic: the proof does not fix a specific delay; it reasons about all possible delays at once. A proof that NOT Shutdown OR Warn (shutdown implies warning) holds for every timing, not just the 2-second preset.

In the generated ST, HELD/ELAPSED map to a native TON instance. No elapsed- time arithmetic appears in the logic; the PLC's own timer block handles it.

This separation — symbolic in proofs, native in generated code — is why timing properties are verified once and never need test-case coverage of every possible scan rate.

See also