Timers, and the tick they count¶
A PLC has no clock in the sense a program on your laptop has one. It has scans, and a timer counts them. Everything awkward about verifying timers follows from that.
Update: released ESBMC 8.6.0
The runs on this page were recorded against the builds named beside them. For comparison, in the paper's evaluation (evidence/variants_302.csv in the release):
g_tof_hold: the released ESBMC 8.6.0 returns SAFE, which matches the expected verdict; 8.4.0 reports a false VIOLATION.g_ton_single: the released ESBMC 8.6.0 passes the ingestion gate and returns SAFE; 8.4.0 fails the gate.ld_tof_hold: the released ESBMC 8.6.0 returns SAFE, which matches the expected verdict; 8.4.0 reports a false VIOLATION.- The expected verdict is unchanged in every case.
Time is counted in scans¶
ESBMC models a timer on a fixed tick: one scan advances time by exactly one task
period. A preset of T#30ms on a task declared at T#10ms is three scans, and the
GOTO program says so in as many words:
The block's power flow is its Q pin, so the coil after it is driven by the timer
output rather than by the contact in front of it.
| file | what it is | size | sha256 |
|---|---|---|---|
program.xml |
ladder program, PLCopen XML | 2.8 KB | 50944a2342fa |
props.yaml |
property file | 0.2 KB | 11304a121ae8 |
Recorded 2026-08-28T18:37:10Z. Every build ran the same command.
cp benchmarks/hvac/g_ton_single/program.xml benchmarks/hvac/g_ton_single/program.ld
esbmc benchmarks/hvac/g_ton_single/program.ld --ld-props benchmarks/hvac/g_ton_single/props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s
Recorded 2026-08-28T18:37:10Z.
| build | ESBMC | verdict | expected | outcome | ingestion gate | cpu |
|---|---|---|---|---|---|---|
| master | 8.4.0 0064c4ac |
SAFE |
SAFE |
correct | pass | 0.016 s |
master found its solution by the inductive step (k = 2).
What the front end encoded. The scan body as the solver receives it, branch guards kept. An assignment-only view hides the guards and makes a guarded accumulator read as a constant.
1: IF !1 THEN GOTO 7
ASSIGN Btn=NONDET(_Bool);
IF !1 THEN GOTO 2
ASSIGN pf3=0;
2: IF !(1 && Btn) THEN GOTO 3
ASSIGN pf3=1;
3: ASSIGN TON0__IN=1 && pf3;
IF !TON0__IN THEN GOTO 5
IF !(TON0__ET < TON0__PT) THEN GOTO 4
ASSIGN TON0__ET=TON0__ET + 1;
4: GOTO 6
5: ASSIGN TON0__ET=0;
6: ASSIGN TON0__Q=TON0__IN && TON0__ET >= TON0__PT;
ASSIGN Light=1 && TON0__Q;
GOTO 1
7:
SUCCESSFUL, with the gate passing. Before believing it, look at what the front end built.
What a timer becomes¶
A TON is not a primitive to the solver. It has to be unrolled into state the scan loop
carries between iterations, and you can read the whole of it:
ASSIGN TOF0__IN=1 && pf3;
IF !TOF0__IN THEN GOTO ...
ASSIGN TOF0__ET=TOF0__ET + 1;
ASSIGN TOF0__Q=...
An elapsed-time counter, incremented on the scans where the input holds, and an output
raised when it passes the preset. That is the timer, and its presence in the scan body is
what makes any verdict about the lamp mean something. A front end that dropped the block
would leave Light as a plain copy of Button, and every property that happened to hold
of that reduced program would come back proved. The gate exists to catch exactly that,
mechanically, without anybody reading the encoding.
The property was wrong, and the tool was right to say so¶
The textual benchmark ld_tof_hold carries this requirement:
format_version: "0.1"
properties:
- id: P1
kind: invariant
expression: "!Light || Pir || Button"
justification: "The off-delay light is on only due to the PIR (held) or the manual button."
Read it against what an off-delay is for. The whole point of a TOF is to keep the lamp lit after the sensor clears. So the property claims the component does not do its job.
Recorded 2026-08-28T18:37:10Z. Every build ran the same command.
cp benchmarks/hvac/g_tof_hold/program.xml benchmarks/hvac/g_tof_hold/program.ld
esbmc benchmarks/hvac/g_tof_hold/program.ld --ld-props benchmarks/hvac/g_tof_hold/implies_input.props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s
Recorded 2026-08-28T18:37:10Z.
| build | ESBMC | verdict | expected | outcome | ingestion gate | cpu |
|---|---|---|---|---|---|---|
| master | 8.4.0 0064c4ac |
VIOLATION |
VIOLATION |
correct | pass | 0.015 s |
What the front end encoded. The scan body as the solver receives it, branch guards kept. An assignment-only view hides the guards and makes a guarded accumulator read as a constant.
1: IF !1 THEN GOTO 12
ASSIGN Pir=NONDET(_Bool);
ASSIGN Button=NONDET(_Bool);
IF !1 THEN GOTO 2
ASSIGN pf6=0;
2: IF !(1 && Button) THEN GOTO 3
ASSIGN pf6=1;
3: IF !1 THEN GOTO 4
ASSIGN pf3=0;
4: IF !(1 && Pir) THEN GOTO 5
ASSIGN pf3=1;
5: ASSIGN TOF0__IN=1 && pf3;
IF !TOF0__IN THEN GOTO 6
ASSIGN TOF0__ET=0;
ASSIGN TOF0__Q=1;
GOTO 8
6: IF !TOF0__Q THEN GOTO 8
IF !(TOF0__ET < TOF0__PT) THEN GOTO 7
ASSIGN TOF0__ET=TOF0__ET + 1;
7: ASSIGN TOF0__Q=TOF0__ET < TOF0__PT;
8: IF !1 THEN GOTO 9
ASSIGN Light__pf0=0;
9: IF !(1 && pf6) THEN GOTO 10
ASSIGN Light__pf0=1;
10: IF !(1 && TOF0__Q) THEN GOTO 11
ASSIGN Light__pf0=1;
11: ASSIGN Light=1 && Light__pf0;
GOTO 1
12:
Counterexample. ESBMC's own output. A trace long enough to need it is elided in the middle, and the omission is marked and counted where it happens.
State 1 thread 0
----------------------------------------------------
Pir = 1
State 2 thread 0
----------------------------------------------------
Button = 0
State 3 thread 0
----------------------------------------------------
TOF0__IN = 1
State 4 thread 0
----------------------------------------------------
Light = 1
State 6 thread 0
----------------------------------------------------
Pir = 0
State 7 thread 0
----------------------------------------------------
Button = 0
State 8 thread 0
----------------------------------------------------
TOF0__IN = 0
State 9 thread 0
----------------------------------------------------
Light = 1
State 10 file benchmarks/hvac/g_tof_hold/program.ld thread 0
----------------------------------------------------
Violated property:
file benchmarks/hvac/g_tof_hold/program.ld
P1
!Light || Pir || Button
** Results:
NOT CHECKED [global.assertion.1] line 0 unwinding assertion loop 1
benchmarks/hvac/g_tof_hold/program.ld
FAILED [global.assertion.2] line 0 P1
** 1 of 2 properties failed, 1 not checked
(this mode stops at the first violation; use --multi-property for a verdict on every property)
Refuted, and the counterexample is the off-delay working: Pir goes high and Light
comes on, then Pir drops to 0 with Button still 0, and Light stays on.
The tool is right and the requirement is wrong. That is a distinction worth keeping separate from a tool being wrong, because both arrive on the page as a red row.
A requirement that does hold¶
Ask for something an off-delay really guarantees: while the sensor sees motion, the lamp is lit. The delay only extends that, it never shortens it.
format_version: "0.1"
properties:
- id: P1
kind: invariant
expression: "!Pir || Light"
justification: "While the PIR sees motion the lamp must be lit; the off-delay only extends that, it never shortens it."
Recorded 2026-08-28T18:37:10Z. Every build ran the same command.
cp benchmarks/hvac/g_tof_hold/program.xml benchmarks/hvac/g_tof_hold/program.ld
esbmc benchmarks/hvac/g_tof_hold/program.ld --ld-props benchmarks/hvac/g_tof_hold/props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s
Recorded 2026-08-28T18:37:10Z.
| build | ESBMC | verdict | expected | outcome | ingestion gate | cpu |
|---|---|---|---|---|---|---|
| master | 8.4.0 0064c4ac |
SAFE |
SAFE |
correct | pass | 0.016 s |
master found its solution by the inductive step (k = 2).
What the front end encoded. The scan body as the solver receives it, branch guards kept. An assignment-only view hides the guards and makes a guarded accumulator read as a constant.
1: IF !1 THEN GOTO 12
ASSIGN Pir=NONDET(_Bool);
ASSIGN Button=NONDET(_Bool);
IF !1 THEN GOTO 2
ASSIGN pf6=0;
2: IF !(1 && Button) THEN GOTO 3
ASSIGN pf6=1;
3: IF !1 THEN GOTO 4
ASSIGN pf3=0;
4: IF !(1 && Pir) THEN GOTO 5
ASSIGN pf3=1;
5: ASSIGN TOF0__IN=1 && pf3;
IF !TOF0__IN THEN GOTO 6
ASSIGN TOF0__ET=0;
ASSIGN TOF0__Q=1;
GOTO 8
6: IF !TOF0__Q THEN GOTO 8
IF !(TOF0__ET < TOF0__PT) THEN GOTO 7
ASSIGN TOF0__ET=TOF0__ET + 1;
7: ASSIGN TOF0__Q=TOF0__ET < TOF0__PT;
8: IF !1 THEN GOTO 9
ASSIGN Light__pf0=0;
9: IF !(1 && pf6) THEN GOTO 10
ASSIGN Light__pf0=1;
10: IF !(1 && TOF0__Q) THEN GOTO 11
ASSIGN Light__pf0=1;
11: ASSIGN Light=1 && Light__pf0;
GOTO 1
12:
Proved. Between them the two properties pin the block down from both sides: the timer
extends the lamp past the sensor, and never cuts it short. A front end that had dropped the
TOF would answer the pair the other way round, refuting the requirement that holds and
proving the one that does not, which makes them a discriminator for the block in exactly
the sense lesson 1.2 used one for a dropped branch.
The trap that cost this suite a factor of ten¶
PLCopen types the task interval as a string and the TC6 schema annotates it: "Either a
constant duration as defined in the IEC or variable name", which reads as T#10ms.
Every program in this suite used to declare interval="PT0.01S", the ISO 8601 spelling,
which the front end does not parse. It then falls back to a one millisecond tick,
silently, and every preset in the suite was ten times longer than intended.
Calling that purely our mistake would be too generous to the tooling. The one file in
this catalog exported by a real engineering tool writes interval="PT0S", ISO 8601 as
well, so a genuine TwinCAT project hits this same silent fallback.
Lesson 4.1 has the comparison.
Nothing failed. No warning was printed. A T#30ms preset simply became 30 scans instead
of 3, and every timer benchmark still verified. It was fixed across all 43 programs on
2026-08-26, which is also why the Beremiz and MatIEC round trip in
docs/INTEROP.md
now runs without a hand patch.
If you write timer benchmarks, check the preset in the GOTO output. It is one grep, and it is the only place the mistake is visible.