[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] Unexpected access to operator through CONSTANT
- From: "leroy.va...@xxxxxxxxx" <leroy.vanengelen@xxxxxxxxx>
- Date: Wed, 15 Sep 2021 02:59:38 -0700 (PDT)
- Ironport-hdrordr: A9a23:Vk40xq2mJjNf37JnVT7aPgqjBJckLtp133Aq2lEZdPWaSL3gqymLppUmPHjP6Ar5OUtQ+uxoV5PwJE80maQFh7X5Xo3NYOCZghrTEGgK1+KLrlGOJ8SZzJ8n6U4KSdkYNDSfNykDse/KpCG0D9JI+qjizEnRv5a9815dCT1PL4tk7wt/F0KyH0BsLTMsb6YEKA==
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/22fae887-1d36-40d7-8a5a-a54d8d1c5c1an%40googlegroups.com.