Sequential control

21. Sequential Control with SSFC

All of the zqel constructs you have seen so far are about values: rules that define what an output should be, invariants that constrain what values are possible, composition that wires values together. This is the right tool when the question is "what should the motor speed be?" or "is the alarm active?"

Many controllers also have a sequential dimension: the process fills first, then heats, then holds at temperature, then drains — and can be pre-empted into a safe-stopped state at any point. This is mode logic. Encoding it as a set of output rules works, but you end up managing boolean phase-registers manually, writing edge detectors with PRE() to move between phases, and asserting the "only one phase active" invariant by hand.

zqel provides a second declaration form — the SSFC (Super Sequential Function Chart) — for exactly this. An SSFC is a hierarchy of named states with declared transitions between them. Semantically, an SSFC declaration defines a FUNCTION_BLOCK type: it is a stateful, instantiable component whose behavior is expressed as a state machine rather than as a set of rules. It is not a separate runtime; it lowers to the same zqel IR and is proved, compiled, and emitted by the same pipeline.

The framing that matters:

Use zqel rules to describe what values should hold.
Use an SSFC to describe which phase the controller is in, how it moves between phases, and what happens on entry, while active, and on exit.

21.1 A minimal state machine

SSFC TankFill
  VAR_INPUT
    go          : BOOL;
    level_high  : BOOL;
    level_empty : BOOL;
  END_VAR
  VAR_OUTPUT
    valve_fill  : BOOL;
    valve_drain : BOOL;
    done        : BOOL;
  END_VAR

  INITIAL STATE Idle
    TRANSITION TO Fill WHEN go;
  END_STATE

  STATE Fill
    EN:  valve_fill  := TRUE;
    EX:  valve_fill  := FALSE;
    TRANSITION TO Drain WHEN level_high;
  END_STATE

  STATE Drain
    EN:  valve_drain := TRUE;
    EX:  valve_drain := FALSE;
    TRANSITION TO Done WHEN level_empty;
  END_STATE

  STATE Done
    EN:  done := TRUE;
    EX:  done := FALSE;
    TRANSITION TO Idle WHEN TRUE;
  END_STATE
END_SSFC

The same chart, drawn:

stateDiagram-v2
    [*] --> Idle
    Idle  --> Fill  : go
    Fill  --> Drain : level_high
    Drain --> Done  : level_empty
    Done  --> Idle  : TRUE

Every arrow is one TRANSITION TO … WHEN … line, and the entry arrow is the INITIAL keyword. The picture adds nothing the text does not say — which is the point: an SSFC is meant to be read both ways.

Reading the syntax:

• SSFC / END_SSFC wrap the block, like FUNCTION_BLOCK / END_FUNCTION_BLOCK.
• VAR_INPUT / VAR_OUTPUT / VAR work identically to FUNCTION_BLOCK.
• One state carries the INITIAL keyword — it is active at startup.
• Each state declares outgoing transitions: TRANSITION TO <target> WHEN <guard-expression>;
• Guards are pure Boolean expressions evaluated against the pre-state (the value of all variables at the start of the current scan, before any lifecycle block has run — exactly like PRE(x) in a FUNCTION_BLOCK).

The scan model for SSFC extends the three-phase model (§2) to nine steps:

1  Snapshot pre-state          — PRE(x) reads from here for the whole scan
2  Evaluate all guards         — of active states and their superstates
3  Select transition           — at most one may fire per scan
4  Execute EX blocks           — of states being left, deepest-first
5  Update marking              — which state is now active
6  Reset T_elapsed             — newly entered states get T_elapsed = 0
7  Execute EN blocks           — of newly entered states, outermost-first
8  Execute DU blocks           — of ALL currently active states, outermost-first
9  Commit                      — outputs observable; becomes pre-state of next scan

If no guard is true in step 3, steps 4–7 are skipped; only DU runs (step 8).

21.2 Lifecycle blocks: EN, DU, EX

Every state may declare up to three lifecycle blocks. All are optional; a missing block is equivalent to an empty one.

Block	Runs when	Typical use
EN	Exactly once: the scan the state is entered (after the marking update, before DU)	Set an output TRUE on entry; arm a timer; increment a counter
DU	Every scan the state is active (including the entry scan, after EN)	Continuous feedback; outputs that depend on sensor readings; T_elapsed-based values
EX	Exactly once: the scan the state is left (before the marking update)	Reset outputs that EN set; latch a result before leaving

STATE Heat
  EN:
    heater       := TRUE;
    alarm_active := FALSE;
  DU:
    heat_warn    := Heat.T_elapsed >= HEAT_WARN_D;
    alarm_active := alarm_active OR temp_exceeded;
  EX:
    heater       := FALSE;
    heat_warn    := FALSE;
  TRANSITION TO Hold WHEN temp_reached;
