Skip to content
Fetching contributors…
Cannot retrieve contributors at this time
42 lines (30 sloc) 1.33 KB
--------------------------------------------------------------------------------
-- 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" })
Jump to Line
Something went wrong with that request. Please try again.