Audit Signal Ownership¶

Use this guide when you have an SSFC and need to answer: "Who controls this output, and is there a write conflict?" The analysis checks every signal written inside the SSFC, classifies each by whether co-active writers could disagree, and flags conflicts as design findings.

For the conceptual explanation of how the analysis works, see concepts/ownership-and-effects.md. For the normative OwnershipClass definitions, see reference/assurance.md.

Step 1: Run the ownership analysis¶

The analysis runs automatically as part of lola <file>.lola --target check. Its output appears in the --target check report under the heading Signal ownership. You do not need to call it separately.

For programmatic access — for example, from a test or a CI script — use the API directly:

from lola.ssfc_ownership import analyze_ownership, render_report_md
from lola.ssfc_marking import build_marking_graph

mg = build_marking_graph(net)
report = analyze_ownership(ssfc, syms, net, mg)
print(render_report_md(report))

Step 2: Read the ownership classification for each signal¶

The report groups signals by their OwnershipClass. For a PasteurizerSequence SSFC with signals heater_command, agitator, and safe, the report looks like this:

## Signal Ownership — PasteurizerSequence

### heater_command — EXCLUSIVE_MULTI_WRITER

  Write sites:
    Heating.DU       heater_command := pid.output
    SafeStopped.EN   heater_command := 0.0

  Mutual exclusion: PROVED
    Heating and SafeStopped are in mutually exclusive regions (verified by marking graph).

  conflict_free: yes

### agitator — CONFLICTING

  Write sites:
    Heating.DU       agitator := TRUE
    Cleaning.DU      agitator := FALSE

  Co-activation: possible (Heating and Cleaning not proved mutually exclusive)
  Value compatibility: different (TRUE vs FALSE)

  conflict_free: NO  ← design finding

### safe — SINGLE_WRITER

  Write site:
    SafeStopped.DU   safe := TRUE

What each classification means and what action is required:

Classification	What it means	Action required
`SINGLE_WRITER`	Exactly one write site; no conflict possible	None
`EXCLUSIVE_MULTI_WRITER`	Multiple writers; mutual exclusion proved by marking graph	None; safe
`COMPATIBLE_MULTI_WRITER`	Multiple co-activatable writers; all write the same value	None; safe
`CONFLICTING`	Co-activatable writers with differing values	Fix the design
`UNKNOWN`	Mutual exclusion could not be determined	Investigate further

In the Pasteurizer example: heater_command is safe because the marking graph proves Heating and SafeStopped cannot both be active; safe has a single writer and needs no further attention; agitator is the only signal that requires action.

Step 3: Fix a CONFLICTING classification¶

The agitator conflict arises because Heating.DU writes TRUE and Cleaning.DU writes FALSE, and the marking graph cannot rule out both states being active simultaneously. Three remediation options are available.

Option A: Structural fix — make the states mutually exclusive¶

If Heating and Cleaning can be placed in separate parallel regions or under a superstate hierarchy that enforces exclusion, the marking graph will detect that. Re-run lola <file>.lola --target check; if mutual exclusion is now provable, the classification becomes EXCLUSIVE_MULTI_WRITER and no further change is needed.

Option B: Value fix — make co-activatable writers agree¶

If both states must be co-activatable (for example, during the Heating→Cleaning transition the EX block of the exiting state and the EN block of the entering state both execute in the same scan), make the boundary assignments write the same value:

STATE Heating
  DU: agitator := TRUE;
  EX: agitator := TRUE;   (* same value as Cleaning.EN *)
END_STATE

STATE Cleaning
  EN: agitator := TRUE;   (* matches Heating.EX; runtime changes it after entry scan *)
  DU: agitator := FALSE;
END_STATE

Because Heating.EX and Cleaning.EN now agree, the classification for that transition boundary becomes COMPATIBLE_MULTI_WRITER. The DU bodies still write different values, so mutual exclusion of those phases must also be proved or the boundary agreement applied there too.

Option C: OutputRules for priority¶

If one writer must win unconditionally, use an OUTPUT_RULES block. Branches inside OUTPUT_RULES are evaluated in order and are mutually exclusive by the OutputRules semantics — only the first matching branch executes:

STATE Shared
  DU:
    OUTPUT_RULES agitator
      IF in_cleaning_phase THEN agitator := FALSE;
      OTHERWISE agitator := TRUE;
    END_OUTPUT_RULES;
END_STATE

Move the competing logic into a single state with OUTPUT_RULES so the tool can see that exactly one branch runs per scan.

Step 4: Read transitive component effects¶

The report also lists component effects — chains where a state's activity influences an output through a wired child component rather than through a direct assignment:

### Component effects

  Heating
    -> pid.enable (via WIRING: enable := Heating.X)
    -> pid.output (internal FB logic)
    -> heater_command (read in Heating.DU)

This tells you that heater_command is not only written directly in Heating.DU; its value depends on the PID block's internal computation, which is gated by Heating.X. When auditing heater_command, also audit the PID's behaviour during the Heating phase. A signal that looks like a SINGLE_WRITER at the direct-assignment level can still carry indirect influence from multiple states through wired components.

Step 5: Use conflict_free() as a CI gate¶

Add an assertion to your test suite or build pipeline to prevent CONFLICTING signals from being merged:

report = analyze_ownership(ssfc, syms, net, mg)
assert report.conflict_free(), (
    f"Signal write conflicts in {report.component}: "
    + ", ".join(s.signal for s in report.conflicts())
)

analysis_complete() is the stricter gate — it also requires that no signal is classified UNKNOWN:

assert report.conflict_free() and report.analysis_complete()

The project TOML policy can enforce both gates declaratively under [ssfc_assurance]:

[ssfc_assurance]
required_claims = ["C-SAF"]
allow_conflict = false
allow_unknown = false

When the policy file is present, lola <file>.lola --target check reads these keys and fails the build if either condition is violated, without requiring explicit assertions in tests.

When UNKNOWN is acceptable¶

UNKNOWN does not mean CONFLICTING. The analysis returns UNKNOWN when complex state guard conditions prevent the solver from determining mutual exclusion — not because a conflict has been found. Two courses of action are available:

Restructure the SSFC. Move states into a superstate hierarchy or separate parallel regions so that mutual exclusion is structurally obvious. The marking graph can then prove it without relying on guard conditions.
Accept UNKNOWN with documented rationale. If you can verify by inspection that the states cannot co-occur, set allow_unknown = true in the project policy and add a comment in the SSFC explaining why the states are exclusive.

Never set allow_conflict = true without documented justification. CONFLICTING signals have genuine write conflicts that will produce non-deterministic output values at runtime.