Permalink
Browse files

Moving examples over from sub-packages.

  • Loading branch information...
1 parent d58e4ad commit d63658713f0b197dea0fe11a1b2f514b6a29d2bc @leepike committed Sep 11, 2011
View
@@ -0,0 +1,45 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+-- |
+
+module Main where
+
+import qualified Prelude as P
+import Copilot.Language
+import Copilot.Language.Prelude
+
+--------------------------------------------------------------------------------
+
+addMult :: Spec
+addMult =
+ do
+ let_ "v" summation
+ trigger "f" true [ arg $ mult 5 ]
+
+ where
+
+ summation = nats + nats + nats
+
+ mult :: Int -> Stream Word64
+ mult 0 = var "v"
+ mult i = var "v" * mult (i-1)
+
+ nats :: Stream Word64
+ nats = [0] ++ nats + 1
+
+main :: IO ()
+main =
+ do
+ putStrLn "PrettyPrinter:"
+ putStrLn ""
+ prettyPrint addMult
+ putStrLn ""
+ putStrLn ""
+ putStrLn "Interpreter:"
+ putStrLn ""
+ interpret 100 [] addMult
+
+
+--------------------------------------------------------------------------------
@@ -0,0 +1,31 @@
+-- | Clocks library tests.
+
+module Copilot.Examples.ClockExamples where
+
+
+import Prelude ( ($), putStrLn )
+import qualified Prelude as P
+import Copilot.Language
+import Copilot.Library.Clocks
+import Data.Bool
+import Data.List ( replicate )
+
+
+p = 5 :: Word8
+
+
+clkStream = clk ( period p ) ( phase 0 )
+clk1Stream = clk1 ( period p ) ( phase 0 )
+
+
+clockTest :: Spec
+clockTest = do
+ observer "clk" clkStream
+ observer "clk1" clk1Stream
+
+
+test = do
+ prettyPrint clockTest
+ putStrLn ""
+ putStrLn ""
+ interpret 10 [] clockTest
@@ -0,0 +1,32 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+{-# LANGUAGE RebindableSyntax #-}
+
+module Main where
+
+import Language.Copilot
+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 drops to 250 or below. Otherwise, trigger an immediate shutdown
+ of the engine." -}
+
+engineMonitor :: Spec
+engineMonitor = do
+ trigger "shutoff" (not overHeat) [arg maj]
+ where
+ vals = map externW8 ["tmp_probe_0", "tmp_probe_1", "tmp_probe_2"]
+ exceed = map (< 250) vals
+ maj = majority exceed
+ checkMaj = aMajority exceed maj
+ overHeat = (extern "cooler" || (maj && checkMaj)) `since` not maj
+
+main :: IO ()
+main =
+ reify engineMonitor >>= S.compile (S.Params { S.prefix = Just "engine" })
+
+
View
@@ -0,0 +1,115 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+-- |
+
+{-# LANGUAGE RebindableSyntax #-}
+
+module Main where
+
+import qualified Prelude as P
+import Copilot.Language
+import Copilot.Language.Prelude hiding (even, odd)
+import Copilot.Language.Reify (reify)
+
+--------------------------------------------------------------------------------
+
+--
+-- Some utility functions:
+--
+
+implyStream :: Stream Bool -> Stream Bool -> Stream Bool
+implyStream p q = not p || q
+
+flipflop :: Stream Bool -> Stream Bool
+flipflop x = y
+ where
+ y = [False] ++ if x then not y else y
+
+nats :: Stream Word64
+nats = [0] ++ nats + 1
+
+even :: (P.Integral a, Typed a) => Stream a -> Stream Bool
+even x = x `mod` 2 == 0
+
+odd :: (P.Integral a, Typed a) => Stream a -> Stream Bool
+odd = not . even
+
+counter :: (Num a, Typed a) => Stream Bool -> Stream a
+counter reset = y
+ where
+ zy = [0] ++ y
+ y = if reset then 0 else zy + 1
+
+booleans :: Stream Bool
+booleans = [True, True, False] ++ booleans
+
+fib :: Stream Word64
+fib = [1, 1] ++ fib + drop 1 fib
+
+bitWise :: Stream Word8
+bitWise = ( let a = [ 1, 1, 0 ] ++ a in a )
+ .^.
+ ( let b = [ 0, 1, 1 ] ++ b in b )
+
+sumExterns :: Stream Word64
+sumExterns =
+ let
+ e1 = extern "e1"
+ e2 = extern "e2"
+ in
+ e1 + e2
+
+--------------------------------------------------------------------------------
+
+--
+-- An example of a complete copilot specification.
+--
+
+-- A specification:
+spec :: Spec
+spec =
+ do
+
+ -- A trigger with four arguments:
+ trigger "f" true -- booleans
+ [ arg fib, arg nats, arg sumExterns, arg bitWise ]
+
+ -- A trigger with two arguments:
+ trigger "f" booleans
+ [ arg fib, arg sumExterns ]
+-- [ arg fib, arg nats ]
+
+ -- A trigger with a single argument:
+ trigger "g" (flipflop booleans)
+ [ arg (sumExterns + counter false + 25) ]
+-- [ arg (counter false + 25 :: Stream Int32) ]
+
+ -- A trigger with a single argument (should never fire):
+ trigger "h" (extern "e3" /= fib)
+ [ arg (0 :: Stream Int8) ]
+
+ observer "i" (odd nats)
+
+--- Some infinite lists for simulating external variables:
+e1, e2, e3 :: [Word64]
+e1 = [0..]
+e2 = 5 : 4 : e2
+e3 = [1, 1] P.++ zipWith (+) e3 (P.drop 1 e3)
+
+main :: IO ()
+main =
+ do
+ putStrLn "PrettyPrinter:"
+ putStrLn ""
+ prettyPrint spec
+ putStrLn ""
+ putStrLn ""
+ putStrLn "Interpreter:"
+ putStrLn ""
+ interpret 10 [input "e1" e1, input "e2" e2, input "e3" e3] spec
+ putStrLn ""
+ putStrLn ""
+
+--------------------------------------------------------------------------------
@@ -0,0 +1,57 @@
+module Copilot.Examples.LTLExamples where
+
+
+import qualified Prelude as P
+import Copilot.Language
+import Copilot.Language.Prelude hiding ( until )
+import Copilot.Library.LTL
+
+
+----------------
+-- LTL tests ---
+----------------
+
+testAlways :: Int -> Int -> Stream Bool
+testAlways i1 i2 = let input = replicate i1 P.True P.++ [ False ] ++ true
+ in always i2 input
+
+
+testNext :: Int -> Stream Bool
+testNext i1 = let input = [ False, False, True ] ++ input
+ in next input
+
+
+testFuture :: Int -> Int -> Stream Bool
+testFuture i1 i2 = let input = replicate i1 False P.++ [ True ] ++ false
+ in eventually i2 input
+
+
+testUntil :: Int -> Int -> Int -> Stream Bool
+testUntil i1 i2 i3 =
+ let t0 = replicate i1 True ++ false
+ t1 = replicate ( i2 - 1 ) False P.++ [ True ] ++ false
+ in until i3 t0 t1
+
+
+testRelease :: Int -> Int -> Int -> Stream Bool
+testRelease i1 i2 i3 =
+ let t0 = replicate i1 True ++ false
+ t1 = replicate ( i2 - 1 ) False P.++ [ True ] ++ false
+ in release i3 t1 t0
+
+
+ltlTest :: Spec
+ltlTest = do
+ trigger "testAlways1" true [ arg $ testAlways 0 0 ]
+ trigger "testAlways2" true [ arg $ testAlways 5 1 ]
+ trigger "testNext" true [ arg $ testNext 10 ]
+ trigger "testFuture" true [ arg $ testFuture 9 10 ]
+ trigger "testUntil" true [ arg $ testUntil 5 6 4 ]
+ trigger "testRelease" true [ arg $ testRelease 5 5 4 ]
+
+
+test = do
+ prettyPrint ltlTest
+ putStrLn ""
+ putStrLn ""
+ interpret 20 [] ltlTest
View
@@ -0,0 +1,44 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+-- | Example demonstrating local variables.
+
+module Main where
+
+import qualified Prelude as P
+import Copilot.Language
+import Copilot.Language.Prelude
+
+--------------------------------------------------------------------------------
+
+nats :: Stream Int32
+nats = [0] ++ (1 + nats)
+
+strm :: Stream Int32
+strm =
+ local "x" (nats * nats) $
+ var "x" + var "x"
+
+-- The above code corresponds to
+--
+-- strm :: Stream Int32
+-- strm =
+-- let x = nats * nats
+-- in x + x
+
+spec :: Spec
+spec =
+ do
+ observer "nats" nats
+ observer "strm" strm
+
+--------------------------------------------------------------------------------
+
+main :: IO ()
+main =
+ do
+ interpret 20 [] spec
+ prettyPrint spec
+
+--------------------------------------------------------------------------------
Oops, something went wrong.

0 comments on commit d636587

Please sign in to comment.