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.