END_STATE

• EN turns on the heater. Because heater is register-backed, it holds TRUE across scans until something writes FALSE. No DU rule is needed to sustain it.
• DU recomputes heat_warn every scan: it becomes TRUE once the state has been active for at least HEAT_WARN_D. It also accumulates alarm_active.
• EX clears both outputs in the same scan the state is left, so the next state inherits a clean slate.

PRE(x) vs. direct read inside lifecycle blocks: EX blocks run before EN blocks in the same scan. A direct read of x inside EN sees any value that EX already wrote. PRE(x) always reads the step-1 snapshot, regardless of what earlier lifecycle blocks wrote. The rule: use PRE(x) for "the value this scan began with"; use direct x for "what the current scan's earlier lifecycle blocks produced."

21.3 Implicit fields: State.X and State.T_elapsed

Every state S exposes two read-only fields available in any lifecycle block or transition guard in the same SSFC:

S.X : BOOL — TRUE iff S is currently active. Useful in DU blocks of a parent superstate, in guards of sibling states, or in the rules of a composed FUNCTION_BLOCK.

S.T_elapsed : TIME — The elapsed time since S was most recently entered. Zero in the entry scan; increments by DT (the scan cycle time) each subsequent scan. Reading T_elapsed of an inactive state is a static error.

STATE Hold
  DU:
    heater        := Hold.T_elapsed < HOLD_TIME;
    hold_ok_light := Hold.T_elapsed >= HOLD_CONFIRM;
  TRANSITION TO Drain WHEN Hold.T_elapsed >= HOLD_TIME;
END_STATE

The compiler treats T_elapsed as a symbolic TIME accumulator. Timing properties derived from it are verified for all consistent scan rates, not for a fixed rate — the same approach as the HELD/ELAPSED predicates in §7.

21.4 Superstates and preemption

A superstate groups child states under a shared parent. Its lifecycle blocks run whenever any child is active. More importantly, a transition declared directly on the superstate is a preemption transition: it fires from any active child, without knowing which one.

SUPERSTATE Production
  INITIAL STATE Fill
    EN:  valve_fill := TRUE;
    EX:  valve_fill := FALSE;
    TRANSITION TO Heat WHEN level_high;
  END_STATE
  STATE Heat
    EN:  heater := TRUE;
    EX:  heater := FALSE;
    TRANSITION TO Hold WHEN temp_reached;
  END_STATE
  STATE Hold
    DU:  heater := Hold.T_elapsed < HOLD_TIME;
    TRANSITION TO Drain WHEN Hold.T_elapsed >= HOLD_TIME;
  END_STATE
  STATE Drain
    EN:  valve_drain := TRUE;
    EX:  valve_drain := FALSE;
    TRANSITION TO Completed WHEN level_empty;
  END_STATE
  TRANSITION TO SafeStopped WHEN abort;    -- preempts ANY of the four children
END_SUPERSTATE

stateDiagram-v2
    state Production {
        [*] --> Fill
        Fill  --> Heat  : level_high
        Heat  --> Hold  : temp_reached
        Hold  --> Drain : T_elapsed >= HOLD_TIME
        Drain --> Completed : level_empty
    }
    Production --> SafeStopped : abort

The one arrow that leaves the box rather than a state inside it is the preemption: it has no source state because it fires from any of them.

TRANSITION TO SafeStopped WHEN abort is checked every scan regardless of which child is active. When abort is TRUE, the entire Production superstate is left: the active child's EX fires, then Production's EX fires (if declared), then SafeStopped's EN fires — all in the same scan.

Priority rule: a superstate's own transitions always have higher implicit priority than any child transition in the same scan. If Fill's level_high guard and Production's abort guard are both TRUE simultaneously, the abort transition is selected.

LCA-based EX/EN ordering: When a transition fires, the compiler computes the Lowest Common Ancestor (LCA) of the source and target states. EX blocks fire from the source up to (but not including) the LCA, deepest-first. EN blocks fire from the LCA down to the target, outermost-first. This mirrors a stack-unwind/push pattern: nested context is removed before new context is added.

21.5 Parallel regions and synchronisation

A superstate may contain parallel regions — two or more independent sub-machines that run concurrently while the superstate is active.

