------------------------------ MODULE MinMax1 ------------------------------
EXTENDS Integers, Sequences

setMax(S) == CHOOSE t \in S : \A s \in S : t >= s
setMin(S) == CHOOSE t \in S : \A s \in S : t =< s

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

Init == (x = "") /\ (turn = "input") /\ (y = {})

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

Report == /\ turn = "output"
          /\ turn' = "input"
          /\ y' = y \cup {x}
          /\ x' = (IF x = setMax(y') THEN "max" ELSE "") \o
                    (IF x = setMin(y') THEN "min" ELSE "")
          
Next == ChooseNum \/ Report

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

Infinity      == CHOOSE n : n \notin Int
MinusInfinity == CHOOSE n : n \notin (Int \cup {Infinity})

M == INSTANCE MinMax2 WITH min <- IF y = {} THEN Infinity      ELSE setMin(y),
                           max <- IF y = {} THEN MinusInfinity ELSE setMax(y)
=============================================================================
\* Modification History
\* Last modified Tue Aug 02 14:41:51 PDT 2016 by lamport
\* Created Mon Aug 01 18:52:32 PDT 2016 by lamport