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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Thu, 22 Feb 2018 13:14:48 -0800 (PST)*References*: <c3bc5e44-2ef5-4b4b-8955-9973ee7a45f0@googlegroups.com>

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.

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

- Prev by Date:
**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:
**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):