| Hello, regarding your first question, "parameterized instantiation" refers to INSTANCE declarations of the form M(a,b) == INSTANCE Module WITH <- ... \* the parameters a and b may appear here Basic "INSTANCE ... WITH ..." works fine. Regarding your question about the error that TLC raises, I got a bit lost in the module names that you indicate, in particular I don't see module "MaxMinH", so I'll just assume that you refer to module MinMax2H that you reproduce (with "M1!" replaced by "M2!"). When evaluating the initial condition InitH and more specifically the conjunct M2!Init, the third conjunct expands to (IF h = {} THEN Infinity ELSE setMin(h)) = Infinity and at that point of evaluation the variable `h' has not yet been initialized. TLC complains because it cannot evaluate the formula. In contrast, the corresponding conjunct for M1!Init expands to h = {} which TLC accepts as an assignment to h. In order to work around this problem, you want to write the initial condition in the form InitH == h = {} /\ M2!Init Similarly, the assignments to the history variable should come first in actions InputNumH and RespondH. See modules below. Regards, Stephan ------------------------------ 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 == <<M2!vars, h>> InitH == h = {} /\ M2!Init InputNumH == /\ h' = h /\ M2!InputNum RespondH == /\ h' = h \cup {x} /\ M2!Respond NextH == InputNumH \/ RespondH SpecH == InitH /\ [][NextH]_varsH ============================================================================= -------------------------------- MODULE Defs -------------------------------- EXTENDS Integers Infinity == CHOOSE n : n \notin Int MinusInfinity == CHOOSE n : n \notin (Int \cup {Infinity}) setMax(S) == CHOOSE t \in S : \A s \in S : t \geq s setMin(S) == CHOOSE t \in S : \A s \in S : t \leq s IsLeq (i,j ) == (j = Infinity) \/ (i \leq j) IsGeq (i,j ) == (j = MinusInfinity) \/ (i \geq j) ============================================================================= ------------------------------ 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, 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 =============================================================================
|