CONSTANTS N      = 3
          MaxNum = 7
CONSTRAINT MCConstraint
SPECIFICATION SBSpec
PROPERTY Bar_MEStarvationFree
INVARIANT SBTypeOK SBInductiveInvariant