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?
You always have to specify what next state of each variable is going to be.
/\ UNCHANGED <<tmState, tmPrepared, msgs>>
is shorthand for
/\ tmState' = tmState
/\ tmPrepared' = tmPrepared
/\ msgs' = msgs
If you comment out UNCHANGED <<...>> part, you get following error.
Successor state is not completely specified by action RMChooseToAbort of the next-state relation. The following variables are not assigned: msgs, tmPrepared, tmState.