CONSTANTS
  Client = {c1, c2} 
  Request <- MCRequest
  State  <- MCState
  InitialState <- MCInitialState 
  NewState <- MCNewState 
  ResponseSet <- MCResponseSet  
  Input <- MCInput
  RtnVal <- MCRtnVal

SPECIFICATION MCSLiveSpec
INVARIANTS MCSTypeInvariant MCSInvariant 
\* PROPERTY MCLiveness