CONSTANTS
  MaxGen = 3
  Refs <- RefsMerge
  Segs <- SegsABC
  KeepLast = 1
  AtomicList = TRUE
  Kind <- KList
  LateStart = TRUE
  MUT = "none"
SPECIFICATION Spec
INVARIANTS TypeOK Healthy NoSpuriousError BoundedRetries