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

[tlaplus] Question regarding Two Phase Commit spec and the enabling condition of one of its definitions



In Two Phase Commit, the formula RMChooseToAbort(r) has rmState[r]="working" as the enabling condition. Shouldn't "prepared" be a permissible enabling condition for a resource manager(RM) wanting to abort?

This is the definition given in the spec from the video course.

RMChooseToAbort(r) ==
 
(*************************************************************************)
 
(* Resource manager r spontaneously decides to abort.  As noted above, r *)
 
(* does not send any message in our simplified spec.                     *)
 
(*************************************************************************)
 
/\ rmState[r] = "working"
 
/\ rmState' = [rmState EXCEPT ![r] = "aborted"]
  /\ UNCHANGED <<tmState, tmPrepared, msgs>>

The state diagram shown in the transaction commit clearly shows the "aborted" can be reached from both "working" and "prepared" states. Two Phase commit seems to be similar.

Shouldn't the enabling condition instead be this? :

rmState[r] \in {"working", "prepared"}

I'm only curious if there is something deeper within this. I'll be glad to hear your response.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/9e5128eb-18fb-426b-9185-c0d7f65a47aa%40googlegroups.com.