I believe this is expected behavior. In module Main, the line EXTENDS ModuleA imports all symbols defined in ModuleA into the Main top-level namespace - specifically the constant-level definition OpInA(_). Then when you declare an instance of ModuleB, there is an implicit assignment of ModuleB's CONSTANT OpInA(_) to the existing OpInA(_) in Main's namespace. It is equivalent to writing the following:
LOCAL INSTANCE ModuleB WITH OpInA(_) <- OpInA(_)
You could write the following to make it more explicit:
MA == INSTANCE ModuleA
LOCAL INSTANCE ModuleB WITH OpInA(_) <- MA!OpInA(_)
Andrew
Hi,
I recently ran into some TLA+ where access to an operator in another module was acquired by using `CONSTANT`. It seems that when a module 'Main' extends a module 'A' and 'B', 'B' can gain access to operators in 'A' by declaring them as CONSTANT instead of using EXTENDS or INSTANCE.
I could replicate the setup as follows:
---- MODULE ModuleA ----
OpInA(x) == TRUE
====
---- MODULE ModuleB ----
\* CONSTANT declaration gives access to OpInA through EXTEND in Main
CONSTANT OpInA(_)
OpInB(x) == OpInA(x)
====
---- MODULE Main ----
EXTENDS ModuleA
LOCAL INSTANCE ModuleB
ASSUME OpInB(1)
====
then run Main with an empty config file, which is successful.
I was wondering whether this is expected behavior. If so, it seems something to avoid? I was surprised as I would expect CONSTANT to be used for parameters external to the model and INSTANCE or EXTENDS to gain access to a module's public operators.
Thanks in advance for any insights,
-Leroy