# Re: Problem with instance substitutions

Many thanks this discussion has been very helpful.

I am trying to understand modularisation in TLA+ prior to teaching it this semester. The restriction of not using parameterised instantiation  I take to mean not using
INSTANCE ...  WITH ... As I had a problem with this myself I was looking for good styles of specification that were modular but avoided this.  Looking at tla example from "Auxiliary variable in TLA+"  I see that INSTANCE ...  WITH ...  worked. Just for practice I amended the first simple MaxMin example. First I introduced a new module Defs  to put all the definitions and imported it with EXTENDS.  Worked fine. Next I moved the  INSTANCE ...  WITH ... from MaxMin1 to MaxMinH along with other simple adjustments still worked fine.

code
------------------------------ MODULE MinMax2H -----------------------------
EXTENDS Integers, Defs
CONSTANTS Lo, Hi, Both, None
VARIABLE  x, turn, h  \* variables x and turn needed for implicit instantion in MinMax2 MinMax1

M2 == INSTANCE MinMax2
WITH min <- IF h = {} THEN Infinity      ELSE setMin(h),
max <- IF h = {} THEN MinusInfinity ELSE setMax(h)

M1 == INSTANCE MinMax1 WITH y <- h

varsH == <<M1!vars, h>>
InitH == M1!Init /\ (h = {})

InputNumH ==  /\ M1!InputNum
/\ h' = h

RespondH == /\ M1!Respond
/\ h' = h \cup {x}

NextH == InputNumH \/ RespondH

SpecH == InitH /\ [][NextH]_varsH
-----------------------------------------------------------------------------

Now the two submodules MaxMin1 and MaxMin2 are very similar . (see at end)

My problem is when I changed the four occurrences of "M1!" to "M2!"  in MaxMinH . TLC failed with

"In evaluation, the identifier h is either undefined or not an operator.
line 15, col 24 to line 15, col 24 of module MinMax2H"

I can see no reason for the failure  is it right to assume that this is caused by the TLC bug or have I made some other blunder.

------------------------------- MODULE MinMax1 ------------------------------
EXTENDS Integers, Defs

CONSTANTS Lo, Hi, Both, None
ASSUME {Lo, Hi, Both, None} \cap Int = { }

VARIABLES x, turn, y
vars == <<x, turn, y>>

Init ==  /\ x = None
/\ turn = "input"
/\ y = {}

InputNum ==  /\ turn = "input"
/\ turn' = "output"
/\ x' \in Int
/\ y' = y

Respond == /\ turn = "output"
/\ turn' = "input"
/\ y' = y \cup {x}
/\ x' = IF x = setMax(y') THEN IF x = setMin(y') THEN Both ELSE Hi
ELSE IF x = setMin(y') THEN Lo   ELSE None

Next == InputNum \/ Respond

Spec == Init /\ [][Next]_vars
=============================================================================

------------------------------ MODULE MinMax2 -------------------------------
EXTENDS Integers, Sequences, Defs

CONSTANTS Lo, Hi, Both, None
ASSUME {Lo, Hi, Both, None} \cap Int = { }

VARIABLES x, turn, min, max
vars == <<x, turn, min, max>>

Init ==  /\ x = None
/\ turn = "input"
/\ min = Infinity
/\ max = MinusInfinity

InputNum ==  /\ turn = "input"
/\ turn' = "output"
/\ x' \in Int
/\ UNCHANGED <<min, max>>

Respond  ==  /\ turn = "output"
/\ turn' = "input"
/\ min' = IF IsLeq(x, min) THEN x ELSE min
/\ max' = IF IsGeq(x, max) THEN x ELSE max
/\ x' = IF x = max' THEN IF x = min' THEN Both ELSE Hi
ELSE IF x = min' THEN Lo   ELSE None

Next == InputNum \/ Respond

Spec == Init /\ [][Next]_vars
=============================================================================