Memory and time together¶

Part 1 closes by putting the two halves together: a timer decides when something is wrong, a latch remembers it, and an operator clears it.

The circuit¶

A door obstruction that persists for three scans sets a latched alarm. An operator acknowledgement clears it. S and R are set and reset coils: unlike an output coil, they write only when power reaches them, and leave the variable alone otherwise.

file	what it is	size	sha256
`program.xml`	ladder program, PLCopen XML	3.3 KB	`9553ee0f55d6`
`props.yaml`	property file	0.2 KB	`b0fb335ad3a5`

The property and the run¶

benchmarks/elevator/g_timer_latch_mix/props.yaml

format_version: "0.1"
properties:
  - id: P1
    kind: invariant
    expression: "!(Alarm && Ack)"
    justification: "Acknowledge is dominant: the latched alarm and Ack never hold together."

Recorded 2026-08-28T18:37:10Z. Every build ran the same command.

cp benchmarks/elevator/g_timer_latch_mix/program.xml benchmarks/elevator/g_timer_latch_mix/program.ld
esbmc benchmarks/elevator/g_timer_latch_mix/program.ld --ld-props benchmarks/elevator/g_timer_latch_mix/props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s

Recorded 2026-08-28T18:37:10Z.

master

cp benchmarks/elevator/g_timer_latch_mix/program.xml benchmarks/elevator/g_timer_latch_mix/program.ld
esbmc benchmarks/elevator/g_timer_latch_mix/program.ld --ld-props benchmarks/elevator/g_timer_latch_mix/props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s

build	ESBMC	verdict	expected	outcome	ingestion gate	cpu
master	8.4.0 `0064c4ac`	`SAFE`	`SAFE`	correct	pass	0.016 s

master found its solution by the inductive step (k = 2).

What the front end encoded. The scan body as the solver receives it, branch guards kept. An assignment-only view hides the guards and makes a guarded accumulator read as a constant.

master

     1: IF !1 THEN GOTO 11
        ASSIGN Trig=NONDET(_Bool);
        ASSIGN Ack=NONDET(_Bool);
        IF !1 THEN GOTO 2
        ASSIGN pf3=0;
     2: IF !(1 && Trig) THEN GOTO 3
        ASSIGN pf3=1;
     3: ASSIGN T0__IN=1 && pf3;
        IF !T0__IN THEN GOTO 5
        IF !(T0__ET < T0__PT) THEN GOTO 4
        ASSIGN T0__ET=T0__ET + 1;
     4: GOTO 6
     5: ASSIGN T0__ET=0;
     6: ASSIGN T0__Q=T0__IN && T0__ET >= T0__PT;
        IF !(1 && T0__Q) THEN GOTO 7
        ASSIGN Alarm=1;
     7: IF !1 THEN GOTO 8
        ASSIGN pf8=0;
     8: IF !(1 && Ack) THEN GOTO 9
        ASSIGN pf8=1;
     9: IF !(1 && pf8) THEN GOTO 10
        ASSIGN Alarm=0;
    10: GOTO 1
    11:

Acknowledgement is dominant: the alarm and the acknowledgement never hold together.

Why it is dominant, and why that should worry you¶

Look at the encoding. A set coil is a guarded write:

IF !(1 && T0__Q) THEN GOTO 7
ASSIGN Alarm=1;
7: ...
IF !(1 && Ack) THEN GOTO 9
ASSIGN Alarm=0;

The set runs, then the reset runs, so the reset wins in any scan where both conduct. Reverse those two statements and the set would win, the alarm would survive its own acknowledgement, and the property would fail.

Nothing in the file asks for that order. As lesson 1.5 showed, the graphical front end takes the order of coils from std::unordered_map iteration whenever the right power rail does not enumerate them. This program happens to come out with the reset last. A file with one more contact in it might not.

So the verdict here is correct and the reason it is correct is an accident. If you depend on reset dominance, and safety circuits usually do, wire the right power rail so the order is written down, and state a property that fails if the order flips. That is the same discipline as lesson 1.2's discriminator, applied to time instead of topology.

End of Part 1¶

Eight lessons, and the pattern behind them is one sentence: a verdict describes the program the tool built, not the program you drew. Contacts and coils were safe ground. Parallel branches, rung order, timers and counters each gave a case where the two came apart, and in every one of them the encoding said so plainly while the verdict did not.