Problem with liveness properties in TLC

[mrynd...@gmail.com]

I have this simple spec describing a sequence of state machine constantly toggling between two states with different periods:

CONSTANT BC

VARIABLES bState

ASSUME /\ BC \in Seq(Nat)

vars == bState

States == {"Active_Off", "Active_On"}

Blinker == [timer : Nat, state : States]

TypeOK == /\ bState \in [DOMAIN BC -> Blinker]

Init ==

    /\ bState = [n \in DOMAIN BC |-> [timer |-> BC[n],

                                      state |-> "Active_Off"]

                ]

                                

Transition(n) == /\ bState[n].timer = 0

                 /\ bState[n].state = "Active_Off"

                 /\ bState' = [bState EXCEPT ![n].timer = BC[n],

                                             ![n].state = "Active_On"]

              \/

                 /\ bState[n].timer = 0

                 /\ bState[n].state = "Active_On"

                 /\ bState' = [bState EXCEPT ![n].timer = BC[n],

                                             ![n].state = "Active_Off"]

             

Tick == /\ \A n \in DOMAIN BC : bState[n].timer > 0

        /\ bState' = [n \in DOMAIN BC |-> [timer |-> bState[n].timer - 1,

                                           state |-> bState[n].state]]

Next == Tick \/ \E n \in DOMAIN BC : Transition(n)

Spec == Init /\ [][Next]_vars

FairSpec == Spec /\ WF_vars(Next)

With BC <- <<3>> this gives me a simple state graph:

Now I'm trying to add some liveness properties. This one fails immediately in <Intial predicate>:

AlwaysTick == []<><<Tick>>_bState

as well as this one:

AlwaysTick == []<><<Next>>_bState

Could someone explain why this happens?

Help is greatly appreciated.

[Stephan Merz]

Hello,

are you sure that you changed the default `Spec' to `FairSpec' in "What is the behavior spec?" in the Model Overview tab? The TLC output seems to indicate that no fairness condition is taken into account.

Best,

Stephan

<out.png>

Now I'm trying to add some liveness properties. This one fails immediately in <Intial predicate>:

AlwaysTick == []<><<Tick>>_bState

as well as this one:

AlwaysTick == []<><<Next>>_bState

Could someone explain why this happens?

Help is greatly appreciated.

--
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/b8246fe3-693d-4e49-9315-6946de773bb2%40googlegroups.com.
<out.png>

[mrynd...@gmail.com]

Oh, yes, you are right. Sometimes still things like this slip my mind. Thank you!

Stephan

To unsubscribe from this group and stop receiving emails from it, send an email to tla...@googlegroups.com.