One rung: contacts and a coil¶

Everything in this suite is built out of the two elements below. A contact asks a question of a Boolean variable, and a coil writes the answer. Three contacts in a row and one coil is enough of a program to state a property about, prove it, and read what the verifier did with it.

The rung¶

Contacts in series conduct only when every one of them is closed, so the rung means Y := A AND B AND C. Nothing is remembered between scans. Whatever the inputs are when the scan starts, Y is decided before it ends.

file	what it is	size	sha256
`program.xml`	ladder program, PLCopen XML	2.1 KB	`a62808ceb550`
`props.yaml`	property file	0.2 KB	`7f98094eb39c`

benchmarks/manufacturing/g_comb_and/program.xml (ladder program, PLCopen XML, 2.1 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-07-09T00:00:00" />
  <contentHeader name="g_comb_and"><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_and" pouType="program">
    <interface><inputVars><variable name="A"><type><BOOL /></type></variable><variable name="B"><type><BOOL /></type></variable><variable name="C"><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="40" y="10" /><connectionPointIn><connection refLocalId="3" /></connectionPointIn><connectionPointOut /><variable>B</variable></contact><contact localId="5" negated="false" storage="none" edge="none"><position x="60" y="10" /><connectionPointIn><connection refLocalId="4" /></connectionPointIn><connectionPointOut /><variable>C</variable></contact><coil localId="6" negated="false" storage="none"><position x="80" y="10" /><connectionPointIn><connection refLocalId="5" /></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_and" /></task></resource></configuration></configurations></instances>
</project>

Four elements and a rail on each side. Notice that each contact names the element it receives power from, in <connectionPointIn>, rather than sitting at a position on a line. The drawing above is a rendering of that graph, not the program itself.

The property¶

benchmarks/manufacturing/g_comb_and/props.yaml

format_version: "0.1"
properties:
  - id: P1
    kind: invariant
    expression: "!Y || (A && B && C)"
    justification: "Output Y is energised only when all series contacts A, B and C are closed."

Read !Y || (A && B && C) as an implication: if Y is energized then all three contacts were closed. It says nothing about the reverse, which is deliberate. A property is a claim you are prepared to defend, not a restatement of the code, and restating the code proves nothing except that the tool can read it.

The extension decides the front end

ESBMC picks its LD front end from the file name, and the benchmark ships as program.xml. Copy it before you run:

cp program.xml program.ld

The run¶

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

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

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

master

cp benchmarks/manufacturing/g_comb_and/program.xml benchmarks/manufacturing/g_comb_and/program.ld
esbmc benchmarks/manufacturing/g_comb_and/program.ld --ld-props benchmarks/manufacturing/g_comb_and/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.

master

     1: IF !1 THEN GOTO 8
        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 && pf4 && C) THEN GOTO 7
        ASSIGN pf5=1;
     7: ASSIGN Y=1 && pf5;
        GOTO 1
     8:

Both builds prove it, and both name the inductive step at k = 2. For a rung with no memory that is what you expect: the base case covers the first scan, one inductive step covers every scan after it, and there is nothing else for the proof to chase.

Read the encoding¶

This is the first place worth slowing down, because the two tabs above disagree about how to write the same rung.

One reasonable compilation is the assignment you would have written yourself:

ASSIGN Y=1 && A && B && C;

master threads power through the rung one contact at a time. pf3 records whether the rail reached the far side of contact A, pf4 whether it got past B, pf5 whether it got past C, and only then is Y assigned:

IF !(1 && A)          THEN GOTO 3
ASSIGN pf3=1;
IF !(1 && pf3 && B)   THEN GOTO 5
ASSIGN pf4=1;
...
ASSIGN Y=1 && pf5;

On this rung the two are the same function. The accumulators exist because a real ladder has branches, and a branch needs somewhere to put a partial result. Lesson 1.4 is where that difference stops being cosmetic and starts changing the verdict.

The same rung in the other languages¶

The rung above is ladder, and ladder is one of five notations the standard defines. The same three-input conjunction can be written in any of them, and the suite ships all four spellings of this one program so a tool's coverage can be measured rather than assumed.

Structured textInstruction listFunction block diagram

Y := A AND B AND C;

      LD    A
      AND   B
      AND   C
      ST    Y

