[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Problem with instance substitutions



What happens if you put the INSTANCE motion line below the CONSTANT C, M line?

On 2/11/19 9:43 PM, Curt Flowers wrote:
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.