content: --------------------------------------------------------------------------------
  -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
  --------------------------------------------------------------------------------
  
  {-# LANGUAGE RebindableSyntax #-}
  
  module EngineExample ( engineExample ) where
  
  import Language.Copilot
  import qualified Prelude as P
  --import qualified Copilot.Compile.SBV as S
  
  {- 
    "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
  
  engineExample :: IO ()
  engineExample = interpret 10 engineMonitor
  
  --  reify engineMonitor >>= S.compile (S.Params { S.prefix = Just "engine" })
    
      
  