Hi Ryan,
Could you please share your .cfg file or a screenshot of your toolbox setup? It's passing for me.
H
I'm trying to adapt one of Hilel Waynes' examples of a hierachical fine state machines.--
My liveness property fails in stuttering.
I want to show that eventually all states are visited
Not sure what I'm missing, any help appreciated
---------------------------------- 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] = {}
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4bffd6a6-3cf5-4efc-8827-8e443301f290n%40googlegroups.com.