Hi Leslie,
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.
Best,
Changjian
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
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