Re: [tlaplus] hierarchical finite state machine

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.

Re: [tlaplus] hierarchical finite state machine - liveness