Edges, and the order rungs run in¶

Every lesson so far has been combinational. Nothing carried a value from one scan into the next, so the order in which rungs ran could not matter. Edge detection breaks that, and the moment order matters this suite stops agreeing with the tool.

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_rtrig_edge: the released ESBMC 8.6.0 returns SAFE and passes the ingestion gate; 8.4.0 returns unknown.
g_ftrig_edge: the released ESBMC 8.6.0 returns SAFE and passes the ingestion gate; 8.4.0 returns unknown.
The expected verdict is unchanged in every case.

Detecting a rising edge¶

A PLC has no interrupt for "this input just went high". You compare the input against what it was last scan, and you keep last scan's value yourself:

Three rungs, and the order is the whole design:

Rise := Sig AND NOT Sig_prev compares now against last scan
OneShot := Rise publishes the pulse
Sig_prev := Sig records now, for the next scan to compare against

Rung 3 has to run last. If it runs before rung 1, then Sig_prev already equals Sig when rung 1 reads it, Rise is always false, and the edge detector detects nothing.

IEC 61131-3 makes that guarantee: rungs execute in order, and each one reads what the rungs above it wrote in this same scan. The order is not a hint from the drawing. It is the semantics.

file	what it is	size	sha256
`program.xml`	ladder program, PLCopen XML	2.7 KB	`1136bfe3dc28`
`props.yaml`	property file	0.2 KB	`ce9e226c5a26`

The property¶

benchmarks/traffic/g_rtrig_edge/props.yaml

format_version: "0.1"
properties:
  - id: P1
    kind: invariant
    expression: "!OneShot || Sig"
    justification: "The rising-edge one-shot fires only when the signal is (now) high."

!OneShot || Sig says the one-shot only fires while the signal is high. Trace the three rungs by hand under sequential evaluation and it holds: OneShot is raised in the same scan as the edge, and in that scan Sig is 1. The suite records the expected verdict as SAFE, and by the standard that is right.

The run¶

Recorded 2026-08-28T18:37:09Z. Every build ran the same command.

cp benchmarks/traffic/g_rtrig_edge/program.xml benchmarks/traffic/g_rtrig_edge/program.ld
esbmc benchmarks/traffic/g_rtrig_edge/program.ld --ld-props benchmarks/traffic/g_rtrig_edge/props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s

Recorded 2026-08-28T18:37:09Z.

master

cp benchmarks/traffic/g_rtrig_edge/program.xml benchmarks/traffic/g_rtrig_edge/program.ld
esbmc benchmarks/traffic/g_rtrig_edge/program.ld --ld-props benchmarks/traffic/g_rtrig_edge/props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s

build	ESBMC	verdict	expected	outcome	ingestion gate	cpu
master	8.4.0 `0064c4ac`	`VIOLATION`	`SAFE`	wrong	pass	0.012 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.

master

     1: IF !1 THEN GOTO 10
        ASSIGN Sig=NONDET(_Bool);
        ASSIGN Rise__prev=1 && Rise;
        ASSIGN Sig_prev__prev=1 && Sig_prev;
        IF !1 THEN GOTO 2
        ASSIGN pf8=0;
     2: IF !(1 && Sig) THEN GOTO 3
        ASSIGN pf8=1;
     3: ASSIGN Sig_prev=1 && pf8;
        IF !1 THEN GOTO 4
        ASSIGN pf6=0;
     4: IF !(1 && Rise__prev) THEN GOTO 5
        ASSIGN pf6=1;
     5: ASSIGN OneShot=1 && pf6;
        IF !1 THEN GOTO 6
        ASSIGN pf3=0;
     6: IF !(1 && Sig) THEN GOTO 7
        ASSIGN pf3=1;
     7: IF !1 THEN GOTO 8
        ASSIGN pf4=0;
     8: IF !(1 && pf3 && !Sig_prev__prev) THEN GOTO 9
        ASSIGN pf4=1;
     9: ASSIGN Rise=1 && pf4;
        GOTO 1
    10:

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.

master

State 1  thread 0
----------------------------------------------------
  Sig = 1

State 2  thread 0
----------------------------------------------------
  Rise = 1

State 3  thread 0
----------------------------------------------------
  Sig = 0

State 4  thread 0
----------------------------------------------------
  Rise__prev = 1

State 5  thread 0
----------------------------------------------------
  OneShot = 1

State 6 file benchmarks/traffic/g_rtrig_edge/program.ld thread 0
----------------------------------------------------
Violated property:
  file benchmarks/traffic/g_rtrig_edge/program.ld
  P1
  !OneShot || Sig


** Results:
  NOT CHECKED  [global.assertion.1]  line 0  unwinding assertion loop 1
benchmarks/traffic/g_rtrig_edge/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)

Neither build agrees.

What went wrong, in the encoding¶

The front end emits the three rungs in this order:

ASSIGN Sig_prev=1 && Sig;              rung 3
ASSIGN OneShot=1 && Rise;              rung 2
ASSIGN Rise=1 && Sig && !Sig_prev;     rung 1

Rung 3 first. By the time rung 1 asks whether Sig_prev differs from Sig, they are equal by construction, so Rise is permanently false. The edge detector is dead code. The property still holds, vacuously, and k-induction cannot close the proof from an arbitrary starting state, so the verdict is UNKNOWN rather than a false SUCCESSFUL.

master reorders too, and then adds a snapshot:

ASSIGN Rise__prev=1 && Rise;           snapshot at scan top
ASSIGN Sig_prev__prev=1 && Sig_prev;
ASSIGN Sig_prev=1 && pf8;              rung 3
ASSIGN OneShot=1 && pf6;               rung 2, from Rise__prev

