As you observe, since (for very good reasons) any TLA+ formula is
invariant under stuttering--that is, insensitive to adding or removing
a finite number of stuttering steps--it is impossible to define the
usual linear-time temporal logic Next operator. For example, the
value of Next x=0 can be changed by adding a single stuttering step.
There are at least two linear-time temporal operators commonly called
"Until". If P and Q are state predicates, then here is a way to
write one common meaning of P Until Q:
\EE r : /\ r = Q
/\ [ \/ /\ r \/ Q
/\ r' = TRUE
\/ /\ ~Q /\ P
/\ r' = r
]_<<r, P, Q>>
I believe that it's possible to generalize this to arbitrary temporal
formulas P and Q (that are invariant under stuttering) only with a
formula that depends on the variables that occur in P and Q. However,
all this is of little interest because (1) TLC cannot handle a formula
containing the temporal existential quantifier \EE and (2) when you
get used to the TLA+ paradigm of thinking in terms of state machines
(with fairness conditions), you will have no desire to use an Until
operator.
Leslie
Enter code here...
Hi guys,
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.
Best Regards,
Changjian Zhang