Re: [tlaplus] Problem with liveness properties in TLC

Stephan

On 30 Dec 2019, at 10:24, mryndzionek@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 tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/b8246fe3-693d-4e49-9315-6946de773bb2%40googlegroups.com.
<out.png>