---------------------  MODULE MCSimpleMultiClientServer --------------------
EXTENDS SimpleMultiClientServer, Sequences, FiniteSets

CONSTANT MaxBalance, MaxTransaction

MCRequest == [type : {"deposit", "withdraw"}, amt : 1..MaxTransaction]
             \cup
             [type : {"transfer"}, dest : Client, amt : 1..MaxTransaction]

MCState == [Client -> 0..(MaxBalance+MaxTransaction)]

MCInitialState == [c \in Client |-> 0]

MCNewState(c, req, st) ==  
   CASE req.type = "deposit"  -> [st EXCEPT ![c] = @ + req.amt]
     [] req.type = "withdraw" -> 
          IF req.amt \leq st[c] THEN [st EXCEPT ![c] = @ - req.amt]
                                ELSE st
     [] req.type = "transfer" -> 
          IF req.amt \leq st[c] 
            THEN [st EXCEPT ![c] = @ - req.amt, ![req.dest] = @ + req.amt]
            ELSE st

MCResponseVal(c, req, st) ==  
  [type |-> "response", val |-> IF  \/ req.type = "deposit"  
                                    \/ req.amt \leq st[c] 
                                  THEN "OK"
                                  ELSE "No"]

MCInput == Request
MCRtnVal(v) == v

MCLiveness ==
  \A c \in Client : (cstate[c].ctl = "calling") ~> (cstate[c].ctl = "idle")



MCConstraint == \A c \in Client : sstate[c] \leq MaxBalance

=============================================================================