diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,29 @@
+2009
+BSD3 License terms
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+
+Redistributions of source code must retain the above copyright
+notice, this list of conditions and the following disclaimer.
+
+Redistributions in binary form must reproduce the above copyright
+notice, this list of conditions and the following disclaimer in the
+documentation and/or other materials provided with the distribution.
+
+Neither the name of the developers nor the names of its contributors
+may be used to endorse or promote products derived from this software
+without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE COPYRIGHT OWNER OR
+CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/copilot-libraries.cabal b/copilot-libraries.cabal
new file mode 100644
--- /dev/null
+++ b/copilot-libraries.cabal
@@ -0,0 +1,49 @@
+cabal-version:       >=1.10
+name:                copilot-libraries
+version:             0.1
+synopsis:            A Haskell-embedded DSL for monitoring hard real-time
+                     distributed systems.
+description:         Libraries for the Copilot language
+license:             BSD3
+license-file:        LICENSE
+author:              Lee Pike, Robin Morisset, Alwyn Goodloe, Sebastian Niller,
+                     Nis Nordby Wegmann
+maintainer:          niswegmann@gmail.com
+stability:           Experimental
+category:            Language, Embedded
+build-type:          Simple
+
+source-repository head
+    type:       git
+    location:   git://github.com/niswegmann/copilot-libraries.git
+
+library
+  default-language: Haskell2010
+
+  hs-source-dirs: src
+
+  build-depends:
+    array,
+    base >= 4.0 && < 5,
+    containers,
+    copilot-language,
+    parsec >= 2.0,
+    mtl >= 2.0
+
+  exposed-modules:
+    Copilot.Library.Clocks
+    Copilot.Library.LTL
+    Copilot.Library.PTLTL
+    Copilot.Library.Statistics
+    Copilot.Library.RegExp
+    Copilot.Library.Utils
+    Copilot.Library.Voting
+    Copilot.Library.Stacks
+
+  other-modules:
+
+  ghc-options:
+    -fwarn-tabs
+    -auto-all
+    -caf-all
+    -Wall
diff --git a/src/Copilot/Library/Clocks.hs b/src/Copilot/Library/Clocks.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Library/Clocks.hs
@@ -0,0 +1,73 @@
+-- | A library that generates new clocks based on a base period.
+-- Usage, supposing @v@ is a Copilot variable, then
+-- @
+-- clk ( period 3 ) ( phase 1 )
+-- @
+-- is equivalent to a stream of values like:
+-- @
+-- cycle [False, True, False]
+-- @
+-- that generates a stream of values
+-- @
+-- False True False False True False False True False ...
+-- 0     1    2     3     4    5     6     7    8
+-- @
+-- That is true every 3 ticks (the period) starting on the 1st tick (the phase).
+-- Constraints:
+-- The period must be greater than 0.
+-- The phase must be greater than or equal to 0.
+-- The phase must be less than the period.
+
+
+module Copilot.Library.Clocks
+  ( clk, clk1, period, phase ) where
+
+import Prelude ( Integral, fromIntegral, ($))
+import qualified Prelude as P
+import Copilot.Language
+import Data.Bool
+import Data.List (replicate)
+
+data ( Integral a ) => Period a = Period a
+data ( Integral a ) => Phase  a = Phase  a
+
+period :: ( Integral a ) => a -> Period a
+period = Period
+
+phase :: ( Integral a ) => a -> Phase a
+phase  = Phase
+
+-- clk generates a clock that counts n ticks by using an array of size n
+clk :: ( Integral a ) => Period a -> Phase a -> Stream Bool
+clk ( Period period' ) ( Phase phase' ) = clk'
+  where clk' = if period' P.< 1 then
+                   badUsage ( "clk: clock period must be 1 or greater" )
+               else if phase' P.< 0 then
+                        badUsage ( "clk: clock phase must be 0 or greater" )
+                    else if phase' P.>= period' then
+                             badUsage ( "clk: clock phase must be less than period")
+                         else replicate ( fromIntegral phase' ) False
+                              P.++ True : replicate
+                                   ( fromIntegral
+                                     $ period' P.- phase' P.- 1 ) False
+                                   ++ clk'
+
+
+-- clk1 generates a clock that counts n ticks by using a
+-- counter variable of integral type a
+clk1 :: ( Integral a, Typed a )
+        => Period a -> Phase a -> Stream Bool
+clk1 ( Period period' ) ( Phase phase' ) =
+    if period' P.< 1 then
+        badUsage ( "clk1: clock period must be 1 or greater" )
+    else if phase' P.< 0 then
+             badUsage ( "clk1: clock phase must be 0 or greater" )
+         else if phase' P.>= period' then
+                  badUsage ( "clk1: clock phase must be less than period")
+              else
+                  let counter = [ P.fromInteger 0 ]
+                                ++ mux ( counter /= ( constant $ 
+                                                        period' P.- 1 ) )
+                                       ( counter P.+ 1 )
+                                       ( 0 )
+                  in counter == fromIntegral phase'
diff --git a/src/Copilot/Library/LTL.hs b/src/Copilot/Library/LTL.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Library/LTL.hs
@@ -0,0 +1,81 @@
+-- | 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,
+-- @
+-- eventually 3 p
+-- @
+-- holds if @p@ holds at least once every four periods (3 transitions).
+--
+-- Interface: see Examples/LTLExamples.hs You can embed an LTL specification
+-- within a Copilot specification using the form:
+-- @
+--   operator spec
+-- @
+--
+-- 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.
+
+{-# LANGUAGE NoImplicitPrelude #-}
+
+module Copilot.Library.LTL
+  ( next, eventually, always, until, release ) where
+
+import Copilot.Language
+import Copilot.Language.Prelude
+import Copilot.Library.Utils
+
+
+-- | 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 :: Stream Bool -> Stream Bool
+next = drop ( 1 :: Int )
+
+
+-- | 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:
+-- @
+--      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 :: ( Integral a ) => a -> Stream Bool -> Stream Bool
+always n = nfoldl1 ( fromIntegral n + 1 ) (&&)
+
+
+-- | 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:
+-- @
+-- s => F F F T F F F T ...
+-- p => F T T T F T T T ...
+-- @
+eventually :: ( Integral a ) => a -> Stream Bool -> Stream Bool
+eventually n = nfoldl1 ( fromIntegral n + 1 ) (||)
+
+
+-- | @until n s0 s1@ means that @eventually n s1@, and up until at least the
+-- period before @s1@ holds, @s0@ continuously holds.
+until :: ( Integral a ) => a -> Stream Bool -> Stream Bool -> Stream Bool
+until n s0 s1 = foldl1 (||) v0
+    where n' = fromIntegral n
+          v0 = [ always ( i :: Int ) s0 && drop ( i + 1 ) s1
+               | i <- [ 0 .. n' - 1 ]
+               ]
+
+
+-- | @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 :: ( Integral a ) => a -> Stream Bool -> Stream Bool -> Stream Bool
+release n s0 s1 = always n s1 || foldl1 (||) v0
+    where n' = fromIntegral n
+          v0 = [ always ( i :: Int ) s1 && drop i s0
+               | i <- [ 0 .. n' - 1 ]
+               ]
diff --git a/src/Copilot/Library/PTLTL.hs b/src/Copilot/Library/PTLTL.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Library/PTLTL.hs
@@ -0,0 +1,39 @@
+-- | Provides past-time linear-temporal logic (ptLTL operators).
+--
+-- Interface: see Examples/PTLTLExamples.hs.
+-- You can embed a ptLTL specification within a Copilot specification using
+-- the form:
+-- @
+--   operator stream
+-- @
+
+module Copilot.Library.PTLTL
+    ( since, alwaysBeen, eventuallyPrev, previous ) where
+
+
+import Prelude ( ($) )
+import Copilot.Language
+import Data.Bool hiding ( (&&), (||) )
+
+
+-- | Did @s@ hold in the previous period?
+previous :: Stream Bool -> Stream Bool
+previous s = [ False ] ++ s
+
+
+-- | Has @s@ always held (up to and including the current state)?
+alwaysBeen :: Stream Bool -> Stream Bool
+alwaysBeen s = s && tmp
+    where tmp = [ True ] ++ s && tmp
+
+
+-- | Did @s@ hold at some time in the past (including the current state)?
+eventuallyPrev :: Stream Bool -> Stream Bool
+eventuallyPrev s = s || tmp
+  where tmp = [ False ] ++ s || tmp
+
+
+-- | Once @s2@ holds, in the following state (period), does @s1@ continuously hold?
+since ::  Stream Bool -> Stream Bool -> Stream Bool
+since s1 s2 = alwaysBeen ( tmp ==> s1 )
+    where tmp = eventuallyPrev $ [ False ] ++ s2
diff --git a/src/Copilot/Library/RegExp.hs b/src/Copilot/Library/RegExp.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Library/RegExp.hs
@@ -0,0 +1,402 @@
+module Copilot.Library.RegExp ( copilotRegexp, copilotRegexpB ) where
+
+
+import Text.ParserCombinators.Parsec
+  ( optional, (<|>), string, char, between, GenParser, many, choice, CharParser
+  , optionMaybe, chainr1, chainr, many1, digit, letter, eof, parse
+  , SourceName )
+import Data.Int
+import Data.Word
+import Data.List
+import Data.Char
+import Data.Maybe
+
+import Control.Monad.State ( evalState, get, modify )
+
+import qualified Copilot.Language as C
+
+-- The symbols in a regular expression, "Any" is any value of type t
+-- (matches any symbol, the "point" character in a regular expression).
+data Sym t = Any | Sym t
+             deriving ( Eq, Ord, Show )
+
+-- A symbol's value can occur multiple times in a regular expression,
+-- e.g. "t(tfft)*". A running number "symbolNum" is used to make all
+-- symbols in a regular expression unique.
+type NumT     = Int
+data NumSym t = NumSym { symbolNum :: Maybe NumT
+                       , symbol    :: Sym t
+                       } deriving ( Eq, Show )
+
+-- The regular expression data type. For our use
+-- regular expressions describing a language with
+-- no word is not supported since empty languages
+-- would not match anything and just yield a
+-- copilot stream of constant false values.
+data RegExp t = REpsilon
+              | RSymbol  ( NumSym t )
+              | ROr      ( RegExp t ) ( RegExp t )
+              | RConcat  ( RegExp t ) ( RegExp t )
+              | RStar    ( RegExp t )
+                deriving Show
+
+
+-- Parsers for single characters.
+lquote, rquote, lparen, rparen,
+  star, plus, qmark, point, minus,
+  nondigit :: CharParser () Char
+lquote = char '<'
+rquote = char '>'
+lparen = char '('
+rparen = char ')'
+star   = char '*'
+plus   = char '+'
+qmark  = char '?'
+point  = char '.'
+minus  = char '-'
+
+nondigit = char '_' <|> letter
+
+-- A "followedBy" combinator for parsing, parses
+-- p, then p' and returns the result of p.
+followedBy :: GenParser tok () a
+           -> GenParser tok () b
+           -> GenParser tok () a
+followedBy p p' = p >>= \ r -> p' >> return r
+
+
+-- Parsing a string p' with prefix p, returning
+-- both in order
+cPrefix, optCPrefix :: GenParser tok () Char
+                    -> GenParser tok () String
+                    -> GenParser tok () String
+cPrefix p p' = p  >>= \ c -> fmap ( c : ) p'
+
+-- Parsing a string p' with the character p as an
+-- optional prefix, return the result with the
+-- optional prefix.
+optCPrefix p p' = optionMaybe p
+                  >>= \ r -> case r of
+                               Nothing -> p'
+                               Just c  -> fmap ( c : ) p'
+
+-- The ci function ("case insensitive") takes one argument of
+-- type string, parses for the string in a case insensitive
+-- manner and yields the parsed string (preserving its case).
+ci :: String -> GenParser Char () String
+ci = mapM ( \ c -> ( char . toLower ) c <|> ( char . toUpper ) c )
+
+
+-- the parser for regular expressions
+regexp  :: ( SymbolParser t ) => GenParser Char () ( RegExp t )
+regexp  = chainr1 term opOr
+
+term    :: ( SymbolParser t ) => GenParser Char () ( RegExp t )
+term    = chainr factor opConcat REpsilon
+
+factor  :: ( SymbolParser t ) => GenParser Char () ( RegExp t )
+factor  = opSuffix factor'
+
+factor' :: ( SymbolParser t ) => GenParser Char () ( RegExp t )
+factor' = between lparen rparen regexp
+          <|> anySym
+          <|> parseSym
+
+-- Parses the "." - point character used to match any symbol.
+anySym  :: ( SymbolParser t ) => GenParser Char () ( RegExp t )
+anySym  = point >> ( return . RSymbol ) ( NumSym Nothing Any )
+
+
+class SymbolParser t where
+    parseSym :: GenParser Char () ( RegExp t )
+
+
+instance SymbolParser Bool where
+    parseSym = do { truth <- ( ci "t" >> optional ( ci "rue" )
+                               >> return True )
+                              <|> ( ci "f" >> optional ( ci "alse" )
+                                    >> return False )
+                              <|> ( string "1" >> return True )
+                              <|> ( string "0" >> return False )
+                  ; return $ RSymbol ( NumSym Nothing $ Sym truth )
+                  }
+
+
+parseWordSym :: ( Integral t )
+                => GenParser Char () ( RegExp t )
+parseWordSym = do { num <- between lquote rquote $ many1 digit
+                  ; return . RSymbol . NumSym Nothing . Sym
+                    $ fromIntegral ( read num :: Integer )
+                  }
+
+parseIntSym :: ( Integral t )
+                => GenParser Char () ( RegExp t )
+parseIntSym = do { num <- between lquote rquote $
+                          optCPrefix minus ( many1 digit )
+                 ; return . RSymbol . NumSym Nothing . Sym
+                   $ fromIntegral ( read num :: Integer )
+                 }
+
+
+type StreamName = String
+newtype P = P { getName :: StreamName }
+    deriving Eq
+
+
+parsePSym :: GenParser Char () ( RegExp P )
+parsePSym = do { pStream <- between lquote rquote $
+                            cPrefix nondigit ( many $ nondigit <|> digit )
+               ; return . RSymbol . NumSym Nothing . Sym
+                 $ P pStream
+               }
+
+
+instance SymbolParser Word8 where
+    parseSym = parseWordSym
+
+instance SymbolParser Word16 where
+    parseSym = parseWordSym
+
+instance SymbolParser Word32 where
+    parseSym = parseWordSym
+
+instance SymbolParser Word64 where
+    parseSym = parseWordSym
+
+instance SymbolParser Int8 where
+    parseSym = parseIntSym
+
+instance SymbolParser Int16 where
+    parseSym = parseIntSym
+
+instance SymbolParser Int32 where
+    parseSym = parseIntSym
+
+instance SymbolParser Int64 where
+    parseSym = parseIntSym
+
+instance SymbolParser P where
+    parseSym = parsePSym
+
+
+opOr       :: GenParser Char () ( RegExp t -> RegExp t -> RegExp t )
+opOr       = char '|' >> return ROr
+
+opConcat   :: GenParser Char () ( RegExp t -> RegExp t -> RegExp t )
+opConcat   = return RConcat
+
+opSuffix   :: GenParser Char () ( RegExp t )
+           -> GenParser Char () ( RegExp t )
+opSuffix r = do 
+  subexp   <- r
+  suffixes <- many $ choice [ star, plus, qmark ]
+  let transform rexp suffix =
+          case suffix of
+            '*'   -> RStar   rexp
+            '+'   -> RConcat rexp ( RStar rexp )
+            '?'   -> ROr     rexp   REpsilon
+            other -> C.badUsage ("in Regular Expression library: " ++
+                               "unhandled operator: " ++ show other)
+  return $ foldl transform subexp suffixes
+
+parser :: ( SymbolParser t )
+         => GenParser Char () ( RegExp t )
+parser = regexp `followedBy` eof
+
+
+hasEpsilon                    :: RegExp t -> Bool
+hasEpsilon   REpsilon         = True
+hasEpsilon ( RSymbol  _     ) = False
+hasEpsilon ( ROr      r1 r2 ) = hasEpsilon r1 || hasEpsilon r2
+hasEpsilon ( RConcat  r1 r2 ) = hasEpsilon r1 && hasEpsilon r2
+hasEpsilon ( RStar    _     ) = True
+
+
+first                    :: RegExp t -> [ NumSym t ]
+first   REpsilon         = []
+first ( RSymbol  s     ) = [ s ]
+first ( ROr      r1 r2 ) = first r1 ++ first r2
+first ( RConcat  r1 r2 ) = first r1 ++ if hasEpsilon r1 then
+                                           first r2 else []
+first ( RStar    r     ) = first r
+
+
+reverse'                   :: RegExp t -> RegExp t
+reverse' ( ROr     r1 r2 ) = ROr     ( reverse' r1 ) ( reverse' r2 )
+reverse' ( RConcat r1 r2 ) = RConcat ( reverse' r2 ) ( reverse' r1 )
+reverse' ( RStar   r     ) = RStar   ( reverse' r  )
+reverse'   e               = e
+
+
+last' :: RegExp t -> [ NumSym t ]
+last' = first . reverse'
+
+
+follow                        :: ( Eq t ) =>
+                                 RegExp t -> NumSym t -> [ NumSym t ]
+follow   REpsilon         _   = []
+follow ( RSymbol  _     ) _   = []
+follow ( ROr      r1 r2 ) sNr = follow r1 sNr ++ follow r2 sNr
+follow ( RConcat  r1 r2 ) sNr = follow r1 sNr ++ follow r2 sNr
+                                ++ if sNr `elem` last' r1 then
+                                       first r2 else []
+follow ( RStar    r     ) sNr = follow r sNr
+                                `union` if sNr `elem` last' r then
+                                            first r else []
+
+
+preceding :: ( Eq t ) => RegExp t -> NumSym t -> [ NumSym t ]
+preceding = follow . reverse'
+
+
+hasFinitePath                   :: RegExp t -> Bool
+hasFinitePath ( ROr     r1 r2 ) = hasFinitePath r1 || hasFinitePath r2
+hasFinitePath ( RConcat _  r2 ) = hasFinitePath r2
+hasFinitePath ( RStar   _     ) = False
+hasFinitePath   _               = True
+
+
+getSymbols                   :: RegExp t -> [ NumSym t ]
+getSymbols ( RSymbol s     ) = [ s ]
+getSymbols ( ROr     r1 r2 ) = getSymbols r1 ++ getSymbols r2
+getSymbols ( RConcat r1 r2 ) = getSymbols r1 ++ getSymbols r2
+getSymbols ( RStar   r     ) = getSymbols r
+getSymbols   _               = []
+
+
+-- assign each symbol in the regular expression a
+-- unique number, counting up from 0
+enumSyms   :: RegExp t -> RegExp t
+enumSyms rexp = evalState ( enumSyms' rexp ) 0
+    where
+      enumSyms' ( RSymbol s     ) = do
+        num <- get
+        modify ( + 1 )
+        return $ RSymbol s { symbolNum = Just num }
+      enumSyms' ( ROr     r1 r2 ) = do
+        r1' <- enumSyms' r1
+        r2' <- enumSyms' r2
+        return $ ROr r1' r2'
+      enumSyms' ( RConcat r1 r2 ) = do
+        r1' <- enumSyms' r1
+        r2' <- enumSyms' r2
+        return $ RConcat r1' r2'
+      enumSyms' ( RStar   r     ) = do
+        r'  <- enumSyms' r
+        return $ RStar   r'
+      enumSyms'   other           =
+        return other
+
+
+regexp2CopilotNFA :: ( C.Typed t, Eq t )
+                     => C.Stream t -> RegExp t -> C.Stream Bool -> C.Stream Bool
+regexp2CopilotNFA inStream rexp reset =
+    let symbols                    = getSymbols rexp
+        first'                     = first rexp
+        start                      = [ True ] C.++ C.false
+
+        preceding'   numSym        = let ps    = preceding rexp numSym
+                                         s     = if numSym `elem` first' then
+                                                   [ start ] else []
+                                     in s ++ [ streams !! i
+                                             | i <- map ( fromJust . symbolNum ) ps ]
+
+        matchesInput numSym        = case symbol numSym of
+                                       Any   -> C.true
+                                       Sym t -> inStream C.== C.constant t
+
+        transitions  numSym ps     = matchesInput numSym
+                                     C.&& ( foldl ( C.|| ) C.false ps )
+
+        stream       numSym        = let ps    = preceding' numSym
+                                         init_ = C.constant $ numSym `elem` first'
+                                     in C.mux reset
+                                        ( [ False ] C.++ matchesInput numSym C.&& init_ )
+                                        ( [ False ] C.++ transitions  numSym ps )
+
+        streams                    = map stream symbols
+
+        outStream                  = foldl ( C.|| ) start streams
+
+    in outStream
+
+
+copilotRegexp :: ( C.Typed t, SymbolParser t, Eq t )
+                 => C.Stream t -> SourceName -> C.Stream Bool -> C.Stream Bool
+copilotRegexp inStream rexp reset =
+  case parse parser rexp rexp of
+    Left  err -> C.badUsage ("parsing regular exp: " ++ show err)
+    Right rexp' -> let nrexp = enumSyms rexp' in
+        if hasFinitePath nrexp then
+            C.badUsage $
+            concat [ "The regular expression contains a finite path "
+                   , "which is something that will fail to match "
+                   , "since we do not have a distinct end-of-input "
+                   , "symbol on infinite streams." ]
+        else if hasEpsilon nrexp then
+                 C.badUsage $
+                 concat [ "The regular expression matches a language "
+                        , "that contains epsilon. This cannot be handled "
+                        , "on infinite streams, since we do not have "
+                        , "a distinct end-of-input symbol." ]
+             else regexp2CopilotNFA inStream nrexp reset
+
+
+regexp2CopilotNFAB :: RegExp P -> [ ( StreamName, C.Stream Bool ) ]
+                      -> C.Stream Bool -> C.Stream Bool
+regexp2CopilotNFAB rexp propositions reset =
+    let symbols                    = getSymbols rexp
+        first'                     = first rexp
+        start                      = [ True ] C.++ C.false
+
+        preceding'   numSym        = let ps    = preceding rexp numSym
+                                         s     = if numSym `elem` first' then
+                                                   [ start ] else []
+                                     in s ++ [ streams !! i
+                                             | i <- map ( fromJust . symbolNum ) ps ]
+
+        lookup' a l = case lookup a l of
+                        Nothing -> C.badUsage ("boolean stream "
+                                             ++ a
+                                             ++ " is not defined")
+                        Just s  -> s
+
+        matchesInput numSym        = case symbol numSym of
+                                       Any   -> C.true
+                                       Sym t -> lookup' ( getName t ) propositions
+
+        transitions  numSym ps     = matchesInput numSym
+                                     C.&& ( foldl ( C.|| ) C.false ps )
+
+        stream       numSym        = let ps    = preceding' numSym
+                                         init_ = C.constant $ numSym `elem` first'
+                                     in C.mux reset
+                                        ( [ False ] C.++ matchesInput numSym C.&& init_ )
+                                        ( [ False ] C.++ transitions  numSym ps )
+
+        streams                    = map stream symbols
+
+        outStream                  = foldl ( C.|| ) start streams
+
+    in outStream
+
+
+copilotRegexpB :: SourceName -> [ ( StreamName, C.Stream Bool ) ]
+                  -> C.Stream Bool -> C.Stream Bool
+copilotRegexpB rexp propositions reset =
+  case parse parser rexp rexp of
+    Left  err -> C.badUsage ("parsing regular exp: " ++ show err)
+    Right rexp' -> let nrexp = enumSyms rexp' in
+        if hasFinitePath nrexp then
+            C.badUsage $
+            concat [ "The regular expression contains a finite path "
+                   , "which is something that will fail to match "
+                   , "since we do not have a distinct end-of-input "
+                   , "symbol on infinite streams." ]
+        else if hasEpsilon nrexp then
+                 C.badUsage $
+                 concat [ "The regular expression matches a language "
+                        , "that contains epsilon. This cannot be handled "
+                        , "on infinite streams, since we do not have "
+                        , "a distinct end-of-input symbol." ]
+             else regexp2CopilotNFAB nrexp propositions reset
diff --git a/src/Copilot/Library/Stacks.hs b/src/Copilot/Library/Stacks.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Library/Stacks.hs
@@ -0,0 +1,71 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+
+module Copilot.Library.Stacks
+  ( stack, stack' ) where
+
+
+import Copilot.Language
+import Copilot.Language.Prelude
+
+
+type PushSignal    = Stream Bool
+type PopSignal     = Stream Bool
+type PushStream  a = Stream a
+type StackTop    a = Stream a
+
+
+-- stack and stack' streams
+--
+-- for the stack stream, the PopSignal has precedence
+-- over the PushSignal in case both are true in the same tick
+--
+-- for the stack' stream, the PushSignal has precedence
+-- over the PopSignal in case both are true in the same tick
+stack, stack' :: ( Integral a, Typed b )
+         => a -> b
+         -> PopSignal
+         -> PushSignal
+         -> PushStream b
+         -> StackTop   b
+stack depth startValue
+  popSignal pushSignal pushValue =
+  let depth'      = fromIntegral depth
+      startValue' = constant startValue
+      stackValue pushValue' popValue' =
+        let stackValue'  = [ startValue ]
+                           ++ mux popSignal
+                                  popValue'
+                                  ( mux pushSignal
+                                        pushValue'
+                                        stackValue' )
+        in  stackValue'
+      toStack l =
+        let toStack' _    []           = startValue'
+            toStack' prev ( sv : svs ) =
+              let current = sv prev ( toStack' current svs )
+              in  current
+        in toStack' pushValue l
+
+   in toStack $ replicate depth' stackValue
+
+
+stack' depth startValue
+  popSignal pushSignal pushValue =
+  let depth'      = fromIntegral depth
+      startValue' = constant startValue
+      stackValue pushValue' popValue' =
+        let stackValue'  = [ startValue ]
+                           ++ mux pushSignal
+                                  pushValue'
+                                  ( mux popSignal
+                                        popValue'
+                                        stackValue' )
+        in  stackValue'
+      toStack l =
+        let toStack' _    []           = startValue'
+            toStack' prev ( sv : svs ) =
+              let current = sv prev ( toStack' current svs )
+              in  current
+        in toStack' pushValue l
+
+   in toStack $ replicate depth' stackValue
diff --git a/src/Copilot/Library/Statistics.hs b/src/Copilot/Library/Statistics.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Library/Statistics.hs
@@ -0,0 +1,37 @@
+-- | Basic bounded statistics.  In the following, a bound @n@ is given stating
+-- the number of periods over which to compute the statistic (@n == 1@ computes
+-- it only over the current period).
+
+{-# LANGUAGE NoImplicitPrelude #-}
+
+module Copilot.Library.Statistics
+    ( max, min, sum, mean, meanNow ) where
+
+import Copilot.Language
+import Copilot.Language.Prelude
+import Copilot.Library.Utils
+
+-- | Summation.
+sum :: ( Typed a, Num a ) => Int -> Stream a -> Stream a
+sum n s = nfoldl1 n (+) s
+
+-- | Maximum value.
+max :: ( Typed a, Ord a ) => Int -> Stream a -> Stream a
+max n s = nfoldl1 n largest s
+    where largest  = \ x y -> mux ( x >= y ) x y
+
+-- | Minimum value.
+min :: ( Typed a, Ord a ) => Int -> Stream a -> Stream a
+min n s = nfoldl1 n smallest s
+    where smallest = \ x y -> mux ( x <= y ) x y
+
+-- | Mean value.  @n@ must not overflow
+-- for word size @a@ for streams over which computation is peformed.
+mean :: ( Typed a, Fractional a ) => Int -> Stream a -> Stream a
+mean n s = ( sum n s ) / ( fromIntegral n )
+
+-- | Mean value over the current set of streams passed in.
+meanNow :: ( Typed a, Integral a ) => [ Stream a ] -> Stream a
+meanNow [] = 
+  badUsage "list of arguments to meanNow must be nonempty"
+meanNow ls = ( foldl1 (+) ls ) `div` ( fromIntegral $ length ls )
diff --git a/src/Copilot/Library/Utils.hs b/src/Copilot/Library/Utils.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Library/Utils.hs
@@ -0,0 +1,107 @@
+module Copilot.Library.Utils
+    ( take, tails, nfoldl, nfoldl1, nfoldr, nfoldr1,
+      nscanl, nscanr, nscanl1, nscanr1,
+      case', (!!), cycle ) 
+where
+
+
+import Copilot.Language
+import Copilot.Language.Prelude 
+import qualified Prelude as P
+
+
+-- | functions similar to the Prelude functions on lists
+
+tails :: ( Typed a )
+         => Stream a -> [ Stream a ]
+tails s = [ drop x s | x <- [ 0 .. ] ]
+
+
+take :: ( Integral a, Typed b )
+        => a -> Stream b -> [ Stream b ]
+take n s = P.take ( fromIntegral n ) $ tails s
+
+
+-- Folds
+
+nfoldl :: ( Typed a, Typed b )
+          => Int -> ( Stream a -> Stream b -> Stream a )
+                 ->   Stream a -> Stream b -> Stream a
+nfoldl n f e s = foldl f e $ take n s
+
+nfoldl1 :: ( Typed a )
+           => Int -> ( Stream a -> Stream a -> Stream a )
+                  ->   Stream a -> Stream a
+nfoldl1 n f s = foldl1 f $ take n s
+
+nfoldr :: ( Typed a, Typed b )
+          => Int -> ( Stream a -> Stream b -> Stream b )
+                 ->   Stream b -> Stream a -> Stream b
+nfoldr n f e s = foldr f e $ take n s
+
+nfoldr1 :: ( Typed a )
+           => Int -> ( Stream a -> Stream a -> Stream a )
+                  ->   Stream a -> Stream a
+nfoldr1 n f s = foldr1 f $ take n s
+
+
+-- Scans
+
+nscanl :: ( Typed a, Typed b )
+          => Int -> ( Stream a -> Stream b -> Stream a )
+          -> Stream a -> Stream b -> [ Stream a ]
+nscanl n f e s = scanl f e $ take n s
+
+nscanr :: ( Typed a )
+          => Int -> ( Stream a -> Stream b -> Stream b )
+          -> Stream b -> Stream a -> [ Stream b ]
+nscanr n f e s = scanr f e $ take n s
+
+nscanl1 :: ( Typed a )
+           => Int -> ( Stream a -> Stream a -> Stream a )
+           -> Stream a -> [ Stream a ]
+nscanl1 n f s = scanl1 f $ take n s
+
+nscanr1 :: ( Typed a )
+           => Int -> ( Stream a -> Stream a -> Stream a )
+           -> Stream a -> [ Stream a ]
+nscanr1 n f s = scanr1 f $ take n s
+
+
+-- Case-like function, the index of the first predicate that is true
+-- in the predicate list selects the stream result, if no predicate
+-- is true, the last element is chosen (default element)
+case' :: ( Typed a )
+         => [ Stream Bool ] -> [ Stream a ] -> Stream a
+case' predicates alternatives =
+  let case'' []         ( default' : _ ) = default'
+      case'' ( p : ps ) ( a : as )       = mux p a ( case'' ps as )
+      case'' _          _                =
+        badUsage $ "in case' in Utils library: "
+                   P.++ "length of alternatives list is not "
+                   P.++ "greater by one than the length of predicates list"
+  in case'' predicates alternatives
+
+
+-- | Index.  WARNING: very expensive!  Consider using this only for very short lists.
+(!!) :: ( Typed a, Integral a )
+        => [ Stream a ] -> Stream a -> Stream a
+ls !! n = let indices      = map
+                             ( constant . fromIntegral )
+                             [ 0 .. P.length ls - 1 ]
+              select [] _  = last ls
+              select
+                ( i : is )
+                ( x : xs ) = mux ( i == n ) x ( select is xs )
+                             -- should not happen
+              select _ []  = badUsage ("in (!!) defined in Utils.hs " P.++ 
+                               "in copilot-libraries")
+          in if null ls then
+               badUsage ("in (!!) defined in Utils.hs " P.++ 
+                            "indexing the empty list with !! is not defined")
+             else
+               select indices ls
+
+cycle :: ( Typed a ) => [ a ] -> Stream a
+cycle ls = cycle'
+  where cycle' = ls ++ cycle'
diff --git a/src/Copilot/Library/Voting.hs b/src/Copilot/Library/Voting.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Library/Voting.hs
@@ -0,0 +1,55 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+-- | An implementation of the Boyer-Moore Majority Vote Algorithm for Copilot.
+--
+-- For details of the Boyer-Moore Majority Vote Algorithm see the following
+-- papers:
+--
+-- * Wim H. Hesselink,
+-- \"The Boyer-Moore Majority Vote Algorithm\", 2005
+--
+-- * Robert S. Boyer and J Strother Moore,
+-- \"MJRTY - A Fast Majority Vote Algorithm\", 1982
+
+{-# LANGUAGE RebindableSyntax #-}
+
+module Copilot.Library.Voting 
+  ( majority, aMajority ) where
+
+import Copilot.Language
+import Copilot.Language.Prelude
+import qualified Prelude as P
+
+--------------------------------------------------------------------------------
+
+majority :: (P.Eq a, Typed a) => [Stream a] -> Stream a
+majority []     = badUsage "majority: empty list not allowed"
+majority (x:xs) = majority' xs x 1
+
+majority' :: (P.Eq a, Typed a)
+   => [Stream a] -> Stream a -> Stream Word32 -> Stream a
+majority' []     can _   = can
+majority' (x:xs) can cnt =
+  local (cnt == 0) $ \ zero -> 
+    local (if zero then x else can) $ \ can' ->
+      local (if zero || x == can then cnt+1 else cnt-1) $ \ cnt' ->
+        majority' xs can' cnt'
+
+--------------------------------------------------------------------------------
+
+aMajority :: (P.Eq a, Typed a) => [Stream a] -> Stream a -> Stream Bool
+aMajority [] _ = badUsage "aMajority: empty list not allowed"
+aMajority xs can =
+  let
+    cnt = aMajority' 0 xs can
+  in
+    (cnt * 2) > fromIntegral (length xs)
+
+aMajority' :: (P.Eq a, Typed a)
+  => Stream Word32 -> [Stream a] -> Stream a -> Stream Word32
+aMajority' cnt []     _   = cnt
+aMajority' cnt (x:xs) can =
+  local (if x == can then cnt+1 else cnt) $ \ cnt' ->
+    aMajority' cnt' xs can