Fri Sep 30 16:52:34 WEST 2005 Malcolm.Wallace@cs.york.ac.uk
* suck in some initial FPTC stuff
{
adddir ./src/FPTC
hunk ./Makefile 26
+ src/FPTC/Expressions.hs src/FPTC/FaultSpec.hs \
+ src/FPTC/ListStuff.hs \
hunk ./Makefile 93
+src/Main.o : src/FPTC/Expressions.hi
hunk ./Makefile 218
+src/FPTC/Expressions.o : src/FPTC/Expressions.hs
+src/FPTC/Expressions.o : src/FPTC/FaultSpec.hi
+src/FPTC/Expressions.o : src/FPTC/ListStuff.hi
+src/FPTC/Expressions.o : src/InfoKind.hi
+src/FPTC/FaultSpec.o : src/FPTC/FaultSpec.hs
+src/FPTC/FaultSpec.o : lib/DData/Set.hi
+src/FPTC/FaultSpec.o : src/FPTC/ListStuff.hi
+src/FPTC/FaultSpec.o : src/InfoKind.hi
+src/FPTC/ListStuff.o : src/FPTC/ListStuff.hs
addfile ./src/FPTC/Expressions.hs
hunk ./src/FPTC/Expressions.hs 1
+module FPTC.Expressions where
+
+import Parse
+import InfoKind
+import FPTC.ListStuff (commasep,readSequence,mapFst,permute,indent)
+import Char (isSpace)
+import FPTC.FaultSpec
+import Text.XML.HaXml.Haskell2XmlNew
+
+-- data types
+data FaultTransform = FaultTransform
+ { clauses :: [FaultClause] } deriving (Eq)
+data FaultClause = Pattern :->: Pattern deriving (Eq,Ord)
+type Pattern = [FaultSpec]
+
+-- projections
+lhs :: FaultClause -> Pattern
+rhs :: FaultClause -> Pattern
+lhs (i :->: _) = i
+rhs (_ :->: o) = o
+
+-- instances
+instance Show FaultTransform where
+ show (FaultTransform cls) = unlines (map show cls)
+instance Show FaultClause where
+ show (l :->: r) = (commasep . map show) l ++ " -> "
+ ++ (commasep . map show) r
+instance Read FaultTransform where
+ readsPrec _ r = (\ (cs,t)-> [(FaultTransform cs, t)]) $
+ foldr (\x (xs,t)-> case reads x of
+ [(v,"")] -> (v:xs, t)
+ [(v,u)] -> (v:xs, u++t)
+ _ | all isSpace x -> (xs, t)
+ | otherwise -> (xs, x++t) )
+ ([],"")
+ (lines r)
+instance Read FaultClause where
+ readsPrec _ r = [ (p:->:q, u) | (p, s) <- readSequence "(" "," ")" r
+ , ("->",t) <- lex s
+ , (q, u) <- readSequence "(" "," ")" t ]
+
+instance Parse FaultTransform where
+{-
+ parse s = mapFst (either Left (Right . FaultTransform)) $
+ foldl (\z x-> case z of
+ (Left e, t) -> (Left e, t++x)
+ (Right vs, _) ->
+ case parse x of
+ (Left e, t) -> (Left e, t++x)
+ (Right v,t) -> (Right (vs++[v]), t) )
+ (Right [], "")
+ (lines s)
+-}
+ parse = fmap FaultTransform $
+ P (\s-> foldl (\z x-> case z of
+ (Left e, t) -> (Left e, t++x)
+ (Right vs, _) ->
+ case runParser parse x of
+ (Left e, t) -> (Left e, t++x)
+ (Right v,t) -> (Right (vs++[v]), t) )
+ (Right [], "")
+ (lines s) )
+instance Parse FaultClause where
+ parse = do { lhs <- bracketSep (isWord "(") (isWord ",") (isWord ")") parse
+ `Parse.onfail`
+ (fmap (:[]) $ parse `addToErr` "lhs of FPTC clause")
+ ; isWord "->" `Parse.onfail` fail "missing ->"
+ ; rhs <- bracketSep (isWord "(") (isWord ",") (isWord ")") parse
+ `Parse.onfail`
+ (fmap (:[]) $ parse `addToErr` "rhs of FPTC clause")
+ ; return (lhs :->: rhs)
+ }
+
+instance InfoKind FaultTransform where
+ blank = FaultTransform [[A (Var 'x')] :->: [A (Var 'x')]]
+ check nm fptc = fptcExhaustive nm ["Timing","Value"] fptc
+
+
+instance Haskell2XmlNew FaultTransform where
+ toHType _ = Defined "FaultTransforms" [] []
+ toContents ft = concatMap toContents (clauses ft)
+ parseContents = fmap FaultTransform $ nonemptylist parseContents
+instance Haskell2XmlNew FaultClause where
+ toHType _ = Defined "FaultClause" [] []
+ toContents (p:->:q) =
+ [ CElem (Elem "Pattern" [] (concatMap toContents p)) ()
+ , CElem (Elem "Result" [] (concatMap toContents q)) () ]
+ parseContents = do
+ { ps <- element' ["Pattern"] $ nonemptylist parseContents
+ ; qs <- element' ["Result"] $ nonemptylist parseContents
+ ; return (ps:->:qs)
+ }
+
+fptcExhaustive :: String -> [String] -> FaultTransform -> [String]
+fptcExhaustive nm faults fptc =
+ check nm (maximum (map (length.lhs) rules)) rules
+ where
+ rules = clauses fptc
+ check nm 0 rules = []
+ check nm n rules =
+ case foldr remove (combinations n) (map lhs rules) of
+ [] -> []
+ xs -> ["non-exhaustive patterns in FPTC for component \""++show nm
+ ++"\"\n expression is "++indent 8 (show rules)
+ ++" fault combinations not covered:\n"
+ ++indent 8 (unlines (map show xs)) ]
+ combinations n = permute (replicate n allFaults)
+ allFaults = A Normal: map (A . Fault) faults
+ remove pat combs = filter (not . foldr1 (&&) . zipWith match pat) combs
+
addfile ./src/FPTC/FaultSpec.hs
hunk ./src/FPTC/FaultSpec.hs 1
+module FPTC.FaultSpec where
+
+import Parse
+import FPTC.ListStuff (commasep,readSequence,mapFst)
+import Set (Set)
+import qualified Set as Set
+import Text.XML.HaXml.Haskell2XmlNew as XML
+import Char (isAlpha)
+
+-- FaultSpec is one of
+-- * = no fault (normal behaviour)
+-- _ = wildcard
+-- v = variable
+-- Fault = named fault type
+-- {...} = a set of faults (including *, and sometimes variables)
+-- Represented as a two-level type, to capture constraints on what can
+-- appear as part of a set.
+data Fault = Normal | Fault { fault::String } | Var { var::Char }
+ deriving (Eq,Ord) -- instance Ord Fault only needed for Set ops
+data Spec a = A { deA::a } | Wildcard | Or { set::Set a }
+ deriving (Eq,Ord)
+
+-- A simple FaultSpec:
+type FaultSpec = Spec Fault
+-- Or each fault type could have some extra information associated with it,
+-- e.g. probability, severity:
+-- type FaultSpec a = Spec (Fault,a)
+
+instance Show Fault where
+ show Normal = "*"
+ show (Fault s) = s
+ show (Var v) = [v]
+instance Show a => Show (Spec a) where
+ show Wildcard = "_"
+ show (A x) = show x
+ show (Or s) = show s
+
+instance Read Fault
+instance Parse Fault where
+ parse = do { isWord "*"; return Normal }
+ `Parse.onfail`
+ do { [c] <- word; if isAlpha c then return (Var c) else fail "" }
+ `Parse.onfail`
+ do { f <- word; if not (null f) && isAlpha (head f)
+ then return (Fault f)
+ else fail ("expected a fault, var, or *: got "++f) }
+instance Read (Spec a)
+instance (Parse a, Ord a) => Parse (Spec a) where
+{-
+ parse s = case head (lex s) of
+ ("",t) -> (Left "lexer ran out of input", t)
+ ("_",t) -> (Right Wildcard, t)
+ ("{",_) -> mapFst (either (Left . ("In a set, "++))
+ (Right . Or)) $ parse s
+ (_,_) -> mapFst (either (Left . ("When expecting a failure name or variable, "++))
+ (Right . A)) $ parse s
+-}
+ parse = do { isWord "_"; return Wildcard }
+ `Parse.onfail`
+ do { fmap Or $ parse } -- try "{" before other possibilities
+ `Parse.onfail`
+ do { fmap A $ parse }
+ `Parse.addToErr` "looking for _, {}, *, or fault"
+
+instance Read (Set a)
+instance (Parse a, Ord a) => Parse (Set a) where
+ parse = fmap Set.fromList $
+ bracketSep (isWord "{") (isWord ",") (isWord "}") parse
+
+{-
+instance Read Fault where
+ readsPrec _ t = case head (lex t) of
+ ("",_) -> []
+ ("*",x) -> [(Normal, x)]
+ ([c],x) -> [(Var c, x)]
+ (s,x) -> [(Fault s, x)]
+instance (Read a, Ord a) => Read (Spec a) where
+ readsPrec _ t = case head (lex t) of
+ ("",_) -> []
+ ("_",x) -> [ (Wildcard, x) ]
+ ("{",_) -> [ (Or s, y) | (s,y) <- reads t ]
+ (_,_) -> [ (A a, y) | (a,y) <- reads t ]
+-- following only needed <= ghc 6.4.x, <= nhc98-1.18
+instance (Read a, Ord a) => Read (Set a) where
+ readsPrec _ r = [ (Set.fromList xs, t)
+ | (xs,t) <- readSequence "{" "," "}" r ]
+-}
+
+instance Haskell2XmlNew Fault where
+ toHType _ = Defined "Fault" [] [ Constr "Normal" [] []
+ , Constr "Fault" [] [Prim "String" "string"]
+ , Constr "Var" [] [Prim "Char" "char"] ]
+ toContents Normal = [CElem (Elem "Normal" [] []) ()]
+ toContents (Var v) = [CElem (Elem "Var" [] (toContents v)) ()]
+ toContents (Fault s) = [CElem (Elem "Fault" [] (toContents s)) ()]
+ parseContents = do
+ { e@(Elem t _ _) <- element ["Normal","Var","Fault"]
+ ; case t of
+ "Normal" -> interior e $ return Normal
+ "Var" -> interior e $ fmap Var parseContents
+ "Fault" -> interior e $ fmap Fault parseContents
+ }
+instance (Haskell2XmlNew a, Ord a) => Haskell2XmlNew (Spec a) where
+ toHType _ = let a = Defined "a" [] [] in
+ Defined "Spec" [a] [ Constr "A" [a] [a]
+ , Constr "Wildcard" [] []
+ , Constr "Or" [a]
+ [Defined "Set" [a] []] ]
+ toContents (A x) = [CElem (Elem "A" [] (toContents x)) ()]
+ toContents Wildcard = [CElem (Elem "Wildcard" [] []) ()]
+ toContents (Or x) = [CElem (Elem "Or" [] (toContents x)) ()]
+ parseContents = do
+ { e@(Elem t _ _) <- element ["A","Wildcard","Or"]
+ ; case t of
+ "A" -> interior e $ fmap A parseContents
+ "Wildcard" -> interior e $ return Wildcard
+ "Or" -> interior e $ fmap Or parseContents
+ }
+instance (Haskell2XmlNew a, Ord a) => Haskell2XmlNew (Set a) where
+ toHType _ = Defined "Set" [Defined "a" [] []] []
+ toContents s = concatMap toContents (Set.toList s)
+ parseContents = fmap Set.fromList (list parseContents)
+
+{-
+instance Ord a => Functor Spec where -- change Spec a -> Spec b
+ fmap f Wildcard = Wildcard
+ fmap f (A x) = A (f x)
+ fmap f (Or s) = Or (Set.map f s)
+-}
+
+-- should matching be one-way? or symmetric as below?
+match :: FaultSpec -> FaultSpec -> Bool
+(A Normal) `match` (A Normal) = True
+Wildcard `match` _ = True
+_ `match` Wildcard = True
+(A (Var _)) `match` _ = True
+_ `match` (A (Var _)) = True
+(A (Fault f)) `match` (A (Fault f')) = f==f'
+--(Or fs) `match` f = any (`match` f) (map A fs)
+--f `match` (Or fs) = any (`match` f) (map A fs)
+-- because of equation ordering, the next three clauses replace the above two.
+(Or fs) `match` (A f) = f `Set.member` fs
+(A f) `match` (Or fs) = f `Set.member` fs
+f@(Or _) `match` (Or fs) = any (`match` f) (map A (Set.elems fs))
+_ `match` _ = False
+
+freevars :: [FaultSpec] -> [Char]
+freevars fs = [ v | A (Var v) <- fs ]
+ ++ [ v | Or s <- fs, Var v <- Set.elems s ]
+
+-- Order FPTC particles by more specific to less specific.
+data PartialOrder = LessThan | GreaterThan | Equal | Incomparable
+ | Overlapping -- for sets only
+ deriving Eq
+po :: FaultSpec -> FaultSpec -> PartialOrder
+(A Normal) `po` (A Normal) = Equal
+(A Normal) `po` (A (Fault _)) = Incomparable
+(A Normal) `po` (A (Var _)) = GreaterThan
+(A Normal) `po` Wildcard = GreaterThan
+(A s@Normal) `po` (Or fs) | s `Set.member` fs = Equal
+ | otherwise = Incomparable
+(A (Fault _)) `po` (A Normal) = Incomparable
+(A (Fault f)) `po` (A (Fault g)) | f==g = Equal
+ | otherwise = Incomparable
+(A (Fault _)) `po` (A (Var _)) = GreaterThan
+(A (Fault _)) `po` Wildcard = GreaterThan
+(A f@(Fault _)) `po` (Or fs) | f `Set.member` fs = Equal
+ | otherwise = Incomparable
+(A (Var _)) `po` (A Normal) = LessThan
+(A (Var _)) `po` (A (Fault _)) = LessThan
+(A (Var _)) `po` (A (Var _)) = Equal
+(A (Var _)) `po` Wildcard = Equal -- GreaterThan
+(A (Var _)) `po` (Or _) = LessThan
+Wildcard `po` (A Normal) = LessThan
+Wildcard `po` (A (Fault _)) = LessThan
+Wildcard `po` (A (Var _)) = Equal -- LessThan
+Wildcard `po` Wildcard = Equal
+Wildcard `po` (Or _) = LessThan
+(Or fs) `po` (A s@Normal) | s `Set.member` fs = Equal
+ | otherwise = Incomparable
+(Or fs) `po` (A f@(Fault _)) | f `Set.member` fs = Equal
+ | otherwise = Incomparable
+(Or _) `po` (A (Var _)) = GreaterThan
+(Or _) `po` Wildcard = GreaterThan
+
+-- more complicated for set/set comparison
+(Or fs) `po` (Or gs) | Set.null (fs `Set.intersection` gs) = Incomparable
+ | fs == gs = Equal
+ | otherwise = Overlapping
+
+-- partial ordering of pattern-tuples, assuming there is no overlapping.
+-- Used to decide which of two equations (LHS) is more specific.
+poTuple :: [FaultSpec] -> [FaultSpec] -> PartialOrder
+poTuple fs gs = let diffs = zipWith po fs gs in
+ if any (==Incomparable) diffs then Incomparable
+ -- else if all (==Equal) diffs then Equal
+ else safehead (filter (/=Equal) diffs)
+ where
+ safehead [] = error ("Cannot choose an ordering for these two LHSs:"
+ ++"\n "++ commasep (map show fs)
+ ++"\n "++ commasep (map show gs))
+ safehead (x:_) = x
addfile ./src/FPTC/ListStuff.hs
hunk ./src/FPTC/ListStuff.hs 1
+module FPTC.ListStuff
+ ( module List
+ , module FPTC.ListStuff
+ ) where
+
+import List
+
+permute :: [[a]] -> [[a]]
+permute [] = [[]]
+permute (xs:xss) = [ f:fs | f <- xs, fs <- permute xss ]
+
+---- pretty-printing
+indent n = unlines . map (replicate n ' ' ++) . lines
+commasep,curlysep :: [String] -> String
+commasep [x] = x
+commasep xs = "("++ concat (intersperse ", " xs) ++ ")"
+curlysep [x] = x
+curlysep xs = "{"++ concat (intersperse ", " xs) ++ "}"
+dotted xs = concat (intersperse "." xs)
+
+-- parsing
+-- e.g. readSequence "(" "," ")"
+-- e.g. readSequence "{" "," "}"
+-- e.g. readSequence "<" "|" ">"
+-- e.g. readSequence "begin" ";" "end"
+-- if only one item, brackets/separators are not required to be present.
+readSequence :: Read a => String -> String -> String -> ReadS [a]
+readSequence bra comma ket r = [ pr | (c,s) <- lex r
+ , c==bra
+ , pr <- readl s ] ++
+ [ ([p],s) | (p,s) <- reads r ]
+ where readl s = [([],t) | (c,t) <- lex s, c==ket ] ++
+ [(x:xs,u) | (x,t) <- readsPrec 0 s
+ , (xs,u) <- readl' t]
+ readl' s = [([],t) | (c,t) <- lex s, c==ket] ++
+ [(x:xs,v) | (c,t) <- lex s
+ , c==comma
+ , (x,u) <- readsPrec 0 t
+ , (xs,v) <- readl' u]
+
+-- useful for parsing
+mapFst :: (a->b) -> (a,c) -> (b,c)
+mapFst f (x,y) = (f x, y)
hunk ./src/Main.hs 8
+import FPTC.Expressions
+
hunk ./src/Main.hs 13
- ; NetworkUI.create state (undefined::())
+ ; NetworkUI.create state (undefined::FaultTransform)
}