copilot-libraries 2.1.1 → 2.2.0

raw patch · 11 files changed

+386/−120 lines, 11 filesdep ~copilot-languagePVP ok

version bump matches the API change (PVP)

Dependency ranges changed: copilot-language

API changes (from Hackage documentation)

Files

• copilot-libraries.cabal +5/−4
• src/Copilot/Library/Clocks.hs +39/−21
• src/Copilot/Library/LTL.hs +28/−14
• src/Copilot/Library/Libraries.hs +4/−5
• src/Copilot/Library/MTL.hs +168/−0
• src/Copilot/Library/PTLTL.hs +13/−9
• src/Copilot/Library/RegExp.hs +12/−1
• src/Copilot/Library/Stacks.hs +53/−25
• src/Copilot/Library/Statistics.hs +6/−5
• src/Copilot/Library/Utils.hs +18/−19
• src/Copilot/Library/Voting.hs +40/−17

@@ -1,8 +1,7 @@ cabal-version:       >=1.10 name:                copilot-libraries-version:             2.1.1-synopsis:            A Haskell-embedded DSL for monitoring hard real-time-                     distributed systems.+version:             2.2.0+synopsis:            Libraries for the Copilot language. description:   Libraries for the Copilot language.   .@@ -19,6 +18,7 @@ license-file:        LICENSE author:              Lee Pike, Robin Morisset, Alwyn Goodloe, Sebastian Niller,                      Nis Nordby Wegmann+homepage:            https://github.com/leepike/copilot-libraries maintainer:          leepike@gmail.com stability:           Experimental category:            Language, Embedded@@ -37,7 +37,7 @@     array,     base >= 4.0 && <= 5.0,     containers,-    copilot-language,+    copilot-language == 2.2.0,     parsec >= 2.0,     mtl >= 2.0 @@ -51,6 +51,7 @@     , Copilot.Library.Utils     , Copilot.Library.Voting     , Copilot.Library.Stacks+    , Copilot.Library.MTL    ghc-options:     -fwarn-tabs

@@ -1,45 +1,61 @@------------------------------------------------------------------------------------ Copyright © 2011 National Institute of Aerospace / Galois, Inc.------------------------------------------------------------------------------------- | A library that generates new clocks based on a base period.--- Usage, supposing @v@ is a Copilot variable, then+-- | +-- Module: Clocks+-- Description: Clocks based on a base period and phase+-- Copyright: (c) 2011 National Institute of Aerospace / Galois, Inc.+--+-- This library generates new clocks based on a base period and phase.+--+-- = Example Usage+-- +-- Also see @Examples/ClockExamples.hs@ in the+-- <https://github.com/leepike/Copilot/tree/master/Examples Copilot repository>.+-- -- @--- clk ( period 3 ) ( phase 1 )+--     'clk' ( 'period' 3 ) ( 'phase' 1 ) -- @+-- -- is equivalent to a stream of values like:+-- -- @--- cycle [False, True, False]+--     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+--     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. +{-# LANGUAGE NoImplicitPrelude #-}+ module Copilot.Library.Clocks   ( clk, clk1, period, phase ) where -import Prelude ( Integral, fromIntegral, ($))+import Prelude () import qualified Prelude as P import Copilot.Language  data ( Integral a ) => Period a = Period a data ( Integral a ) => Phase  a = Phase  a +-- | Constructor for a 'Period'. Note that period must be greater than 0. period :: ( Integral a ) => a -> Period a period = Period +-- | Constructor for a 'Phase'. Note that phase must be greater than or equal+-- to 0, and must be less than the 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+-- | Generate a clock that counts every @n@ ticks, starting at tick @m@, by+-- using an array of size @n@.+clk :: ( Integral a ) =>+       Period a       -- ^ Period @n@ of clock+       -> Phase a     -- ^ Phase @m@ of clock+       -> Stream Bool -- ^ Clock signal - 'True' on clock ticks, 'False' otherwise clk ( Period period' ) ( Phase phase' ) = clk'   where clk' = if period' P.< 1 then                    badUsage ( "clk: clock period must be 1 or greater" )@@ -54,10 +70,12 @@                                    ++ 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+-- | This follows the same convention as 'clk', but uses a counter variable of+-- integral type /a/ rather than an array.+clk1 :: ( Integral a, Typed a ) =>+        Period a       -- ^ Period @n@ of clock+        -> Phase a     -- ^ Phase @m@ of clock+        -> Stream Bool -- ^ Clock signal - 'True' on clock ticks, 'False' otherwise clk1 ( Period period' ) ( Phase phase' ) =     if period' P.< 1 then         badUsage ( "clk1: clock period must be 1 or greater" )

