[tlaplus] Re: Unexpected access to operator through CONSTANT

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:

On Wednesday, September 15, 2021 at 5:59:38 AM UTC-4 leroy.va...@xxxxxxxxx wrote:

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