Nondeterminism and equivalence

[Ron Pressler]

My question concerns the more theoretical aspects of TLA.

Consider the following three specifications, assuming we have `VARIABLES t, x` (for simplicity of notation, I’ll drop the stuttering invariant actions):

    x = 1 ∧ t = 1 ∧ ☐(t’ = t + 1 ∧ x’ = x + 1)

    x ∈ Nat ∧ t = 1 ∧ ☐(t’ = t + 1 ∧ x’ = x + 1 ∧ t = 100 ⇒ x = 100)

    x = 1 ∧ t = 1 ∧ ☐(t’ = t + 1 ∧ ((t < 100 ∧ x’ = x - 1) ∨ x’ = x + 1) ∧ t = 100 ⇒ x = 100)

Each of these specifications admits exactly the same set of behaviors (which happens to contain just a single one). By taking the formulas apart we can see that the second is different from the first by looking at the initial condition, and we can see that the third is different from the first by examining their next-state relations. But can we tell them apart without breaking the formulas open (perhaps by conjuncting them with another formula)? Are they equivalent?

If they are, are the algorithms they describe “really” equivalent? Obviously, for the sake of abstraction-refinement relations, it makes sense to ignore internal nondeterminism, but on the other hand, we know that an algorithm that employs nondeterminism can have significantly different complexity than one that does not, so shouldn’t there be a way to tell them apart?

Ron

[Ioannis Filippidis]

Hi Ron,

If these three formulae describe the same collection of behaviors

(this seems to me to be the case, so will assume that it is for the comments below),

then, semantically, there is no difference between them.

The meaning of a temporal formula is defined on p.315 of [1].

For each behavior `sigma` and each formula `F`, the semantics defines whether

the behavior satisfies the formula or not (in some cases we may be unable to

decide this. For example, if it depends on values unspecified by the

axioms of TLA+ (Sec.6.2, p.67 and pp.71--72 [1])).

Syntactically, the formulae are different. They are different sequences of symbols,

but this is irrelevant to what behaviors satisfy them.

If we split a formula into pieces, then it is no longer a single formula.

We create multiple new formulae, for example:

Init == x = 1 ∧ t = 1

Changes == ☐(t’ = t + 1 ∧ x’ = x + 1)

Each of these formulae describes a separate collection of behaviors,

(interpreting them separately).

If we conjoin them:

F1 == x = 1 ∧ t = 1 ∧ ☐(t’ = t + 1 ∧ x’ = x + 1)

then we create a new formula (F1), and interpret that formula

separately. Due to how the semantics is defined for temporal formulae,

and the initial condition (again, ignoring that `Changes` is not a TLA+ formula),

it so happens that a behavior satisfies the formula `F1` if, and only if,

it satisfies the formula `Init` and it satisfies the formula `Changes`.

A behavior is a sequence of states, informally: sigma[0], sigma[1], ..., where:

\A n \in Nat:  IsAState(sigma[n])  (see p.313, and p.316).

If the first state of a behavior assigns the value 1 to variable "x" and the value 1 to variable "t":

(sigma[0]["x"] = 1)  /\  (sigma[1]["t"] = 1),

then the behavior `sigma` satisfies the formula `Init`.

If each step in a behavior satisfies the action:

(t’ = t + 1 ∧ x’ = x + 1),

then the behavior satisfies the formula `Changes`.

This requirement can be written as (again, ignoring that `Changes` is *not* a TLA+ formula):

\A n \in Nat:  << sigma[n], sigma[n + 1] >>[[ "(t’ = t + 1 ∧ x’ = x + 1)" ]]

\equiv  (* From the semantics of actions and state predicates defined in Sec.16.2 [1],

               assuming that x, t have been declared as variables. *)

\A n \in Nat:  /\ sigma[n + 1]["t"] [[=]] [[1]] [[+]] sigma[n]["t"]

                     /\ sigma[n + 1]["x"] [[=]] [[1]] [[+]] sigma[n]["x"]

