diff --git a/CHANGELOG b/CHANGELOG --- a/CHANGELOG +++ b/CHANGELOG @@ -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). diff --git a/copilot-libraries.cabal b/copilot-libraries.cabal --- a/copilot-libraries.cabal +++ b/copilot-libraries.cabal @@ -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 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,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 diff --git a/src/Copilot/Library/MTL.hs b/src/Copilot/Library/MTL.hs --- a/src/Copilot/Library/MTL.hs +++ b/src/Copilot/Library/MTL.hs @@ -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 = 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,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 --- . +-- For an example, see +-- {-# 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: +-- +-- @ +-- "\(\)+" +-- @ +-- +-- 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) 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 @@ -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'