The door that pauses instead of reversing¶

A sectional door on a loading bay closes at about half a meter per second and weighs enough to matter. A photo-eye across the opening catches anything in the way. What the door does next is the whole of the safety function, and EN 13241 is specific about it: the door reverses. Stopping is not enough.

The difference shows up when the obstruction clears. A door that paused resumes closing, onto whatever moved.

The rungs¶

Reversing := (Reversing OR Beam) AND NOT TopLimit, MoveDown := CloseCmd AND NOT Beam AND NOT Reversing, MoveUp := OpenCmd OR Reversing. Reversing latches on the beam and holds until the top limit. The latch is the safety function. Everything else is plumbing.

file	what it is	size	sha256
`program.xml`	ladder program, PLCopen XML	3.8 KB	`f6673a537b31`
`momentary.xml`	ladder program, PLCopen XML	3.6 KB	`44a7408425fd`
`props.yaml`	property file	0.2 KB	`61809139c726`
`reversal_check.props.yaml`	property file	0.5 KB	`db727e6ab299`

The property everyone writes¶

benchmarks/building_automation/g_door_reversal/props.yaml

format_version: "0.1"
properties:
  - id: P1
    kind: invariant
    expression: "!(MoveDown && Beam)"
    justification: "The door never drives down while the photo-eye beam is broken."

Recorded 2026-09-04T23:40:39Z. Every build ran the same command.

cp benchmarks/building_automation/g_door_reversal/program.xml benchmarks/building_automation/g_door_reversal/program.ld
esbmc benchmarks/building_automation/g_door_reversal/program.ld --ld-props benchmarks/building_automation/g_door_reversal/props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 20s

Recorded 2026-09-04T23:40:39Z.

v8.4

cp benchmarks/building_automation/g_door_reversal/program.xml benchmarks/building_automation/g_door_reversal/program.ld
esbmc benchmarks/building_automation/g_door_reversal/program.ld --ld-props benchmarks/building_automation/g_door_reversal/props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 20s

build	ESBMC	verdict	expected	outcome	ingestion gate	cpu
v8.4	8.4.0	`SAFE`	`SAFE`	correct	pass	0.018 s

v8.4 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.

v8.4

     1: IF !1 THEN GOTO 2
        ASSIGN CloseCmd=NONDET(_Bool);
        ASSIGN OpenCmd=NONDET(_Bool);
        ASSIGN Beam=NONDET(_Bool);
        ASSIGN TopLimit=NONDET(_Bool);
        ASSIGN MoveUp=1 && OpenCmd;
        ASSIGN MoveUp=1 && Reversing;
        ASSIGN MoveDown=1 && CloseCmd && !Beam && !Reversing;
        ASSIGN Reversing=1 && Reversing && !TopLimit;
        ASSIGN Reversing=1 && Beam && !TopLimit;
        GOTO 1
     2:

The variant beside it drops the self-hold branch, leaving Reversing := Beam AND NOT TopLimit. Reversal now lasts exactly as long as the obstruction does.

Predict the verdict

The reversal is momentary: it ends when the beam clears. Does the door still refuse to drive down through a broken beam?

Answer

build	verdict	expected	ingestion gate
v8.4	`SAFE`	`SAFE`	pass

NOT Beam sits in the drive-down rung directly, so the property holds whatever the latch does. It is true of a door that reverses and true of a door that pauses and resumes, which are different machines with different accident reports.

The discriminator¶

benchmarks/building_automation/g_door_reversal/reversal_check.props.yaml

# Discriminator, not a safety requirement. EN 13241 asks for a reversal that carries the
# door back to open, not a pause. A latched reversal keeps running after the obstruction
# has cleared, which refutes this; a momentary one proves it and resumes closing.
format_version: "0.1"
properties:
  - id: P1
    kind: invariant
    expression: "!Reversing || Beam"
    justification: "Reversal lasts only while the beam is broken. A latched reversal must refute this."

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

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

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

master

