[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Unexpected access to operator through CONSTANT

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

--
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/22fae887-1d36-40d7-8a5a-a54d8d1c5c1an%40googlegroups.com.