|
-- A temperature monitor
-- For Chapter 4 (Logic)
types
TempRead = seq of int
inv temp == len temp = 5
functions
-- the last reading in a sample is greater than the first
Rising: TempRead -> bool
Rising(temp) ==
temp(1) < temp(5);
-- there is a reading in excess of 400 degrees
OverLimit: TempRead -> bool
OverLimit(temp) ==
temp(1) > 400 or temp(2) > 400 or
temp(3) > 400 or temp(4) > 400 or
temp(5) > 400;
-- alternative formulation using a quantified expression
OverLimit2: TempRead -> bool
OverLimit2(temp) ==
exists t in seq temp & t > 400;
-- all readings in a sample exceed 400 degrees
ContOverLimit: TempRead -> bool
ContOverLimit(temp) ==
temp(1) > 400 and temp(2) > 400 and
temp(3) > 400 and temp(4) > 400 and
temp(5) > 400;
-- alternative formulation using a quantified expression
ContOverLimit2: TempRead -> bool
ContOverLimit2(temp) ==
forall t in seq temp & t > 400;
-- detecting whether a reactor can be considered safe
Safe: TempRead -> bool
Safe(temp) ==
temp(3) > 400 => temp(5) < 400;
-- detecting whether an alarm should be raised
RaiseAlarm(temp: TempRead) alarm : bool
post not Safe(temp) <=> alarm;
MixQuant: TempRead -> bool
MixQuant(temp) ==
exists min in set {1,...,5} &
forall i in set {1,...,5} &
i <> min =>
temp(i) > temp(min)
¤ Dauer der Verarbeitung: 0.15 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.
|
