[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[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:
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(_)
On Wednesday, September 15, 2021 at 5:59:38 AM UTC-4 leroy.va...@xxxxxxxxx wrote:
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
OpInB(x) == OpInA(x)
---- MODULE Main ----
LOCAL INSTANCE ModuleB
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,
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 on the web visit https://groups.google.com/d/msgid/tlaplus/645bff10-811f-4115-8b3d-e4e34f003f45n%40googlegroups.com.