timer latch mix (K-LD feature benchmark)¶
| suite id | ld_timer_latch_mix |
| domain | elevator |
| language | LD-textual |
| difficulty | easy |
| validation status | candidate |
| origin | authored |
| license | CC-BY-4.0 |
K-LD executable-semantics feature suite (rung10_wp2/family)
What is proved¶
From benchmarks/elevator/ld_timer_latch_mix/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 |
!(Alarm && Ack) |
Acknowledge is dominant: the latched alarm and Ack never hold together. |
Variants¶
| file | expected verdict | violates | method |
|---|---|---|---|
timer_latch_mix.ld |
SAFE | none | expert |
Files¶
| file | what it is | size | sha256 |
|---|---|---|---|
benchmark.yml |
benchmark metadata | 0.5 KB | be27e2c79729 |
props.yaml |
property file | 0.2 KB | b0fb335ad3a5 |
timer_latch_mix.ld |
ladder program, textual DSL | 0.1 KB | 32ab8b73109a |
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.
No ESBMC run is recorded against this task yet. The lessons carry the recorded runs; see Reproducing to make your own.