SSFC Semantics — Why, What, and How¶

Audience: control-system engineer or language user who wants to understand why SSFC is designed the way it is — how it relates to IEC SFC and UML statecharts, why the 9-step scan model exists, and what the assurance claims actually prove.\ Reference: Language Reference §14 — SSFC\ Tutorial: Introduction by Example §21 — Sequential Control with SSFC

Why SSFC exists as a separate declaration form¶

LoLa's FUNCTION_BLOCK is a declarative value language: you state what outputs should hold, the compiler derives priorities and writes the code, the prover verifies invariants. This is the right tool for data-flow logic — "the brake must be off while the motor is running", "the alarm is on when pressure exceeds 40 bar AND temperature exceeds 80 °C".

Sequential control is different. "Fill the tank, then heat the contents, then hold at temperature for 120 s, then drain — and abort to a safe state at any time" is not naturally expressed as a set of output rules. If you encode it as rules you end up with a set of boolean phase-registers, a tangle of PRE()-based edge detectors to move between phases, and a proof obligation that only one phase-register is TRUE at a time. That obligation is real and mandatory, but you wrote it implicitly and the compiler has to guess it.

SSFC makes the sequential structure explicit: - States are named; exactly one is active per exclusive region at all times. The "one active at a time" invariant is not a user obligation — it is a structural fact, enforced by the marking semantics and verified by the C-SAF claim before any other analysis runs. - Transitions are declared with their guards; non-determinism must be resolved by explicit PRIORITY declarations or is rejected as a static error. - Lifecycle blocks (EN / DU / EX) replace the phase-register tangle with named hooks that the compiler sequences correctly.

The result is a program whose sequential structure is visible to reviewers, machine-checkable by the compiler, and unambiguous under the same synchronous semantics as the rest of LoLa.

The computation model: a state is a LoLa context¶

One principle governs the relationship between SSFC and the rest of LoLa:

LoLa describes computation. SSFC describes when that computation is active.

A STATE is not a restricted action language. It is a full LoLa computation context whose effect is gated by the SSFC marking. Conceptually:

STATE ≈  LoLa computation context
       + activation flag          (.X — TRUE when the state is in the marking)
       + elapsed time             (.T_elapsed — duration since last entry, ms)
       + three lifecycle-gated execution windows:
           EN   — runs in the entry scan, exactly once
           DU   — runs in every active scan (including the entry scan)
           EX   — runs in the exit scan, exactly once

The lifecycle hooks determine when the computation runs, not what language it speaks. Inside EN, DU, and EX bodies, the complete LoLa expression language is available: arithmetic and boolean expressions, comparisons, PRE(x), EXTERN function calls, user-defined pure functions, IF-THEN-ELSE, and output rules (var: ON WHEN cond; HOLD OTHERWISE;). Access to PARAMETER, VAR, VAR_INPUT, and VAR_OUTPUT variables and state fields (StateName.X, StateName.T_elapsed) is unrestricted.

The body of a lifecycle block consists of assignments (var := expr) and output rules — the same two statement forms that drive computation in FUNCTION_BLOCK bodies. EN, DU, and EX are windows into that same language, not a separate, smaller one.

What stays at the SSFC structural level: Sub-FB instance wiring (inst(Input := expr)) is a structural declaration, not a per-scan lifecycle concern. Sub-components are declared in the SSFC's VAR block; their output variables are readable anywhere, including inside lifecycle blocks. The distinction is: lifecycle bodies express what to compute in this phase; structural declarations express which components participate in the design.

SUPERSTATE and PARALLEL extend the same model hierarchically:

SUPERSTATE ≈  STATE
            + an exclusive sub-region (exactly one child active at a time)
            + optional preemption transitions (fire from any active child)

PARALLEL   ≈  SUPERSTATE
            + multiple concurrent sub-regions (AND-semantics)
            + JOIN declarations for synchronised exit

A SUPERSTATE's own EN/DU/EX hooks apply to the superstate level: EN fires when the superstate is entered (before the initial child's EN), EX fires when it is exited, DU runs every scan any child is active. The same lifecycle semantics apply uniformly at every nesting level.

Relation to IEC 61131-3 SFC¶

IEC 61131-3 Sequential Function Charts and LoLa SSFCs share the same graphical origin (Petri-net-inspired: places = steps, transitions = transitions, tokens = active marking), but differ in several ways:

	IEC SFC	LoLa SSFC
Action qualifiers	N / S / R / P / D / L (7 letter codes)	EN / DU / EX lifecycle blocks
Timing	Action qualifier D/L with separate timers	`State.T_elapsed` field, symbolic in proofs
Hierarchy	Non-standard / vendor extension	First-class SUPERSTATE nesting
Parallel regions	Explicit divergence/convergence	`PARALLEL` / `REGION` / `JOIN`
Determinism	Convention (priority not normative)	Structural: PRIORITY required, conflicts are errors
Formal semantics	Normative prose, no formal model	9-step scan model, SMT-verifiable
Proof	None defined	Structural + SMT assurance suite

