Four-way header selector valve lockout¶
| suite id | st_quad_valve_lockout |
| domain | water_treatment |
| language | ST |
| difficulty | medium |
| validation status | candidate |
| origin | authored |
| license | CC-BY-4.0 |
Authored for the ESBMC-PLC benchmark suite to cover N-ary (N>2) mutual_exclusion at N=4, alongside st_three_pump_lockout (N=3), previously unrepresented in the corpus.
What is proved¶
From benchmarks/water_treatment/st_quad_valve_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 |
mutual_exclusion |
never true together: valve_1, valve_2, valve_3, valve_4 |
Exactly one (or none) of the four header outlet valves may be open at a time; the shared header would cross-contaminate batches if two lines were supplied together. |
P2 |
reachability |
reachable: valve_1 && valve_3 |
Trigger synthesis: a witness recovers the fast-flush input combination that violates pairwise exclusion between valve_1 and valve_3. |
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.2 KB | 6f5f389e56fc |
bomb.st |
structured text | 1.2 KB | b5c3b5417cb8 |
clean.st |
structured text | 1.1 KB | 84e9c7cd6987 |
props.yaml |
property file | 0.6 KB | 1dd12a6fd456 |
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.