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

*From*: mlj...@xxxxxxxxx*Date*: Fri, 23 Feb 2018 07:54:15 -0800 (PST)*References*: <c3bc5e44-2ef5-4b4b-8955-9973ee7a45f0@googlegroups.com> <ea122e60-7107-438f-9431-93151d205b3a@googlegroups.com> <5f539176-aba8-47b3-8794-7b5108a8b031@googlegroups.com> <eeba4d99-733a-4794-984a-579546bc7369@googlegroups.com>

Hi Leslie,

On Friday, February 23, 2018 at 1:11:27 AM UTC-5, Leslie Lamport wrote:

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

On Friday, February 23, 2018 at 1:11:27 AM UTC-5, Leslie Lamport wrote:

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

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

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

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

- Prev by Date:
**Re: How can I express Next and Until operator in TLA+?** - Next by Date:
**Multi-threaded TLC Simulation Mode** - 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):