--------------------------  MODULE MCOneClientServer --------------------
EXTENDS OneClientServer, Sequences, FiniteSets

CONSTANT RegisterVal

MCRequest == [type : {"read"}] \cup [type : {"write"}, val : RegisterVal]

OK == CHOOSE v : v \notin RegisterVal

MCState == RegisterVal

MCInitialState == CHOOSE v \in RegisterVal : TRUE

MCNewState(req, st) ==  
   IF req.type = "read"
     THEN st
     ELSE req.val

MCResponseVal(req, st) ==  
   IF req.type = "read"
     THEN st
     ELSE OK

MCInput == Request
MCRtnVal(v) == v

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