-------------------------------- MODULE smachine --------------------------------
EXTENDS TLC, Sequences \* For @@
VARIABLE state, visited
States == {
"s",
"s1", "s2",
"s11", "s21", "s211"
}
Events == {"A", "B", "C", "D", "E", "F", "G", "H"}
TopDown == [s |-> {"s1", "s2", "Reports"},
s1 |-> {"s11"}, s2 |-> {"s21"}, s21 |-> {"s211"}] @@ [s \in States |-> {}]
Init ==
/\ state = "s11"
/\ visited = {}
vars == <<state, visited>>
Next ==
/\ \E evt \in Events:
\/ state = "s11" /\ evt = "G"
/\ visited' = {state} \union visited
/\ state' = "s211"
\/ state = "s211" /\ evt = "B"
/\ visited' = {state} \union visited
/\ state' = "s11"
all == {"s11","s211"}
EventuallyVisited == <>(visited = all)
Spec == Init /\ [][Next]_vars /\ WF_vars(Next)
AlwaysInLeaf == TopDown[state] = {}