### Lecture 5

This web page was written on:
30 August 2021

The video was produced on:
12 August 2017

STOP  AND
T H I N K

Copy the following tiny text, either by clicking on the Copy button below it, or by your usual method of copying text.
(***************************************************************************)
(* 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 rm.
-----------------------------------------------------------------------------
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.                                                         *)
(*************************************************************************)

Then paste the text into the module editor as the body of specification TCommit .