[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: How can I express Next and Until operator in TLA+?
Thank you for your reply.
I think I understand how the _expression_ works. However, I am still confused about why not TLA+ just provide
the 'Util' operator, at least in grammar level. For example, TLA+ allows using the Util operator, although TLC
may not be able to check it. Still, I wonder why TLC cannot support checking the Until operator and also the
temporal existential quantifier.
On Thursday, February 22, 2018 at 4:14:48 PM UTC-5, Leslie Lamport wrote:
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
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.