diff --git a/Language/Copilot/Analyser.hs b/Language/Copilot/Analyser.hs
--- a/Language/Copilot/Analyser.hs
+++ b/Language/Copilot/Analyser.hs
@@ -1,4 +1,4 @@
-{-# OPTIONS_GHC -XRelaxedPolyRec #-}
+{-# LANGUAGE RelaxedPolyRec #-}
 
 -- | This module provides a way to check that a /Copilot/ specification is
 -- compilable
@@ -16,6 +16,7 @@
 import Language.Copilot.Core
 
 import Data.List
+import Data.Maybe(mapMaybe)
 
 type Weight = Int
 
@@ -23,17 +24,11 @@
 data Error =
       BadSyntax String Var -- ^ the BNF is not respected
     | BadDrop Int Var -- ^ A drop expression of less than 0 is used
-    -- | BadSamplingPhase Var Ext -- ^ if an external variable is sampled at phase
-    --                            -- 0 then there is no time for the stream to be
-    --                            -- updated
-    -- | BadSamplingArrPhase Var Ext -- ^ if an external variable is sampled at
-    --                               -- phase 0 then there is no time for the
-    --                               -- stream to be updated
     | BadPArrSpec Var Ext String -- ^ External array indexes can only take
                                  -- variables or constants as indexes.
-    | BadType Var Var -- ^ either a variable is not defined, or not with the
-                      -- good type ; there is no implicit conversion of types in
-                      -- /Copilot/
+    | BadType Var String -- ^ either a variable is not defined, or not with the
+                         -- good type ; there is no implicit conversion of types
+                         -- in /Copilot/.
     | BadTypeExt Ext Var -- ^ either an external variable is not defined, or not
                          -- with the good type; there is no implicit conversion
                          -- of types in /Copilot/
@@ -50,6 +45,9 @@
     | DependsOnFuture [Var] Ext Weight -- ^ If an output depends of a future of
                                        -- an input it will be hard to compile to
                                        -- say the least
+    | NoInit Var -- ^ If we are sampling a function and it has an
+                 -- argument that is a Copilot stream, the weight of
+                 -- that stream must have at least one initial element.
 
 instance Show Error where
     show (BadSyntax s v) =
@@ -62,18 +60,6 @@
           "of elements.\n" 
         , show i ++ " is negative, and Drop only accepts positive arguments.\n"
         ]
-    -- show (BadSamplingPhase v v' ph) =
-    --    unlines
-    --     [ "Error : the external variable " ++ show v' ++ " is sampled at phase " ++ 
-    --       show ph ++ " in the stream " ++ v ++ "." 
-    --     , "Sampling can only occur from phase 1 onwards.\n"
-    --     ]
-    -- show (BadSamplingArrPhase v arr ph) =
-    --    unlines
-    --     [ "Error : the external array " ++ show arr ++ " is sampled at phase " ++ 
-    --       show ph ++ " in the stream " ++ v ++ "."
-    --     , " Sampling can only occur from phase 1 onwards.\n"
-    --     ]
     show (BadPArrSpec v arr idx) = 
        unlines
         [ "Error : the index into an external array can only take a "
@@ -84,7 +70,7 @@
         ]
     show (BadType v v') =
        unlines
-        [ "Error : the monitor variable " ++ v ++ ", called in the stream " 
+        [ "Error : the monitor variable " ++ v ++ ", called from " 
           ++ v' ++ ", either"
         , "does not exist, or don't have the right type (there is no implicit " 
           ++ "conversion).\n"
@@ -127,6 +113,11 @@
           ++ "obviously impossible."
         , "Path : " ++ show (reverse vs) ++ "\n"
         ]
+    show (NoInit v) = 
+          "Error : the Copilot variable " ++ v ++ " appears either as an argument in an "
+          ++ "external function that is sampled or an index in an external array being sampled. "
+          ++ "In either case, the stream must have an initial value (that is not drawn from an "
+          ++ "external variable)."
 
 (&&>) :: Maybe a -> Maybe a -> Maybe a
 m &&> m' =
@@ -145,18 +136,18 @@
 
 -- | Check a /Copilot/ specification.
 -- If it is not compilable, then returns an error describing the issue.
--- Else, returns @Nothing@
+-- Else, returns @Nothing@.
 check :: StreamableMaps Spec -> Maybe Error
 check streams =
-    syntaxCheck streams &&> defCheck streams
+  syntaxCheck streams &&> defCheck streams &&> checkInitsArgs streams
 
 -- Represents all the kind of specs that are authorized after a given operator.
-data SpecSet = AllSpecSet | FunSpecSet | DropSpecSet | PArrSet 
-             deriving Eq
+data SpecSet = AllSpecSet | FunSpecSet | DropSpecSet 
+  deriving Eq
 
--- Check that the AST of the copilot specification match the BNF
--- Could have been verified by the type checker if the type of Spec had been cut
--- But then there would have been quite a lot construction/deconstruction to do everywhere.
+-- Check that the AST of the copilot specification match the BNF could have been
+-- verified by the type checker if the type of Spec had been cut But then there
+-- would have been quite a lot construction/deconstruction to do everywhere.
 -- Hence the compact type for Spec and this extra check.
 syntaxCheck :: StreamableMaps Spec -> Maybe Error
 syntaxCheck streams =
@@ -169,10 +160,16 @@
                 case s of
                     Var _ -> Nothing
                     Const _ -> Nothing
-                    PVar _ _ -> Nothing -- ph > 0 ||> BadSamplingPhase v v' ph
+                    PVar _ _ -> Nothing -- checkSampling s0
                     PArr _ (arr,s0) -> checkIndex v arr s0 
---                      &&> ph > 0 ||> BadSamplingArrPhase v arr ph 
-                      &&> checkSyntaxSpec PArrSet v s0 Nothing
+-- case chkInitElem streams (getElem v streams `asTypeOf` s0) of
+--                                       Left ()  -> Just $ NoInit (show arr) v
+--                                       Right () -> Nothing
+--                          _       -> Just $ BadArrIdx (show arr) (show s0)
+--                      ) &&> checkSampling arr
+--                        &&> checkSyntaxSpec PArrSet v s0 Nothing                      
+                    -- PVar _ _ -> Nothing 
+                    -- PArr _ (arr,s0) -> 
                     F _ _ s0 -> set /= DropSpecSet ||> BadSyntax "F" v 
                       &&> checkSyntaxSpec FunSpecSet v s0 Nothing
                     F2 _ _ s0 s1 -> set /= DropSpecSet ||> BadSyntax "F2" v 
@@ -189,7 +186,20 @@
         checkIndex _ _ (Var _)      = Nothing
         checkIndex _ _ (Const _)    = Nothing
         checkIndex v arr idx = Just $ BadPArrSpec v arr (show idx)
+        -- checkSampling s = 
+        --   case s of
+        --     ExtV _   -> Nothing
+        --     fun@(Fun f args) ->  
+        --       foldl (\n arg -> case arg of
+        --                          C _ -> n &&> Nothing
+        --                                 -- already check elems defined in defCheck
+        --                          V v -> n &&> (case chkInitElem streams (getElem v streams) of 
+        --                                          Left ()  -> Just $ NoInit (show fun) v
+        --                                          Right () -> Nothing
+        --                                       )
+        --             ) Nothing args
 
+
 -- | Checks that streams are well defined (i.e., can be compiled).
 defCheck :: StreamableMaps Spec -> Maybe Error
 defCheck streams =
@@ -248,12 +258,16 @@
 getExternalVars streams =
     nub $ foldStreamableMaps decl streams []
     where
-        decl :: Streamable a 
-             => Var -> Spec a -> [Exs] -> [Exs]
+        decl :: Streamable a => Var -> Spec a -> [Exs] -> [Exs]
         decl _ s ls =
             case s of
                 PVar t v -> (t, v, ExtRetV) : ls
-                PArr t (arr, s0) -> (t, arr, ExtRetA (show s0)) : ls
+                PArr t (arr, s0) -> (t, arr
+                                    , ExtRetA (case s0 of
+                                                 Var v -> V v
+                                                 Const c -> C (show c)
+                                                 _ -> error "Error in getExternalVars.")
+                                    ) : ls
                 F _ _ s0 -> decl undefined s0 ls
                 F2 _ _ s0 s1 -> decl undefined s0 $ decl undefined s1 ls
                 F3 _ _ s0 s1 s2 -> decl undefined s0 $ decl undefined s1 
@@ -262,6 +276,73 @@
                 Append _ s' -> decl undefined s' ls
                 _ -> ls
 
+-- | Is there an initial element (for sampling functions)?
+checkInitsArgs :: StreamableMaps Spec -> Maybe Error
+checkInitsArgs streams =
+  let checkInits :: Streamable a => Var -> Spec a -> Maybe Error -> Maybe Error
+      checkInits v s err =
+        err &&> if checkPath 0 [v] s >= 0 then Just (NoInit v)
+                  else Nothing
+        where checkPath :: Streamable a => Int -> [Var] -> Spec a -> Int
+              checkPath n vs s0 = 
+                if (v `elem` samplingFuncs) || (v `elem` arrIndices)
+                  then case s0 of
+                         Var v0    -> if elem v0 vs then n
+                                       else checkPath n (v0:vs) 
+                                              (getElem v0 streams `asTypeOf` s0)
+                         Append ls s1 -> checkPath (n - length ls) vs s1
+                         Drop m s1    -> checkPath (m + n) vs s1
+                         _ -> n
+                         -- Const _  -> n
+                         -- PVar _ _ -> n
+                         -- PArr _ _ -> n
+                         -- F _ _ _      -> n
+                         -- F2 _ _ _ _   -> n
+                         -- F3 _ _ _ _ _ -> n
+                  else (-1)
+              samplingFuncs = 
+                concatMap (\x -> case x of 
+                                   (_, Fun _ args, _) -> 
+                                     mapMaybe (\arg -> 
+                                       case arg of
+                                         C _ -> Nothing
+                                         V v0 -> Just v0
+                                              ) args
+                                   (_, ExtV _, _) -> [])
+                (getExternalVars streams)
+              arrIndices = mapMaybe (\x -> case x of
+                                             (_,_,ExtRetV) -> Nothing 
+                                             (_,_,ExtRetA idx) -> 
+                                               case idx of
+                                                 V v' -> Just v'
+                                                 C _ -> Nothing)
+                           (getExternalVars streams)
+  in foldStreamableMaps checkInits streams Nothing
+
+-- chkInitElem :: Streamable a => StreamableMaps Spec -> Spec a -> Either () ()
+-- chkInitElem streams spec = 
+--   initElem spec 0 []
+--   where 
+--     -- getSpec :: Streamable a => Var -> Spec a
+--     -- getSpec v = let s = getMaybeElem v streams in
+--     --                case s of
+--     --                  Nothing -> error $ "Error: No Copilot stream "
+--     --                             ++ v ++ " exists."
+--     --                  Just s0 -> s0 `asTypeOf` s
+--     initElem :: Streamable a => Spec a -> Int -> [Var] -> Either () ()
+--     initElem s cnt vs =
+--       case s of
+--         Var v    -> if elem v vs then initChk 
+--                       else initElem (getElem v streams) cnt (v:vs)
+--         Const _  -> initChk
+--         PVar t v -> initChk
+--         PArr t (arr, s0) -> initChk
+--         F _ _ _      -> initChk
+--         F2 _ _ _ _   -> initChk
+--         F3 _ _ _ _ _ -> initChk
+--         Append ls s0 -> initElem s0 (cnt - length ls) vs
+--         Drop n s0    -> initElem s0 (cnt + n) vs
+--       where initChk = if cnt < 0 then Right () else Left ()
 
 ---- Dependency graphs (for next version of nNWCP, and for scheduling)
 {-
diff --git a/Language/Copilot/AtomToC.hs b/Language/Copilot/AtomToC.hs
--- a/Language/Copilot/AtomToC.hs
+++ b/Language/Copilot/AtomToC.hs
@@ -3,21 +3,28 @@
 -- | Defines a main() and print statements to easily execute generated Copilot specs.
 module Language.Copilot.AtomToC(getPrePostCode) where
 
-import Language.Copilot.Compiler (tmpSampleStr, tmpArrName, tmpVarName)
 import Language.Copilot.AdHocC
 
 import Language.Copilot.Core
 
+import Data.Maybe (fromMaybe)
 import Data.List
 
 -- allExts represents all the variabbles to monitor (used for declaring them)
 -- inputExts represents the monitored variables which are to be fed to the
 -- standard input of the C program.  only used for the testing with random
 -- streams and values.
-getPrePostCode :: Name -> StreamableMaps Spec -> [Exs] 
-               -> [(Ext,Int)] -> Vars -> Period -> (String, String)
-getPrePostCode cName streams allExts arrDecs inputExts p =
-    (preCode $ extDecls allExts arrDecs, postCode cName streams allExts inputExts p)
+getPrePostCode :: Bool -> (Maybe String, Maybe String) -> Name 
+               -> StreamableMaps Spec -> [Exs] -> [(Ext,Int)] -> Vars 
+               -> Period -> (String, String)
+getPrePostCode simulatation (pre, post) cName streams allExts 
+               arrDecs inputExts p =
+    ( (if simulatation then preCode (extDecls allExts arrDecs)
+         else "") ++ fromMaybe "" pre
+    , fromMaybe "" post ++ periodLoop cName p 
+      ++ if simulatation then (postCode cName streams inputExts)
+           else ""
+    )
 
 -- Make the declarations for external vars
 extDecls :: [Exs] -> [(Ext,Int)] -> [String]
@@ -43,19 +50,35 @@
   [ includeBracket "stdio.h"
   , includeBracket "stdlib.h"
   , includeBracket "string.h"
-  , includeBracket "inttypes.h"
+--  , includeBracket "inttypes.h"
   , ""
   , "unsigned long long rnd;"
   ]
   ++ extDeclarations
-  
-postCode :: Name -> StreamableMaps Spec -> [Exs] -> Vars -> Period -> String
-postCode cName streams allExts inputExts p = 
+
+-- | Generate a temporary C file name. 
+tmpCFileName :: String -> String
+tmpCFileName name = "__" ++ name
+
+periodLoop :: Name -> Period -> String
+periodLoop cName p = unlines
+  [ "\n"
+  , "void " ++ tmpCFileName cName ++ "(void) {"
+  , "  int i;"
+  , "  for(i = 0; i < " ++ show p ++ "; i++) {"
+  , "    "  ++ cName ++ "();"
+  , "  }"
+  , "}"
+  ]
+
+postCode :: Name -> StreamableMaps Spec -> Vars -> String
+postCode cName streams inputExts = 
   unlines $
+  [""] ++
   (if isEmptySM inputExts
-    then []
-    else cleanString)
-  ++
+     then []
+     else cleanString)
+  ++ -- make a loop to complete a period of computation.
   [ "int main(int argc, char *argv[]) {"
   , "  if (argc != 2) {"
   , "    " ++ printfNewline 
@@ -64,27 +87,14 @@
   , "    return 1;"
   , "  }"
   , "  rnd = atoi(argv[1]);"
-  ]
-  ++
-  inputExtVars inputExts "  "
-  ++
-  sampleExtVars allExts cName
-  ++
-  [ "  int i = 0;"
-  , "  for(; i < rnd ; i++) {"
-  ]
-  ++
-  inputExtVars inputExts "    "
-  ++
-  [ "    int j = 0;"
-  , "    for (; j < " ++ show p ++ " ; j++) {"
-  , "      " ++ cName ++ "();"
-  , "    }"
+  , "  int i;"
+  , "  for(i = 0; i < rnd ; i++) {"
   , "    " ++ printf "period: %i   " ["i"]
   ]
-  ++
-  outputVars cName streams 
-  ++
+  ++ inputExtVars inputExts "    "
+  ++ ["    " ++ tmpCFileName cName ++ "();"]
+  ++ outputVars cName streams 
+  ++ 
   [ "    " ++ printfNewline "" []
   , "    fflush(stdout);"
   , "  }"
@@ -118,20 +128,6 @@
             (indent ++ "sscanf (" ++ string ++ ", \"" 
                     ++ typeId (head l) ++ "\", &" ++ v ++ ");") :
             (indent ++ "clean (" ++ string ++ ", stdin);") : ls
-
-sampleExtVars :: [Exs] -> Name -> [String]
-sampleExtVars allExts cName =
-    map (\ext -> let (v,e) = sample ext in
-           "  " ++ vPre cName ++ tmpSampleStr ++ (normalizeVar e)
-           ++ " = " ++ v ++ ";") 
-        allExts
-    where 
-        sample :: Exs -> (Var, String)
-        sample (_, v, ExtRetV) = ( case v of 
-                                     ExtV var -> var
-                                     Fun fname args -> funcShow cName fname args
-                                  , tmpVarName v)
-        sample (_, v, ExtRetA idx) = (show v ++ "[0]", tmpArrName v idx)
 
 outputVars :: Name -> StreamableMaps Spec -> [String]
 outputVars cName streams =
diff --git a/Language/Copilot/Compiler.hs b/Language/Copilot/Compiler.hs
--- a/Language/Copilot/Compiler.hs
+++ b/Language/Copilot/Compiler.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE ScopedTypeVariables, Rank2Types #-}
+{-# LANGUAGE ScopedTypeVariables, Rank2Types, GADTs #-}
 
 -- XXX Clean this up!
 
@@ -12,7 +12,7 @@
 import Data.Maybe
 import qualified Data.Map as M
 import Data.List
-import Data.Word (Word64)
+import Data.Word (Word32)
 
 import qualified Language.Atom as A
 
@@ -29,8 +29,13 @@
                     (\_ -> initExtSamples streams outputs prophArrs outputIndexes) 
                     streams 
                     (return emptyTmpSamples)
+
+    let nextStates = makeStates $ 
+          mapStreamableMaps (nextSt streams prophArrs tmpSamples outputIndexes 0) 
+            streams
+
     -- One atom rule for each stream
-    foldStreamableMaps (makeRule p' streams outputs prophArrs tmpSamples 
+    foldStreamableMaps (makeRule nextStates outputs prophArrs
                            updateIndexes outputIndexes) 
       streams (return ())
 
@@ -46,12 +51,14 @@
 --  where
 --    optP = getOptimalPeriod streams sends
 
--- | For period of length n:
--- Phase 0: state update.
--- Phase 1: Compute output variables.
--- Phase 2 - n-2: send values (if any).
--- Phase 2 - n-2: Sample external vars (if any).
--- Phase n-1: update indexes.
+
+-- | For period n >= 5:
+-- Phase 0: Sample external vars (if any).
+-- Phase 1: state update.
+-- Phase 2: Compute output variables.
+-- Phase 3: Fire triggers (if any).
+-- Phase 3: send values (if any).
+-- Phase 4 up to n: update indexes.
 period :: Maybe Int -> Int
 period p = 
   case p of
@@ -61,10 +68,10 @@
                 else error $ "Copilot error: the period is too short, " 
                        ++ "it should be at least " ++ show minPeriod ++ " ticks."
   where minPeriod :: Int
-        minPeriod = 4
+        minPeriod = 5
 
 -- For the prophecy arrays
-type ArrIndex = Word64
+type ArrIndex = Word32
 type ProphArrs = StreamableMaps BoundedArray
 type Outputs = StreamableMaps A.V
 type Indexes = M.Map Var (A.V ArrIndex)
@@ -74,14 +81,98 @@
 
 data BoundedArray a = B ArrIndex (Maybe (A.A a))
 
-nextSt :: Streamable a => StreamableMaps Spec -> ProphArrs -> TmpSamples -> Indexes 
-       -> Spec a -> ArrIndex -> A.E a
-nextSt streams prophArrs tmpSamples outputIndexes s index = 
+-- nextSt :: Streamable a => StreamableMaps Spec -> ProphArrs -> TmpSamples -> Indexes 
+--        -> Spec a -> ArrIndex -> A.E a
+-- nextSt streams prophArrs tmpSamples outputIndexes s index = 
+--     case s of
+--         PVar _ v  -> 
+--           let PhV var = getElem (tmpVarName v) (tmpVars tmpSamples) in
+--           A.value var
+--         PArr _ (v, idx) -> 
+--           let PhA var = e tmp (tmpArrs tmpSamples) 
+--               tmp = tmpArrName v (show idx) 
+--               e a b = case getMaybeElem a b of
+--                         Nothing -> 
+--                           error "Error in application of getElem in nextSt."
+--                         Just x  -> x 
+--           in A.value var
+--         Var v -> nextStVar v streams prophArrs tmpSamples outputIndexes index
+--         Const e -> A.Const e
+--         F _ f s0 -> f $ next s0 index 
+--         F2 _ f s0 s1 -> 
+--             f (next s0 index) 
+--               (next s1 index)
+--         F3 _ f s0 s1 s2 -> 
+--             f (next s0 index) 
+--               (next s1 index) 
+--               (next s2 index)
+--         Append _ s0 -> next s0 index
+--         Drop i s0 -> next s0 (fromInteger (toInteger i) + index)
+--     where next :: Streamable b => Spec b -> ArrIndex -> A.E b
+--           next = nextSt streams prophArrs tmpSamples outputIndexes
+
+-- nextStVar v streams prophArrs tmpSamples outputIndexes index = 
+--   let B initLen maybeArr = getElem v prophArrs in
+--   -- This check is extremely important It means that if x at time n depends on y
+--   -- at time n then x is obtained not by y, but by inlining the definition of y
+--   -- so it increases the size of code (sadly), but is the only thing preventing
+--   -- race conditions from occuring
+--   if index < initLen
+--     then getVar v initLen maybeArr 
+--     else let s0 = getElem v streams in 
+--          nextSt streams prophArrs tmpSamples outputIndexes s0 (index - initLen)
+--   where getVar :: Streamable a => Var -> ArrIndex -> Maybe (A.A a) -> A.E a
+--         getVar v initLen maybeArr =
+--            let outputIndex = case M.lookup v outputIndexes of
+--                                Nothing -> error "Error in function getVar."
+--                                Just x -> x
+--                arr = case maybeArr of
+--                        Nothing -> error "Error in function getVar (maybeArr)."
+--                        Just x -> x in 
+--            arr A.!. ((A.Const index + A.VRef outputIndex) `A.mod_`  
+--                        (A.Const (initLen + 1)))
+
+
+-- | Takes the NextSts and walks over the tree building the Atom expression.  
+makeStates :: StreamableMaps NextSt -> StreamableMaps A.E
+makeStates trees = 
+  mapStreamableMaps (\_ -> makeState) trees
+  where 
+    makeState :: (Streamable a) => NextSt a -> A.E a
+    makeState tree = 
+      case tree of 
+        ExpLeaf s -> s
+        F1Node f s0 -> f (makeState s0) 
+        F2Node f s0 s1 -> f (makeState s0) (makeState s1)
+        F3Node f s0 s1 s2 -> f (makeState s0) (makeState s1) (makeState s2)
+        VarRefLeaf v -> makeState (getElem v trees)
+
+-- | A tree datatype that holds Atom expressions from the 'nextSt' function
+-- | until we've got all variable references collected up.  In particular, we
+-- | have told function applications.
+data NextSt a where
+    -- Leaves
+    ExpLeaf :: A.E a -> NextSt a
+    VarRefLeaf :: Var -> NextSt a
+    -- Parent nodes
+    F1Node :: (Streamable a, Streamable b) 
+           => (A.E b -> A.E a) -> NextSt b -> NextSt a
+    F2Node :: (Streamable a, Streamable b, Streamable c) 
+           => (A.E b -> A.E c -> A.E a) -> NextSt b -> NextSt c -> NextSt a 
+    F3Node :: (Streamable a, Streamable b, Streamable c, Streamable d) 
+           => (A.E b -> A.E c -> A.E d -> A.E a) 
+              -> NextSt b -> NextSt c -> NextSt d -> NextSt a
+
+-- | Compute the next state value.
+nextSt :: Streamable a 
+       => StreamableMaps Spec -> ProphArrs -> TmpSamples -> Indexes -> ArrIndex 
+       -> Var -> Spec a -> NextSt a
+nextSt streams prophArrs tmpSamples outputIndexes index _ s = 
     case s of
-        PVar _ v  -> 
+        PVar _ v  -> ExpLeaf $ 
           let PhV var = getElem (tmpVarName v) (tmpVars tmpSamples) in
           A.value var
-        PArr _ (v, idx) -> 
+        PArr _ (v, idx) -> ExpLeaf $
           let PhA var = e tmp (tmpArrs tmpSamples) 
               tmp = tmpArrName v (show idx) 
               e a b = case getMaybeElem a b of
@@ -89,34 +180,39 @@
                           error "Error in application of getElem in nextSt."
                         Just x  -> x 
           in A.value var
-        Var v -> let B initLen maybeArr = getElem v prophArrs in
-            -- This check is extremely important
-            -- It means that if x at time n depends on y at time n
-            -- then x is obtained not by y, but by inlining the definition of y
-            -- so it increases the size of code (sadly),
-            -- but is the only thing preventing race conditions from occuring
-            if index < initLen
-                then getVar v initLen maybeArr 
-                else let s0 = getElem v streams in 
-                     next s0 (index - initLen)
-        Const e -> A.Const e
-        F _ f s0 -> f $ next s0 index
-        F2 _ f s0 s1 ->
-            f (next s0 index) 
-              (next s1 index)
-        F3 _ f s0 s1 s2 ->
-            f (next s0 index) 
-              (next s1 index) 
-              (next s2 index)
+        Var v -> nextStVar v streams prophArrs tmpSamples outputIndexes index
+        Const e -> ExpLeaf $ A.Const e
+        F _ f s0 -> F1Node f (next s0 index)
+        F2 _ f s0 s1 -> F2Node f (next s0 index) (next s1 index)
+        F3 _ f s0 s1 s2 -> F3Node f (next s0 index) (next s1 index) (next s2 index)
         Append _ s0 -> next s0 index
         Drop i s0 -> next s0 (fromInteger (toInteger i) + index)
-    where
-        next :: Streamable b => Spec b -> ArrIndex -> A.E b
-        next = nextSt streams prophArrs tmpSamples outputIndexes 
-        getVar :: Streamable a 
-               => Var -> ArrIndex -> Maybe (A.A a) -> A.E a
-        getVar v initLen maybeArr =
-           let outputIndex = case M.lookup v outputIndexes of
+    where next :: Streamable b => Spec b -> ArrIndex -> NextSt b
+          next s' ind = 
+            nextSt streams prophArrs tmpSamples outputIndexes ind undefined s'
+
+-- | Get the next state when one stream references another Copilot stream variable.
+nextStVar :: Streamable a => Var -> StreamableMaps Spec -> ProphArrs 
+          -> TmpSamples -> Indexes -> ArrIndex -> NextSt a
+nextStVar v streams prophArrs tmpSamples outputIndexes index = 
+  let B initLen maybeArr = getElem v prophArrs in
+  -- This check is extremely important. It means that if x at time n depends on y
+  -- at time n then x is obtained not by y, but by inlining the definition of y
+  -- so it increases the size of code (sadly), but is the only thing preventing
+  -- race conditions from occuring.
+  if index < initLen
+    then getVar v initLen maybeArr 
+    else let s0 = getElem v streams in 
+         -- XXX This should be generalized to handle arbitrary index values.
+         -- For now, as a test, we'll just use the cahced nextState value if
+         -- it's like computing that stream's nextState from scratch.
+         let newIndex = index - initLen in
+         if newIndex == 0 then VarRefLeaf v
+           else nextSt streams prophArrs tmpSamples outputIndexes 
+                  newIndex undefined s0
+  where getVar :: Streamable a => Var -> ArrIndex -> Maybe (A.A a) -> NextSt a
+        getVar v' initLen maybeArr = ExpLeaf $
+           let outputIndex = case M.lookup v' outputIndexes of
                                Nothing -> error "Error in function getVar."
                                Just x -> x
                arr = case maybeArr of
@@ -125,7 +221,8 @@
            arr A.!. ((A.Const index + A.VRef outputIndex) `A.mod_`  
                        (A.Const (initLen + 1)))
 
-initProphArr :: forall a. Streamable a => Var -> Spec a -> A.Atom (BoundedArray a)
+initProphArr :: forall a. Streamable a 
+             => Var -> Spec a -> A.Atom (BoundedArray a)
 initProphArr v s =
     let states = initState s
         name = "prophVal__" ++ normalizeVar v
@@ -220,66 +317,64 @@
                           => Spec b -> A.Atom TmpSamples -> A.Atom TmpSamples
           initExtSamples' = initExtSamples streams outputs prophArrs outputIndexes
 
+-- | For each stream, make an index into its array of values telling you where
+-- the next value in the array to update is.
 makeUpdateIndex :: Var -> BoundedArray a -> A.Atom Indexes -> A.Atom Indexes
 makeUpdateIndex v (B n arr) indexes =
     case arr of
         Nothing -> indexes
         Just _ ->  
-            do
-                mindexes <- indexes
+            do  mindexes <- indexes
                 index <- atomConstructor ("updateIndex__" ++ normalizeVar v) n
                 return $ M.insert v index mindexes
 
+-- | For each stream, make an index into its array of values telling you where
+-- its current output value is.
 makeOutputIndex :: Var -> BoundedArray a -> A.Atom Indexes -> A.Atom Indexes
 makeOutputIndex v (B _ arr) indexes =
     case arr of
         Nothing -> indexes
         Just _ ->  
-            do
-                mindexes <- indexes
+            do  mindexes <- indexes
                 index <- atomConstructor ("outputIndex__" ++ normalizeVar v) 0
                 return $ M.insert v index mindexes
 
+--        where nextSt' = nextSt streams prophArrs tmpSamples outputIndexes s 0
 makeRule :: forall a. Streamable a => 
-    Period -> StreamableMaps Spec -> Outputs -> ProphArrs -> TmpSamples -> 
-    Indexes -> Indexes -> Var -> Spec a -> A.Atom () -> A.Atom ()
-makeRule p streams outputs prophArrs tmpSamples updateIndexes outputIndexes v s r = do
+    StreamableMaps A.E -> Outputs -> ProphArrs
+    -> Indexes -> Indexes -> Var -> Spec a -> A.Atom () -> A.Atom ()
+makeRule exps outputs prophArrs updateIndexes outputIndexes v _ r = do
     r 
     let B n maybeArr = getElem v prophArrs::BoundedArray a
     case maybeArr of
         Nothing ->
             -- Fusing together the update and the output if the prophecy array doesn't exist 
             -- (ie if it would only have hold the output value)
-            A.exactPhase 0 $ A.atom ("updateOutput__" ++ normalizeVar v) $ do
-                ((getElem v outputs)::(A.V a)) A.<== nextSt'
+            A.exactPhase 2 $ A.atom ("updateOutput__" ++ normalizeVar v) $ do
+                ((getElem v outputs)::(A.V a)) A.<== getElem v exps
 
         Just arr -> do
             let updateIndex = fromJust $ M.lookup v updateIndexes
                 outputIndex = fromJust $ M.lookup v outputIndexes
 
-            A.exactPhase 0 $ A.atom ("update__" ++ normalizeVar v) $ do
-                arr A.! (A.VRef updateIndex) A.<== nextSt'
+            A.exactPhase 1 $ A.atom ("update__" ++ normalizeVar v) $ do
+                arr A.! (A.VRef updateIndex) A.<== getElem v exps
             
-            A.exactPhase 1 $ A.atom ("output__" ++ normalizeVar v) $ do
+            A.exactPhase 2 $ A.atom ("output__" ++ normalizeVar v) $ do
                 ((getElem v outputs)::(A.V a)) A.<== arr A.!. (A.VRef outputIndex)
                 outputIndex A.<==          (A.VRef outputIndex + A.Const 1) 
                                   `A.mod_` A.Const (n + 1)
             
-            -- XXX For now, we put these all in the last phase.  We want better
-            -- distribution though at some point.
-            A.phase (p - 1)
+            A.phase 4
               $ A.atom ("incrUpdateIndex__" ++ normalizeVar v) $ do
                 updateIndex A.<==          (A.VRef updateIndex + A.Const 1) 
                                   `A.mod_` A.Const (n + 1)
-
-       where nextSt' = nextSt streams prophArrs tmpSamples outputIndexes s 0
              
--- Do sends in phase 2.
 makeSend :: forall a. Streamable a 
          => Outputs -> String -> Send a -> A.Atom () -> A.Atom ()
 makeSend outputs name (Send v port portName) r = do
         r 
-        A.exactPhase 2 $ A.atom ("__send_" ++ name) $
+        A.exactPhase 3 $ A.atom ("__send_" ++ name) $
             mkSend (A.value $ getElem (getMaybeVar v) outputs :: A.E a) 
                    port 
                    portName
@@ -313,7 +408,7 @@
                      Nothing ->  error $ "Copilot error: variable " ++ v' 
                                    ++ " was not defined!."
                      Just (PhV var') -> PhV var' in
-     (v', A.exactPhase minSampPh $ 
+     (v', A.exactPhase 0 $ 
             A.atom (sampleStr ++ normalizeVar v') $ 
                var A.<== (A.value $ externalAtomConstructor $ getSampleFuncVar v)
      ) : a
@@ -324,7 +419,7 @@
                case getMaybeElem arr' (tmpArrs ts) :: Maybe (PhasedValueArr a) of
                  Nothing -> error "Error in fucntion sampleExts."
                  Just x -> x in
-         (arr', A.exactPhase minSampPh $ 
+         (arr', A.exactPhase 0 $ 
             A.atom (sampleStr ++ normalizeVar arr') $ 
                arrV A.<== A.array' (getSampleFuncVar arr)
                                    (atomType (unit::a)) A.!. i
@@ -335,8 +430,8 @@
                          sampleExts' s2 a
     Append _ s0 -> sampleExts' s0 a
     Drop _ s0 -> sampleExts' s0 a
-  where minSampPh :: Int
-        minSampPh = 2
+  where -- minSampPh :: Int
+        --minSampPh = 2
         sampleExts' s' a' = sampleExts outputs ts cFileName s' a'
         getSampleFuncVar v = case v of
                                ExtV extV -> extV
@@ -364,7 +459,7 @@
 makeTrigger :: Outputs -> Name -> Trigger -> A.Atom () -> A.Atom ()
 makeTrigger outputs cFileName trigger@(Trigger s fnName args) r = 
   do r 
-     (A.exactPhase 2 $ A.atom (show trigger) $ 
+     (A.exactPhase 3 $ A.atom (show trigger) $ 
         do A.cond (getOutput outputs s)
            fnCall cFileName fnName args)
 
diff --git a/Language/Copilot/Core.hs b/Language/Copilot/Core.hs
--- a/Language/Copilot/Core.hs
+++ b/Language/Copilot/Core.hs
@@ -49,7 +49,7 @@
     Var :: Streamable a => Var -> Spec a
     Const :: Streamable a => a -> Spec a
 
-    PVar :: Streamable a => A.Type -> Ext  -> Spec a
+    PVar :: Streamable a => A.Type -> Ext -> Spec a
     PArr :: (Streamable a, Streamable b, A.IntegralE b) 
          => A.Type -> (Ext, Spec b) -> Spec a
 
@@ -98,19 +98,20 @@
 -- XXX in Ext, we throw away the type info for Args.  This is because we're just
 -- making external calls, and we don't know anything about the types anyway (we
 -- just make strings).  Remove from the datatype.
+
 -- | Holds external variables or external functions to call.
 data Ext = ExtV Var
          | Fun String Args
 
+instance Show Ext where
+  show (ExtV v) = v
+  show (Fun f args) = normalizeVar f ++ show args
+
 type Exs = (A.Type, Ext, ExtRet)
 
 data ExtRet = ExtRetV 
-            | ExtRetA String
+            | ExtRetA ArgConstVar
   deriving Eq
-
-instance Show Ext where
-  show (ExtV v) = v
-  show (Fun f args) = normalizeVar f ++ show args
 
 -- | For calling a function with Atom variables.
 funcShow :: Name -> String -> Args -> String
diff --git a/Language/Copilot/Dispatch.hs b/Language/Copilot/Dispatch.hs
--- a/Language/Copilot/Dispatch.hs
+++ b/Language/Copilot/Dispatch.hs
@@ -33,13 +33,14 @@
     , interpreted :: Interpreted -- ^ Interpret the program or not
     , outputDir :: String -- ^ Where to put the executable
     , compiler :: String -- ^ Which compiler to use
-    , prePostCode :: Maybe (String, String) -- ^ Code to replace the default
-                                            -- initialization and main
+    , sim :: Bool -- ^ Are we running a C simulator?
+    , prePostCode :: (Maybe String, Maybe String) -- ^ Code to replace the default
+                                                  -- initialization and main
     , arrDecs :: [(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."
+                                 -- size allows them to be declared.
     , clock :: Maybe A.Clock     -- Use the hardware clock to drive the timing
                                  -- of the program.
     }
@@ -72,7 +73,7 @@
         mapM_ putStrLn preludeText 
         isValid <-
             case check (strms elems) of
-                Just x -> putStrLn (show x) >> return False
+                Just x -> print x >> return False
                 Nothing -> return True
         when isValid $
             -- because haskell is lazy, will only get computed if later used
@@ -81,7 +82,7 @@
             in case backEnd of
                 Interpreter -> 
                     do
-                        when (not allInputsPresents) $ error errMsg
+                        unless allInputsPresents $ error errMsg
                         mapM_ putStrLn interpretedLines
                 Opts opts ->
                     let isInterpreted =
@@ -99,15 +100,15 @@
                         let delete ext = do 
                               f0 <- canonicalizePath (cName opts ++ ext) 
                               f1 <- canonicalizePath (dirName ++ cName opts ++ ext)
-                              if f0 == f1 then return ()
-                                else removeFile (cName opts ++ ext)
+                              unless (f0 == f1) $ removeFile (cName opts ++ ext)
                         putStrLn $ "Moving " ++ cName opts ++ ".c and " ++ cName opts 
                                         ++ ".h to " ++ dirName ++ "  ..."
                         copy ".c"
                         copy ".h"
                         delete ".c"
                         delete ".h"
-                        when (prePostCode opts == Nothing) $ gccCall (Opts opts)
+--                        when (prePostCode opts == Nothing) $ gccCall (Opts opts)
+                        when (sim opts) (gccCall (Opts opts))
                         when ((isInterpreted || isExecuted) && not allInputsPresents) $ 
                             error errMsg
                         when isExecuted $ execute (strms elems) (dirName ++ cName opts) 
@@ -127,12 +128,15 @@
     let cFileName = cName opts
         (p', program) = copilotToAtom elems (getPeriod opts) cFileName
         (preCode, postCode) = 
-            case (prePostCode opts) of
-                Nothing ->  
-                  getPrePostCode cFileName (strms elems) allExts 
-                                 (map (\(x,y) -> (ExtV x,y)) (arrDecs opts))
-                                 trueInputExts p'
-                Just (pre, post) -> (pre, post)
+            getPrePostCode (sim opts) (prePostCode opts) cFileName 
+                           (strms elems) allExts (map (\(x,y) -> (ExtV x,y)) 
+                           (arrDecs opts)) trueInputExts p'
+            -- case (prePostCode opts) of
+            --     Nothing ->  
+            --       getPrePostCode cFileName (strms elems) allExts 
+            --                      (map (\(x,y) -> (ExtV x,y)) (arrDecs opts))
+            --                      trueInputExts p'
+            --     Just (pre, post) -> (pre, post)
         atomConfig = A.defaults 
             { A.cCode = \_ _ _ -> (preCode, postCode)
             , A.cRuleCoverage = False
@@ -143,11 +147,10 @@
     in do
         putStrLn $ "Compiling Copilot specs to C  ..."
         (sched, _, _, _, _) <- A.compile cFileName atomConfig program
-        if isVerbose
-            then putStrLn $ A.reportSchedule sched
-            else return ()
+        when isVerbose (putStrLn $ A.reportSchedule sched)
         putStrLn $ "Generated " ++ cFileName ++ ".c and " ++ cFileName ++ ".h"
 
+-- | Call Gcc to compile the code.
 gccCall :: BackEnd -> IO ()
 gccCall backend = 
   case backend of
@@ -157,8 +160,9 @@
           programName = cName opts
       in
         do
-          let command = (compiler opts) ++ " " ++ dirName ++ cName opts ++ ".c" ++ " -o " 
-                        ++ dirName ++ programName ++ " " ++ gccOpts opts
+          let command = compiler opts ++ " " ++ dirName ++ cName opts 
+                        ++ ".c" ++ " -o " ++ dirName ++ programName 
+                        ++ " " ++ gccOpts opts
           putStrLn "Calling the C compiler  ..."
           putStrLn command
           _ <- system command
@@ -172,10 +176,9 @@
 
         when isInterpreted 
                  (do putStrLn "\n *** Checking the randomly-generated Copilot specification: ***\n"
-                     putStrLn $ show streams)
+                     print streams)
         let inputVar v (val:vals) ioVars =
-                do
-                    hPutStr hin (showAsC val ++ " \n")
+                do  hPutStr hin (showAsC val ++ " \n")
                     hFlush hin
                     vars <- ioVars
                     return $ updateSubMap (\m -> M.insert v vals m) vars
@@ -184,11 +187,10 @@
             executePeriod _ [] _ = error "Impossible : empty ExecutePeriod"
             executePeriod inputExts (inLine:inLines) n =
                 when (n > 0) $ 
-                    do
-                        nextInputExts <- foldStreamableMaps inputVar inputExts (return emptySM)
+                    do  nextInputExts <- foldStreamableMaps inputVar inputExts (return emptySM)
                         line <- hGetLine hout
                         let nextPeriod = 
-                                (when (not isSilent) $ putStrLn line) >> 
+                                (unless isSilent $ putStrLn line) >> 
                                     executePeriod nextInputExts inLines (n - 1)
                         -- Checking the compiler and interpreter.
                         if isInterpreted
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
@@ -9,7 +9,7 @@
 
 -- for specifying options
 import Data.Map (fromList) 
-import Data.Maybe (Maybe (..))
+--import Data.Maybe (Maybe (..))
 --import System.Random
 
 import Language.Copilot 
@@ -103,22 +103,7 @@
   trigger w "z0_trigger" (a <> b <> true)
   trigger w "z1_trigger" (d <> constW16 3 <> w)
 
--- If the temperature rises more than 2.3 degrees within 0.2 seconds, then the
--- engine is immediately shut off.  From the paper.
-engine :: Streams
-engine = do
-  -- external vars
-  let temp     = extF "temp"
-      shutoff  = extB "shutoff"
-  -- Copilot vars
-      temps    = varF "temps"
-      overTemp = varB "overTemp"
-      err  = varB "trigger"
 
-  temps    .= [0, 0, 0] ++ temp
-  overTemp .= drop 2 temps > 2.3 + temps
-  err  .= overTemp ==> shutoff
-
 -- | Sending over ports.
 distrib :: Streams
 distrib = do
@@ -132,6 +117,17 @@
   send "portA" (port 2) a 
   send "portB" (port 1) b 
 
+monitor :: Streams
+monitor = do
+  -- external variables
+  let word     = extW32 "rx"
+      arbiter  = extB "arbiter"
+  -- Copilot variables
+      words    = varW32 "words"
+      arbiters = varB "arbiters"
+  words   .=      [0] ++ mux arbiter word words
+  arbiters .= [False] ++ mux arbiter false arbiter
+
 -- greatest common divisor.
 gcd :: Word16 -> Word16 -> Streams
 gcd n0 n1 = do
@@ -174,25 +170,28 @@
 testCoercions :: Streams
 testCoercions = do
   let word = varW8 "word"
+      int = varI16 "int"
   word .= [1] ++ word * (-2)
-  let int = varI16 "int"
   int  .= 1 + cast word
 
 testCoercions2 :: Streams
 testCoercions2 = do
   let b = varB "b"
+      i = varI16 "i"
+      j = varI16 "j"
   b .= [True] ++ not b
-  let i = varI16 "i"
-  let j = varI16 "j"
   i .= cast j
   j .= 3
 
 testCoercions3 :: Streams
 testCoercions3 = do
   let x = varB "x"
-  x .= [True] ++ not x
-  let y = varI32 "y"
+      y = varI32 "y"
+      z = varI32 "z"
+  x .= [True, True] ++ not x
   y .= cast x + cast x
+--  z .= drop 1 (cast x)
+  z .= cast (not true)
 
 i8 :: Streams
 i8 = let v = varI8 "v" in v .= [0, 1] ++ v + 1 
@@ -285,6 +284,77 @@
 t11 = do
   let v = varB "v"
   v .= [False, True, False] ++ v
+
+tdiv :: Streams
+tdiv = do
+  let a = varW16 "a"
+      b = varW16 "b"
+  a .= [3] ++ a `div` 5
+  b .= [3] ++ a `mod` 5
+
+extT :: Streams
+extT = do
+  let x = extW16 "x"
+  let y = varW16 "y"
+  y .= x 
+
+-- Examples:
+interpretExtT :: Prelude.IO ()
+interpretExtT =
+  interpret extT 10 $ 
+    setE (emptySM {w16Map = fromList [("x", [8,9..])]})
+      baseOpts
+compileExtT :: P.IO ()
+compileExtT =
+  compile extT "extT" $ setCode (P.Just "#include \"mylib.h\"", P.Nothing) baseOpts
+
+-- Testing error checking for badly-formed external sampling.
+
+-- Should fail.
+extT2 :: Streams
+extT2 = do
+  let y = varW16 "y"
+      x = extW16 (fun "f" y)
+  y .= x 
+
+-- Should pass.
+extT3 :: Streams
+extT3 = do
+  let y = varW16 "y"
+      x = extW16 (fun "f" y)
+  y .= [3] ++ x 
+
+-- Should fail.
+extT4 :: Streams
+extT4 = do
+  let y = varW16 "y"
+      x = extArrW16 "arr" y
+      z = extW16 "z"
+      w = varW16 "w"
+  y .= z
+  w .= x
+
+-- Should fail.
+extT5 :: Streams
+extT5 = do
+  let y = varW16 "y"
+      x = extW16 (fun "f" y)
+      z = extW16 "z"
+      w = varW16 "w"
+  y .= z
+  w .= x
+
+-- Should work.
+extT6 :: Streams
+extT6 = do
+  let y = varW16 "y"
+      x = extArrW16 "arr" y
+      z = extW16 "z"
+      w = varW16 "w"
+  y .= [7] ++ z
+  w .= x
+
+
 
 -- test external idx before after and in the stream it references
 -- test multiple defs
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
@@ -6,8 +6,9 @@
 import qualified Prelude as P
 import Data.Map (fromList)
 
-import Language.Copilot
+import Language.Copilot hiding (check)
 import Language.Copilot.Libs.PTLTL
+import Language.Copilot.Libs.Vote
 
 -- Next examples are for testing of the ptLTL library
 
@@ -91,36 +92,41 @@
   t `ptltl` (alwaysBeen $ not a)
   e .= e1 ==> d
 
--- "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."
+-- "If the majority of the engine temperature probes exeeds 250 degrees, then
+-- the cooler is engaged and remains engaged until the majority of the engine
+-- temperature drops to 250 or below.  Otherwise, trigger an immediate shutdown
+-- of the engine."
 engine :: Streams
 engine = do
   -- external vars
-  let engineTemp = extW8 "engineTemp"
-      engineOff  = extB "engineOff"
-      coolerOn   = extB "coolerOn"
+  let t0       = extW8 "temp_probe_0"
+      t1       = extW8 "temp_probe_1"
+      t2       = extW8 "temp_probe_2"
+      cooler   = extB  "fan_status"
   -- Copilot vars
-      cnt        = varW8 "cnt"
-      temp       = varB "temp"
-      cooler     = varB "cooler"
-      off        = varB "off"
-      monitor    = varB "monitor"
+      maj      = varW8 "maj"
+      check    = varB  "maj_check"
+      overHeat = varB  "over_heat"
+      monitor  = varB  "monitor"
+  -- local vars
+      temps    = [t0, t1, t2]
+  maj      .= majority temps
+  check    .= aMajority temps maj
+  overHeat `ptltl` (        (cooler || (maj <= 250 && check)) 
+                    `since` (maj > 250))
+  monitor .= not overHeat
+  trigger monitor "shutoff_engine" void
 
-  temp    `ptltl` (alwaysBeen (engineTemp > 250))
-  cnt     .=      [0] ++ mux (temp && cnt < 10) (cnt + 1) cnt
-  off     .=      cnt >= 10 ==> engineOff
-  cooler  `ptltl` (coolerOn `since` engineOff)
-  monitor .=      off && cooler
 
-engineRun :: IO ()
-engineRun = 
+engineRun :: Bool -> IO ()
+engineRun b = if b then 
   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..])]
+    setE (emptySM { bMap  = fromList [("fan_status", replicate 3 False P.++ repeat False)]
+                  , w8Map = fromList [ ("temp_probe_0", [240,240..])
+                                     , ("temp_probe_1", [240,241..])
+                                     , ("temp_probe_2", [240,241..])
+                                     ]
                   }) 
     baseOpts
+  else compile engine "engine" $ setSim baseOpts
 
diff --git a/Language/Copilot/Examples/StatExamples.hs b/Language/Copilot/Examples/StatExamples.hs
--- a/Language/Copilot/Examples/StatExamples.hs
+++ b/Language/Copilot/Examples/StatExamples.hs
@@ -3,8 +3,6 @@
 import Prelude ()
 import Language.Copilot.Core
 import Language.Copilot.Language
-import Language.Copilot.Interface
-import Language.Copilot.PrettyPrinter
 import Language.Copilot.Libs.Statistics
 
 t0 :: Streams
diff --git a/Language/Copilot/Help.hs b/Language/Copilot/Help.hs
--- a/Language/Copilot/Help.hs
+++ b/Language/Copilot/Help.hs
@@ -50,9 +50,9 @@
   , "   (NaN), and that no uninitialized local variables are used.  The entry"
   , "   point of main() is assumed, and it is also assumed that main() can be"
   , "   unrolled at least n times, where n is an Int.  This command is thus"
-  , "   best used when generating a simulation program (i.e., the setPP flag"
-  , "   is not used when compiling).  For more information on the properties"  
-  , "   checked, see <http://www.cprover.org/cprover-manual/properties.shtml>."
+  , "   best used when generating a simulation program (see the setSim option)."  
+  , "   For more information on the properties checked, see"
+  , "   <http://www.cprover.org/cprover-manual/properties.shtml>."
   , ""
   , " > help "
   , "   Displays this help message."
@@ -106,39 +106,39 @@
   , "    is returned if the number is too small.  For any program, the number"
   , "    of ticks must be at least 2."
   , ""
-  , "  setPP :: (String, String) -> Options -> Options                       (c)"
-  , "    default: Nothing.  The default generates a main() function that calls"
-  , "    Copilot code to run simulations."
+  , "  setR :: Int -> Options -> Options                                     (t)"
+  , "    default: 0"
+  , "    Sets the seed for generating random Copilot specification during"
+  , "    testing."
   , ""
-  , "    Sets C code to pretty-print before and after the generated Copilot"
-  , "    code: the before code is the first element of the tuple and the after"
-  , "    code is the second element.  For writing ad-hoc C, please see"
+  , "  setCode :: (Maybe String, Maybe String) -> Options -> Options         (c)"
+  , "    default: (Nothing, Nothing)."
+  , "    To place arbitrary C code in the generated file.  The first element of"
+  , "    the pair is code to place above the generated code, and the second"
+  , "    element is code to place below.  For writing ad-hoc C, please see"
   , "    Language.Copilot.AdHocC (and please add to it and send patches!)."
   , "    For exmple, pre-code might include 'includes'.  Post-code might include"
-  , "    a custom main() function.  ('PP' stands for 'pretty-print'.)"  
-  , ""
-  , "    NOTE: when the pre-/post-code is anything but Nothing, the C compiler"
-  , "    is NOT called---we assume you're doing a custom build.  We do NOT"
-  , "    instrument your code with a 'main()' function simulator.  Use this"
-  , "    function to generate embedded programs."
+  , "    a custom main() function."  
   , "" 
+  , "  setSim :: Options -> Options                                          (c)"
+  , "    default: False"
+  , "    When used, generates a main() function in the generated C file that"
+  , "    includes a driver to call the scheduler to simulate the function and"
+  , "    print the reults to standard out.  Additionally, we attempt to compile"
+  , "    the code when setSim is used."
+  , ""
   , "  setArrs :: [(String,Int)] -> Options -> Options                       (c)"
   , "    default: Nothing" 
   , "    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."  
   , ""
-  , "  setO :: Name -> Options -> Options                                    (t)"
-  , "    default: \"copilotProgram\""
-  , "    Sets the name of the executable (e.g., -o) generated by the C"
-  , "    compiler."
   , ""
-  , ""
   , "EXAMPLES:"
   , "The following examples reference Copilot specs defined in"
   , "Language.Copilot.Examples.Examples."
   , ""
-  , " > interpret t0 50 noOpts"
+  , " > interpret t0 50 baseOpts"
   , "   Interprets t0 for 50 iterations."
   , ""
   , " > interpret t3 40"
@@ -149,24 +149,24 @@
   , "   Interpret t3 for 40 iterations, seeding the external variable \"ext\""
   , "   to [0,1,..], with 'Verbose' verbosity."
   , ""
-  , " > compile t1 \"t1\" noOpts"
+  , " > compile t1 \"t1\" baseOpts"
   , "   Compile Copilot spec t1 to t1.c, t1.h, and executable t1 in the default"
   , "   directory, /tmp/copilot/ .  This is compiled with a simulation main()"
   , ""
-  , " > compile t2 \"t2\" $ setC \"-O2\" $ setP 100"
+  , " > compile t2 \"t2\" $ setC \"-O2\" $ setP 100 baseOpts"
   , "   Compile Copilot spec t2 to t2.c, t2.h, and executable t2 in the default"
   , "   directory, /tmp/copilot/ , with optimization level -02 and period 100."
   , "   This is compiled with a simulation main()."
   , ""
-  , " > test 1000"
+  , " > test 1000 baseOpts"
   , "   Compare the compiler and interpreter for a randomly-generated Copilot"
   , "   spec for 1000 iterations."
   , ""
-  , " > Prelude.sequence_ [test 100 $ setR x | x <- [0..100]]"
-  , "   Compare the compiler and interpreter on 100 randomly-generated Copilot"
-  , "   specs, for 100 iterations each."
+  , " > Prelude.sequence_ [test 10 $ setR x baseOpts | x <- [0..100]]"
+  , "   Compare the compiler and interpreter on 100 random seeds generating"
+  , "   Copilot specs, for 10 iterations each."
   , ""
-  , " > verify \"foo.c\" n"
+  , " > verify \"foo.c\" n baseOpts"
   , "   Calls cbmc on foo.c (where foo.c is in the current directory) and"
   , "   unrolls the program n times."
   ]
diff --git a/Language/Copilot/Interface.hs b/Language/Copilot/Interface.hs
--- a/Language/Copilot/Interface.hs
+++ b/Language/Copilot/Interface.hs
@@ -3,8 +3,8 @@
 -- | Used by the end-user to easily give its arguments to dispatch.
 module Language.Copilot.Interface (
           Options(), baseOpts, test, interpret, compile, verify, interface
-        , help , setE, setC, setO, setP, setI, setPP, setN, setV, setR
-        , setDir, setGCC, setArrs, setClock, noOpts,
+        , help , setE, setC, setO, setP, setI, setCode, setN, setV, setR
+        , setDir, setGCC, setArrs, setClock, setSim,
         module Language.Copilot.Dispatch
     ) where
 
@@ -39,7 +39,8 @@
         optCName :: Name, -- ^ Name of the C file generated.
         optCompiler :: String, -- ^ The C compiler to use, as a path to the executable.
         optOutputDir :: String, -- ^ Where to place the output C files (.c, .h, and binary).
-        optPrePostCode :: Maybe (String, String), -- ^ Code to append above and below the C file.
+        optPrePostCode :: (Maybe String, Maybe String), -- ^ Code to append above and below the C file.
+        optSimulate :: Bool, -- ^ Do we want a simulation driver?
         optTriggers :: Triggers, -- ^ A list of Copilot variable C function name
                                  -- pairs.  The C funciton is called if the
                                  -- Copilot stream becomes True.  The Stream
@@ -53,7 +54,7 @@
                                     -- so we cannot declare them.  Passing in
                                     -- pairs containing the name of the array
                                     -- and it's size allows them to be
-                                    -- declared."
+                                    -- declared.
         optClock :: Maybe A.Clock  -- ^ Use the hardware clock to drive the timing of the program?
     }
 
@@ -71,7 +72,8 @@
         optCName = "copilotProgram",
         optCompiler = "gcc",
         optOutputDir = "./",
-        optPrePostCode = Nothing,
+        optPrePostCode = (Nothing, Nothing),
+        optSimulate = False,
         optTriggers = M.empty,
         optArrs = [],
         optClock = Nothing
@@ -79,12 +81,9 @@
 
 -- Functions for making it easier for configuring copilot in the frequent use cases
 
-noOpts :: Options -> Options
-noOpts = id
-
 test :: Int -> Options -> IO ()
 test n opts = 
-  interface $ setC "-Wall" $ setI $ setN n $ setV OnlyErrors $ opts 
+  interface $ setC "-Wall" $ setI $ setN n $ setV OnlyErrors $ setSim opts 
 
 interpret :: Streams -> Int -> Options -> IO ()
 interpret streams n opts = 
@@ -176,6 +175,7 @@
 setV :: Verbose -> Options -> Options
 setV v opts = opts {optVerbose = v}
 
+-- | Set the random seed for generating random `Copilot` specs.
 setR :: Int -> Options -> Options
 setR seed opts = opts {optRandomSeed = Just seed}
 
@@ -194,9 +194,13 @@
 
 -- | Sets the code to precede and follow the copilot specification
 -- If nothing, then code appropriate for communication with the interpreter is generated
-setPP :: (String, String) -> Options -> Options
-setPP pp opts = opts {optPrePostCode = Just pp}
+setCode :: (Maybe String, Maybe String) -> Options -> Options
+setCode pp opts = opts {optPrePostCode = pp}
 
+-- | Include simulation driver code (in a main() loop)?
+setSim :: Options -> Options
+setSim opts = opts {optSimulate = True}
+
 -- | The "main" function that dispatches.
 interface :: Options -> IO ()
 interface opts =
@@ -249,6 +253,7 @@
                 outputDir = optOutputDir opts,
                 compiler  = optCompiler opts,
                 prePostCode = optPrePostCode opts,
+                sim = optSimulate opts,
 --                triggers = optTriggers opts,
                 arrDecs = optArrs opts,
                 clock = optClock opts
diff --git a/Language/Copilot/Interpreter.hs b/Language/Copilot/Interpreter.hs
--- a/Language/Copilot/Interpreter.hs
+++ b/Language/Copilot/Interpreter.hs
@@ -10,10 +10,8 @@
 -- It takes a /Copilot/ specification, the values of the monitored values,
 -- and returns the values of the streams.
 interpretStreams :: StreamableMaps Spec -> Vars -> Vars
-interpretStreams streams moVs =
-    inVs
-    where 
-        inVs = mapStreamableMaps (\ _ -> interpret inVs moVs) streams
+interpretStreams streams moVs = inVs
+  where inVs = mapStreamableMaps (\ _ -> interpret inVs moVs) streams
 
 interpret :: forall a. Streamable a => Vars -> Vars -> Spec a -> [a]
 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
@@ -67,7 +67,7 @@
 -- Same risk with mod. Use div0 and mod0 if unsure.
 mod, div :: (Streamable a, A.IntegralE a) => Spec a -> Spec a -> Spec a
 mod = F2 P.mod A.mod_
-div = F2 P.mod A.div_
+div = F2 P.div A.div_
 
 -- | As mod and div, except that if the division would be by 0, the first
 -- argument is used as a default.
diff --git a/Language/Copilot/Language/Sampling.hs b/Language/Copilot/Language/Sampling.hs
--- a/Language/Copilot/Language/Sampling.hs
+++ b/Language/Copilot/Language/Sampling.hs
@@ -85,15 +85,15 @@
   extF = PVar A.Float
   extD = PVar A.Double
   -- for arrays 
-  extArrB = \fn idx -> PArr A.Bool (fn, idx)
-  extArrI8 = \fn idx -> PArr A.Int8 (fn, idx)
-  extArrI16 = \fn idx -> PArr A.Int16 (fn, idx)
-  extArrI32 = \fn idx -> PArr A.Int32 (fn, idx)
-  extArrI64 = \fn idx -> PArr A.Int64 (fn, idx)
-  extArrW8 = \fn idx -> PArr A.Word8 (fn, idx)
-  extArrW16 = \fn idx -> PArr A.Word16 (fn, idx)
-  extArrW32 = \fn idx -> PArr A.Word32 (fn, idx)
-  extArrW64 = \fn idx -> PArr A.Word64 (fn, idx)
-  extArrF = \fn idx -> PArr A.Float (fn, idx)
-  extArrD = \fn idx -> PArr A.Double (fn, idx)
+  extArrB = curry (PArr A.Bool)
+  extArrI8 = curry (PArr A.Int8)
+  extArrI16 = curry (PArr A.Int16)
+  extArrI32 = curry (PArr A.Int32)
+  extArrI64 = curry (PArr A.Int64)
+  extArrW8 = curry (PArr A.Word8)
+  extArrW16 = curry (PArr A.Word16)
+  extArrW32 = curry (PArr A.Word32)
+  extArrW64 = curry (PArr A.Word64)
+  extArrF = curry (PArr A.Float)
+  extArrD = curry (PArr A.Double)
 
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
@@ -2,9 +2,10 @@
 -- the number of periods over which to compute the statistic (@n == 1@ computes
 -- it only over the current period). 
 
-module Language.Copilot.Libs.Statistics(max, min, sum, mean) where
+module Language.Copilot.Libs.Statistics
+    (max, min, sum, mean, meanNow) where
 
-import Prelude (Int, ($), foldl1, fromIntegral)
+import Prelude (Int, ($), foldl1, fromIntegral, foldl, error, length)
 --import qualified Prelude as P 
 
 import qualified Language.Atom as A
@@ -39,5 +40,11 @@
 mean n s = 
   nOneChk "mean" n $ (sum n s) / (fromIntegral n)
 
--- majority :: (Streamable a, A.NumE a) => Int -> Spec a -> Spec a
--- majority n s =
+-- | Mean value over the current set of specs passed in.
+meanNow :: (Streamable a, A.IntegralE a) => [Spec a] -> Spec a
+meanNow [] = error 
+    "Error in majority: list of arguments must be nonempty."
+meanNow ls = 
+  (foldl (+) 0 ls) `div` (fromIntegral $ length ls)
+
+
diff --git a/Language/Copilot/Libs/Vote.hs b/Language/Copilot/Libs/Vote.hs
new file mode 100644
--- /dev/null
+++ b/Language/Copilot/Libs/Vote.hs
@@ -0,0 +1,76 @@
+-- | Voting algorithms over streams of data.
+
+module Language.Copilot.Libs.Vote 
+    (majority, aMajority, ftAvg) where
+
+import Prelude 
+  ( ($), fromIntegral, error, length, otherwise
+  , Bounded(..), maxBound, minBound, Int)
+import Data.List (replicate, foldl')
+import qualified Prelude as P 
+import Data.Word
+
+import Language.Copilot.Language
+import Language.Copilot.Core
+import qualified Language.Atom as A
+
+-- | Boyer-Moore linear majority algorithm.  Warning!  Returns an arbitary
+-- element if no majority is returned.  See 'aMajority' below.
+majority :: (Streamable a, A.EqE a) => [Spec a] -> Spec a
+majority [] = 
+  error "Error in majority: list of arguments must be nonempty."
+majority ls = majority' ls (const unit) 0
+
+majority' :: (Streamable a, A.EqE a) 
+          => [Spec a] -> Spec a -> Spec Word32 -> Spec a
+majority' [] candidate _ = candidate
+majority' (x:xs) candidate cnt = 
+  majority' xs (mux (cnt == 0) x candidate)
+               (mux (cnt == 0 || x == candidate) (cnt + 1) (cnt - 1))
+
+aMajority :: (Streamable a, A.EqE a) => [Spec a] -> Spec a -> Spec Bool
+aMajority [] _ = 
+  error "Error in aMajority: list of arguments must be nonempty."
+aMajority ls candidate = 
+    (foldl' (\cnt x -> mux (x == candidate)
+                           (cnt + 1)
+                           cnt :: Spec Word32
+            ) 0 ls
+    ) * 2
+  > (fromIntegral $ length ls)
+
+-- | Fault-tolerant average.  Throw away the bottom and top @n@ elements and
+-- take the average of the rest.  Return an error if there are less than @2 * n
+-- + 1@ elements in the list.
+ftAvg :: (Streamable a, A.IntegralE a, Bounded a) => [Spec a] -> Int -> Spec a
+ftAvg ls n | length ls P.<= 2 P.* n = 
+  error $      "Error in ftAvg: list of arguments must be at least " 
+          P.++ P.show (2 * n + 1) P.++ "."
+           | otherwise =       (ftAvg' ls (replicate n low) (replicate n high) 0)
+                         `div` (fromIntegral $ length ls P.- (2 P.* n))
+  where low = const maxBound
+        high = const minBound
+
+-- | Return the total sum of values, minus the high and low values.
+ftAvg' :: (Streamable a, A.IntegralE a, Bounded a) 
+       => [Spec a] -> [Spec a] -> [Spec a] -> Spec a -> Spec a
+ftAvg' [] lows highs sum = foldl' (-) sum (lows P.++ highs)
+ftAvg' (x:xs) lows highs sum = 
+  ftAvg' xs (insert (<) lows x) (insert (>) highs x) (sum + x)
+
+-- | Insert an element into an ordered list.
+-- insert :: (Streamable a, A.OrdE a) 
+--        => (Spec a -> Spec a -> Spec Bool) 
+--        -> [Spec a] -> Spec a -> Int -> [Spec a]
+-- insert _ xs _ idx   | idx P.== length xs = []
+-- insert ord xs x idx | otherwise =
+--   let n = xs !! idx
+--       choice = mux (x `ord` n) x n in
+--   choice : insert ord xs choice (idx + 1)
+insert :: (Streamable a, A.OrdE a) 
+       => (Spec a -> Spec a -> Spec Bool) 
+       -> [Spec a] -> Spec a -> [Spec a]
+insert _ [] _ = []
+insert ord (n:ns) x = 
+  let pred = x `ord` n in
+  mux pred x n : insert ord ns (mux pred n x) 
diff --git a/copilot.cabal b/copilot.cabal
--- a/copilot.cabal
+++ b/copilot.cabal
@@ -1,5 +1,5 @@
 name:                copilot
-version:             1.0
+version:             1.0.1
 cabal-version:       >= 1.2
 license:             BSD3
 license-file:        LICENSE
@@ -32,11 +32,11 @@
 extra-source-files:  README
 
 library
-    ghc-options:     -Wall 
+    ghc-options:     -Wall
     -- These build depends represent my current system.  This will probably
-    -- build on packages outside these constaints.
+    -- build on packages outside these constraints.
     build-depends:     
-                       base >= 4.2 && < 6
+                       base >= 4.0 && < 6
                      , atom >= 1.0.8
                      , containers >= 0.2.0.1
                      , process >= 1.0.0.0
@@ -68,6 +68,7 @@
                      Language.Copilot.Libs.LTL
                      Language.Copilot.Libs.Indexes
                      Language.Copilot.Libs.Statistics
+                     Language.Copilot.Libs.Vote
                      Language.Copilot.Examples.Examples
                      Language.Copilot.Examples.LTLExamples
                      Language.Copilot.Examples.PTLTLExamples