[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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.