types

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

  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.schedule(per)
  pre per in set dom plant.schedule;

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

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

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