--------------------------- MODULE smachineDfish ---------------------------
\* Based on Miro Samek Practical Statecharts 4.2 An Annotated Example Practical State Charts - First edition has more explanation of this state machine.
EXTENDS Integers, TLC, Sequences, FiniteSets
\* from tla community modules
MapThenFoldSet(op(_,_), base, f(_), choose(_), S) ==
LET iter[s \in SUBSET S] ==
IF s = {} THEN base
ELSE LET x == choose(s)
IN op(f(x), iter[s \ {x}])
IN iter[S]
FoldSet(op(_,_), base, set) ==
MapThenFoldSet(op, base, LAMBDA x : x, LAMBDA s : CHOOSE x \in s : TRUE, set)
Reverse(seq) ==
[ i \in 1..Len(seq) |-> seq[(Len(seq) - i) + 1] ]
ToSet(s) ==
{ s[i] : i \in DOMAIN s }
\* end tla community modules
VARIABLES foo, SmachineState, SmachineVisited
Events == {"A", "B", "C", "D", "E", "F", "G", "H"}
\* Use this definition for a failure case, s12 has no transitions to i
\* SmachineParents == [s |-> "", s1 |-> "s", s2 |-> "s", s11 |-> "s1", s12 |-> "s1", s21 |-> "s2", s211 |-> "s21"]
\* This is the passing case
SmachineParents == [s |-> "", s1 |-> "s", s2 |-> "s", s11 |-> "s1", s21 |-> "s2", s211 |-> "s21"]
\* Assumption that initial transition has no conditionals
\* We can transition to a state that is not a leaf, state but there always must be a path to a leaf state
\* This works
\*SmachineInit == [s |-> "s1", s1 |-> "s11", s2 |-> "s21", s11 |-> "", s21 |-> "s211", s211 |-> ""]
SmachineInit == [s |-> "s2", s1 |-> "s11", s2 |-> "s21", s11 |-> "", s12 |-> "", s21 |-> "s211", s211 |-> ""]
\* Enter and exit actions never look at current event
\* Given a state return a sequence of states to the root, ordered.
RootPath(state,parents) == LET
path == <<>>
RECURSIVE Helper(_, _)
Helper(state_,path_) == IF parents[state_] = "" THEN Append(path_,state_) ELSE
Helper(parents[state_], Append(path_,state_))
IN Helper(state,path)
\* Given a state, return the set of states to the root, not ordered
Root(state,parents) == LET
path == {}
RECURSIVE Helper(_, _)
Helper(state_,path_) == IF parents[state_] = "" THEN path_ \union {state_} ELSE
Helper(parents[state_], path_ \union {state_})
IN Helper(state,path)
\* Lca - Lowest common ancestor of two states, used for transition path
Lca(state1,state2,parents) == LET
path1 == Root(state1,parents)
path2 == RootPath(state2,parents)
RECURSIVE Helper(_, _)
Helper(path1_,path2_) == IF Head(path2_) \in path1_ THEN Head(path2_) ELSE
Helper(path1_, Tail(path2_))
IN
Helper(path1,path2)
\* This create initial path to a leaf state, this example SmachineInit is passed in
InitPath(state,init) == LET
enterpath == <<>>
RECURSIVE Helper(_,_,_)
Helper(enterpath_,init_,start_) ==
IF init[start_] = "" THEN enterpath_ ELSE Helper(Append(enterpath_, init_[start_]),init_,init_[start_])
IN
Helper(enterpath,init,state)
\* In this example Op is SmachineTransition that defines the next state, depending on current state and event
\* To transition from one state to another the following is required
\*
\* FindNext looks up the path to root to find a transition to a next state
FindNext(state,event,parents,Op(_,_)) == LET
rootpath == RootPath(state,parents)
RECURSIVE Helper(_)
Helper(rootpath_) == IF Op(Head(rootpath_),event) = "super" THEN
Helper(Tail(rootpath_)) ELSE Op(Head(rootpath_),event)
IN
Helper(rootpath)
\* Find next can return a next "none" as this means this state and none of it's parents handle the event
\* Check that returned state is an actual state
Transition(state,event,parents,Op(_,_)) == LET
nextstate == FindNext(state,event,parents,Op)
IN
IF nextstate \in DOMAIN parents THEN nextstate ELSE "none"
ExitPath(start,event,parents,NextState(_,_)) == LET
end == Transition(start,event,parents,NextState)
lca == Lca(start,end,parents)
rootpath == RootPath(start,parents)
exitpath == <<>>
RECURSIVE Helper(_,_,_)
Helper(lca_,rootpath_,exitpath_) == IF Head(rootpath_) = lca THEN exitpath_ ELSE
Helper(lca_,Tail(rootpath_), Append(exitpath_,Head(rootpath_)))
IN
IF end = "none" THEN <<start>> ELSE Helper(lca,rootpath,exitpath)
\* Enter path is more complicated because the initial transitions need to added on, transitions to non-leaf state are allowed as long as initial transtions
\* path ends up in a leaf state, assumption is there are no conditional in the initial path
EnterPath(start,event,parents,NextState(_,_),init) == LET
enterpath == <<>>
end == Transition(start,event,parents,NextState)
lca == Lca(start,end,parents)
rootpath == RootPath(end,parents)
RECURSIVE Helper(_,_,_)
Helper(lca_,rootpath_,enterpath_) == IF Head(rootpath_) = lca THEN enterpath_ ELSE
Helper(lca_,Tail(rootpath_), Append(enterpath_,Head(rootpath_)))
RECURSIVE HelperInit(_,_,_)
HelperInit(enterpath_,init_,end_) == IF init[end_] = "" THEN enterpath_ ELSE HelperInit(Append(enterpath_, init_[end_]),init_,init_[end_])
IN
IF end = "none" THEN <<start>> ELSE HelperInit(Reverse(Helper(lca,rootpath,enterpath)),init,end)
\*Helper(lca,rootpath,enterpath)
\* The finish state is determined by taking the last state in the enter path, which includes initial transitions,
\* Need special case for self transition
FinishState(start,enterpath) == LET
\* Example S211 and B involves no enters - self transition
reverseEnter == Reverse(enterpath)
IN
IF reverseEnter = <<>> THEN start ELSE Head(reverseEnter)
\* -- Find all leaf states
\* Helfper for Leaf States
LeafFilter(set,member) == LET
find == {x \in set: member \subseteq x }
IN
Cardinality(find)
LeafStates(parents) == LET
allRootPaths == {Root(x,parents): x \in (DOMAIN parents)}
uniqueRootPaths == {x \in allRootPaths: LeafFilter(allRootPaths,x) = 1}
diff == allRootPaths \ uniqueRootPaths
IN
(UNION uniqueRootPaths) \ (UNION diff)
SmachineVars == <<foo, SmachineState, SmachineVisited>>
SmachineVarsWF == <<foo, SmachineVisited>>
\* End of generic statement
\* Smachine statements
SmachineExit(state,foo_) ==
CASE state = "s211"
-> 4
[] state = "s1"
-> 4
[] OTHER -> foo_
RunSmachineExits(path,statevar) == LET
RECURSIVE Helper(_,_)
Helper(path_,statevar_) == IF path_ = <<>> THEN statevar_ ELSE Helper(Tail(path_),SmachineExit(Head(path_),statevar_))
IN
Helper(path,statevar)
SmachineEnter(state,foo_) ==
CASE state = "s211"
-> 1
[] state = "s1"
-> 0
[] OTHER -> foo_
RunSmachineEnters(path,statevar) == LET
RECURSIVE Helper(_,_)
Helper(path_,statevar_) == IF path_ = <<>> THEN statevar_ ELSE Helper(Tail(path_),SmachineEnter(Head(path_),statevar_))
IN
Helper(path,statevar)
\* Unlike the actual code that executes this machine, transitions and state updates statements are defined separately
\* This provides the next state and does not update the state variables
SmachineTransition(state,event) ==
CASE (state = "s") /\ (event = "E") -> "s11"
[] (state = "s1") /\ (event = "C") -> "s2"
[] (state = "s1") /\ (event = "F") -> "s211"
[] (state = "s1") /\ (event = "A") -> "s1"
[] (state = "s1") /\ (event = "B") -> "s11"
[] (state = "s1") /\ (event = "D") -> "s"
[] (state = "s11") /\ (event = "G") -> "s211"
[] (state = "s11") /\ (event = "H") -> "s"
[] (state = "s11") /\ (event = "D") -> "s1"
[] (state = "s2") /\ (event = "F") -> "s11"
[] (state = "s2") /\ (event = "C") -> "s1"
[] (state = "s21") /\ (event = "A") -> "s21"
[] (state = "s21") /\ (event = "C") -> "s1"
[] (state = "s21") /\ (event = "B") -> "s211"
[] (state = "s211") /\ (event = "D") -> "s21"
[] (state = "s211") /\ (event = "H") -> "s"
[] (state = "s") -> "done" \* need this to end recursion in FindNext statement
[] OTHER -> "super" \* need this to enable recusion in FindNext statement
SmachineFinish(state,event,foo_) ==
CASE (state = "s") /\ (event = "I")
-> 0
[] (state = "s1") /\ (event = "D")
-> 1
[] (state = "s11") /\ (event = "D") \*/\ (foo = 1)
-> 1
[] (state = "s11") /\ (event = "D") \* /\ (foo = 1)
-> 1
[] (state = "s2") /\ (event = "I") \*/\ (foo = 0)
-> 1
[] OTHER -> foo_
\* Make state variable updates before leavng state, then make state variable update along exit and enter path
SmachineUpdate(state,event,statevar,exitpath,enterpath) == LET
SmachineStateVarFinish == SmachineFinish(state,event,statevar) \* State variable before exiting
SmachineStateVarExit == RunSmachineExits(exitpath,SmachineStateVarFinish)
IN
RunSmachineEnters(enterpath, SmachineStateVarExit) \* State variable after exit)
SmachineLeafs == LeafStates(SmachineParents)
SmachineAllStates == DOMAIN SmachineParents \ {"s"}
firstPath == InitPath("s",SmachineInit)
initState == Head(Reverse(firstPath))
Init ==
/\ SmachineState = initState
/\ foo = 0\*RunSmachineEnters(firstPath,0)
/\ SmachineVisited = {}
Next ==
/\ \E evt \in Events:
LET
exitPath == ExitPath(SmachineState, evt, SmachineParents, SmachineTransition)
enterPath == EnterPath(SmachineState, evt, SmachineParents, SmachineTransition, SmachineInit)
IN
/\ SmachineVisited' = ToSet(enterPath) \union SmachineVisited
/\ SmachineState' = FinishState(SmachineState,enterPath)
/\ foo' = SmachineUpdate(SmachineState,evt,foo,exitPath,enterPath)
Spec == Init /\ [][Next]_SmachineVars /\ WF_SmachineVarsWF(Next)
EnterCheck == <>(foo = 1) \* This passes
\*EnterCheck == <>(foo = 4) \* This fails
EventuallyVisited == <>(SmachineAllStates \subseteq SmachineVisited)
AlwaysInLeaf == (SmachineState \in SmachineLeafs) = TRUE