SPECIFICATION Spec
CONSTANTS
  MAX_TIME = 20
  INTERVAL = 2
  NUM_MODELS = 2
  BASELINE_LEN = 3
  WARMUP_LEN = 1
  SETTLE_LEN = 1
  GEN_MIN = 2
  GEN_MAX = 4
INVARIANTS
  TypeOK
  MeasuredDisjoint
  InSamplerPeriod
  GenClearOfWarmupSettle
  BaselineHasSample
  GenTwoSamples
CHECK_DEADLOCK FALSE