Series, parallel, and the wired OR¶
Lesson 1.1 put three contacts in a row. Put two of them side by side instead and the rung gains something a series chain never has: a second way for power to arrive. That is the whole idea, and it is also where a verifier can quietly get your program wrong.
Two branches, one coil¶
Either contact conducting is enough, so the rung means Y := A OR B. In the file that
junction is not a symbol of its own. It is two <connection> elements sitting inside
the coil's single <connectionPointIn>:
<coil localId="5" negated="false" storage="none">
<connectionPointIn>
<connection refLocalId="3" />
<connection refLocalId="4" />
</connectionPointIn>
<variable>Y</variable>
</coil>
A wired OR is a fan-in, and a tool that reads such a list has to combine the incoming paths rather than take the last one it saw. Hold that thought.
| file | what it is | size | sha256 |
|---|---|---|---|
program.xml |
ladder program, PLCopen XML | 1.9 KB | 6f4c9406570c |
props.yaml |
property file | 0.2 KB | 1c69e0ba66fd |
branch_check.props.yaml |
property file | 0.4 KB | fc3a68ba4029 |
benchmarks/building_automation/g_comb_or/program.xml (ladder program, PLCopen XML, 1.9 KB)
<?xml version="1.0" encoding="utf-8"?>
<project xmlns="http://www.plcopen.org/xml/tc6_0200">
<fileHeader companyName="Anonymous" productName="Benchmark Suite" productVersion="1.0" creationDateTime="2026-08-26T00:00:00" />
<contentHeader name="g_comb_or"><coordinateInfo><fbd><scaling x="1" y="1" /></fbd><ld><scaling x="1" y="1" /></ld><sfc><scaling x="1" y="1" /></sfc></coordinateInfo></contentHeader>
<types><dataTypes /><pous><pou name="g_comb_or" pouType="program">
<interface><inputVars><variable name="A"><type><BOOL /></type></variable><variable name="B"><type><BOOL /></type></variable></inputVars><outputVars><variable name="Y"><type><BOOL /></type></variable></outputVars></interface>
<body><LD>
<leftPowerRail localId="0"><position x="0" y="0" /><connectionPointOut formalParameter="none" /></leftPowerRail>
<contact localId="3" negated="false" storage="none" edge="none"><position x="20" y="10" /><connectionPointIn><connection refLocalId="0" /></connectionPointIn><connectionPointOut /><variable>A</variable></contact><contact localId="4" negated="false" storage="none" edge="none"><position x="20" y="40" /><connectionPointIn><connection refLocalId="0" /></connectionPointIn><connectionPointOut /><variable>B</variable></contact><coil localId="5" negated="false" storage="none"><position x="80" y="10" /><connectionPointIn><connection refLocalId="3" /><connection refLocalId="4" /></connectionPointIn><connectionPointOut /><variable>Y</variable></coil>
<rightPowerRail localId="2147483646"><position x="400" y="0" /><connectionPointIn /></rightPowerRail>
</LD></body>
</pou></pous></types>
<instances><configurations><configuration name="Config0"><resource name="Res0"><task name="tcyclic" interval="T#10ms" priority="0"><pouInstance name="inst0" typeName="g_comb_or" /></task></resource></configuration></configurations></instances>
</project>
The property, and the run¶
format_version: "0.1"
properties:
- id: P1
kind: invariant
expression: "!Y || A || B"
justification: "Output Y is energised only when contact A or B is closed."
Recorded 2026-08-28T18:37:07Z. Every build ran the same command.
cp benchmarks/building_automation/g_comb_or/program.xml benchmarks/building_automation/g_comb_or/program.ld
esbmc benchmarks/building_automation/g_comb_or/program.ld --ld-props benchmarks/building_automation/g_comb_or/props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s
Recorded 2026-08-28T18:37:07Z.
| 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 9
ASSIGN A=NONDET(_Bool);
ASSIGN B=NONDET(_Bool);
IF !1 THEN GOTO 2
ASSIGN pf4=0;
2: IF !(1 && B) THEN GOTO 3
ASSIGN pf4=1;
3: IF !1 THEN GOTO 4
ASSIGN pf3=0;
4: IF !(1 && A) THEN GOTO 5
ASSIGN pf3=1;
5: IF !1 THEN GOTO 6
ASSIGN Y__pf0=0;
6: IF !(1 && pf4) THEN GOTO 7
ASSIGN Y__pf0=1;
7: IF !(1 && pf3) THEN GOTO 8
ASSIGN Y__pf0=1;
8: ASSIGN Y=1 && Y__pf0;
GOTO 1
9:
Proved at k = 2. Stop there and you would file this benchmark as done.
Read the encoding¶
A wired OR is the first place a ladder front end can quietly get a rung wrong, because there is an obvious and incorrect way to compile it: emit one assignment per branch and let the later one land on top of the earlier one.
After that pair of statements Y equals B, contact A has no effect on anything, and the
rung drawn above has been flattened into a rung with one branch. No diagnostic would be
printed, because nothing went wrong as far as the compiler is concerned.
What this build actually emits is a per-coil accumulator. pf3 and pf4 record whether
each branch conducted, then Y__pf0 starts at 0 and is raised by either one:
IF !(1 && B) THEN GOTO 3
ASSIGN pf4=1;
IF !(1 && A) THEN GOTO 5
ASSIGN pf3=1;
ASSIGN Y__pf0=0;
IF !(1 && pf4) THEN GOTO 7
ASSIGN Y__pf0=1;
IF !(1 && pf3) THEN GOTO 8
ASSIGN Y__pf0=1;
Two writes to Y__pf0 with the same value 1, guarded separately. That is a disjunction
written out longhand, and it is the rung you drew.
Why the property would not have noticed¶
!Y || A || B says that Y implies at least one of the two inputs. Under the accumulator
encoding Y is A OR B, so it holds. Under the flattened one Y is B, and B implies
A OR B, so it would hold there too. The property is true of the correct rung and of the
broken one alike, which makes it useless for telling them apart. A green row here would
have carried no information about whether the branch survived compilation.
So ask something that only a real OR refutes. If both branches are live, A can close
while B stays open, and Y still comes up:
format_version: "0.1"
# Discriminator, not a safety requirement. A rung whose two branches are a real OR
# lets B stay open while A closes, which VIOLATES this. A tool that proves it has
# encoded only one of the two branches.
properties:
- id: P1
kind: invariant
expression: "!Y || B"
justification: "Y implies B. A rung that ORs its branches must refute this."
Recorded 2026-08-28T18:37:07Z. Every build ran the same command.
cp benchmarks/building_automation/g_comb_or/program.xml benchmarks/building_automation/g_comb_or/program.ld
esbmc benchmarks/building_automation/g_comb_or/program.ld --ld-props benchmarks/building_automation/g_comb_or/branch_check.props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s
Recorded 2026-08-28T18:37:07Z.
cp benchmarks/building_automation/g_comb_or/program.xml benchmarks/building_automation/g_comb_or/program.ld
esbmc benchmarks/building_automation/g_comb_or/program.ld --ld-props benchmarks/building_automation/g_comb_or/branch_check.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 |
VIOLATION |
correct | 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.
1: IF !1 THEN GOTO 9
ASSIGN A=NONDET(_Bool);
ASSIGN B=NONDET(_Bool);
IF !1 THEN GOTO 2
ASSIGN pf4=0;
2: IF !(1 && B) THEN GOTO 3
ASSIGN pf4=1;
3: IF !1 THEN GOTO 4
ASSIGN pf3=0;
4: IF !(1 && A) THEN GOTO 5
ASSIGN pf3=1;
5: IF !1 THEN GOTO 6
ASSIGN Y__pf0=0;
6: IF !(1 && pf4) THEN GOTO 7
ASSIGN Y__pf0=1;
7: IF !(1 && pf3) THEN GOTO 8
ASSIGN Y__pf0=1;
8: ASSIGN Y=1 && Y__pf0;
GOTO 1
9:
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
----------------------------------------------------
A = 1
State 2 thread 0
----------------------------------------------------
B = 0
State 3 thread 0
----------------------------------------------------
Y = 1
State 4 file benchmarks/building_automation/g_comb_or/program.ld thread 0
----------------------------------------------------
Violated property:
file benchmarks/building_automation/g_comb_or/program.ld
P1
!Y || B
** Results:
benchmarks/building_automation/g_comb_or/program.ld
FAILED [global.assertion.1] line 0 P1
** 1 of 1 properties failed
Refuted, with the scan handed to you: A closed, B open, Y energized. That
counterexample is only constructible if the upper branch reached the solver, so the
refutation is the evidence that it did. Had the rung been flattened, this property would
have been proved instead, soundly, about a program with one branch in it.
Series inside a branch¶
The second twin adds a negated contact and puts a series pair on the upper branch:
Y := (A AND NOT B) OR C.
| file | what it is | size | sha256 |
|---|---|---|---|
g_comb_mixed_program.xml |
ladder program, PLCopen XML | 2.1 KB | 54de48eef918 |
g_comb_mixed_props.yaml |
property file | 0.2 KB | 945cf173c7f5 |
Recorded 2026-08-28T18:37:07Z. Every build ran the same command.
cp benchmarks/building_automation/g_comb_mixed/program.xml benchmarks/building_automation/g_comb_mixed/program.ld
esbmc benchmarks/building_automation/g_comb_mixed/program.ld --ld-props benchmarks/building_automation/g_comb_mixed/props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s
Recorded 2026-08-28T18:37:07Z.
cp benchmarks/building_automation/g_comb_mixed/program.xml benchmarks/building_automation/g_comb_mixed/program.ld
esbmc benchmarks/building_automation/g_comb_mixed/program.ld --ld-props benchmarks/building_automation/g_comb_mixed/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 |
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 11
ASSIGN A=NONDET(_Bool);
ASSIGN B=NONDET(_Bool);
ASSIGN C=NONDET(_Bool);
IF !1 THEN GOTO 2
ASSIGN pf3=0;
2: IF !(1 && A) THEN GOTO 3
ASSIGN pf3=1;
3: IF !1 THEN GOTO 4
ASSIGN pf4=0;
4: IF !(1 && pf3 && !B) THEN GOTO 5
ASSIGN pf4=1;
5: IF !1 THEN GOTO 6
ASSIGN pf5=0;
6: IF !(1 && C) THEN GOTO 7
ASSIGN pf5=1;
7: IF !1 THEN GOTO 8
ASSIGN Y__pf0=0;
8: IF !(1 && pf4) THEN GOTO 9
ASSIGN Y__pf0=1;
9: IF !(1 && pf5) THEN GOTO 10
ASSIGN Y__pf0=1;
10: ASSIGN Y=1 && Y__pf0;
GOTO 1
11:
Same story, one level deeper. Flattening would give ASSIGN Y=1 && A && !B; followed by
ASSIGN Y=1 && C;, leaving Y as just C. What is built instead threads pf3 for A,
pf4 for the series pair, pf5 for C, and merges the two branches into the coil
accumulator. The shipped property reports SUCCESSFUL either way, for the same reason as
before.
What to take from this¶
A parallel branch is not another contact. It is a fan-in, and a front end has to decide what to do when two paths arrive at one input. Getting that wrong does not crash anything and does not produce a warning. It produces a smaller program that still verifies.
That is why every lesson here shows the scan body next to the verdict. A verdict tells you what the solver concluded about the program it was given. Only the encoding tells you whether that was your program.
Lesson 1.4 is the same defect with memory attached, where the branch feeding back into the coil is what makes a latch a latch.