SUPERSTATE Calibrate
  PARALLEL
    REGION arm_a
      INITIAL STATE A_Move
        EN:  joint_a := TRUE;
        EX:  joint_a := FALSE;
        TRANSITION TO A_Done WHEN a_at_position;
      END_STATE
      STATE A_Done END_STATE
    END_REGION
    REGION arm_b
      INITIAL STATE B_Move
        EN:  joint_b := TRUE;
        EX:  joint_b := FALSE;
        TRANSITION TO B_Done WHEN b_at_position;
      END_STATE
      STATE B_Done END_STATE
    END_REGION
    JOIN FROM A_Done, B_Done TO Ready;
  END_PARALLEL
  TRANSITION TO Aborted WHEN emergency;
END_SUPERSTATE
STATE Ready
  EN: ready_light := TRUE;
  TRANSITION TO Idle WHEN NOT start;
END_STATE

stateDiagram-v2
    state Calibrate {
        state fork_c <<fork>>
        [*] --> fork_c
        fork_c --> A_Move
        fork_c --> B_Move
        A_Move --> A_Done : a_at_position
        B_Move --> B_Done : b_at_position
        state join_c <<join>>
        A_Done --> join_c
        B_Done --> join_c
    }
    join_c --> Ready
    Calibrate --> Aborted : emergency

The JOIN is the bar both regions must reach: Ready is entered only once both A_Done and B_Done are active. The emergency arrow again leaves the box, not a state — it preempts both regions at once.

• Entering Calibrate is a fork: both A_Move and B_Move activate in the same scan.
• Each region advances independently. A_Move may reach A_Done while B_Move is still moving.
• The JOIN fires in the first scan where both A_Done and B_Done are simultaneously active. It exits both regions atomically and enters Ready.
• TRANSITION TO Aborted WHEN emergency preempts both regions at once, just as a superstate preemption exits all child states in an exclusive SSFC.

Write-conflict rule: Two simultaneously-active regions must not write the same output variable in lifecycle blocks. The compiler rejects it: ssfc-cross-region-conflict.

21.6 What the compiler checks

python -m zqel batch_controller.zqel

The assurance report names eight claims:

Claim	What it verifies
C-SAF	1-Safeness: for every (region, transition) pair, token balance adds up. Exact.
C-INT	Region integrity: transitions stay within structural scope; parallel coverage is consistent. Exact.
C-DEAD	No leaf state is structurally stuck (zero outgoing transitions, no TERMINAL). Exact.
C-GUARD-SAT	Every WHEN guard is satisfiable over the type domain. SMT.
C-DET	No two guards of the same state can be simultaneously TRUE without PRIO. SMT.
C-DATA-DEAD	No guard is permanently FALSE. Environmental Waiting (EW) distinguished from deadlock. SMT.
C-REACH	Every state reachable via individually-SAT-satisfiable guard sequence. SMT.
C-HOME	Per-place witness path to a nominated home state found. Over-approximation: PASS ≠ guaranteed return-to-home. SMT.

For an EW verdict on a transition: the machine is correctly waiting for a VAR_INPUT to change — that is not a bug. A WARN on C-HOME for a state in a parallel region means the per-place BFS found no witness path; this is a sound indicator but does not constitute a formal deadlock proof.

Add TERMINAL to a state that is intended to be a valid resting point with no outgoing transitions:

STATE Completed TERMINAL
END_STATE

21.7 Composing components with WIRING

An SSFC can host a child component — a FUNCTION_BLOCK or another SSFC — as a wired sub-controller. There is exactly one WIRING block per POU, at the SSFC's own level. It is not written inside a state, and it is not a call: it declares connections that exist in every scan.

SSFC PasteurizerSequence
  VAR_INPUT
    temp_actual : MATHREAL;
    abort       : BOOL;
  END_VAR
  VAR_OUTPUT
    heater_cmd  : MATHREAL;
  END_VAR
  VAR
    pid : PID_Temperature;
  END_VAR

  WIRING
    pid(
      setpoint := HEAT_SETPOINT,
      actual   := temp_actual,
      enable   := Heat.X          (* only while Heat is the active state *)
    );
    heater_cmd := pid.output;
  END_WIRING

  INITIAL STATE Heat
    TRANSITION TO Hold WHEN temp_reached;
  END_STATE

  STATE Hold
    TRANSITION TO Drain WHEN Hold.T_elapsed >= HOLD_TIME;
  END_STATE
END_SSFC

What WIRING does:

• The child instance pid runs every scan, not only while some state is active. What a state controls is the value wired to the child — here enable := Heat.X, which is FALSE whenever Heat is not active.
• Bindings are written as child(port := expr, …) for inputs and parent_output := child.port for outputs.
• There is no __ssfc_dt port. Elapsed time is runtime-owned: every SSFC tracks scan duration against the runtime clock, and a parent forwards nothing.
• inst* (star-wiring): if the child has input ports whose names and types match signals already in scope, pid*; wires them. Explicit bindings take priority.

