star-delta starter with open transition¶


suite id	`g_star_delta`
domain	motor_control
language	LD-graphical
difficulty	easy
validation status	validated
origin	authored
license	CC-BY-4.0

Authored as the contactor-selection half of a wye-delta starter; the start/stop latch that drives Call is upstream and is the subject of lesson 1.4

What is proved¶

From benchmarks/motor_control/g_star_delta/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: `Star`, `Delta`	Closing the star and delta contactors together shorts the supply through the winding ends.

Variants¶

file	expected verdict	violates	method
`program.xml`	SAFE	none	cross-tool-consensus
`no_deadtime.xml`	SAFE	none	fault-injection

Files¶

file	what it is	size	sha256
`benchmark.yml`	benchmark metadata	1.2 KB	`1d7cc1d46c3a`
`deadtime_check.props.yaml`	property file	0.5 KB	`d245d377774e`
`no_deadtime.xml`	ladder program, PLCopen XML	2.6 KB	`665abfd022dc`
`program.xml`	ladder program, PLCopen XML	2.8 KB	`cdd9bfe99115`
`props.yaml`	property file	0.2 KB	`e347ee93997f`

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.

no_deadtime.xmlprogram.xml

PROGRAM g_star_delta_no_deadtime
VAR_INPUT
    Call : BOOL;
    StarDone : BOOL;
    DeadDone : BOOL;
END_VAR

VAR_OUTPUT
    Star : BOOL;
    Delta : BOOL;
END_VAR


Star := (Call AND NOT StarDone);
Delta := (Call AND StarDone);

END_PROGRAM

PROGRAM g_star_delta
VAR_INPUT
    Call : BOOL;
    StarDone : BOOL;
    DeadDone : BOOL;
END_VAR

VAR_OUTPUT
    Star : BOOL;
    Delta : BOOL;
END_VAR


Star := (Call AND NOT StarDone);
Delta := ((Call AND StarDone) AND DeadDone);

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_star_delta__no_deadtime (props.yaml, expected SAFE): v8.4 SAFE
g_star_delta__program (props.yaml, expected SAFE): v8.4 SAFE
stardelta_deadtime_closed (deadtime_check.props.yaml, expected SAFE): master SAFE
stardelta_deadtime_open (deadtime_check.props.yaml, expected VIOLATION): master VIOLATION