Benchmarks
comb and (Function Block Diagram rendering)
|
|
| suite id |
fbd_comb_and |
| domain |
manufacturing |
| language |
FBD |
| difficulty |
easy |
| validation status |
candidate |
| origin |
authored |
| license |
CC-BY-4.0 |
| syntax pair of |
ld_comb_and |
Function Block Diagram rendering of the three-contact series rung, for cross-language comparison in lesson 1.1
What is proved
From benchmarks/manufacturing/fbd_comb_and/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 |
!Y || (A && B && C) |
Output Y is energised only when all series contacts A, B and C are closed. |
Variants
| file |
expected verdict |
violates |
method |
program.xml |
SAFE |
none |
expert |
Files
| file |
what it is |
size |
sha256 |
benchmark.yml |
benchmark metadata |
0.7 KB |
26bc56ce9556 |
program.xml |
ladder program, PLCopen XML |
3.0 KB |
0323eb4dad89 |
props.yaml |
property file |
0.2 KB |
7f98094eb39c |
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.
comb_and_fbd_viac via C (props.yaml, expected SAFE): master SAFEfbd_comb_and__program (props.yaml, expected SAFE): v8.4 SAFE — ingestion gate failed on v8.4