Three inVariables into one variadic AND block, its output wired to an outVariable. Beremiz renders that graph back to text as _TMP_AND4_OUT := AND(A, B, C);.

file	what it is	size	sha256
`comb_and.st`	structured text	0.3 KB	`2ff49cd53fb1`
`comb_and.il`	instruction list	0.3 KB	`3272ea4b7dfa`
`fbd_comb_and_program.xml`	ladder program, PLCopen XML	3.0 KB	`0323eb4dad89`
`comb_and.ld`	ladder program, textual DSL	0.1 KB	`00a3e169a63c`

ESBMC's LD front end reads none of them. It registers one extension, ld, and one body type, so a structured text file is failed to figure out type of file and an FBD body inside a .ld file is discarded without a diagnostic. That is not a gap you can close by writing the property differently.

Real verdicts for all four, through C¶

There is a second route to the same solver, described in full on How ESBMC-PLC works. Beremiz renders any PLCopen body as structured text, MatIEC compiles structured text or instruction list to C, and ESBMC has read C for years. Every rendering below was verified that way, on this machine, against the property this lesson already uses.

Structured text¶

Recorded 2026-08-27T19:24:12Z. Every build ran the same command.

runner/record_via_c.py benchmarks/manufacturing/st_comb_and/comb_and.st benchmarks/manufacturing/st_comb_and/props.yaml true --tool master=<path-to-esbmc>

which generates the C below and hands it to ESBMC as:

esbmc <generated>/harness.c -I $PLC_TOOLS/matiec/lib/C -I <generated> --k-induction --timeout 120s

Translated by Beremiz df4370c and MatIEC 7949c0b.

build	ESBMC	verdict	expected	outcome	cpu
master	8.4.0 `d88a9fa4`	`SAFE`	`SAFE`	correct	0.963 s

master found its solution by the forward condition; all states are reachable (k = 4).

What ESBMC was given. The harness the adapter generated, with the property written over the variables MatIEC emitted.

#include "iec_std_lib.h"
#include "POUS.h"
#include "POUS.c"

int main(void) {
  DRIVE_data__ d = {0};
  DRIVE_init__(&d, 0);
  for (int scan = 0; scan < 3; scan++) {
    __SET_VAR(d., A, , nondet_bool());
    __SET_VAR(d., B, , nondet_bool());
    __SET_VAR(d., C, , nondet_bool());
    DRIVE_body__(&d);
    __ESBMC_assert(!__GET_VAR(d.Y,) || (__GET_VAR(d.A,) && __GET_VAR(d.B,) && __GET_VAR(d.C,)), "P1");
  }
  return 0;
}

Instruction list¶

Recorded 2026-08-27T19:24:13Z. Every build ran the same command.

runner/record_via_c.py benchmarks/manufacturing/il_comb_and/comb_and.il benchmarks/manufacturing/il_comb_and/props.yaml true --tool master=<path-to-esbmc>

which generates the C below and hands it to ESBMC as:

esbmc <generated>/harness.c -I $PLC_TOOLS/matiec/lib/C -I <generated> --k-induction --timeout 120s

Translated by Beremiz df4370c and MatIEC 7949c0b.

build	ESBMC	verdict	expected	outcome	cpu
master	8.4.0 `d88a9fa4`	`SAFE`	`SAFE`	correct	0.840 s

master found its solution by the forward condition; all states are reachable (k = 4).

What ESBMC was given. The harness the adapter generated, with the property written over the variables MatIEC emitted.

#include "iec_std_lib.h"
#include "POUS.h"
#include "POUS.c"

int main(void) {
  DRIVE_data__ d = {0};
  DRIVE_init__(&d, 0);
  for (int scan = 0; scan < 3; scan++) {
    __SET_VAR(d., A, , nondet_bool());
    __SET_VAR(d., B, , nondet_bool());
    __SET_VAR(d., C, , nondet_bool());
    DRIVE_body__(&d);
    __ESBMC_assert(!__GET_VAR(d.Y,) || (__GET_VAR(d.A,) && __GET_VAR(d.B,) && __GET_VAR(d.C,)), "P1");
  }
  return 0;
}

Function block diagram¶

Recorded 2026-08-27T19:24:15Z. Every build ran the same command.

