------------------------  MODULE MCOneClientRegister ------------------------
EXTENDS OneClientRegister

\* Assumptions from Instantiated  module are thrown away.

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

MCOCSTypeInvariant ==  
  /\ 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

MCLiveness ==
  (cstate.ctl = "calling") ~> (cstate.ctl = "idle")
=============================================================================