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

Re: [tlaplus] Problem with instance substitutions



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


On 12 Feb 2019, at 05:40, Curt Flowers <curtycurt01@xxxxxxxxx> wrote:

 The M doesn't have an error, but that would be because the spec now believes M to be a CONSTANT in the spec. But the same error occurs with INSTANCE, just with a new line number and only complaining about "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.

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