SPECIFICATION Spec
CONSTANTS
  Acceptor <- MCAcceptor
  Value    <- MCValue
  Quorum1   <- MCQuorum1
  Quorum2   <- MCQuorum2
  Ballot   <- MCBallot
  None     =  None

INVARIANT SafeValue TypeOK