In one of my specs, I have a module (call it BadSubmodule) that defines:
Variables == << submodule_a, submodule_b >>
I have an enclosing module that instantiates the submodule, substituting its own variables:
ModuleInstance == INSTANCE BadSubmodule WITH submodule_a <- a, submodule_b <- b
The containing module had a bug that I isolated to this line:
/\ UNCHANGED ModuleInstance!Variables
Because of how substitution is defined, I expected that to be equivalent to:
/\ UNCHANGED << a, b >>
but it is not.
Is that a bug, or a misunderstanding on my part?
---------------------------------- MODULE Bad ----------------------------------
EXTENDS TLC
VARIABLE a, b
Variables == << a, b >>
ModuleInstance == INSTANCE BadSubmodule WITH submodule_a <- a, submodule_b <- b
TypeOK ==
ModuleInstance!TypeOK
Init ==
ModuleInstance!Init(TRUE, FALSE)
Action ="">
/\ ModuleInstance!Init(TRUE, FALSE)
/\ UNCHANGED ModuleInstance!Variables \* Doesn't mean /\ UNCHANGED << a, b >>
Next ==
\/ Action
Spec ==
/\ Init
/\ [][Next]_Variables
================================================================================
---------------------------- MODULE BadSubmodule -------------------------------
VARIABLE submodule_a, submodule_b
Variables ==
<< submodule_a, submodule_b >>
Init(given_a, given_b) ==
/\ submodule_a = given_a
/\ submodule_b = given_b
TypeOK ==
/\ submodule_a \in BOOLEAN
/\ submodule_b \in BOOLEAN
================================================================================