------------------------- MODULE MultiClientServer  ------------------------- 
EXTENDS Naturals, Sequences

Remove(i, q) == [k \in 1..(Len(q)-1) |-> IF k < i THEN q[k] ELSE q[k+1]]
  (*************************************************************************)
  (* Equals sequence q, except with the element number i removed (assuming *)
  (* i is in 1..Len(q)).                                                   *)
  (*************************************************************************)
  
CONSTANTS Client, Request, State, InitialState, NewState(_, _, _,_), 
          ResponseVal(_, _, _,_), RequestEnabled(_, _, _, _)

Response  == {ResponseVal(c, v, s, q) : 
                c \in Client, v \in Request, s \in State,
                q \in Seq(Client \X Request)}
  
ASSUME /\ InitialState \in State
       /\ \A c \in Client, v \in Request, s \in State :
           /\ \A q \in Seq(Client \X Request) :
                 /\ RequestEnabled(c, v, s, q) \in {TRUE, FALSE}
                 /\ RequestEnabled(c, v, s, q) => NewState(c, v, s, q) \in State
-----------------------------------------------------------------------------
VARIABLES sstate, cstate, pendingQ, iFace

INSTANCE CSCallReturn WITH Input  <- Client \X Request,
                           Output <- Client \X Response

MCSInit == /\ sstate = InitialState
           /\ \E v \in Response :
                 cstate = [c \in Client |-> [ctl |-> "idle", val |-> v]]
           /\ pendingQ = << >>
           /\ CRInit

MCSTypeInvariant ==  
  /\ sstate \in State
  /\ cstate \in [Client -> [ctl : {"idle", "calling", "pending", "returning"},
                            val : Request \cup Response]]
  /\ \A c \in Client :
       /\ (cstate[c].ctl \in {"calling", "pending"}) => 
              (cstate[c].val \in Request)
       /\ (cstate[c].ctl \in {"returning", "idle"}) => 
              (cstate[c].val \in Response)
  /\ pendingQ \in Seq(Client \X Request)
  /\ \A i \in 1..Len(pendingQ) :
       /\ cstate[pendingQ[i][1]].ctl = "pending"
       /\ cstate[pendingQ[i][1]].val = pendingQ[i][2]
  /\ CRTypeOK
-----------------------------------------------------------------------------
MCSIssueRequest(c, req) ==
  /\ cstate[c].ctl = "idle"
  /\ Call(<<c, req>>)
  /\ cstate' = [cstate EXCEPT ![c] = [ctl |-> "calling", val |-> req]]
  /\ UNCHANGED <<sstate, pendingQ>>

MCSEnqueue(c) ==
  /\ cstate[c].ctl = "calling"
  /\ cstate' = [cstate EXCEPT ![c].ctl = "pending"]
  /\ pendingQ' = Append(pendingQ, <<c, cstate[c].val>>)
  /\ UNCHANGED <<sstate, iFace>>

MCSDo(c) ==
  /\ cstate[c].ctl = "pending"
  /\ RequestEnabled(c, cstate[c].val, sstate, pendingQ)
  /\ sstate' = NewState(c, cstate[c].val, sstate, pendingQ)
  /\ cstate' = [cstate EXCEPT 
                  ![c]= [ctl |-> "returning",
                         val |-> ResponseVal(c, cstate[c].val, sstate,
                                             pendingQ)]]
  /\ pendingQ' = Remove(CHOOSE i \in 1..Len(pendingQ) : pendingQ[i][1] = c, 
                        pendingQ)
  /\ UNCHANGED iFace

MCSRespond(c) == 
  /\ cstate[c].ctl = "returning"
  /\ Return(<<c, cstate[c].val>>)
  /\ cstate' = [cstate EXCEPT ![c].ctl = "idle"]
  /\ UNCHANGED <<sstate, pendingQ>>

MCSNext == \E c \in Client : \/ \E req \in Request : MCSIssueRequest(c, req)
                             \/ MCSEnqueue(c)
                             \/ MCSDo(c)
                             \/ MCSRespond(c)

mcsvars == <<cstate, sstate, pendingQ, iFace>>

MCSSpec == /\ MCSInit 
           /\ [][MCSNext]_mcsvars 
           /\ \A c \in Client : 
                  WF_mcsvars(MCSEnqueue(c) \/ MCSDo(c) \/ MCSRespond(c))
===========================================================================