diff --git a/Examples/AddMult.hs b/Examples/AddMult.hs new file mode 100644 --- /dev/null +++ b/Examples/AddMult.hs @@ -0,0 +1,36 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2011 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +-- | Another small example. + +module AddMult ( addMult ) where + +import Prelude () +import Copilot.Language +import Copilot.Language.Prelude + +-------------------------------------------------------------------------------- + +spec :: Spec +spec = + trigger "f" true [ arg $ mult 5 ] + + where + mult :: Word64 -> Stream Word64 + mult 0 = 1 + mult i = constant i * mult (i-1) + +addMult :: IO () +addMult = do + putStrLn "PrettyPrinter:" + putStrLn "" + prettyPrint spec + putStrLn "" + putStrLn "" + putStrLn "Interpreter:" + putStrLn "" + interpret 100 spec + + +-------------------------------------------------------------------------------- diff --git a/Examples/Array.hs b/Examples/Array.hs new file mode 100644 --- /dev/null +++ b/Examples/Array.hs @@ -0,0 +1,47 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2011 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +-- | Example in sampling external arrays. + +{-# LANGUAGE RebindableSyntax #-} + +module Array ( array ) where + +import Language.Copilot hiding (cycle) +import Data.List (cycle) +--import qualified Copilot.Compile.C99 as C +import qualified Copilot.Compile.SBV as S + +-------------------------------------------------------------------------------- + +extArr :: Stream Word32 +extArr = externArray "arr1" arrIdx 5 (Just $ repeat [7,8,9,10,11]) + +arrIdx :: Stream Word32 +arrIdx = [0] ++ (arrIdx + 1) `mod` 4 + +arrIdx2 :: Stream Word8 +arrIdx2 = extern "idx2" (Just [0,0..]) + +extArr2 :: Stream Word16 -> Stream Word32 +extArr2 idx = externArray "arr2" idx 4 (Just $ repeat [1,2,3,4]) + +extArr3 :: Stream Word32 +extArr3 = extArr2 (cast $ externW8 "idx3" (Just $ cycle [0,1,2])) + +spec :: Spec +spec = trigger "trigger" true [ arg extArr + , arg (extArr2 (cast arrIdx2)) + , arg extArr3 +-- Throws an exception since the index is too big for the array! +-- , arg (extArr2 5) + ] + +array :: IO () +array = do +-- reify spec >>= C.compile C.defaultParams + interpret 10 spec + reify spec >>= S.compile S.defaultParams + +-------------------------------------------------------------------------------- diff --git a/Examples/Cast.hs b/Examples/Cast.hs new file mode 100644 --- /dev/null +++ b/Examples/Cast.hs @@ -0,0 +1,32 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2011 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +{-# LANGUAGE RebindableSyntax #-} + +-- Examples of casting types. + +module Cast ( castEx ) where + +import Language.Copilot hiding (even, odd) +import Copilot.Compile.C99 + +b :: Stream Bool +b = [True] ++ not b + +i :: Stream Int8 +i = cast b + +x :: Stream Word16 +x = [0] ++ x + 1 + +y :: Stream Int32 +y = 1 + cast x + +spec :: Spec +spec = trigger "trigger" true [arg y, arg i] + +castEx :: IO () +castEx = do + interpret 10 spec + reify spec >>= compile defaultParams diff --git a/Examples/ClockExamples.hs b/Examples/ClockExamples.hs new file mode 100644 --- /dev/null +++ b/Examples/ClockExamples.hs @@ -0,0 +1,28 @@ +-- | Clocks library tests. + +module ClockExamples ( clockExamples ) where + +import Prelude ( putStrLn, IO, Bool ) +import Copilot.Language +import Copilot.Library.Clocks + +p :: Word8 +p = 5 + +clkStream, clk1Stream :: Stream Bool +clkStream = clk ( period p ) ( phase 0 ) +clk1Stream = clk1 ( period p ) ( phase 0 ) + + +clockTest :: Spec +clockTest = do + observer "clk" clkStream + observer "clk1" clk1Stream + + +clockExamples :: IO () +clockExamples = do + prettyPrint clockTest + putStrLn "" + putStrLn "" + interpret 10 clockTest diff --git a/Examples/EngineExample.hs b/Examples/EngineExample.hs new file mode 100644 --- /dev/null +++ b/Examples/EngineExample.hs @@ -0,0 +1,41 @@ +-------------------------------------------------------------------------------- +-- 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" }) + + diff --git a/Examples/Examples.hs b/Examples/Examples.hs new file mode 100644 --- /dev/null +++ b/Examples/Examples.hs @@ -0,0 +1,145 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2011 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +-- | Some Copilot examples. + +{-# LANGUAGE RebindableSyntax #-} + +module Examples ( examples ) where + +import qualified Prelude as P +import Language.Copilot hiding (even, odd) +--import Copilot.Compile.C99 +import qualified Copilot.Tools.CBMC as C + +-------------------------------------------------------------------------------- + +-- +-- Some utility functions: +-- + +{- + +implyStream :: Stream Bool -> Stream Bool -> Stream Bool +implyStream p q = not p || q + + +extEven :: Stream Bool +extEven = externX `mod` 2 == 0 + +oddSpec :: Spec +oddSpec = trigger "f" true [arg (odd nats)] + +prop :: Stream Bool +prop = (x - x') <= 5 && (x - x') <= (-5) + where + x :: Stream Int32 + x = [0] ++ cast externX + x' = drop 1 x + +externX :: Stream Int8 +externX = extern "x" (Just [0..]) + +foo :: Spec +foo = do + let x = cast externX :: Stream Int16 + trigger "trigger" true [arg $ x < 3] + observer "debug_x" x + +-} + +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 ex1 = extern "e1" (Just e1) + ex2 = extern "e2" (Just e2) + in ex1 + ex2 + +--- Some infinite lists for simulating external variables: +e1, e2 :: [Word64] +e1 = [0..] +e2 = 5 : 4 : e2 + +-------------------------------------------------------------------------------- + +-- +-- An example of a complete copilot specification. +-- + +-- A specification: +spec :: Spec +spec = do + + -- A trigger with four arguments: + trigger "e" 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): + let e3 = [1, 1] P.++ zipWith (+) e3 (P.drop 1 e3) + trigger "h" (extern "e3" (Just e3) /= fib) + [ arg (0 :: Stream Int8) ] + + observer "i" (odd nats) + +examples :: IO () +examples = do + putStrLn "PrettyPrinter:" + putStrLn "" + prettyPrint spec + putStrLn "" + putStrLn "" + putStrLn "Interpreter:" + putStrLn "" + interpret 10 spec + -- putStrLn "" + -- putStrLn "" + -- putStrLn "Atom:" + -- reify spec >>= compile defaultParams + putStrLn "Check equivalence:" + putStrLn "" + putStrLn "" + reify spec >>= + C.genCBMC C.defaultParams {C.numIterations = 20} + +-------------------------------------------------------------------------------- diff --git a/Examples/Examples2.hs b/Examples/Examples2.hs new file mode 100644 --- /dev/null +++ b/Examples/Examples2.hs @@ -0,0 +1,60 @@ +module Examples2 ( examples2 ) where + +import Prelude () + +import Copilot.Language.Prelude +import Copilot.Language +import Copilot.Language.Reify (reify) + +import qualified Copilot.Compile.SBV as S + +import Data.List (cycle) + +-------------------------------------------------------------------------------- + +{- +alt2 :: Stream Word64 +alt2 = [0,1,2] ++ alt2 + 1 + +alt3 :: Stream Bool +alt3 = [True,True,False] ++ alt3 + +fib' :: Stream Word64 +fib' = [0, 1] ++ fib' + drop 1 fib + +fib :: Stream Word64 +fib = [0, 1] ++ fib + drop 1 fib + +fibSpec :: Spec +fibSpec = do + trigger "fib_out" true [arg fib] +-} + +nats :: Stream Word64 +nats = [0] ++ nats + 1 + +alt :: Stream Bool +alt = [True] ++ not alt + +logic :: Stream Bool +logic = [True, False] ++ logic || drop 1 logic + +sumExterns :: Stream Word64 +sumExterns = + let + e1 = extern "e1" (Just [0..]) + e2 = extern "e2" (Just $ cycle [2,3,4]) + in + e1 + e2 + e1 + +spec :: Spec +spec = do + trigger "trig1" alt [ arg $ nats < 3 + , arg sumExterns + , arg logic + ] + +examples2 :: IO () +examples2 = do +-- reify fibSpec >>= S.compile S.defaultParams + reify spec >>= S.compile S.defaultParams diff --git a/Examples/ExtFuns.hs b/Examples/ExtFuns.hs new file mode 100644 --- /dev/null +++ b/Examples/ExtFuns.hs @@ -0,0 +1,56 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2011 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +-- | Example in sampling external functions. + +{-# LANGUAGE RebindableSyntax #-} + +module ExtFuns ( extFuns ) where + +import Language.Copilot +--import qualified Copilot.Compile.C99 as C + +-------------------------------------------------------------------------------- + +nats :: Stream Word16 +nats = [0] ++ nats + 1 + +--------------------------------------------------------------------------------- +-- Function func0 and it's environment for interpreting + +func0 :: Stream Word16 +func0 = externFun "func0" [ funArg x, funArg nats ] + (Just $ cast x + nats) + where x = externW8 "x" (Just [0..]) + +--------------------------------------------------------------------------------- +-- Function func0 with another set of args and it's environment for interpreting + +-- func2 :: Stream Word16 +-- func2 = externFun "func0" [ funArg $ constW8 3, funArg $ constW16 4 ] +-- (Just $ constW16 4 + 1) + +--------------------------------------------------------------------------------- + +--------------------------------------------------------------------------------- +-- Function func1 and it's environment for interpreting +func1 :: Stream Bool +func1 = externFun "func1" [] (Just $ [False] ++ not func1) + +--------------------------------------------------------------------------------- + +a :: Stream Word16 +a = func0 + func0 + +spec :: Spec +spec = trigger "trigger" true [ arg func0 + , arg func1 + , arg a ] + +extFuns :: IO () +extFuns = do +-- reify spec >>= C.compile C.defaultParams + interpret 10 spec + +-------------------------------------------------------------------------------- diff --git a/Examples/LTLExamples.hs b/Examples/LTLExamples.hs new file mode 100644 --- /dev/null +++ b/Examples/LTLExamples.hs @@ -0,0 +1,50 @@ +module LTLExamples where + +import qualified Prelude as P +import Copilot.Language +import Copilot.Language.Prelude +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 :: Stream Bool +testNext = 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 ] + trigger "testFuture" true [ arg $ testFuture 12 10 ] + trigger "testUntil" true [ arg $ testUntil 5 6 4 ] + trigger "testRelease" true [ arg $ testRelease 5 5 4 ] + +ltlExamples :: IO () +ltlExamples = do + prettyPrint ltlTest + putStrLn "" + putStrLn "" + interpret 20 ltlTest diff --git a/Examples/Local.hs b/Examples/Local.hs new file mode 100644 --- /dev/null +++ b/Examples/Local.hs @@ -0,0 +1,44 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2011 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +-- | Example demonstrating local variables. + +module Local ( localEx ) where + +import Prelude () +import Copilot.Language +import Copilot.Language.Prelude + +-------------------------------------------------------------------------------- + +nats :: Stream Int32 +nats = [0] ++ (1 + nats) + +strm :: Stream Int32 +strm = + local (nats + 1) $ \nats' -> nats' + nats' + +-- The above code corresponds to +-- +-- strm :: Stream Int32 +-- strm = +-- let x = nats * nats +-- in x + x + +spec :: Spec +spec = do + trigger "strm" true [arg strm] +-- trigger "strm" true [arg $ replStrm 100000] +-- trigger "strm" true [arg $ replStrm_ 100000 10000] + -- observer "nats" nats + -- observer "strm" strm + +-------------------------------------------------------------------------------- + +localEx :: IO () +localEx = do + interpret 20 spec + prettyPrint spec + +-------------------------------------------------------------------------------- diff --git a/Examples/PTLTLExamples.hs b/Examples/PTLTLExamples.hs new file mode 100644 --- /dev/null +++ b/Examples/PTLTLExamples.hs @@ -0,0 +1,80 @@ +-- | The examples are for testing the ptLTL library + +module PTLTLExamples ( ptltlExamples ) where + +import Copilot.Language +import Copilot.Language.Prelude +import Copilot.Library.PTLTL +import Prelude () +import qualified Data.List as L + + +-- | test of previous +previousTestData :: Stream Bool +previousTestData = [ True, False ] ++ previousTestData + +previousTest :: Spec +previousTest = do + observer "previousTest" ( previous previousTestData ) + + +-- | test of alwaysBeen +alwaysBeenTestData :: Stream Bool +alwaysBeenTestData = [ True, True, True, True, True, True, True, False ] + ++ alwaysBeenTestData + +alwaysBeenTest :: Spec +alwaysBeenTest = do + observer "testAlwaysBeen" ( alwaysBeen alwaysBeenTestData ) + + +-- | test of eventuallyPrevious +eventuallyPrevTestData :: Stream Bool +eventuallyPrevTestData = [ False, False, False, False, False, True, False ] + ++ eventuallyPrevTestData + +eventuallyPrevTest :: Spec +eventuallyPrevTest = observer "eventuallyPrevTest" + ( eventuallyPrev eventuallyPrevTestData ) + + +-- | test of since +sinceTestData1 :: Stream Bool +sinceTestData1 = [ False, False, False ] ++ true + +sinceTestData2 :: Stream Bool +sinceTestData2 = [ False, False, True, False, False, False, False ] + ++ sinceTestData2 + +sinceTest :: Spec +sinceTest = observer "sinceTest" + ( sinceTestData1 `since` sinceTestData2 ) + + +-- | test since with external variables +sinceExtTest :: Spec +sinceExtTest = observer "sinceExtTest" + ( extern "e1" (Just e1) `since` extern "e2" (Just e2)) + +-- | external variables +e1, e2 :: [Bool] +e1 = replicate 10 False L.++ repeat True +e2 = replicate 9 False L.++ [ True ] L.++ repeat False + +ptltlExamples :: IO () +ptltlExamples = do + prettyPrint previousTest + interpret 20 previousTest + + prettyPrint alwaysBeenTest + interpret 20 alwaysBeenTest + + prettyPrint eventuallyPrevTest + interpret 20 eventuallyPrevTest + + prettyPrint sinceTest + interpret 20 sinceTest + + prettyPrint sinceExtTest + interpret 20 sinceExtTest + diff --git a/Examples/Random.hs b/Examples/Random.hs new file mode 100644 --- /dev/null +++ b/Examples/Random.hs @@ -0,0 +1,21 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2011 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +-- | Generate a random spec and pretty-print it. + +module Random ( randomEx ) where + +import Copilot.Core.PrettyPrint as P +import Copilot.Core.Random (randomSpec) +import Copilot.Core.Random.Weights (simpleWeights) +import System.Random (newStdGen) + +randomEx :: IO () +randomEx = do + g <- newStdGen + let p = randomSpec 10 simpleWeights g -- have to give a dummy number of rounds + -- to simulate to generate a + -- spec---mostly used for + -- interpreting/QuickCheck testing. + putStrLn (P.prettyPrint p) diff --git a/Examples/RegExpExamples.hs b/Examples/RegExpExamples.hs new file mode 100644 --- /dev/null +++ b/Examples/RegExpExamples.hs @@ -0,0 +1,52 @@ +-- | Regular expression library tests for the +-- copilotRegexp and copilotRegexpB functions + +module RegExpExamples ( regExpExamples ) where + +import qualified Prelude as P +import Copilot.Language +import Copilot.Language.Prelude +import Copilot.Library.RegExp +import Copilot.Library.Utils + +reset :: Stream Bool +reset = [ False ] ++ cycle [ False, False, False, True ] + + +-- | Regular expression matching on integral streams +s :: Stream Int8 +s = extern "e" (Just $ P.cycle [ 0, 1 ]) + +test1 :: Stream Bool +test1 = copilotRegexp s "(<0>?<0>?<1>)+|<2>?<3>+" reset + + +-- | Regular expressions over boolean streams + +s0, s1, s2, s3, s4, s5 :: Stream Bool +s0 = [ True, False, False, False, False, False ] ++ s1 +s1 = [ False, True, False, False, False, False ] ++ s2 +s2 = [ False, False, True, False, False, False ] ++ s3 +s3 = [ False, False, False, True, False, False ] ++ s4 +s4 = [ False, False, False, False, True, False ] ++ s5 +s5 = [ False, False, False, False, False, True ] ++ s0 + + +test2 :: Stream Bool +test2 = copilotRegexpB + "(|||||)+" + [ ( "s0", s0 ) + , ( "s1", s1 ) + , ( "s2", s2 ) + , ( "s3", s3 ) + , ( "s4", s4 ) + , ( "s5", s5 ) ] false + +spec :: Spec +spec = do + observer "test1" test1 + observer "test2" test2 + observer "reset" reset + +regExpExamples :: IO () +regExpExamples = interpret 15 spec diff --git a/Examples/StackExamples.hs b/Examples/StackExamples.hs new file mode 100644 --- /dev/null +++ b/Examples/StackExamples.hs @@ -0,0 +1,39 @@ +-- | Stack library tests. + +module StackExamples ( stackExamples ) where + + +import Prelude () +import qualified Prelude as P +import Copilot.Language +import Copilot.Library.Stacks +import Copilot.Language.Prelude + + +-- push a counter from 1 to 5 onto the stack +pushSignal :: Stream Bool +pushSignal = replicate 5 True ++ false + +pushValue :: Stream Word16 +pushValue = [ 1 ] ++ pushValue + 1 + +-- then wait one tick and pop 6 values off the stack again +-- ( leaving the default/start value ) +popSignal :: Stream Bool +popSignal = replicate 6 False P.++ replicate 6 True ++ false + +-- all operations on a stack of depth 5, of type Word16 and with +-- start/default value 0 +stackStream :: Stream Word16 +stackStream = stack (5::Int) 0 popSignal pushSignal pushValue + +stackTest :: Spec +stackTest = + observer "stack" stackStream + +stackExamples :: IO () +stackExamples = do + prettyPrint stackTest + putStrLn "" + putStrLn "" + interpret 15 stackTest diff --git a/Examples/StatExamples.hs b/Examples/StatExamples.hs new file mode 100644 --- /dev/null +++ b/Examples/StatExamples.hs @@ -0,0 +1,44 @@ +module StatExamples ( statExamples ) where + +-- | Statistics examples + +import Prelude () +import Copilot.Language +import Copilot.Language.Prelude +import Copilot.Library.Statistics + + +inputData :: Stream Word16 +inputData = replicate 5 0 ++ inputData + 5 + +inputFData :: Stream Float +inputFData = replicate 5 0 ++ inputFData + 5 + + +minV :: Stream Word16 +minV = min 3 inputData + +maxV :: Stream Word16 +maxV = max 3 inputData + +sumV :: Stream Word16 +sumV = sum 3 inputData + +meanV :: Stream Float +meanV = mean 3 inputFData + + +statisticsTest :: Spec +statisticsTest = do + observer "minV" minV + observer "maxV" maxV + observer "sumV" sumV + observer "meanV" meanV + + +statExamples :: IO () +statExamples = do + prettyPrint statisticsTest + putStrLn "" + putStrLn "" + interpret 20 statisticsTest diff --git a/Examples/VotingExamples.hs b/Examples/VotingExamples.hs new file mode 100644 --- /dev/null +++ b/Examples/VotingExamples.hs @@ -0,0 +1,63 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2011 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +-- | Fault-tolerant voting examples. + +{-# LANGUAGE RebindableSyntax #-} + +module VotingExamples ( votingExamples ) where + +import Copilot.Library.Voting +import Copilot.Language +import Copilot.Language.Prelude + +-------------------------------------------------------------------------------- + +vote :: Spec +vote = do + trigger "maj" true [ arg maj ] + + trigger "aMaj" true + [ arg $ aMajority xs maj ] + + where + + maj = majority xs + xs = concat (replicate 1 ls) + ls = [a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z] + + a = [0] ++ a + 1 :: Stream Word32 + b = [0] ++ b + 1 + c = [0] ++ c + 1 + d = [0] ++ d + 1 + e = [1] ++ e + 1 + f = [1] ++ f + 1 + g = [1] ++ g + 1 + h = [1] ++ h + 1 + i = [1] ++ i + 1 + j = [1] ++ j + 1 + k = [1] ++ k + 1 + l = [1] ++ l + 1 + m = [1] ++ m + 1 + n = [1] ++ n + 1 + o = [1] ++ o + 1 + p = [1] ++ p + 1 + q = [1] ++ q + 1 + r = [1] ++ r + 1 + s = [1] ++ s + 1 + t = [1] ++ t + 1 + u = [1] ++ u + 1 + v = [1] ++ v + 1 + w = [1] ++ w + 1 + x = [1] ++ x + 1 + y = [1] ++ y + 1 + z = [1] ++ z + 1 + +-------------------------------------------------------------------------------- + +votingExamples :: IO () +votingExamples = + do + interpret 20 vote +-- prettyPrint vote diff --git a/copilot.cabal b/copilot.cabal --- a/copilot.cabal +++ b/copilot.cabal @@ -1,5 +1,5 @@ name: copilot -version: 2.0.2 +version: 2.0.3 cabal-version: >= 1.10 license: BSD3 license-file: LICENSE @@ -50,3 +50,19 @@ , copilot-c99 >= 0.2 , directory >= 1.1 , random + other-modules: AddMult + , Array + , Cast + , ClockExamples + , EngineExample + , Examples + , Examples2 + , ExtFuns + , Local + , LTLExamples + , PTLTLExamples + , Random + , RegExpExamples + , StackExamples + , StatExamples + , VotingExamples