FWD/REV Motor Interlock¶


suite id	`g_fwd_rev_interlock`
domain	motor_control
language	LD-graphical
difficulty	easy
validation status	candidate
origin	lessons-electric-circuits
license	Design Science License

Lessons In Electric Circuits, Volume IV - Digital, Chapter 6 (Ladder Logic), by Tony R. Kuphaldt

What is proved¶

From benchmarks/motor_control/g_fwd_rev_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`	`invariant`	`!(M1_FWD && M2_REV)`	Motor Short-Circuit Hazard: Forward and Reverse contactors must never be closed at the same time.

Variants¶

file	expected verdict	violates	method
`fwd_rev_interlock.xml`	SAFE	none	cross-tool-consensus

Files¶

file	what it is	size	sha256
`NOTES.md`	notes	1.4 KB	`1b04fe27722d`
`benchmark.yml`	benchmark metadata	0.8 KB	`6dc5714ab2ac`
`fwd_rev_interlock.xml`	ladder program, PLCopen XML	4.5 KB	`f6f091217062`
`props.yaml`	property file	0.2 KB	`6003a3f456ff`

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.

fwd_rev_interlock.xml

PROGRAM main
VAR
    START_FWD : BOOL;
    START_REV : BOOL;
    STOP : BOOL;
    M1_FWD : BOOL;
    M2_REV : BOOL;
END_VAR


M1_FWD := (((START_FWD OR M1_FWD) AND NOT STOP) AND NOT M2_REV);
M2_REV := (((START_REV OR M2_REV) AND NOT STOP) AND NOT M1_FWD);

END_PROGRAM

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_fwd_rev_interlock__fwd_rev_interlock (props.yaml, expected SAFE): paper-pin SAFE