-------------------------- MODULE OneClientServer  --------------------------
CONSTANTS Request, State, InitialState, ResponseVal(_, _), NewState(_, _)

ASSUME /\ InitialState \in State
       /\ \A v \in Request, s \in State : NewState(v, s) \in State

Response == {ResponseVal(v, s) : v \in Request, s \in State}
-----------------------------------------------------------------------------
VARIABLES sstate, cstate, iFace
        
INSTANCE CSCallReturn WITH Input <- Request, Output <- Response
-----------------------------------------------------------------------------
OCSInit == /\ sstate = InitialState
           /\ \E v \in Response : cstate = [ctl |-> "idle", val |-> v]
           /\ CRInit

OCSTypeInvariant ==  
  /\ sstate \in State
  /\ cstate \in [ctl : {"idle", "calling", "returning"},
                 val : Request \cup Response ]
  /\ (cstate.ctl \in {"calling"}) => (cstate.val \in Request)
  /\ (cstate.ctl \in {"returning", "idle"}) => (cstate.val \in Response)
  /\ CRTypeOK
-----------------------------------------------------------------------------
OCSIssueRequest(req) == /\ cstate.ctl = "idle"
                        /\ Call(req)
                        /\ cstate' = [ctl |-> "calling", val |-> req]
                        /\ UNCHANGED sstate

OCSDo == /\ cstate.ctl = "calling"
         /\ sstate' = NewState(cstate.val, sstate)
         /\ cstate' = [ctl |-> "returning", 
                       val |-> ResponseVal(cstate.val, sstate)]
         /\ UNCHANGED iFace

OCSRespond == /\ cstate.ctl = "returning"
              /\ Return(cstate.val)
              /\ cstate' = [cstate EXCEPT !.ctl = "idle"]
              /\ UNCHANGED sstate

OCSNext == \/ \E req \in Request : OCSIssueRequest(req)
           \/ OCSDo
           \/ OCSRespond

ocsvars == <<cstate, sstate, iFace>>

OCSSpec == /\ OCSInit 
           /\ [][OCSNext]_ocsvars 
           /\ WF_ocsvars(OCSDo \/ OCSRespond)
===========================================================================