[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: How can I express Next and Until operator in TLA+?



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

at 8:08:55 PM UTC-8, m....@xxxxxxxxx wrote:
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