[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`?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 thatsuggests 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]_vimplies 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