# [tlaplus] Problem with liveness properties in TLC

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.

--
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.