cp benchmarks/building_automation/g_door_reversal/program.xml benchmarks/building_automation/g_door_reversal/program.ld
esbmc benchmarks/building_automation/g_door_reversal/program.ld --ld-props benchmarks/building_automation/g_door_reversal/reversal_check.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`	`VIOLATION`	`VIOLATION`	correct	pass	0.017 s

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 22
        ASSIGN CloseCmd=NONDET(_Bool);
        ASSIGN OpenCmd=NONDET(_Bool);
        ASSIGN Beam=NONDET(_Bool);
        ASSIGN TopLimit=NONDET(_Bool);
        ASSIGN Reversing__prev=1 && Reversing;
        IF !1 THEN GOTO 2
        ASSIGN pf12=0;
     2: IF !(1 && Reversing__prev) THEN GOTO 3
        ASSIGN pf12=1;
     3: IF !1 THEN GOTO 4
        ASSIGN pf11=0;
     4: IF !(1 && OpenCmd) THEN GOTO 5
        ASSIGN pf11=1;
     5: IF !1 THEN GOTO 6
        ASSIGN MoveUp__pf0=0;
     6: IF !(1 && pf12) THEN GOTO 7
        ASSIGN MoveUp__pf0=1;
     7: IF !(1 && pf11) THEN GOTO 8
        ASSIGN MoveUp__pf0=1;
     8: ASSIGN MoveUp=1 && MoveUp__pf0;
        IF !1 THEN GOTO 9
        ASSIGN pf7=0;
     9: IF !(1 && CloseCmd) THEN GOTO 10
        ASSIGN pf7=1;
    10: IF !1 THEN GOTO 11
        ASSIGN pf8=0;
    11: IF !(1 && pf7 && !Beam) THEN GOTO 12
        ASSIGN pf8=1;
    12: IF !1 THEN GOTO 13
        ASSIGN pf9=0;
    13: IF !(1 && pf8 && !Reversing__prev) THEN GOTO 14
        ASSIGN pf9=1;
    14: ASSIGN MoveDown=1 && pf9;
        IF !1 THEN GOTO 15
        ASSIGN pf4=0;
    15: IF !(1 && Beam) THEN GOTO 16
        ASSIGN pf4=1;
    16: IF !1 THEN GOTO 17
        ASSIGN pf3=0;
    17: IF !(1 && Reversing__prev) THEN GOTO 18
        ASSIGN pf3=1;
    18: IF !1 THEN GOTO 19
        ASSIGN pf5=0;
    19: IF !(1 && pf4 && !TopLimit) THEN GOTO 20
        ASSIGN pf5=1;
    20: IF !(1 && pf3 && !TopLimit) THEN GOTO 21
        ASSIGN pf5=1;
    21: ASSIGN Reversing=1 && pf5;
        GOTO 1
    22:

Counterexample. ESBMC's own output. A trace long enough to need it is elided in the middle, and the omission is marked and counted where it happens.

master

State 1  thread 0
----------------------------------------------------
  Beam = 1

State 2  thread 0
----------------------------------------------------
  TopLimit = 0

State 3  thread 0
----------------------------------------------------
  Reversing = 1

State 5  thread 0
----------------------------------------------------
  Beam = 0

State 6  thread 0
----------------------------------------------------
  TopLimit = 0

State 7  thread 0
----------------------------------------------------
  Reversing__prev = 1

State 8  thread 0
----------------------------------------------------
  Reversing = 1

State 9 file benchmarks/building_automation/g_door_reversal/program.ld thread 0
----------------------------------------------------
Violated property:
  file benchmarks/building_automation/g_door_reversal/program.ld
  P1
  !Reversing || Beam


** Results:
  NOT CHECKED  [global.assertion.1]  line 0  unwinding assertion loop 1
benchmarks/building_automation/g_door_reversal/program.ld
  FAILED       [global.assertion.2]  line 0  P1

** 1 of 2 properties failed, 1 not checked
   (this mode stops at the first violation; use --multi-property for a verdict on every property)

Commit to an answer before reading on.

Refuted, which is the right answer: a latched reversal outlives the beam.

It is worth knowing what a wrong answer here would look like. Lesson 1.4 sets out the flattening a ladder front end can apply to a coil fed by two parallel branches:

ASSIGN Reversing = 1 && Reversing && !TopLimit;
ASSIGN Reversing = 1 && Beam && !TopLimit;

The second assignment overwrites the first, the self-hold is gone, and what gets verified is the momentary door. Such a proof is sound about the program it built. That program is not the one in the file.

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

cp benchmarks/building_automation/g_door_reversal/momentary.xml benchmarks/building_automation/g_door_reversal/momentary.ld
esbmc benchmarks/building_automation/g_door_reversal/momentary.ld --ld-props benchmarks/building_automation/g_door_reversal/reversal_check.props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s

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

master

cp benchmarks/building_automation/g_door_reversal/momentary.xml benchmarks/building_automation/g_door_reversal/momentary.ld
esbmc benchmarks/building_automation/g_door_reversal/momentary.ld --ld-props benchmarks/building_automation/g_door_reversal/reversal_check.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 19
        ASSIGN CloseCmd=NONDET(_Bool);
        ASSIGN OpenCmd=NONDET(_Bool);
        ASSIGN Beam=NONDET(_Bool);
        ASSIGN TopLimit=NONDET(_Bool);
        ASSIGN Reversing__prev=1 && Reversing;
        IF !1 THEN GOTO 2
        ASSIGN pf10=0;
     2: IF !(1 && OpenCmd) THEN GOTO 3
        ASSIGN pf10=1;
     3: IF !1 THEN GOTO 4
        ASSIGN pf11=0;
     4: IF !(1 && Reversing__prev) THEN GOTO 5
        ASSIGN pf11=1;
     5: IF !1 THEN GOTO 6
        ASSIGN MoveUp__pf0=0;
     6: IF !(1 && pf10) THEN GOTO 7
        ASSIGN MoveUp__pf0=1;
     7: IF !(1 && pf11) THEN GOTO 8
        ASSIGN MoveUp__pf0=1;
     8: ASSIGN MoveUp=1 && MoveUp__pf0;
        IF !1 THEN GOTO 9
        ASSIGN pf6=0;
     9: IF !(1 && CloseCmd) THEN GOTO 10
        ASSIGN pf6=1;
    10: IF !1 THEN GOTO 11
        ASSIGN pf7=0;
    11: IF !(1 && pf6 && !Beam) THEN GOTO 12
        ASSIGN pf7=1;
    12: IF !1 THEN GOTO 13
        ASSIGN pf8=0;
    13: IF !(1 && pf7 && !Reversing__prev) THEN GOTO 14
        ASSIGN pf8=1;
    14: ASSIGN MoveDown=1 && pf8;
        IF !1 THEN GOTO 15
        ASSIGN pf3=0;
    15: IF !(1 && Beam) THEN GOTO 16
        ASSIGN pf3=1;
    16: IF !1 THEN GOTO 17
        ASSIGN pf4=0;
    17: IF !(1 && pf3 && !TopLimit) THEN GOTO 18
        ASSIGN pf4=1;
    18: ASSIGN Reversing=1 && pf4;
        GOTO 1
    19:

The momentary variant proves it, as it should, because here there is no latch to lose.

What to take from it¶

The discriminator was written to separate two designs, and it separates two toolchains for free, because any property sensitive to whether a latch still holds its value after the set condition has gone away is equally sensitive to whether the front end built a latch in the first place. A check that catches this class of defect in a plant program catches it in the verifier too. Write one even when you trust the code.