Re: [tlaplus] Problem with liveness properties in TLC

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

W dniu wtorek, 31 grudnia 2019 09:05:32 UTC+1 użytkownik Stephan Merz napisał:

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

On 30 Dec 2019, at 10:24, mrynd...@xxxxxxxxx wrote:

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:
<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 tla...@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>