--------------------------------------------------------------------------------
-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
--------------------------------------------------------------------------------

-- | Example implementing an engine cooling control system.

{-# LANGUAGE RebindableSyntax #-}

module Copilot.Verifier.Examples.ShouldPass.Engine where

import Language.Copilot
import Copilot.Compile.C99
import Copilot.Verifier ( Verbosity, VerifierOptions(..)
                        , defaultVerifierOptions, verifyWithOptions )

import qualified Prelude as P

{- If the majority of the engine temperature probes exeeds 250 degrees, then
 - the cooler is engaged and remains engaged until the majority of the engine
 - temperature probes drop to 250 or below.  Otherwise, trigger an immediate
 - shutdown of the engine.
-}

engineMonitor :: Spec
engineMonitor :: Spec
engineMonitor = do
  String -> Stream Bool -> [Arg] -> Spec
trigger String
"shutoff" (Stream Bool -> Stream Bool
not Stream Bool
ok) [Stream Bool -> Arg
forall a. Typed a => Stream a -> Arg
arg Stream Bool
maj]

  where
  vals :: [Stream Word8]
vals     = [ String -> Maybe [Word8] -> Stream Word8
externW8 String
"tmp_probe_0" Maybe [Word8]
two51
             , String -> Maybe [Word8] -> Stream Word8
externW8 String
"tmp_probe_1" Maybe [Word8]
two51
             , String -> Maybe [Word8] -> Stream Word8
externW8 String
"tmp_probe_2" Maybe [Word8]
zero]
  exceed :: [Stream Bool]
exceed   = (Stream Word8 -> Stream Bool) -> [Stream Word8] -> [Stream Bool]
forall a b. (a -> b) -> [a] -> [b]
map (Stream Word8 -> Stream Word8 -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
> Stream Word8
250) [Stream Word8]
vals
  maj :: Stream Bool
maj      = [Stream Bool] -> Stream Bool
forall a. (Eq a, Typed a) => [Stream a] -> Stream a
majority [Stream Bool]
exceed
  checkMaj :: Stream Bool
checkMaj = [Stream Bool] -> Stream Bool -> Stream Bool
forall a. (Eq a, Typed a) => [Stream a] -> Stream a -> Stream Bool
aMajority [Stream Bool]
exceed Stream Bool
maj
  ok :: Stream Bool
ok       = Stream Bool -> Stream Bool
alwaysBeen ((Stream Bool
maj Stream Bool -> Stream Bool -> Stream Bool
&& Stream Bool
checkMaj) Stream Bool -> Stream Bool -> Stream Bool
==> String -> Maybe [Bool] -> Stream Bool
forall a. Typed a => String -> Maybe [a] -> Stream a
extern String
"cooler" Maybe [Bool]
cooler)

  two51 :: Maybe [Word8]
two51  = [Word8] -> Maybe [Word8]
forall a. a -> Maybe a
Just ([Word8] -> Maybe [Word8]) -> [Word8] -> Maybe [Word8]
forall a b. (a -> b) -> a -> b
$ [Word8
251, Word8
251] [Word8] -> [Word8] -> [Word8]
forall a. [a] -> [a] -> [a]
P.++ Word8 -> [Word8]
forall a. a -> [a]
repeat (Word8
250 :: Word8)
  zero :: Maybe [Word8]
zero   = [Word8] -> Maybe [Word8]
forall a. a -> Maybe a
Just ([Word8] -> Maybe [Word8]) -> [Word8] -> Maybe [Word8]
forall a b. (a -> b) -> a -> b
$ Word8 -> [Word8]
forall a. a -> [a]
repeat (Word8
0 :: Word8)
  cooler :: Maybe [Bool]
cooler = [Bool] -> Maybe [Bool]
forall a. a -> Maybe a
Just ([Bool] -> Maybe [Bool]) -> [Bool] -> Maybe [Bool]
forall a b. (a -> b) -> a -> b
$ [Bool
True, Bool
True] [Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
P.++ Bool -> [Bool]
forall a. a -> [a]
repeat Bool
False

verifySpec :: Verbosity -> IO ()
verifySpec :: Verbosity -> IO ()
verifySpec Verbosity
verb = Spec -> IO Spec
forall a. Spec' a -> IO Spec
reify Spec
engineMonitor IO Spec -> (Spec -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= VerifierOptions -> CSettings -> [String] -> String -> Spec -> IO ()
verifyWithOptions VerifierOptions
defaultVerifierOptions{verbosity = verb}
                                                            CSettings
mkDefaultCSettings [] String
"engine"
--verifySpec _ = interpret 10 engineMonitor