tof hold (graphical LD twin)¶


suite id	`g_tof_hold`
domain	hvac
language	LD-graphical
difficulty	medium
validation status	candidate
origin	authored
license	CC-BY-4.0
syntax pair of	`ld_tof_hold`

Graphical twin of ld_tof_hold. The textual twin's property, Light implies Pir or Button, is false of an off-delay and is kept as implies_input.props.yaml; props.yaml carries the requirement that does hold

What is proved¶

From benchmarks/hvac/g_tof_hold/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`	`!Pir \|\| Light`	While the PIR sees motion the lamp must be lit; the off-delay only extends that, it never shortens it.

Variants¶

file	expected verdict	violates	method
`program.xml`	SAFE	none	expert

Files¶

file	what it is	size	sha256
`benchmark.yml`	benchmark metadata	0.8 KB	`b9a71616a1bf`
`implies_input.props.yaml`	property file	0.2 KB	`64d844e0813d`
`program.xml`	ladder program, PLCopen XML	3.1 KB	`1d1fcd19f094`
`props.yaml`	property file	0.2 KB	`ffec421ab81f`

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.xml

PROGRAM g_tof_hold
VAR_INPUT
    Pir : BOOL;
    Button : BOOL;
END_VAR

VAR_OUTPUT
    Light : BOOL;
END_VAR

VAR
    TOF0 : TOF;
END_VAR


TOF0(IN:=Pir, PT:=T#50ms);
Light := (TOF0.Q OR Button);

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.

tof_hold (props.yaml, expected SAFE): master SAFE
tof_implies_input (implies_input.props.yaml, expected VIOLATION): master VIOLATION