Skip to content
flowss
Start freeChecking your session
Petri Nets templates

Petri — traffic light

Simple three-phase traffic-light cycle.

Petri NetsUML & SoftwarePetri Nets syntax docs
Template previewPetri Nets
Traffic lightRed≤1Yellow≤1Green≤1T1enabledT2T3Reachable markings33 places · 3 transitionsTerminatesneverruns for everLive transitions3/3every one firesSafe places3/3bound ≤ 1 tokenConservation laws1every place covered3 reachable markings, 3 places, 3 transitions — bounded, deadlock-free, and every transition fires.Conservation law: Red + Yellow + Green = 1, at every reachable marking, for ever. No firing of any transition can change it — that is proved from the incidence matrix, not observed over a search.

Make it your own.

title "Traffic light"
place R tokens 1 "Red"
place Y tokens 0 "Yellow"
place G tokens 0 "Green"
transition T1
transition T2
transition T3
R -> T1
T1 -> G
G -> T2
T2 -> Y
Y -> T3
T3 -> R