45 lines
No EOL
1.1 KiB
Text
45 lines
No EOL
1.1 KiB
Text
---- MODULE traffic_lights_spain ----
|
|
VARIABLE
|
|
light, \* Current light color
|
|
going_to_green \* Direction of transition (TRUE if going to green, FALSE if going to red)
|
|
|
|
Colors == {"red", "yellow", "green"}
|
|
|
|
Init ==
|
|
/\ light = "red"
|
|
/\ going_to_green = TRUE \* Starting sequence towards green
|
|
|
|
Next ==
|
|
\/ /\ light = "red"
|
|
/\ going_to_green = TRUE
|
|
/\ light' = "yellow"
|
|
/\ UNCHANGED going_to_green
|
|
\/ /\ light = "yellow"
|
|
/\ going_to_green = TRUE
|
|
/\ light' = "green"
|
|
/\ going_to_green' = FALSE
|
|
\/ /\ light = "green"
|
|
/\ going_to_green = FALSE
|
|
/\ light' = "yellow"
|
|
/\ UNCHANGED going_to_green
|
|
\/ /\ light = "yellow"
|
|
/\ going_to_green = FALSE
|
|
/\ light' = "red"
|
|
/\ going_to_green' = TRUE
|
|
|
|
vars == <<light, going_to_green>>
|
|
|
|
Spec == Init /\ [][Next]_vars
|
|
|
|
\* Safety properties
|
|
TypeOK ==
|
|
/\ light \in Colors
|
|
/\ going_to_green \in BOOLEAN
|
|
|
|
\* No regression in yellow state
|
|
NoRegression ==
|
|
[][light = "yellow" =>
|
|
\/ (going_to_green /\ light' = "green")
|
|
\/ (~going_to_green /\ light' = "red")]_vars
|
|
|
|
==== |