diff --git a/Data/FsmActions.hs b/Data/FsmActions.hs new file mode 100644 --- /dev/null +++ b/Data/FsmActions.hs @@ -0,0 +1,242 @@ +{- | + +Finite state machines. + +Here an 'FSM' is a map from symbols to actions. Symbols are parametric +(will usually be Strings or Chars). 'Action's specify the action of a +symbol on each state, and are represented as lists of transitions: one +per state. States are just numbers, from 0 to n, corresponding to +indices on transition lists in 'Action's. Then deterministic actions +are just Ints, identifying the state to transition to under that +action; nondeterministic actions are lists of Ints: all the states to +possibly transition to under that action. + +-} + +-- 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 +) where + +import Control.Arrow (second) +import Control.Monad +import qualified Data.List as L +import qualified Data.Map as M + +-- | States are integers, counting from zero. +type State = Int +-- Could be parametric (as in HaLeX), but for now, YAGNI. + +-- | Destination sets are just lists of 'State's. +newtype DestinationSet = DestinationSet { + destinations :: [State] + } deriving (Eq, Ord, Show) + +-- | Actions are lists of 'DestinationSets', indexed by source +-- 'State'. +newtype Action = Action { + destinationSets :: [DestinationSet] + } deriving (Eq, Ord, Show) + +-- | Finite state machine whose nodes are labelled with type sy. +newtype FSM sy = FSM { + unFSM :: M.Map sy Action + } deriving (Eq, Ord, Show) + +-- | Words are lists of symbols. +newtype Word sy = Word [sy] + + + +-- | Compute the list of states of the 'FSM'. Only really meaningful +-- if the FSM's well-formedness is not 'BadLengths'. With current +-- implementation, is just [0..n] for some n (or empty). +states :: FSM sy -> [State] +states fsm = case M.elems (unFSM fsm) of + ((Action ds):_) -> [0..length ds-1] + _ -> [] + +-- | Compute the alphabet of an 'FSM'. +alphabet :: FSM sy -> [sy] +alphabet = M.keys . unFSM + +-- | Look up a symbol's 'Action' in an 'FSM' +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 + +-- | Build a deterministic action given a list of destination states. +mkDAction :: [State] -> Action +mkDAction = Action . map (\x -> DestinationSet [x]) + +-- | Append two 'Action's, ie compute the 'Action' corresponding to +-- the application of the first followed by the second. +append :: Action -> Action -> Action +append (Action d1) a2 = Action $ map (flip appendAtState a2) d1 + +-- Given the 'DestinationSet' for some state, and an 'Action', compute +-- the 'DestinationSet' reached by following the 'Action' from each +-- each state in the 'DestinationSet', and collecting the results. +appendAtState :: DestinationSet -> Action -> DestinationSet +appendAtState (DestinationSet xs) a2 = + collect $ L.map destinations $ map (actionLookup a2) xs + where collect = DestinationSet . L.nub . L.sort . L.concat + +-- | Compute the 'DestinationSet' reached by following some 'Action' +-- from some 'State'. +actionLookup :: Action -> State -> DestinationSet +actionLookup (Action ds) src = ds !! src + +-- | Compute the 'Action' for some 'Word' over some 'FSM'. The word +-- might contain symbols outside the FSM's alphabet, so the result +-- could be Nothing. +action :: Ord sy => FSM sy -> Word sy -> Maybe Action +action fsm (Word syms) = foldM (liftMaybe append) (fsmIdentity fsm) actions + where actions :: [Maybe Action] + actions = map (flip M.lookup (unFSM fsm)) syms + liftMaybe :: (a -> a -> a) -> (a -> Maybe a -> Maybe a) + liftMaybe f x y = case y of Nothing -> Nothing + Just z -> Just $ f x z + +-- | Test if two 'Word's are action-equivalent over some FSM. +actionEquiv :: Ord sy => FSM sy -> Word sy -> Word sy -> Bool +actionEquiv fsm w1 w2 = action fsm w1 == action fsm w2 + + + +-- | Compute the 'DestinationSet' for some 'Word' at some 'State' of +-- an 'FSM'. The word might contain symbols outside the FSM's +-- alphabet, or the state might be out of range, so the result could +-- be Nothing. +destinationSet :: Ord sy => FSM sy -> State -> Word sy -> Maybe DestinationSet +destinationSet fsm src word = + if (src >= 0) && (src < (length $ states fsm)) + then case (action fsm word) of Just (Action ds) -> Just $ ds !! src + _ -> Nothing + + else Nothing + +-- | Test if two 'Word's are destination-equivalent at some 'State' of +-- an 'FSM'. +destinationEquiv :: Ord sy => FSM sy -> State -> Word sy -> Word sy -> Bool +destinationEquiv fsm src w1 w2 = + destinationSet fsm src w1 == destinationSet fsm src w2 + + + +-- | Compute the identity action for a given FSM. +fsmIdentity :: FSM sy -> Action +fsmIdentity = Action . map (\x -> DestinationSet [x]) . states + + + +-- | Test if an 'Action' is deterministic or not. +isDAction :: Action -> Bool +isDAction (Action destSets) = + all (\x -> (length (destinations x) == 1)) destSets + +-- | Compute whether an 'FSM' is deterministic or not. +isDFSM :: FSM sy -> Bool +isDFSM = L.all isDAction . M.elems . unFSM + + + +-- | Normalise an 'FSM', i.e. normalise all its 'Actions'. +normalise :: FSM sy -> FSM sy +normalise = FSM . M.map normaliseAction . unFSM + +-- Normalise an 'Action'. Ensures that all its 'DestinationSet's are +-- non-empty (empty ones becomes singleton transitions to self), +-- sorted, and free from redundancy. +normaliseAction :: Action -> Action +normaliseAction (Action destSets) = + Action $ L.map normDS $ zipWithIndex destSets + where -- If 'DestinationSet' is empty, replace it with a transition + -- to self. Otherwise, sort it and remove duplicates. + normDS :: (State, DestinationSet) -> DestinationSet + normDS (self, DestinationSet []) = DestinationSet [self] + normDS (_, DestinationSet x) = DestinationSet $ L.nub $ L.sort x + zipWithIndex :: [a] -> [(Int, a)] + zipWithIndex xs = zip [0..(length xs-1)] xs diff --git a/Data/FsmActions/ActionMatrix.hs b/Data/FsmActions/ActionMatrix.hs new file mode 100644 --- /dev/null +++ b/Data/FsmActions/ActionMatrix.hs @@ -0,0 +1,123 @@ +{- | + +Serialisation/deserialisation of 'Data.FsmActions.FSM's and +'Data.FsmActions.Action's as 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 +'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'. + +-} + +-- TODO: tests, working properly for empty strings, single element +-- rows, etc. + +module Data.FsmActions.ActionMatrix ( + readFSMFromMxFiles, + readAdjMxFromFile, + readAdjMxFromString +) 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 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 +-- directly. If you want to work with actions, use the Core +-- '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 + +-- | 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). +-- +-- 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 + 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 + case act of + Right a -> return a + Left e -> throwError (mkIOError userErrorType (show e) + Nothing (Just path)) + + + +-- | Given a bytestring we expect to contain a serialisation of an +-- adjacency matrix, compute the corresponding 'Data.FsmActions.Action'. +-- +-- 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)) + + + +-- | Given an 'AdjacencyMatrix', compute the corresponding +-- 'Data.FsmActions.Action'. +parseActionMatrix :: AdjacencyMatrix -> ReadMxMonad Action +parseActionMatrix 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 + 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) + 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 diff --git a/Data/FsmActions/Error.hs b/Data/FsmActions/Error.hs new file mode 100644 --- /dev/null +++ b/Data/FsmActions/Error.hs @@ -0,0 +1,33 @@ +{- | + +Error handling for FSMs. + +-} + +-- 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.Error ( + MxError(..), + ReadMxMonad +) where + +import Control.Monad.Error + +-- | Errors when reading matrices from strings. +data MxError = MxError { + -- | Explanatory message + msg :: String, + -- | Offending value + value :: String + } deriving (Eq) + +instance Error MxError where + noMsg = MxError "Matrix error" "" + strMsg s = MxError s "" + +instance Show MxError where + show (MxError message val) = message ++ " (" ++ val ++ ")" + +-- | Error monad for reading matrices from strings. +type ReadMxMonad = Either MxError diff --git a/Data/FsmActions/FsmMatrix.hs b/Data/FsmActions/FsmMatrix.hs new file mode 100644 --- /dev/null +++ b/Data/FsmActions/FsmMatrix.hs @@ -0,0 +1,120 @@ +{- | + +Serialisation/deserialisation of 'Data.FsmActions.FSM's as FSM transition +matrices. + +A 'Data.FsmActions.FSM' may be represented as an transition matrix whose +rows correspond to states of the FSM, and whose columns correspond to +its possible actions (labels on its transitions). A given cell then +represents the transition(s) from some (row) state under some (column) +action, and contains a comma-separated list of integers: the row +numbers of the destination states. (Of course, for a deterministic +action, there's just one, and no comma.) Rows are numbered from 0 and +increment strictly. + +-} + +module Data.FsmActions.FsmMatrix + (parseFsmFile, + parseFsmString, + printFsmMatrix, + ) +where + +import Control.Monad.Error +import Data.Char (isSpace) +import qualified Data.List as L +import qualified Data.Map as M +import System.IO.Error (mkIOError, userErrorType) +import qualified Text.ParserCombinators.Parsec as P +import Text.PrettyPrint.HughesPJ + +import Data.FsmActions +import Data.FsmActions.Error + +-- | Parse an FsmMatrix-formatted FSM held in a file, by reading the +-- file and calling 'parseFsmString'. +parseFsmFile :: FilePath -> IO (FSM String) +parseFsmFile path = + do contents <- readFile path + let result = parseFsmString contents + case result of + Right fsm -> return fsm + Left e -> throwError (mkIOError userErrorType (show e) + Nothing (Just path)) + +-- | 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 + Right parts -> + do fsm <- interpretFsm parts + case (isWellFormed fsm) of + WellFormed _ -> return fsm + err -> throwError (MxError "Fsm matrix ill-formed" (show err)) + Left err -> + throwError (MxError "Fsm matrix parse error" (show err)) + +-- 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) + where -- An action name is a string of non-whitespace characters. + actionName :: P.Parser String + actionName = P.many1 (P.satisfy (\c -> not $ isSpace c)) + -- A row of transitions is a space-separated line of transitions. + transitionRow :: P.Parser [[Int]] + transitionRow = transition `P.sepEndBy1` nonEOLSpace + -- A transition is a comma-separated list of states (no spaces). + transition :: P.Parser [Int] + 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) + -- 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)) + 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 + +-- Pretty printer to FsmMatrix format (building Doc not String). +ppFsmMatrix :: FSM String -> Doc +ppFsmMatrix fsm = actionRow $$ transitionRows + where -- Space-separated list of action names. + actionRow :: Doc + actionRow = hsep $ map (text . fst) asList + -- Newline-separated list of transition rows. + transitionRows :: Doc + transitionRows = vcat $ map transitionRow transitions + -- Space-separated list of transitions. + transitionRow :: [DestinationSet] -> Doc + transitionRow = hsep . map transition + -- Comma-separated list of state numbers. + transition :: DestinationSet -> Doc + transition = commas . map int . destinations + -- Extract transitions from FSM. + transitions :: [[DestinationSet]] + transitions = L.transpose $ map (destinationSets . snd) asList + asList :: [(String, Action)] + asList = M.toList $ unFSM fsm + -- 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/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,36 @@ +Copyright (c) 2009, Andy Gimblett +All rights reserved. + +Developed by: + + Andy Gimblett + http://www.cs.swan.ac.uk/~csandy/ + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are +met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditi ons and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of Andy Gimblett, Swansea University, nor the + names of its contributors may be used to endorse or promote + products derived from this software without specific prior + written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/README b/README new file mode 100644 --- /dev/null +++ b/README @@ -0,0 +1,20 @@ +fsmActions +========== + +This is a library for representing and manipulating finite state +machines (FSMs) in Haskell, with an emphasis on computing the effects +of sequences of transitions across entire machines (which we call +actions), and in particular investigating action equivalences between +such sequences. + +The motivation for writing this library is investigating models of +user interfaces; in this context, states are implicit, transitions +correspond to UI events (e.g. button presses), and sequences of +transitions correspond to sequences of user actions. We're interested +in comparing actions, which are the effects of sequences of +transitions across the whole device (for example, noticing when some +action is in fact an undo); for that we need a representation geared +towards such comparisons -- hence this library, and its idiosyncratic +view of FSMs. + +See doc/fsmActions.pdf for more information. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/doc/fsmActions.pdf b/doc/fsmActions.pdf new file mode 100644 Binary files /dev/null and b/doc/fsmActions.pdf differ diff --git a/fsmActions.cabal b/fsmActions.cabal new file mode 100644 --- /dev/null +++ b/fsmActions.cabal @@ -0,0 +1,26 @@ +Name: fsmActions +Version: 0.1 +Synopsis: Finite state machines and FSM actions +Description: + This is a library for representing and manipulating finite state + machines (FSMs) in Haskell, with an emphasis on computing the + effects of sequences of transitions across entire machines (which + we call actions), and in particular investigating action + equivalences between such sequences. +Category: Data +License: BSD3 +License-file: LICENSE +Author: Andy Gimblett +Maintainer: Andy Gimblett +Build-Type: Simple +Cabal-Version: >=1.2 +Extra-source-files: README + doc/fsmActions.pdf + +Library + Build-Depends: base >= 3 && < 5, bytestring, containers, mtl, parsec, pretty + Exposed-modules: Data.FsmActions, + Data.FsmActions.ActionMatrix, + Data.FsmActions.Error, + Data.FsmActions.FsmMatrix + ghc-options: -fwarn-tabs -Wall