# Re: [tlaplus] Nondeterminism and equivalence

On Sunday, November 20, 2016 at 1:59:54 PM UTC-8, Ron Pressler wrote:

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?

Good point, no I do not have such an example. I think that the following claim can be proved.

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

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