@@ -1,24 +1,31 @@------------------------------------------------------------------------------------ Copyright © 2011 National Institute of Aerospace / Galois, Inc.------------------------------------------------------------------------------------- | Bounded Linear Temporal Logic (LTL) operators.  For a bound @n@, a property+-- | +-- Module: LTL+-- Description: Bounded Linear Temporal Logic (LTL) operators+-- Copyright: (c) 2011 National Institute of Aerospace / Galois, Inc.+--+-- 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+--   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:+-- /Interface:/ See @Examples/LTLExamples.hs@ in the+-- <https://github.com/leepike/Copilot/tree/master/Examples Copilot repository>.+-- +-- 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.+-- variable.  In general, the "Copilot.Library.PTLTL" library is probably more useful.  {-# LANGUAGE NoImplicitPrelude #-} @@ -26,24 +33,25 @@   ( 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.+-- 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+-- 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 ...@@ -57,18 +65,23 @@ -- 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 :: ( Integral a ) =>+              a -- ^ 'n'+              -> Stream Bool -- ^ 's'+              -> 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+until 0 _ s1 = s1+until n s0 s1 = foldl (||) s1 v0     where n' = fromIntegral n           v0 = [ always ( i :: Int ) s0 && drop ( i + 1 ) s1                | i <- [ 0 .. n' - 1 ]@@ -78,6 +91,7 @@ -- | @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 0 _ s1 = s1 release n s0 s1 = always n s1 || foldl1 (||) v0     where n' = fromIntegral n           v0 = [ always ( i :: Int ) s1 && drop i s0