The action-qualifier replacement is the sharpest design decision. IEC SFC's S (set) and R (reset) qualifiers modify a register across scans regardless of the action block's state — they are imperative updates to a shared variable. SSFC lifecycle blocks are declarative assignments within a single scan: EN runs in the entry scan, EX runs in the exit scan. The register persists because LoLa registers are register-backed (they hold their value until overwritten), not because the qualifier carries state. The effect is the same; the mechanism is consistent with the rest of LoLa.

Relation to UML Statecharts¶

UML statecharts (Harel 1987) introduced hierarchical states, orthogonal regions, history states, and entry/exit actions — the direct intellectual ancestors of SSFC.

LoLa SSFCs adopt hierarchy (SUPERSTATE) and orthogonal regions (PARALLEL / REGION) and entry/exit actions (EN / EX). They deliberately omit:

History states (H / H*): Require a persistent sub-marking that survives re-entry. This is not expressible in the current marking model without a separate register per history point. Deferred to a future version.
Internal transitions: UML "internal" transitions execute the action but do not fire EX/EN. SSFC does not have this concept; all transitions fire the full LCA-based EX/EN sequence.
Do-activities: UML "do" activities run concurrently with the state machine. SSFC DU blocks are synchronous — they execute in a fixed step of the scan.

The synchronous scan model is the fundamental difference from both IEC SFC and UML statecharts: SSFC executes in lock-step with the PLC scan cycle. There is no event queue, no concurrent thread of execution, no interrupt. Everything observable happens in one of the nine scan steps, in a fixed order, exactly once per scan. This is what makes formal verification tractable.

The 9-step scan model¶

Every SSFC scan executes exactly these nine steps, in this order. No step may be skipped or reordered.

Step 1   Pre-State Snapshot   — capture all register values; PRE(x) reads from here
Step 2   Guard Evaluation     — evaluate all WHEN guards of active states / superstates
Step 3   Transition Selection — select at most one transition (priority resolution)
Step 4   EX Phase             — exit lifecycle blocks, deepest-first
Step 5   Marking Update       — update state.X and T_elapsed bookkeeping
Step 6   T_elapsed Reset      — newly entered states get T_elapsed := 0
Step 7   EN Phase             — entry lifecycle blocks, outermost-first
Step 8   DU Phase             — during lifecycle blocks, outermost-first, ALL active states
Step 9   Commit               — atomically write all register values; outputs observable

If no transition fires (step 3), steps 4–7 are skipped and only step 8 (DU of all active states) runs before commit.

Why this order?

EX before EN before DU: EX de-arms outputs set by the outgoing state; EN arms outputs for the incoming state; DU runs after the new marking is settled. This matches the operator's mental model ("when I leave state A, A's cleanup runs; when I enter state B, B's setup runs; then B's per-scan logic runs").
Deepest-first EX, outermost-first EN: Mirrors undo/redo semantics. Exiting a deeply nested state means unwinding the stack from the bottom up (deepest EX first); entering a nested state means pushing the stack from top down (outermost EN first).
DU for ALL active states after EN: In the entry scan, DU runs after EN in the same scan. This means a value set by EN is immediately visible to DU in the entry scan — there is no "first scan DU gets the pre-state". This prevents a one-scan lag on newly entered states.
PRE(x) stays frozen from step 1: Inside any lifecycle block, PRE(x) reads the step-1 snapshot regardless of what earlier lifecycle blocks wrote. This makes PRE(x) a reliable "what was the value at the start of this scan" predicate. Direct reads see intra-scan writes; PRE reads do not.

Pre-State vs. direct read in lifecycle blocks¶

EX of A writes:    alarm := FALSE
EN of B reads:     alarm       →  FALSE  (direct: sees the EX write)
                   PRE(alarm)  →  old value  (snapshot from step 1)

Use PRE(x) to express "the value this scan began with." Use direct x to express "the value resulting from earlier lifecycle blocks in this scan."

This distinction matters most when EX clears an output (e.g., alarm := FALSE) and EN needs to decide whether to re-arm it. If EN uses PRE(alarm), it sees the pre-scan value (which may be TRUE); if it uses alarm, it sees the already-cleared value. The compiler does not choose for you — the semantics are precise and the difference is intentional.

LCA-based exit/entry traversal¶

The Lowest Common Ancestor (LCA) of the departing state S and the arriving state T determines which lifecycle blocks fire for a transition.