runner/record_via_c.py benchmarks/manufacturing/fbd_comb_and/program.xml benchmarks/manufacturing/fbd_comb_and/props.yaml true --tool master=<path-to-esbmc>

which generates the C below and hands it to ESBMC as:

esbmc <generated>/harness.c -I $PLC_TOOLS/matiec/lib/C -I <generated> --k-induction --timeout 120s

Translated by Beremiz df4370c and MatIEC 7949c0b.

build	ESBMC	verdict	expected	outcome	cpu
master	8.4.0 `d88a9fa4`	`SAFE`	`SAFE`	correct	0.855 s

master found its solution by the forward condition; all states are reachable (k = 4).

What ESBMC was given. The harness the adapter generated, with the property written over the variables MatIEC emitted.

#include "iec_std_lib.h"
#include "POUS.h"
#include "POUS.c"

int main(void) {
  DRIVE_data__ d = {0};
  DRIVE_init__(&d, 0);
  for (int scan = 0; scan < 3; scan++) {
    __SET_VAR(d., A, , nondet_bool());
    __SET_VAR(d., B, , nondet_bool());
    __SET_VAR(d., C, , nondet_bool());
    DRIVE_body__(&d);
    __ESBMC_assert(!__GET_VAR(d.Y,) || (__GET_VAR(d.A,) && __GET_VAR(d.B,) && __GET_VAR(d.C,)), "P1");
  }
  return 0;
}

Ladder, for comparison¶

Recorded 2026-08-27T19:24:11Z. Every build ran the same command.

runner/record_via_c.py benchmarks/manufacturing/g_comb_and/program.xml benchmarks/manufacturing/g_comb_and/props.yaml true --tool master=<path-to-esbmc>

which generates the C below and hands it to ESBMC as:

esbmc <generated>/harness.c -I $PLC_TOOLS/matiec/lib/C -I <generated> --k-induction --timeout 120s

Translated by Beremiz df4370c and MatIEC 7949c0b.

build	ESBMC	verdict	expected	outcome	cpu
master	8.4.0 `d88a9fa4`	`SAFE`	`SAFE`	correct	0.833 s

master found its solution by the forward condition; all states are reachable (k = 4).

What ESBMC was given. The harness the adapter generated, with the property written over the variables MatIEC emitted.

#include "iec_std_lib.h"
#include "POUS.h"
#include "POUS.c"

int main(void) {
  G_COMB_AND_data__ d = {0};
  G_COMB_AND_init__(&d, 0);
  for (int scan = 0; scan < 3; scan++) {
    __SET_VAR(d., A, , nondet_bool());
    __SET_VAR(d., B, , nondet_bool());
    __SET_VAR(d., C, , nondet_bool());
    G_COMB_AND_body__(&d);
    __ESBMC_assert(!__GET_VAR(d.Y,) || (__GET_VAR(d.A,) && __GET_VAR(d.B,) && __GET_VAR(d.C,)), "P1");
  }
  return 0;
}

Four notations, one program, four proofs, all closing by the forward condition at k = 4. The ladder column is the interesting one: it is the same file the panel further up this page verified through the LD front end, and it now has a second verdict reached without that front end at all. Two independent routes agreeing is worth more than one route insisting.

Read the generated harness in any of those panels. The property is not carried over from the YAML file: it is written out over the C variables MatIEC emitted, which is the price of this route and the reason it answers is this program correct rather than does the ladder front end read it correctly.

One notation is missing from the four. The K-LD textual rung, OTE(Y) := XIC(A) * XIC(B) * XIC(C);, is in the download table and no tool here reads it: ESBMC XML-parses the file and fails, and Beremiz only reads PLCopen. NuSMV confirms it, through the suite's converter and a translation to SMV that we wrote, which is why the suite keeps more than one tool in view.

Try it¶

Change the property and predict the answer before you run it.

!Y || A claims that Y implies A alone. Weaker than the original, so it still holds.
Y || !A claims the reverse, that A alone is enough to energize Y. Run it and ESBMC hands you a scan where A is closed, one of the others is not, and Y stays low.

The second is the useful habit. Write the property you expect to fail, and check that the tool fails it for the reason you expected, because a verifier that says SUCCESSFUL to everything is telling you nothing.