WellFormed.hs

{- |

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)