Benchmarks
comb mixed (K-LD feature benchmark)
|
|
| suite id |
ld_comb_mixed |
| domain |
building_automation |
| language |
LD-textual |
| difficulty |
easy |
| validation status |
validated |
| origin |
authored |
| license |
CC-BY-4.0 |
K-LD executable-semantics feature suite (rung10_wp2/family)
What is proved
From benchmarks/building_automation/ld_comb_mixed/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 || C |
Output Y can be energised only through input A or C (series/parallel with a negated contact). |
Variants
| file |
expected verdict |
violates |
method |
comb_mixed.ld |
SAFE |
none |
expert |
Files
| file |
what it is |
size |
sha256 |
benchmark.yml |
benchmark metadata |
0.5 KB |
108a4c8f7333 |
comb_mixed.ld |
ladder program, textual DSL |
0.1 KB |
05bb3ec1fbdf |
props.yaml |
property file |
0.2 KB |
945cf173c7f5 |
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.
ld_comb_mixed__comb_mixed (props.yaml, expected SAFE): v8.4 SAFE