Re: Problem with instance substitutions

[davidis...@xxxxxxxxx]

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.

Thanks in advance .  david streader


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