TLA Misc

AB.tla

--------------------------------- MODULE AB ---------------------------------
EXTENDS Integers, Sequences

CONSTANT Data

(***************************************************************************)
(* We first define Remove(i, seq) to be the sequence obtained by removing  *)
(* element number i from sequence seq.                                     *)
(***************************************************************************)
Remove(i, seq) ==
  [j \in 1..(Len(seq)-1) |-> IF j < i THEN seq[j]
                                      ELSE seq[j+1]]

VARIABLES AVar, BVar,   \* The same as in module ABSpec
          AtoB,  \* The sequence of data messages in transit from sender to receiver.
          BtoA   \* The sequence of ack messages in transit from receiver to sender.
                 \* Messages are sent by appending them to the end of the sequence.
                 \* and received by removing them from the head of the sequence.

vars == << AVar, BVar, AtoB, BtoA >>

TypeOK == /\ AVar \in Data \X {0,1}
          /\ BVar \in Data \X {0,1}
          /\ AtoB \in Seq(Data \X {0,1})
          /\ BtoA \in Seq({0,1})

Init == /\ AVar \in Data \X {1}
        /\ BVar = AVar
        /\ AtoB = << >>
        /\ BtoA = << >>

(***************************************************************************)
(* The action of the sender sending a data message by appending AVar to    *)
(* the end of the message queue AtoB.  It will keep sending the same       *)
(* message until it receives an acknowledgment for it from the receiver.   *)
(***************************************************************************)
ASnd == /\ AtoB' = Append(AtoB, AVar)
        /\ UNCHANGED <<AVar, BtoA, BVar>>

(***************************************************************************)
(* The action of the sender receiving an ack message.  If that ack is for  *)
(* the value it is sending, then it chooses another message to send and    *)
(* sets AVar to that message.  If the ack is for the previous value it     *)
(* sent, it ignores the message.  In either case, it removes the message   *)
(* from BtoA.                                                              *)
(***************************************************************************)
ARcv == /\ BtoA # << >>
        /\ IF Head(BtoA) = AVar[2]
             THEN \E d \in Data : AVar' = <<d, 1 - AVar[2]>>
             ELSE AVar' = AVar
        /\ BtoA' = Tail(BtoA)
        /\ UNCHANGED <<AtoB, BVar>>

(***************************************************************************)
(* The action of the receiver sending an acknowledgment message for the    *)
(* last data item it received.                                             *)
(***************************************************************************)
BSnd == /\ BtoA' = Append(BtoA, BVar[2])
        /\ UNCHANGED <<AVar, BVar, AtoB>>

