copilot 0.23 → 0.25

raw patch · 18 files changed

+554/−259 lines, 18 filesdep ~basedep ~directoryPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base, directory

API changes (from Hackage documentation)

Files

• Language/Copilot.hs +9/−7
• Language/Copilot/AdHocC.hs +8/−7
• Language/Copilot/Compiler.hs +15/−10
• Language/Copilot/Core.hs +11/−12
• Language/Copilot/Dispatch.hs +9/−27
• Language/Copilot/Examples/Examples.hs +17/−20
• Language/Copilot/Examples/LTLExamples.hs +46/−33
• Language/Copilot/Examples/PTLTLExamples.hs +55/−9
• Language/Copilot/Interface.hs +21/−9
• Language/Copilot/Interpreter.hs +1/−1
• Language/Copilot/Language.hs +177/−40
• Language/Copilot/Libs/ErrorChks.hs +7/−9
• Language/Copilot/Libs/Indexes.hs +4/−8
• Language/Copilot/Libs/LTL.hs +100/−34
• Language/Copilot/Libs/PTLTL.hs +51/−27
• Language/Copilot/Libs/Statistics.hs +2/−2
• README +15/−0
• copilot.cabal +6/−4

@@ -2,6 +2,7 @@   ( module Language.Copilot.Core   , module Language.Copilot.Analyser   , module Language.Copilot.Interpreter+  -- , module Language.Copilot.Variables   , module Language.Copilot.Help   , module Language.Copilot.AtomToC   , module Language.Copilot.Compiler@@ -9,9 +10,9 @@   -- , module Language.Copilot.Dispatch   , module Language.Copilot.Interface   , module Language.Copilot.Tests.Random-  , module Language.Copilot.Libs.Indexes-  , module Language.Copilot.Libs.LTL-  , module Language.Copilot.Libs.PTLTL+  -- , module Language.Copilot.Libs.Indexes+  -- , module Language.Copilot.Libs.LTL+  -- , module Language.Copilot.Libs.PTLTL   -- , module Language.Copilot.AdHocC   -- , module Language.Copilot.Examples.Examples   -- , module Language.Copilot.Examples.LTLExamples@@ -21,17 +22,18 @@ import Language.Copilot.Core import Language.Copilot.Analyser import Language.Copilot.Interpreter+-- import Language.Copilot.Variables import Language.Copilot.Help import Language.Copilot.AtomToC import Language.Copilot.Compiler import Language.Copilot.Language -- (opsF, opsF2, opsF3) import Language.Copilot.PrettyPrinter() import Language.Copilot.Tests.Random-import Language.Copilot.Dispatch+-- import Language.Copilot.Dispatch import Language.Copilot.Interface-import Language.Copilot.Libs.Indexes-import Language.Copilot.Libs.LTL-import Language.Copilot.Libs.PTLTL+-- import Language.Copilot.Libs.Indexes+-- import Language.Copilot.Libs.LTL+-- import Language.Copilot.Libs.PTLTL -- import Language.Copilot.AdHocC -- import Language.Copilot.Examples.Examples -- import Language.Copilot.Examples.LTLExamples

@@ -16,7 +16,7 @@     cType t ++ " " ++ unwords (intersperse "," vars) ++ ";"  -- | Takes a type and a list of array names and their sizes declares them.-arrDecl :: Type -> [(String,Int)] -> String+arrDecl :: Type -> [(String, Int)] -> String arrDecl t arrs =      cType t ++ " " ++ unwords (intersperse "," mkArrs) ++ ";"   where mkArrs = map (\(a,size) -> a ++ "[" ++ show size ++ "]") arrs@@ -26,16 +26,17 @@ varInit :: Show a => Type -> String -> a -> String varInit t var val = cType t ++ " " ++ var ++ " = " ++ show val ++ ";" --- Show a list with braces {} rather than brackets [].-bracesListShow :: Show a => [a] -> String-bracesListShow ls =-  "{" ++ (foldl (++) "" $ intersperse "," $ map show ls) ++ "}"- -- | Takes a type and an array and initializes it.  It is YOUR responsibility to -- ensure that @vals@ is of type @t@. arrayInit :: Show a => Type -> String -> [a] -> String arrayInit t var vals = -  cType t ++ " " ++ var ++ " = " ++ bracesListShow vals ++ ";"+  cType t ++ " " ++ var ++ "[" ++ show (length vals)+        ++ "] = " ++ bracesListShow ++ ";"+  where +  -- Show a list with braces {} rather than brackets [].+  bracesListShow :: String+  bracesListShow =+    "{" ++ (foldl (++) "" $ intersperse "," $ map show vals) ++ "}"  -- | Declare function prototypes, given a return type, a function name, and a -- | list of argument types.  Use 'Nothing' for a return type of @void@.

@@ -10,7 +10,6 @@ import Data.Maybe import Data.Map as M import Data.List-import Control.Monad (when)  import qualified Language.Atom as A @@ -96,7 +95,7 @@         F3 _ _ s0 s1 s2 -> initExtSamples' s0 $ initExtSamples' s1 $                              initExtSamples' s2 tmpSamples         PVar _ v ph -> -            do  checkVar v +            do  -- checkVar v                  ts <- tmpSamples                 let v' = tmpVarName v ph                     vts = tmpVars ts@@ -109,7 +108,7 @@                             return $ ts {tmpVars = updateSubMap (\_ -> m') vts}                     Just _ -> return ts         PArr _ (arr, idx) ph -> -            do  checkVar arr+            do  --checkVar arr                 ts <- tmpSamples                 let arr' = tmpArrName arr ph (show idx)                     arrts = tmpArrs ts@@ -137,9 +136,10 @@                                      , tmpIdxs = updateSubMap (\_ -> m'') idxts                                      }                   Just _ -> return ts-    where checkVar v = when (normalizeVar v /= v)-                       (error $ "Copilot: external variable " ++ v ++ " is not "-                               ++ "a valid C99 variable.")+    where +    --      checkVar v = when (normalizeVar v /= v)+    --                    (error $ "Copilot: external variable " ++ v ++ " is not "+    --                            ++ "a valid C99 variable.")           initExtSamples' :: Streamable b                           => Spec b -> A.Atom TmpSamples -> A.Atom TmpSamples           initExtSamples' = initExtSamples streams prophArrs outputIndexes@@ -196,8 +196,8 @@         where nextSt' = nextSt streams prophArrs tmpSamples outputIndexes s 0              --- | Find the maximum phase as which an array sampling depends on this stream.--- | Returns zero by default.+-- | Find the maximum phase as which an array sampling depends on this stream by+-- computing it's index in terms of it. Returns zero by default. maxSampleDep :: Var -> StreamableMaps Spec -> Int maxSampleDep v streams =   foldStreamableMaps (\_ -> streamDep) streams 0@@ -281,8 +281,13 @@     getMaximumSamplingPhase :: Var -> Spec a -> Period -> Period      getMaximumSamplingPhase _ spec n =       case spec of-        PVar _ _ p -> max (p + 1) n-        PArr _ _ p -> max (p + 1) n+        PVar _ _ ph -> max (ph + 1) n +        PArr _ (_, Var _) ph -> max (ph + 2) n -- because this may depend on a+                                               -- variable, and if that variable+                                               -- has a prophecy array, it needs+                                               -- an extra phase to update after+                                               -- the index is taken.+        PArr _ _ ph -> max (ph + 1) n         F _ _ s -> getMaximumSamplingPhase "" s n         F2 _ _ s0 s1 -> maximum [n,                 (getMaximumSamplingPhase "" s0 n),

@@ -320,17 +320,17 @@     (Streamable a => Var -> c a -> b -> b) ->      StreamableMaps c -> b -> b foldStreamableMaps f (SM bm i8m i16m i32m i64m w8m w16m w32m w64m fm dm) acc =-    let acc0  = M.foldrWithKey f acc  bm-        acc1  = M.foldrWithKey f acc0 i8m        -        acc2  = M.foldrWithKey f acc1 i16m-        acc3  = M.foldrWithKey f acc2 i32m-        acc4  = M.foldrWithKey f acc3 i64m-        acc5  = M.foldrWithKey f acc4 w8m-        acc6  = M.foldrWithKey f acc5 w16m-        acc7  = M.foldrWithKey f acc6 w32m-        acc8  = M.foldrWithKey f acc7 w64m-        acc9  = M.foldrWithKey f acc8 fm      -        acc10 = M.foldrWithKey f acc9 dm+    let acc0  = M.foldWithKey f acc  bm+        acc1  = M.foldWithKey f acc0 i8m        +        acc2  = M.foldWithKey f acc1 i16m+        acc3  = M.foldWithKey f acc2 i32m+        acc4  = M.foldWithKey f acc3 i64m+        acc5  = M.foldWithKey f acc4 w8m+        acc6  = M.foldWithKey f acc5 w16m+        acc7  = M.foldWithKey f acc6 w32m+        acc8  = M.foldWithKey f acc7 w64m+        acc9  = M.foldWithKey f acc8 fm      +        acc10 = M.foldWithKey f acc9 dm     in acc10  -- XXX only sends Word8s right now@@ -427,7 +427,6 @@                    (M.union i32m i32m') (M.union i64m i64m') (M.union w8m w8m')                     (M.union w16m w16m') (M.union w32m w32m') (M.union w64m w64m')                     (M.union fm fm') (M.union dm dm')-  -- | Get the Copilot variables. getVars :: StreamableMaps Spec -> [Var]

@@ -45,7 +45,8 @@                                  -- we cannot declare them.  Passing in pairs                                  -- containing the name of the array and it's                                  -- size allows them to be declared."-+    , clock :: Maybe A.Clock     -- Use the hardware clock to drive the timing+                                 -- of the program.     }  data BackEnd = Opts AtomToC @@ -95,12 +96,9 @@                         dirName = outputDir opts                     in do                         putStrLn $ "Trying to create the directory " ++ dirName -                                     ++  "(if missing)  ..."+                                     ++  " (if missing)  ..."                         createDirectoryIfMissing False dirName                         checkTriggerVars streams (triggers opts) -                        -- copilotToC streams sends allExts trueInputExts -                        --            (cName opts) (getPeriod opts) (prePostCode opts) -                        --            (triggers opts) isVerbose                         copilotToC streams sends allExts trueInputExts opts isVerbose                         let copy ext = copyFile (cName opts ++ ext)                                          (dirName ++ cName opts ++ ext)@@ -159,10 +157,12 @@                   getPrePostCode cFileName streams allExts (arrDecs opts) trueInputExts p'                 Just (pre, post) -> (pre, post)         atomConfig = A.defaults -            {A.cCode = \_ _ _ -> (preCode, postCode),-            A.cRuleCoverage = False,-            A.cAssert = False,-            A.cStateName = "copilotState" ++ cFileName}+            { A.cCode = \_ _ _ -> (preCode, postCode)+            , A.cRuleCoverage = False+            , A.cAssert = False+            , A.hardwareClock = clock opts+            , A.cStateName = "copilotState" ++ cFileName+            }     in do         putStrLn $ "Compiling Copilot specs to C  ..."         (sched, _, _, _, _) <- A.compile cFileName atomConfig program@@ -170,24 +170,6 @@             then putStrLn $ A.reportSchedule sched             else return ()         putStrLn $ "Generated " ++ cFileName ++ ".c and " ++ cFileName ++ ".h"--- copilotToC streams sends allExts trueInputExts cFileName p prePostC trigs isVerbose =---     let (p', program) = copilotToAtom streams sends p trigs---         (preCode, postCode) = ---             case prePostC of---                 Nothing ->  getPrePostCode cFileName streams allExts trueInputExts p'---                 Just (pre, post) -> (pre, post)---         atomConfig = A.defaults ---             {A.cCode = \_ _ _ -> (preCode, postCode),---             A.cRuleCoverage = False,---             A.cAssert = False,---             A.cStateName = "copilotState" ++ cFileName}---     in do---         putStrLn $ "Compiling Copilot specs to C  ..."---         (sched, _, _, _, _) <- A.compile cFileName atomConfig program---         if isVerbose ---             then putStrLn $ A.reportSchedule sched---             else return ()---         putStrLn $ "Generated " ++ cFileName ++ ".c and " ++ cFileName ++ ".h"  gccCall :: BackEnd -> IO () gccCall backend = 

@@ -21,7 +21,7 @@   "fib" .= [0,1] ++ var "fib" + (drop 1 $ varW64 "fib")   "t"   .= even (var "fib")     where even :: Spec Word64 -> Spec Bool-          even w' = w' `mod` const 2 == const 0+          even w' = w' `mod` 2 == 0  t1 :: Streams t1 = do@@ -71,7 +71,7 @@ engine :: Streams engine = do    "temps" .= [0, 0, 0] ++ extF "temp" 1-   "overTempRise" .= drop 2 (varF "temps") > const 2.3 + var "temps"+   "overTempRise" .= drop 2 (varF "temps") > 2.3 + var "temps"    "trigger" .= (var "overTempRise") ==> (extB "shutoff" 2)   -- To compile: > let (streams, ss) = dist in interface $ compileOpts streams ss "dist"@@ -104,30 +104,27 @@   a .= alg "n" (sub a b)   b .= alg "m" (sub b a)   "ans" .= varW16 a == varW16 b && not (var "init")-  "init" .= [True] ++ const False+  "init" .= [True] ++ false     where sub hi lo = mux (varW16 hi > var lo) (var hi - var lo) (var hi)           alg ext ex = [0] ++ mux (var "init") (extW16 ext 1) ex  testCoercions :: Streams testCoercions = do-    "short" .= ((cast (varW64 "fib"))::(Spec Word8))  -    "long" .= ((cast (varW8 "short"))::(Spec Word32))+    "word" .= [1] ++ (varW8 "word") * (-2)+    "int"  .= 1 + castI16 (varW8 "word")  -testCoercionsInt :: Streams-testCoercionsInt = do-    "counter" .= [0] ++ varW8 "counter" + 1 -    "int" .= ((cast (varW8 "counter"))::(Spec Int8)) +testCoercions2 :: Streams+testCoercions2 = do+    b .= [True] ++ not (var b)+    i .= castI8 (varB b) -testRules :: Streams-testRules = do-    "v1" .= (not (Const True)) || Var "v2" -    "v2" .= [True, False] ++ [True] ++ Var "v3" < extI8 "v4" 5 -    "v3" .= 0 + drop 3 (int8 6) -    "v4" .= always 5 (Var "v1") +testCoercions3 :: Streams+testCoercions3 = do+  x .= [True] ++ not (var x)+  y .= castI32 (varB x) + castI32 (castW8 (varB x))   i8 :: Streams-i8 = do-    v .=  [0, 1] ++ (varI8 v) + 1 +i8 = do v .= [0, 1] ++ (varI8 v) + 1       trap :: Streams trap = do@@ -187,13 +184,13 @@ testArr = do    -- a .= [True] ++ extArrB ("ff", varW16 b) 5 && extArrB ("ff", varW16 b) 1    --       && extArrB ("ff", varW16 b) 2-  -- b .= [7] ++ varW16 b + const 3 + extArrW16 ("gg", varW16 f) 2 +  -- b .= [7] ++ varW16 b + 3 + extArrW16 ("gg", varW16 f) 2    -- b .= [0] ++ extArrW16 ("gg", varW16 b) 4    -- c .= [True] ++ var c   -- d .= varB c -  e .= varW16 g -- + extArrW16 ("gg", varW16 b) 2+  e .= [6,7,8] ++ (constW16 3) -- + extArrW16 ("gg", varW16 b) 2 --  f .= extArrW16 ("gg", varW16 e) 2 + extArrW16 ("gg", varW16 e) 2 -  g .= extArrW16 ("gg", varW16 e) 2 +  g .= (extArrW16 ("gg", varW16 e) 1) == (extArrW16 ("gg", varW16 e) 1)   -- h .= [0] ++ drop 1 (varW16 g)  

@@ -1,10 +1,13 @@ {-# LANGUAGE FlexibleContexts #-} -module Language.Copilot.Examples.LTLExamples () where+module Language.Copilot.Examples.LTLExamples where -import Prelude (replicate, Int)+import Prelude (replicate, Int, replicate)+import qualified Prelude as P  import Language.Copilot+import Language.Copilot.Libs.Indexes+import Language.Copilot.Libs.LTL import Language.Copilot.Variables  ----------------@@ -12,47 +15,57 @@ ----------------  testing, output :: Var-testing = "test"+testing = "testing" output = "output" ---- Can be tested with various values of n.  Use  the interpreter to see the outputs.+-- Can be tested with various values of val.  Use the interpreter to see the+-- outputs.  tSoonest :: Int -> Streams-tSoonest n = do testing .= (replicate (n+2) False) ++ const True-                output .= soonest n (var testing)-           +tSoonest val = do +  testing .= replicate (val+2) False ++ true+  output  .= soonest val (var testing)  tLatest :: Int -> Streams-tLatest n = do testing .= (replicate (n-2) False) ++ const True-               output .= latest n (var testing)-          +tLatest val = do +  testing .= replicate (val-2) False ++ true+  output  .= latest val (var testing) -tAlways :: Int -> Streams-tAlways n = do testing .= (replicate (n+3) True) ++ const False-               output .= always n (varB testing)-          +tAlways :: Int -> Int -> Streams+tAlways i1 i2 = do +  testing .=    (replicate i1 True P.++ [False]) ++ true+  output  `ltl` always i2 (varB testing) -tFuture :: Int -> Streams-tFuture n = do testing .= (replicate (n+3) False) ++ varB a-               a .= [False] ++ not (var a)-               output .= eventually n (varB testing)-          +tNext :: Int -> Streams+tNext i1 = do +  testing .=    (replicate i1 False P.++ [True]) ++ false+  output  `ltl` next (varB testing) -tUntil :: Int -> Streams-tUntil n = do "t1" .= (replicate (n+2) False) ++ varB c-              c .= [True] ++ not (var c)-              "t0" .= const True-              output .= until n (varB "t0") (varB "t1")-          +tFuture :: Int -> Int -> Streams+tFuture i1 i2 = do +  testing .=    (replicate i1 False P.++ [True]) ++ varB testing+  output  `ltl` eventually i2 (varB testing) +tUntil :: Int -> Int -> Int -> Streams+tUntil i1 i2 i3 = do +  "t1"   .=    replicate i1 False ++ true+  "t0"   .=    replicate i2 True ++ false+  output `ltl` until i3 (varB "t0") (varB "t1")+ tRelease0 :: Int -> Streams-tRelease0 n = do output .= release n (const False) (const True)-            +tRelease0 val = output `ltl` release val false true -tRelease1 :: Int -> Streams-tRelease1 n = do "t1" .= (replicate (n+2) True) ++ varB c-                 c .= [False] ++ not (var c)-                 "t0" .= const True-                 output .= release n (varB "t0") (varB "t1")+tRelease1 :: Int -> Int -> Streams+tRelease1 i1 i2 = do +  "t1"   .=    replicate i1 True ++ varB c+  c      .=    [False] ++ not (var c)+  "t0"   .=    true+  output `ltl` release i2 (varB "t0") (varB "t1")           +testRules :: Streams+testRules = do+    "v1" .=    (not true) || Var "v2" +    "v2" .=    [True, False] ++ [True] ++ Var "v3" < extI8 "v4" 5 +    "v3" .=    0 + drop 3 (int8 6) +    "v4" `ltl` always 5 (Var "v1") +

@@ -2,9 +2,12 @@  module Language.Copilot.Examples.PTLTLExamples where -import Prelude ()+import Prelude (($), String, repeat, replicate, IO())+import qualified Prelude as P+import Data.Map (fromList)  import Language.Copilot+import Language.Copilot.Libs.PTLTL import Language.Copilot.Variables  -- Next examples are for testing of the ptLTL library@@ -16,7 +19,7 @@ tprv :: Streams tprv = do   tstdatprv -  c `previous` (varB a) +  c `ptltl` (previous $ varB a)  -- test of alwaysBeen tstdatAB ::  Streams@@ -25,7 +28,7 @@ tAB :: Streams tAB = do    tstdatAB -   f `alwaysBeen` (var d) +   f `ptltl` (alwaysBeen $ var d)  -- test of eventuallyPrev tstdatEP ::  Streams@@ -34,23 +37,66 @@ tEP :: Streams tEP = do     tstdatEP -    h `eventuallyPrev` (varB g) +    h `ptltl` (eventuallyPrev $ varB g)  -- test of since tstdat1Sin :: Streams-tstdat1Sin = "q1" .= [True, True, True, True, True, True, False ] ++ varB "q1"+tstdat1Sin = "q1" .= [False, False, False, False, True] ++ true --varB "q1"  tstdat2Sin :: Streams tstdat2Sin = "q2" .= [False, False, True, False, False, False, False ] ++ varB "q2"                   -tSin :: Streams -tSin = do +tSince :: Streams +tSince = do     tstdat1Sin      tstdat2Sin -    "z1" `since` (varB "q1", varB "q2") +    "z1" `ptltl` (varB "q1" `since` varB "q2")  -- with external variables -- interface $ setE (emptySM {bMap = fromList [("e1", [True,True ..]), ("e2", [False,False ..])]}) $ interpretOpts tSinExt 20 tSinExt :: Streams  tSinExt = do-      "z1" `since` (extB "e1" 2, extB "q2" 3) +  ptltl "z1" $ extB "e1" 2 `since`extB "q2" 3++tSinExt2 :: Streams +tSinExt2 = do+  a .= not (extB "e1" 2)+  b .= constW16 3 > 2+  s `ptltl` ((extB "e2" 2) `since` (var b))+  t `ptltl` (alwaysBeen $ not (varB a))+  e .= extB "e1" 2 ==> varB d+++engineTemp, engineOff, coolerOn, monitor, temp, cooler, off, cnt :: String+engineTemp = "engineTemp"+engineOff  = "engineOff"+coolerOn   = "coolerOn"+monitor    = "trigger"+temp       = "temp"+off        = "off"+cnt        = "cnt"+cooler     = "cooler"++-- "If the engine temperature exeeds 250 degrees, then the engine is shutoff+-- within the next 10 periods, and in the period following the shutoff, the+-- cooler is engaged and remains engaged."+engine :: Streams+engine = do+  temp    `ptltl` alwaysBeen (extW8 engineTemp 1 > 250)+  cnt     .=      [0] ++ mux (varB temp && varW8 cnt < 10) +                             (varW8 cnt + 1)+                             (varW8 cnt)+  off     .=      (varW8 cnt >= 10 ==> extB engineOff 1)+  cooler  `ptltl` (extB coolerOn 1 `since` extB engineOff 1)+  monitor .=      varB off && varB cooler++engineRun :: IO ()+engineRun = +  interpret engine 40 $ +    setE (emptySM { bMap = fromList +                            [ (engineOff, replicate 8 False P.++ repeat True)+                            , (coolerOn, replicate 9 False P.++ repeat True)+                            ]+                  , w8Map = fromList [(engineTemp, [99,100..])]+                  }) baseOpts+

@@ -2,7 +2,7 @@ module Language.Copilot.Interface (           Options(), baseOpts, test, interpret, compile, verify, interface         , help , setS, setE, setC, setO, setP, setI, setPP, setN, setV, setR-        , setDir, setGCC, setTriggers, setArrs,+        , setDir, setGCC, setTriggers, setArrs, setClock,         module Language.Copilot.Dispatch     ) where @@ -11,6 +11,7 @@ import Language.Copilot.Tests.Random import Language.Copilot.Dispatch import Language.Copilot.Help+import qualified Language.Atom as A (Clock)  import Data.Set as Set (fromList, toList) import Data.List ((\\))@@ -26,7 +27,8 @@         optSends :: Sends, -- ^ For distributed monitors.         optExts :: Maybe Vars, -- ^ Assign values to external variables.         optCompile :: Maybe String, -- ^ Set gcc options.-        optPeriod :: Maybe Period, -- ^ Set the period.  If none is given, then the smallest feasible period is computed.+        optPeriod :: Maybe Period, -- ^ Set the period.  If none is given, then+                                   -- the smallest feasible period is computed.         optInterpret :: Bool, -- ^ Interpreting?         optIterations :: Int, -- ^ How many iterations are we simulating for?         optVerbose :: Verbose, -- ^ Verbosity level: OnlyErrors | DefaultVerbose | Verbose.@@ -45,11 +47,13 @@                                         -- per trigger variable.  Triggers fire                                         -- in the same phase (1) that output                                         -- vars are assigned.-        optArrs :: [(String, Int)] -- ^ When generating C programs to test, we-                                   -- don't know how large external arrays are,-                                   -- so we cannot declare them.  Passing in-                                   -- pairs containing the name of the array and-                                   -- it's size allows them to be declared."+        optArrs :: [(String, Int)], -- ^ When generating C programs to test, we+                                    -- don't know how large external arrays are,+                                    -- so we cannot declare them.  Passing in+                                    -- pairs containing the name of the array+                                    -- and it's size allows them to be+                                    -- declared."+        optClock :: Maybe A.Clock  -- ^ Use the hardware clock to drive the timing of the program?     }  baseOpts :: Options@@ -68,7 +72,8 @@         optOutputDir = "./",         optPrePostCode = Nothing,         optTriggers = [],-        optArrs = []+        optArrs = [],+        optClock = Nothing     }  -- Functions for making it easier for configuring copilot in the frequent use cases@@ -125,9 +130,15 @@ setE :: Vars -> Options -> Options setE vs opts = opts {optExts = Just vs} +-- | Set the external arrays. setArrs :: [(String,Int)] -> Options -> Options setArrs ls opts = opts {optArrs = ls} +-- | Sets the hardware clock.  See+-- http://github.com/tomahawkins/atom/blob/master/Language/Atom/Code.hs.+setClock :: A.Clock -> Options -> Options+setClock clk opts = opts {optClock = Just clk}+ -- | Sets the options for the compiler, e.g., -- -- @ setC \"-O2\" ... @@@ -241,7 +252,8 @@                 compiler  = optCompiler opts,                 prePostCode = optPrePostCode opts,                 triggers = optTriggers opts,-                arrDecs = optArrs opts+                arrDecs = optArrs opts,+                clock = optClock opts                     }  help :: IO ()

@@ -18,7 +18,7 @@     Const c -> repeat c     Var v -> getElem v inVs     PVar _ v _ -> getElem v moVs-    PArr _ (v,s') _ -> map (\i -> (getElem v moVs) !! fromIntegral i) +    PArr _ (v,s') _ -> map (\i -> getElem v moVs !! fromIntegral i)                             (interpret inVs moVs s')     Append ls s' -> ls ++ interpret inVs moVs s'     Drop i s' -> drop i $ interpret inVs moVs s'

@@ -16,7 +16,7 @@         -- * Division         Fractional((/)),         mux,-        CastIntTo(..),+--        CastIntTo(..),         -- * The next functions are used only to coerce the type of their argument         bool, int8, int16, int32, int64,         word8, word16, word32, word64, float, double,@@ -29,7 +29,7 @@         -- * Set of operators from which to choose during the generation of random streams         opsF, opsF2, opsF3,         -- * Constructs of the copilot language-        var, const, drop, (++), (.=), (..|), +        var, drop, (++), (.=), (..|),          -- * The next functions are typed variable declarations to help the type-checker.         varB, varI8, varI16, varI32, varI64,         varW8, varW16, varW32, varW64, varF, varD,@@ -39,7 +39,12 @@         sendW8, -- , sendW16, sendW32, sendW64, sendF, sendD         -- * Typed constant declarations.         constB, constI8, constI16, constI32, constI64,-        constW8, constW16, constW32, constW64, constF, constD+        constW8, constW16, constW32, constW64, constF, constD,+        -- * Cast functions (the name tells you what you're casting *into*).+        castI8, castI16, castI32, castI64,+        castW8, castW16, castW32, castW64,+        -- * Constants+        true, false     ) where  import qualified Language.Atom as A@@ -47,8 +52,8 @@ import Data.Word import System.Random import qualified Data.Map as M-import Prelude ( Bool(..), Num(..), Float, Double-               , Fractional(..), fromInteger, zip, Show(..), Integer)+import Prelude ( Bool(..), Num(..), Float, Double, (.), String, error, ($)+               , Fractional(..), fromInteger, zip, Show(..)) import qualified Prelude as P import Control.Monad.Writer @@ -72,9 +77,11 @@ -- argument is used as a default. mod0, div0 :: (Streamable a, A.IntegralE a) => a -> Spec a -> Spec a -> Spec a mod0 d = F2 (\ x0 x1 -> if x1 P.== 0 then x0 `P.div` d -                          else x0 `P.div` x1) (\ e0 e1 -> A.mod0_ e0 e1 d)+                          else x0 `P.div` x1) +            (\ e0 e1 -> A.mod0_ e0 e1 d) div0 d = F2 (\ x0 x1 -> if x1 P.== 0 then x0 `P.mod` d -                          else x0 `P.mod` x1) (\ e0 e1 -> A.div0_ e0 e1 d)+                          else x0 `P.mod` x1) +            (\ e0 e1 -> A.div0_ e0 e1 d)  (<), (<=), (>=), (>) :: (Streamable a, A.OrdE a) => Spec a -> Spec a -> Spec Bool (<) = F2 (P.<) (A.<.)@@ -94,40 +101,166 @@     (\ x y -> (x A.&&. A.not_ y) A.||. (y A.&&. A.not_ x)) (==>) = F2 (\ x y -> y P.|| P.not x) A.imply -class (Streamable a, P.Integral a) => CastIntTo a where-    cast :: (Streamable b, A.IntegralE b) => Spec b -> Spec a+-- | Cast 'a' into 'b'.  We only allow "safe casts" to larger types.+class Streamable a => Castable a where+  cast :: (Streamable b, A.IntegralE b) => Spec a -> Spec b -instance CastIntTo Word8 where-    cast = F (P.fromInteger P.. P.toInteger) (-            A.Retype P.. A.ue P.. (`A.mod_` (256::(A.E Word64))) P.. A.Retype P.. A.ue)-instance CastIntTo Word16 where-    cast = F (P.fromInteger P.. P.toInteger) (-            A.Retype P.. A.ue P.. (`A.mod_` (65536::(A.E Word64))) P.. A.Retype P.. A.ue)-instance CastIntTo Word32 where-    cast = F (P.fromInteger P.. P.toInteger) (-            A.Retype P.. A.ue P.. (`A.mod_` ((2 P.^ (32::Integer))::(A.E Word64))) P.. A.Retype P.. A.ue)-instance CastIntTo Word64 where-    cast = F (P.fromInteger P.. P.toInteger) (A.Retype P.. A.ue)+castErr :: String -> A.Type -> String+castErr toT fromT = "Error: cannot cast type " P.++ show fromT +                    P.++ " into " P.++ toT P.++ ".  Only casts guarnateed \n" +                    P.++ "not to change sign and to larger types are allowed." -instance CastIntTo Int8 where-    cast = F (P.fromInteger P.. P.toInteger) (-            A.Retype P.. A.ue P.. (\x -> ((x P.+ (128::(A.E Word64))) -                                          `A.mod_` 256) P.- 128) P.. A.Retype P.. A.ue)-instance CastIntTo Int16 where-    cast = F (P.fromInteger P.. P.toInteger) (-            A.Retype P.. A.ue P.. (\x -> ((x P.+ ((2 P.^ (15::Integer))::(A.E Word64))) -                                          `A.mod_` (2 P.^ (16::Integer))) P.- (2 P.^ (15::Integer))) -                                      P.. A.Retype P.. A.ue)-instance CastIntTo Int32 where-    cast = F (P.fromInteger P.. P.toInteger) (-            A.Retype P.. A.ue P.. (\x -> ((x P.+ (128::(A.E Word64))) -                                          `A.mod_` 256) P.- 128) P.. A.Retype P.. A.ue)-instance CastIntTo Int64 where-    cast = F (P.fromInteger P.. P.toInteger) (-            A.Retype P.. A.ue P.. (\x -> ((x P.+ (128::(A.E Word64))) -                                          `A.mod_` 256) P.- 128) P.. A.Retype P.. A.ue)+instance Castable Bool where+  cast = F (\b -> if b then 1 else 0)+           (\b -> A.mux b 1 0) +instance Castable Word8 where+  cast = F (P.fromInteger . P.toInteger) +           (A.Retype . A.ue) +instance Castable Word16 where+  cast = F (P.fromInteger . P.toInteger) +           (A.Retype . A.ue)++instance Castable Word32 where+  cast = F (P.fromInteger . P.toInteger) +           (A.Retype . A.ue)++instance Castable Word64 where+  cast = F (P.fromInteger . P.toInteger) +           (A.Retype . A.ue)++instance Castable Int8 where+  cast = F (P.fromInteger . P.toInteger) +           (A.Retype . A.ue)++instance Castable Int16 where+  cast = F (P.fromInteger . P.toInteger) +           (A.Retype . A.ue)++instance Castable Int32 where+  cast = F (P.fromInteger . P.toInteger) +           (A.Retype . A.ue)++instance Castable Int64 where+  cast = F (P.fromInteger . P.toInteger) +           (A.Retype . A.ue)++castW8 :: (Streamable a, Castable a) => Spec a -> Spec Word8+castW8 x = +  case getAtomType x of+    A.Bool   -> cast x+    t        -> error $ castErr "Word8" t++castW16 :: (Streamable a, Castable a) => Spec a -> Spec Word16+castW16 x = +  case getAtomType x of+    A.Bool   -> cast x+    A.Word8  -> cast x+    t        -> error $ castErr "Word16" t++castW32 :: (Streamable a, Castable a) => Spec a -> Spec Word32+castW32 x = +  case getAtomType x of+    A.Bool   -> cast x+    A.Word8  -> cast x+    A.Word16 -> cast x+    t        -> error $ castErr "Word32" t++castW64 :: (Streamable a, Castable a) => Spec a -> Spec Word64+castW64 x = +  case getAtomType x of+    A.Bool   -> cast x+    A.Word8  -> cast x+    A.Word16 -> cast x+    A.Word32 -> cast x+    t        -> error $ castErr "Word64" t++castI8 :: (Streamable a, Castable a) => Spec a -> Spec Int8+castI8 x = +  case getAtomType x of+    A.Bool   -> cast x+    t        -> error $ castErr "Int8" t++castI16 :: (Streamable a, Castable a) => Spec a -> Spec Int16+castI16 x = +  case getAtomType x of+    A.Bool   -> cast x+    A.Int8   -> cast x+    A.Word8  -> cast x+    t        -> error $ castErr "Int16" t++castI32 :: (Streamable a, Castable a) => Spec a -> Spec Int32+castI32 x = +  case getAtomType x of+    A.Bool   -> cast x+    A.Int8  -> cast x+    A.Int16 -> cast x+    A.Word8  -> cast x+    A.Word16  -> cast x+    t        -> error $ castErr "Int32" t++castI64 :: (Streamable a, Castable a) => Spec a -> Spec Int64+castI64 x = +  case getAtomType x of+    A.Bool   -> cast x+    A.Int8  -> cast x+    A.Int16 -> cast x+    A.Int32 -> cast x+    A.Word8  -> cast x+    A.Word16  -> cast x+    A.Word32  -> cast x+    t        -> error $ castErr "Int64" t++-- F (P.fromInteger . P.toInteger) +--             (A.Retype . A.ue . (`A.mod_` (size 16))+--                . A.Retype . A.ue)+++-- instance CastIntTo Word8 where+--     cast = F (P.fromInteger . P.toInteger) +--              (A.Retype . A.ue . (`A.mod_` (size 8))+--                  . A.Retype . A.ue)+-- instance CastIntTo Word16 where+--     cast = F (P.fromInteger . P.toInteger) +--              (A.Retype . A.ue . (`A.mod_` (size 16))+--                  . A.Retype . A.ue)+-- instance CastIntTo Word32 where+--     cast = F (P.fromInteger . P.toInteger) +--              (A.Retype . A.ue . (`A.mod_` (size 32))+--                  . A.Retype . A.ue)+-- instance CastIntTo Word64 where+--     cast = F (P.fromInteger . P.toInteger) +--              (A.Retype . A.ue . (`A.mod_` (size 64))+--                  . A.Retype . A.ue)++-- Ints++-- XXX this is how Robin had casts.  Can't we do it more simply?+-- instance CastIntTo Int8 where+--     cast = F (P.fromInteger . P.toInteger) +--              (A.Retype . A.ue . +--                  (\x -> ((x P.+ sMinOne) `A.mod_` s) P.-  s)+--                    . A.Retype . A.ue)+--       where s = size 8+--             sMinOne = size 7+-- instance CastIntTo Int8 where+--     cast = F (P.fromInteger . P.toInteger) +--              (A.Retype . A.ue . (`A.mod_` (size 7)) +--                    . A.Retype . A.ue)+-- instance CastIntTo Int16 where+--     cast = F (P.fromInteger . P.toInteger) +--              (A.Retype . A.ue . (`A.mod_` (size 15)) +--                    . A.Retype . A.ue)+-- instance CastIntTo Int32 where+--     cast = F (P.fromInteger . P.toInteger) +--              (A.Retype . A.ue . (`A.mod_` (size 31)) +--                    . A.Retype . A.ue)+-- instance CastIntTo Int64 where+--     cast = F (P.fromInteger . P.toInteger) +--              (A.Retype . A.ue . (`A.mod_` (size 63))+--                    . A.Retype . A.ue)+ -- | Beware : both sides are executed, even if the result of one is later discarded mux :: (Streamable a) => Spec Bool -> Spec a -> Spec a -> Spec a mux = F3 (\ b x y -> if b then x else y) A.mux@@ -451,12 +584,16 @@ sendD :: Var -> (Phase, Port) -> Send Double sendD v (ph, port) = Send (v, ph, port) -} --- | A constant stream-const :: Streamable a => a -> Spec a-const x = Const x + constB :: Bool -> Spec Bool constB = Const++true, false :: Spec Bool+true = constB True+false = constB False++-- | Constant streams constI8 :: Int8 -> Spec Int8 constI8 = Const constI16 :: Int16 -> Spec Int16

@@ -2,17 +2,15 @@  module Language.Copilot.Libs.ErrorChks(nOneChk, nPosChk, int16Chk) where -import Prelude (Integral, Int, String, error, ($), show, maxBound, toInteger)-import qualified Prelude as P  import Data.Int (Int16)  import Language.Copilot.Core  chk :: String -> Int -> Spec a -> Int -> Spec a chk name n s m = -  if n P.< m -    then error $ "Value " P.++ show n P.++ " in operator " P.++ name -         P.++ " must be greater than or equal to " P.++ show m P.++ "."+  if n < m +    then error $ "Value " ++ show n ++ " in operator " ++ name +         ++ " must be greater than or equal to " ++ show m ++ "."     else s  nPosChk :: String -> Int -> Spec a -> Spec a@@ -23,8 +21,8 @@  int16Chk :: String -> Int -> Spec a -> Spec a int16Chk name n s = -  if (toInteger n) P.> max-    then error $ "Offset " P.++ show n P.++ " in operator " P.++ name -         P.++ " is larger than the Int16 maxBound, " P.++ show max P.++ "."+  if (toInteger n) > maxVal+    then error $ "Offset " ++ show n ++ " in operator " ++ name +         ++ " is larger than the Int16 maxBound, " ++ show maxVal ++ "."     else s-  where max = toInteger (maxBound::Int16)+  where maxVal = toInteger (maxBound::Int16)

@@ -16,15 +16,15 @@ soonestHlp :: String -> (Spec Bool -> Spec Bool) -> Int -> Spec Bool -> Spec Int16 soonestHlp name f n s = int16Chk name n $ nPosChk name n (buildStr 0)   where buildStr m = -          if m P.> n then const (-1)-             else mux (f $ drop m s) (const $ fI m) (buildStr (m P.+ 1))+          if m P.> n then (-1)+             else mux (f $ drop m s) (fI m) (buildStr (m P.+ 1))         fI = fromIntegral  latestHlp :: String -> (Spec Bool -> Spec Bool) -> Int -> Spec Bool -> Spec Int16 latestHlp name f n s = int16Chk name n $ nPosChk name n (buildStr n)   where buildStr m = -          if m P.< 0 then const (-1)-             else mux (f $ drop m s) (const $ fI m) (buildStr (m P.- 1))+          if m P.< 0 then (-1)+             else mux (f $ drop m s) (fI m) (buildStr (m P.- 1))         fI = fromIntegral  -- | Returns the smallest @m <= n@ such that @drop m s@ is true, and @-1@ if no@@ -46,7 +46,3 @@ -- such @m@ exists.   latestFail :: Int -> Spec Bool -> Spec Int16 latestFail = latestHlp "latest" not---                     -

@@ -1,8 +1,34 @@--- | Bounded Linear Temporal Logic (LTL) operators.+-- XXX test until, release+-- XXX move the engineLTL example+-- XXX fix engine example in ppt slides -module Language.Copilot.Libs.LTL(always, next, eventually, until, release) where+-- | Bounded Linear Temporal Logic (LTL) operators.  For a bound @n@, a property+-- @p@ holds if it holds on the next @n@ transitions (between periods).  If @n+-- == 0@, then the trace includes only the current period.  For example,+-- @+-- always 3 p+-- @+-- holds if @p@ holds at least once every four periods (3 transitions).  +-- +-- Interface: see Examples/LTLExamples.hs You can embed a LTL specification+-- within a Copilot specification using the form:+-- @+--   var `ltl` (operator spec)+-- @+-- where 'var' is the variable you want to assign to the LTL specification+-- you're writing.+--+-- For some properties, stream dependencies may not allow their specification.+-- In particular, you cannot determine the "future" value of an external+-- variable.  In general, the ptLTL library is probaby more useful. -import Prelude (Int, ($))+module Language.Copilot.Libs.LTL+  ( ltl, eventually, next, always, until, release +  ) +  where++import Prelude (Int, ($), String)+import qualified Prelude as P import Data.List (foldl1)  import Language.Copilot.Core@@ -10,47 +36,87 @@ import Language.Copilot.Libs.Indexes import Language.Copilot.Libs.ErrorChks --- | Property @s@ holds for the next @n@ periods.  If @n == 0@, then @s@ holds--- in the current period.  We require @n >= 0@.--- E.g., if @p = always 2 s@, then we have the following relationship between the streams generated:+ltl :: Var -> (Var -> Streams) -> Streams+ltl v f = f v++tmpName :: Var -> String -> Var+tmpName v name = v P.++ "_" P.++ name++-- | Property @s@ holds for the next @n@ periods.  We require @n >= 0@. If @n ==+-- 0@, then @s@ holds in the current period.  E.g., if @p = always 2 s@, then we+-- have the following relationship between the streams generated: -- @--- s => T T T T F F F F ...--- p => T T F F F F F F ...+--      0 1 2 3 4 5 6 7+-- s => T T T F T T T T ...+-- p => T F F F T T ... -- @-always :: Int -> Spec Bool -> Spec Bool-always n s = nPosChk "always" n $ foldl1 (&&) [drop x s | x <- [0..n]]+always :: Int -> Spec Bool -> Var -> Streams+always n s v = do+  v .= (nPosChk "always" n $ foldl1 (&&) [drop x (varB s') | x <- [0..n]])+  s' .= s+  where s' = tmpName v "always" --- | Property @s@ holds at the next period.-next :: Spec Bool -> Spec Bool-next s = drop 1 s+-- | Property @s@ holds at the next period.  For example:+-- @+--           0 1 2 3 4 5 6 7+-- s      => F F F T F F T F ...+-- next s => F F T F F T F ...+-- @+-- Note: s must have sufficient history to drop a value from it.+next :: Spec Bool -> Var -> Streams+next s v = do +  v  .= drop 1 (varB s')+  s' .= s+  where s' = tmpName v "next"  -- | Property @s@ holds at some period in the next @n@ periods.  If @n == 0@,--- then @s@ holds in the current period.  We require @n >= 0@.--- E.g., if @p = eventually 2 s@, then we have the following relationship between the streams generated:+-- then @s@ holds in the current period.  We require @n >= 0@.  E.g., if @p =+-- eventually 2 s@, then we have the following relationship between the streams+-- generated: -- @--- s => F F F F T F T F ...--- p => F F T T T T T T ...+-- s => F F F T F F F T ...+-- p => F T T T F T T T ... -- @-eventually :: Int -> Spec Bool -> Spec Bool-eventually n s = nPosChk "eventually" n $ foldl1 (||) [drop x s | x <- [0..n]] +eventually :: Int -> Spec Bool -> Var -> Streams+eventually n s v = do+  v .= (nPosChk "eventually" n $ foldl1 (||) [drop x (varB s') | x <- [0..n]])+  s' .= s+  where s' = tmpName v "eventually"  -- | @until n s0 s1@ means that @eventually n s1@, and up until at least the -- period before @s1@ holds, @s0@ continuously holds.-until :: Int -> Spec Bool -> Spec Bool -> Spec Bool-until n s0 s1 = -  nPosChk "until" n $    (   (whenS0 < const 0) -- s0 didn't fail within n periods.-                          || (soonest n s1 <= whenS0)) -- s0 failed at some point before n.-                      && eventually n s1 -- guarantees that soonest n s1 >= 0-  where whenS0 = soonestFail n s0+until :: Int -> Spec Bool -> Spec Bool -> Var -> Streams+until n s0 s1 v = do+  v'  .= (nPosChk "until" n $ +            (   (whenS0 < 0) -- s0 didn't fail within n periods.+             || (soonest n (varB s1') <= whenS0))) -- s0 failed at some point before n.+  v'' `ltl` eventually n (varB s1') -- guarantees that soonest n s1 >= 0+  v   .= (varB v') && (varB v'')+  s0' .= s0+  s1' .= s1+  where +    s0' = tmpName v "until_0"+    s1' = tmpName v "until_1"+    v''  = tmpName v "until_2"+    v' = tmpName v "until3"+    whenS0 = soonestFail n (varB s0')  -- | @release n s0 s1@ means that either @always n s1@, or @s1@ holds up to and -- including the period at which @s0@ becomes true.-release :: Int -> Spec Bool -> Spec Bool -> Spec Bool-release n s0 s1 = -  nPosChk "release" n $    (whenS1 < const 0) -- s1 never fails-                        || (   (whenS0 >= const 0) -- s0 becomes true at some point-                            && (whenS0 < whenS1)) -- and when s0 becomes true,-                                                  -- is strictly sooner than-                                                  -- whne s1 fails.-  where whenS1 = soonestFail n s1-        whenS0 = soonest n s0+release :: Int -> Spec Bool -> Spec Bool -> Var -> Streams+release n s0 s1 v = do+  v' .= (nPosChk "release" n $ (   (whenS0 >= 0) -- s0 becomes true at some point+                                && (whenS0 < whenS1))) -- and when s0 becomes true,+                                                       -- is strictly sooner than+                                                       -- when s1 fails.+  v'' `ltl` always n (varB s1') -- s1 never fails+  v   .= (varB v') || (varB v'')+  s0' .= s0+  s1' .= s1+  where +    s0' = tmpName v "release0"+    s1' = tmpName v "release1"+    v''  = tmpName v "release2"+    v' = tmpName v "release3"+    whenS1 = soonestFail n (varB s1')+    whenS0 = soonest n (varB s0')

@@ -1,38 +1,62 @@--- | Provides past-time linear-temporal logic (ptLTL operators).  Currently--- won't make unique tmp stream names if you use the same operator twice in one--- stream definition.+-- | Provides past-time linear-temporal logic (ptLTL operators).+-- +-- Interface: see Examples/PTLTLExamples.hs, particularly function tSinExt2 in+-- that file.  You can embed a ptLTL specification within a Copilot+-- specification using the form:+-- @+--   var `ptltl` (operator spec)+-- @+-- where 'var' is the variable you want to assign to the ptLTL specification+-- you're writing. -module Language.Copilot.Libs.PTLTL(previous, alwaysBeen, eventuallyPrev, since) where+module Language.Copilot.Libs.PTLTL +  ( ptltl, since, alwaysBeen, eventuallyPrev, previous ) +  where -import Prelude ()+import Prelude (String, ($)) import qualified Prelude as P  import Language.Copilot.Core import Language.Copilot.Language +tmpName :: Var -> String -> Var+tmpName v name = v P.++ "_" P.++ name++ptltl :: Var -> (Var -> Streams) -> Streams+ptltl v f = f v+ -- | Did @s@ hold in the previous period?-previous :: Var -> Spec Bool -> Streams-previous v s =  do-     v .= [False] ++ s  - --- | Has @s@ always held?-alwaysBeen :: Var -> Spec Bool -> Streams-alwaysBeen v s = do-     tmp .= [True] ++ (var tmp) && s       -     v .= s && varB tmp-  where tmp = "alwaysBeenTmp_" P.++ v+previous :: Spec Bool -> Var -> Streams+previous s v = v .= [False] ++ s  ++-- | Has @s@ always held (up to and including the current state)?+alwaysBeen :: Spec Bool -> Var -> Streams+alwaysBeen s v = do+     tmp .= [True] ++ varB v+     v   .= varB tmp && varB s'+     s'  .= s+  where +    tmp = tmpName v "ab_tmp"+    s'  = tmpName v "ab"      -- | Did @s@ hold at some time in the past (including the current state)?-eventuallyPrev :: Var -> Spec Bool -> Streams-eventuallyPrev v s = do-     tmp .= [False] ++ (var tmp) || s-     v .= s || varB tmp-  where tmp = "eventuallyPrevTmp_" P.++ v---- | Once @s2@ holds, in the following state (period), does @s1@ continuously hold?-since ::  Var -> (Spec Bool, Spec Bool) -> Streams-since v (s1, s2) = do-     tmp .= [False] ++ (s2 || (s1 &&  varB v)) -     v .= varB tmp && s1-  where tmp = "sinceTmp_" P.++ v+eventuallyPrev :: Spec Bool -> Var -> Streams+eventuallyPrev s v = do+     tmp .= [False] ++ (var tmp) || varB s'+     v   .= varB s' || varB tmp+     s'  .= s+  where +    tmp = tmpName v "ep_tmp"+    s'  = tmpName v "ep" +-- | Once @s2@ holds, in the following state (period), does @s1@ continuously hold? +since ::  Spec Bool -> Spec Bool -> Var -> Streams+since s1 s2 v = do+    tmp `ptltl` (eventuallyPrev $ [False] ++ s2) -- has s2 been true at some point?+    v   `ptltl` (alwaysBeen $ varB tmp ==> varB s1')+    s1' .= s1+    s2' .= s2+  where +    tmp  = tmpName v "since_tmp"+    s1'  = tmpName v "since1"+    s2'  = tmpName v "since2"

