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 ================================================================================ 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/BB1A0422-3248-4C4A-A92F-4A3F7EB17C1A%40TimLeonard.us. |