UNCHANGED ModuleInstance!Variables

24 views

Skip to first unread message

Tim Leonard

unread,

Feb 19, 2021, 5:28:18 PM2/19/21

to tlaplus

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

================================================================================

Leslie Lamport

unread,

Feb 19, 2021, 10:55:42 PM2/19/21

to tlaplus

Hi Tim,

This is not a bug; it's an example of why a program can't have a bug if it doesn't have a precise specification. In this case, what is not precisely specified is the rule for when a subformula of an action is recognized by TLC as specifying the value of a variable in the next state. I've been bitten by the problem you describe a few times, but it has never bothered me enough to try to get it fixed. There are more important issues that need fixing, and not enough people to fix them.