comb or (graphical LD twin)¶


suite id	`g_comb_or`
domain	building_automation
language	LD-graphical
difficulty	easy
validation status	validated
origin	authored
license	CC-BY-4.0
syntax pair of	`ld_comb_or`

Graphical PLCopen XML twin of the K-LD textual benchmark (syntax-coverage pair)

What is proved¶

From benchmarks/building_automation/g_comb_or/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`	`!Y \|\| A \|\| B`	Output Y is energised only when contact A or B is closed.

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	`21440ee8094a`
`branch_check.props.yaml`	property file	0.4 KB	`fc3a68ba4029`
`program.xml`	ladder program, PLCopen XML	1.9 KB	`6f4c9406570c`
`props.yaml`	property file	0.2 KB	`1c69e0ba66fd`

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_comb_or
VAR_INPUT
    A : BOOL;
    B : BOOL;
END_VAR

VAR_OUTPUT
    Y : BOOL;
END_VAR


Y := (A OR B);

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.

comb_or (props.yaml, expected SAFE): master SAFE
comb_or_branch (branch_check.props.yaml, expected VIOLATION): master VIOLATION
g_comb_or__program__viac via C (props.yaml, expected SAFE): master SAFE