CONSTANTS
  RegisterVal = {v1, v2, v3, v4}
  Request <- MCRequest
  State  <- MCState
  InitialState <- MCInitialState 
  NewState <- MCNewState 
  ResponseVal <- MCResponseVal  
  Input <- MCInput
  RtnVal <- MCRtnVal
  OK = OK

SPECIFICATION OCSSpec
INVARIANTS OCSTypeInvariant 
PROPERTY MCLiveness