Skip to content
Petri Nets templates

Petri Net — Level Crossing Interlock

Interlock model of an automatic half-barrier crossing where the protecting signal can only clear once the barriers are proved down and the crossing is proved clear.

Template previewPetri Nets
Automatic half-barrier crossing interlockTrain on the approa…≤1Barriers up, road o…≤1Crossing proved cle…≤1Barriers proved down≤1Protecting signal c…≤1Train on the crossi…≤1Approach treadle stru…enabledClear the protecting …Train enters the cros…Train clear, raise ba…Reachable markings56 places · 4 transitionsTerminatesyes1 final markingLive transitions4/4every one firesSafe places6/6bound ≤ 1 tokenConservation laws21 place in none5 reachable markings, 6 places, 4 transitions — bounded, deadlock-free, and every transition fires: it stops at 1 final marking, each of them a net that used up what it was given rather than one …This net runs to completion and stops at Barriers up, road open 1 · Crossing proved clear 1. Nothing is enabled there, and it is not a deadlock: every transition still short of an input is short of one that NOTHING in this n…Conservation law: Barriers up, road open + Barriers proved down + Protecting signal cleared + Train on the crossing = 1, at every reachable marking, for ever. No firing of any transition can change it — that is proved from t…Conservation law: Crossing proved clear + Protecting signal cleared + Train on the crossing = 1, at every reachable marking, for ever. No firing of any transition can change it — that is proved from the incidence matrix, not…1 place is weighted by no conservation law — `Train on the approach circuit`. Nothing in the structure of this net holds what it holds constant, so its token count is free to drift with the firing sequence. That is where an …

Make it your own.

title Automatic half-barrier crossing interlock

place trainApproach tokens 1 "Train on the approach circuit"
place roadOpen tokens 1 "Barriers up, road open"
place crossingClear tokens 1 "Crossing proved clear"
place barriersDown tokens 0 "Barriers proved down"
place signalClear tokens 0 "Protecting signal cleared"
place crossingOccupied tokens 0 "Train on the crossing"
transition strike "Approach treadle struck"
transition clearSignal "Clear the protecting signal"
transition occupy "Train enters the crossing"
transition restore "Train clear, raise barriers"

trainApproach -> strike
roadOpen -> strike
strike -> barriersDown
barriersDown -> clearSignal
crossingClear -> clearSignal
clearSignal -> signalClear
signalClear -> occupy
occupy -> crossingOccupied
crossingOccupied -> restore
restore -> roadOpen
restore -> crossingClear