Packaging conveyor jam lockout¶
| suite id | conveyor_jam_lockout |
| domain | packaging |
| language | ST |
| difficulty | medium |
| validation status | candidate |
| origin | authored |
| license | CC-BY-4.0 |
Authored to target the temporal/procedural-phrasing translation gap identified in the kiln_door_lockout diagnosis, this time phrasing the second requirement as a sequencing/timing constraint ('stays off for the remainder of that run') tied to a run/cycle boundary rather than a simple set/reset latch. See ml/README.md.
What is proved¶
From benchmarks/packaging/conveyor_jam_lockout/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 |
!(belt_drive && jam_detected) |
The belt drive must never run while the jam sensor is tripped. |
P2 |
invariant |
!(belt_drive && jam_this_run) |
Once a jam has been detected during a production run, the belt drive must stay off for the remainder of that run, even after the jam clears on its own, so an operator can inspect the line before the next run. |
P3 |
reachability |
reachable: belt_drive && jam_this_run |
Trigger synthesis: a witness recovers the bad state P2 forbids, so the counterexample search has a concrete target when the run-lockout 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.3 KB | b56113dbbfd2 |
bomb.st |
structured text | 1.3 KB | acb417166f34 |
clean.st |
structured text | 1.2 KB | 9941e319813a |
props.yaml |
property file | 0.7 KB | cb28762ee50a |
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.