\* Two environments, a 5-sample ring, refits from 2 samples, a queue of 3.
\* DropMin = MinFit is the corrected design: an inconsistent buffer always
\* drops its older half.  Each such refit halves the buffer, so the mixed
\* refits after an environment change are bounded by 2 for BufMax <= 5.
CONSTANTS
  Envs = {E1, E2}
  Blend = Blend
  NoModel = NoModel
  BufMax = 5
  MinFit = 2
  DropMin = 2
  Q = 3
  MaxBlendRefits = 2

INIT Init
NEXT Next

INVARIANTS
  TypeOK
  NoSuspectShown
  LiveFromQueue
  OutlierRejected
  BoundedBlend

PROPERTIES
  PersistNotSuspect
  LatchHysteresis

CHECK_DEADLOCK FALSE