|
types
Plant :: schedule : Schedule
alarms : set of Alarm
inv mk_Plant(schedule,alarms) ==
forall a in set alarms &
forall peri in set dom schedule &
QualificationOK(schedule(peri),a.quali);
Schedule = map Period to set of Expert
inv sch ==
forall exs in set rng sch &
exs <> {} and
forall ex1, ex2 in set exs &
ex1 <> ex2 => ex1.expertid <> ex2.expertid;
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(peri,plant) ==
card plant.schedule(peri)
pre peri in set dom plant.schedule;
ExpertIsOnDuty: Expert * Plant -> set of Period
ExpertIsOnDuty(ex,mk_Plant(sch,-)) ==
{peri| peri in set dom sch & ex in set sch(peri)};
ExpertToPage(a:Alarm,peri:Period,plant:Plant) r: Expert
pre peri in set dom plant.schedule and
a in set plant.alarms
post r in set plant.schedule(peri) 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;
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
