diff --git a/copilot-libraries.cabal b/copilot-libraries.cabal --- a/copilot-libraries.cabal +++ b/copilot-libraries.cabal @@ -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 diff --git a/src/Copilot/Library/Clocks.hs b/src/Copilot/Library/Clocks.hs --- a/src/Copilot/Library/Clocks.hs +++ b/src/Copilot/Library/Clocks.hs @@ -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 +-- . +-- -- @ --- 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" ) diff --git a/src/Copilot/Library/LTL.hs b/src/Copilot/Library/LTL.hs --- a/src/Copilot/Library/LTL.hs +++ b/src/Copilot/Library/LTL.hs @@ -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 +-- . +-- +-- 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 diff --git a/src/Copilot/Library/Libraries.hs b/src/Copilot/Library/Libraries.hs --- a/src/Copilot/Library/Libraries.hs +++ b/src/Copilot/Library/Libraries.hs @@ -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 diff --git a/src/Copilot/Library/MTL.hs b/src/Copilot/Library/MTL.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Library/MTL.hs @@ -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) diff --git a/src/Copilot/Library/PTLTL.hs b/src/Copilot/Library/PTLTL.hs --- a/src/Copilot/Library/PTLTL.hs +++ b/src/Copilot/Library/PTLTL.hs @@ -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 +-- . +-- -- 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 diff --git a/src/Copilot/Library/RegExp.hs b/src/Copilot/Library/RegExp.hs --- a/src/Copilot/Library/RegExp.hs +++ b/src/Copilot/Library/RegExp.hs @@ -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 +-- . + +{-# LANGUAGE FlexibleContexts #-} module Copilot.Library.RegExp ( copilotRegexp, copilotRegexpB ) where diff --git a/src/Copilot/Library/Stacks.hs b/src/Copilot/Library/Stacks.hs --- a/src/Copilot/Library/Stacks.hs +++ b/src/Copilot/Library/Stacks.hs @@ -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 diff --git a/src/Copilot/Library/Statistics.hs b/src/Copilot/Library/Statistics.hs --- a/src/Copilot/Library/Statistics.hs +++ b/src/Copilot/Library/Statistics.hs @@ -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). diff --git a/src/Copilot/Library/Utils.hs b/src/Copilot/Library/Utils.hs --- a/src/Copilot/Library/Utils.hs +++ b/src/Copilot/Library/Utils.hs @@ -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 diff --git a/src/Copilot/Library/Voting.hs b/src/Copilot/Library/Voting.hs --- a/src/Copilot/Library/Voting.hs +++ b/src/Copilot/Library/Voting.hs @@ -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 +-- * -- --- * Robert S. Boyer and J Strother Moore, --- \"MJRTY - A Fast Majority Vote Algorithm\", 1982 +-- * +-- +-- In addition, in +-- 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 +-- . {-# 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