ltl (empty) → 0.0.0

raw patch · 4 files changed

+139/−0 lines, 4 filesdep +basedep +vcdsetup-changed

Dependencies added: base, vcd

Files

• LICENSE +27/−0
• Language/LTL.hs +65/−0
• Setup.lhs +8/−0
• ltl.cabal +39/−0

@@ -0,0 +1,27 @@+Copyright (c) Tom Hawkins 2010++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:+1. Redistributions of source code must retain the above copyright+   notice, this list of conditions and the following disclaimer.+2. Redistributions in binary form must reproduce the above copyright+   notice, this list of conditions and the following disclaimer in the+   documentation and/or other materials provided with the distribution.+3. Neither the name of the author nor the names of his contributors+   may be used to endorse or promote products derived from this software+   without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE+ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS+OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT+LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY+OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF+SUCH DAMAGE.

@@ -0,0 +1,65 @@+-- | Using linear temporal logic (LTL) to verify embedded software and hardware.+module Language.LTL+  (+  -- * Formula Combinators+    N, B, R, F, E+  -- * Verification Directives+  , Directive (..)+  , checkVCD+  ) where++import Data.VCD++data N -- Number phantom type.+data B -- Boolean phantom type.+data R -- Regular expression phantom type.+data F -- Formula phantom type.++-- | Class of booleans or formulas.+class BF a+instance BF B+instance BF F++-- | Class of booleans or regular expressions.+class BR a+instance BR B+instance BR R++-- | Class of numbers or booleans.+class NB a+instance NB N+instance NB B++-- | LTL (and other) expressions.+data E a where+  Var      :: NB a => [String] -> E a+  Add      :: E N -> E N -> E N+  Sub      :: E N -> E N -> E N+  Mul      :: E N -> E N -> E N+  Eq       :: NB a => E a -> E a -> E B+  Lt       :: E N -> E N -> E B+  Sequence :: (BR a, BR b) => E a -> E b -> E R+  Infusion :: (BR a, BR b) => E a -> E b -> E R+  Not      :: BF a => E a -> E a+  And      :: E a -> E a -> E a+  Or       :: E a -> E a -> E a+  Empty    :: E R+  Many     :: BR a => E a -> E R+  Formula' :: BR a => E a -> E F+  Formula  :: BR a => E a -> E F+  Next'    :: E F -> E F+  Until'   :: E F -> E F -> E F+  Imply    :: E R -> E F++-- | Verification directives.+data Directive+  = Assert String (E F)  -- ^ Property must be true.+  | Assume String (E F)  -- ^ Property is assumed to be true.  Becomes an assertion in simulation.+  | Cover  String (E R)  -- ^ Sequence must be excited.++-- | Check VCD data against a set of verification directives.  Returns a list of violations with time of failure (Just: safety violation, Nothing: liveness violation).+checkVCD :: String -> Int -> [Directive] -> [(Directive, Maybe Int)]+checkVCD vcd period formulas = []+  where+  VCD _ defs samples = parseVCD vcd+

@@ -0,0 +1,8 @@+#! /usr/bin/env runhaskell++> module Main (main) where+>+> import Distribution.Simple (defaultMain)+>+> main :: IO ()+> main = defaultMain

@@ -0,0 +1,39 @@+name:    ltl+version: 0.0.0++category: Language++synopsis: Using linear temporal logic (LTL) to verify embedded software and hardware.++description:+  TODO++author:     Tom Hawkins <tomahawkins@gmail.com>+maintainer: Tom Hawkins <tomahawkins@gmail.com>++license:      BSD3+license-file: LICENSE++homepage: http://tomahawkins.org++build-type:    Simple+cabal-version: >= 1.6++library+    build-depends:+        base       >= 4.2 && < 5,+        vcd        >= 0.1++    exposed-modules:+        Language.LTL++    extensions: GADTs, EmptyDataDecls++    if impl(ghc > 6.8)+          ghc-options: -fwarn-tabs+    ghc-options:       -W++source-repository head+    type:     git+    location: git://github.com/tomahawkins/ltl.git+