air compressor load/unload with minimum-off interlock¶


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

Authored as a receiver-pressure load/unload control with a minimum-off interlock, the usual guard against short-cycling the motor

What is proved¶

From benchmarks/manufacturing/g_compressor_cycle/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`	`!(Load && PressHigh)`	The compressor never loads at or above the cut-out pressure.

Variants¶

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

Files¶

file	what it is	size	sha256
`benchmark.yml`	benchmark metadata	1.2 KB	`7e2e1768a313`
`mincycle_check.props.yaml`	property file	0.4 KB	`874b14eae58f`
`program.xml`	ladder program, PLCopen XML	2.4 KB	`6fc4e650e9b3`
`props.yaml`	property file	0.2 KB	`1aff1839ace5`
`short_cycle.xml`	ladder program, PLCopen XML	2.2 KB	`57ac44247b5c`

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

PROGRAM g_compressor_cycle
VAR_INPUT
    PressLow : BOOL;
    PressHigh : BOOL;
    MinOffDone : BOOL;
END_VAR

VAR_OUTPUT
    Load : BOOL;
END_VAR


Load := ((Load OR (PressLow AND MinOffDone)) AND NOT PressHigh);

END_PROGRAM

PROGRAM g_compressor_cycle_short_cycle
VAR_INPUT
    PressLow : BOOL;
    PressHigh : BOOL;
    MinOffDone : BOOL;
END_VAR

VAR_OUTPUT
    Load : BOOL;
END_VAR


Load := ((Load OR PressLow) AND NOT PressHigh);

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.

compressor_mincycle_interlocked (mincycle_check.props.yaml, expected VIOLATION): master VIOLATION
compressor_mincycle_short (mincycle_check.props.yaml, expected SAFE): master SAFE
g_compressor_cycle__program (props.yaml, expected SAFE): v8.4 SAFE
g_compressor_cycle__short_cycle (props.yaml, expected SAFE): v8.4 SAFE