{- | 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, polishFSM ) where import Control.Monad.Error import qualified Data.Map as M import qualified Data.List as L import Data.FsmActions import Data.FsmActions.Error import {-# SOURCE #-} Data.FsmActions.Graph (weakCCs) -- | 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.concatMap 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 -- | Given an FSM, normalise it and check it's well-formed. -- -- This should be called whenever an FSM is read/computed from an -- outside source. If parsing, the right time to call this is -- immediately after you've decided if the parse of the FSM was -- successful or not. (In other words, here are some static checks!) polishFSM :: (Ord sy, Show sy) => FSM sy -> ReadFsmMonad (FSM sy) polishFSM fsm = let norm = normalise fsm in case isWellFormed norm of WellFormed -> return norm Disconnected wccs -> throwError (FsmError "FSM disconnected" (show wccs)) err -> throwError (FsmError "FSM ill-formed" (show err)) -- 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)