content: --------------------------------------------------------------------------------
  -- 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 = do
    trigger "shutoff" (not ok) [arg maj]
  
    where
    vals     = [ externW8 "tmp_probe_0" two51
               , externW8 "tmp_probe_1" two51
               , externW8 "tmp_probe_2" zero]
    exceed   = map (> 250) vals
    maj      = majority exceed
    checkMaj = aMajority exceed maj
    ok       = alwaysBeen ((maj && checkMaj) ==> extern "cooler" cooler)
  
    two51  = Just $ [251, 251] P.++ repeat (250 :: Word8)
    zero   = Just $ repeat (0 :: Word8)
    cooler = Just $ [True, True] P.++ repeat False
  
  verifySpec :: Verbosity -> IO ()
  verifySpec verb = reify engineMonitor >>= verifyWithOptions defaultVerifierOptions{verbosity = verb}
                                                              mkDefaultCSettings [] "engine"
  --verifySpec _ = interpret 10 engineMonitor
  