EX fires: S, parent(S), …, up to (but not including) LCA(S,T)  — deepest first
EN fires: LCA(S,T), …, down to T (but not including T itself's parent)  — outermost first

If S and T are in different branches of the same SUPERSTATE, the LCA is that superstate. If S and T are at the top level (different branches from the root), the LCA is the root and the full EX/EN chain fires.

Parent-level preemption fires the same LCA traversal regardless of which child S is currently active. The preemption transition declares its target T; the active child provides S; LCA(S, T) is computed at compile time.

For parallel regions: when a JOIN fires, the LCA is computed from the parallel superstate (which contains all the join-source regions). All active region leaves fire EX (in reversed-region/deepest-first order), then the parallel superstate exits, then the target state fires EN. A parent-level preemption on a parallel superstate similarly collects all active region leaves as the "departing states" and runs their EX before exiting the superstate.

The assurance model: what is and is not proved¶

The compiler produces a structured assurance report with eight named claims. Understanding what each one actually proves — and where the limits are — is critical for safety-case use.

Claims proved structurally (without SMT, purely by graph analysis)¶

C-SAF — 1-Safeness (P-invariant token balance). For every (region, transition) pair, the token delta matches the expected change: +1 when entering, −1 when exiting, 0 otherwise. This is checked for all transitions, including FORK (entering all regions) and JOIN (exiting all regions). Verdict is PASS or FAIL with the violating transition listed.

C-INT — Region integrity. For exclusive regions: every transition source/target is within the region's state set. For parallel superstates: every incoming/outgoing transition covers all regions consistently.

C-DEAD — Structural deadlock. Every non-TERMINAL atomic leaf state has at least one outgoing transition. A state with no outgoing transitions and no TERMINAL flag is structurally stuck. Note: this does not prove that the transition guard can ever be true — that is C-DATA-DEAD.

Claims proved by SMT (Z3 BitVec model, over-approximation)¶

C-GUARD-SAT — Guard satisfiability. Every guard is checked for satisfiability over the variable type domain (INT = 16-bit signed BitVec, TIME = 64-bit signed). A guard that is always FALSE is a dead transition and is flagged. The model uses declared REQUIRE constraints as assumptions.

C-DET — Determinism. For each state, no two outgoing guards are simultaneously satisfiable unless explicit PRIORITY declarations resolve the conflict. An ambiguous guard pair is a static error.

C-DATA-DEAD — Data deadlock and environmental waiting. Transitions that can never fire given variable types and REQUIRE constraints are flagged as data-dead. Guards that are not data-dead but can only fire when a VAR_INPUT has a specific value are classified as Environmental Waiting (EW) — the machine is correctly waiting for the environment, not stuck. EW is not an error; it is distinguished from deadlock.

C-REACH — Reachability. Forward BFS from the initial marking. A state is reachable if it is in the initial marking, or if there is a sequence of transitions to it where each transition's guard is satisfiable (individually — not simultaneously). For JOIN transitions, all source states must be reachable before the JOIN can fire. This is an over-approximation: reachability of each guard individually does not prove that the guards can fire in a sequence satisfying all ordering constraints.

C-HOME — Home-state possibility reachability (over-approximation). For a user-nominated set of home states H (e.g., {Idle}), the checker asks: "is there a path from state S back to some h ∈ H where each edge on the path is individually SAT-satisfiable?" A PASS warrant means such a per-edge-SAT witness path was found; a WARN warrant means no such path exists, suggesting the state may be unreachable from home or trapped.

C-HOME is an over-approximation (⟸ only). PASS does not mean: - That the sequence of guards along the witness path can all be true simultaneously or in the claimed order. - That all concurrent regions in a parallel superstate can simultaneously reach home (co-reachability across regions is not verified). - That the path from S to H is guaranteed to eventually fire in execution.

For exclusive regions (non-parallel SSFCs), the over-approximation is tight: each guard is checked independently and the path is a valid possible execution sequence. For parallel SSFCs, a state in region A may receive a PASS by a path that passes through region B's states via an abort-then-re-entry route; whether both regions can simultaneously follow that path is not verified.

Structural JOIN coverage (C-SYNC-DEAD)¶

This is a sub-check within the structural report (part of the C-INT family). For every JOIN declaration, each named source state must be either in the initial marking or reachable by at least one transition. A source that is never entered by any transition (a structural orphan) is flagged. This is orphan detection only — it does not prove that all sources can be simultaneously active (which would require co-reachability analysis).

When to use SSFC vs. FUNCTION_BLOCK¶

Use a FUNCTION_BLOCK when: - The logic is primarily value-based (combinational or registered outputs derived from inputs and state registers). - There are no distinct operational phases. - The "mode" logic is simple enough to express as HELD()/ELAPSED() predicates or a small set of boolean phase-registers without becoming tangled.

Use an SSFC when: - The controller has distinct operational phases that must be executed in sequence. - Phase transitions depend on conditions that may persist across multiple scans. - The same output variable should be handled differently in different phases (EN sets it, EX resets it, DU updates it per-scan based on sensors). - An emergency preemption must exit any sub-phase and go directly to a safe state. - Two or more concurrent sequences must proceed independently and synchronise at a barrier (JOIN).

You can mix both in the same project. An SSFC can use FUNCTION_BLOCKs as composed sub-components (§10 of the Language Reference), and SSFC outputs are valid inputs to FUNCTION_BLOCKs.