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

# Re: [tlaplus] Re: Problem with instance substitutions

 Hello,regarding your first question, "parameterized instantiation" refers to INSTANCE declarations of the formM(a,b) == INSTANCE Module WITH <- ... \* the parameters a and b may appear hereBasic "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)) = Infinityand 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 toh = {}which TLC accepts as an assignment to h. In order to work around this problem, you want to write the initial condition in the formInitH == h = {} /\ M2!InitSimilarly, the assignments to the history variable should come first in actions InputNumH and RespondH. See modules below.Regards,Stephan------------------------------ MODULE MinMax2H ------------------------------EXTENDS Integers, DefsCONSTANTS Lo, Hi, Both, NoneVARIABLE  x, turn, h  \* variables x and turn needed for implicit instantion in MinMax2 MinMax1M2 == 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 == <>             InitH == h = {} /\ M2!InitInputNumH ==   /\ h' = h   /\ M2!InputNumRespondH ==   /\ h' = h \cup {x}  /\ M2!RespondNextH == InputNumH \/ RespondHSpecH == InitH /\ [][NextH]_varsH=============================================================================-------------------------------- MODULE Defs --------------------------------EXTENDS IntegersInfinity == CHOOSE n : n \notin IntMinusInfinity == CHOOSE n : n \notin (Int \cup {Infinity})setMax(S) == CHOOSE t \in S : \A s \in S : t \geq ssetMin(S) == CHOOSE t \in S : \A s \in S : t \leq sIsLeq (i,j ) == (j = Infinity) \/ (i \leq j)IsGeq (i,j ) == (j = MinusInfinity) \/ (i \geq j)=============================================================================------------------------------ MODULE MinMax1 ------------------------------EXTENDS Integers, DefsCONSTANTS Lo, Hi, Both, NoneASSUME {Lo, Hi, Both, None} \cap Int = { }VARIABLES x, turn, yvars == <>Init == /\ x = None         /\ turn = "input"         /\ y = {}InputNum == /\ turn = "input"            /\ turn' = "output"            /\ x' \in Int            /\ y' = yRespond == /\ 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 NoneNext == InputNum \/ RespondSpec == Init /\ [][Next]_vars=============================================================================------------------------------ MODULE MinMax2 ------------------------------EXTENDS Integers, DefsCONSTANTS Lo, Hi, Both, NoneASSUME {Lo, Hi, Both, None} \cap Int = { }VARIABLES x, turn, min, maxvars == <>Init == /\ x = None        /\ turn = "input"         /\ min = Infinity         /\ max = MinusInfinityInputNum == /\ turn = "input"            /\ turn' = "output"            /\ x' \in Int            /\ UNCHANGED <>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 NoneNext == InputNum \/ RespondSpec == Init /\ [][Next]_vars=============================================================================On 29 Jan 2019, at 06:01, davidis...@xxxxxxxxx wrote: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, DefsCONSTANTS Lo, Hi, Both, NoneVARIABLE  x, turn, h  \* variables x and turn needed for implicit instantion in MinMax2 MinMax1M2 == 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 == <>             InitH == M1!Init /\ (h = {})InputNumH ==  /\ M1!InputNum              /\ h' = hRespondH == /\ M1!Respond            /\ h' = h \cup {x}NextH == InputNumH \/ RespondHSpecH == 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, DefsCONSTANTS Lo, Hi, Both, NoneASSUME {Lo, Hi, Both, None} \cap Int = { }VARIABLES x, turn, yvars == <>Init ==  /\ x = None         /\ turn = "input"         /\ y = {}InputNum ==  /\ turn = "input"             /\ turn' = "output"             /\ x' \in Int             /\ y' = yRespond == /\ 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 NoneNext == InputNum \/ RespondSpec == Init /\ [][Next]_vars=============================================================================------------------------------ MODULE MinMax2 -------------------------------EXTENDS Integers, Sequences, DefsCONSTANTS Lo, Hi, Both, NoneASSUME {Lo, Hi, Both, None} \cap Int = { }VARIABLES x, turn, min, maxvars == <>Init ==  /\ x = None         /\ turn = "input"         /\ min = Infinity         /\ max = MinusInfinityInputNum ==  /\ turn = "input"             /\ turn' = "output"             /\ x' \in Int             /\ UNCHANGED <>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 NoneNext == InputNum \/ RespondSpec == Init /\ [][Next]_vars=============================================================================-- 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+u...@xxxxxxxxxxxxxxxx.To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.Visit this group at https://groups.google.com/group/tlaplus.For more options, visit https://groups.google.com/d/optout.