Unexpected access to operator through CONSTANT

[leroy.va...@gmail.com]

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

[Andrew Helwer]

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

[Andrew Helwer]

To correct the syntax of the above, actually you omit the placeholders in the substitution statements. So it would be like:

LOCAL INSTANCE ModuleB WITH OpInA <- OpInA

and

MA == INSTANCE ModuleA

LOCAL INSTANCE ModuleB WITH OpInA <- MA!OpInA

Andrew