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.
Edit: Additional question
When writing specs, should UNCHANGED <<>> condition be applied to all variables which have not been explicitly changed? Should we apply UNCHANGED to all such variables by default or should it be used when UNCHANGED has a strong significance in the context of the definition?