Benchmarks
seal in (Instruction List rendering)
|
|
| suite id |
il_seal_in |
| domain |
motor_control |
| language |
IL |
| difficulty |
easy |
| validation status |
candidate |
| origin |
authored |
| license |
CC-BY-4.0 |
| syntax pair of |
ld_seal_in |
One of five renderings of the same seal-in latch. IL was deprecated in edition 3.0 and removed in edition 4.0; kept for tools that still parse it
What is proved
From benchmarks/motor_control/il_seal_in/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 |
!Run || !Stop |
Stop always drops the seal-in coil: Run and Stop never hold together. |
Variants
| file |
expected verdict |
violates |
method |
seal_in.il |
SAFE |
none |
expert |
Files
| file |
what it is |
size |
sha256 |
benchmark.yml |
benchmark metadata |
0.6 KB |
438f4244893b |
props.yaml |
property file |
0.2 KB |
ebfe6cdbb2fc |
seal_in.il |
instruction list |
0.5 KB |
2d1ddbb717ae |
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.
il_seal_in__seal_in__viac via C (props.yaml, expected SAFE): master SAFE