{- | 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 {- -- 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.Graph -- | 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 = fsmMap (\s -> \a -> (s, aLength a)) fsm -- Submap containing only Actions with bad destinations. -- XXX Re-improve this function; add natural map to FSM? badParts = M.filter isBad $ M.fromList $ toList 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)