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

*From*: mlj...@xxxxxxxxx*Date*: Thu, 22 Feb 2018 19:53:02 -0800 (PST)*References*: <c3bc5e44-2ef5-4b4b-8955-9973ee7a45f0@googlegroups.com> <ea122e60-7107-438f-9431-93151d205b3a@googlegroups.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

On Thursday, February 22, 2018 at 4:14:48 PM UTC-5, Leslie Lamport wrote:

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:*Leslie Lamport

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

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