-- 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)