Snapshotting at the top of the scan makes the result independent of rung order, which is coherent, and it is the semantics of a synchronous language such as Lustre or SMV. It is not the semantics of IEC 61131-3. Every rung now reads last scan's values, so OneShot lags the edge by one scan and fires when Sig has already gone low. That is a real violation of the property, in the program master built.

The counterexample above is worth reading slowly. Sig goes high, Rise goes high. Next scan Sig is back low, Rise__prev still carries the 1, and OneShot comes up against a low signal.

The cause¶

This is not a heuristic that guessed wrong. parser/plcopen_xml_parser.cpp decides scan order in what its comment calls step 7:

emit one sink per coil, in rightPowerRail order — the order the vendor tool draws the networks, hence the scan execution order.

Coils that the right power rail does not enumerate fall through to a second loop over the node table, and that table is a std::unordered_map<int, GNode>. Scan order then comes from hash iteration order.

In this repository, 35 of the 51 graphical programs leave the right rail's <connectionPointIn /> empty, so 35 of them take the fallback. The consequences are visible without reading any source:

program	coil localIds	order executed
`g_rtrig_edge`	5, 7, 9	9, 7, 5
`demo/interlock.ld`	12, 21	12, 21
`demo/interlock_bug.ld`	the same file, one contact fewer	the opposite order

Two files that differ by a single deleted contact run their rungs in opposite orders. Nothing in either file asked for that.

The falling-edge twin behaves the same way¶

file	what it is	size	sha256
`g_ftrig_edge_program.xml`	ladder program, PLCopen XML	2.7 KB	`38824ff959f4`
`g_ftrig_edge_props.yaml`	property file	0.2 KB	`028ffa662763`

Recorded 2026-08-28T18:37:08Z. Every build ran the same command.

cp benchmarks/packaging/g_ftrig_edge/program.xml benchmarks/packaging/g_ftrig_edge/program.ld
esbmc benchmarks/packaging/g_ftrig_edge/program.ld --ld-props benchmarks/packaging/g_ftrig_edge/props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s

Recorded 2026-08-28T18:37:08Z.

master

cp benchmarks/packaging/g_ftrig_edge/program.xml benchmarks/packaging/g_ftrig_edge/program.ld
esbmc benchmarks/packaging/g_ftrig_edge/program.ld --ld-props benchmarks/packaging/g_ftrig_edge/props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s

build	ESBMC	verdict	expected	outcome	ingestion gate	cpu
master	8.4.0 `0064c4ac`	`VIOLATION`	`SAFE`	wrong	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.

master

     1: IF !1 THEN GOTO 10
        ASSIGN Sig=NONDET(_Bool);
        ASSIGN Fall__prev=1 && Fall;
        ASSIGN Sig_prev__prev=1 && Sig_prev;
        IF !1 THEN GOTO 2
        ASSIGN pf8=0;
     2: IF !(1 && Sig) THEN GOTO 3
        ASSIGN pf8=1;
     3: ASSIGN Sig_prev=1 && pf8;
        IF !1 THEN GOTO 4
        ASSIGN pf6=0;
     4: IF !(1 && Fall__prev) THEN GOTO 5
        ASSIGN pf6=1;
     5: ASSIGN OneShot=1 && pf6;
        IF !1 THEN GOTO 6
        ASSIGN pf3=0;
     6: IF !(1 && !Sig) THEN GOTO 7
        ASSIGN pf3=1;
     7: IF !1 THEN GOTO 8
        ASSIGN pf4=0;
     8: IF !(1 && pf3 && Sig_prev__prev) THEN GOTO 9
        ASSIGN pf4=1;
     9: ASSIGN Fall=1 && pf4;
        GOTO 1
    10:

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.

master

State 1  thread 0
----------------------------------------------------
  Sig = 1

State 2  thread 0
----------------------------------------------------
  Sig_prev = 1

State 3  thread 0
----------------------------------------------------
  Sig = 0

State 4  thread 0
----------------------------------------------------
  Sig_prev__prev = 1

State 5  thread 0
----------------------------------------------------
  Fall = 1

State 6  thread 0
----------------------------------------------------
  Sig = 1

State 7  thread 0
----------------------------------------------------
  Fall__prev = 1

State 8  thread 0
----------------------------------------------------
  OneShot = 1

State 9 file benchmarks/packaging/g_ftrig_edge/program.ld thread 0
----------------------------------------------------
Violated property:
  file benchmarks/packaging/g_ftrig_edge/program.ld
  P1
  !OneShot || !Sig


** Results:
  NOT CHECKED  [global.assertion.1]  line 0  unwinding assertion loop 1
benchmarks/packaging/g_ftrig_edge/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)

What to take from this¶

Read the verdict column and you would conclude the benchmark is wrong. Read the encoding and you find the opposite: the program is right, the property is right, the expected verdict is right under the standard, and the tool ran the rungs in an order the file never specified.

This is what a benchmark suite is for. A task with a defensible expected verdict, established independently of any tool, is the only thing that can tell you a tool is wrong rather than merely different. Had the expected verdict been recorded as "whatever ESBMC says", this defect would have been invisible.

Two practical consequences if you are writing PLCopen XML by hand. Wire the right power rail: list every coil in <connectionPointIn> in the order you want the scan to run, and the well-defined path is taken. And when order matters to your program, write a property that is sensitive to it, the way lesson 1.2 used a discriminator, rather than trusting that the tool read your drawing the way you drew it.