Benchmarks
Two-out-of-three overpressure trip (FBD)
|
|
| suite id |
fbd_reactor_2oo3 |
| domain |
chemical_batch |
| language |
FBD |
| difficulty |
medium |
| validation status |
candidate |
| origin |
authored |
| license |
CC-BY-4.0 |
Voted trip logic, authored for FBD language coverage
What is proved
From benchmarks/chemical_batch/fbd_reactor_2oo3/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 |
!((ps1 && ps2) || (ps2 && ps3) || (ps1 && ps3)) || trip |
Any two pressure switches agreeing high must trip the reactor, or the vessel stays pressurised behind a closed relief path. |
P2 |
invariant |
!trip || ((ps1 && ps2) || (ps2 && ps3) || (ps1 && ps3)) |
A single stuck-high switch must not trip: spurious trips on a batch plant cost a charge and train operators to bypass the vote. |
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.0 KB |
08dd40c4876d |
bomb.xml |
ladder program, PLCopen XML |
5.6 KB |
bf03536740e2 |
clean.xml |
ladder program, PLCopen XML |
6.8 KB |
72a1205e72e1 |
props.yaml |
property file |
0.5 KB |
de519b56ea30 |
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.
fbd_reactor_2oo3__bomb (props.yaml, expected VIOLATION): v8.4 VIOLATION — ingestion gate failed on v8.4fbd_reactor_2oo3__bomb__viac via C (props.yaml, expected VIOLATION): master VIOLATIONfbd_reactor_2oo3__clean (props.yaml, expected SAFE): v8.4 VIOLATION — ingestion gate failed on v8.4fbd_reactor_2oo3__clean__viac via C (props.yaml, expected SAFE): master SAFE