This is as good a place as any for questions about the content of the video course.
The existence of the commit message implies that the RM is in either the "prepared" or "committed" state. In either case, the action asserts that the new value of the RM's state is "committed". If it was already in the "committed" state, this does nothing, so there is no need to disallow the step permitted by the action in that case. A step that does nothing does no harm.
In a later lecture you will learn that a step which leaves the state unchanged,is always allowed. Therefore the change that you made to the definition does not change the spec. But you needn't worry about that now.
Leslie
On Friday, June 15, 2018 at 10:30:52 PM UTC-7, Morgan Weetman wrote:
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