Prove Safe Recovery

This guide walks through verifying that an SSFC is guaranteed to reach a designated safe state, and how quickly. The Pasteurizer is used as the running example throughout, with two queries:

• Production → SafeStopped (with ASSUME abort_signal)
• SafeStopped → Idle (no ASSUME for reset_request)

For the conceptual explanation of how GUARANTEED and BOUNDED are computed, see concepts/recovery-and-progress.md. For the normative claim level definitions, see reference/assurance.md.

---

Step 1: Choose source and home states

Decide which (source, home) pair to analyse. Common patterns:

• Fault recovery: source = fault or production state, home = safe or stopped state
• Reset sequence: source = safe state, home = idle or ready state
• Any reachable state to safe: source = initial state, home = safe terminal state

For the Pasteurizer:

• Source: Production — the normal running state
• Home: SafeStopped — the safe mode the system must reach on abort

A second query covers the subsequent reset path:

• Source: SafeStopped
• Home: Idle

---

Step 2: Declare ASSUME clauses only where justified

ASSUME clauses assert that the environment will keep a condition True. They are engineering commitments, not free assumptions. Add an ASSUME only when there is an external contract — a hardware interlock, a system-level safety requirement, or an operator procedure — that guarantees the condition.

SSFC PasteurizerSequence
  VAR_INPUT
    abort_signal  : BOOL;
    reset_request : BOOL;
  END_VAR
  ASSUME abort_signal;   (* external: safety interlock guarantees abort stays asserted *)
  ...

reset_request does not get an ASSUME here. It depends on operator action and no external contract guarantees it will ever become True.

Do not add ASSUME clauses to make GUARANTEED pass. A PROVED-CONDITIONAL result is only meaningful if the ASSUME reflects a real guarantee. A spurious ASSUME produces a proof that is technically valid but unsafe in practice.

---

Step 3: Run the recovery analysis

The analysis is available via analyze_recovery():

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

mg = build_marking_graph(net)

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

For the complete Pasteurizer report covering both queries:

from lola.ssfc_recovery import RecoveryReport, render_report_md

report = RecoveryReport(
    component="PasteurizerSequence",
    claims=[
        analyze_recovery("Production", "SafeStopped", ssfc, net, mg),
        analyze_recovery("SafeStopped", "Idle", ssfc, net, mg),
    ],
)
print(render_report_md(report))

---

Step 4: Read the four claim levels separately

Each claim level is an independent result. Do not collapse them into a single verdict.

Target report for Production → SafeStopped:

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

POSSIBLE     ✓ PROVED
             per-edge SAT path: abort_signal is satisfiable
             (over-approximation: guard satisfiability checked per transition)

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

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

Target report for SafeStopped → Idle:

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

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

GUARANTEED   ✗ NOT PROVED
             marking {safestopped} may idle without progressing to 'idle'.
             Add ASSUME to guarantee the relevant guard eventually becomes TRUE.

BOUNDED      ✗ NOT PROVED
             (requires GUARANTEED to hold)

What to do with each level:

Level	NOT PROVED means	Action
STRUCTURAL	No path in the state machine topology	Fix the state machine structure
POSSIBLE	No guard-feasible path	Check guards; they may be contradictory or the state may be unreachable
GUARANTEED	System may idle or diverge to a non-home state	Add ASSUME (if justified), or accept that GUARANTEED does not hold
BOUNDED	GUARANTEED does not hold	Fix GUARANTEED first

---

Step 5: Inspect assumptions_used

When GUARANTEED is PROVED-CONDITIONAL, assumptions_used lists only the ASSUME clauses that are actually needed for the proof to hold — the load-bearing assumes. Non-load-bearing clauses are excluded.

claim = analyze_recovery("Production", "SafeStopped", ssfc, net, mg)
print(claim.guaranteed.assumptions_used)
# ['abort_signal']

If an ASSUME clause you expected to be load-bearing does not appear in assumptions_used, it is not contributing to the GUARANTEED proof. It may still be needed for other reasons — POSSIBLE feasibility, other claims — but you can consider whether it is architecturally justified.

---

Step 6: Use BOUNDED for WCRT planning

bound_scans gives the worst-case number of scans to reach home, under GUARANTEED conditions:

print(claim.bounded.bound_scans)  # 1

This is the maximum number of scans in which the system is guaranteed to reach the home state, counting from the moment the abort signal becomes and remains asserted. It is a worst-case bound: the actual number may be less.

In safety planning: if the scan cycle is 10 ms and BOUNDED = 3, the guaranteed recovery time is at most 30 ms. This bound is only valid under the ASSUME conditions.

---

Step 7: Treat NOT PROVED as a design finding

GUARANTEED = NOT PROVED is not a solver failure. It means the analysis found a reachable marking from which the home state is not guaranteed to be reached. The reason field says what was found:

• "marking {X} may idle without progressing": the system can stall in marking X indefinitely if the relevant guard is never True. To fix: add an ASSUME for the guard (if there is an external guarantee), or restructure the SSFC so the guard becomes always True in this marking.
• "marking {X} reachable via admissible transitions and does not lead to home on all executions": a branch from X leads to a non-home sink. To fix: eliminate the non-home branch, or make the diverging transition guard impossible under ASSUMEs.

Do not add ASSUMEs blindly to pass GUARANTEED. If the system genuinely cannot be guaranteed to reach the home state — for example, SafeStopped → Idle depends on operator action — document this explicitly and rely on POSSIBLE instead.

---

Quick reference: POSSIBLE vs GUARANTEED

Scenario	POSSIBLE	GUARANTEED
Path exists and guard satisfiable	PROVED	NOT PROVED (no ASSUME)
Path exists, ASSUME covers all guards	PROVED	PROVED-CONDITIONAL
Path exists, guard is always True (tautological)	PROVED	PROVED
No structural path	NOT PROVED	NOT PROVED

The most important case: POSSIBLE = PROVED but GUARANTEED = NOT PROVED. This means the system can reach the safe state but is not required to on every execution. This is the normal situation for operator-triggered resets and similar environment-dependent transitions. It is not a bug; it is a correct characterisation of the system.