[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] hierarchical finite state machine - liveness



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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/57408a6b-b061-4029-a313-30d42c2ff814n%40googlegroups.com.

Attachment: Screen Shot 2023-10-03 at 11.30.46 PM (2).png
Description: PNG image