[tlaplus] Problem with instance substitutions

[Curt Flowers <curtycurt01@xxxxxxxxx>]

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>>
=============================================================================

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.