@@ -1,8 +1,7 @@------------------------------------------------------------------------------------ Copyright © 2011 National Institute of Aerospace / Galois, Inc.------------------------------------------------------------------------------------- | Main import module for the front-end lanugage.+-- | +-- Module: Libraries+-- Description: Main import module for libraries+-- Copyright: (c) 2011 National Institute of Aerospace / Galois, Inc.  module Copilot.Library.Libraries (     module Copilot.Library.Clocks

@@ -0,0 +1,168 @@+-- Metric Temporal Logic (MTL) operators over a discrete time+-- domain consisting of sampled time values++module Copilot.Library.MTL+  ( eventually, eventuallyPrev, always, alwaysBeen,+    until, release, since, Copilot.Library.MTL.trigger, matchingUntil,+    matchingRelease, matchingSince, matchingTrigger ) where++import Copilot.Language+import qualified Prelude as P+import Copilot.Library.Utils++-- It is necessary to provide a positive number of time units+-- dist to each function, where the distance between the times+-- of any two adjacent clock samples is no less than dist++-- Eventually: True at time t iff s is true at some time t',+-- where (t + l) <= t' <= (t + u)+eventually :: ( Typed a, Integral a ) =>+  a -> a -> Stream a -> a -> Stream Bool -> Stream Bool+eventually l u clk dist s = res clk s $ (u `P.div` dist) + 1+  where+  mins = clk + (constant l)+  maxes = clk + (constant u)+  res _ _ 0 = false+  res c s k =+    c <= maxes && ((mins <= c && s) || nextRes c s k)+  nextRes c s k = res (drop 1 c) (drop 1 s) (k - 1)++-- EventuallyPrev: True at time t iff s is true at some time t',+-- where (t - u) <= t' <= (t - l)+eventuallyPrev :: ( Typed a, Integral a ) =>+  a -> a -> Stream a -> a -> Stream Bool -> Stream Bool+eventuallyPrev l u clk dist s = res clk s $ (u `P.div` dist) + 1+  where+  mins = clk - (constant u)+  maxes = clk - (constant l)+  res _ _ 0 = false+  res c s k =+    mins <= c && ((c <= maxes && s) || nextRes c s k)+  nextRes c s k = res ([0] ++ c) ([False] ++ s) (k - 1)++-- Always: True at time t iff s is true at all times t'+-- where (t + l) <= t' <= (t + u)+always :: ( Typed a, Integral a ) =>+  a -> a -> Stream a -> a -> Stream Bool -> Stream Bool+always l u clk dist s = res clk s $ (u `P.div` dist) + 1+  where +  mins = clk + (constant l)+  maxes = clk + (constant u)+  res _ _ 0 = true +  res c s k = +    c > maxes || ((mins <= c ==> s) && nextRes c s k)+  nextRes c s k = res (drop 1 c) (drop 1 s) (k - 1)++-- AlwaysBeen: True at time t iff s is true at all times t'+-- where (t - u) <= t' <= (t - l)+alwaysBeen :: ( Typed a, Integral a ) =>+  a -> a -> Stream a -> a -> Stream Bool -> Stream Bool+alwaysBeen l u clk dist s = res clk s $ (u `P.div` dist) + 1+  where+  mins = clk - (constant u)+  maxes = clk - (constant l)+  res _ _ 0 = true+  res c s k =+    c < mins || ((c <= maxes ==> s) && nextRes c s k)+  nextRes c s k = res ([0] ++ c) ([True] ++ s) (k - 1)++-- Until: True at time t iff there exists a d with l <= d <= u+-- such that s1 is true at time (t + d),+-- and for all times t' with t <= t' < t + d, s0 is true+until :: ( Typed a, Integral a ) =>+  a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool+until l u clk dist s0 s1 = res clk s0 s1 $ (u `P.div` dist) + 1+  where+  mins = clk + (constant l)+  maxes = clk + (constant u)+  res _ _ _ 0 = false+  res c s s' k =+    c <= maxes && ((mins <= c && s') || (s && nextRes c s s' k))+  nextRes c s s' k = res (drop 1 c) (drop 1 s) (drop 1 s') (k - 1)++-- Since: True at time t iff there exists a d with l <= d <= u+-- such that s1 is true at time (t - d),+-- and for all times t' with t - d < t' <= t, s0 is true+since :: ( Typed a, Integral a ) =>+  a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool+since l u clk dist s0 s1 = res clk s0 s1 $ (u `P.div` dist) + 1+  where+  mins = clk - (constant u)+  maxes = clk - (constant l)+  res _ _ _ 0 = false +  res c s s' k =+    mins <= c && ((c <= maxes && s') || (s && nextRes c s s' k))+  nextRes c s s' k = res ([0] ++ c) ([True] ++ s) ([False] ++ s') (k - 1)++-- Release: true at time t iff for all d with l <= d <= u where there+-- is a sample at time (t + d), s1 is true at time (t + d),+-- or s0 has a true sample at some time t' with t <= t' < t + d+release :: ( Typed a, Integral a ) =>+  a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool+release l u clk dist s0 s1 =+  (mins > clk || clk > maxes || s1) &&+  (res (drop 1 clk) s0 (drop 1 s1) $ u `P.div` dist)+  where+  mins = clk + (constant l)+  maxes = clk + (constant u)+  res _ _ _ 0 = true+  res c s s' k =+    s || ((mins > c || c > maxes || s') && nextRes c s s' k)+  nextRes c s s' k = res (drop 1 c) (drop 1 s) (drop 1 s') (k - 1)++-- Trigger: True at time t iff for all d with l <= d <= u where there+-- is a sample at time (t - d), s1 is true at time (t - d),+-- or s0 has a true sample at some time t' with t - d < t' <= t +trigger :: ( Typed a, Integral a ) =>+  a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool+trigger l u clk dist s0 s1 =+  (mins > clk || clk > maxes || s1) &&+  (res ([0] ++ clk) s0 ([True] ++ s1) $ u `P.div` dist)+  where+  mins = clk - (constant u)+  maxes = clk - (constant l)+  res _ _ _ 0 = true+  res c s s' k =+    s || ((mins > c || c > maxes || s') && nextRes c s s' k)+  nextRes c s s' k = res ([0] ++ c) ([False] ++ s) ([True] ++ s') (k - 1)++-- Matching Variants++-- Matching Until: Same semantics as Until, except with both s1 and s0+-- needing to hold at time (t + d) instead of just s1+matchingUntil :: ( Typed a, Integral a ) =>+  a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool+matchingUntil l u clk dist s0 s1 = res clk s0 s1 $ (u `P.div` dist) + 1+  where+  mins = clk + (constant l)+  maxes = clk + (constant u)+  res _ _ _ 0 = false+  res c s s' k =+    c <= maxes && s && ((mins <= c && s') || nextRes c s s' k)+  nextRes c s s' k = res (drop 1 c) (drop 1 s) (drop 1 s') (k - 1)++-- Matching Since: Same semantics as Since, except with both s1 and s0+-- needing to hold at time (t - d) instead of just s1+matchingSince :: ( Typed a, Integral a ) =>+  a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool+matchingSince l u clk dist s0 s1 = since l u clk dist s0 (s0 && s1)++-- Matching Release: Same semantics as Release, except with+-- s1 or s0 needing to hold at time (t + d) instead of just s1+matchingRelease :: ( Typed a, Integral a ) =>+  a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool+matchingRelease l u clk dist s0 s1 = res clk s0 s1 $ (u `P.div` dist) + 1+  where+  mins = clk + (constant l)+  maxes = clk + (constant u)+  res _ _ _ 0 = true+  res c s s' k =+    s || ((mins > c || c > maxes || s') && nextRes c s s' k)+  nextRes c s s' k = res (drop 1 c) (drop 1 s) (drop 1 s') (k - 1)++-- Matching Trigger: Same semantics as Trigger, except with+-- s1 or s0 needing to hold at time (t - d) instead of just s1+matchingTrigger :: ( Typed a, Integral a ) =>+  a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool+matchingTrigger l u clk dist s0 s1 =+  Copilot.Library.MTL.trigger l u clk dist s0 (s0 || s1)

@@ -1,23 +1,27 @@------------------------------------------------------------------------------------ Copyright © 2011 National Institute of Aerospace / Galois, Inc.------------------------------------------------------------------------------------- | Provides past-time linear-temporal logic (ptLTL operators).+-- | +-- Module: PTLTL+-- Description: Past-Time Linear-Temporal Logic+-- Copyright: (c) 2011 National Institute of Aerospace / Galois, Inc. ----- Interface: see Examples/PTLTLExamples.hs.+-- Provides past-time linear-temporal logic (ptLTL operators).+--+-- /Interface:/ See @Examples/PTLTLExamples.hs@ in the+-- <https://github.com/leepike/Copilot/tree/master/Examples Copilot repository>.+-- -- You can embed a ptLTL specification within a Copilot specification using -- the form:+-- -- @ --   operator stream -- @ +{-# LANGUAGE NoImplicitPrelude #-}+ module Copilot.Library.PTLTL     ( since, alwaysBeen, eventuallyPrev, previous ) where --import Prelude ( ($) )+import Prelude () import Copilot.Language-  -- | Did @s@ hold in the previous period? previous :: Stream Bool -> Stream Bool

@@ -1,4 +1,15 @@--- | A regular expression librariy.+{-# LANGUAGE FlexibleContexts #-}+-- | +-- Module: RegExp+-- Description: Regular expression library+-- Copyright: (c) 2011 National Institute of Aerospace / Galois, Inc.+--+-- A regular expression library.+--+-- For examples, see @Examples/RegExpExamples.hs@ in the+-- <https://github.com/leepike/Copilot/tree/master/Examples Copilot repository>.++{-# LANGUAGE FlexibleContexts #-}  module Copilot.Library.RegExp ( copilotRegexp, copilotRegexpB ) where 

@@ -1,8 +1,38 @@------------------------------------------------------------------------------------ Copyright © 2011 National Institute of Aerospace / Galois, Inc.------------------------------------------------------------------------------------- | Stack machine.+-- | +-- Module: Stacks+-- Description: Stream for a stack machine+-- Copyright: (c) 2011 National Institute of Aerospace / Galois, Inc.+-- +-- This is a stream for a stack machine.+--+-- The stack is created from a specified depth, a specified start value, and+-- three input streams:+--+-- * a pop signal which pops off the stack when true,+-- * a push signal which pushes the value from the push stream onto the stack when true,+-- * a push stream.+-- The resultant stream is the top value of the stack.+--+-- In 'stack' the push signal takes priority over the pop signal in the event+-- that both are true in the same tick. This priority is reversed in 'stack''.+-- +-- Here is an example sequence with one stack of each type, both depth 3 and+-- starting value 0:+--+-- @ +-- popSignal:   pushSignal:  pushValue:   stack:       stack':     +-- false        true         100          0            0           +-- false        true         101          100          100         +-- true         true         102          101          101         +-- true         false        103          100          102         +-- true         false        104          0            101         +-- true         false        105          0            100         +-- true         false        106          0            0           +-- @+-- +-- Note the difference at the 4th tick after /popSignal/ and /pushSignal/ were+-- both true.  Note also that one cannot pop the start value off the stack -+-- that is, the stack is never empty.  {-# LANGUAGE NoImplicitPrelude #-} @@ -11,25 +41,15 @@  import Copilot.Language -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 stream in which the pop signal has precedence over the push signal+-- in case both are true in the same tick+stack :: (Integral a, Typed b) =>+         a              -- ^ Depth+         -> b           -- ^ Start value+         -> Stream Bool -- ^ Pop signal+         -> Stream Bool -- ^ Push signal+         -> Stream b    -- ^ Push stream+         -> Stream b    -- ^ Stack top stack depth startValue   popSignal pushSignal pushValue =   let depth'      = fromIntegral depth@@ -51,7 +71,15 @@     in toStack $ replicate depth' stackValue -+-- | Stack stream in which the push signal has precedence over the pop signal+-- in case both are true in the same tick+stack' :: (Integral a, Typed b) =>+         a              -- ^ Depth+         -> b           -- ^ Start value+         -> Stream Bool -- ^ Pop signal+         -> Stream Bool -- ^ Push signal+         -> Stream b    -- ^ Push stream+         -> Stream b    -- ^ Stack top stack' depth startValue   popSignal pushSignal pushValue =   let depth'      = fromIntegral depth

@@ -1,8 +1,9 @@------------------------------------------------------------------------------------ Copyright © 2011 National Institute of Aerospace / Galois, Inc.------------------------------------------------------------------------------------- | Basic bounded statistics.  In the following, a bound @n@ is given stating+-- | +-- Module: Statistics+-- Description: Basic bounded statistics+-- Copyright: (c) 2011 National Institute of Aerospace / Galois, Inc.+--+-- 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). 

@@ -1,20 +1,24 @@------------------------------------------------------------------------------------ Copyright © 2011 National Institute of Aerospace / Galois, Inc.------------------------------------------------------------------------------------- | Utility bounded-list functions (e.g., folds, scans, etc.)+-- | +-- Module: Utils+-- Description: Utility bounded-list functions (e.g., folds, scans, etc.)+-- Copyright: (c) 2011 National Institute of Aerospace / Galois, Inc.+--+-- Utility bounded-list functions (e.g., folds, scans, etc.)  module Copilot.Library.Utils-    ( take, tails, nfoldl, nfoldl1, nfoldr, nfoldr1,-      nscanl, nscanr, nscanl1, nscanr1,-      case', (!!), cycle ) +       ( -- * Functions similar to the Prelude functions on lists+         take, tails, cycle,+         -- ** Folds+         nfoldl, nfoldl1, nfoldr, nfoldr1,+         -- ** Scans+         nscanl, nscanr, nscanl1, nscanr1,+         -- ** Indexing+         case', (!!))  where  import Copilot.Language 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 .. ] ]@@ -24,9 +28,6 @@         => 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@@ -47,9 +48,6 @@                   ->   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 ]@@ -71,8 +69,8 @@ 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+-- | 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@@ -86,7 +84,8 @@   in case'' predicates alternatives  --- | Index.  WARNING: very expensive!  Consider using this only for very short lists.+-- | 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

