Skip to content

Two textbook rungs, transcribed

Tony Kuphaldt's Lessons In Electric Circuits teaches ladder logic the way most people first meet it: a forward/reverse starter with a cross-interlock, a fail-safe stop wired through normally-closed contacts. Both rungs are correct relay diagrams, drawn the way an electrician reads them, contacts and coils resolving together. Transcribe them into a scanned PLC program and both stay safe, but for a reason the relay diagram never needed, and an earlier version of the verifier got that reason wrong.

The interlock, as drawn

START_FWDM2_REV (NC)M1_FWDSTART_REVM1_FWD (NC)M2_REV

M1_FWD := START_FWD AND NOT M2_REV, M2_REV := START_REV AND NOT M1_FWD. On a relay panel this is airtight: the two coils and the two auxiliary contacts settle together, so whichever direction's demand contact closes first, its own coil energizes and the other direction's normally-closed contact opens before the second coil ever gets a chance. There is no "before". Contacts and coils are simultaneous.

file what it is size sha256
fwd_rev_interlock.xml ladder program, PLCopen XML 4.5 KB f6f091217062
props.yaml property file 0.2 KB 6003a3f456ff

The property, and the proof that it holds

benchmarks/motor_control/g_fwd_rev_interlock/props.yaml
format_version: "0.1"
properties:
  - id: P1
    kind: invariant
    expression: "!(M1_FWD && M2_REV)"
    justification: "Motor Short-Circuit Hazard: Forward and Reverse contactors must never be closed at the same time."

Recorded 2026-10-18T05:49:13Z. Every build ran the same command.

cp benchmarks/motor_control/g_fwd_rev_interlock/fwd_rev_interlock.xml benchmarks/motor_control/g_fwd_rev_interlock/fwd_rev_interlock.ld
esbmc benchmarks/motor_control/g_fwd_rev_interlock/fwd_rev_interlock.ld --ld-props benchmarks/motor_control/g_fwd_rev_interlock/props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 120s

Recorded 2026-10-18T05:49:13Z.

cp benchmarks/motor_control/g_fwd_rev_interlock/fwd_rev_interlock.xml benchmarks/motor_control/g_fwd_rev_interlock/fwd_rev_interlock.ld
esbmc benchmarks/motor_control/g_fwd_rev_interlock/fwd_rev_interlock.ld --ld-props benchmarks/motor_control/g_fwd_rev_interlock/props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 120s
build ESBMC verdict expected outcome ingestion gate cpu
paper-pin 8.5.0 03ad8f91af SAFE SAFE correct pass 0.029 s

paper-pin 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.

     1: IF !1 THEN GOTO 20
        ASSIGN START_FWD=NONDET(_Bool);
        ASSIGN START_REV=NONDET(_Bool);
        ASSIGN STOP=NONDET(_Bool);
        IF !1 THEN GOTO 2
        ASSIGN pf1=0;
     2: IF !(1 && START_FWD) THEN GOTO 3
        ASSIGN pf1=1;
     3: IF !1 THEN GOTO 4
        ASSIGN pf2=0;
     4: IF !(1 && M1_FWD) THEN GOTO 5
        ASSIGN pf2=1;
     5: IF !1 THEN GOTO 6
        ASSIGN pf3=0;
     6: IF !(1 && pf1 && !STOP) THEN GOTO 7
        ASSIGN pf3=1;
     7: IF !(1 && pf2 && !STOP) THEN GOTO 8
        ASSIGN pf3=1;
     8: IF !1 THEN GOTO 9
        ASSIGN pf4=0;
     9: IF !(1 && pf3 && !M2_REV) THEN GOTO 10
        ASSIGN pf4=1;
    10: ASSIGN M1_FWD=1 && pf4;
        IF !1 THEN GOTO 11
        ASSIGN pf6=0;
    11: IF !(1 && START_REV) THEN GOTO 12
        ASSIGN pf6=1;
    12: IF !1 THEN GOTO 13
        ASSIGN pf7=0;
    13: IF !(1 && M2_REV) THEN GOTO 14
        ASSIGN pf7=1;
    14: IF !1 THEN GOTO 15
        ASSIGN pf8=0;
    15: IF !(1 && pf6 && !STOP) THEN GOTO 16
        ASSIGN pf8=1;
    16: IF !(1 && pf7 && !STOP) THEN GOTO 17
        ASSIGN pf8=1;
    17: IF !1 THEN GOTO 18
        ASSIGN pf9=0;
    18: IF !(1 && pf8 && !M1_FWD) THEN GOTO 19
        ASSIGN pf9=1;
    19: ASSIGN M2_REV=1 && pf9;
        GOTO 1
    20:

k-induction proves the property at k = 2, and ESBMC proves it again, also at k = 2, on the C that MatIEC generates from the same file. Two independent routes, one answer: the two contactors are never closed together at the end of a scan.

What the scan cycle changes

