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.