copilot 2.0.2 → 2.0.3

raw patch · 17 files changed

+855/−1 lines, 17 files

Files

• Examples/AddMult.hs +36/−0
• Examples/Array.hs +47/−0
• Examples/Cast.hs +32/−0
• Examples/ClockExamples.hs +28/−0
• Examples/EngineExample.hs +41/−0
• Examples/Examples.hs +145/−0
• Examples/Examples2.hs +60/−0
• Examples/ExtFuns.hs +56/−0
• Examples/LTLExamples.hs +50/−0
• Examples/Local.hs +44/−0
• Examples/PTLTLExamples.hs +80/−0
• Examples/Random.hs +21/−0
• Examples/RegExpExamples.hs +52/−0
• Examples/StackExamples.hs +39/−0
• Examples/StatExamples.hs +44/−0
• Examples/VotingExamples.hs +63/−0
• copilot.cabal +17/−1

@@ -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+++--------------------------------------------------------------------------------

@@ -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 ++--------------------------------------------------------------------------------

@@ -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

@@ -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

@@ -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" })+  +    

@@ -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}++--------------------------------------------------------------------------------

@@ -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 

@@ -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++--------------------------------------------------------------------------------

@@ -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

@@ -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++--------------------------------------------------------------------------------

@@ -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+

@@ -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)

@@ -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><s1><s2><s3><s4><s5>(<s0>|<s1>|<s2>|<s3>|<s4>|<s5>)+"+       [ ( "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

@@ -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

@@ -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

@@ -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

@@ -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