diff --git a/Data/FsmActions.hs b/Data/FsmActions.hs --- a/Data/FsmActions.hs +++ b/Data/FsmActions.hs @@ -16,45 +16,44 @@ -- Copyright (c) 2009 Andy Gimblett - http://www.cs.swan.ac.uk/~csandy/ -- BSD Licence (see http://www.opensource.org/licenses/bsd-license.php) -module Data.FsmActions - (-- * Data types - State, - DestinationSet(..), - Action(..), - FSM(..), - Word(..), - -- * Simple FSM operations - states, - alphabet, - fsmAction, - -- * Well-formedness - WellFormed(..), - isWellFormed, - -- * Normalisation - normalise, - normaliseAction, - -- * Operations on actions - mkAction, - mkDAction, - append, - actionLookup, - action, - actionEquiv, - -- * Destination sets - destinationSet, - destinationEquiv, - -- * Identity - fsmIdentity, - -- * Determinism - isDAction, - isDFSM +module Data.FsmActions ( + -- * Data types + State, + DestinationSet(..), + Action(..), + FSM(..), + Word(..), + -- * Simple FSM operations + states, + alphabet, + fsmAction, + -- * Normalisation + normalise, + normaliseAction, + -- * Operations on actions + mkAction, + mkDAction, + append, + actionLookup, + action, + actionEquiv, + -- * Destination sets + destinationSet, + destinationEquiv, + -- * Identity + fsmIdentity, + identity, + -- * Determinism + isDAction, + isDFSM ) where -import Control.Arrow (second) import Control.Monad -import qualified Data.List as L import qualified Data.Map as M +import qualified Data.List as L +--import Data.FsmActions.FGL + -- | States are integers, counting from zero. type State = Int -- Could be parametric (as in HaLeX), but for now, YAGNI. @@ -96,53 +95,8 @@ fsmAction :: Ord sy => sy -> FSM sy -> Maybe Action fsmAction sy = M.lookup sy . unFSM --- | An 'FSM' is well-formed if all its actions are the same length, --- and none of its actions contain destinations which are out of --- range. -data WellFormed sy - -- | 'FSM' is well-formed. (Carries an empty list: this is a slight - -- wart, as no cargo is necessary; unfortunately, fixing that - -- would require use of a GADT here, which seems excessive.) - = WellFormed [sy] - -- | Lengths of Actions in the 'FSM' don't all match. Carries a - -- sorted list of (symbol, 'Action' length) pairs, one for every - -- symbol in the alphabet of the 'FSM'. - | BadLengths [(sy, Int)] - -- | Some 'Action's contain out-of-range (negative or too-high) - -- destinations. Carries a sorted list of all such actions and - -- their corresponding symbols. - | BadActions [(sy, Action)] - deriving (Eq, Show) --- | Check if an 'FSM' is well-formed or not. -isWellFormed :: Ord sy => FSM sy -> WellFormed sy -isWellFormed fsm = - if not $ allSame $ L.map snd actionLengths - then BadLengths (L.sort actionLengths) - else if not $ M.null badParts - then BadActions (L.sort $ M.toList badParts) - else WellFormed [] - where -- All (symbol, Action length) pairs in FSM. - actionLengths = L.map (second aLength) (M.toList $ unFSM fsm) - -- Submap containing only Actions with bad destinations. - badParts = M.filter isBad $ unFSM fsm - -- Check if an Action has any bad destinations. - isBad a = any badDest (flatten a) - where -- Flatten lists of destination states in an Action. - flatten (Action xs) = L.concat $ map destinations xs - -- Check if a destination is bad (negative or too high). - badDest x = (x<0) || (x >= (length $ states fsm)) - -- Compute the length of an action - aLength (Action xs) = length xs --- Check if every element of a list is identical. -allSame :: Eq a => [a] -> Bool -allSame [] = True -allSame [_] = True -allSame (x:y:xs) = (x == y) && allSame (y:xs) - - - -- | Build an action given a nested list of destination states. mkAction :: [[State]] -> Action mkAction = Action . map DestinationSet @@ -192,7 +146,7 @@ -- be Nothing. destinationSet :: Ord sy => FSM sy -> State -> Word sy -> Maybe DestinationSet destinationSet fsm src word = - if (src >= 0) && (src < (length $ states fsm)) + if (src >= 0) && (src < length (states fsm)) then case (action fsm word) of Just (Action ds) -> Just $ ds !! src _ -> Nothing @@ -208,8 +162,11 @@ -- | Compute the identity action for a given FSM. fsmIdentity :: FSM sy -> Action -fsmIdentity = Action . map (\x -> DestinationSet [x]) . states +fsmIdentity = identity . length . states +-- | Compute the identity action for a given number of states +identity :: Int -> Action +identity n = Action $ map (\x -> DestinationSet [x]) [0..n-1] -- | Test if an 'Action' is deterministic or not. diff --git a/Data/FsmActions/ActionMatrix.hs b/Data/FsmActions/ActionMatrix.hs --- a/Data/FsmActions/ActionMatrix.hs +++ b/Data/FsmActions/ActionMatrix.hs @@ -1,37 +1,39 @@ {- | Serialisation/deserialisation of 'Data.FsmActions.FSM's and -'Data.FsmActions.Action's as adjacency matrices. +'Data.FsmActions.Action's as binary adjacency matrices. -An 'Data.FsmActions.Action' may be represented as an adjacency matrix of -0s and 1s. The rows and columns of the matrix correspond to states of -the 'Data.FA.Core.FSM': a 1 in a cell indicates that the +An 'Data.FsmActions.Action' may be represented as an adjacency matrix +of 0s and 1s. The rows and columns of the matrix correspond to states +of an 'Data.FsmActions.FSM': a 1 in a cell indicates that the 'Data.FsmActions.Action' causes a transition from the \'row\' state to the \'column\' state. If any of the rows in the matrix contain more -than one 1, the corresponding 'Data.FsmActions.Action' is a -nondeterministic: an 'Data.FsmActions.NAction'. +than one 1, the corresponding 'Data.FsmActions.Action' and +'Data.FsmActions.FSM' will be nondeterministic. -} --- TODO: tests, working properly for empty strings, single element --- rows, etc. - module Data.FsmActions.ActionMatrix ( - readFSMFromMxFiles, - readAdjMxFromFile, - readAdjMxFromString + -- * Input + parseFsmActionMxFiles, + parseActionMxFile, + parseActionMx, + -- * Output + printActionMx ) where import Control.Monad.Error -import qualified Data.ByteString.Char8 as B import qualified Data.List as L import qualified Data.Map as M import Data.Maybe (mapMaybe) import System.IO.Error (mkIOError, userErrorType) +import qualified Text.ParserCombinators.Parsec as P +import Text.PrettyPrint.HughesPJ import Data.FsmActions import Data.FsmActions.Error + -- | This module's internal represenation of adjacency matrices is as -- nested lists of booleans. These are only ever used as intermediate -- data structures, and should not be generated or manipulated @@ -39,85 +41,99 @@ -- 'Data.FsmActions.Action' type. If you want serialised matrices for -- storage or transmission, convert them to strings of 0s and 1s using -- the functions in this module. -type AdjacencyMatrix = [AdjacencyMatrixRow] -type AdjacencyMatrixRow = [AdjacencyMatrixCell] -type AdjacencyMatrixCell = Bool +type ActionMatrix = [ActionMatrixRow] +type ActionMatrixRow = [Bool] -- | Given a list of (symbol, path) pairs, compute an --- 'Data.FsmActions.FSM' whose actions are read from matrices in each of --- the paths using 'readAdjMxFromFile' (and associated with their --- corresponding symbols). +-- 'Data.FsmActions.FSM' whose actions are read from action matrices +-- in the specified paths, associated with their corresponding +-- symbols. -- -- Note that if the same symbol appears multiple times, only one -- instance will appear in the 'Data.FsmActions.FSM'; the choice of which -- appears is not defined. ---readFSMFromMxFiles :: Ord sy => [(sy, String)] -> IO (FSM sy) -readFSMFromMxFiles :: Ord sy => [(sy, String)] -> IO (FSM sy) -readFSMFromMxFiles xs = - liftM (FSM . M.fromList) $ mapM (liftMSnd readAdjMxFromFile) xs +parseFsmActionMxFiles :: Ord sy => [(sy, FilePath)] -> IO (FSM sy) +parseFsmActionMxFiles xs = + liftM (FSM . M.fromList) $ mapM (liftMSnd parseActionMxFile) xs where liftMSnd :: Monad m => (a -> m b) -> (c, a) -> m (c, b) liftMSnd f (x, y) = f y >>= \z -> return (x, z) --- | Read an action matrix from a specified file; uses --- 'readAdjMxFromString' to interpret the file contents. -readAdjMxFromFile :: String -> IO Action -readAdjMxFromFile path = - do contents <- B.readFile path - let act = readAdjMxFromString contents - -- Catch error and act appropriately +-- | Read an action matrix from a specified file, and parse it into an +-- 'Data.FsmActions.Action'. +parseActionMxFile :: FilePath -> IO Action +parseActionMxFile path = + do contents <- readFile path + let act = parseActionMx contents case act of Right a -> return a Left e -> throwError (mkIOError userErrorType (show e) Nothing (Just path)) - +-- | Parse an action matrix string, and turn it into an +-- 'Data.FsmActions.Action'. +parseActionMx :: String -> ReadMxMonad Action +parseActionMx actionString = + case P.parse actionMxParser "" actionString of + Right mx -> interpretActionMx mx + Left err -> throwError (MxError "Action matrix parse error" (show err)) --- | Given a bytestring we expect to contain a serialisation of an --- adjacency matrix, compute the corresponding 'Data.FsmActions.Action'. +-- | Parse an action matrix from a string. -- --- The serialisation format for an 'Data.FsmActions.Action' on an --- /n/-state 'Data.FsmActions.FSM' is as follows: there are /n/ --- (newline-separated) lines, each containing /n/ (comma-separated) 0s --- or 1s. No other characters are allowed (not even whitespace), and --- it is an error for any of the rows to contain anything other than --- /n/ cells. (Note that /n/ is not specified, but inferred from the --- number of lines in the string). -readAdjMxFromString :: B.ByteString -> ReadMxMonad Action -readAdjMxFromString s = splitMxString s >>= parseActionMatrix - --- | Turn a string into an adjacency matrix. -splitMxString :: B.ByteString -> ReadMxMonad AdjacencyMatrix -splitMxString = mapM readMxRow . B.lines - -readMxRow :: B.ByteString -> ReadMxMonad AdjacencyMatrixRow -readMxRow = mapM readMxCell . B.split ',' - -readMxCell :: B.ByteString -> ReadMxMonad AdjacencyMatrixCell -readMxCell cell = - if cell == B.singleton '0' - then return False - else if cell == B.singleton '1' - then return True - else throwError (MxError "Bad cell in matrix string" (show cell)) - - +-- The string being parsed should contain newline-separated rows, +-- where each row contains comma-separated cells, where each cell is a +-- 0 or a 1. Trailing newlines are ignored. +actionMxParser :: P.Parser ActionMatrix +actionMxParser = do rows <- parseRow `P.sepEndBy1` P.char '\n' + P.skipMany $ P.char '\n' -- Ignore any trailing newlines + P.eof + return rows + where parseRow :: P.Parser [Bool] + parseRow = parseCell `P.sepBy1` P.char ',' + parseCell :: P.Parser Bool + parseCell = P.choice [ do P.char '0' + return False + , do P.char '1' + return True + ] --- | Given an 'AdjacencyMatrix', compute the corresponding +-- | Given an 'ActionMatrix', compute the corresponding -- 'Data.FsmActions.Action'. -parseActionMatrix :: AdjacencyMatrix -> ReadMxMonad Action -parseActionMatrix rows = +interpretActionMx :: ActionMatrix -> ReadMxMonad Action +interpretActionMx rows = if all (== length transitions) rowLengths -- check matrix is square then return $ normaliseAction $ mkAction transitions else throwError (MxError "action matrix is not square (see row lengths)" (show rowLengths)) - where transitions = L.map parseActionMatrixRow rows + where transitions = L.map parseActionMxRow rows rowLengths = L.map length rows --- | Given an 'AdjacencyMatrixRow', compute the list of indices of --- cells in the row which are set (i.e. which represent transitions). -parseActionMatrixRow :: AdjacencyMatrixRow -> [Int] -parseActionMatrixRow xs = mapMaybe isSet (withIdxs xs) +-- | Given an 'ActionMatrixRow', compute the list of indices of cells +-- in the row which are set (i.e. which represent transitions). +parseActionMxRow :: ActionMatrixRow -> [Int] +parseActionMxRow xs = mapMaybe isSet (withIdxs xs) where -- | Zip the cells of a list together with their indices. withIdxs ys = zip ys [0..(length ys-1)] -- | Iff the cell is set, include its index.. isSet (cell, index) = if cell then Just index else Nothing + +-- | Pretty-print an action in action matrix format. +printActionMx :: Action -> String +printActionMx = show . ppActionMx + +-- Pretty printer to action matrix format. +ppActionMx :: Action -> Doc +ppActionMx (Action dSets) = vcat $ map mkRow dSets + where -- Space-separated list of cells + mkRow :: DestinationSet -> Doc + mkRow (DestinationSet ds) = commas $ map (isCell ds) stateList + -- List of states to iterate over + stateList :: [State] + stateList = [0..length dSets-1] + -- Check if a certain cell should be set or not + isCell :: [State] -> State -> Doc + isCell dests src = if src `elem` dests then char '1' else char '0' + -- Separate a list of Docs with commas + commas :: [Doc] -> Doc + commas [] = empty + commas (x:[]) = x + commas (x:xs) = x <> comma <> commas xs diff --git a/Data/FsmActions/FGL.hs b/Data/FsmActions/FGL.hs new file mode 100644 --- /dev/null +++ b/Data/FsmActions/FGL.hs @@ -0,0 +1,86 @@ +{- | + +Interface to fgl graph library (). + +-} + +-- Copyright (c) 2009 Andy Gimblett - http://www.cs.swan.ac.uk/~csandy/ +-- BSD Licence (see http://www.opensource.org/licenses/bsd-license.php) + +module Data.FsmActions.FGL ( + SelfLoops(..), + fsmToFGL, + strongCCs, + weakCCs +) where + +import qualified Data.Map as M +import Data.Graph.Inductive.Basic (undir) +import Data.Graph.Inductive.Graph (Graph, mkGraph) +import qualified Data.Graph.Inductive.PatriciaTree as P +import qualified Data.Graph.Inductive.Tree as T +import Data.Graph.Inductive.Query.DFS (scc) + +import Data.FsmActions + +-- | When converting an 'Data.FsmActions.FSM' into a graph, do we keep +-- all self-loops, or only those which are sources of nondeterminism? +data SelfLoops = Keep | Trim + +-- | Turn an FSM into an fgl graph with labelled edges. +fsmToFGL :: FSM sy -> SelfLoops -> T.Gr () sy +-- Note use of T.Gr; this instance of Graph allows multiple edges +-- between the same pair of nodes, which is what we _usually_ (but not +-- always) want. +fsmToFGL = fsmToFGL' + +-- Generalised FSM to graph conversion; works with any Graph instance. +fsmToFGL' :: (Graph gr) => FSM sy -> SelfLoops -> gr () sy +fsmToFGL' fsm selfs = mkGraph nodes edges + where nodes = map (\state -> (state, ())) $ states fsm + edges = fsmEdges selfs fsm + +-- Compute an FSM's labelled edges +fsmEdges :: SelfLoops -> FSM sy -> [(State, State, sy)] +fsmEdges selfs = concatMap (symbolEdges selfs) . M.toList . unFSM + +-- Given a symbol, action pair, compute the list of edges with that +-- symbol. +symbolEdges :: SelfLoops -> (sy, Action) -> [(State, State, sy)] +symbolEdges selfs (s, a) = + concatMap (syStateEdges selfs s) $ zipWithIndex $ destinationSets a + +-- Given a symbol, a start state, and a destination set, compute the +-- list of edges leading from that state with that symbol, possibly +-- taking account of a desire to trim deterministic self-loops. +syStateEdges :: SelfLoops -> sy -> (State, DestinationSet) -> + [(State, State, sy)] +syStateEdges Keep s (src, dSet) = syStateEdges' s (src, dSet) +syStateEdges Trim s (src, dSet) = + if destinations dSet == [src] then [] else syStateEdges' s (src, dSet) + +-- Given a symbol, a start state, and a destination set, compute the +-- list of edges leading from that state with that symbol. +syStateEdges' :: sy -> (State, DestinationSet) -> [(State, State, sy)] +syStateEdges' s (src, dSet) = map (\x -> (src, x, s)) $ destinations dSet + +-- Create a zip of a list with its index list. +zipWithIndex :: [a] -> [(Int, a)] +zipWithIndex xs = zip [0..(length xs-1)] xs + + + +-- | Compute an FSM's strongly-connected components. +strongCCs :: Eq sy => FSM sy -> [[State]] +strongCCs = scc . fsmToPatriciaTree Trim + +-- | Compute an FSM's weakly-connected components. +weakCCs :: Eq sy => FSM sy -> [[State]] +weakCCs = scc . undir . fsmToPatriciaTree Trim + +-- | The PatriciaTree instance of Graph is faster, but not generally +-- useful to us because it doesn't allow multiple edges between the +-- same pair of nodes. For SCC checks, however, that doesn't matter, +-- so we use it. +fsmToPatriciaTree :: SelfLoops -> FSM sy -> P.Gr () sy +fsmToPatriciaTree = flip fsmToFGL' diff --git a/Data/FsmActions/FsmMatrix.hs b/Data/FsmActions/FsmMatrix.hs --- a/Data/FsmActions/FsmMatrix.hs +++ b/Data/FsmActions/FsmMatrix.hs @@ -14,12 +14,13 @@ -} -module Data.FsmActions.FsmMatrix - (parseFsmFile, - parseFsmString, - printFsmMatrix, - ) -where +module Data.FsmActions.FsmMatrix ( + -- * Input + parseFsmMxFile, + parseFsmMx, + -- * Output + printFsmMx, +) where import Control.Monad.Error import Data.Char (isSpace) @@ -31,13 +32,14 @@ import Data.FsmActions import Data.FsmActions.Error +import Data.FsmActions.WellFormed -- | Parse an FsmMatrix-formatted FSM held in a file, by reading the -- file and calling 'parseFsmString'. -parseFsmFile :: FilePath -> IO (FSM String) -parseFsmFile path = +parseFsmMxFile :: FilePath -> IO (FSM String) +parseFsmMxFile path = do contents <- readFile path - let result = parseFsmString contents + let result = parseFsmMx contents case result of Right fsm -> return fsm Left e -> throwError (mkIOError userErrorType (show e) @@ -45,28 +47,35 @@ -- | Parse an FsmMatrix-formatted FSM held in a string. Includes -- normalisation and well-formedness checks. -parseFsmString :: String -> ReadMxMonad (FSM String) -parseFsmString fsmString = - case P.parse fsmParser "" fsmString of +parseFsmMx :: String -> ReadMxMonad (FSM String) +parseFsmMx fsmString = + case P.parse fsmMatrixParser "" fsmString of Right parts -> - do fsm <- interpretFsm parts + do fsm <- interpretFsmMx parts case (isWellFormed fsm) of - WellFormed _ -> return fsm - err -> throwError (MxError "Fsm matrix ill-formed" (show err)) + WellFormed -> return fsm + Disconnected wccs -> + throwError (MxError "FSM disconnected" (show wccs)) + err -> throwError (MxError "FSM matrix ill-formed" (show err)) Left err -> - throwError (MxError "Fsm matrix parse error" (show err)) + throwError (MxError "FSM matrix parse error" (show err)) +-- TODO: there are well-formedness checks here, but not when reading +-- in from action matrices. Generalise! Either remove the checks +-- here, or factor them out into an handy "run this after input" +-- function. + -- FsmMatrix-format parser. -fsmParser :: P.Parser ([String], [[[Int]]]) -fsmParser = do actions <- actionName `P.sepEndBy` nonEOLSpace - P.char '\n' - transitionRows <- transitionRow `P.sepEndBy` P.char '\n' - P.many (P.satisfy isSpace) -- Parse trailing whitespace. - P.eof - return (actions, transitionRows) +fsmMatrixParser :: P.Parser ([String], [[[Int]]]) +fsmMatrixParser = do actions <- actionName `P.sepEndBy` nonEOLSpace + P.char '\n' + transitionRows <- transitionRow `P.sepEndBy` P.char '\n' + P.many (P.satisfy isSpace) -- Parse trailing whitespace. + P.eof + return (actions, transitionRows) where -- An action name is a string of non-whitespace characters. actionName :: P.Parser String - actionName = P.many1 (P.satisfy (\c -> not $ isSpace c)) + actionName = P.many1 (P.satisfy (not . isSpace)) -- A row of transitions is a space-separated line of transitions. transitionRow :: P.Parser [[Int]] transitionRow = transition `P.sepEndBy1` nonEOLSpace @@ -75,27 +84,27 @@ transition = state `P.sepBy1` P.char ',' -- A state is a natural number. state :: P.Parser Int - state = P.many1 P.digit >>= (\c -> return $ read c) + state = liftM read (P.many1 P.digit) -- Parse whitespace that isn't an end of line. nonEOLSpace :: P.Parser String nonEOLSpace = P.many1 (P.satisfy (\c -> isSpace c && c /= '\n')) --- Turn some FsmMatrix-formatted data into an (normalised) FSM. -interpretFsm :: ([String], [[[Int]]]) -> ReadMxMonad (FSM String) -interpretFsm (actionNames, stateLines) = - case (all (== (length actionNames)) lineLengths) of - True -> return $ normalise $ FSM $ M.fromList $ zip actionNames actions - False -> throwError (MxError "FSM matrix ill-formed" (show lineLengths)) +-- Turn some FsmMatrix-formatted data into an (normalised) FSM. +interpretFsmMx :: ([String], [[[Int]]]) -> ReadMxMonad (FSM String) +interpretFsmMx (actionNames, stateLines) = + if all (== (length actionNames)) lineLengths + then return $ normalise $ FSM $ M.fromList $ zip actionNames actions + else throwError (MxError "FSM matrix ill-formed" (show lineLengths)) where actions = map mkAction $ L.transpose stateLines lineLengths = L.map length stateLines -- | Pretty-print a string FSM in FsmMatrix format. -printFsmMatrix :: FSM String -> String -printFsmMatrix = show . ppFsmMatrix +printFsmMx :: FSM String -> String +printFsmMx = show . ppFsmMx -- Pretty printer to FsmMatrix format (building Doc not String). -ppFsmMatrix :: FSM String -> Doc -ppFsmMatrix fsm = actionRow $$ transitionRows +ppFsmMx :: FSM String -> Doc +ppFsmMx fsm = actionRow $$ transitionRows where -- Space-separated list of action names. actionRow :: Doc actionRow = hsep $ map (text . fst) asList diff --git a/Data/FsmActions/GraphViz.hs b/Data/FsmActions/GraphViz.hs new file mode 100644 --- /dev/null +++ b/Data/FsmActions/GraphViz.hs @@ -0,0 +1,29 @@ +{- | + +GraphViz (dot) rendering using the graphviz library. + +-} + +-- Copyright (c) 2009 Andy Gimblett - http://www.cs.swan.ac.uk/~csandy/ +-- BSD Licence (see http://www.opensource.org/licenses/bsd-license.php) + +module Data.FsmActions.GraphViz ( + fsmToDot +) where + +import Data.GraphViz +import Data.Graph.Inductive.Graph (Graph) + +import Data.FsmActions +import Data.FsmActions.FGL + +-- | Turn an FSM into a 'Data.GraphViz.DotGraph', trimming any +-- self-loops which aren't sources of nondeterminism. +fsmToDot :: (Ord sy, Show sy) => FSM sy -> DotGraph +fsmToDot = fglDot . flip fsmToFGL Trim + +-- Turn an FGL into a DotGraph with labelled edges. +fglDot :: (Ord b, Show b, Graph gr) => gr a b -> DotGraph +fglDot g = graphToDot g [] nodeFn edgeFn + where nodeFn _ = [] + edgeFn (_, _, label) = [Label $ Left $ show label] diff --git a/Data/FsmActions/WellFormed.hs b/Data/FsmActions/WellFormed.hs new file mode 100644 --- /dev/null +++ b/Data/FsmActions/WellFormed.hs @@ -0,0 +1,75 @@ +{- | + +Well-formedness checks for finite state machines. + +-} + +-- Copyright (c) 2009 Andy Gimblett - http://www.cs.swan.ac.uk/~csandy/ +-- BSD Licence (see http://www.opensource.org/licenses/bsd-license.php) + +module Data.FsmActions.WellFormed ( + WellFormed(..), + isWellFormed, +) where + +import Control.Arrow (second) +{- +-- We use a PatriciaTree because we care about speed, and it doesn't +-- matter if duplicate edges are lost when checked for SCCs. +import Data.Graph.Inductive.PatriciaTree (Gr) +-} +import qualified Data.Map as M +import qualified Data.List as L + +import Data.FsmActions +import Data.FsmActions.FGL + +-- | An 'FSM' is well-formed if all its actions are the same length, +-- none of its actions contain destinations which are out of range, +-- and it is not disjoint. +data WellFormed sy + -- | Lengths of Actions in the 'FSM' don't all match. Carries a + -- sorted list of (symbol, 'Action' length) pairs, one for every + -- symbol in the alphabet of the 'FSM'. + = BadLengths [(sy, Int)] + -- | Some 'Action's contain out-of-range (negative or too-high) + -- destinations. Carries a sorted list of all such actions and + -- their corresponding symbols. + | BadActions [(sy, Action)] + -- | The FSM is disconnected, i.e. not even weakly-connected. + -- Carries a list of its weakly-connected components (each is a + -- list of 'State's). + | Disconnected [[State]] + -- | Well-formed. + | WellFormed + deriving (Eq, Show) + +-- | Check if an 'FSM' is well-formed or not. +isWellFormed :: Ord sy => FSM sy -> WellFormed sy +isWellFormed fsm + | not $ allSame $ L.map snd actionLengths = + BadLengths (L.sort actionLengths) + | not $ M.null badParts = BadActions (L.sort $ M.toList badParts) + | length wccs /= 1 = Disconnected wccs + | otherwise = WellFormed + where -- All (symbol, Action length) pairs in FSM. + actionLengths = L.map (second aLength) (M.toList $ unFSM fsm) + -- Submap containing only Actions with bad destinations. + badParts = M.filter isBad $ unFSM fsm + -- Check if an Action has any bad destinations. + isBad a = any badDest (flatten a) + where -- Flatten lists of destination states in an Action. + flatten (Action xs) = L.concat $ map destinations xs + -- Check if a destination is bad (negative or too high). + badDest x = (x<0) || (x >= length (states fsm)) + -- Compute the length of an action + aLength (Action xs) = length xs + -- Compute the FSM's undirected strongly-connected + -- components. + wccs = weakCCs fsm + +-- Check if every element of a list is identical. +allSame :: Eq a => [a] -> Bool +allSame [] = True +allSame [_] = True +allSame (x:y:xs) = (x == y) && allSame (y:xs) diff --git a/doc/fsmActions.pdf b/doc/fsmActions.pdf Binary files a/doc/fsmActions.pdf and b/doc/fsmActions.pdf differ diff --git a/fsmActions.cabal b/fsmActions.cabal --- a/fsmActions.cabal +++ b/fsmActions.cabal @@ -1,5 +1,6 @@ Name: fsmActions -Version: 0.1 +Version: 0.2.0 +Stability: Alpha Synopsis: Finite state machines and FSM actions Description: This is a library for representing and manipulating finite state @@ -10,17 +11,27 @@ Category: Data License: BSD3 License-file: LICENSE +Homepage: http://projects.haskell.org/fsmActions/ +Copyright: Andy Gimblett Author: Andy Gimblett Maintainer: Andy Gimblett Build-Type: Simple -Cabal-Version: >=1.2 +Cabal-Version: >=1.6 Extra-source-files: README doc/fsmActions.pdf +Source-Repository head + Type: darcs + Location: http://code.haskell.org/fsmActions + Library - Build-Depends: base >= 3 && < 5, bytestring, containers, mtl, parsec, pretty + Build-Depends: base >= 3 && < 5, containers, fgl, graphviz + >=2999.0.0.0, mtl, parsec, pretty Exposed-modules: Data.FsmActions, Data.FsmActions.ActionMatrix, Data.FsmActions.Error, - Data.FsmActions.FsmMatrix + Data.FsmActions.FGL, + Data.FsmActions.FsmMatrix, + Data.FsmActions.GraphViz, + Data.FsmActions.WellFormed ghc-options: -fwarn-tabs -Wall