------------------------------ MODULE MinMax2 ------------------------------
EXTENDS Integers, Sequences

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

IsLeq(i, j) == (j = Infinity) \/ (i =< j)
IsGeq(i, j) == (j = MinusInfinity) \/ (i >= j) 

VARIABLES x, turn, min, max
vars == <<x, turn, min, max>>

Init == (x = "") /\ (turn = "input") /\ (min = Infinity) /\ (max = MinusInfinity)

ChooseNum ==  /\ turn = "input"
              /\ turn' = "output"
              /\ x' \in Int
              /\ UNCHANGED <<min, max>>

Report == /\ 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 "max" ELSE "") \o
                    (IF x = min' THEN "min" ELSE "")
          
Next == ChooseNum \/ Report

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

=============================================================================
\* Modification History
\* Last modified Tue Aug 02 14:36:38 PDT 2016 by lamport
\* Created Mon Aug 01 19:05:04 PDT 2016 by lamport