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

[tlaplus] Re: UNCHANGED ModuleInstance!Variables

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.


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 <- 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 ----------------------------------



Variables == << a, b >>

ModuleInstance == INSTANCE BadSubmodule WITH submodule_a <- a, submodule_b <- b

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/d42f20f4-c4e8-45d8-98c7-4cb3934d1d3en%40googlegroups.com.