Benchmarks
PPU LD evolution 1 (graphical LD)
|
|
| suite id |
g_ppu_evolution_1 |
| domain |
manufacturing |
| language |
LD-graphical |
| difficulty |
easy |
| validation status |
candidate |
| origin |
ppu |
| license |
CC-BY-4.0 |
Named after the xPPU evolution scenarios (Vogel-Heuser et al.), but no code from x-PPU/PLC_TwinCAT_Projects is present. That repository is GPL-3.0 and holds Structured Text in TwinCAT .TcPOU form (Stack, Crane, TurningTable); this file is a single ladder rung, Open := A AND B, in PLCopen XML carrying a 3S/CODESYS vendorElement. Checked against the upstream repository on 2026-08-28, so CC-BY-4.0 stands.
What is proved
From benchmarks/manufacturing/g_ppu_evolution_1/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 |
!Open || (A && B) |
The Open coil is energised only when both series contacts A and B are closed. |
Variants
| file |
expected verdict |
violates |
method |
evolution_1.xml |
SAFE |
none |
expert |
Files
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_ppu_evolution_1__evolution_1 (props.yaml, expected SAFE): v8.4 SAFE