| The instantiated module (called motion) has a constant parameter M and a variable parameter mState. When you declare an instance of that module, you have to specify the substitutions for these parameters by writing INSTANCE motion WITH M <- ..., mState <- ... As a shorthand, you may omit the substitutions when you wish the parameters to be instantiated by symbols of the same name that exist at the place of instantiation. In other words, your declaration boils down to INSTANCE motion WITH M <- M, mState <- mState However, the symbols M and mState have no meaning at the place where this INSTANCE declaration appears, hence the error. From what you have shown, it is not clear to me why you wish to instantiate module motion in module case: the specification given by CInit and CNext doesn't make any use of operators defined in module motion. If you intend to relate the specifications in the two modules, it would perhaps make sense to move the INSTANCE declaration further down in module case, to a point where you actually make use of what module motion defines. Hope this helps, Stephan
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. |