CONSTANTS
  MaxGen = 4
  Refs <- RefsMerge4
  Segs <- SegsABCD
  KeepLast = 2
  AtomicList = TRUE
  Kind <- KList
  LateStart = TRUE
  MUT = "none"
SPECIFICATION Spec
INVARIANTS TypeOK Healthy NoSpuriousError BoundedRetries