A scanned program cannot evaluate two coils at once, so it evaluates them in order. The forward rung is drawn above the reverse rung, the runtime takes the drawing order, and the reverse rung's normally-closed M1_FWD contact reads the value the forward rung wrote a moment earlier in the same scan. Press both start buttons on one scan with the motor stopped: the forward coil energizes, and the reverse rung sees it and stays off. The interlock holds from the very first scan.

This benchmark used to carry the opposite label. An earlier ESBMC LD front end read every coil's previous-scan value, so on the first scan both interlock contacts saw false and both coils came on together. That counterexample was an artifact of the translator, not of the program (esbmc/esbmc#7352, fixed in #8036), and the label was corrected once two routes agreed that the property holds.

Predict the verdict

If the reverse rung were drawn above the forward rung, which contactor would win when both start buttons are pressed on one scan with the motor stopped?

Answer
build verdict expected ingestion gate
paper-pin SAFE SAFE pass

The reverse one. Safety does not depend on the order, but priority does. A relay panel gives the race to whichever contact physically closes first; a scanned program gives it to whichever rung comes first in the drawing, every time. That is a design decision the transcription makes silently, and it is worth stating in the program's documentation.

The fail-safe latch, and a property that would not parse

STARTTHERMAL_OVL (NC)STOP (NC)MOTOR_RUNMOTOR_RUN

MOTOR_RUN := (START OR MOTOR_RUN) AND THERMAL_OVERLOAD_NC AND STOP_NC. Both guard contacts are wired normally-closed, so a broken wire or a tripped overload reads as false and drops the seal-in the same way an active stop command would. This rung has no scan-order dependency: nothing here reads another coil's value, so there is no __prev to get stale.

file what it is size sha256
failsafe_motor_latch.xml ladder program, PLCopen XML 3.0 KB 3d16843f5bb5
g_failsafe_motor_latch_props.yaml property file 0.3 KB c3fb22b09d1e

The property the textbook's own language suggests is an implication: if the overload contact has opened, the motor must not be running.

!THERMAL_OVERLOAD_NC -> !MOTOR_RUN

ESBMC's --ld-props parser does not accept it:

ERROR: property 'P1': undeclared variable '!THERMAL_OVERLOAD_NC -> !MOTOR_RUN'

Not a spelling problem. -> is not in the grammar at all, so the whole right-hand side is swallowed as one malformed identifier. This is a different gap from the IEC-keyword trap in lesson 1.3's NOT/AND rejection, which is about spelling an operator the parser does have; -> is an operator the parser does not have, regardless of spelling, and no other property in this suite had exercised it before this one.

benchmarks/motor_control/g_failsafe_motor_latch/props.yaml
format_version: "0.1"
properties:
  - id: P1
    kind: invariant
    expression: "THERMAL_OVERLOAD_NC || !MOTOR_RUN"
    justification: "Fire Hazard: The motor coil must instantly de-energize if the hardware thermal overload relay physically trips (opening the NC circuit)."

De Morgan's law rewrites A -> B as !A || B, so !THERMAL_OVERLOAD_NC -> !MOTOR_RUN becomes THERMAL_OVERLOAD_NC || !MOTOR_RUN, the same statement without an implication in it.

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

cp benchmarks/motor_control/g_failsafe_motor_latch/failsafe_motor_latch.xml benchmarks/motor_control/g_failsafe_motor_latch/failsafe_motor_latch.ld
esbmc benchmarks/motor_control/g_failsafe_motor_latch/failsafe_motor_latch.ld --ld-props benchmarks/motor_control/g_failsafe_motor_latch/props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 20s

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

cp benchmarks/motor_control/g_failsafe_motor_latch/failsafe_motor_latch.xml benchmarks/motor_control/g_failsafe_motor_latch/failsafe_motor_latch.ld
esbmc benchmarks/motor_control/g_failsafe_motor_latch/failsafe_motor_latch.ld --ld-props benchmarks/motor_control/g_failsafe_motor_latch/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.017 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.

     1: IF !1 THEN GOTO 2
        ASSIGN START=NONDET(_Bool);
        ASSIGN THERMAL_OVERLOAD_NC=NONDET(_Bool);
        ASSIGN STOP_NC=NONDET(_Bool);
        ASSIGN MOTOR_RUN=1 && START && THERMAL_OVERLOAD_NC && STOP_NC;
        ASSIGN MOTOR_RUN=1 && MOTOR_RUN && THERMAL_OVERLOAD_NC && STOP_NC;
        GOTO 1
     2:

k-induction closes at k = 2. The rewrite is not a weaker property standing in for the original; it is the same formula, and the equivalence is checkable by hand from the truth table, which is the standard the workaround has to clear before it goes in the suite rather than around it.

What the pair says together

Two textbook rungs, two different lessons. The interlock shows that a verifier's model of the scan cycle has to match the runtime's: a translator that read previous-scan values reported a hazard the program does not have, and the fix was in the tool, not in the ladder. The fail-safe latch shows a natural, correct way to state a safety property that the property language cannot parse. Neither would have surfaced from reading the ladder diagram alone, and both surfaced from trying to prove something about it.

Reproducing has the commands.