Benchmarks
Batch fill and drain cycle (SFC)
|
|
| suite id |
sfc_batch_fill_drain |
| domain |
chemical_batch |
| language |
SFC |
| difficulty |
easy |
| validation status |
candidate |
| origin |
authored |
| license |
CC-BY-4.0 |
Four-step batch cycle, authored for SFC language coverage
What is proved
From benchmarks/chemical_batch/sfc_batch_fill_drain/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: fill_valve, drain_valve |
Fill and drain must never be open together: unreacted feed reaches the effluent line, which is a loss of containment rather than a lost batch. |
Variants
| file |
expected verdict |
violates |
method |
clean.xml |
SAFE |
none |
expert |
bomb.xml |
VIOLATION |
P1 |
fault-injection |
Files
| file |
what it is |
size |
sha256 |
benchmark.yml |
benchmark metadata |
1.1 KB |
eb44592ead8e |
bomb.xml |
ladder program, PLCopen XML |
6.0 KB |
2db8f1564a81 |
clean.xml |
ladder program, PLCopen XML |
5.8 KB |
8425f099016c |
props.yaml |
property file |
0.3 KB |
8d6f0531b82f |
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.
sfc_batch_fill_drain__bomb (props.yaml, expected VIOLATION): v8.4 unknown — ingestion gate failed on v8.4sfc_batch_fill_drain__bomb__viac via C (props.yaml, expected VIOLATION): master timeoutsfc_batch_fill_drain__clean (props.yaml, expected SAFE): v8.4 SAFE — ingestion gate failed on v8.4sfc_batch_fill_drain__clean__viac via C (props.yaml, expected SAFE): master timeout