types

  Plant :: plan   : Plan
           alarms : set of Alarm
  inv mk_Plant(plan,alarms) ==
        forall a in set alarms &
	   forall per in set dom plan &
	     QualificationOK(plan(per),a.quali);
	     
  Plan = map Period to set of Expert
  inv plan == forall exs in set rng plan & exs <> {};

  Period = token;

  Expert :: expertid : ExpertId
            quali    : set of Qualification
  inv ex == ex.quali <> {};

  ExpertId = token;

  Qualification = <Elec> | <Mech> | <Bio> | <Chem>;
	   
  Alarm :: alarmtext : seq of char
           quali     : Qualification

functions

  NumberOfExperts: Period * Plant -> nat
  NumberOfExperts(per,plant) ==
    card plant.plan(per)
  pre per in set dom plant.plan;

  ExpertIsOnDuty: Expert * Plant -> set of Period
  ExpertIsOnDuty(ex,mk_Plant(plan,alarms)) ==
    {per| per in set dom plan & ex in set plan(per)};

  ExpertToPage(a:Alarm,per:Period,plant:Plant) r: Expert
  pre per in set dom plant.plan and
      a in set plant.alarms
  post r in set plant.plan(per) and
       a.quali in set r.quali;

  QualificationOK: set of Expert * Qualification -> bool
  QualificationOK(exs,reqquali) ==
    exists ex in set exs & reqquali in set ex.quali