SPECIFICATION Spec

CONSTANTS
  Versions = {1, 2}
  MaxRestarts = 3

INVARIANTS
  TypeOK
  ReportedVersionIsServing
  ReportedIsCommitted

PROPERTIES
  ServedAfterReport
  NoServeWhileNotServing

CHECK_DEADLOCK TRUE