copilot-libraries 0.3 → 0.4

raw patch · 9 files changed

+57/−8 lines, 9 files

Files

copilot-libraries.cabal +2/−3
src/Copilot/Library/Clocks.hs +4/−1
src/Copilot/Library/LTL.hs +4/−0
src/Copilot/Library/Libraries.hs +26/−0
src/Copilot/Library/PTLTL.hs +4/−0
src/Copilot/Library/RegExp.hs +1/−0
src/Copilot/Library/Stacks.hs +6/−2
src/Copilot/Library/Statistics.hs +4/−0
src/Copilot/Library/Utils.hs +6/−2

copilot-libraries.cabal view

@@ -1,6 +1,6 @@ cabal-version:       >=1.10 name:                copilot-libraries-version:             0.3+version:             0.4 synopsis:            A Haskell-embedded DSL for monitoring hard real-time                      distributed systems. description:         @@ -42,6 +42,7 @@     mtl >= 2.0    exposed-modules:+    Copilot.Library.Libraries     Copilot.Library.Clocks     Copilot.Library.LTL     Copilot.Library.PTLTL@@ -50,8 +51,6 @@     Copilot.Library.Utils     Copilot.Library.Voting     Copilot.Library.Stacks--  other-modules:    ghc-options:     -fwarn-tabs

src/Copilot/Library/Clocks.hs view

@@ -1,3 +1,7 @@+--------------------------------------------------------------------------------+-- 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 -- @@@ -17,7 +21,6 @@ -- 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, clk1, period, phase ) where

src/Copilot/Library/LTL.hs view

@@ -1,3 +1,7 @@+--------------------------------------------------------------------------------+-- Copyright © 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,

+ src/Copilot/Library/Libraries.hs view

@@ -0,0 +1,26 @@+--------------------------------------------------------------------------------+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++-- | Main import module for the front-end lanugage.++module Copilot.Library.Libraries (+    module Copilot.Library.Clocks+  , module Copilot.Library.LTL+  , module Copilot.Library.PTLTL+  , module Copilot.Library.Statistics+  , module Copilot.Library.RegExp+  , module Copilot.Library.Utils+  , module Copilot.Library.Voting+  , module Copilot.Library.Stacks+  ) where++import Copilot.Library.Clocks+import Copilot.Library.LTL+import Copilot.Library.PTLTL+import Copilot.Library.Statistics+import Copilot.Library.RegExp+import Copilot.Library.Utils+import Copilot.Library.Voting+import Copilot.Library.Stacks+

src/Copilot/Library/PTLTL.hs view

@@ -1,3 +1,7 @@+--------------------------------------------------------------------------------+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------+ -- | Provides past-time linear-temporal logic (ptLTL operators). -- -- Interface: see Examples/PTLTLExamples.hs.

src/Copilot/Library/RegExp.hs view

@@ -1,5 +1,6 @@ module Copilot.Library.RegExp ( copilotRegexp, copilotRegexpB ) where +-- | A regular expression librariy.  import Text.ParserCombinators.Parsec   ( optional, (<|>), string, char, between, GenParser, many, choice, CharParser

src/Copilot/Library/Stacks.hs view

@@ -1,12 +1,16 @@+--------------------------------------------------------------------------------+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++-- | Stack machine.+ {-# LANGUAGE NoImplicitPrelude #-}  module Copilot.Library.Stacks   ( stack, stack' ) where - import Copilot.Language import Copilot.Language.Prelude-  type PushSignal    = Stream Bool type PopSignal     = Stream Bool

src/Copilot/Library/Statistics.hs view

@@ -1,3 +1,7 @@+--------------------------------------------------------------------------------+-- Copyright © 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).

src/Copilot/Library/Utils.hs view

@@ -1,14 +1,18 @@+--------------------------------------------------------------------------------+-- Copyright © 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 )  where - import Copilot.Language import Copilot.Language.Prelude  import qualified Prelude as P-  -- | functions similar to the Prelude functions on lists