diff --git a/Language/Copilot.hs b/Language/Copilot.hs
--- a/Language/Copilot.hs
+++ b/Language/Copilot.hs
@@ -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
diff --git a/Language/Copilot/AdHocC.hs b/Language/Copilot/AdHocC.hs
--- a/Language/Copilot/AdHocC.hs
+++ b/Language/Copilot/AdHocC.hs
@@ -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@.
diff --git a/Language/Copilot/Compiler.hs b/Language/Copilot/Compiler.hs
--- a/Language/Copilot/Compiler.hs
+++ b/Language/Copilot/Compiler.hs
@@ -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),
diff --git a/Language/Copilot/Core.hs b/Language/Copilot/Core.hs
--- a/Language/Copilot/Core.hs
+++ b/Language/Copilot/Core.hs
@@ -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]
diff --git a/Language/Copilot/Dispatch.hs b/Language/Copilot/Dispatch.hs
--- a/Language/Copilot/Dispatch.hs
+++ b/Language/Copilot/Dispatch.hs
@@ -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 = 
diff --git a/Language/Copilot/Examples/Examples.hs b/Language/Copilot/Examples/Examples.hs
--- a/Language/Copilot/Examples/Examples.hs
+++ b/Language/Copilot/Examples/Examples.hs
@@ -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)
 
 
diff --git a/Language/Copilot/Examples/LTLExamples.hs b/Language/Copilot/Examples/LTLExamples.hs
--- a/Language/Copilot/Examples/LTLExamples.hs
+++ b/Language/Copilot/Examples/LTLExamples.hs
@@ -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") 
+
diff --git a/Language/Copilot/Examples/PTLTLExamples.hs b/Language/Copilot/Examples/PTLTLExamples.hs
--- a/Language/Copilot/Examples/PTLTLExamples.hs
+++ b/Language/Copilot/Examples/PTLTLExamples.hs
@@ -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
+
diff --git a/Language/Copilot/Interface.hs b/Language/Copilot/Interface.hs
--- a/Language/Copilot/Interface.hs
+++ b/Language/Copilot/Interface.hs
@@ -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 ()
diff --git a/Language/Copilot/Interpreter.hs b/Language/Copilot/Interpreter.hs
--- a/Language/Copilot/Interpreter.hs
+++ b/Language/Copilot/Interpreter.hs
@@ -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'
diff --git a/Language/Copilot/Language.hs b/Language/Copilot/Language.hs
--- a/Language/Copilot/Language.hs
+++ b/Language/Copilot/Language.hs
@@ -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
diff --git a/Language/Copilot/Libs/ErrorChks.hs b/Language/Copilot/Libs/ErrorChks.hs
--- a/Language/Copilot/Libs/ErrorChks.hs
+++ b/Language/Copilot/Libs/ErrorChks.hs
@@ -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)
diff --git a/Language/Copilot/Libs/Indexes.hs b/Language/Copilot/Libs/Indexes.hs
--- a/Language/Copilot/Libs/Indexes.hs
+++ b/Language/Copilot/Libs/Indexes.hs
@@ -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
-
-
-                     
-
diff --git a/Language/Copilot/Libs/LTL.hs b/Language/Copilot/Libs/LTL.hs
--- a/Language/Copilot/Libs/LTL.hs
+++ b/Language/Copilot/Libs/LTL.hs
@@ -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')
diff --git a/Language/Copilot/Libs/PTLTL.hs b/Language/Copilot/Libs/PTLTL.hs
--- a/Language/Copilot/Libs/PTLTL.hs
+++ b/Language/Copilot/Libs/PTLTL.hs
@@ -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"
diff --git a/Language/Copilot/Libs/Statistics.hs b/Language/Copilot/Libs/Statistics.hs
--- a/Language/Copilot/Libs/Statistics.hs
+++ b/Language/Copilot/Libs/Statistics.hs
@@ -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 =
diff --git a/README b/README
--- a/README
+++ b/README
@@ -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).
diff --git a/copilot.cabal b/copilot.cabal
--- a/copilot.cabal
+++ b/copilot.cabal
@@ -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: