Hello,
I am trying to prove that the transaction commit [
TCommit.tla] eventually decides, i.e, it either commits or aborts. I added the following statements to the spec:
```
-----------------------------------------------------------------------------
FairTCSpec == TCSpec /\ WF_rmState(TCNext)
EventuallyDecided ==
<> (\A rm \in RM: rmState[rm] \in {"committed", "aborted"})
THEOREM FairTCSpec => EventuallyDecided
======================================
```
TLC can quickly verify `PROPERTY EventuallyDecided`. I am now trying to formally prove it with TLAPS, but I am struggling with TLAPS syntax.
I am trying to express the proof strategy that "U = number of RMs that are not decided" is a well-founded partial order. Initially, U is equal to the number of RMs. Prepare actions do not change U. Decide actions reduce U by 1. Whenever U is greater than 0, actions remain enabled. Therefore, U must go to zero, i.e, all RMs must eventually decide. This uses the "Lattice" and "WF1" proof rules from Figure 5 of
"The Temporal Logic of Actions".
This is what I have so far:
```
---- 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
```
Are such proofs supported by TLAPS? Any help including pointers to similar proofs would be much appreciated.
Best regards,
Abhilash Jindal
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to
tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit
https://groups.google.com/d/msgid/tlaplus/5be4d308-7d0b-4cf1-b972-f95da743f52an%40googlegroups.com.