How to Model a Sequential Machine with SSFC¶

Goal: Write a working SSFC for a controller that has named operational phases, phase-specific outputs, and timed or condition-based transitions.\ Requires: familiarity with the basic LoLa FUNCTION_BLOCK (see the Introduction by Example through §10).

The pattern in one sentence¶

Identify the operational phases of your controller, name them as states, declare what each phase does in lifecycle blocks (EN on entry, DU per scan, EX on exit), and write transitions for when to move between phases.

Mental model: lifecycle as a gate, not a language¶

Each STATE is a LoLa computation context gated by the SSFC marking. The expression language inside EN, DU, and EX is identical to what you write in a FUNCTION_BLOCK — arithmetic, boolean logic, PRE(), EXTERN function calls, output rules. The lifecycle hooks control only when those computations execute:

Block	Runs when	Typical use
`EN`	Entry scan — once	Arm outputs, initialise accumulators, reset timers
`DU`	Every active scan (incl. entry)	Sensor-driven outputs, `T_elapsed`-based logic, PRE()-based accumulation
`EX`	Exit scan — once	De-arm outputs, save values for the next state's EN to see

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

Step 1 — Name your phases¶

Draw a state diagram on paper (or in your head) before touching the keyboard.

For a batch pasteurisation controller the phases are:

Idle → Fill → Heat → Hold → Drain → Completed → Idle
                                  ↑ abort
                             SafeStopped

Each arrow is a transition condition: - Idle → Fill: start input goes HIGH - Fill → Heat: level_high sensor goes HIGH - Heat → Hold: temp_reached sensor goes HIGH - Hold → Drain: Hold.T_elapsed >= HOLD_TIME (timed) - Drain → Completed: level_empty sensor goes HIGH - Completed → Idle: after one scan (done signal delivered) - any Production child → SafeStopped: abort goes HIGH (preemption)

Step 2 — Write the SSFC skeleton¶

SSFC BatchController
  VAR_INPUT
    start         : BOOL;
    level_high    : BOOL;
    level_empty   : BOOL;
    temp_reached  : BOOL;
    abort         : BOOL;
    reset         : BOOL;
  END_VAR
  VAR_OUTPUT
    valve_fill  : BOOL;
    valve_drain : BOOL;
    heater      : BOOL;
    done_signal : BOOL;
  END_VAR
  VAR
    batch_count : INT;
  END_VAR

  INITIAL STATE Idle
    TRANSITION TO Fill WHEN start;
  END_STATE

  SUPERSTATE Production
    -- states go here (Fill, Heat, Hold, Drain)
    TRANSITION TO SafeStopped WHEN abort;
  END_SUPERSTATE

  STATE Completed
    TRANSITION TO Idle WHEN TRUE;
  END_STATE

  STATE SafeStopped
    TRANSITION TO Idle WHEN reset AND NOT abort;
  END_STATE
END_SSFC

Note how Fill, Heat, Hold, Drain are children of Production. This is why the abort preemption only needs to appear once: TRANSITION TO SafeStopped WHEN abort on the superstate fires from any of its active children.

Step 3 — Fill in lifecycle blocks¶

Lifecycle blocks let each state manage its own outputs without scattering phase-specific assignments across the entire file.

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
    PARAMETER HOLD_TIME : TIME; END_PARAMETER   -- or VAR/PARAMETER at SSFC level
    EN:
      heater := TRUE;
    DU:
      heater := Hold.T_elapsed < HOLD_TIME;     -- turns off automatically
    EX:
      heater := FALSE;
    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;
END_SUPERSTATE

STATE Completed
  EN:
    done_signal := TRUE;
    batch_count := PRE(batch_count) + 1;
  DU:
    done_signal := FALSE;        -- clear after one scan
  TRANSITION TO Idle WHEN NOT done_signal;
END_STATE

STATE SafeStopped
  EN:
    valve_fill  := FALSE;  valve_drain := FALSE;
    heater      := FALSE;
  DU:
    done_signal := FALSE;
  TRANSITION TO Idle WHEN reset AND NOT abort;
END_STATE

Rules of thumb for lifecycle blocks:

EN sets outputs that should be active immediately on entry and persist until explicitly cleared. Register-backed values hold across scans once set.
EX clears outputs that should stop when the state is left. Because EX runs before the marking changes, the cleared value is seen by the next state's EN in the same scan.
DU handles outputs that need to be recomputed every scan (feedback signals, accumulated values, outputs that depend on State.T_elapsed).
PRE(x) inside any lifecycle block reads the start-of-scan value. Use it when you need "the value before this scan's lifecycle blocks ran" — for example, batch_count := PRE(batch_count) + 1 adds 1 to the value from the previous scan.

Step 4 — Add a PARAMETER block for configuration values¶

Times, thresholds, and other deployment-time constants belong in PARAMETER, not VAR:

SSFC BatchController
  PARAMETER
    HOLD_TIME    : TIME;    -- default can be added: TIME := 120_000ms;
    HEAT_WARN_D  : TIME;
    HOLD_CONFIRM : TIME;
  END_PARAMETER
  ...

PARAMETER values are fixed at configuration time, not at runtime. They participate in the compiler's proof: a transition guard like Hold.T_elapsed >= HOLD_TIME is provably satisfiable because HOLD_TIME is a positive TIME (the compiler checks this).

Step 5 — Add SSFC assurance annotations¶

Before running the compiler, annotate the SSFC with assurance contracts. These are optional but strongly recommended for safety-critical controllers.

