65 lines
1.9 KiB
Text
65 lines
1.9 KiB
Text
---- MODULE fsm3 ----
|
|
(* from https://www.learntla.com/topics/state-machines.html *)
|
|
|
|
(*--algorithm lamp
|
|
variable state = "BothOff";
|
|
|
|
macro transition(from, set_to) begin
|
|
await state = from;
|
|
with to \in set_to do
|
|
state := to;
|
|
end with;
|
|
end macro;
|
|
|
|
process StateMachine = "SM" \* No semicolon here !
|
|
begin
|
|
Action:
|
|
either transition("BothOff", {"LampOff", "WallOff"}); \* We turned the lamp or wall switch on
|
|
or transition("LampOff", {"BothOff", "On"}) \* We turned the wall switch on or off
|
|
or transition("WallOff", {"BothOff", "On"}) \* We turned the lamp switch on or off
|
|
or transition("On", {"LampOff", "WallOff"}) \* We turned the wall switch on or off
|
|
end either;
|
|
goto Action;
|
|
end process;
|
|
end algorithm *)
|
|
\* BEGIN TRANSLATION (chksum(pcal) = "cdedebdc" /\ chksum(tla) = "83e9daae")
|
|
VARIABLES state, pc
|
|
|
|
vars == << state, pc >>
|
|
|
|
ProcSet == {"SM"}
|
|
|
|
Init == (* Global variables *)
|
|
/\ state = "BothOff"
|
|
/\ pc = [self \in ProcSet |-> "Action"]
|
|
|
|
Action == /\ pc["SM"] = "Action"
|
|
/\ \/ /\ state = "BothOff"
|
|
/\ \E to \in {"LampOff", "WallOff"}:
|
|
state' = to
|
|
\/ /\ state = "LampOff"
|
|
/\ \E to \in {"BothOff", "On"}:
|
|
state' = to
|
|
\/ /\ state = "WallOff"
|
|
/\ \E to \in {"BothOff", "On"}:
|
|
state' = to
|
|
\/ /\ state = "On"
|
|
/\ \E to \in {"LampOff", "WallOff"}:
|
|
state' = to
|
|
/\ 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
|
|
====
|