Substation breaker closing-coil dual interlock¶
| suite id | breaker_earth_trip_interlock |
| domain | power_substation |
| language | ST |
| difficulty | easy |
| validation status | candidate |
| origin | authored |
| license | CC-BY-4.0 |
Authored alongside elevator_door_motion_interlock and mixer_lid_stall_interlock to give the corpus's 2-invariant-plus-reachability-witness shape enough repetition to be learned. Both guards act on the same output (closing_coil), unlike the other two benchmarks added with it, to also cover the shared-actuator structural variant. See ml/README.md.
What is proved¶
From benchmarks/power_substation/breaker_earth_trip_interlock/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 |
!(closing_coil && earth_switch_closed) |
The closing coil must never energise while the earthing switch is closed; closing onto an earthed line is catastrophic. |
P2 |
invariant |
!(closing_coil && trip_latched) |
The closing coil must never energise while a protection trip is latched; closing into a known fault re-energises it. |
P3 |
reachability |
reachable: closing_coil && trip_latched |
Trigger synthesis: a witness recovers the bad state P2 forbids, so the counterexample search has a concrete target when the trip interlock 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 | 5b4d5cff3051 |
bomb.st |
structured text | 1.1 KB | 653e28c18672 |
clean.st |
structured text | 1.1 KB | 2c2d04309387 |
props.yaml |
property file | 0.7 KB | 5aed4aecf96c |
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.