Forward/reverse motor interlock (graphical LD)¶


suite id	`g_motor_interlock`
domain	motor_control
language	LD-graphical
difficulty	easy
validation status	validated
origin	authored
license	CC-BY-4.0
syntax pair of	`motor_interlock`

Graphical PLCopen XML twin of benchmark 'motor_interlock' (syntax-coverage pair)

What is proved¶

From benchmarks/motor_control/motor_interlock/props.yaml. What each kind claims, and what it becomes on either route, is on The properties we prove.

id	kind	claim	requirement
`P1`	`mutual_exclusion`	never true together: `Motor_A`, `Motor_B`	Forward/reverse contactors must never be energised together (contactor short / mechanical damage).
`P2`	`reachability`	reachable: `Motor_A && Motor_B`	Trigger synthesis: a witness recovers the secret-knock input combination that violates the interlock.

Variants¶

file	expected verdict	violates	method
`clean.xml`	SAFE	none	cross-tool-consensus
`bomb.xml`	VIOLATION	`P1`	fault-injection

Files¶

file	what it is	size	sha256
`benchmark.yml`	benchmark metadata	1.1 KB	`0cfdcf2e630f`
`bomb.xml`	ladder program, PLCopen XML	4.2 KB	`2edbdad821a7`
`clean.xml`	ladder program, PLCopen XML	3.2 KB	`7b3eaffbf490`
`witness.props.yaml`	property file	0.4 KB	`f1dbc9a1a972`

Structured text, derived¶

Read off the ladder graph by runner/ld_to_st.py: every rung's contacts and coils rewritten as IEC 61131-3 assignments, in the same series/parallel logic the PLCopen XML encodes. This is a reading aid, not a second source of expected verdicts; ESBMC verifies the ladder program shown above, never this rendering.

bomb.xmlclean.xml

PROGRAM drive
VAR_INPUT
    fwd : BOOL;
    rev : BOOL;
    maint : BOOL;
END_VAR

VAR_OUTPUT
    Motor_A : BOOL;
    Motor_B : BOOL;
END_VAR


Motor_A := ((NOT rev OR (rev AND maint)) AND fwd);
Motor_B := rev;

END_PROGRAM

PROGRAM drive
VAR_INPUT
    fwd : BOOL;
    rev : BOOL;
    maint : BOOL;
END_VAR

VAR_OUTPUT
    Motor_A : BOOL;
    Motor_B : BOOL;
END_VAR


Motor_A := (fwd AND NOT rev);
Motor_B := rev;

END_PROGRAM

Notes¶

g_motor_interlock — graphical LD twin¶

Graphical PLCopen XML (tc6_0200) twin of the textual benchmark motor_interlock — a syntax-coverage pair: identical logic in graphical LD, used to test whether a tool handles both PLCopen encodings. Properties are inherited from the textual twin (properties_file: ../motor_interlock/props.yaml).

Logic¶

clean.xml: two rungs — Motor_A := fwd AND NOT rev, Motor_B := rev. Mutually exclusive → SAFE.
bomb.xml: adds an OR-branch fwd AND rev AND maint into both coils (the secret-knock LLB), so the knock energises both motors → VIOLATION of P1.

Modeling note¶

The ST original re-evaluates coils each scan; the graphical twin is non-latching to match. The knock's OR is modeled by factoring fwd to the end (Motor_A = ((NOT rev) OR (rev AND maint)) AND fwd) so the OR-junction lands on a contact (multiple <connection> children in a contact's connectionPointIn) — the junction pattern the parseable corpus (e.g. PLC-LD-dataset/legitimate_lstop_eq.xml) is proven to use — rather than on the coil. Motor_B = rev needs no bomb branch: rev is already TRUE during the knock, so the interlock breaks the moment Motor_A also energises.

Verified so far: namespace (tc6_0200), element set (powerrail/contact/coil), and the contact-junction construct all match the corpus ESBMC-GraphPLC parses. Not yet run through the actual frontend (no binary in the authoring environment) — see suite README for the exact --ld-props command.

Recorded runs¶

A task can carry two routes. ld is ESBMC's ladder front end reading the program directly. via C is the same solver reached through Beremiz and MatIEC, which is the only route that reaches ST, IL, FBD and SFC; see How ESBMC-PLC works.

g_motor_interlock__bomb (props.yaml, expected VIOLATION): v8.4 VIOLATION
g_motor_interlock__bomb__viac via C (props.yaml, expected VIOLATION): master VIOLATION
g_motor_interlock__clean (props.yaml, expected SAFE): v8.4 SAFE
g_motor_interlock__clean__viac via C (props.yaml, expected SAFE): master SAFE
motor_witness_bomb (witness.props.yaml, expected VIOLATION): master VIOLATION
motor_witness_clean (witness.props.yaml, expected SAFE): master SAFE