This is the complete spec with addition of the in between states suffixed with RDL (Response Deadline). The TLC finds no errors and the reasonable amount of distinct states. As before I've added comments throughout (mainly in the Inv section).
------------------------------- MODULE motion -------------------------------
CONSTANT M
VARIABLE mState, movant, respondent
MTypeOK ==
/\ mState \in [M -> {"motion", "response", "reply", "surreply", "hearing", "granted", "denied", "ruling"}]
/\ movant \in {"idle", "active"}
/\ respondent \in {"idle", "active"}
(* Init State Formula *)
MInit ==
/\ mState = [m \in M |-> "motion"]
/\ movant = "active"
/\ respondent = "idle"
(* motion and intermediate idle states for parties to respond *)
MotionRDL(m) == \* response deadline (RDL). Each party is idle after each state.
/\ mState[m] = "motion"
/\ movant = "active"
/\ respondent = "idle"
/\ movant' = "idle"
/\ UNCHANGED <<respondent, mState>>
MotionResponse(m) ==
/\ mState[m] = "motion"
/\ movant = "idle"
/\ respondent = "idle"
/\ mState' = [mState EXCEPT ![m] = "response"]
/\ respondent' = "active"
/\ UNCHANGED movant
ResponseRDL(m) ==
/\ mState[m] = "response"
/\ respondent = "active"
/\ respondent' = "idle"
/\ UNCHANGED <<mState, movant>>
ResponseReply(m) ==
/\ mState[m] = "response"
/\ movant = "idle"
/\ respondent = "idle"
/\ mState' = [mState EXCEPT ![m] = "reply"]
/\ movant' = "active"
/\ UNCHANGED respondent
ReplyRDL(m) ==
/\ mState[m] = "reply"
/\ movant = "active"
/\ respondent = "idle"
/\ movant' = "idle"
/\ UNCHANGED <<mState, respondent>>
SurReply(m) ==
/\ mState[m] = "reply"
/\ movant = "idle"
/\ respondent = "idle"
/\ mState' = [mState EXCEPT ![m] = "surreply"]
/\ respondent' = "active"
/\ UNCHANGED movant
Hearing(m) ==
/\ mState[m] \in {"motion", "response", "reply", "surreply"}
/\ mState' = [mState EXCEPT ![m] = "hearing"]
/\ movant' = "idle"
/\ respondent' = "idle"
MotionRuling(m) ==
/\ mState[m] \in {"motion", "response", "reply", "surreply", "hearing"}
/\ mState' = [mState EXCEPT ![m] = "ruling"]
/\ movant' = "idle"
/\ respondent' = "idle"
(* Next State Formula *)
MNext == \E m \in M :
\/ MotionRDL(m)
\/ MotionResponse(m)
\/ ResponseRDL(m)
\/ ResponseReply(m)
\/ ReplyRDL(m)
\/ SurReply(m)
\/ Hearing(m)
\/ MotionRuling(m)
-----------------------------------------------------------------------------
(* Checks that movant and respondent are never both in "active" state *)
BothNotActiveInv ==
/\ movant # "idle"
/\ respondent # "idle"
Below OutOfTurnInv and MTypeInv are trying to do the same thing. I just tried to get on aspect working at a time. I tried at least 30 different combination of formulas. I looked for typos (by copying and pasting just to make sure), checked m1, m, M, mState, every state, etc. I basically manually TLC'd this formula to the best my ability. I only had one Inv on at a time while checking also.
OutOfTurnInv ==
/\ \E m \in M: [m |-> "motion"]
/\ respondent # "idle"
MTypeInv ==
\/ /\ \E m \in M : mState[m] = "motion"
/\ ~respondent = "active"
(*\/ /\ \A m \in M : mState[m] \in {"response", "surreply"}
/\ ~movant = "active"
/\ respondent = "active"
\/ /\ \A m \in M: mState[m] \in {"hearing", "ruling"}
/\ ~movant = "active"
/\ respondent # "active"*)
=============================================================================