hierarchical finite state machine - liveness

[Ryan Dumouchel]

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] = {}

         

[Hillel Wayne]

Hi Ryan,

Could you please share your .cfg file or a screenshot of your toolbox setup? It's passing for me.

H

--
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4bffd6a6-3cf5-4efc-8827-8e443301f290n%40googlegroups.com.

[Ryan Dumouchel]

Hi Hillel, does this work

[Hillel Wayne]

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

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/57408a6b-b061-4029-a313-30d42c2ff814n%40googlegroups.com.

[Ryan Dumouchel]

Thank you Hillel

It worked.   Your Hfsm example finally made TLA click for me.