CONSTANT
  AppendEntriesReply = AppendEntriesReply
  AppendEntriesRequest = AppendEntriesRequest

  LogMerge = LogMerge
  LogNormal = LogNormal
  LogPreMerge = LogPreMerge
  LogRollback = LogRollback

  RegionA = RegionA
  RegionB = RegionB

  RegionMerging = RegionMerging
  RegionNormal = RegionNormal
  RegionTombStone = RegionTombStone

  Region = {RegionA, RegionB}
  LeaderA = 1
  LeaderB = 1
  MaxClientRequests = 2
  QuorumSize = 1
  Store = {1, 2}
  WillPerformRollback = FALSE

SPECIFICATION
  Spec

INVARIANT
  TypeInvariant
  SimpliedRaftInvariant
  RaftMergeInvariant