--------------------------  MODULE MCMultiClientServer --------------------
EXTENDS MultiClientServer, Sequences, FiniteSets, Naturals

MCRequest == {"gimme", "I_dont_want_it"}

MCResponse == {"its_yours", "error", "got_it"}

MCState == {seq \in UNION {[1..n -> Client] : n \in 0..Cardinality(Client)} :
           \A i,j \in 1..Len(seq) : (i#j) => (seq[i]#seq[j])}

MCInitialState == << >>

MCNewState(c, req, st) ==  
   IF req = "gimme"
     THEN IF \A i \in 1..Len(st) : st[i] # c
            THEN Append(st, c)
            ELSE st
     ELSE IF (st # <<>>) /\ (c = Head(st)) THEN Tail(st)
                                           ELSE st

MCResponseSet(c, req, st) ==  
   IF req = "gimme"
     THEN IF \A i \in 1..Len(st) : st[i] # c
            THEN IF st = << >> THEN {[client |-> c, val |-> "its_yours"]}
                               ELSE {}
            ELSE {[client |-> c, val |-> "error"]}
     ELSE IF (st # <<>>) /\ (c = Head(st))
            THEN {[client |-> c, val |-> "got_it"]}
                   \cup
                 IF Len(st) > 1
                    THEN {[client |-> Head(Tail(st)), val |-> "its_yours"]}
                    ELSE {}
            ELSE {[client |-> c, val |-> "error"]}

MCInput == {<<c, req>> : c \in Client, req \in Request}
MCRtnVal(v) == v

MCSLiveSpec == /\ MCSInit 
               /\ [][MCSNext]_mcsvars 
               /\ \A c \in Client : WF_mcsvars(MCSDo(c) \/ MCSRespond(c))
               /\ \A c \in Client : 
                    WF_mcsvars( /\ sstate # << >>
                                /\ c = Head(sstate)
                                /\ MCSIssueRequest(c, "I_dont_want_it"))

(* The following liveness property doesn't hold, because that 
owns the resource can continually execute "gimme" calls, that return
"error", without ever giving up the resource.  This could cause another
process to starve. *)
MCLiveness ==
  \A c \in Client : (cstate[c].ctl = "calling") ~> (cstate[c].ctl = "idle")
=============================================================================