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