75 lines
2.4 KiB
Text
75 lines
2.4 KiB
Text
---- MODULE fsm2 ----
|
|
(* from https://www.learntla.com/topics/state-machines.html *)
|
|
|
|
(*--algorithm lamp
|
|
variable state = "BothOff";
|
|
|
|
macro transition(from, to) begin
|
|
await state = from;
|
|
state := to;
|
|
end macro;
|
|
|
|
process StateMachine = "SM" \* No semicolon here !
|
|
begin
|
|
Action:
|
|
either transition("BothOff", "WallOff"); \* We turned the lamp switch on
|
|
or transition("BothOff", "LampOff") \* We turned the wall switch on
|
|
or transition("LampOff", "BothOff") \* We turned the wall switch off
|
|
or transition("LampOff", "On") \* We turned the wall switch on
|
|
or transition("WallOff", "BothOff") \* We turned the lamp switch off
|
|
or transition("WallOff", "On") \* We turned the wall switch on
|
|
or transition("On", "LampOff") \* We turned the lamp switch off
|
|
or transition("On", "WallOff") \* We turned the wall switch off
|
|
end either;
|
|
goto Action;
|
|
end process;
|
|
end algorithm *)
|
|
\* BEGIN TRANSLATION (chksum(pcal) = "5c9b8d1e" /\ chksum(tla) = "e1654e57")
|
|
VARIABLES pc, state
|
|
|
|
vars == << pc, state >>
|
|
|
|
ProcSet == {"SM"}
|
|
|
|
Init == (* Global variables *)
|
|
/\ state = "BothOff"
|
|
/\ pc = [self \in ProcSet |-> "Action"]
|
|
|
|
Action == /\ pc["SM"] = "Action"
|
|
/\ \/ /\ state = "BothOff"
|
|
/\ state' = "WallOff"
|
|
\/ /\ state = "BothOff"
|
|
/\ state' = "LampOff"
|
|
\/ /\ state = "LampOff"
|
|
/\ state' = "BothOff"
|
|
\/ /\ state = "LampOff"
|
|
/\ state' = "On"
|
|
\/ /\ state = "WallOff"
|
|
/\ state' = "BothOff"
|
|
\/ /\ state = "WallOff"
|
|
/\ state' = "On"
|
|
\/ /\ state = "On"
|
|
/\ state' = "LampOff"
|
|
\/ /\ state = "On"
|
|
/\ state' = "WallOff"
|
|
/\ pc' = [pc EXCEPT !["SM"] = "Action"]
|
|
|
|
StateMachine == Action
|
|
|
|
(* Allow infinite stuttering to prevent deadlock on termination. *)
|
|
Terminating == /\ \A self \in ProcSet: pc[self] = "Done"
|
|
/\ UNCHANGED vars
|
|
|
|
Next == StateMachine
|
|
\/ Terminating
|
|
|
|
Spec == Init /\ [][Next]_vars
|
|
|
|
Termination == <>(\A self \in ProcSet: pc[self] = "Done")
|
|
|
|
\* END TRANSLATION
|
|
TypeOK == /\ state \in {"BothOff", "WallOff", "LampOff", "On"}
|
|
/\ pc \in [ProcSet -> {"Action"}]
|
|
|
|
NeverEnding == ~Termination
|
|
====
|