SPECIFICATION Spec

INVARIANTS
  TypeInvariant
  UniqueOwnerForEveryKey
  DeadPartitionsAreOutsideTree

CONSTANTS
  PartitionIds = {p0, p1, p2, p3, p4}
  Threads = {t0, t1}
  NoThread = NoThread
  KeyCount = 8
  MinPartitionSize = 2
  MaxPartitionSize = 4
  MaxLoad = 8