CONSTANTS
  MaxBalance = 2
  MaxTransaction = 1
  Client = {c1,c2}
  Request <- MCRequest
  State  <- MCState
  InitialState <- MCInitialState 
  NewState <- MCNewState 
  ResponseVal <- MCResponseVal  
\*  Input <- MCInput
  RtnVal <- MCRtnVal

SPECIFICATION SMCSpec
INVARIANTS SMCTypeInvariant 
PROPERTY MCLiveness

CONSTRAINT MCConstraint