Hi Ryan
The problem is you have "What is the behavior spec" set to "initial predicate and next state relation", which doesn't use fairness. Change it to "temporal formula" and set the formula to "Spec" and it should work.
H
On 10/3/2023 10:34 PM, Ryan Dumouchel wrote:
Hi Hillel, does this work
--On Tuesday, October 3, 2023 at 11:20:30 PM UTC-4 Hillel Wayne wrote:
Hi Ryan,
Could you please share your .cfg file or a screenshot of your toolbox setup? It's passing for me.
H
On 10/3/2023 9:52 PM, Ryan Dumouchel wrote:
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+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4bffd6a6-3cf5-4efc-8827-8e443301f290n%40googlegroups.com.
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+u...@xxxxxxxxxxxxxxxx.To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/57408a6b-b061-4029-a313-30d42c2ff814n%40googlegroups.com.