The reset nobody has to press¶
Twist the mushroom button back out. Does the conveyor start moving?
On a machine built to ISO 13850 it must not. Releasing the actuator clears the stop command, and nothing more; the safety function comes back only when somebody presses a separate reset button, sited where they can see the whole hazard zone. ISO 13849-1 calls this a manual reset. The clause exists because the person who pressed the button is often not the person standing in the machine.
The rungs¶
ResetEdge := Reset_prev AND NOT Reset, Safe := (Safe OR ResetEdge) AND NOT EStop,
Run := Safe AND Start AND NOT EStop, Reset_prev := Reset. The reset is taken on the falling edge, when the button comes back up. A reset that has
been bridged with a jumper, or taped down by an operator who got tired of walking to it,
then restores nothing at all. That is the whole point of the word "monitored".
EStop also breaks the drive rung directly, not only through Safe. Real stop circuits
are wired that way, and it happens to make the property below independent of the order
the rungs run in, which lesson 1.5 shows is not the order the file specifies.
| file | what it is | size | sha256 |
|---|---|---|---|
program.xml |
ladder program, PLCopen XML | 4.2 KB | f5c1c2055de6 |
auto_reset.xml |
ladder program, PLCopen XML | 2.6 KB | b8ca85ab016f |
props.yaml |
property file | 0.2 KB | 1ce16a3f5a05 |
restart_check.props.yaml |
property file | 0.5 KB | c0b53659bed5 |
The property everyone writes¶
format_version: "0.1"
properties:
- id: P1
kind: invariant
expression: "!(Run && EStop)"
justification: "ISO 13850 stop function: the drive is never energised while the emergency stop is actuated."
The drive is never energized while the button is in. It is the requirement a reviewer asks for, it is true, and the checker discharges it at k = 2.
Recorded 2026-09-04T23:40:49Z. Every build ran the same command.
cp benchmarks/motor_control/g_estop_reset/program.xml benchmarks/motor_control/g_estop_reset/program.ld
esbmc benchmarks/motor_control/g_estop_reset/program.ld --ld-props benchmarks/motor_control/g_estop_reset/props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 20s
Recorded 2026-09-04T23:40:49Z.
| build | ESBMC | verdict | expected | outcome | ingestion gate | cpu |
|---|---|---|---|---|---|---|
| v8.4 | 8.4.0 | SAFE |
SAFE |
correct | pass | 0.016 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 EStop=NONDET(_Bool);
ASSIGN Reset=NONDET(_Bool);
ASSIGN Start=NONDET(_Bool);
ASSIGN Reset_prev=1 && Reset;
ASSIGN Run=1 && Safe && Start && !EStop;
ASSIGN Safe=1 && Safe && !EStop;
ASSIGN Safe=1 && ResetEdge && !EStop;
ASSIGN ResetEdge=1 && Reset_prev && !Reset;
GOTO 1
2:
Now the same property against a program with no reset in it at all, where Safe follows
the emergency stop contact directly.
Predict the verdict
The reset latch has been deleted, so the drive is available again the moment the button is twisted out. Does !(Run && EStop) still hold?
Answer
| build | verdict | expected | ingestion gate |
|---|---|---|---|
| v8.4 | SAFE |
SAFE |
pass |
It holds. Nothing in that property mentions how the machine comes back, so it cannot distinguish a monitored reset from a machine that restarts under your hands. Both programs pass, and one of them is the hazard the clause was written to prevent.
The discriminator¶
Ask instead whether the machine is allowed to sit still with the button already out.
# Discriminator, not a safety requirement. ISO 13849-1 requires the safety function to be
# restored by a separate manual action, so a monitored reset must be able to hold the drive
# down after the emergency stop is released. A program that PROVES this has an automatic
# restart in it.
format_version: "0.1"
properties:
- id: P1
kind: invariant
expression: "Safe || EStop"
justification: "The safety function is available whenever the emergency stop is clear. A monitored reset must refute this."
Recorded 2026-08-28T18:37:08Z. Every build ran the same command.
cp benchmarks/motor_control/g_estop_reset/program.xml benchmarks/motor_control/g_estop_reset/program.ld
esbmc benchmarks/motor_control/g_estop_reset/program.ld --ld-props benchmarks/motor_control/g_estop_reset/restart_check.props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s
Recorded 2026-08-28T18:37:08Z.
cp benchmarks/motor_control/g_estop_reset/program.xml benchmarks/motor_control/g_estop_reset/program.ld
esbmc benchmarks/motor_control/g_estop_reset/program.ld --ld-props benchmarks/motor_control/g_estop_reset/restart_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.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 21
ASSIGN EStop=NONDET(_Bool);
ASSIGN Reset=NONDET(_Bool);
ASSIGN Start=NONDET(_Bool);
ASSIGN ResetEdge__prev=1 && ResetEdge;
ASSIGN Reset_prev__prev=1 && Reset_prev;
ASSIGN Safe__prev=1 && Safe;
IF !1 THEN GOTO 2
ASSIGN pf13=0;
2: IF !(1 && Reset) THEN GOTO 3
ASSIGN pf13=1;
3: ASSIGN Reset_prev=1 && pf13;
IF !1 THEN GOTO 4
ASSIGN pf10=0;
4: IF !(1 && Safe__prev) THEN GOTO 5
ASSIGN pf10=1;
5: IF !1 THEN GOTO 6
ASSIGN pf11=0;
6: IF !(1 && pf10 && Start) THEN GOTO 7
ASSIGN pf11=1;
7: IF !1 THEN GOTO 8
ASSIGN pf15=0;
8: IF !(1 && pf11 && !EStop) THEN GOTO 9
ASSIGN pf15=1;
9: ASSIGN Run=1 && pf15;
IF !1 THEN GOTO 10
ASSIGN pf7=0;
10: IF !(1 && ResetEdge__prev) THEN GOTO 11
ASSIGN pf7=1;
11: IF !1 THEN GOTO 12
ASSIGN pf6=0;
12: IF !(1 && Safe__prev) THEN GOTO 13
ASSIGN pf6=1;
13: IF !1 THEN GOTO 14
ASSIGN pf8=0;
14: IF !(1 && pf7 && !EStop) THEN GOTO 15
ASSIGN pf8=1;
15: IF !(1 && pf6 && !EStop) THEN GOTO 16
ASSIGN pf8=1;
16: ASSIGN Safe=1 && pf8;
IF !1 THEN GOTO 17
ASSIGN pf3=0;
17: IF !(1 && Reset_prev__prev) THEN GOTO 18
ASSIGN pf3=1;
18: IF !1 THEN GOTO 19
ASSIGN pf4=0;
19: IF !(1 && pf3 && !Reset) THEN GOTO 20
ASSIGN pf4=1;
20: ASSIGN ResetEdge=1 && pf4;
GOTO 1
21:
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
----------------------------------------------------
EStop = 0
State 2 file benchmarks/motor_control/g_estop_reset/program.ld thread 0
----------------------------------------------------
Violated property:
file benchmarks/motor_control/g_estop_reset/program.ld
P1
Safe || EStop
** Results:
benchmarks/motor_control/g_estop_reset/program.ld
FAILED [global.assertion.1] line 0 P1
** 1 of 1 properties failed
Read the counterexample. It is one state long: EStop = 0, and Safe is still down. A
trace that short is not a weakness of the property. It is the requirement, arriving in
the first scan, because "stopped with the button released" is precisely the state a
manual reset has to be able to hold.
Against the automatic restart, the same property is provable.
Recorded 2026-08-28T18:37:08Z. Every build ran the same command.
cp benchmarks/motor_control/g_estop_reset/auto_reset.xml benchmarks/motor_control/g_estop_reset/auto_reset.ld
esbmc benchmarks/motor_control/g_estop_reset/auto_reset.ld --ld-props benchmarks/motor_control/g_estop_reset/restart_check.props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s
Recorded 2026-08-28T18:37:08Z.
cp benchmarks/motor_control/g_estop_reset/auto_reset.xml benchmarks/motor_control/g_estop_reset/auto_reset.ld
esbmc benchmarks/motor_control/g_estop_reset/auto_reset.ld --ld-props benchmarks/motor_control/g_estop_reset/restart_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.017 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 EStop=NONDET(_Bool);
ASSIGN Reset=NONDET(_Bool);
ASSIGN Start=NONDET(_Bool);
ASSIGN Safe__prev=1 && Safe;
IF !1 THEN GOTO 2
ASSIGN pf5=0;
2: IF !(1 && Safe__prev) THEN GOTO 3
ASSIGN pf5=1;
3: IF !1 THEN GOTO 4
ASSIGN pf6=0;
4: IF !(1 && pf5 && Start) THEN GOTO 5
ASSIGN pf6=1;
5: IF !1 THEN GOTO 6
ASSIGN pf8=0;
6: IF !(1 && pf6 && !EStop) THEN GOTO 7
ASSIGN pf8=1;
7: ASSIGN Run=1 && pf8;
IF !1 THEN GOTO 8
ASSIGN pf3=0;
8: IF !(1 && !EStop) THEN GOTO 9
ASSIGN pf3=1;
9: ASSIGN Safe=1 && pf3;
GOTO 1
10:
Both builds discharge it at k = 2. The program can never be in the state the standard requires it to reach, and the proof says so.
What to take from it¶
Two programs, one property, one verdict each way. The safety property is true of the dangerous program; the discriminator is false of the safe one. Neither result is a tool error, and no amount of running the first property harder would have found the defect.
The general shape recurs through this part. A requirement written as "the machine never does X" is usually cheap to satisfy by doing nothing, and a program that does nothing satisfies every property of that form. The requirement worth checking is the one that says the machine can still be brought to a state you need, and that one has to be refuted, not proved.
| file | what it is | size | sha256 |
|---|---|---|---|
estop_reset.st |
structured text | 0.8 KB | 234d460f66dd |
The Structured Text twin carries the same four assignments and reaches the solver through Beremiz and MatIEC rather than the ladder front end.
Recorded 2026-08-28T18:38:49Z. Every build ran the same command.
runner/record_via_c.py benchmarks/motor_control/st_estop_reset/estop_reset.st benchmarks/motor_control/st_estop_reset/props.yaml true --tool master=<path-to-esbmc>
which generates the C below and hands it to ESBMC as:
Translated by Beremiz df4370c and MatIEC 7949c0b.
| build | ESBMC | verdict | expected | outcome | cpu |
|---|---|---|---|---|---|
| master | 8.4.0 0064c4ac |
SAFE |
SAFE |
correct | 2.144 s |
master found its solution by the forward condition; all states are reachable (k = 9).
What ESBMC was given. The harness the adapter generated, with the property written over the variables MatIEC emitted.
#include "iec_std_lib.h"
#include "POUS.h"
#include "POUS.c"
int main(void) {
DRIVE_data__ d = {0};
DRIVE_init__(&d, 0);
for (int scan = 0; scan < 8; scan++) {
__SET_VAR(d., ESTOP, , nondet_bool());
__SET_VAR(d., RESET, , nondet_bool());
__SET_VAR(d., START, , nondet_bool());
DRIVE_body__(&d);
__ESBMC_assert(!(__GET_VAR(d.RUN,) && __GET_VAR(d.ESTOP,)), "P1");
}
return 0;
}