A junction that shows two greens¶

The first two machines in this part could hurt one person standing in the wrong place. A junction hurts people who never see the controller and have no reason to distrust it.

The machine¶

A two-phase signalized junction. North-south and east-west each have a demand input from a loop detector, and each has a green. East-west holds priority: north-south greens only when east-west is not asking.

Conflicting greens is the failure everyone means when they say a signal has failed. Two streams of traffic are given right of way through the same conflict area at the same time, at whatever speed the approach allows, and both drivers believe they have it.

benchmarks/traffic/g_traffic_light/props.yaml

format_version: "0.1"
properties:
  - id: P1
    kind: mutual_exclusion
    variables: [ns_green, ew_green]
    justification: "Conflicting green phases must never be energised simultaneously."

This is the first mutual_exclusion property in this part. It takes a variable list rather than an expression and becomes assert(!(ns_green && ew_green)), which is the same claim the invariants in 2.1 and 2.2 made, written in the form that says what it is.

The correct program¶

ns_green := NOT ew_req AND ns_req
ew_green := ew_req

The conflict is prevented by one normally closed contact. East-west asking is enough to hold north-south red, and there is no path by which both coils energize.

file	what it is	size	sha256
`clean.xml`	ladder program, PLCopen XML	2.4 KB	`647b0ea73adf`
`bomb.xml`	ladder program, PLCopen XML	2.9 KB	`6e660342835c`
`props.yaml`	property file	0.2 KB	`108b172e36e2`

Recorded 2026-09-04T23:40:58Z. Every build ran the same command.

cp benchmarks/traffic/g_traffic_light/clean.xml benchmarks/traffic/g_traffic_light/clean.ld
esbmc benchmarks/traffic/g_traffic_light/clean.ld --ld-props benchmarks/traffic/g_traffic_light/props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 20s

Recorded 2026-09-04T23:40:58Z.

v8.4

cp benchmarks/traffic/g_traffic_light/clean.xml benchmarks/traffic/g_traffic_light/clean.ld
esbmc benchmarks/traffic/g_traffic_light/clean.ld --ld-props benchmarks/traffic/g_traffic_light/props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 20s

build	ESBMC	verdict	expected	outcome	ingestion gate	cpu
v8.4	8.4.0	`SAFE`	`SAFE`	correct	pass	0.017 s

v8.4 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.

v8.4

     1: IF !1 THEN GOTO 2
        ASSIGN ns_req=NONDET(_Bool);
        ASSIGN ew_req=NONDET(_Bool);
        ASSIGN maint=NONDET(_Bool);
        ASSIGN ew_green=1 && ew_req;
        ASSIGN ns_green=1 && !ew_req && ns_req;
        GOTO 1
     2:

The same junction, bypassed¶

The bomb is the shape you have now seen twice, and the third time it should be recognizable before you read the caption: a parallel branch that conducts exactly when the protective contact would have opened.

ns_green := (NOT ew_req OR (ew_req AND maint)) AND ns_req

Recorded 2026-09-04T23:40:58Z. Every build ran the same command.

cp benchmarks/traffic/g_traffic_light/bomb.xml benchmarks/traffic/g_traffic_light/bomb.ld
esbmc benchmarks/traffic/g_traffic_light/bomb.ld --ld-props benchmarks/traffic/g_traffic_light/props.yaml --incremental-bmc --unwind 20 --ld-scan-watchdog --ld-scan-budget 8 --timeout 20s

Recorded 2026-09-04T23:40:58Z.

v8.4

cp benchmarks/traffic/g_traffic_light/bomb.xml benchmarks/traffic/g_traffic_light/bomb.ld
esbmc benchmarks/traffic/g_traffic_light/bomb.ld --ld-props benchmarks/traffic/g_traffic_light/props.yaml --incremental-bmc --unwind 20 --ld-scan-watchdog --ld-scan-budget 8 --timeout 20s

build	ESBMC	verdict	expected	outcome	ingestion gate	cpu
v8.4	8.4.0	`VIOLATION`	`VIOLATION`	correct	pass	0.013 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.

v8.4

     1: IF !1 THEN GOTO 2
        ASSIGN ns_req=NONDET(_Bool);
        ASSIGN ew_req=NONDET(_Bool);
        ASSIGN maint=NONDET(_Bool);
        ASSIGN ew_green=1 && ew_req;
        ASSIGN ns_green=1 && !ew_req && ns_req;
        ASSIGN ns_green=1 && ew_req && maint && ns_req;
        GOTO 1
     2:

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.

v8.4

State 1  thread 0
----------------------------------------------------
  ns_req = 1

State 2  thread 0
----------------------------------------------------
  ew_req = 1

State 3  thread 0
----------------------------------------------------
  maint = 1

State 4  thread 0
----------------------------------------------------
  ew_green = 1

State 5  thread 0
----------------------------------------------------
  ns_green = 1

State 6 file benchmarks/traffic/g_traffic_light/bomb.ld thread 0
----------------------------------------------------
Violated property:
  file benchmarks/traffic/g_traffic_light/bomb.ld
  P1
  !(ns_green && ew_green)

ns_req = 1   ew_req = 1   maint = 1   ->   ns_green = 1   and   ew_green = 1

Both directions green, both detectors demanding, one maintenance input asserted.

What this property does not say¶

Here is where a junction differs from a conveyor, and where an honest benchmark has to be careful about what it claims.

!(ns_green && ew_green) is conflict-freedom and nothing else. Verify it and these remain wide open:

No intergreen. Nothing stops ns_green dropping and ew_green rising in consecutive scans, with no amber and no all-red between them. On a real junction that is the interval that clears the conflict area, and it is measured in seconds, not scans.

No minimum green. A green can appear for exactly one scan and vanish.

Starvation. Hold ew_req high, by a stuck detector or a shorted loop, and ns_green never comes up again. The safety property is perfectly content with a junction that never serves one arm.

None of those three is expressible over this program, and that is not a limitation of the verifier. The program has no memory of the previous scan and no notion of elapsed time, so there is nothing to write the requirement over. Stating an intergreen means adding the timer machinery from lesson 1.6, and then stating it against a model whose tick is a scan rather than a second.

Why it is still worth proving¶

Because the three things it does not say cost delay, and the one thing it does say costs lives. Conflict-freedom is the property that a signal engineer will not compromise, and it is exactly the property this program is small enough to prove outright rather than argue about.

The benchmark claims conflict-freedom and no more. A suite that says what it checks, and is quiet about what it does not, is worth more to somebody validating a tool than one whose properties imply a completeness they never had.