packages feed

copilot-libraries 3.2 → 3.2.1

raw patch · 6 files changed

+182/−70 lines, 6 filesdep ~copilot-languagePVP ok

version bump matches the API change (PVP)

Dependency ranges changed: copilot-language

API changes (from Hackage documentation)

Files

CHANGELOG view
@@ -1,3 +1,7 @@+2021-03-07+        * Version bump (3.2.1). (#10)+        * Completed the documentation. (#9)+ 2020-12-06         * Version bump (3.2).         * Update description, bug-reports, homepage fields in cabal file (#7).
copilot-libraries.cabal view
@@ -1,6 +1,6 @@ cabal-version:       >=1.10 name:                copilot-libraries-version:             3.2+version:             3.2.1 synopsis:            Libraries for the Copilot language. description:   Libraries for the Copilot language.@@ -40,7 +40,7 @@                , data-reify       >= 0.6 && < 0.7                , mtl              >= 2.0 && < 2.3                , parsec           >= 2.0 && < 3.2-               , copilot-language >= 3.2 && < 3.3+               , copilot-language >= 3.2.1 && < 3.3    exposed-modules:       Copilot.Library.Libraries
src/Copilot/Library/Libraries.hs view
@@ -1,7 +1,11 @@--- | +-- | -- Module: Libraries -- Description: Main import module for libraries -- Copyright: (c) 2011 National Institute of Aerospace / Galois, Inc.+--+-- This is a convenience module that re-exports a useful subset of modules from+-- @copilot-library@. Not all modules are exported due to name clashes (e.g.,+-- in temporal logics implementations).  module Copilot.Library.Libraries (     module Copilot.Library.Clocks
src/Copilot/Library/MTL.hs view
@@ -1,5 +1,16 @@--- Metric Temporal Logic (MTL) operators over a discrete time--- domain consisting of sampled time values+-- |+-- Description: Metric Temporal Logic (MTL) over a discrete time domain.+--+-- Metric Temporal Logic (MTL) over a discrete time domain consisting of+-- sampled time values.+--+-- The operators in this module receive two additional arguments: a clock+-- stream @clk@, indicating the current time, and a distance between samples+-- @dist@.  For the purposes of explaining the MTL aspects, we ignore those+-- arguments.  If you are using streams for which you can treat time as a+-- discrete increasing number, you can safely assume that the clock is a+-- counter (i.e., @[0, 1, 2,...]@, which can be defined by the stream @counter+-- = [0] ++ counter@) and the distance between samples is @1@.  module Copilot.Library.MTL   ( eventually, eventuallyPrev, always, alwaysBeen,@@ -14,8 +25,10 @@ -- 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 true in the future, within the time bounds specified.+--+-- @eventually l u clk dist s@ is true at time @t@ if and only if @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@@ -27,8 +40,10 @@     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)+-- | True at some point in the past within the time bounds specified.+--+-- @eventuallyPrev l u clk dist s@ is true at time @t@ if and only if @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@@ -40,21 +55,25 @@     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 true in the future, within the time bounds specified.+--+-- @always l u clk dist s@ is 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 +  where   mins = clk + (constant l)   maxes = clk + (constant u)-  res _ _ 0 = true -  res c s k = +  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)+-- | Always true in the past, within the time bounds specified.+--+-- @alwaysBeen l u clk dist s@ is 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@@ -66,9 +85,11 @@     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+-- | True until another stream is true, within the time bounds specified.+--+-- @until l u clk dist s0 s1@ is 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 at those times. 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@@ -80,23 +101,27 @@     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+-- | True since another stream became true, within the time bounds specified.+--+-- @since l u clk dist s0 s1@ is 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 at those times. 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 _ _ _ 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+-- | True if a stream is true until another one releases it.+--+-- @release l u clk dist s0 s1@ is 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 =@@ -110,9 +135,11 @@     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 +-- | True if a stream is true until another one releases it.+--+-- 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 =@@ -128,8 +155,8 @@  -- 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+-- | 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@@ -141,14 +168,14 @@     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+-- | 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+-- | 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@@ -160,8 +187,8 @@     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+-- | 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 =
src/Copilot/Library/RegExp.hs view
@@ -1,13 +1,13 @@ {-# 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>.+-- For an example, see+-- <https://github.com/Copilot-Language/examplesForACSL/blob/master/example15/main.hs>  {-# LANGUAGE FlexibleContexts #-} @@ -27,24 +27,26 @@  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).+-- | 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+-- | 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. data NumSym t = NumSym { symbolNum :: Maybe NumT                        , symbol    :: Sym t                        } deriving ( Eq, Show )+type NumT     = Int --- 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.+-- | The regular expression data type.+--+-- For our use, regular expressions describing a language with no words are 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 )@@ -53,7 +55,7 @@                 deriving Show  --- Parsers for single characters.+-- | Parsers for single characters. lquote, rquote, lparen, rparen,   star, plus, qmark, point, minus,   nondigit :: CharParser () Char@@ -69,37 +71,35 @@  nondigit = char '_' <|> letter --- A "followedBy" combinator for parsing, parses--- p, then p' and returns the result of p.+-- | 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+-- | 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.+-- | 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).+-- | "case insensitive". Take 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+-- | Parser for regular expressions regexp  :: ( SymbolParser t ) => GenParser Char () ( RegExp t ) regexp  = chainr1 term opOr @@ -114,7 +114,7 @@           <|> anySym           <|> parseSym --- Parses the "." - point character used to match any symbol.+-- | Parses the "." - point character used to match any symbol. anySym  :: ( SymbolParser t ) => GenParser Char () ( RegExp t ) anySym  = point >> ( return . RSymbol ) ( NumSym Nothing Any ) @@ -199,7 +199,7 @@  opSuffix   :: GenParser Char () ( RegExp t )            -> GenParser Char () ( RegExp t )-opSuffix r = do +opSuffix r = do   subexp   <- r   suffixes <- many $ choice [ star, plus, qmark ]   let transform rexp suffix =@@ -333,8 +333,13 @@     in outStream  +-- | Regular expression matching over an arbitrary stream copilotRegexp :: ( C.Typed t, SymbolParser t, Eq t )-                 => C.Stream t -> SourceName -> C.Stream Bool -> C.Stream Bool+              => C.Stream t     -- ^ The stream to monitor.+              -> SourceName     -- ^ The regular expression.+              -> C.Stream Bool  -- ^ A stream indicating when to reset the+                                --   monitor.+              -> C.Stream Bool copilotRegexp inStream rexp reset =   case parse parser rexp rexp of     Left  err -> C.badUsage ("parsing regular exp: " ++ show err)@@ -393,8 +398,28 @@     in outStream  -copilotRegexpB :: SourceName -> [ ( StreamName, C.Stream Bool ) ]-                  -> C.Stream Bool -> C.Stream Bool+-- | Regular expression matching over a collection of boolean streams.+--+-- Regular expressions can contain symbols, which are expanded to match+-- specific streams.+--+-- For example, the regular expression:+--+-- @+-- "\<s0\>(\<s1\>)+"+-- @+--+-- would match if you provide a map (association list) that assigns, to the+-- symbol @"s0"@, a stream that is true at the first sample, and to @"s1"@, a+-- stream that is true at every sample after the first sample.+copilotRegexpB :: SourceName                         -- ^ Regular expression+               -> [ ( StreamName, C.Stream Bool ) ]  -- ^ A table with the+                                                     -- stream associated to+                                                     -- each symbol.+               -> C.Stream Bool                      -- ^ A stream indicating+                                                     -- when to reset the+                                                     -- monitor.+               -> C.Stream Bool copilotRegexpB rexp propositions reset =   case parse parser rexp rexp of     Left  err -> C.badUsage ("parsing regular exp: " ++ show err)
src/Copilot/Library/Utils.hs view
@@ -19,50 +19,100 @@ import Copilot.Language import qualified Prelude as P +-- | Given a stream, produce an infinite list of streams dropping an increasing+-- number of elements of the given stream. For example, for a given stream @s@,+-- the expression @tails s@ is equal to @[ drop 0 s, drop 1 s, drop 2 s, ...]@.+-- tails :: ( Typed a )          => Stream a -> [ Stream a ] tails s = [ drop x s | x <- [ 0 .. ] ]  +-- | Given a stream and a number, produce a finite list of streams dropping an+-- increasing number of elements of the given stream, up to that number. For+-- example, for a given stream @s@, the expression @take 2 s@ is equal to+-- @[ drop 0 s, drop 1 s]@. take :: ( Integral a, Typed b )         => a -> Stream b -> [ Stream b ] take n s = P.take ( fromIntegral n ) $ tails s +-- | Given a number, a function on streams, and two streams, fold from the left+-- the function over the finite list of tails of the second stream (up to the+-- given number). 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 +-- | Given a number, a function on streams, and two streams, fold from the left+-- the function over the finite list of tails of the second stream (up to the+-- given number).+--+-- This function differs from 'nfoldl' in that it does not require an initial+-- accumulator and it assumes the argument number @n@ is positive. nfoldl1 :: ( Typed a )            => Int -> ( Stream a -> Stream a -> Stream a )                   ->   Stream a -> Stream a nfoldl1 n f s = foldl1 f $ take n s +-- | Given a number, a function on streams, and two streams, fold from the+-- right the function over the finite list of tails of the second stream (up to+-- the given number). 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 +-- | Given a number, a function on streams, and two streams, fold from the+-- right the function over the finite list of tails of the second stream (up to+-- the given number).+--+-- This function differs from 'nfoldr' in that it does not require an initial+-- accumulator and it assumes the argument number @n@ is positive. nfoldr1 :: ( Typed a )            => Int -> ( Stream a -> Stream a -> Stream a )                   ->   Stream a -> Stream a nfoldr1 n f s = foldr1 f $ take n s +-- | Given a number, a function on streams, and two streams, fold from the left+-- the function over the finite list of tails of the second stream (up to the+-- given number).+--+-- This function differs from 'nfoldl' in that it returns the intermediate+-- results as well. 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 +-- | Given a number, a function on streams, and two streams, fold from the+-- right the function over the finite list of tails of the second stream (up to+-- the given number).+--+-- This function differs from 'nfoldr' in that it returns the intermediate+-- results as well. 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 +-- | Given a number, a function on streams, and two streams, fold from the left+-- the function over the finite list of tails of the second stream (up to the+-- given number).+--+-- This function assumes the number of elements to scan is positive, and it+-- also returns the intermediate results. nscanl1 :: ( Typed a )            => Int -> ( Stream a -> Stream a -> Stream a )            -> Stream a -> [ Stream a ] nscanl1 n f s = scanl1 f $ take n s +-- | Given a number, a function on streams, and two streams, fold from the+-- right the function over the finite list of tails of the second stream (up to+-- the given number).+--+-- This function assumes the number of elements to scan is positive, and it+-- also returns the intermediate results. nscanr1 :: ( Typed a )            => Int -> ( Stream a -> Stream a -> Stream a )            -> Stream a -> [ Stream a ]@@ -83,8 +133,9 @@                    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.+-- | Index.+--+-- WARNING: Very expensive! Consider using this only for very short lists. (!!) :: (Typed a, Eq b, Num b, Typed b) => [Stream a] -> Stream b -> Stream a ls !! n = let indices      = map                              ( constant . fromIntegral )@@ -102,6 +153,7 @@              else                select indices ls +-- | Cycle a list to form an infinite stream. cycle :: ( Typed a ) => [ a ] -> Stream a cycle ls = cycle'   where cycle' = ls ++ cycle'