@@ -1,17 +1,36 @@------------------------------------------------------------------------------------ Copyright © 2011 National Institute of Aerospace / Galois, Inc.------------------------------------------------------------------------------------- | An implementation of the Boyer-Moore Majority Vote Algorithm for Copilot.+-- | +-- Module: Voting+-- Description: Implementation of the Boyer-Moore Majority Vote Algorithm+-- Copyright: (c) 2011 National Institute of Aerospace / Galois, Inc. ----- For details of the Boyer-Moore Majority Vote Algorithm see the following--- papers:+-- This is an implementation of the Boyer-Moore Majority Vote Algorithm for+-- Copilot, which solves the majority vote problem in linear time and constant+-- memory in two passes. 'majority' implements the first pass, and 'aMajority'+-- the second pass. For details of the Boyer-Moore Majority Vote Algorithm see+-- the following papers: ----- * Wim H. Hesselink,--- \"The Boyer-Moore Majority Vote Algorithm\", 2005+-- * <http://www.cs.rug.nl/~wim/pub/whh348.pdf Wim H. Hesselink, \"The Boyer-Moore Majority Vote Algorithm\", 2005> ----- * Robert S. Boyer and J Strother Moore,--- \"MJRTY - A Fast Majority Vote Algorithm\", 1982+-- * <ftp://net9.cs.utexas.edu/pub/techreports/tr81-32.pdf Robert S. Boyer and J Strother Moore, \"MJRTY - A Fast Majority Vote Algorithm\", 1981>+--+-- In addition, <https://github.com/leepike/copilot-discussion/blob/master/tutorial/copilot_tutorial.pdf An Introduction to Copilot> in+-- <https://github.com/leepike/copilot-discussion copilot-discussion> explains+-- a form of this code in section 4.+--+-- For instance, with four streams passed to 'majority', and the candidate stream+-- then passed to 'aMajority':+--+-- @+-- vote1:       vote2:       vote3:       vote4:       majority:    aMajority:+-- 0            0            0            0            0            true+-- 1            0            0            0            0            true+-- 1            1            0            0            1            false+-- 1            1            1            0            1            true+-- 1            1            1            1            1            true+-- @+--+-- For other examples, see @Examples/VotingExamples.hs@ in the+-- <https://github.com/leepike/Copilot/tree/master/Examples Copilot repository>.  {-# LANGUAGE RebindableSyntax #-} @@ -21,9 +40,10 @@ import Copilot.Language import qualified Prelude as P -----------------------------------------------------------------------------------majority :: (P.Eq a, Typed a) => [Stream a] -> Stream a+-- | Majority vote first pass: choosing a candidate.+majority :: (P.Eq a, Typed a) =>+            [Stream a] -- ^ Vote streams+            -> Stream a -- ^ Candidate stream majority []     = badUsage "majority: empty list not allowed" majority (x:xs) = majority' xs x 1 @@ -40,9 +60,12 @@       where        inCnt cnt' = majority' xs can' cnt' -----------------------------------------------------------------------------------aMajority :: (P.Eq a, Typed a) => [Stream a] -> Stream a -> Stream Bool+-- | Majority vote second pass: checking that a candidate indeed has more than+-- half the votes.+aMajority :: (P.Eq a, Typed a) =>+             [Stream a] -- ^ Vote streams+             -> Stream a -- ^ Candidate stream+             -> Stream Bool -- ^ True if candidate holds majority aMajority [] _ = badUsage "aMajority: empty list not allowed" aMajority xs can =   let