-------------------------- MODULE OneClientRegister ------------------------- 
CONSTANT RegisterVal 

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

State   == RegisterVal

InitialState == CHOOSE v \in RegisterVal : TRUE
	
ResponseVal(req, s) == IF req.type = "read" THEN s
                                            ELSE "OK"
NewState(req, s)    == IF req.type = "read" THEN s
                                            ELSE req.val

VARIABLES iFace, sstate, cstate
INSTANCE OneClientServer
=============================================================================