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

[Janice D'Sa <dsaj...@xxxxxxxxx>]

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.