-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | A Haskell-embedded DSL for monitoring hard real-time distributed systems. -- -- Libraries for the Copilot language @package copilot-libraries @version 0.2 module Copilot.Library.Stacks stack, stack' :: (Integral a, Typed b) => a -> b -> PopSignal -> PushSignal -> PushStream b -> StackTop b -- | An implementation of the Boyer-Moore Majority Vote Algorithm for -- Copilot. -- -- For details of the Boyer-Moore Majority Vote Algorithm see the -- following papers: -- -- module Copilot.Library.Voting majority :: (Eq a, Typed a) => [Stream a] -> Stream a aMajority :: (Eq a, Typed a) => [Stream a] -> Stream a -> Stream Bool module Copilot.Library.RegExp copilotRegexp :: (Typed t, SymbolParser t, Eq t) => Stream t -> SourceName -> Stream Bool -> Stream Bool copilotRegexpB :: SourceName -> [(StreamName, Stream Bool)] -> Stream Bool -> Stream Bool instance Eq t => Eq (Sym t) instance Ord t => Ord (Sym t) instance Show t => Show (Sym t) instance Eq t => Eq (NumSym t) instance Show t => Show (NumSym t) instance Show t => Show (RegExp t) instance Eq P instance SymbolParser P instance SymbolParser Int64 instance SymbolParser Int32 instance SymbolParser Int16 instance SymbolParser Int8 instance SymbolParser Word64 instance SymbolParser Word32 instance SymbolParser Word16 instance SymbolParser Word8 instance SymbolParser Bool -- | 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 -- | Once s2 holds, in the following state (period), does -- s1 continuously hold? since :: Stream Bool -> Stream Bool -> Stream Bool -- | Has s always held (up to and including the current state)? alwaysBeen :: Stream Bool -> Stream Bool -- | Did s hold at some time in the past (including the current -- state)? eventuallyPrev :: Stream Bool -> Stream Bool -- | Did s hold in the previous period? previous :: Stream Bool -> Stream Bool module Copilot.Library.Utils take :: (Integral a, Typed b) => a -> Stream b -> [Stream b] -- | functions similar to the Prelude functions on lists tails :: Typed a => Stream a -> [Stream a] nfoldl :: (Typed a, Typed b) => Int -> (Stream a -> Stream b -> Stream a) -> Stream a -> Stream b -> Stream a nfoldl1 :: Typed a => Int -> (Stream a -> Stream a -> Stream a) -> Stream a -> Stream a nfoldr :: (Typed a, Typed b) => Int -> (Stream a -> Stream b -> Stream b) -> Stream b -> Stream a -> Stream b nfoldr1 :: Typed a => Int -> (Stream a -> Stream a -> Stream a) -> Stream a -> Stream a nscanl :: (Typed a, Typed b) => Int -> (Stream a -> Stream b -> Stream a) -> Stream a -> Stream b -> [Stream a] nscanr :: Typed a => Int -> (Stream a -> Stream b -> Stream b) -> Stream b -> Stream a -> [Stream b] nscanl1 :: Typed a => Int -> (Stream a -> Stream a -> Stream a) -> Stream a -> [Stream a] nscanr1 :: Typed a => Int -> (Stream a -> Stream a -> Stream a) -> Stream a -> [Stream a] case' :: Typed a => [Stream Bool] -> [Stream a] -> Stream a -- | Index. WARNING: very expensive! Consider using this only for very -- short lists. (!!) :: (Typed a, Integral a) => [Stream a] -> Stream a -> Stream a cycle :: Typed a => [a] -> Stream a -- | 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). module Copilot.Library.Statistics -- | Maximum value. max :: (Typed a, Ord a) => Int -> Stream a -> Stream a -- | Minimum value. min :: (Typed a, Ord a) => Int -> Stream a -> Stream a -- | Summation. sum :: (Typed a, Num a) => Int -> Stream a -> Stream a -- | 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 value over the current set of streams passed in. meanNow :: (Typed a, Integral a) => [Stream a] -> Stream a -- | 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. module Copilot.Library.LTL -- | 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 -- | 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 -- | 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 -- | 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 -- | 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 -- | 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 :: Integral a => Period a -> Phase a -> Stream Bool clk1 :: (Integral a, Typed a) => Period a -> Phase a -> Stream Bool period :: Integral a => a -> Period a phase :: Integral a => a -> Phase a