counter with reset-to-value (Instruction List)¶
| suite id | il_counter_reset |
| domain | manufacturing |
| language | IL |
| difficulty | easy |
| validation status | candidate |
| origin | beremiz |
| license | GPL-2.0-or-later |
| syntax pair of | st_counter_reset |
Imported from the Beremiz IEC 61131-3 language test (tests/projects/iec61131_lang_test, CounterIL function block, checked at aeb89e8 on 2026-08-29). The body is carried over unchanged; only the enclosing POU differs, since upstream declares a function block reading a global ResetCounterValue and this file declares an equivalent PROGRAM taking it as an input, so the task stands alone. Beremiz ships its IDE tree under GPLv2-or-later with no per-file header, which is the license recorded here.
What is proved¶
From benchmarks/manufacturing/il_counter_reset/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 |
!Reset || (OUT == ResetCounterValue) |
Reset is a load, not a clear: on a scan where Reset holds, the counter output equals the supplied reset value rather than the incremented count. |
Variants¶
| file | expected verdict | violates | method |
|---|---|---|---|
counter_reset.il |
SAFE | none | expert |
Files¶
| file | what it is | size | sha256 |
|---|---|---|---|
benchmark.yml |
benchmark metadata | 1.0 KB | dbe3f8f9645d |
counter_reset.il |
instruction list | 0.6 KB | ef82e1fc06fc |
props.yaml |
property file | 0.3 KB | 81e77ecfe357 |
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.