I've explored the threads before posting and its good to know that there was an error in the video (though I spend a few hours trying to fix my issue). I'm having a problem with the INSTANCE of my module into another. I read the other thread that mentioned how to do it, but I'm still confused when I read it because of wording.
I have one module called "motion" which had no errors (yay! first successful module... though its very simple). Then I made another module called "case" (below) and I keep getting the following errors:
"Substitution missing for symbol mState declared at line 4, col 10 to line 4, col 15 of module motion and instantiated in module case."
"Substitution missing for symbol M declared at line 2, col 10 to line 2, col 15 of module motion and instantiated in module case."
----------------MODULE case ----------------------
INSTANCE motion \* <- red error line here
CONSTANT C, M \* <- error for M from the "motion" module
VARIABLE cState, mState
CTypeOK ==
cState \in [C -> {"pleadings", "discovery", "trial", "ruling"}]
CInit ==
cState = [c \in C |-> "pleadings"]
Discovery(c) ==
/\ cState[c] = "discovery"
/\ cState' = [cState EXCEPT ![c] = "trial"]
Trial(c) ==
/\ cState[c] = "discovery"
/\ cState' = [cState EXCEPT ![c] = "ruling"]
CNext == \E c \in C:
\/ Discovery(c)
\/ Trial(c)
============================================
Here is the first module in case its needed
------------------------------- MODULE motion -------------------------------
CONSTANT M
VARIABLE mState
MTypeOK ==
mState \in [M -> {"motion", "response", "reply", "surreply", "hearing", "granted", "denied", "ruling"}]
MInit ==
mState = [m \in M |-> "motion"]
MotionResponse(m) ==
/\ mState[m] = "motion"
/\ mState' = [mState EXCEPT ![m] = "response"]
ResponseReply(m) ==
/\ mState[m] = "response"
/\ mState' = [mState EXCEPT ![m] = "reply"]
SurReply(m) ==
/\ mState[m] = "reply"
/\ mState' = [mState EXCEPT ![m] = "surreply"]
Hearing(m) ==
/\ mState[m] \in {"motion", "response", "reply", "surreply"}
/\ mState' = [mState EXCEPT ![m] = "hearing"]
MotionRuling(m) ==
/\ mState[m] \in {"motion", "response", "reply", "surreply", "hearing"}
/\ mState' = [mState EXCEPT ![m] = "ruling"]
MNext == \E m \in M : MotionResponse(m)
\/ ResponseReply(m)
\/ SurReply(m)
\/ Hearing(m)
\/ MotionRuling(m)
\*\/ UNCHANGED <<mState>>
=============================================================================