ctd load (graphical LD twin)¶


suite id	`g_ctd_load`
domain	elevator
language	LD-graphical
difficulty	medium
validation status	candidate
origin	authored
license	CC-BY-4.0
syntax pair of	`ld_ctd_load`

Graphical twin of ld_ctd_load. The IEC LD pin is wired but the graphical front end reads only R, so the modelled counter never reloads

What is proved¶

From benchmarks/elevator/g_ctd_load/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`	`!(Empty && Load)`	Load is dominant: the count-down Empty flag and Load never hold together.

Variants¶

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

Files¶

file	what it is	size	sha256
`benchmark.yml`	benchmark metadata	0.7 KB	`74023cd70113`
`program.xml`	ladder program, PLCopen XML	3.2 KB	`cea534618ccf`
`props.yaml`	property file	0.2 KB	`3223ae0dbc67`

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_ctd_load
VAR_INPUT
    Pulse : BOOL;
    Load : BOOL;
END_VAR

VAR_OUTPUT
    Empty : BOOL;
END_VAR

VAR
    CTD0 : CTD;
END_VAR


CTD0(CD:=Pulse, PV:=2, LD:=Load);
Empty := CTD0.Q;

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.

ctd_load (props.yaml, expected SAFE): master VIOLATION