What WIRING does not do: it does not alter state machine execution or create a separate control thread. The child's scan is synchronous with the parent's — one child update per parent scan — and its internal registers persist across scans like any FUNCTION_BLOCK.

21.8 Signal ownership analysis

When multiple states write the same output, the compiler cannot statically guarantee that exactly one writer is active at any moment. zqel's Write Ownership analysis resolves this at analysis time.

The Pasteurizer above writes heater_cmd in exactly one place — its WIRING block — so it needs no such analysis. The interesting case is a sequence whose states each set the same output themselves, say heater_cmd in Heat's DU, in Hold's DU, and in SafeStopped's EN. Run the analysis:

from zqel.ssfc_ownership import analyze_ownership

report = analyze_ownership(ssfc, net, mg)
for sig in report.all_signals():
    print(sig.name, sig.ownership_class)

Typical output:

heater_cmd   EXCLUSIVE_MULTI_WRITER

The result means: multiple states write heater_cmd, but the compiler has proved they cannot all be active in the same scan. Heat, Hold, and SafeStopped are in an exclusive hierarchy — at most one is active per scan — so no write conflict is possible.

This is also the reason to prefer one WIRING block over per-state writes where the choice exists: a single writer needs no proof of exclusivity at all.

OwnershipClass summary:

Class	Safe?	Meaning
SINGLE_WRITER	Yes	Only one write site exists.
EXCLUSIVE_MULTI_WRITER	Yes	Multiple sites; mutual exclusion formally proved.
COMPATIBLE_MULTI_WRITER	Yes	Co-activatable sites, but they write the same value.
CONFLICTING	No	Co-activatable sites write different values. Design error.
UNKNOWN	Review	Mutual exclusion could not be determined.

CONFLICTING is the only outcome that blocks CI (under the default policy). UNKNOWN is worth reviewing but is not a failure by default.

A transitive component effect is automatically traced when a WIRING block references State.X (the activity marker):

state activation → WIRING → child.input → (child FB) → child.output → parent output

These chains appear in report.component_effects and are analysed alongside direct variable writes. See concepts/ownership-and-effects.md for the full classification rules and how-to/audit-signal-ownership.md for the step-by-step workflow.

21.9 Recovery and progress analysis

Write Ownership proves which state writes an output. Recovery and Progress analysis proves whether the SSFC is guaranteed to reach a designated safe state from any reachable configuration.

The Pasteurizer has a natural recovery pair: from Production (any child active) to SafeStopped. Declare the environment's commitment as an ASSUME clause, then run the analysis:

ASSUME abort;   (* safety interlock: abort stays asserted once raised *)

from zqel.ssfc_recovery import analyze_recovery, render_claim_md
from zqel.ssfc_marking import build_marking_graph

mg    = build_marking_graph(net)
claim = analyze_recovery("Production", "SafeStopped", ssfc, net, mg)
print(render_claim_md(claim))

The report has four independent claim levels:

STRUCTURAL   ✓ PROVED
             path: Production → SafeStopped (1 transition)

POSSIBLE     ✓ PROVED
             per-edge SAT path: abort is satisfiable

GUARANTEED   ≈ PROVED-CONDITIONAL
             all admissible executions reach SafeStopped
             requires: ASSUME abort

BOUNDED      ≈ PROVED-CONDITIONAL
             within 1 scan (worst-case attractor rank)
             requires: ASSUME abort

Reading the levels:

• STRUCTURAL checks the marking-graph topology, ignoring all guards. It confirms a path exists at all.
• POSSIBLE checks that a guard-satisfiable path exists (per-edge SAT). It does not prove all executions take that path.
• GUARANTEED proves that every admissible execution from Production eventually reaches SafeStopped. PROVED-CONDITIONAL means this holds given the declared ASSUMEs; without them the guard abort might never be TRUE and the system could remain in Production indefinitely.
• BOUNDED gives the worst-case number of scans. If the scan cycle is 10 ms and BOUNDED = 1, the guaranteed recovery time is at most 10 ms.

The assumptions_used field (on the GUARANTEED evidence) lists only the ASSUME clauses that are load-bearing — those whose removal causes GUARANTEED to fail. Non-contributing ASSUMEs are excluded.

A second pair, SafeStopped → Idle, depends on an operator action (reset_request). With no ASSUME for it, GUARANTEED is NOT PROVED — which is the correct result: the system can reach Idle (POSSIBLE = PROVED), but no external contract guarantees it ever will. This is not a bug; it is an accurate characterisation of an operator-triggered transition.

For the full step-by-step workflow — choosing states, when to add ASSUMEs, and how to interpret NOT PROVED — see how-to/prove-safe-recovery.md.

---