MIG welder shielding-gas interlock¶
| suite id | welder_gas_shield_interlock |
| domain | manufacturing |
| language | ST |
| difficulty | easy |
| validation status | candidate |
| origin | authored |
| license | CC-BY-4.0 |
Authored for the esbmc-plc-benchmark-suite to add a single-scan, single-output interlock example distinct from the corpus's dominant peer-actuator mutual_exclusion shape.
What is proved¶
From benchmarks/manufacturing/welder_gas_shield_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 |
!arc_on || (gas_flow_ok && trigger_pull) |
The arc must never strike unless both shielding-gas flow is confirmed and the torch trigger is pulled. |
P2 |
reachability |
reachable: arc_on && !gas_flow_ok |
Trigger synthesis: a witness recovers the case where the arc is live while the gas flow sensor reads a dropout, matching the seeded defect that removes the gas interlock from the trigger branch. |
Variants¶
| file | expected verdict | violates | method |
|---|---|---|---|
clean.st |
SAFE | none | expert |
bomb.st |
VIOLATION | P1 |
fault-injection |
Files¶
| file | what it is | size | sha256 |
|---|---|---|---|
benchmark.yml |
benchmark metadata | 1.1 KB | c760f29f523d |
bomb.st |
structured text | 1.1 KB | 48c625b976f8 |
clean.st |
structured text | 0.9 KB | c3156f53c923 |
props.yaml |
property file | 0.5 KB | 0d20a9e84195 |
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.