Benchmarks
Burner pre-ignition purge fault lockout
|
|
| suite id |
purge_fault_lockout |
| domain |
hvac |
| language |
LD-textual |
| difficulty |
easy |
| validation status |
validated |
| origin |
authored |
| license |
CC-BY-4.0 |
Authored for the esbmc-plc-benchmark-suite to close a training gap found by ml/scripts/build_task_slice.py: a latch that fans out to two independent readouts, where the safety property is about the trigger, not the readouts' mutual relationship.
What is proved
From benchmarks/hvac/purge_fault_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 |
purge_fail -> !burner_enable |
A failed pre-ignition purge must lock out the burner; this must hold on the trigger condition itself, not merely on the internal fault_latch/fault_indicator wiring the trigger happens to drive. |
P2 |
reachability |
reachable: purge_fail && burner_enable |
Witness: purge_fail=1, burner_req=1 reaches burner_enable=1 in bomb, because the latch mechanism was removed rather than merely reworded. |
Variants
| file |
expected verdict |
violates |
method |
clean.ld |
SAFE |
none |
expert |
bomb.ld |
VIOLATION |
P1 |
fault-injection |
Files
| file |
what it is |
size |
sha256 |
benchmark.yml |
benchmark metadata |
1.1 KB |
671c06435a02 |
bomb.ld |
ladder program, textual DSL |
0.3 KB |
f91c6be39a03 |
clean.ld |
ladder program, textual DSL |
0.2 KB |
fa4f4f0e850a |
props.yaml |
property file |
0.6 KB |
b6165d6456b8 |
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.
purge_fault_lockout__bomb (props.yaml, expected VIOLATION): v8.4 error — ingestion gate failed on v8.4purge_fault_lockout__clean (props.yaml, expected SAFE): v8.4 VIOLATION