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

*From*: Leslie Lamport <tlaplus.ll@xxxxxxxxx>*Date*: Fri, 19 Feb 2021 19:55:42 -0800 (PST)*References*: <BB1A0422-3248-4C4A-A92F-4A3F7EB17C1A@TimLeonard.us>

Hi Tim,

Leslie

On Friday, February 19, 2021 at 2:28:18 PM UTC-8 t...@xxxxxxxxxxxxxx wrote:

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 <- bThe containing module had a bug that I isolated to this line:/\ UNCHANGED ModuleInstance!VariablesBecause 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 TLCVARIABLE a, bVariables == << a, b >>ModuleInstance == INSTANCE BadSubmodule WITH submodule_a <- a, submodule_b <- bTypeOK ==ModuleInstance!TypeOKInit ==ModuleInstance!Init(TRUE, FALSE)Action ="">/\ ModuleInstance!Init(TRUE, FALSE)/\ UNCHANGED ModuleInstance!Variables \* Doesn't mean /\ UNCHANGED << a, b >>Next ==\/ ActionSpec ==/\ Init/\ [][Next]_Variables================================================================================---------------------------- MODULE BadSubmodule -------------------------------VARIABLE submodule_a, submodule_bVariables ==<< submodule_a, submodule_b >>Init(given_a, given_b) ==/\ submodule_a = given_a/\ submodule_b = given_bTypeOK ==/\ 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/d42f20f4-c4e8-45d8-98c7-4cb3934d1d3en%40googlegroups.com.

**References**:**[tlaplus] UNCHANGED ModuleInstance!Variables***From:*Tim Leonard

- Prev by Date:
**[tlaplus] UNCHANGED ModuleInstance!Variables** - Next by Date:
**Re: [tlaplus] Modelling the Philosophers Dining Problem** - Previous by thread:
**[tlaplus] UNCHANGED ModuleInstance!Variables** - Next by thread:
**[tlaplus] Latex Margin** - Index(es):