Benchmarks
counter with reset-to-value (Sequential Function Chart)
|
|
| suite id |
sfc_counter_reset |
| domain |
manufacturing |
| language |
SFC |
| 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, CounterSFC 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/sfc_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 |
program.xml |
SAFE |
none |
expert |
Files
| file |
what it is |
size |
sha256 |
benchmark.yml |
benchmark metadata |
1.2 KB |
4475bcb61242 |
program.xml |
ladder program, PLCopen XML |
9.8 KB |
5ee236b77267 |
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.
sfc_counter_reset__program (props.yaml, expected SAFE): v8.4 error — ingestion gate failed on v8.4