New to TLA+: Questions about content in video courses 5 & 6

[Janice D'Sa]

First of all, I want to say that the video course is very engaging. TLA+ and the videos are helping me think of and understand software systems in a new way. Thank you for making these videos.

1. This question is about the TCommit formula in video lecture 6. I took a stab at writing it and my version looks like this:

TMCommit ==
/\ tmState = "init"
/\ tmPrepared = RM
/\ \A r \in RM : [type |-> "Prepared", rm |-> r] \in msgs \* DIFF-1
/\ \A r \in RM : rmState[r] = "Prepared" \* DIFF-2
/\ tmState' = "done"
/\ msgs' = msgs \cup {[type |-> "Commit"]}

The version in the video looks like this:

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>>

Questions: Please look for the lines with comments DIFF-1 and DIFF-2 in my solution. Why are DIFF-1 and DIFF-2 not enabling conditions for the transaction manager's commit? Shouldn't all resource managers have sent a "Prepared" message and shouldn't all resource managers be in the "Prepared" state for the transaction manager to commit?

2. This question is about the canCommit formula in video lecture 5.

Questions: In the canCommit formula, why is it OK for all resource managers to be in prepared OR committed states? Shouldn't they only be in the prepared state?

Thanks,
Janice.

[Leslie Lamport]

Question 1:  You can use TLC to check that it is an invariant of the
specification that the first two conjuncts of TMCommit imply your
conjuncts DIFF-1 and DIFF-2 (assuming you correct "Prepared" in DIFF-2
to "prepared").  Hence, they are correct but redundant.  And, of
course, you omitted the UNCHANGED clause in your definition.

Question 2: If canCommit were defined to equal

   \A r \in RM : rmState[r] = "prepared"

how could more than one RM ever decide to commit?

Leslie