two-hand control on a power press, Type II¶


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

Authored from the Type II requirements in ISO 13851: anti-tie-down and anti-repeat, so a taped actuator cannot start a cycle. The program has no timer, so it does not model the 0.5 s synchronous-actuation window of Type II control

What is proved¶

From benchmarks/manufacturing/g_two_hand/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`	`!Stroke \|\| (LH && RH)`	ISO 13851 requires the ram to descend only while both actuators are held. Releasing either one stops the stroke.

Variants¶

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

Files¶

file	what it is	size	sha256
`benchmark.yml`	benchmark metadata	1.3 KB	`4286836110a6`
`program.xml`	ladder program, PLCopen XML	3.9 KB	`01ffc81a68d2`
`props.yaml`	property file	0.2 KB	`01c905820f28`
`tiedown_check.props.yaml`	property file	0.5 KB	`d1118ab8f733`
`type_i.xml`	ladder program, PLCopen XML	3.0 KB	`40e1b1f2e89c`

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.

program.xmltype_i.xml

PROGRAM g_two_hand
VAR_INPUT
    LH : BOOL;
    RH : BOOL;
END_VAR

VAR_OUTPUT
    BothOff : BOOL;
    Armed : BOOL;
    Stroke : BOOL;
END_VAR


BothOff := (NOT LH AND NOT RH);
Armed := ((Armed OR BothOff) AND NOT Stroke);
Stroke := (((Stroke OR Armed) AND LH) AND RH);

END_PROGRAM

PROGRAM g_two_hand_type_i
VAR_INPUT
    LH : BOOL;
    RH : BOOL;
END_VAR

VAR_OUTPUT
    BothOff : BOOL;
    Armed : BOOL;
    Stroke : BOOL;
END_VAR


BothOff := (NOT LH AND NOT RH);
Armed := BothOff;
Stroke := (LH AND RH);

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_two_hand__program (props.yaml, expected SAFE): v8.4 SAFE
g_two_hand__type_i (props.yaml, expected SAFE): v8.4 SAFE
twohand_tiedown_i (tiedown_check.props.yaml, expected SAFE): master SAFE
twohand_tiedown_ii (tiedown_check.props.yaml, expected VIOLATION): master VIOLATION