Reject gate fault latch with gate, counter, and line-stop readouts¶


suite id	`reject_gate_triple_output`
domain	packaging
language	LD-textual
difficulty	easy
validation status	validated
origin	authored
license	CC-BY-4.0

Authored for the esbmc-plc-benchmark-suite to close a training gap found by ml/scripts/build_task_slice.py: a latch that fans out to three independent readouts, where the safety property is about the trigger, not the readouts' mutual relationship.

What is proved¶

From benchmarks/packaging/reject_gate_triple_output/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`	`defect_detect -> gate_actuate`	A detected defect must actuate the reject gate in the same scan; the property is grounded in the trigger, not in gate_actuate's relationship to the two other readouts (counter_enable, line_stop) the same internal latch happens to also drive.
`P2`	`reachability`	reachable: `defect_detect && !gate_actuate`	Witness: defect_detect=1 reaches gate_actuate=0 in bomb, because reject_latch no longer triggers on the defect sensor at all.

Variants¶

file	expected verdict	violates	method
`clean.ld`	SAFE	none	expert
`bomb.ld`	VIOLATION	`P1`	fault-injection

Files¶

file	what it is	size	sha256
`benchmark.yml`	benchmark metadata	1.2 KB	`d0ff0d612aa8`
`bomb.ld`	ladder program, textual DSL	0.5 KB	`b88f86d862f0`
`clean.ld`	ladder program, textual DSL	0.3 KB	`e25b6de44e92`
`props.yaml`	property file	0.6 KB	`09f7a7f46802`

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.

reject_gate_triple_output__bomb (props.yaml, expected VIOLATION): v8.4 error — ingestion gate failed on v8.4
reject_gate_triple_output__clean (props.yaml, expected SAFE): v8.4 VIOLATION