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

*From*: davidis...@xxxxxxxxx*Date*: Mon, 28 Jan 2019 21:01:22 -0800 (PST)*References*: <CAH4a_VUMA9f5-Nt3iGRDavnpViG-+H468KzYnd356pQxc4sGwQ@mail.gmail.com>

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

**Follow-Ups**:**Re: [tlaplus] Re: Problem with instance substitutions***From:*Stephan Merz

**References**:**Problem with instance substitutions***From:*Bekir Oguz

- Prev by Date:
**Two Questions about (State) Constraints in TLC** - Next by Date:
**Re: [tlaplus] Two Questions about (State) Constraints in TLC** - Previous by thread:
**Re: [tlaplus] Problem with instance substitutions** - Next by thread:
**Re: [tlaplus] Re: Problem with instance substitutions** - Index(es):