Re: [tlaplus] Module instantiation semantics

CCC is also imported into M2 as H1!CCC, so the Main _expression_ should resolve to `43 + H!H1!CCC`.

On Tue, Dec 31, 2024, 11:41 AM William Schultz <will62794@xxxxxxxxx> wrote:

Consider the following set of modules:

---- MODULE M3 ----
EXTENDS Sequences, Naturals
CCC == 99
ExprM3 == 43 + CCC
====

---- MODULE M2 ----
H1 == INSTANCE M3
====

---- MODULE Main ----
EXTENDS Naturals
VARIABLE x
H == INSTANCE M2
Init == x = H!H1!ExprM3
Next == x' = x
====

Based on my understanding of instantiation semantics (from Chapter 17 of Specifying Systems, "The Meaning of a Module"), the H == INSTANCE M2 definition in the Main module will import into Main all definitions from M2 but prefixed with H!. This will (transitively) include all definitions from M3 prefixed with H1! (i.e. the definitions from M3 will be prefixed by H!H1!).

So, in Main, the _expression_ H!H1!ExprM3 would then refer, syntactically, to the _expression_

43 + CCC

This seems problematic, though, since CCC is not actually a definition that appears in the context of Main by the basic instantiation rules.

Is there some detail about instantiation semantics I am missing here? Intuitively, it seems as if CCC in the case above should in some sense be evaluated "in the context of" M3 (i.e. where CCC is a well defined _expression_), but I am trying to reconcile this with the basic instantiation rules as I understand them.

--
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 view this discussion visit https://groups.google.com/d/msgid/tlaplus/ed20d2bb-76b3-4d7f-bbd8-d5d7a95129a7n%40googlegroups.com.