23 lines
813 B
Text
23 lines
813 B
Text
---- MODULE fsm_tla ----
|
|
(* from https://www.learntla.com/topics/state-machines.html *)
|
|
|
|
VARIABLE state
|
|
|
|
Transition(a, b) ==
|
|
/\ state = a
|
|
/\ state' = b
|
|
|
|
Init == state = "BothOff"
|
|
|
|
Next ==
|
|
\/ Transition("BothOff", "WallOff") \* We turned the lamp switch on
|
|
\/ Transition("BothOff", "LampOff") \* We turned the wall switch on
|
|
\/ Transition("LampOff", "BothOff") \* We turned the wall switch off
|
|
\/ Transition("LampOff", "On") \* We turned the wall switch on
|
|
\/ Transition("WallOff", "BothOff") \* We turned the lamp switch off
|
|
\/ Transition("WallOff", "On") \* We turned the wall switch on
|
|
\/ Transition("On", "LampOff") \* We turned the lamp switch off
|
|
\/ Transition("On", "WallOff") \* We turned the wall switch off
|
|
|
|
Spec == Init /\ [][Next]_state
|
|
====
|