State invariants (C-INV)¶

An INVARIANT inside a state declares a property the compiler must prove holds whenever that state is active. Z3 checks SAT(¬φ) over the type domain; UNSAT is a proof:

STATE Hold
  INVARIANT heater = TRUE OR Hold.T_elapsed >= HOLD_TIME;
  DU:
    heater := Hold.T_elapsed < HOLD_TIME;
  TRANSITION TO Drain WHEN Hold.T_elapsed >= HOLD_TIME;
END_STATE

Bounded response (C-WITHIN)¶

WITHIN on a transition declares that the guard must become satisfiable within a stated time bound. The compiler checks this is Z3-consistent with the state's invariants:

STATE Heat
  TRANSITION TO Hold WHEN temp_reached WITHIN 30_000ms;
END_STATE

Environment contracts (C-ASSUME)¶

ASSUME at SSFC level declares a property the environment guarantees. The clause is wired into every Z3 query as an additional premise, tightening the proofs:

SSFC BatchController
  VAR_INPUT level_high : BOOL; level_empty : BOOL; temp_reached : BOOL; END_VAR
  ASSUME NOT (level_high AND level_empty);   -- sensors are mutually exclusive
  ...

Structural liveness (C-LIVE)¶

LIVENESS FROM S EVENTUALLY T; causes the compiler to verify (via exact marking BFS) that a T-containing marking is reachable from any S-containing marking:

SSFC BatchController
  LIVENESS FROM Idle EVENTUALLY Completed;
  LIVENESS FROM SafeStopped EVENTUALLY Idle;
  ...

Step 6 — Run the assurance check¶

python -m lola batch_controller.lola

The compiler reports structural, SMT, and (with assurance annotations) marking-graph assurance claims. For a correctly written SSFC:

C-SAF             PASS  1-safeness: token balance verified for all 8 transitions
C-INT             PASS  region integrity: all transition sources/targets consistent
C-DEAD            PASS  no structural deadlock (7 atomic states checked)
C-GUARD-SAT       PASS  all 7 guards satisfiable
C-DET             PASS  no ambiguous guard pairs
C-DATA-DEAD       EW    Idle.WHEN start: environmental waiting (VAR_INPUT)
C-REACH           PASS  all 7 states reachable from initial marking
C-HOME            PASS/WARN  ...
C-NO-STUCK-MARKING PASS  no deadlock in 8 reachable markings
C-REVERSI         PASS  all markings can return to initial
C-INV             PASS  2 state invariants proved
C-WITHIN          PASS  Heat→Hold bounded within 30 000 ms
C-ASSUME          PASS  environment contract acknowledged
C-LIVE            PASS  Idle→Completed, SafeStopped→Idle

EW (Environmental Waiting) on Idle.WHEN start is correct and expected: the machine waits for the operator to press start. That is not a deadlock.

If C-DEAD fires on a state you intended to be a final state, add TERMINAL:

STATE Done TERMINAL
  -- no outgoing transition needed; TERMINAL suppresses C-DEAD
END_STATE

Getting a full engineering report¶

from lola.parser import parse_ssfc
from lola.sema_ssfc import analyze_ssfc
from lola.ssfc_net import build_net
from lola.ssfc_report import check_all
from lola.ssfc_report_md import generate_engineering_report

ssfc = parse_ssfc(open("batch_controller.lola").read())
syms = analyze_ssfc(ssfc)
net  = build_net(ssfc)
report = check_all(net, syms, ssfc=ssfc)
print(generate_engineering_report(report, source_ref="batch_controller.lola"))

The engineering report emits a Markdown document with a claim evidence table (one row per claim, showing verdict, evidence strength, and layer provenance), a marking-graph summary, and a detailed failures-and-warnings section.

Step 7 — Emit code¶

python -m lola batch_controller.lola --target st     # Structured Text
python -m lola batch_controller.lola --target rust   # Rust

The generated code handles all lifecycle sequencing, marking updates, and T_elapsed increments. You do not write the sequencing code — the compiler derives it from the SSFC structure.

Common mistakes and diagnostics¶

Symptom	Likely cause	Fix
`ssfc-no-initial`	A region has no `INITIAL STATE` declaration	Add `INITIAL` keyword to one state
`ssfc-ambiguous-priority`	Two guards can be simultaneously true with no PRIORITY	Add `PRIO n` to the higher-priority transition
`ssfc-cross-region-conflict`	Two parallel regions write the same output variable	Route the write through a shared superstate DU block, or use separate output variables
`ssfc-unknown-join-source`	JOIN names a state that does not exist	Check the state name spelling
C-DEAD fires on an intended final state	Missing TERMINAL flag	Add `TERMINAL` keyword
C-DATA-DEAD fires unexpectedly	A guard uses a variable with no satisfying value	Check REQUIRE constraints or VAR type
C-REACH WARN on a state	The state has no path from the initial marking through SAT-satisfiable guards	Verify the transition chain; check if a preemption bypasses it
C-INV WARN on a state	INVARIANT φ is not Z3-provable; Z3 returned a satisfying assignment for ¬φ	Check the invariant expression and the state's lifecycle blocks
C-WITHIN WARN on a transition	Guard is not satisfiable within the declared time bound given current invariants	Increase the WITHIN bound or strengthen the state's INVARIANT
C-LIVE WARN on a LIVENESS declaration	No marking containing the target state is reachable from any marking containing the source	Check that a transition path exists from source to target state