Re: TLA+ Video Course

[Morgan Weetman <morgan....@xxxxxxxxx>]

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