[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
How can I express Next and Until operator in TLA+?
Enter code here...
I'm currently learning TLA+ and I met a problem that how can I express Next and Until operators of LTL in TLA+.
Suppose the follow spec
VARIABLES a, b
Init == a = 0 /\ b = 0
A == b = 1 /\ a' = 1 /\ UNCHANGED b
B == b = 0 /\ b' = 1 /\ UNCHANGED a
Spec == Init /\ [A /\ B]_<<a, b>>
For the above spec, how can I assert that
1. a = 0 \Until b = 1
2. b = 0 \Next b = 1
PS: Since TLA+ allows stuttering steps, so \Next operator does not provide much meaning. The second formula should always be false due to the stuttering steps.