20 lines
413 B
Text
20 lines
413 B
Text
---- MODULE traffic_lights ----
|
|
VARIABLE light \* Current light color
|
|
|
|
Colors == {"red", "yellow", "green"}
|
|
|
|
Init == light = "red"
|
|
|
|
Next ==
|
|
\/ /\ light = "red"
|
|
/\ light' = "green"
|
|
\/ /\ light = "green"
|
|
/\ light' = "yellow"
|
|
\/ /\ light = "yellow"
|
|
/\ light' = "red"
|
|
|
|
Spec == Init /\ [][Next]_light
|
|
|
|
\* Safety property: light is always a valid color
|
|
TypeOK == light \in Colors
|
|
====
|