TLAPS and Coq proof of TwoPC protocol.

TwoPC/Coq/.gitignore

@@ -0,0 +1,30 @@
+.*.aux
+*.a
+*.cma
+*.cmi
+*.cmo
+*.cmx
+*.cmxa
+*.cmxs
+*.glob
+*.ml.d
+*.ml4.d
+*.mli.d
+*.mllib.d
+*.mlpack.d
+*.native
+*.o
+*.v.d
+*.vio
+*.vo
+.coq-native/
+.csdp.cache
+.lia.cache
+.nia.cache
+.nlia.cache
+.nra.cache
+csdp.cache
+lia.cache
+nia.cache
+nlia.cache
+nra.cache

TwoPC/Coq/Crush.v

@@ -0,0 +1,248 @@
+(* Copyright (c) 2008-2012, Adam Chlipala
+ * 
+ * This work is licensed under a
+ * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
+ * Unported License.
+ * The license text is available at:
+ *   http://creativecommons.org/licenses/by-nc-nd/3.0/
+ *)
+
+Require Import Eqdep List Omega.
+
+Set Implicit Arguments.
+
+
+(** A version of [injection] that does some standard simplifications afterward: clear the hypothesis in question, bring the new facts above the double line, and attempt substitution for known variables. *)
+Ltac inject H := injection H; clear H; intros; try subst.
+
+(** Try calling tactic function [f] on all hypotheses, keeping the first application that doesn't fail. *)
+Ltac appHyps f :=
+  match goal with
+    | [ H : _ |- _ ] => f H
+  end.
+
+(** Succeed iff [x] is in the list [ls], represented with left-associated nested tuples. *)
+Ltac inList x ls :=
+  match ls with
+    | x => idtac
+    | (_, x) => idtac
+    | (?LS, _) => inList x LS
+  end.
+
+(** Try calling tactic function [f] on every element of tupled list [ls], keeping the first call not to fail. *)
+Ltac app f ls :=
+  match ls with
+    | (?LS, ?X) => f X || app f LS || fail 1
+    | _ => f ls
+  end.
+
+(** Run [f] on every element of [ls], not just the first that doesn't fail. *)
+Ltac all f ls :=
+  match ls with
+    | (?LS, ?X) => f X; all f LS
+    | (_, _) => fail 1
+    | _ => f ls
+  end.
+
+(** Workhorse tactic to simplify hypotheses for a variety of proofs.
+   * Argument [invOne] is a tuple-list of predicates for which we always do inversion automatically. *)
+Ltac simplHyp invOne :=
+  (** Helper function to do inversion on certain hypotheses, where [H] is the hypothesis and [F] its head symbol *)
+  let invert H F :=
+    (** We only proceed for those predicates in [invOne]. *)
+    inList F invOne;
+    (** This case covers an inversion that succeeds immediately, meaning no constructors of [F] applied. *)
+      (inversion H; fail)
+    (** Otherwise, we only proceed if inversion eliminates all but one constructor case. *)
+      || (inversion H; [idtac]; clear H; try subst) in
+
+  match goal with
+    (** Eliminate all existential hypotheses. *)
+    | [ H : ex _ |- _ ] => destruct H
+
+    (** Find opportunities to take advantage of injectivity of data constructors, for several different arities. *)
+    | [ H : ?F ?X = ?F ?Y |- ?G ] =>
+      (** This first branch of the [||] fails the whole attempt iff the arguments of the constructor applications are already easy to prove equal. *)
+      (assert (X = Y); [ assumption | fail 1 ])
+      (** If we pass that filter, then we use injection on [H] and do some simplification as in [inject].
+         * The odd-looking check of the goal form is to avoid cases where [injection] gives a more complex result because of dependent typing, which we aren't equipped to handle here. *)
+      || (injection H;
+        match goal with
+          | [ |- X = Y -> G ] =>
+            try clear H; intros; try subst
+        end)
+    | [ H : ?F ?X ?U = ?F ?Y ?V |- ?G ] =>
+      (assert (X = Y); [ assumption
+        | assert (U = V); [ assumption | fail 1 ] ])
+      || (injection H;
+        match goal with
+          | [ |- U = V -> X = Y -> G ] =>
+            try clear H; intros; try subst
+        end)
+
+    (** Consider some different arities of a predicate [F] in a hypothesis that we might want to invert. *)
+    | [ H : ?F _ |- _ ] => invert H F
+    | [ H : ?F _ _ |- _ ] => invert H F
+    | [ H : ?F _ _ _ |- _ ] => invert H F
+    | [ H : ?F _ _ _ _ |- _ ] => invert H F
+    | [ H : ?F _ _ _ _ _ |- _ ] => invert H F
+
+    (** Use an (axiom-dependent!) inversion principle for dependent pairs, from the standard library. *)
+    | [ H : existT _ ?T _ = existT _ ?T _ |- _ ] => generalize (inj_pair2 _ _ _ _ _ H); clear H
+
+    (** If we're not ready to use that principle yet, try the standard inversion, which often enables the previous rule. *)
+    | [ H : existT _ _ _ = existT _ _ _ |- _ ] => inversion H; clear H
+
+    (** Similar logic to the cases for constructor injectivity above, but specialized to [Some], since the above cases won't deal with polymorphic constructors. *)
+    | [ H : Some _ = Some _ |- _ ] => injection H; clear H
+  end.
+
+(** Find some hypothesis to rewrite with, ensuring that [auto] proves all of the extra subgoals added by [rewrite]. *)
+Ltac rewriteHyp :=
+  match goal with
+    | [ H : _ |- _ ] => rewrite H by solve [ auto ]
+  end.
+
+(** Combine [autorewrite] with automatic hypothesis rewrites. *)
+Ltac rewriterP := repeat (rewriteHyp; autorewrite with core in *).
+Ltac rewriter := autorewrite with core in *; rewriterP.
+
+(** This one is just so darned useful, let's add it as a hint here. *)
+Hint Rewrite app_ass.
+
+(** Devious marker predicate to use for encoding state within proof goals *)
+Definition done (T : Type) (x : T) := True.
+
+(** Try a new instantiation of a universally quantified fact, proved by [e].
+   * [trace] is an accumulator recording which instantiations we choose. *)
+Ltac inster e trace :=
+  (** Does [e] have any quantifiers left? *)
+  match type of e with
+    | forall x : _, _ =>
+      (** Yes, so let's pick the first context variable of the right type. *)
+      match goal with
+        | [ H : _ |- _ ] =>
+          inster (e H) (trace, H)
+        | _ => fail 2
+      end
+    | _ =>
+      (** No more quantifiers, so now we check if the trace we computed was already used. *)
+      match trace with
+        | (_, _) =>
+          (** We only reach this case if the trace is nonempty, ensuring that [inster] fails if no progress can be made. *)
+          match goal with
+            | [ H : done (trace, _) |- _ ] =>
+              (** Uh oh, found a record of this trace in the context!  Abort to backtrack to try another trace. *)
+              fail 1
+            | _ =>
+              (** What is the type of the proof [e] now? *)
+              let T := type of e in
+                match type of T with
+                  | Prop =>
+                    (** [e] should be thought of as a proof, so let's add it to the context, and also add a new marker hypothesis recording our choice of trace. *)
+                    generalize e; intro;
+                      assert (done (trace, tt)) by constructor
+                  | _ =>
+                    (** [e] is something beside a proof.  Better make sure no element of our current trace was generated by a previous call to [inster], or we might get stuck in an infinite loop!  (We store previous [inster] terms in second positions of tuples used as arguments to [done] in hypotheses.  Proofs instantiated by [inster] merely use [tt] in such positions.) *)
+                    all ltac:(fun X =>
+                      match goal with
+                        | [ H : done (_, X) |- _ ] => fail 1
+                        | _ => idtac
+                      end) trace;
+                    (** Pick a new name for our new instantiation. *)
+                    let i := fresh "i" in (pose (i := e);
+                      assert (done (trace, i)) by constructor)
+                end
+          end
+      end
+  end.
+
+(** After a round of application with the above, we will have a lot of junk [done] markers to clean up; hence this tactic. *)
+Ltac un_done :=
+  repeat match goal with
+           | [ H : done _ |- _ ] => clear H
+         end.
+
+Require Import JMeq.
+
+(** A more parameterized version of the famous [crush].  Extra arguments are:
+   * - A tuple-list of lemmas we try [inster]-ing 
+   * - A tuple-list of predicates we try inversion for *)
+Ltac crush' lemmas invOne :=
+  (** A useful combination of standard automation *)
+  let sintuition := simpl in *; intuition; try subst;
+    repeat (simplHyp invOne; intuition; try subst); try congruence in
+
+  (** A fancier version of [rewriter] from above, which uses [crush'] to discharge side conditions *)
+  let rewriter := autorewrite with core in *;
+    repeat (match goal with
+              | [ H : ?P |- _ ] =>
+                match P with
+                  | context[JMeq] => fail 1 (** JMeq is too fancy to deal with here. *)
+                  | _ => rewrite H by crush' lemmas invOne
+                end
+            end; autorewrite with core in *) in
+
+  (** Now the main sequence of heuristics: *)
+    (sintuition; rewriter;
+      match lemmas with
+        | false => idtac (** No lemmas?  Nothing to do here *)
+        | _ =>
+          (** Try a loop of instantiating lemmas... *)
+          repeat ((app ltac:(fun L => inster L L) lemmas
+          (** ...or instantiating hypotheses... *)
+            || appHyps ltac:(fun L => inster L L));
+          (** ...and then simplifying hypotheses. *)
+          repeat (simplHyp invOne; intuition)); un_done
+      end;
+      sintuition; rewriter; sintuition;
+      (** End with a last attempt to prove an arithmetic fact with [omega], or prove any sort of fact in a context that is contradictory by reasoning that [omega] can do. *)
+      try omega; try (elimtype False; omega)).
+
+(** [crush] instantiates [crush'] with the simplest possible parameters. *)
+Ltac crush := crush' false fail.
+
+(** * Wrap Program's [dependent destruction] in a slightly more pleasant form *)
+
+Require Import Program.Equality.
+
+(** Run [dependent destruction] on [E] and look for opportunities to simplify the result.
+   The weird introduction of [x] helps get around limitations of [dependent destruction], in terms of which sorts of arguments it will accept (e.g., variables bound to hypotheses within Ltac [match]es). *)
+Ltac dep_destruct E :=
+  let x := fresh "x" in
+    remember E as x; simpl in x; dependent destruction x;
+      try match goal with
+            | [ H : _ = E |- _ ] => try rewrite <- H in *; clear H
+          end.
+
+(** Nuke all hypotheses that we can get away with, without invalidating the goal statement. *)
+Ltac clear_all :=
+  repeat match goal with
+           | [ H : _ |- _ ] => clear H
+         end.
+
+(** Instantiate a quantifier in a hypothesis [H] with value [v], or, if [v] doesn't have the right type, with a new unification variable.
+   * Also prove the lefthand sides of any implications that this exposes, simplifying [H] to leave out those implications. *)
+Ltac guess v H :=
+  repeat match type of H with
+           | forall x : ?T, _ =>
+             match type of T with
+               | Prop =>
+                 (let H' := fresh "H'" in
+                   assert (H' : T); [
+                     solve [ eauto 6 ]
+                     | specialize (H H'); clear H' ])
+                 || fail 1
+               | _ =>
+                 specialize (H v)
+                 || let x := fresh "x" in
+                   evar (x : T);
+                   let x' := eval unfold x in x in
+                     clear x; specialize (H x')
+             end
+         end.
+
+(** Version of [guess] that leaves the original [H] intact *)
+Ltac guessKeep v H :=
+  let H' := fresh "H'" in
+    generalize H; intro H'; guess v H'.

TwoPC/Coq/Learn.v

@@ -0,0 +1,21 @@
+(* Forward chaining of applications, to facilitate "saturating" the known facts
+   without specializing. See Clément's thesis
+
+   http://pit-claudel.fr/clement/MSc/#org036d20e for a nicer explanation.
+*)
+
+Inductive Learnt {P:Prop} :=
+  | AlreadyLearnt (H:P).
+
+Local Ltac learn_fact H :=
+  let P := type of H in
+  lazymatch goal with
+    (* matching the type of H with the Learnt hypotheses means the
+    learning fails even when the proposition is known by a different
+    but unifiable type term *)
+  | [ Hlearnt: @Learnt P |- _ ] =>
+    fail 0 "already knew" P "through" Hlearnt
+  | _ => pose proof H; pose proof (AlreadyLearnt H)
+  end.
+
+Tactic Notation "learn" constr(H) := learn_fact H.

TwoPC/Coq/Makefile

@@ -0,0 +1,20 @@
+# Makefile originally taken from coq-club.
+
+%: Makefile.coq phony
+	+make -f Makefile.coq $@
+
+all: Makefile.coq
+	+make -f Makefile.coq all
+
+clean: Makefile.coq
+	+make -f Makefile.coq clean
+	rm -f Makefile.coq
+
+Makefile.coq: _CoqProject Makefile
+	coq_makefile -f _CoqProject | sed 's/$$(COQCHK) $$(COQCHKFLAGS) $$(COQLIBS)/$$(COQCHK) $$(COQCHKFLAGS) $$(subst -Q,-R,$$(COQLIBS))/' > Makefile.coq
+
+_CoqProject:
+
+Makefile:
+
+.PHONY: all clean

TwoPC/Coq/TwoPC.v

@@ -0,0 +1,291 @@
+Require Import List Bool Arith.
+Require Import TwoPC.Crush TwoPC.Learn.
+
+(** The collection of resource managers (RM). *)
+Axiom RM : Type.
+
+(** Assumes two RMs are distinguishable. *)
+Axiom RMDecidable :
+  forall x y : RM, { x = y } + { x <> y }.
+
+Inductive RMState : Set :=
+  RMWorking | RMPrepared | RMCommitted | RMAborted.
+
+Inductive TMState : Set :=
+| TMInit | TMCommitted | TMAborted.
+
+Inductive Message : Type :=
+  MsgPrepared : RM -> Message
+| MsgCommit | MsgAbort.
+
+Record State := {
+  rmState : RM -> RMState;
+  tmState : TMState;
+  tmPrepared : RM -> bool;
+  msgs : list Message
+}.
+
+Inductive StateInit : State -> Prop :=
+| InitIntro :
+    forall (rmInit : RM -> RMState) (tmPreparedInit : RM -> bool),
+    (forall rm, rmInit rm = RMWorking /\ tmPreparedInit rm = false) ->
+    StateInit {| rmState := rmInit;
+                 tmState := TMInit;
+                 tmPrepared := tmPreparedInit;
+                 msgs := nil |}.
+
+Inductive StateStep : State -> State -> Prop :=
+| TMRcvPrepared :
+    forall rm rmState tmState msgs tmPrepared tmPrepared',
+      tmState = TMInit ->
+      In (MsgPrepared rm) msgs ->
+      (forall rm0, rm0 <> rm -> tmPrepared rm0 = tmPrepared' rm0) ->
+      tmPrepared' rm = true ->
+      StateStep {| rmState := rmState;
+                   tmState := tmState;
+                   tmPrepared := tmPrepared;
+                   msgs := msgs |}
+                {| rmState := rmState;
+                   tmState := tmState;
+                   tmPrepared := tmPrepared';
+                   msgs := msgs |}
+
+| TMCommit :
+    forall rmState tmState tmState' tmPrepared msgs msgs',
+      tmState = TMInit ->
+      (forall rm, tmPrepared rm = true) ->
+      tmState' = TMCommitted ->
+      msgs' = cons MsgCommit msgs ->
+      StateStep {| rmState := rmState;
+                   tmState := tmState;
+                   tmPrepared := tmPrepared;
+                   msgs := msgs |}
+                {| rmState := rmState;
+                   tmState := tmState';
+                   tmPrepared := tmPrepared;
+                   msgs := msgs' |}
+
+| TMAbort :
+    forall rmState tmState tmState' tmPrepared msgs msgs',
+      tmState = TMInit ->
+      tmState' = TMAborted ->
+      msgs' = cons MsgAbort msgs ->
+      StateStep {| rmState := rmState;
+                   tmState := tmState;
+                   tmPrepared := tmPrepared;
+                   msgs := msgs |}
+                {| rmState := rmState;
+                   tmState := tmState';
+                   tmPrepared := tmPrepared;
+                   msgs := msgs' |}
+
+| RMPrepare :
+    forall rm rmState rmState' tmState tmPrepared msgs msgs',
+      rmState rm = RMWorking ->
+      (forall rm0, rm0 <> rm -> rmState rm0 = rmState' rm0) ->
+      rmState' rm = RMPrepared ->
+      msgs' = cons (MsgPrepared rm) msgs ->
+      StateStep {| rmState := rmState;
+                   tmState := tmState;
+                   tmPrepared := tmPrepared;
+                   msgs := msgs |}
+                {| rmState := rmState';
+                   tmState := tmState;
+                   tmPrepared := tmPrepared;
+                   msgs := msgs' |}
+
+| RMChooseToAbort :
+    forall rm rmState rmState' tmState tmPrepared msgs,
+      rmState rm = RMWorking ->
+      (forall rm0, rm0 <> rm -> rmState rm0 = rmState' rm0) ->
+      rmState' rm = RMAborted ->
+      StateStep {| rmState := rmState;
+                   tmState := tmState;
+                   tmPrepared := tmPrepared;
+                   msgs := msgs |}
+                {| rmState := rmState';
+                   tmState := tmState;
+                   tmPrepared := tmPrepared;
+                   msgs := msgs |}
+
+| RMRcvCommitMsg :
+    forall rm rmState rmState' tmState tmPrepared msgs,
+      In MsgCommit msgs ->
+      (forall rm0, rm0 <> rm -> rmState rm0 = rmState' rm0) ->
+      rmState' rm = RMCommitted ->
+      StateStep {| rmState := rmState;
+                   tmState := tmState;
+                   tmPrepared := tmPrepared;
+                   msgs := msgs |}
+                {| rmState := rmState';
+                   tmState := tmState;
+                   tmPrepared := tmPrepared;
+                   msgs := msgs |}
+
+| RMRcvAbortMsg :
+    forall rm rmState rmState' tmState tmPrepared msgs,
+      In MsgAbort msgs ->
+      (forall rm0, rm0 <> rm -> rmState rm0 = rmState' rm0) ->
+      rmState' rm = RMAborted ->
+      StateStep {| rmState := rmState;
+                   tmState := tmState;
+                   tmPrepared := tmPrepared;
+                   msgs := msgs |}
+                {| rmState := rmState';
+                   tmState := tmState;
+                   tmPrepared := tmPrepared;
+                   msgs := msgs |}.
+
+Inductive StateMultiStep : State -> State -> Prop :=
+| StateMultiStep0 :
+    forall state,
+      StateMultiStep state state
+| StateMultiStep1 :
+    forall state state1 state2,
+      StateMultiStep state1 state2 ->
+      StateMultiStep state state1 ->
+      StateMultiStep state state2.
+
+Inductive Consistency : State -> Prop :=
+| ConsistencyIntro :
+    forall rmState tmState tmPrepared msgs,
+      ( (* if one RM is committed, other RMs cannot be aborted. *)
+        (exists rm, rmState rm = RMCommitted) ->
+        (forall rm, rmState rm <> RMAborted)
+      ) ->
+      ( (* if one RM is aborted, other RMs cannot be committed. *)
+        (exists rm, rmState rm = RMAborted) ->
+        (forall rm, rmState rm <> RMCommitted)
+      ) ->
+      Consistency {| rmState := rmState;
+                     tmState := tmState;
+                     tmPrepared := tmPrepared;
+                     msgs := msgs |}.
+
+Inductive Invariant : State -> Prop :=
+| InvariantIntro :
+    forall rmState tmState tmPrepared msgs,
+      (
+        tmState = TMInit -> (* 1PC *)
+        (
+          (forall rm, rmState rm <> RMCommitted) /\
+          (forall rm, (In (MsgPrepared rm) msgs <-> rmState rm = RMPrepared)) /\
+          (forall rm, tmPrepared rm = true -> rmState rm = RMPrepared)
+        )
+      ) ->
+      ( (* 2PC: Commit *)
+        tmState = TMCommitted ->
+        (
+          forall rm, rmState rm = RMCommitted \/ rmState rm = RMPrepared
+        )
+      ) ->
+      ( (* 2PC: Abort *)
+        tmState = TMAborted ->
+        (
+          forall rm, rmState rm <> RMCommitted
+        )
+      ) ->
+      ( (* Abort message in message list <==> TM is aborted *)
+        In MsgAbort msgs <-> tmState = TMAborted
+      ) ->
+      ( (* Committed message in message list <==> TM is committed *)
+        In MsgCommit msgs <-> tmState = TMCommitted
+      ) ->
+      Invariant {| rmState := rmState;
+                   tmState := tmState;
+                   tmPrepared := tmPrepared;
+                   msgs := msgs |}.
+
+Ltac inst_rm x :=
+  repeat
+    ( match goal with
+      | [ H: forall rm, _ |- _ ] => learn (H x)
+      end
+    );
+  repeat
+    ( match goal with
+      | [ H : Learnt |- _ ] => clear H
+      end
+    ).
+
+Ltac invert H := inversion H; subst; clear H.
+
+Lemma InvariantImpliesConsistency :
+  forall state, Invariant state -> Consistency state.
+Proof.
+  intros.
+  invert H. constructor; crush.
+  + destruct tmState0; crush;
+      try (inst_rm x; crush);
+      try (inst_rm rm; crush).
+  + destruct tmState0; crush;
+      try (inst_rm x; crush);
+      try (inst_rm rm; crush).
+Qed.
+
+Lemma InitStateSatisfiesInvariant :
+  forall state, StateInit state -> Invariant state.
+Proof.
+  intros.
+  invert H; constructor; crush;
+    try (inst_rm x); try (inst_rm rm); crush.
+Qed.
+
+Lemma StateStepKeepsInvariant :
+  forall state state',
+    StateStep state state' ->
+    Invariant state ->
+    Invariant state'.
+Proof.
+  intros.
+  invert H0; invert H.
+  + constructor; crush.
+    destruct (RMDecidable rm0 rm).
+    - inst_rm rm; crush.
+    - inst_rm rm0; eauto.
+  + constructor; crush.
+  + constructor; crush.
+  + destruct tmState0.
+    - constructor; crush;
+      destruct (RMDecidable rm0 rm); crush; inst_rm rm; inst_rm rm0; crush.
+    - crush. inst_rm rm; crush.
+    - constructor; crush;
+      destruct (RMDecidable rm0 rm); crush; inst_rm rm; inst_rm rm0; crush.
+  + destruct tmState0.
+    - constructor; crush;
+      destruct (RMDecidable rm0 rm); crush; inst_rm rm; inst_rm rm0; crush.
+    - crush. inst_rm rm; crush.
+    - constructor; crush;
+      destruct (RMDecidable rm0 rm); crush; inst_rm rm; inst_rm rm0; crush.
+  + constructor; crush.
+    destruct (RMDecidable rm0 rm).
+    - crush.
+    - inst_rm rm0; crush.
+      left; crush.
+      right; crush.
+  + constructor; crush.
+    destruct (RMDecidable rm0 rm).
+    - crush.
+    - inst_rm rm0; crush.
+Qed.
+
+Lemma Safety' :
+  forall state state',
+    StateMultiStep state state' ->
+    Invariant state ->
+    Invariant state'.
+Proof.
+  induction 1; crush.
+Qed.
+
+Theorem Safety :
+  forall state state',
+    StateMultiStep state state' ->
+    StateInit state ->
+    Consistency state'.
+Proof.
+  intros.
+  apply InvariantImpliesConsistency.
+  apply InitStateSatisfiesInvariant in H0.
+  eapply Safety'; eauto.
+Qed.

TwoPC/Coq/_CoqProject

@@ -0,0 +1,4 @@
+-R . TwoPC
+TwoPC.v
+Learn.v
+Crush.v

TwoPC/TLAPS/TwoPC.tla

@@ -0,0 +1,178 @@
+-------------------------------- MODULE TwoPC --------------------------------
+EXTENDS TLAPS
+
+CONSTANTS RM, RMState, TMState, Msgs
+
+VARIABLES rmState, tmState, tmPrepared, msgs
+
+vars == <<rmState, tmState, tmPrepared, msgs>>
+
+AXIOM RMStateAxiom ==
+    /\ RMState = {"working", "prepared", "committed", "aborted"}
+
+AXIOM TMStateAxiom ==
+    /\ TMState = {"init", "committed", "aborted"}
+
+AXIOM MsgsAxiom ==
+    /\ Msgs = [type: {"prepared"}, rm: RM] \union [type: {"commit", "abort"}]
+
+ExistAbortMsg ==
+    /\ [type |-> "abort"] \in msgs
+
+ExistCommitMsg ==
+    /\ [type |-> "commit"] \in msgs
+
+Init ==
+    /\ rmState = [rm \in RM |-> "working"]
+    /\ tmState = "init"
+    /\ tmPrepared = {}
+    /\ msgs = {}
+
+TMRcvPrepared(rm) ==
+    /\ tmState = "init"
+    /\ [type |-> "prepared", rm |-> rm] \in msgs
+    /\ tmPrepared' = tmPrepared \union {rm}
+    /\ UNCHANGED <<rmState, tmState, msgs>>
+
+TMCommit ==
+    /\ tmState = "init"
+    /\ tmPrepared = RM
+    /\ tmState' = "committed"
+    /\ msgs' = msgs \union {[type |-> "commit"]}
+    /\ UNCHANGED <<rmState, tmPrepared>>
+
+TMAbort ==
+    /\ tmState = "init"
+    /\ tmState' = "aborted"
+    /\ msgs' = msgs \union {[type |-> "abort"]}
+    /\ UNCHANGED <<rmState, tmPrepared>>
+
+RMPrepare(rm) ==
+    /\ rmState[rm] = "working"
+    /\ rmState' = [rmState EXCEPT ![rm] = "prepared"]
+    /\ msgs' = msgs \union {[type |-> "prepared", rm |-> rm]}
+    /\ UNCHANGED <<tmState, tmPrepared>>
+
+RMChooseToAbort(rm) ==
+    /\ rmState[rm] = "working"
+    /\ rmState' = [rmState EXCEPT ![rm] = "aborted"]
+    /\ UNCHANGED <<tmState, tmPrepared, msgs>>
+
+RMRcvCommitMsg(rm) ==
+    /\ ExistCommitMsg
+    /\ rmState' = [rmState EXCEPT ![rm] = "committed"]
+    /\ UNCHANGED <<tmState, tmPrepared, msgs>>
+
+RMRcvAbortMsg(rm) ==
+    /\ ExistAbortMsg
+    /\ rmState' = [rmState EXCEPT ![rm] = "aborted"]
+    /\ UNCHANGED <<tmState, tmPrepared, msgs>>
+
+RMOp(rm) ==
+    \/ TMRcvPrepared(rm)
+    \/ RMPrepare(rm)
+    \/ RMChooseToAbort(rm)
+    \/ RMRcvCommitMsg(rm)
+    \/ RMRcvAbortMsg(rm)
+
+ChooseRMOp ==
+    /\ \E rm \in RM:
+        /\ RMOp(rm)
+
+Next ==
+    \/ TMCommit
+    \/ TMAbort
+    \/ ChooseRMOp
+
+Spec == Init /\ [][Next]_vars
+
+RMStateTypeInvariant ==
+    /\ rmState \in [RM -> RMState]
+
+TMStateTypeInvariant ==
+    /\ tmState \in TMState
+
+TMPreparedTypeInvariant ==
+    /\ tmPrepared \subseteq RM
+
+MsgsTypeInvariant ==
+    /\ msgs \subseteq Msgs
+
+TypeInvariant ==
+    /\ RMStateTypeInvariant
+    /\ TMStateTypeInvariant
+    /\ TMPreparedTypeInvariant
+    /\ MsgsTypeInvariant
+
+ExistCommittedRM ==
+    /\ \E rm \in RM: rmState[rm] = "committed"
+
+ExistAbortedRM ==
+    /\ \E rm \in RM: rmState[rm] = "aborted"
+
+Consistency ==
+    /\ ExistCommittedRM => ~ExistAbortedRM
+    /\ ExistAbortedRM => ~ExistCommittedRM
+
+Invariant ==
+    /\ TypeInvariant
+    /\ ( tmState = "init" => 
+         ( /\ \A rm \in RM : rmState[rm] # "committed"
+           /\ \A rm \in RM : [type |-> "prepared", rm |-> rm] \in msgs <=> rmState[rm] = "prepared"
+           /\ \A rm \in tmPrepared : rmState[rm] = "prepared" )
+       )
+    /\ ( tmState = "committed" =>
+         ( /\ \A rm \in RM : (rmState[rm] = "committed" \/ rmState[rm] = "prepared") )
+       )
+    /\ ( tmState = "aborted" =>
+         ( /\ \A rm \in RM : rmState[rm] # "committed" )
+       )
+    /\ tmState = "committed" <=> ExistCommitMsg
+    /\ tmState = "aborted" <=> ExistAbortMsg
+
+LEMMA InvariantImpliesConsistency ==
+  Invariant => Consistency
+<1> USE DEF TypeInvariant, TMStateTypeInvariant, RMStateTypeInvariant, TMPreparedTypeInvariant, MsgsTypeInvariant
+<1> USE DEF Invariant, Consistency
+<1> USE DEF ExistCommittedRM, ExistAbortedRM
+<1>a CASE tmState = "init"
+  <2> QED BY <1>a, RMStateAxiom 
+<1>b CASE tmState = "committed"
+  <2> QED BY <1>b, RMStateAxiom 
+<1>c CASE tmState = "aborted"
+  <2> QED BY <1>c, RMStateAxiom 
+<1> QED BY <1>a, <1>b, <1>c, TMStateAxiom
+
+LEMMA InitStateSatisfiesInvariant ==
+  Init => Invariant
+<1> USE DEF TypeInvariant, TMStateTypeInvariant, RMStateTypeInvariant, TMPreparedTypeInvariant, MsgsTypeInvariant
+<1> USE DEF Init, Invariant, ExistCommitMsg, ExistAbortMsg
+<1> QED BY TMStateAxiom, RMStateAxiom, MsgsAxiom
+
+LEMMA StateStepKeepsInvariant ==
+  Invariant /\ Next => Invariant'
+<1> USE DEF TypeInvariant, TMStateTypeInvariant, RMStateTypeInvariant, TMPreparedTypeInvariant, MsgsTypeInvariant
+<1> USE DEF Invariant, Next
+<1> USE DEF ExistCommitMsg, ExistAbortMsg
+<1> USE DEF TMCommit, TMAbort, ChooseRMOp
+<1> USE DEF RMOp, TMRcvPrepared, RMPrepare, RMChooseToAbort, RMRcvCommitMsg, RMRcvAbortMsg
+<1> USE TMStateAxiom, RMStateAxiom, MsgsAxiom
+<1>a CASE TMCommit BY <1>a
+<1>b CASE TMAbort BY <1>b
+<1>c CASE ChooseRMOp
+  <2> PICK rm \in RM : RMOp(rm) BY <1>c
+  <2>a CASE TMRcvPrepared(rm) BY <2>a
+  <2>b CASE RMPrepare(rm) BY <2>b
+  <2>c CASE RMChooseToAbort(rm) BY <2>c
+  <2>d CASE RMRcvCommitMsg(rm) BY <2>d
+  <2>e CASE RMRcvAbortMsg(rm) BY <2>e
+  <2> QED BY <2>a, <2>b, <2>c, <2>d, <2>e
+<1> QED BY <1>a, <1>b, <1>c
+
+THEOREM Safety ==
+  Spec => []Consistency
+<1> SUFFICES Spec => []Invariant BY InvariantImpliesConsistency, PTL
+<1> SUFFICES ASSUME Init /\ [][Next]_vars PROVE []Invariant BY DEF Spec
+<1> QED BY InitStateSatisfiesInvariant, StateStepKeepsInvariant, PTL
+
+=============================================================================