CONSTANTS  MaxBalance = 3
           MaxTransaction = 2
           Client = {c1,c2}
           State <- MCState
           Request <- MCRequest

SPECIFICATION SMCSpec
INVARIANTS SMCTypeInvariant 
\* PROPERTY MCLiveness
CONSTRAINT MCConstraint