Benchmarks

Water treatment dosing pump fault lockout

suite id	dosing_pump_lockout
domain	water_treatment
language	ST
difficulty	medium
validation status	candidate
origin	authored
license	CC-BY-4.0

Authored to target the temporal/procedural-phrasing translation gap identified in the kiln_door_lockout diagnosis, phrased as a behavioral consequence clause ('any subsequent start command is ignored ... regardless of how many times start is pressed') rather than a state description, to vary the surface form once more. See ml/README.md.

What is proved

From benchmarks/water_treatment/dosing_pump_lockout/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	!(dosing_pump && level_low)	The dosing pump must never run while the tank level is below the low-level cutoff.
P2	invariant	!(dosing_pump && dry_run_fault)	If the pump ever runs dry, any subsequent start command must be ignored and the pump must stay off, until an operator acknowledges the fault.
P3	reachability	reachable: dosing_pump && dry_run_fault	Trigger synthesis: a witness recovers the bad state P2 forbids, so the counterexample search has a concrete target when the fault acknowledgement requirement is bypassed.

Variants

file	expected verdict	violates	method
clean.st	SAFE	none	expert
bomb.st	VIOLATION	P2	fault-injection

Files

file	what it is	size	sha256
benchmark.yml	benchmark metadata	1.4 KB	e32180d13912
bomb.st	structured text	1.2 KB	e5fcf969c706
clean.st	structured text	1.2 KB	87d4004260fc
props.yaml	property file	0.7 KB	8d1e404a6403

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.

No ESBMC run is recorded against this task yet. The lessons carry the recorded runs; see Reproducing to make your own.