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

[mlj...@gmail.com]

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

[Leslie Lamport]

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

[mlj...@gmail.com]

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

[Leslie Lamport]

TLA+ does not provide Until or the dozens of other such temporal
operators that have been proposed because they aren't needed.  Those
dozens of operators were introduced to ordinary linear-time temporal
logic because the simple [] (always) operator isn't expressive enough
to specify systems if the atomic formulas are state predicates.  The
resulting temporal logics were incapable of writing understandable
specs of anything but the most trivial of systems.  TLA's introduction
of action formulas as the atomic formulas made it possible to write
understandable specs of complicated systems using only [], and made
all those other operators useless.

Incidentally, in your example, (a=0) Until (b=1) is obviously implied
by (a=0) /\ [](b#1 => a=0), which TLC can check is satisfied by your spec
(when the typo  A /\ B  is corrected to A \/ B).

I'll let you figure out for yourself why checking that a spec
satisfies a formula containing the \EE operator is a computationally
very difficult problem.

Leslie

[mlj...@gmail.com]

Hi Leslie,

I think the answer is as follow.

According to the example in your book, that \EE x : [](x \in y), to evaluate the formula,

TLC has to check all the possible values of x in each state of a trace of the behavior.

The trace could be infinite, and the behavior of a system is the composition of all the

possible traces which is also infinite. Thus, it is very difficult to compute it. Moreover,

TLA+ is untyped, so the possible values of x could be any value in the universe.

Am I close to it?

Best Regards,

Changjian

[Hillel Wayne]

\Next should be representable as

[][b = 0 => b' = 1]_<<a, b>>

Which accounts for stuttering: either b = 0 \Next b = 1 OR you stutter.

\Until should be representable using the open-system operator:

b /= 1 -+-> a = 0

a is zero at least one step longer than b isn't 1. Unfortunately, -+-> is currently unimplemented in TLC and TLAPS.