The gap between two contactors¶
A 30 kW pump motor draws six or seven times its rated current if you throw it straight onto the line. The wye-delta starter is the old answer: run the windings in star while the rotor gets moving, then reconnect them in delta for normal running. Three contactors, one changeover, and a hazard everybody in the trade knows. Close star and delta together and you have shorted the supply through the winding ends.
The rungs¶
Star := Call AND NOT StarDone, Delta := Call AND StarDone AND DeadDone. StarDone and DeadDone come from the changeover timer. The start and stop latch that
drives Call sits upstream and is the subject of lesson 1.4, so it is deliberately not
in this file; two rungs is the whole of the contactor selection.
| file | what it is | size | sha256 |
|---|---|---|---|
program.xml |
ladder program, PLCopen XML | 2.8 KB | cdd9bfe99115 |
no_deadtime.xml |
ladder program, PLCopen XML | 2.6 KB | 665abfd022dc |
props.yaml |
property file | 0.2 KB | e347ee93997f |
deadtime_check.props.yaml |
property file | 0.5 KB | d245d377774e |
The property everyone writes¶
format_version: "0.1"
properties:
- id: P1
kind: mutual_exclusion
variables: [Star, Delta]
justification: "Closing the star and delta contactors together shorts the supply through the winding ends."
Recorded 2026-09-04T23:40:50Z. Every build ran the same command.
cp benchmarks/motor_control/g_star_delta/program.xml benchmarks/motor_control/g_star_delta/program.ld
esbmc benchmarks/motor_control/g_star_delta/program.ld --ld-props benchmarks/motor_control/g_star_delta/props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 20s
Recorded 2026-09-04T23:40:50Z.
| 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.
Star carries NOT StarDone and delta carries StarDone, so exclusion is structural and
the proof is immediate. Now delete the dead-time term, so that delta closes on the same
signal that opens star.
Predict the verdict
Delta now closes the instant the star time expires. Are the two commands still mutually exclusive?
Answer
| build | verdict | expected | ingestion gate |
|---|---|---|---|
| v8.4 | SAFE |
SAFE |
pass |
They are. One rung has the contact and the other has its complement, and that is all mutual exclusion of the two coils ever asked for.
The discriminator¶
An open-transition starter opens star, waits for the arc to clear, and only then closes delta. During that wait the motor is called for and neither contactor is in. The window is deliberate. Ask whether it exists.
# Discriminator, not a safety requirement. An open-transition starter opens star, waits
# out the arc, and only then closes delta, so there is a window with the motor called for
# and neither contactor in. A starter that proves this has no dead time.
format_version: "0.1"
properties:
- id: P1
kind: invariant
expression: "Star || Delta || !Call"
justification: "Whenever the motor is called for, one of the two contactors is closed. An open transition must refute this."
Recorded 2026-08-28T18:37:10Z. Every build ran the same command.
cp benchmarks/motor_control/g_star_delta/program.xml benchmarks/motor_control/g_star_delta/program.ld
esbmc benchmarks/motor_control/g_star_delta/program.ld --ld-props benchmarks/motor_control/g_star_delta/deadtime_check.props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s
Recorded 2026-08-28T18:37:10Z.
| build | ESBMC | verdict | expected | outcome | ingestion gate | cpu |
|---|---|---|---|---|---|---|
| master | 8.4.0 0064c4ac |
VIOLATION |
VIOLATION |
correct | pass | 0.012 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.
1: IF !1 THEN GOTO 12
ASSIGN Call=NONDET(_Bool);
ASSIGN StarDone=NONDET(_Bool);
ASSIGN DeadDone=NONDET(_Bool);
IF !1 THEN GOTO 2
ASSIGN pf6=0;
2: IF !(1 && Call) THEN GOTO 3
ASSIGN pf6=1;
3: IF !1 THEN GOTO 4
ASSIGN pf7=0;
4: IF !(1 && pf6 && StarDone) THEN GOTO 5
ASSIGN pf7=1;
5: IF !1 THEN GOTO 6
ASSIGN pf8=0;
6: IF !(1 && pf7 && DeadDone) THEN GOTO 7
ASSIGN pf8=1;
7: ASSIGN Delta=1 && pf8;
IF !1 THEN GOTO 8
ASSIGN pf3=0;
8: IF !(1 && Call) THEN GOTO 9
ASSIGN pf3=1;
9: IF !1 THEN GOTO 10
ASSIGN pf4=0;
10: IF !(1 && pf3 && !StarDone) THEN GOTO 11
ASSIGN pf4=1;
11: ASSIGN Star=1 && pf4;
GOTO 1
12:
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.
State 1 thread 0
----------------------------------------------------
Call = 1
State 2 thread 0
----------------------------------------------------
StarDone = 1
State 3 thread 0
----------------------------------------------------
DeadDone = 0
State 4 thread 0
----------------------------------------------------
Delta = 0
State 5 thread 0
----------------------------------------------------
Star = 0
State 6 file benchmarks/motor_control/g_star_delta/program.ld thread 0
----------------------------------------------------
Violated property:
file benchmarks/motor_control/g_star_delta/program.ld
P1
Star || Delta || !Call
** Results:
benchmarks/motor_control/g_star_delta/program.ld
FAILED [global.assertion.1] line 0 P1
** 1 of 1 properties failed
Recorded 2026-08-28T18:37:09Z. Every build ran the same command.
cp benchmarks/motor_control/g_star_delta/no_deadtime.xml benchmarks/motor_control/g_star_delta/no_deadtime.ld
esbmc benchmarks/motor_control/g_star_delta/no_deadtime.ld --ld-props benchmarks/motor_control/g_star_delta/deadtime_check.props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s
Recorded 2026-08-28T18:37:09Z.
cp benchmarks/motor_control/g_star_delta/no_deadtime.xml benchmarks/motor_control/g_star_delta/no_deadtime.ld
esbmc benchmarks/motor_control/g_star_delta/no_deadtime.ld --ld-props benchmarks/motor_control/g_star_delta/deadtime_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.
1: IF !1 THEN GOTO 10
ASSIGN Call=NONDET(_Bool);
ASSIGN StarDone=NONDET(_Bool);
ASSIGN DeadDone=NONDET(_Bool);
IF !1 THEN GOTO 2
ASSIGN pf6=0;
2: IF !(1 && Call) THEN GOTO 3
ASSIGN pf6=1;
3: IF !1 THEN GOTO 4
ASSIGN pf7=0;
4: IF !(1 && pf6 && StarDone) THEN GOTO 5
ASSIGN pf7=1;
5: ASSIGN Delta=1 && pf7;
IF !1 THEN GOTO 6
ASSIGN pf3=0;
6: IF !(1 && Call) THEN GOTO 7
ASSIGN pf3=1;
7: IF !1 THEN GOTO 8
ASSIGN pf4=0;
8: IF !(1 && pf3 && !StarDone) THEN GOTO 9
ASSIGN pf4=1;
9: ASSIGN Star=1 && pf4;
GOTO 1
10:
The starter with a dead time refutes it. The one without proves it at k = 2, which is the formal way of saying the second contactor pulls in on the same scan the first drops.
The honest caveat¶
!(Star && Delta) is a statement about two program variables. A contactor is not one.
It carries a drop-out time of some tens of milliseconds, and the arc across its contacts
outlives the coil current by long enough that two commands which never overlap anywhere
in the model can still put two sets of contacts in circuit at the same instant on the
panel.
This is the part of the argument formal verification does not reach, and pretending otherwise is how a proof becomes a liability. What the run above establishes is that the program does not command the overlap. Whether the hardware permits it is a question for the contactor's data sheet and the mechanical interlock bolted between the two blocks.