@@ -5,7 +5,7 @@ module Language.Copilot.Libs.Statistics(max, min, sum, mean) where  import Prelude (Int, ($), foldl1, fromIntegral)-import qualified Prelude as P +--import qualified Prelude as P   import qualified Language.Atom as A @@ -37,7 +37,7 @@ -- for word size @a@ for streams over which computation is peformed. mean :: (Streamable a, Fractional a, A.NumE a) => Int -> Spec a -> Spec a mean n s = -  nOneChk "mean" n $ (sum n s) / (const $ fromIntegral n)+  nOneChk "mean" n $ (sum n s) / (fromIntegral n)  -- majority :: (Streamable a, A.NumE a) => Int -> Spec a -> Spec a -- majority n s =

@@ -35,6 +35,21 @@ ******************************************************************************* Release notes +* Copilot-0.25++  * Added true, false Specs (Spec Bool)+  * Removed generic const -- unneeded, since Spec instantiates Num.+  * Change casting to only allow casts that (1) are guaranteed not to change the+    sign and (2) are to a larger type.+  * Removed libs from Copilot.hs.  You must import these explicitly.+  * Fixed buts with LTL and ptLTL libraries and examples and added documentation.++* Copilot-0.24++  * Fixed a bug in external array analysis for computing the minimum period+    size.+  * Added the ability to specify a HW clock for Atom.+ * Copilot-0.23    * All -Wall warnings removed (from importing Copilot.hs).

@@ -1,5 +1,5 @@ name:                copilot-version:             0.23+version:             0.25 cabal-version:       >= 1.2 license:             BSD3 license-file:        LICENSE@@ -31,13 +31,15 @@  library     ghc-options:     -Wall-    build-depends:     base > 4 && < 5+    -- These build depends represent my current system.  This will probably+    -- build on packages outside these constaints.+    build-depends:     base > 4 && < 6                      , atom >= 1.0.7                      , containers >= 0.2.0.1                      , process >= 1.0.0.0                      , random >= 1.0.0.0-                     , directory-                     , mtl >= 1.0.0.0                   +                     , directory >= 1.0.0.0+                     , mtl >= 1.0.0.0                      , filepath >= 1.0.0.0      extensions: