[tlaplus] Proving liveness with TLAPM

---- MODULE TCLivenessProof ----
EXTENDS TCommit, Naturals, FiniteSets, Sequences, TLAPS
(*********************************************************************
We assume the TCommit module already defines:
TCInit, TCNext, TCSpec, FairTCSpec, EventuallyDecided
and the state variables including rmState, etc.
*********************************************************************)

(************************************************************************)
(* Useful shorthands and the measure U *)
(************************************************************************)
U(st) == { rm \in RM : st[rm] \notin {"committed","aborted"} }
Decided == \A rm \in RM: rmState[rm] \in {"committed", "aborted"}

AXIOM CardinalityDecreases ==
\A S \in SUBSET RM:
\A x \in S:
Cardinality(S \ {x}) = Cardinality(S) - 1

AXIOM ZeroCardIsEmpty ==
\A S \in SUBSET RM:
Cardinality(S) = 0 => S = {}

(************************************************************************)
(* Lemmas about initial and final state *)
(************************************************************************)
LEMMA InitsToRM ==
TCInit => Cardinality(U(rmState)) = Cardinality(RM)
PROOF
<1> QED BY DEF U, TCInit

LEMMA ZeroIsDecided ==
Cardinality(U(rmState)) = 0 => Decided
PROOF
<1> HAVE Cardinality(U(rmState)) = 0
<1> { rm \in RM : rmState[rm] \notin {"committed","aborted"} } = {}
<2> QED BY ZeroCardIsEmpty DEF U
<1> QED BY DEF Decided

(************************************************************************)
(* Lemmas about how actions affect U *)
(************************************************************************)
LEMMA PrepareDoesNotDecreaseU ==
\A s \in RM, st \in [RM -> {"working", "prepared", "committed", "aborted"}]:
LET st' == [st EXCEPT ![s] = "prepared"] IN
st[s] \notin {"committed", "aborted"} =>
U(st) = U(st')
PROOF
OBVIOUS

LEMMA CommitDecreasesU ==
\A s \in RM, st \in [RM -> {"working", "prepared", "committed", "aborted"}]:
st[s] \notin {"committed", "aborted"} =>
LET st2 == [st EXCEPT ![s] = "committed"] IN
Cardinality(U(st2)) = Cardinality(U(st)) - 1
PROOF
<1> TAKE s \in RM, st \in [RM -> {"working", "prepared", "committed", "aborted"}]
<1> HAVE st[s] \notin {"committed", "aborted"}
<1>1. U(st) \in SUBSET RM
<2> QED BY DEF U
<1>2. s \in U(st)
<2> QED BY DEF U
<1>3. Cardinality(U(st) \ {s}) = Cardinality(U(st)) - 1
<2> QED BY <1>1, <1>2, CardinalityDecreases
<1>4. U([st EXCEPT ![s] = "committed"]) = U(st) \ {s}
<2> QED BY DEF U
<1>5. QED BY <1>3, <1>4

LEMMA AbortDecreasesU ==
\A s \in RM, st \in [RM -> {"working", "prepared", "committed", "aborted"}]:
st[s] \notin {"committed", "aborted"} =>
LET st2 == [st EXCEPT ![s] = "aborted"] IN
Cardinality(U(st2)) = Cardinality(U(st)) - 1
PROOF
<1> TAKE s \in RM, st \in [RM -> {"working", "prepared", "committed", "aborted"}]
<1> HAVE st[s] \notin {"committed", "aborted"}
<1>1. U(st) \in SUBSET RM
<2> QED BY DEF U
<1>2. s \in U(st)
<2> QED BY DEF U
<1>3. Cardinality(U(st) \ {s}) = Cardinality(U(st)) - 1
<2> QED BY <1>1, <1>2, CardinalityDecreases
<1>4. U([st EXCEPT ![s] = "aborted"]) = U(st) \ {s}
<2> QED BY DEF U
<1>5. QED BY <1>3, <1>4

(************************************************************************)
(* Prove for each k that U>=k ~> U <= k-1 using WF on TCNext. *)
(************************************************************************)
LEMMA WF1 ==
ASSUME NEW k \in 1..Cardinality(RM)
PROVE ([][TCNext]_rmState /\ WF_rmState(TCNext)) => (U(rmState) = k ~> U(rmState) <= k-1)
<1>1. (U(rmState) = k /\ [TCNext]_rmState) => (U(rmState') <= k-1)
<2> QED OMITTED
<1>2. (U(rmState) = k) => ENABLED TCNext
<2> QED OMITTED
<1>3. QED BY <1>1, <1>2, PTL \* Does not work