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

Re: [tlaplus] Nondeterminism and equivalence

Hi Ioannis,

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

    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.