burner purge, light-off and lockout (ST twin)¶


suite id	`st_burner_purge`
domain	hvac
language	ST
difficulty	easy
validation status	candidate
origin	authored
license	CC-BY-4.0
syntax pair of	`g_burner_purge`

Structured Text rendering of g_burner_purge, for cross-language comparison of the same machine

What is proved¶

From benchmarks/hvac/st_burner_purge/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`	`!MainValve \|\| (PurgeDone && FlameProven)`	EN 298 light-off order: the main gas valve opens only after the purge has completed and the flame is proven.

Variants¶

file	expected verdict	violates	method
`burner_purge.st`	SAFE	none	expert

Files¶

file	what it is	size	sha256
`benchmark.yml`	benchmark metadata	0.5 KB	`5a483921b743`
`burner_purge.st`	structured text	0.8 KB	`0a41e161455d`
`props.yaml`	property file	0.2 KB	`0d8c0bb4baa6`

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.

st_burner_purge__burner_purge__viac via C (props.yaml, expected SAFE): master SAFE