diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,27 @@ +Copyright (c) Tom Hawkins 2010-2011 + +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. diff --git a/Language/FaultTree.hs b/Language/FaultTree.hs new file mode 100644 --- /dev/null +++ b/Language/FaultTree.hs @@ -0,0 +1,114 @@ +module Language.FaultTree + ( Event (..) + , imply + , dot + , cutsets + ) where + +import Data.List +import Data.Maybe +import Math.SMT.Yices.Pipe +import Math.SMT.Yices.Syntax +import Text.Printf + +type Name = String + +-- | An event. +data Event + = Leaf Name -- ^ Leaf node. + | Branch Name Event -- ^ Named branch node. + | Not Event -- ^ Logical NOT. + | And [Event] -- ^ Logical AND. + | Or [Event] -- ^ Logical OR. + deriving (Show, Eq) + +-- | Logical implication. +imply :: Event -> Event -> Event +imply a b = Or [Not a, b] + +-- | Render a Graphviz dot file from a set of 'Event' (fault) trees. +dot :: [Event] -> String +dot a = unlines + [ "digraph {" + , "\trankdir=BT" + , unlines $ map node events' + , unlines $ map edge events' + , "}" + ] + where + events'' :: [(Event, String)] + events'' = [ (a, "event_" ++ show i) | (i, a) <- zip [0 ..] $ nub $ concatMap events a ] + events' = fst $ unzip events'' + eventId :: Event -> String + eventId a = fromJust $ lookup a events'' + node :: Event -> String + node a = case a of + Leaf name -> printf "\t%s [label=\"%s\"]" (eventId a) name + Branch name _ -> printf "\t%s [label=\"%s\"]" (eventId a) name + Not _ -> printf "\t%s [label=\"NOT\"]" (eventId a) + And _ -> printf "\t%s [label=\"AND\"]" (eventId a) + Or _ -> printf "\t%s [label=\"OR\"]" (eventId a) + + edge :: Event -> String + edge a = case a of + Leaf _ -> "" + Branch _ b -> printf "\t%s -> %s" (eventId b) (eventId a) + Not b -> printf "\t%s -> %s" (eventId b) (eventId a) + And b -> unlines [ printf "\t%s -> %s" (eventId b) (eventId a) | b <- b ] + Or b -> unlines [ printf "\t%s -> %s" (eventId b) (eventId a) | b <- b ] + +-- Unique list of events. +events :: Event -> [Event] +events a = case a of + Leaf _ -> [a] + Branch _ b -> a : events b + Not b -> a : events b + And b -> a : nub (concatMap events b) + Or b -> a : nub (concatMap events b) + +-- | Minimal cut set analysis. +-- > cutsets pathToYices maxNumberOfLeafEvents failureEvent assumptions +cutsets :: FilePath -> Int -> Event -> [Event] -> IO () +cutsets yices n event assumes = do + --mapM_ print model + check 1 [] + where + eventId :: Event -> String + eventId a = fromJust $ lookup a eventNames + events' = nub $ concatMap events $ event : assumes + eventNames = [ (a, "event_" ++ show i) | (i, a) <- zip [0 ..] events' ] + model :: [CmdY] + model = map var events' ++ mapMaybe expr events' ++ [ASSERT $ VarE $ eventId event] ++ [ ASSERT $ VarE $ eventId assume | assume <- assumes ] + var :: Event -> CmdY + var a = DEFINE (eventId a, VarT "bool") Nothing + expr :: Event -> Maybe CmdY + expr a = case a of + Leaf _ -> Nothing + Branch _ b -> Just $ ASSERT $ VarE (eventId a) := VarE (eventId b) + Not b -> Just $ ASSERT $ VarE (eventId a) := NOT (VarE $ eventId b) + And b -> Just $ ASSERT $ VarE (eventId a) := AND [ VarE $ eventId b | b <- b ] + Or b -> Just $ ASSERT $ VarE (eventId a) := OR [ VarE $ eventId b | b <- b ] + + nEvents :: Int -> CmdY + nEvents n = ASSERT $ LitI (fromIntegral n) := foldl1 (:+:) [ IF (VarE $ eventId a) (LitI 1) (LitI 0) | a@(Leaf _) <- events' ] + + check :: Int -> [[String]] -> IO () + check i _ | i > n = return () + check i assumes = do + result <- quickCheckY yices [] $ model ++ [nEvents i] ++ [ ASSERT $ NOT $ AND [ VarE a | a <- assume ] | assume <- assumes ] + case result of + Sat a -> do + putStrLn $ concat [ name ++ "\n" | Leaf name <- cutSet a ] + check i $ [ eventId a | a <- cutSet a ] : assumes + UnSat _ -> check (i + 1) assumes + a -> error $ "unexpected smt result: " ++ show a + + cutSet :: [ExpY] -> [Event] + cutSet result = [ a | (a@(Leaf _), label) <- eventNames, elem' label ] + where + match label (VarE label' := LitB True) = label == label' + match _ _ = False + elem' a = case find (match a) result of + Nothing -> False + Just _ -> True + diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/fault-tree.cabal b/fault-tree.cabal new file mode 100644 --- /dev/null +++ b/fault-tree.cabal @@ -0,0 +1,38 @@ +name: fault-tree +version: 0.0.0 + +category: Language, Embedded + +synopsis: A fault tree analysis library. + +description: + Fault tree analysis is used to determine probability of failure modes + in safety critical applications. Generates fault tree graphs (Graphviz) + and calculates cutsets. + Yices (required) is the backend SMT solver used for cutset calculation. + +author: Tom Hawkins +maintainer: Tom Hawkins + +license: BSD3 +license-file: LICENSE + +homepage: http://tomahawkins.org + +build-type: Simple +cabal-version: >= 1.6 + +library + build-depends: + base >= 4.0 && < 5, + yices >= 0.0.0.7 && < 0.0.1 + + exposed-modules: + Language.FaultTree + + ghc-options: -W + +source-repository head + type: git + location: git://github.com/tomahawkins/fault-tree.git +