Skip to content

Benchmarks

duty-standby pump station with alternation
suite id g_pump_alternation
domain water_treatment
language LD-graphical
difficulty medium
validation status validated
origin authored
license CC-BY-4.0

Authored as a licence-clean counterpart to the imported tank benchmarks: two pumps, one wet well, duty advancing each time the well empties

What is proved

From benchmarks/water_treatment/g_pump_alternation/props.yaml. What each kind claims, and what it becomes on either route, is on The properties we prove.

id kind claim requirement
P1 mutual_exclusion never true together: PumpA, PumpB Duty-standby: one pump runs at a time, so the standby stays available and the rising main is not over-pressured.

Variants

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

Files

file what it is size sha256
alternation_check.props.yaml property file 0.5 KB cf5d60e99918
benchmark.yml benchmark metadata 1.3 KB 4dd31b04fd57
program.xml ladder program, PLCopen XML 4.6 KB 8987780ce8bd
props.yaml property file 0.2 KB e07405d45fbc
stuck_duty.xml ladder program, PLCopen XML 4.2 KB 249cfc022e01

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 g_pump_alternation
VAR_INPUT
    LevelHigh : BOOL;
    LevelLow : BOOL;
END_VAR

VAR_OUTPUT
    Call : BOOL;
    Duty : BOOL;
    PumpA : BOOL;
    PumpB : BOOL;
END_VAR


Call := ((Call OR LevelHigh) AND NOT LevelLow);
Duty := ((Duty AND NOT LevelLow) OR (NOT Duty AND LevelLow));
PumpA := (Call AND NOT Duty);
PumpB := (Call AND Duty);

END_PROGRAM

PROGRAM g_pump_alternation_stuck_duty
VAR_INPUT
    LevelHigh : BOOL;
    LevelLow : BOOL;
END_VAR

VAR_OUTPUT
    Call : BOOL;
    Duty : BOOL;
    PumpA : BOOL;
    PumpB : BOOL;
END_VAR


Call := ((Call OR LevelHigh) AND NOT LevelLow);
Duty := (Duty AND LevelLow);
PumpA := (Call AND NOT Duty);
PumpB := (Call AND Duty);

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.

  • g_pump_alternation__program (props.yaml, expected SAFE): v8.4 SAFE
  • g_pump_alternation__stuck_duty (props.yaml, expected SAFE): v8.4 SAFE
  • pump_alternation_stuck (alternation_check.props.yaml, expected SAFE): master unknown
  • pump_alternation_working (alternation_check.props.yaml, expected VIOLATION): master VIOLATION