Elevator door/motion dual interlock¶
| suite id | elevator_door_motion_interlock |
| domain | elevator |
| language | ST |
| difficulty | easy |
| validation status | candidate |
| origin | authored |
| license | CC-BY-4.0 |
Authored to close a specific SLM coverage gap: the entire 169-benchmark corpus (as of the prior round) had exactly one example pairing two independent invariants with a shared reachability witness (kiln_door_lockout), and the model failed to reproduce even that single training example, dropping one invariant. Authored with two genuinely independent hazards (door state, overload state) on the same actuator, not fan-out from one shared latch, to test whether the failure was structural (output shape) or content-specific (latch fan-out). See ml/README.md.
What is proved¶
From benchmarks/elevator/elevator_door_motion_interlock/props.yaml. What each kind claims, and what it becomes on either route, is on The properties we prove.
| id | kind | claim | requirement |
|---|---|---|---|
P1 |
invariant |
!(car_moving && door_open) |
The car must never move while a door is open. |
P2 |
invariant |
!(car_moving && overload_tripped) |
The car must never move while the overload sensor is tripped, independent of the door state. |
P3 |
reachability |
reachable: car_moving && overload_tripped |
Trigger synthesis: a witness recovers the bad state P2 forbids, so the counterexample search has a concrete target when the overload interlock is bypassed. |
Variants¶
| file | expected verdict | violates | method |
|---|---|---|---|
clean.st |
SAFE | none | expert |
bomb.st |
VIOLATION | P2 |
fault-injection |
Files¶
| file | what it is | size | sha256 |
|---|---|---|---|
benchmark.yml |
benchmark metadata | 1.5 KB | 864f215f0441 |
bomb.st |
structured text | 1.1 KB | b88fbd754879 |
clean.st |
structured text | 0.9 KB | 8bbefcd38281 |
props.yaml |
property file | 0.6 KB | b9aaf812c829 |
Recorded runs¶
A task can carry two routes. ld is ESBMC's ladder front end reading the program directly. via C is the same solver reached through Beremiz and MatIEC, which is the only route that reaches ST, IL, FBD and SFC; see How ESBMC-PLC works.
No ESBMC run is recorded against this task yet. The lessons carry the recorded runs; see Reproducing to make your own.