(***************************************************************************)
(* The action of the receiver receiving a data message.  It sets BVar to   *)
(* that message if it's not for the data item it has already received.     *)
(***************************************************************************)
BRcv == /\ AtoB # << >>
        /\ IF Head(AtoB)[2] # BVar[2]
             THEN BVar' = Head(AtoB)
             ELSE BVar' = BVar
        /\ AtoB' = Tail(AtoB)
        /\ UNCHANGED <<AVar, BtoA>>

(***************************************************************************)
(* LoseMsg is the action that removes an arbitrary message from queue AtoB *)
(* or BtoA.                                                                *)
(***************************************************************************)
LoseMsg == /\ \/ /\ \E i \in 1..Len(AtoB):
                         AtoB' = Remove(i, AtoB)
                 /\ BtoA' = BtoA
              \/ /\ \E i \in 1..Len(BtoA):
                         BtoA' = Remove(i, BtoA)
                 /\ AtoB' = AtoB
           /\ UNCHANGED << AVar, BVar >>

Next == ASnd \/ ARcv \/ BSnd \/ BRcv \/ LoseMsg

Spec == Init /\ [][Next]_vars
-----------------------------------------------------------------------------
ABS == INSTANCE ABSpec

THEOREM Spec => ABS!Spec
-----------------------------------------------------------------------------
(***************************************************************************)
(* FairSpec is Spec with fairness conditions added.                        *)
(***************************************************************************)
FairSpec == Spec  /\  SF_vars(ARcv) /\ SF_vars(BRcv) /\
                      WF_vars(ASnd) /\ WF_vars(BSnd)
=============================================================================

AB2.tla

--------------------------------- MODULE AB2 ---------------------------------
(***************************************************************************)
(* This is a modification of spec AB in which instead of losing messages,  *)
(* messages are detectably "corrupted"--represented by being changed to    *)
(* the value Bad.  The to communication channels are represented by the    *)
(* variables AtoB2 and BtoA2.                                              *)
(***************************************************************************)
EXTENDS Integers, Sequences\* , TLC

CONSTANT Data, Bad
ASSUME Bad \notin (Data \X {0,1}) \cup {0,1}
  \* We need to asssume that Bad is different from any of the legal
  \* messsages.
VARIABLES AVar, BVar,   \* The same as in module ABSpec
          AtoB2, \* The sequence of data messages in transit from sender to receiver
          BtoA2  \* The sequence of ack messages in transit from receiver to sender
                 \* Messages are sent by appending them to the end of the sequence
                 \* and received by removing them from the head of the sequence.

vars == << AVar, BVar, AtoB2, BtoA2 >>

TypeOK == /\ AVar  \in Data \X {0,1}
          /\ BVar  \in Data \X {0,1}
          /\ AtoB2 \in Seq((Data \X {0,1}) \cup {Bad})
          /\ BtoA2 \in Seq({0,1, Bad})

Init == /\ AVar  \in Data \X {1}
        /\ BVar  = AVar
        /\ AtoB2 = << >>
        /\ BtoA2 = << >>

(***************************************************************************)
(* The action of the sender sending a data message by appending AVar to    *)
(* the end of the message queue AtoB2.  It will keep sending the same      *)
(* message until it receives an acknowledgment for it from the receiver.   *)
(***************************************************************************)
ASnd == /\ AtoB2' = Append(AtoB2, AVar)
        /\ UNCHANGED <<AVar, BtoA2, BVar>>

(***************************************************************************)
(* The action of the sender receiving an ack message.  If that ack is for  *)
(* the value it is sending, then it chooses another message to send and    *)
(* sets AVar to that message.  If the ack is for the previous value it     *)
(* sent, it ignores the message.  In either case, it removes the message   *)
(* from BtoA2.  Note that Bad cannot equal AVar[2], which is in {0,1}.     *)
(***************************************************************************)
ARcv == /\ BtoA2 # << >>
        /\ IF Head(BtoA2) = AVar[2]
             THEN \E d \in Data: AVar' = <<d, 1 - AVar[2]>>
             ELSE AVar' = AVar
        /\ BtoA2' = Tail(BtoA2)
        /\ UNCHANGED <<AtoB2, BVar>>

(***************************************************************************)
(* The action of the receiver sending an acknowledgment message for the    *)
(* last data item it received.                                             *)
(***************************************************************************)
BSnd == /\ BtoA2' = Append(BtoA2, BVar[2])
        /\ UNCHANGED <<AVar, BVar, AtoB2>>

(***************************************************************************)
(* The action of the receiver receiving a data message.  It ignores a Bad  *)
(* message.  Otherwise, it sets BVar to the message if it's not for the    *)
(* data item it has already received.                                      *)
(***************************************************************************)
BRcv == /\ AtoB2 # << >>
        /\ IF (Head(AtoB2) # Bad) /\ (Head(AtoB2)[2] # BVar[2])
             THEN BVar' = Head(AtoB2)
             ELSE BVar' = BVar
        /\ AtoB2' = Tail(AtoB2)
        /\ UNCHANGED <<AVar, BtoA2>>

(***************************************************************************)
(* CorruptMsg is the action that changes an arbitrary message in AtoB2 or  *)
(* BtoA2 to Bad.  (We don't bother testing if the message in AtoB2 already *)
(* equals Bad, since setting to Bad a message that already equals Bad is   *)
(* just a stuttering step.)                                                *)
(***************************************************************************)
CorruptMsg == /\ \/ /\ \E i \in 1..Len(AtoB2):
                         AtoB2' = [AtoB2 EXCEPT ![i] = Bad]
                    /\ BtoA2' = BtoA2
                 \/ /\ \E i \in 1..Len(BtoA2):
                         BtoA2' = [BtoA2 EXCEPT ![i] = Bad]
                    /\ AtoB2' = AtoB2
              /\ UNCHANGED << AVar, BVar >>

Next == ASnd \/ ARcv \/ BSnd \/ BRcv \/ CorruptMsg

Spec == Init /\ [][Next]_vars
-----------------------------------------------------------------------------
ABS == INSTANCE ABSpec

THEOREM Spec => ABS!Spec
-----------------------------------------------------------------------------
(***************************************************************************)
(* FairSpec is the analogue of formula FairSpec of module AB2.  That is,   *)
(* it is obtained by conjoining to formula Spec the fairness conditions    *)
(* that correspond to the ones in module AB2.  However, specification      *)
(* FairSpec of this module does not implement ABS!FairSpec.  You can use   *)
(* TLC to find a behavior in which no new values are ever sent.            *)
(***************************************************************************)
FairSpec ==
  Spec /\ SF_vars(ARcv) /\ SF_vars(BRcv) /\ WF_vars(ASnd) /\ WF_vars(BSnd)

(***************************************************************************)
(* A little thought reveals that, since messages are corrupted but not     *)
(* deleted, strong fairness of ARcv and BRcv is equivalent to weak         *)
(* fairness of those actions.  The shortest counterexample showing that    *)
(* FairSpec does not implement ABS!FairSpec, which is probably the one     *)
(* found by TLC, is a behavior in which a message is sent on an empty      *)
(* message channel, but is always corrupted before it can received.  This  *)
(* suggests that in addition to weak fairness of ARcv and BRcv, we want    *)
(* strong fairness of those actions when the head of the queue is not      *)
(* corrupt.  That leads to the following spec.                             *)
(***************************************************************************)
FairSpec2 ==
  Spec /\ WF_vars(ARcv) /\ WF_vars(BRcv) /\ WF_vars(ASnd) /\ WF_vars(BSnd)
       /\ SF_vars(ARcv /\ Head(BtoA2) # Bad)
       /\ SF_vars(BRcv /\ Head(AtoB2) # Bad)

(***************************************************************************)
(* Running TLC shows that FairSpec2 also does not implement ABS!FairSpec.  *)
(* In fact, I believe that it is impossible to obtain a specification that *)
(* implements ABS!FairSpec by conjoining to Spec fairness conditions on    *)
(* subactions of Next.  Module AB2P shows how we can modify the AB2        *)
(* specification to obtain a specification that implements ABS!Spec.       *)
(***************************************************************************)
-----------------------------------------------------------------------------
(***************************************************************************)
(* We define RemoveBad so that RemoveBad(seq) is the value obtained by     *)
(* removing from the sequence seq all elements that equal Bad.             *)
(***************************************************************************)
RECURSIVE RemoveBad(_)
RemoveBad(seq) ==
  IF seq = << >>
    THEN << >>
    ELSE (IF Head(seq) = Bad THEN << >> ELSE <<Head(seq)>>)
           \o RemoveBad(Tail(seq))

(***************************************************************************)
(* There's an easy way to define RemoveBad using the SelectSeq operator of *)
(* the Sequences module.  Here's the alternative definition.               *)
(***************************************************************************)
RemoveBadAlt(seq) == LET Test(elt) == elt # Bad
                     IN  SelectSeq(seq, Test)

(***************************************************************************)
(* The following statement defines AB!Spec to be the specification Spec of *)
(* module AB with RemoveBad(AtoB2) substituted for AtoB and                *)
(* RemoveBad(BtoA2) substituted for BtoA.                                  *)
(***************************************************************************)
AB == INSTANCE AB WITH AtoB <- RemoveBad(AtoB2), BtoA <- RemoveBad(BtoA2)

(***************************************************************************)
(* The following theorem asserts that the specification Spec of this       *)
(* module implements the specification Spec of module AB under the         *)
(* refinement mapping that substitutes RemoveBad(AtoB2) for AtoB and       *)
(* substitutes for every other variable and every constant of module AB    *)
(* the variable or constant of the same name.  This theorem is checked by  *)
(* having TLC check that the temporal property AB!Spec is satisfied by the *)
(* specification Spec.                                                     *)
(***************************************************************************)
THEOREM Spec => AB!Spec

=============================================================================
\* Modification History
\* Last modified Wed Jan 24 16:33:07 PST 2018 by lamport
\* Created Wed Mar 25 11:53:40 PDT 2015 by lamport

ABModel.cfg

CONSTANT
    a = a
    b = b
    c = c
    Data <- abc
CONSTRAINT SmallQueueConstraint
SPECIFICATION FairSpec
INVARIANT TypeOK
PROPERTY ABSpecFairSpec

ABModel.tla

---- MODULE ABModel ----

EXTENDS AB

CONSTANT a, b, c
abc == {a, b, c}
SmallQueueConstraint ==
    /\ Len(AtoB) =< 4
    /\ Len(BtoA) =< 4
ABSpecSpec == ABS!Spec
ABSpecFairSpec == ABS!FairSpec

====

ABSpec.tla

------------------------------ MODULE ABSpec --------------------------------
EXTENDS Integers

CONSTANT Data  \* The set of all possible data values.

VARIABLES AVar,   \* The last <<value, bit>> pair A decided to send.
          BVar    \* The last <<value, bit>> pair B received.

(***************************************************************************)
(* Type correctness means that AVar and BVar are tuples <<d, i>> where     *)
(* d \in Data and i \in {0, 1}.                                            *)
(***************************************************************************)
TypeOK == /\ AVar \in Data \X {0,1}
          /\ BVar \in Data \X {0,1}

(***************************************************************************)
(* It's useful to define vars to be the tuple of all variables, for        *)
(* example so we can write [Next]_vars instead of [Next]_<< ...  >>        *)
(***************************************************************************)
vars == << AVar, BVar >>


(***************************************************************************)
(* Initially AVar can equal <<d, 1>> for any Data value d, and BVar equals *)
(* AVar.                                                                   *)
(***************************************************************************)
Init == /\ AVar \in Data \X {1}
        /\ BVar = AVar

(***************************************************************************)
(* When AVar = BVar, the sender can "send" an arbitrary data d item by     *)
(* setting AVar[1] to d and complementing AVar[2].  It then waits until    *)
(* the receiver "receives" the message by setting BVar to AVar before it   *)
(* can send its next message.  Sending is described by action A and        *)
(* receiving by action B.                                                  *)
(***************************************************************************)
A == /\ AVar = BVar
     /\ \E d \in Data: AVar' = <<d, 1 - AVar[2]>>
     /\ BVar' = BVar

B == /\ AVar # BVar
     /\ BVar' = AVar
     /\ AVar' = AVar

Next == A \/ B

Spec == Init /\ [][Next]_vars

(***************************************************************************)
(* For understanding the spec, it's useful to define formulas that should  *)
(* be invariants and check that they are invariant.  The following         *)
(* invariant Inv asserts that, if AVar and BVar have equal second          *)
(* components, then they are equal (which by the invariance of TypeOK      *)
(* implies that they have equal first components).                         *)
(***************************************************************************)
Inv == (AVar[2] = BVar[2]) => (AVar = BVar)
-----------------------------------------------------------------------------
(***************************************************************************)
(* FairSpec is Spec with the addition requirement that it keeps taking     *)
(* steps.                                                                  *)
(***************************************************************************)
FairSpec == Spec /\ WF_vars(Next)
=============================================================================

ABSpecModel.cfg

SPECIFICATION FairSpec
CONSTANT Data <- abc
INVARIANT
    TypeOK
    Inv
PROPERTY
    BEventuallyCopiesA

ABSpecModel.tla

---- MODULE ABSpecModel ----

EXTENDS ABSpec

abc == {"a", "b", "c"}

BEventuallyCopiesA ==
    \A x \in (Data \X {0, 1}): AVar = x ~> BVar = x

====

gistfile1.txt

.

TCommit.tla

---- MODULE TCommit ----
EXTENDS TLC

(***************************************************************************)
(* This specification is explained in "Transaction Commit", Lecture 5 of   *)
(* the TLA+ Video Course.                                                  *)
(***************************************************************************)
CONSTANT RM       \* The set of participating resource managers

VARIABLE rmState  \* rmState[rm] is the state of resource manager r.
-----------------------------------------------------------------------------
TCTypeOK ==
  (*************************************************************************)
  (* The type-correctness invariant                                        *)
  (*************************************************************************)
  rmState \in [RM -> {"working", "prepared", "committed", "aborted"}]

TCInit ==   rmState = [r \in RM |-> "working"]
  (*************************************************************************)
  (* The initial predicate.                                                *)
  (*************************************************************************)

canCommit == \A r \in RM : rmState[r] \in {"prepared", "committed"}
  (*************************************************************************)
  (* True iff all RMs are in the "prepared" or "committed" state.          *)
  (*************************************************************************)

notCommitted == \A r \in RM : rmState[r] # "committed"
  (*************************************************************************)
  (* True iff no resource manager has decided to commit.                   *)
  (*************************************************************************)
-----------------------------------------------------------------------------
(***************************************************************************)
(* We now define the actions that may be performed by the RMs, and then    *)
(* define the complete next-state action of the specification to be the    *)
(* disjunction of the possible RM actions.                                 *)
(***************************************************************************)
Prepare(r) == /\ rmState[r] = "working"
              /\ rmState' = [rmState EXCEPT ![r] = "prepared"]

Decide(r)  == \/ /\ rmState[r] = "prepared"
                 /\ canCommit
                 /\ rmState' = [rmState EXCEPT ![r] = "committed"]
              \/ /\ rmState[r] \in {"working", "prepared"}
                 /\ notCommitted
                 /\ rmState' = [rmState EXCEPT ![r] = "aborted"]

TCNext == \E r \in RM : Prepare(r) \/ Decide(r)

  (*************************************************************************)
  (* The next-state action.                                                *)
  (*************************************************************************)
-----------------------------------------------------------------------------
TCConsistent ==
  (*************************************************************************)
  (* A state predicate asserting that two RMs have not arrived at          *)
  (* conflicting decisions.  It is an invariant of the specification.      *)
  (*************************************************************************)
  \A r1, r2 \in RM : ~ /\ rmState[r1] = "aborted"
                       /\ rmState[r2] = "committed"
-----------------------------------------------------------------------------
(***************************************************************************)
(* The following part of the spec is not discussed in Video Lecture 5.  It *)
(* will be explained in Video Lecture 8.                                   *)
(***************************************************************************)
TCSpec == TCInit /\ [][TCNext]_rmState
  (*************************************************************************)
  (* The complete specification of the protocol written as a temporal      *)
  (* formula.                                                              *)
  (*************************************************************************)

THEOREM TCSpec => [](TCTypeOK /\ TCConsistent)
  (*************************************************************************)
  (* This theorem asserts the truth of the temporal formula whose meaning  *)
  (* is that the state predicate TCTypeOK /\ TCInvariant is an invariant   *)
  (* of the specification TCSpec.  Invariance of this conjunction is       *)
  (* equivalent to invariance of both of the formulas TCTypeOK and         *)
  (* TCConsistent.                                                         *)
  (*************************************************************************)

=========================

TCommitModel.cfg

INIT TCInit
NEXT TCNext
CONSTANT
    a = a
    b = b
    c = c
    RM <- abc
SYMMETRY
    AbcSymmetry
INVARIANT
    TCTypeOK
    TCConsistent

TCommitModel.tla

---- MODULE TCommitModel ----

EXTENDS TCommit

CONSTANT a, b, c
abc == {a, b, c}
AbcSymmetry == Permutations(abc)

====

TwoPhase.tla

---- MODULE TwoPhase ----

(***************************************************************************)
(* This specification is discussed in "Two-Phase Commit", Lecture 6 of the *)
(* TLA+ Video Course.  It describes the Two-Phase Commit protocol, in      *)
(* which a transaction manager (TM) coordinates the resource managers      *)
(* (RMs) to implement the Transaction Commit specification of module       *)
(* TCommit.  In this specification, RMs spontaneously issue Prepared       *)
(* messages.  We ignore the Prepare messages that the TM can send to the   *)
(* RMs.                                                                    *)
(*                                                                         *)
(* For simplicity, we also eliminate Abort messages sent by an RM when it  *)
(* decides to abort.  Such a message would cause the TM to abort the       *)
(* transaction, an event represented here by the TM spontaneously deciding *)
(* to abort.                                                               *)
(***************************************************************************)
CONSTANT RM  \* The set of resource managers

VARIABLES
  rmState,       \* rmState[r] is the state of resource manager r.
  tmState,       \* The state of the transaction manager.
  tmPrepared,    \* The set of RMs from which the TM has received "Prepared"
                 \* messages.
  msgs
    (***********************************************************************)
    (* In the protocol, processes communicate with one another by sending  *)
    (* messages.  For simplicity, we represent message passing with the    *)
    (* variable msgs whose value is the set of all messages that have been *)
    (* sent.  A message is sent by adding it to the set msgs.  An action   *)
    (* that, in an implementation, would be enabled by the receipt of a    *)
    (* certain message is here enabled by the presence of that message in  *)
    (* msgs.  For simplicity, messages are never removed from msgs.  This  *)
    (* allows a single message to be received by multiple receivers.       *)
    (* Receipt of the same message twice is therefore allowed; but in this *)
    (* particular protocol, that's not a problem.                          *)
    (***********************************************************************)

Messages ==
  (*************************************************************************)
  (* The set of all possible messages.  Messages of type "Prepared" are    *)
  (* sent from the RM indicated by the message's rm field to the TM.       *)
  (* Messages of type "Commit" and "Abort" are broadcast by the TM, to be  *)
  (* received by all RMs.  The set msgs contains just a single copy of     *)
  (* such a message.                                                       *)
  (*************************************************************************)
  [type : {"Prepared"}, rm : RM]  \cup  [type : {"Commit", "Abort"}]

TPTypeOK ==
  (*************************************************************************)
  (* The type-correctness invariant                                        *)
  (*************************************************************************)
  /\ rmState \in [RM -> {"working", "prepared", "committed", "aborted"}]
  /\ tmState \in {"init", "done"}
  /\ tmPrepared \subseteq RM
  /\ msgs \subseteq Messages

TPInit ==
  (*************************************************************************)
  (* The initial predicate.                                                *)
  (*************************************************************************)
  /\ rmState = [r \in RM |-> "working"]
  /\ tmState = "init"
  /\ tmPrepared   = {}
  /\ msgs = {}
-----------------------------------------------------------------------------
(***************************************************************************)
(* We now define the actions that may be performed by the processes, first *)
(* the TM's actions, then the RMs' actions.                                *)
(***************************************************************************)
TMRcvPrepared(r) ==
  (*************************************************************************)
  (* The TM receives a "Prepared" message from resource manager r.  We     *)
  (* could add the additional enabling condition r \notin tmPrepared,      *)
  (* which disables the action if the TM has already received this         *)
  (* message.  But there is no need, because in that case the action has   *)
  (* no effect; it leaves the state unchanged.                             *)
  (*************************************************************************)
  /\ tmState = "init"
  /\ [type |-> "Prepared", rm |-> r] \in msgs
  /\ tmPrepared' = tmPrepared \cup {r}
  /\ UNCHANGED <<rmState, tmState, msgs>>

TMCommit ==
  (*************************************************************************)
  (* The TM commits the transaction; enabled iff the TM is in its initial  *)
  (* state and every RM has sent a "Prepared" message.                     *)
  (*************************************************************************)
  /\ tmState = "init"
  /\ tmPrepared = RM
  /\ tmState' = "done"
  /\ msgs' = msgs \cup {[type |-> "Commit"]}
  /\ UNCHANGED <<rmState, tmPrepared>>

TMAbort ==
  (*************************************************************************)
  (* The TM spontaneously aborts the transaction.                          *)
  (*************************************************************************)
  /\ tmState = "init"
  /\ tmState' = "done"
  /\ msgs' = msgs \cup {[type |-> "Abort"]}
  /\ UNCHANGED <<rmState, tmPrepared>>

RMPrepare(r) ==
  (*************************************************************************)
  (* Resource manager r prepares.                                          *)
  (*************************************************************************)
  /\ rmState[r] = "working"
  /\ rmState' = [rmState EXCEPT ![r] = "prepared"]
  /\ msgs' = msgs \cup {[type |-> "Prepared", rm |-> r]}
  /\ UNCHANGED <<tmState, tmPrepared>>

RMChooseToAbort(r) ==
  (*************************************************************************)
  (* Resource manager r spontaneously decides to abort.  As noted above, r *)
  (* does not send any message in our simplified spec.                     *)
  (*************************************************************************)
  /\ rmState[r] = "working"
  /\ rmState' = [rmState EXCEPT ![r] = "aborted"]
  /\ UNCHANGED <<tmState, tmPrepared, msgs>>

RMRcvCommitMsg(r) ==
  (*************************************************************************)
  (* Resource manager r is told by the TM to commit.                       *)
  (*************************************************************************)
  /\ [type |-> "Commit"] \in msgs
  /\ rmState' = [rmState EXCEPT ![r] = "committed"]
  /\ UNCHANGED <<tmState, tmPrepared, msgs>>

RMRcvAbortMsg(r) ==
  (*************************************************************************)
  (* Resource manager r is told by the TM to abort.                        *)
  (*************************************************************************)
  /\ [type |-> "Abort"] \in msgs
  /\ rmState' = [rmState EXCEPT ![r] = "aborted"]
  /\ UNCHANGED <<tmState, tmPrepared, msgs>>

TPNext ==
  \/ TMCommit \/ TMAbort
  \/ \E r \in RM :
       TMRcvPrepared(r) \/ RMPrepare(r) \/ RMChooseToAbort(r)
         \/ RMRcvCommitMsg(r) \/ RMRcvAbortMsg(r)
-----------------------------------------------------------------------------
(***************************************************************************)
(* The material below this point is not discussed in Video Lecture 6.  It  *)
(* will be explained in Video Lecture 8.                                   *)
(***************************************************************************)

TPSpec == TPInit /\ [][TPNext]_<<rmState, tmState, tmPrepared, msgs>>
  (*************************************************************************)
  (* The complete spec of the Two-Phase Commit protocol.                   *)
  (*************************************************************************)

THEOREM TPSpec => []TPTypeOK
  (*************************************************************************)
  (* This theorem asserts that the type-correctness predicate TPTypeOK is  *)
  (* an invariant of the specification.                                    *)
  (*************************************************************************)
-----------------------------------------------------------------------------
(***************************************************************************)
(* We now assert that the Two-Phase Commit protocol implements the         *)
(* Transaction Commit protocol of module TCommit.  The following statement *)
(* imports all the definitions from module TCommit into the current        *)
(* module.                                                                 *)
(***************************************************************************)
INSTANCE TCommit

THEOREM TPSpec => TCSpec
  (*************************************************************************)
  (* This theorem asserts that the specification TPSpec of the Two-Phase   *)
  (* Commit protocol implements the specification TCSpec of the            *)
  (* Transaction Commit protocol.                                          *)
  (*************************************************************************)
(***************************************************************************)
(* The two theorems in this module have been checked with TLC for six      *)
(* RMs, a configuration with 50816 reachable states, in a little over a    *)
(* minute on a 1 GHz PC.                                                   *)
(***************************************************************************)

====

TwoPhaseModel.cfg

INIT TPInit
NEXT TPNext
CONSTANT
    a = a
    b = b
    c = c
    RM <- abc
SYMMETRY
    AbcSymmetry
INVARIANT
    TPTypeOK
PROPERTY
    TCSpec

TwoPhaseModel.tla

---- MODULE TwoPhaseModel ----

EXTENDS TwoPhase

CONSTANT a, b, c
abc == {a, b, c}
AbcSymmetry == Permutations(abc)

====