where [[=]] and [[+]] denote the interpretation of equality and addition within ZF (see p.292 [1]),

and [[1]] is the interpretation of the constant expression "1".

So, a behavior that starts with x |-> 5, t |-> 6 could satisfy `Changes`,

but does not satisfy `Init`. When we interpret the formula `F1`,

it turns out that such a behavior does not satisfy `F1`.

A behavior that starts with x |-> 1, t |-> 1, and at the second state

x |-> 10, t |-> 1, satisfies `Init`, but not `Changes`, nor `F1`.

Note that this behavior doesn't "start" at a state with x |-> 1, t |-> 1,

and later "finds out" that it violated `Changes`. It simply satisfies or

not entire temporal formulae.

So, the "algorithms" that `F1`, F2`, and `F3` describe (understood as the collections of behaviors, see [2, 3])

are the same. Also, "nondeterminism" has been given many meanings in

the literature. What happens here is that a formula can describe more than one behaviors.

For example, `Init` describes several behaviors. `F1`, too, describes several behaviors,

not just one, for reasons described below.

The "algorithms" that `Init` and `Changes` describe are different.

Without splitting the formula `F1`, it is "equivalent" to:

F2 == x ∈ Nat ∧ t = 1 ∧ ☐(t’ = t + 1 ∧ x’ = x + 1 ∧ t = 100 ⇒ x = 100)

provided that as "equivalent" we define two formulae that describe the same collection of behaviors.

Had we agreed that "equivalent" would mean something else,

for example, something about the sequence of symbols of `F1`, compared to

the sequence of symbols of `F2`, then, yes, they wouldn't be "equivalent",

because `F1` and `F2` are different sequences of symbols.

But that is a syntactic viewpoint, not a semantic one.

A notion that involves similar observations is machine closure

(Sec.8.9.2, p.111 [1], Sec.3.4.2 [5]). The main question involved in determining

machine closure of two properties (described by two separate formulae),

a safety and a liveness property, is whether the liveness property

imposes any "safety constraint" on behaviors that satisfy the safety property.

See also Sec.8.9.3, especially paragraph 1 on p.114 [1].

Also, each of the three formulae describes a collection that contains infinitely many

behaviors (in TLA+, keeping in mind that these formulae are LTL-like).

The first formula:

F1 == x = 1 ∧ t = 1 ∧ ☐(t’ = t + 1 ∧ x’ = x + 1)

is satisfied by a behavior that starts with:

x |-> 1, t |-> 1 and increments them to x |-> 2, t |-> 2, etc.

(Assuming that, for arguments that are natural numbers, the operator "+" is defined as usual.)

F1 is satisfied by any behavior that assigns values to the variables x, t as above,

and assigns arbitrary values to all other variables (Sec.2.3, p.18 [1]). There are infinitely many values (sets) that

a behavior can assign to a variable, so there are infinitely many behaviors that

satisfy the formula F1. Moreover, this collection of behaviors is not a set (at the semantic level, in ZF),

because it contains "too many" behaviors (Sec.6.1, pp.65-66 [1], see also p.311).

(The collection of behaviors described by `F1` is a (proper) class [4].)

[1] http://research.microsoft.com/en-us/um/people/lamport/tla/book-02-08-08.pdf

[2] http://research.microsoft.com/en-us/um/people/lamport/pubs/pubs.html#state-machine

[3] http://research.microsoft.com/en-us/um/people/lamport/pubs/pubs.html#deroever-festschrift

[4] https://en.wikipedia.org/wiki/Class_(set_theory)

[5] http://research.microsoft.com/en-us/um/people/lamport/pubs/pubs.html#abadi-conjoining

ioannis

[Stephan Merz]

Hi Ron,

your claim that all of the three specifications admit the same single behavior is true only because you ignore stuttering. The TLA+ specification

x ∈ Nat ∧ t = 1 ∧ ☐[t’ = t + 1 ∧ x’ = x + 1 ∧ t = 100 ⇒ x = 100]_<<x,t>>

has behaviors where x initially holds an arbitrary natural number, and t and x get incremented until t hits 100, at which point only stuttering is possible. So it cannot be equivalent to the TLA+ specification

    x = 1 ∧ t = 1 ∧ ☐[t’ = t + 1 ∧ x’ = x + 1]_<<t,x>>

A similar observation holds for (the TLA+ version of) the third specification

    x = 1 ∧ t = 1 ∧ ☐[t’ = t + 1 ∧ ((t < 100 ∧ x’ = x - 1) ∨ x’ = x + 1) ∧ (t = 100 ⇒ x = 100)]_<<x,t>>

You can force the equivalence of the specifications by adding the conjunct

    ⬦(t > 100)

and this observation shows that liveness conditions may sometimes constrain the safety part of the specifications. Such specifications are known as "not machine-closed" [1], and are hard to reason about. (You'd have to prove the invariant ☐(x=t), but this requires temporal logic reasoning since you must appeal to the liveness condition to show that the execution would be blocked when t hits 100.)

The standard form of TLA+ specifications where liveness conditions are conjunctions of (weak or strong) fairness conditions on sub-actions of the specification (essentially, disjuncts of the next-state relation) ensures that specifications are machine closed, and all safety properties can be proved just from the initial condition and the next-state relation.

Best regards,

Stephan

[1] M. Abadi, L. Lamport. The existence of refinement mappings. TCS 81(2), 1991. See also section 8.9.2 of Specifying Systems.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

[Ron Pressler]

Hi Ioannis.
As to the single-behavior vs. infinite behaviors, of course you are right. That was a silly mistake on my part. You are also correct about them not being a set in axiomatic set theory.

But as to the rest, I understand the semantic equivalence, but my point is that the equivalence is extensional (with respect to behaviors), and there may be cases where a more intensional equivalence would be desired (with respect to the algorithm's internal nondeterminism). This more intensional equivalence need not necessarily be entirely syntactic.

Ron

[Ron Pressler]

On Saturday, November 19, 2016 at 10:23:02 AM UTC+2, Stephan Merz wrote:

your claim that all of the three specifications admit the same single behavior is true only because you ignore stuttering...

Oh! Of course!

 

You can force the equivalence of the specifications by adding the conjunct

    ⬦(t > 100)

and this observation shows that liveness conditions may sometimes constrain the safety part of the specifications. Such specifications are known as "not machine-closed" [1], and are hard to reason about. (You'd have to prove the invariant ☐(x=t), but this requires temporal logic reasoning since you must appeal to the liveness condition to show that the execution would be blocked when t hits 100.)

Ah, so does machine closure in addition to stuttering invariance place constraints on internal nondeterminism? My cursory reading of machine closure made me believe that in order for it to be violated, the liveness requirement would need to explicitly contain "safety subformulas", but I guess this is an example where this is not the case.
 

The standard form of TLA+ specifications where liveness conditions are conjunctions of (weak or strong) fairness conditions on sub-actions of the specification (essentially, disjuncts of the next-state relation) ensures that specifications are machine closed, and all safety properties can be proved just from the initial condition and the next-state relation.

Does that guarantee, then, that formulas with different nondeterminism would admit different behaviors and could be distinguished?

Ron

[Stephan Merz]

Ah, so does machine closure in addition to stuttering invariance place constraints on internal nondeterminism? My cursory reading of machine closure made me believe that in order for it to be violated, the liveness requirement would need to explicitly contain "safety subformulas", but I guess this is an example where this is not the case.

Not sure I understand your question but allow me to reformulate. The liveness requirement filters out behaviors that would be perfectly acceptable for the safety part of the specification. The idea of machine closure is that the state machine executing the safety part of the specification does not need "prescience" in order to make those choices that will be compatible with the liveness condition: any choice allowed by the next-state relation can be completed to an infinite behavior satisfying the overall specification, using a fair scheduler. A machine-closed specification does not place any constraints on internal non-determinism, whereas non machine-closed specifications may have such constraints.

The standard form of TLA+ specifications where liveness conditions are conjunctions of (weak or strong) fairness conditions on sub-actions of the specification (essentially, disjuncts of the next-state relation) ensures that specifications are machine closed, and all safety properties can be proved just from the initial condition and the next-state relation.

Does that guarantee, then, that formulas with different nondeterminism would admit different behaviors and could be distinguished?

Morally, yes, assuming that the different choices are actually possible based on the safety part (think invariants). For example, the following (trivially machine-closed) variation of your example

    x = 1 ∧ t = 1 ∧ ☐[t’ = t + 1 ∧ ((x < 0 ∧ x'=x-1) ∨ x’ = x + 1)]_<<t,x>>

allows for an apparent choice of decrementing x that cannot be realized due to the invariant ☐(x > 0).

Stephan

[Ron Pressler]

On Saturday, November 19, 2016 at 11:00:30 AM UTC+2, Stephan Merz wrote:

 

 The idea of machine closure is that the state machine executing the safety part of the specification does not need "prescience" in order to make those choices that will be compatible with the liveness condition: any choice allowed by the next-state relation can be completed to an infinite behavior satisfying the overall specification, using a fair scheduler.

OK! So now I understand the importance of machine closure much better (and should probably go back and read about it more carefully), and I guess this is one more reason for the importance of stuttering invariance. Anyway, this precisely addresses my question. If algorithms that are not machine-closed are discarded as "invalid", they do not muddle the equivalence. The only problem is (I think) that such formulas cannot themselves be detected within the logic, correct?

Thanks!

[Stephan Merz]

The only problem is (I think) that such formulas cannot themselves be detected within the logic, correct?

Correct. The restriction to (countable) conjunctions of fairness conditions on sub-actions is just a sufficient condition.

Stephan

[Leslie Lamport]

Hi Ron,

 

I have two comments.

 

First, the main reason that specifications that aren't machine closed

are usually bad has nothing to do with provability.  It's because they

are usually hard to understand.  Moreover, if they are supposed to

describe an algorithm, they are almost certainly wrong.  There are

rare cases in which a non-machine closed spec is the best way to

describe what a system is supposed to do (rather than how it does it).

The simplest spec I know of sequential consistency is not machine

closed.

 

Second, you seem to forget that a TLA+ specification is a mathematical

formula.  Mathematics cannot express anything about the syntax in

which a mathematical formula is written.  You can model a language

like TLA+ in TLA+ and make all sorts of statements about the TLA+

formulas--for example that the meaning of a certain sequence seq of

characters is the formula F, and that seq is the shortest sequence of

characters whose meeaning is F.  However, that's a statement about a

sequences of characters, not about a mathematical formula.

 

Thus, if Wiles's proof is correct, then the following two formulas A

and B are completely equivalent

 

   A  ==  q = 42

 

   B  ==

     (\A x, y, z, n \in Nat \ {0} : (n>2) => (x^n + y^n # z^n))

        => (q = 42)

 

Thus, P(A) = P(B) for any mathematical (or TLA+) operator P. A tool

like TLC may be able to evaluate one and not the other, but that's because

tools operate on strings of characters representing formulas, not on

formulas.  The correctness condition that TLC is supposed to satisfy

is that if it can evaluate both P(A) and P(B), then it gets the same

value for both .  Mathematics gives no meaning to the concept of evaluation

of a formula.

 

If you want to distinguish between two TLA+ formulas that are

mathematically equivalent (which I believe is what you mean by

equivalent with respect to behaviors), then you're looking for a tool

not for a logic.  We already have one such tool: the TLATeX

pretty-printer.  Also, a lot of the output that TLC produces depends

on the particular way a specification is written--even if TLC

produces the same yes or no answer of whether the spec satisfies the

properties that TLC is checking.  Perhaps there are others tools that

can tell us something useful about a specification that depends on how

it's written.

 

Leslie

 

 

 

 

[Ron Pressler]

Let me clarify that my question had absolutely nothing to do with the practice of specification in TLA+, but merely with the philosophical value of TLA’s notion of algorithm equivalence, and was thus purely theoretical. My original thought was that in some cases, trace-equivalence may seem unsatisfactory, as it allows algorithms that are unimplementable in practice (let alone efficiently). I understand that the semantics of a logic are usually unable to talk about its syntax, but there are formalisms that do have a more intensional notion of algorithm equivalence, and they do so by syntactically (and semantically) separating the abstract levels, where nondeterminism lies, from the algorithm level. Those formalisms are much more complicated -- and, at least so far, less practical -- than TLA, but I had thought that behavior-equivalence missed something that may be of importance.

Anyway, I found Stephan’s answer, that the “problematic” specifications I gave as examples are known as “non machine-closed” to be completely satisfactory, especially combined with this note that clearly explains the tradeoffs and why preventing non-machine-closed specification at the logic level is not what we want (it says we want machine closure only for a low-level algorithm spec, but for higher-level abstractions we want to allow non machine-closed ones). I had come across the concept of machine closure, but never understood its significance until now.

BTW, that note ends with a terrific (and apt) quote by Stephen Jay Gould which says “One cannot avoid complexity by definition”, and I was wondering where it came from; I couldn’t find the source.

Ron

[Ron Pressler]

P.S.

I was also surprised to learn how invariance under stuttering interacts with this issue. I haven't thought it through, but it seems to me that without stuttering invariance, machine specifications would still be safety properties (i.e., closed), but safety properties would be able to specify undesired "prescience". Stuttering pushes future events indefinitely ahead, into the realm of liveness properties, which makes prescience a machine-closure-breaking liveness property. So far, I've seen invariance under stuttering justified as pragmatic or obvious, but this is an additional justification, it seems.

Ron

[Ioannis Filippidis]

On Saturday, November 19, 2016 at 2:19:39 PM UTC-8, Ron Pressler wrote:

 

I haven't thought it through, but it seems to me that without stuttering invariance, machine specifications would still be safety properties (i.e., closed), but safety properties would be able to specify undesired "prescience". Stuttering pushes future events indefinitely ahead, into the realm of liveness properties, which makes prescience a machine-closure-breaking liveness property.

A small comment: outside TLA, a formula of the form `Init /\ [] SomeAction` can "block later", because some step other than the first few violates the formula.

Stuttering allows `Init /\ [][ SomeAction ]_v` (outside TLA: `Init /\ []( SomeAction \/ (v = v') )`)
to reach just before the state where it would have blocked above, and then remain there, stuttering forever (the `v = v'` term).
This infinite stuttering may still be undesired, and a liveness property can require that it doesn't happen.

 

So far, I've seen invariance under stuttering justified as pragmatic or obvious, but this is an additional justification, it seems.

Stuttering invariance is also useful for comparing specifications at different levels of abstraction [1].

[1] https://research.microsoft.com/en-us/um/people/lamport/pubs/pubs.html#what-good

Ron

 
ioannis

[Stephan Merz]

Safety properties constrain finite sequences of states (prefixes of behaviors), and the possibility of stuttering forever from any point – rather than actual stuttering invariance – effectively lets you represent finite sequences in an LTL framework. In standard LTL or with "raw TLA" specifications (where []A is a temporal formula for an arbitrary action A), the mere fact that the semantics talks about infinite sequences already introduces an element of liveness because "the clock ticks infinitely often". For example, the specification

x = 0 /\ [](x' = x+1)

implies the liveness property

\A n \in Nat : <>(x > n)

so the specification is not a safety property. The formula

x = 0 /\ [](x' = x+1 \/ \E z : [](x=z))

is not stuttering invariant, but it still describes a safety property.

Stephan

[Ioannis Filippidis]

On Sun, Nov 20, 2016 at 12:37 AM, Stephan Merz <stepha...@gmail.com> wrote:

For example, the specification

   x = 0 /\ [](x' = x+1)

implies the liveness property

  \A n \in Nat : <>(x > n)

so the specification is not a safety property.

Hi Stephan,

I am trying to understand why this specification is not a safety property.

Every behavior that violates it has some finite prefix that contains some step that violates either the initial condition `x = 0` or the action `x' = x + 1`.

If a safety property is one for which every violating behavior has a finite prefix that cannot be extended to a satisfying behavior,

then this raw TLA formula seems to describe a safety property. Is this wrong, or another definition of safety used?

I do see the element of liveness originating from the semantics, in the comparison that

we are able to require a liveness property, even though (I think) no TLA formula of the form `Init /\ [][A]_v` implies
any liveness property of the form `[]<><< B >>_v`. On the other hand, it could imply a liveness property

that doesn't mention steps (of the form `[]<> P` for `P` a state predicate).

ioannis

[Stephan Merz]

Hi Ioannis,

you are of course right – I don't know what I was thinking.

Sorry,

Stephan

[Ron Pressler]

On Sunday, November 20, 2016 at 1:03:42 AM UTC+2, Ioannis Filippidis wrote:

A small comment: outside TLA, a formula of the form `Init /\ [] SomeAction` can "block later", because some step other than the first few violates the formula.

Stuttering allows `Init /\ [][ SomeAction ]_v` (outside TLA: `Init /\ []( SomeAction \/ (v = v') )`)
to reach just before the state where it would have blocked above, and then remain there, stuttering forever (the `v = v'` term).
This infinite stuttering may still be undesired, and a liveness property can require that it doesn't happen.

That is precisely the "painting into a corner" that Dederichs and Weber mention in the paper that Abadi, Lamport et al. respond to. By delaying the point of hitting the wall indefinitely, stuttering invariance pushes any prescient behavior that avoids it into a (machine closure breaking) liveness property. But while D&W try to redefine liveness so that it never breaks machine closure, A&L respond that non-machine closed specifications are useful for abstraction.
 
 

So far, I've seen invariance under stuttering justified as pragmatic or obvious, but this is an additional justification, it seems.

Stuttering invariance is also useful for comparing specifications at different levels of abstraction

Yes, that's the pragmatic justification I was referring to. The "obvious" one was that it hides internal behavior (the two are really just one).

Ron

 

[Ron Pressler]

On Sunday, November 20, 2016 at 2:38:23 PM UTC+2, Ioannis Filippidis wrote:

On the other hand, it could imply a liveness property

that doesn't mention steps (of the form `[]<> P` for `P` a state predicate).

Do you have an example of  `Init /\ [][A]_v` implying `[]<> P` but not `[]P`?

[Ioannis Filippidis]

Good point, no I do not have such an example. I think that the following claim can be proved.
(Please correct me if wrong.)

ASSUME:
    1. VARIABLE v    (* If there are more, define `v` as a tuple of all mentioned variables. *)
    2. STATE Init(v), P(v)
    3. ACTION A(v)    (* The expression `v'` can appear within the formula `A(v)`. *)
    4. \EE v:  Init(v)
    5. No variable symbols other than `v` occur in `Init(v), P(v), A(v)`
    6. |= ( Init(v) /\ [][ A(v) ]_v ) => ( []<>P(v) /\ ~ []P(v) )
PROVE: FALSE  (* contradiction *)

Proof sketch:
<1>1. |= ([]<> P(v) /\ ~ [] P(v))   =>   (<>P(v) /\ <> ~P(v))
    <2>1. |= []<> P /\ ~ []P \equiv []<> P /\ <> ~P
    <2>2. |= []<> P /\ <> ~P => <> P /\ <> ~P
    <2>3. QED.    BY <2>1, <2>2.
<1>2. F == Init(v) /\ [][ A(v) ]_v
<1>3. \E sigma:  IsABehavior(sigma) /\ sigma |= Init(v)    (* So we can start from state `sigma[0]`. *)
    <2>1. \EE v:  Init(v)    BY A3.
    <2>2. QED.   BY <2>1, DEF \EE, /\-elim.
<1>4. PICK sigma:  IsABehavior(sigma) /\ sigma |= Init(v)
    BY <1>3.
<1>5. tau == [n \in Nat |-> sigma[0] ]
<1>6. IsABehavior(tau) /\ tau |= F    (* The behavior `tau` stutters forever at state `sigma[0]`. *)
    <2>1. IsABehavior(tau)    BY <1>4, <1>5, DEF IsABehavior.
    <2>2. tau |= Init(v)    BY <2>1, <1>4.
    <2>3. tau |= [][ FALSE ]_v    BY <2>1 (\A n \in Nat:  tau[n] = tau[n + 1]).
    <2>4. QED.   BY <2>2, <2>3, TLA+ semantics.
<1>7. CASE  sigma[0] |= P(v)
    <2>1. tau |= [] P(v)    BY <1>5, <1>7/A.    (* A = Assumption *)
    <2>2. tau |= ~ <> ~ P(v)    BY <2>1.
    <2>3. IsABehavior(tau) /\ tau |= F /\ ~ <> ~ P(v)    BY <1>6, <2>2.
    <2>4. QED.    BY <2>3, <1>1, <1>2, A6.
<1>8. CASE  sigma[0] |= ~ P(v)
    PROOF: similar to that of <1>7.
<1>9. QED.
    BY <1>7, <1>8, which are exhaustive.


So, the liveness property `[]<>P /\ ~ []P` requires that a nonstuttering step `<< sigma[k], sigma[k + 1] >>, k \in Nat` with
`sigma[k] |= P  \equiv ~ sigma[k + 1] |= P` should eventually happen, and so cannot be implied by a formula of
the form `Init /\ [][A]_v`, for the same reason that a liveness property of the form `<><< B >>_v` cannot be implied.

I think that the comment about an example that does not imply `[]P` was a good observation that
suggests the following about the element of liveness
(which seems to be the main point about the clock "ticking" in the original comment):
a raw TLA safety property (e.g., `Init /\ []A`) can require liveness properties over nonstuttering steps,
whereas a TLA safety property (e.g., `Init /\ [][A]_v`) cannot.

ioannis

[Stephan Merz]

Hi Ioannis,

Do you have an example of  `Init /\ [][A]_v` implying `[]<> P` but not `[]P`?

ASSUME:
    1. VARIABLE v    (* If there are more, define `v` as a tuple of all mentioned variables. *)
    2. STATE Init(v), P(v)
    3. ACTION A(v)    (* The expression `v'` can appear within the formula `A(v)`. *)
    4. \EE v:  Init(v)
    5. No variable symbols other than `v` occur in `Init(v), P(v), A(v)`
    6. |= ( Init(v) /\ [][ A(v) ]_v ) => ( []<>P(v) /\ ~ []P(v) )
PROVE: FALSE  (* contradiction *)

that is not exactly what is claimed above. A specification implying ~[]P is different from (actually, stronger than) a specification not implying []P.

I think that the comment about an example that does not imply `[]P` was a good observation that
suggests the following about the element of liveness
(which seems to be the main point about the clock "ticking" in the original comment):
a raw TLA safety property (e.g., `Init /\ []A`) can require liveness properties over nonstuttering steps,
whereas a TLA safety property (e.g., `Init /\ [][A]_v`) cannot.

Indeed, it is quite easy to prove that a specification of the form

  Init /\ [][A]_v

implies a formula <>P (where P is a state predicate) only if it implies P, and it implies []<>P or <>[]P only if it implies []P.

Thanks,

Stephan