Benchmarks
|
|
| suite id |
g_traffic_light_pedestrian |
| domain |
traffic |
| language |
LD-graphical |
| difficulty |
medium |
| validation status |
candidate |
| origin |
beremiz |
| license |
GPL-2.0-or-later |
Beremiz sample projects, github.com/beremiz/beremiz (exemples/svghmi_traffic_light/plc.xml); Beremiz is Free Software for machine automation
What is proved
From benchmarks/traffic/g_traffic_light_pedestrian/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 |
!(RED_LIGHT && GREEN_LIGHT) |
Traffic safety hazard: for the same approach, red and green lights must never be illuminated together. |
P2 |
invariant |
!(PEDESTRIAN_GREEN_LIGHT && GREEN_LIGHT) |
Pedestrian safety: cars must not have green while pedestrians have green on a conflicting movement. |
Variants
| file |
expected verdict |
violates |
method |
plc.xml |
SAFE |
none |
expert |
Files
| file |
what it is |
size |
sha256 |
NOTES.md |
notes |
0.7 KB |
305bf9afc90b |
benchmark.yml |
benchmark metadata |
1.0 KB |
bb40de30f757 |
plc.xml |
ladder program, PLCopen XML |
57.8 KB |
f7e22a67fa51 |
props.yaml |
property file |
0.4 KB |
0d6f9e0491bf |
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_traffic_light_pedestrian__plc (props.yaml, expected SAFE): v8.4 SAFE — ingestion gate failed on v8.4