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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Thu, 22 Feb 2018 22:11:26 -0800 (PST)*References*: <c3bc5e44-2ef5-4b4b-8955-9973ee7a45f0@googlegroups.com> <ea122e60-7107-438f-9431-93151d205b3a@googlegroups.com> <5f539176-aba8-47b3-8794-7b5108a8b031@googlegroups.com>

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.

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).

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.

satisfies a formula containing the \EE operator is a computationally

very difficult problem.

Leslie

On Thursday, February 22, 2018 at 7:53:02 PM UTC-8, m....@xxxxxxxxx wrote:

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 providethe 'Util' operator, at least in grammar level. For example, TLA+ allows using the Util operator, although TLCmay not be able to check it. Still, I wonder why TLC cannot support checking the Until operator and also thetemporal 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.Leslieat 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 specVARIABLES 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 that1. a = 0 \Until b = 12. b = 0 \Next b = 1PS: 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

**Follow-Ups**:**Re: How can I express Next and Until operator in TLA+?***From:*mlj . . .

**References**:**How can I express Next and Until operator in TLA+?***From:*mlj . . .

**Re: How can I express Next and Until operator in TLA+?***From:*Leslie Lamport

**Re: How can I express Next and Until operator in TLA+?***From:*mlj . . .

- Prev by Date:
**Re: How can I express Next and Until operator in TLA+?** - Next by Date:
**Re: How can I express Next and Until operator in TLA+?** - Previous by thread:
**Re: How can I express Next and Until operator in TLA+?** - Next by thread:
**Re: How can I express Next and Until operator in TLA+?** - Index(es):