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

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

On Tuesday, October 31, 2017 at 10:15:30 AM UTC-7, Janice D'Sa wrote:

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.