Re: TLA+ Video Course

On Wednesday, 4 April 2018 07:30:41 UTC+10, Leslie Lamport  wrote:
> Lecture 10, the final lecture of the TLA+ Video Course, consisting of two videos, has now been posted.  As always, the home page of the course is:
>
>
>     https://lamport.azurewebsites.net/video/videos.html
>
>
> Leslie

Hi,

This may not be the right thread to post in, please feel free to correct me.

I'm enjoying the video series, currently up to video 6 (two phase commit) and I had a question:

From memory the state machine only allowed progress to the "committed" state from "prepared", however the definition for RMRcvCommitMsg(r) does not enforce that rmState[r] is equal to "prepared". The model works none the less, is this simply an oversight or am I misunderstanding something?

RMRcvCommitMsg(r) ==
(*************************************************************************)
(* Resource manager r is told by the TM to commit.                       *)
(*************************************************************************)
/\ rmState[r] = "prepared"  /* I added this to my definition */
/\ [type |-> "Commit"] \in msgs
/\ rmState' = [rmState EXCEPT ![r] = "committed"]
/\ UNCHANGED <<tmState, tmPrepared, msgs>>

Many thanks for creating this video series, I was finding it hard going just using the book,

regards