90 lines
2.6 KiB
Text
90 lines
2.6 KiB
Text
---- MODULE fsm ----
|
|
(* from https://www.learntla.com/topics/state-machines.html *)
|
|
|
|
(*--algorithm lamp
|
|
variable state = "BothOff";
|
|
|
|
process StateMachine = "SM" \* No semicolon here !
|
|
begin
|
|
Action:
|
|
either \* This is the FSM
|
|
\* We turned the lamp switch on
|
|
await state = "BothOff"; \* if the await is false, the BRANCH is blocked, but the other branches are still available
|
|
state := "WallOff";
|
|
or
|
|
\* We turned the wall switch on
|
|
await state = "BothOff";
|
|
state := "LampOff";
|
|
or
|
|
\* We turned the wall switch off
|
|
await state = "LampOff";
|
|
state := "BothOff";
|
|
or
|
|
\* We turned the wall switch on
|
|
await state = "LampOff";
|
|
state := "On";
|
|
or
|
|
\* We turned the lamp switch off
|
|
await state = "WallOff";
|
|
state := "BothOff";
|
|
or
|
|
\* We turned the wall switch on
|
|
await state = "WallOff";
|
|
state := "On";
|
|
or
|
|
\* We turned the lamp switch off
|
|
await state = "On";
|
|
state := "LampOff";
|
|
or
|
|
\* We turned the wall switch off
|
|
await state = "On";
|
|
state := "WallOff";
|
|
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
|
|
====
|