\documentclass[12pt, a4paper]{article} \usepackage{a4wide} \usepackage{amsmath,amssymb, amsthm} \usepackage{listings} \usepackage{parskip} \usepackage{pgf} \usepackage{subfig} \usepackage{tikz} \usetikzlibrary{arrows,automata} \lstdefinestyle{haskell} {language=Haskell, columns=fullflexible, breaklines=true, frame=single } \lstnewenvironment{haskell}{\lstset{style=haskell}}{} \newcommand{\defn}{\textbf} \newcommand{\secref}[1]{$\S$\ref{#1}} \newcommand{\comprehend}{\;|\;} \newcommand{\powerset}[1]{\mathcal{P}(#1)} \newcommand{\suchthat}{\;\bullet\;} \newcommand{\states}{S} \newcommand{\state}{p} \newcommand{\stateAlt}{q} \newcommand{\stateAltAlt}{r} \newcommand{\alphabet}{\Sigma} \newcommand{\letter}{a} \newcommand{\strings}{\Sigma^*} \newcommand{\emptystring}{\lambda} \newcommand{\word}{w} \newcommand{\wordAlt}{x} \newcommand{\wordAltAlt}{y} \newcommand{\transition}{\curvearrowright} \newcommand{\transitionset}[2]{#1_{\stackrel{\transition}{#2}}} \newcommand{\goesto}[3]{#1\!\stackrel{#2}{\transition}\!#3} \newcommand{\stringtransition}{\twoheadrightarrow} \newcommand{\stringgoesto}[3]{#1\!\stackrel{#2}{\stringtransition}\!#3} \newcommand{\destinationset}[2]{#1_{\action{#2}}} \newcommand{\destinationequiv}[1]{\sim_{#1}} \newcommand{\action}[1]{\overrightarrow{#1}} \newcommand{\actionequiv}{\sim} \title{\texttt{fsmActions} -- a Haskell library for\\finite state machines \& FSM actions} \author{Andy Gimblett\\\texttt{haskell@gimbo.org.uk}} \date{version 0.4.0 --- October 21, 2009} \begin{document} \maketitle \emph{Please note that \secref{sec:implementation} of this document is falling somewhat behind reality; however, the library's Haddock documentation is up to date and fairly complete -- and the rest of this document is accurate and relevant.} \section{Introduction} This is a library for representing and manipulating \emph{finite state machines} (FSMs) in Haskell, with an emphasis on computing the effects of sequences of transitions across entire machines (which we call \emph{actions}), and in particular investigating \emph{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 \emph{undo}); for that we need a representation geared towards such comparisons -- hence this library, and its idiosyncratic view of what's important about FSMs, which differs somewhat from alternative definitions the reader may be familiar with. E.g. we are unconcerned with start/accepting states (as found in finite automata), and -- for now at least -- output functions (as found in finite state transducers). We are interested only in finite machines with total transition functions, else we might call our machines labelled transition systems. Future versions of the library might add some or all of these features, particularly if someone else has an itch to scratch. More generally, perhaps someone else will find this useful, hence its release as a library. The rest of this document is structured as follows. Section \ref{sec:definitions} introduces and defines the mathmatical abstractions on which the library is based. Section \ref{sec:implementation} outlines the current implementation in Haskell, though the full details are left to the Haddock documentation. Section \ref{sec:future_work} suggests future work. Section \ref{sec:history} describes the history of the library. \section{Definitions} \label{sec:definitions} \subsection{Finite state machines} \label{sec:basic_definitions_fsm} \label{sec:eliminating_implicit_self_loops} For the purpose of this library, a \defn{finite state machine} (FSM) is a tuple $(\states, \alphabet, \transition)$ where $\states$ is a finite set (of states), $\alphabet$ is a finite set (of symbols) called the system's \defn{alphabet}, and $\transition \; : \states \times \alphabet \rightarrow \powerset{\states}$ is a total function, called the machine's \defn{transition function} (we have chosen to define $\transition$ as a total function to the powerset of states, as this unifies the treatment of deterministic and nondeterministic machines). Given $\state \in \states$ and $\letter \in \alphabet$, we call the set of states in $\transition\!(\state, \letter)$ the \defn{transition set} for $\letter$ at $\state$, written $\transitionset{\state}{\letter}$. We introduce an infix shorthand for single \defn{transitions}: \begin{quote} $\forall \; \state, \stateAlt \in \states \suchthat \forall \; \letter \in \alphabet \suchthat \goesto{\state}{\letter}{\stateAlt} \iff \stateAlt \in \transitionset{\state}{\letter}$ \end{quote} Here, $\state$ and $\stateAlt$ are called the \defn{source} and \defn{destination} states of the transition, respectively, and $\letter$ is called its \defn{label}. \subsubsection*{Example} %% Adapted from http://www.texample.net/tikz/examples/state-machine/ \begin{figure} \centering \subfloat[A finite state machine]{ \begin{minipage}[b]{0.4\textwidth} \label{fig:deterministic_fsm_full} \begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=2.8cm, semithick] \tikzstyle{every state}=[fill=blue,draw=none,text=white] \node[state] (A) {$A$}; \node[state] (B) [above right of=A] {$B$}; \node[state] (C) [below right of=B] {$C$}; \node[state] (D) [below right of=A] {$D$}; \path (A) edge node {x} (B) edge node {y} (C) (B) edge [loop above] node {x} (B) edge node {y} (C) (C) edge [loop right] node {y} (C) edge node {x} (D) (D) edge [loop below] node {x} (D) edge node {y} (A); \end{tikzpicture} \end{minipage}} \hspace{0.08\textwidth} \subfloat[With self-loops removed]{ \begin{minipage}[b]{0.4\textwidth} \label{fig:deterministic_fsm_noselfloops} \begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=2.8cm, semithick] \tikzstyle{every state}=[fill=blue,draw=none,text=white] \node[state] (A) {$A$}; \node[state] (B) [above right of=A] {$B$}; \node[state] (C) [below right of=B] {$C$}; \node[state] (D) [below right of=A] {$D$}; \path (A) edge node {x} (B) edge node {y} (C) (B) edge node {y} (C) (C) edge node {x} (D) (D) edge node {y} (A); \end{tikzpicture} \end{minipage}} \caption{Two graphical representations of the same FSM} \label{fig:deterministic_fsm} \end{figure} Consider the FSM illustrated in figure \ref{fig:deterministic_fsm}\subref{fig:deterministic_fsm_full}, i.e. $(\states, \alphabet, \transition)$ with: \begin{eqnarray*} \states & = & \{A, B, C, D \}\\ \alphabet & = & \{ x, y \} \\ \transition & = & \{ \goesto{A}{x}{B}, \goesto{A}{y}{C}, \goesto{B}{x}{B}, \goesto{B}{y}{C}, \goesto{C}{x}{D}, \goesto{C}{y}{C}, \goesto{D}{x}{D}, \goesto{D}{y}{A} \} \end{eqnarray*} Note abuse of notation in enumerating $\transition$ here; properly it would written as \begin{eqnarray*} \transition & = & \{ (A, x) \mapsto \{ B \}, (A, y) \mapsto \{ C \} , (B, x) \mapsto \{ B \}, (B, y) \mapsto \{ C \}, \cdots \} \end{eqnarray*} So, e.g. $\transitionset{A}{x} = \{ B \}$, $\transitionset{A}{y} = \{ C \}$, etc. This FSM includes a number of \defn{self-loops}, e.g. $\goesto{B}{x}{B}$. Because $\transition$ is total, self-loops may in general be omitted from FSM representations without difficulty: provided $\states$ and $\alphabet$ are known, the self-loops may be easily inferred. For example, figure \ref{fig:deterministic_fsm}\subref{fig:deterministic_fsm_noselfloops} illustrates the same FSM without self-loops, and we could write it out as: \begin{eqnarray*} \states & = & \{A, B, C, D \}\\ \alphabet & = & \{ x, y \} \\ \transition & = & \{ \goesto{A}{x}{B}, \goesto{A}{y}{C}, \goesto{B}{y}{C}, \goesto{C}{x}{D}, \goesto{D}{y}{A}, \} \end{eqnarray*} \subsection{Nondeterminism} \label{sec:nondeterminism} \label{sec:nondeterminism_and_self_loops} An FSM $(\states, \alphabet, \transition)$ is \defn{nondeterministic} (an NFSM) if the transition set for some word at some state has more than one member. Equivalently, if: \begin{quote} $\exists~\state, \stateAlt, \stateAltAlt \in \states \wedge \exists~\letter \in \alphabet \suchthat \goesto{\state}{\letter}{\stateAlt} \wedge \goesto{\state}{\letter}{\stateAltAlt} \wedge \stateAlt \neq \stateAltAlt$ \end{quote} Otherwise the machine is \defn{deterministic} (a DFSM). \subsubsection*{Examples} \begin{figure} \centering \begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=2.8cm, semithick] \tikzstyle{every state}=[fill=blue,draw=none,text=white] \node[state] (E) {$E$}; \node[state] (F) [above right of=E] {$F$}; \node[state] (G) [below right of=F] {$G$}; \node[state] (H) [below right of=E] {$H$}; \path (E) edge node {k} (F) edge node {k} (G) % edge [loop left] node {j} (E) % implicit self-loop (F) edge node {j} (G) %edge [loop above] node {k} (F) % implicit self-loop (G) edge node {k} (H) % edge [loop right] node {j} (G) % implicit self-loop (H) edge node {j} (E) % edge [loop right] node {k} (H) % implicit self-loop edge [loop below] node {j} (H); % explicit self-loop \end{tikzpicture} \caption{A nondeterministic FSM} \label{fig:nondeterministic_fsm} \end{figure} Both machines in figure \ref{fig:deterministic_fsm} are deterministic. Figure \ref{fig:nondeterministic_fsm} illustrates a nondeterministic FSM where $\states = \{ E, F, G, H \}$ and $\alphabet = \{ j, k\}$ (with implicit self-loops omitted, e.g. $\goesto{E}{j}{E}$). Here, for example, we have $\transitionset{E}{k} = \{ F, G \}$, i.e. both $\goesto{E}{k}{F}$ and $\goesto{E}{k}{G}$. In \secref{sec:eliminating_implicit_self_loops} we stated that self-loops may in general be omitted from FSM representations, and inferred as required. With NFSMs, some care must be taken. Consider the example in figure \ref{fig:nondeterministic_fsm}; as well as four implicit self-loops, there is also an \emph{explicit} self-loop $\goesto{H}{j}{H}$. This \emph{cannot} be removed, because it is a source of nondeterminism, along with $\goesto{H}{j}{E}$. \subsection{Strings and destination sets} We adopt the standard definition of \defn{strings} over an alphabet. Specifically, if $\alphabet$ is an alphabet then $\strings$, the set of strings over $\alphabet$ is the smallest set such that: \begin{enumerate} \item $\strings$ contains the empty string: $\emptystring \in \strings$ \item $\word \in \strings \wedge \letter \in \alphabet \implies \word\letter \in \strings$ \end{enumerate} Then the transition function $\transition \; : (\states \times \alphabet) \rightarrow \powerset{\states}$ may be lifted to the \defn{string transition function} $\stringtransition \; : (\states \times \strings) \rightarrow \powerset{\states}$ as follows: \begin{enumerate} \item $\stringtransition\!(\state, \emptystring) = \{ \state \}$ \item $\stringtransition\!(\state, \word\letter) = \bigcup \; \{ \transitionset{\stateAlt}{\letter} \comprehend \stateAlt \in \destinationset{\state}{\word} \}$ \end{enumerate} Given $\state \in \states$ and $\word \in \strings$, we call the set of states in $\stringtransition\!(\state, \word)$ the \defn{destination set} for $\word$ at $\state$, written $\destinationset{\state}{\word}$. As with single symbols, we introduce an infix shorthand for single \defn{string transitions}: \begin{quote} $\forall \; \state, \stateAlt \in \states \suchthat \forall \; \word \in \strings \suchthat \stringgoesto{\state}{\word}{\stateAlt} \iff \stateAlt \in \destinationset{\state}{\word}$ \end{quote} Given $\state \in \states$, two strings are said to be \defn{destination equivalent} at $\state$, written $\destinationequiv{\state}$, if their destination sets at $\state$ are identical: \begin{quote} $\forall \; \state \in \states \suchthat \forall \; \word, \wordAlt \in \strings \suchthat \word \destinationequiv{\state} \wordAlt ~ \Longleftrightarrow ~ \destinationset{\state}{\word} \; = \; \destinationset{\state}{\wordAlt}$ \end{quote} \subsubsection*{Examples} Consider the DFSM in figure \ref{fig:deterministic_fsm}; here we have, for example $\stringgoesto{A}{xyxxx}{D}$ and $\stringgoesto{C}{xyxxx}{B}$. Consider the NFSM in figure \ref{fig:nondeterministic_fsm}; here we have (for example) $\destinationset{E}{kkjjk} = \{ H, F \}$, so that both $\stringgoesto{E}{kkjjk}{H}$ and $\stringgoesto{E}{kkjjk}{F}$. \subsection{Actions and action equivalence} \label{sec:actions} Given an FSM $(\states, \alphabet, \transition)$, for every $\word \in \strings$, $w$'s \defn{action}, written $\action{\word} \; \subseteq \states \times \powerset{\states}$ captures its effect across every state in $\states$: \begin{quote} $\action{\word} = \{ (\state, \destinationset{\state}{\word}) \comprehend \state \in \states \}$ \end{quote} Thus, an action captures the effect of a string of transitions, across all states in the machine. An action is \defn{deterministic} if, for every one of its pairs, the destination set found in the pair's second element has only a single member; otherwise it is \defn{nondeterministic}. We state without proof that an FSM is deterministic if and only if all of its actions are deterministic. Two strings are said to be \defn{action equivalent}, written $\actionequiv$, if their actions are identical: \begin{quote} $\forall \word, \wordAlt \in \strings \suchthat \word \actionequiv \wordAlt ~ \Longleftrightarrow ~ \action{\word} \; = \; \action{\wordAlt}$ \end{quote} \subsubsection{Examples} Consider again the FSM in figure \ref{fig:deterministic_fsm}. Here are some actions over this machine: \begin{eqnarray*} \action{x} & = & \{ (A,\{B\}), (B,\{B\}), (C,\{D\}), (D,\{D\}) \} \\ \action{y} & = & \{ (A,\{C\}), (B,\{C\}), (C,\{C\}), (D,\{A\}) \} \\ \action{xx} & = & \{ (A,\{B\}), (B,\{B\}), (C,\{D\}), (D,\{D\}) \} \\ \action{xy} & = & \{ (A,\{C\}), (B,\{C\}), (C,\{A\}), (D,\{A\}) \} \\ \action{xxx} & = & \{ (A,\{B\}), (B,\{B\}), (C,\{D\}), (D,\{D\}) \} \\ \action{xyy} & = & \{ (A,\{C\}), (B,\{C\}), (C,\{C\}), (D,\{C\}) \} \end{eqnarray*} Notice that $xx \actionequiv xxx$, for example, and that all of these actions are determinstic -- as we would expect as the FSM is determinstic too. Conversely, consider the nondeterministic FSM in figure \ref{fig:nondeterministic_fsm}. Here we have some nondeterminstic actions, e.g. \begin{eqnarray*} \action{j} & = & \{ (E, \{ E \}), (F, \{ G \}), (G, \{ G \}), (H, \{ E, H\}) \} \\ \action{jk} & = & \{ (E, \{ F, G \}), (F, \{ H \}), (G, \{ H \}), (H, \{ F, G, H \}) \} \\ \action{jkj} & = & \{ (E, \{ G \}), (F, \{ E, H \}), (G, \{ E, H \}), (H, \{ E, G, H \}) \} \end{eqnarray*} \section{Implementation} \label{sec:implementation} \emph{Please note that this section is falling somewhat behind reality; however, the library's Haddock documentation is up to date and fairly complete.} \subsection{\texttt{Data.FsmActions}} \subsubsection{States, destination sets, actions, and words} The current Haskell implementation is focused strongly on actions, and makes some simplifying assumptions about FSMs. In particular, the members of the set $\states$ of states are integers, counting upwards from 0 (so e.g. in an FSM with 5 states, $S = \{ 0, 1, 2, 3, 4 \}$. In the current implementation, $\states$ is not represented explicitly, but rather implicitly, as a property of the actions in the FSM (see below). \begin{haskell} type State = Int \end{haskell} A destination set then consists of a set of integers, where all members of the set must be smaller than the number of states in the FSM. In the current implementation, we represent such sets as plain Haskell integer lists: \begin{haskell} newtype DestinationSet = DestinationSet { destinations :: [State] } deriving (Eq, Ord, Show) \end{haskell} Then an action is just a list of destination sets; the index of each destination set within the list is the set's corresponding source state; for example, the first entry in the list contains the destination set for state 0. Contrast this with the definition in \secref{sec:actions}, where source states are explicitly paired with their destination sets. \begin{haskell} newtype Action = Action { destinationSets :: [DestinationSet] } deriving (Eq, Ord, Show) \end{haskell} Actions may be constructed either directly using the \texttt{Action} constructor, or via convenience functions obviating the need to decorate destination lists with the \texttt{DestinationSet} constructor. \begin{haskell} mkAction :: [[State]] -> Action mkDAction :: [State] -> Action \end{haskell} Finally, we introduce a type, \texttt{Word}, for sequences of symbols. \begin{haskell} newtype Word sy = Word [sy] \end{haskell} \subsubsection{Finite state machines} A finite state machine is then a mapping from alphabet symbols to actions; each action tells us the effect, over the whole machine, of a particular singleton symbol. Note that this is parametric over the symbol type --- typically we expect to use \texttt{Char}s or \texttt{String}s. \begin{haskell} newtype FSM sy = FSM { unFSM :: M.Map sy Action } deriving (Eq, Ord, Show) \end{haskell} It's then easy to compute the machine's set of states (from the length of the first action found in the map, assuming they're all the same length -- see \secref{sec:wellformedness}) and its alphabet (just the keys of the map); but note that both of these results are lists, not sets. \begin{haskell} states :: FSM sy -> [State] alphabet :: FSM sy -> [sy] \end{haskell} For convenience, we expose the \texttt{lookup} function of an \texttt{FSM}'s underlying \texttt{Map}. \begin{haskell} fsmAction :: Ord sy => sy -> FSM sy -> Maybe Action \end{haskell} \subsubsection{Normalisation} An FSM which may be \emph{normalised}, which ensures that all of its actions' destination sets are non-empty (empty ones become self-loops), are sorted and free from duplicates. Like well-formedness checks, this can be useful for cleaning data after I/O or conversion from other formats. \begin{haskell} normalise :: FSM sy -> FSM sy \end{haskell} \subsubsection{Computing actions/equivalences for strings} Given the actions for two strings $\word$ and $\wordAlt$, \texttt{append} computes the action for the string $\word\wordAlt$ formed by concatenating the strings. We map over every source state in the first action, and for every state in each destination set, we (\texttt{appendAtState}) look up the set of destination states reached from that state via the second action (\texttt{actionLookup}), collecting the results for each source state by flattening the list produced, sorting it, and removing duplicates. \begin{haskell} append :: Action -> Action -> Action appendAtState :: DestinationSet -> Action -> DestinationSet actionLookup :: Action -> State -> DestinationSet \end{haskell} While this works nicely as an easily comprehensible canonical implementation of \texttt{append} --- and is handy for testing purposes --- we suspect a more efficient algorithm, probably based on a better representation than Haskell lists, will be found for future versions of the library. It's then quite straightforward to compute the action of a given word (by folding \texttt{append} over the actions for the word's constituent symbols), and to test action equivalences on words. Note that since a word may include symbols not in the machine's alphabet, \texttt{action}'s return type (and much of the computation) necessarily has type \texttt{Maybe Action}. \begin{haskell} action :: Ord sy => FSM sy -> Word sy -> Maybe Action actionEquiv :: Ord sy => FSM sy -> Word sy -> Word sy -> Bool \end{haskell} \subsubsection{Computing destination sets/equivalences for strings} Given a method to compute actions, computation of destination sets and destination equivalences is then straightforward (with the same comment regarding the use of \texttt{Maybe}). \begin{haskell} destinationSet :: Ord sy => FSM sy -> State -> Word sy -> Maybe DestinationSet destinationEquiv :: Ord sy => FSM sy -> State -> Word sy -> Word sy -> Bool \end{haskell} \subsubsection{The identity action} An FSM's \defn{identity action} is the action which maps all states back onto just themselves. Because this depends on the size of the FSM, there is no general identity action for all FSMs --- which is the primary reason \texttt{FSM} is not an instance of \texttt{Data.Monoid}. \begin{haskell} fsmIdentity :: FSM sy -> Action identity :: Int -> Action \end{haskell} \subsubsection{Determinism checks} We can test if an action or FSM is determinstic. \begin{haskell} isDAction :: Action -> Bool isDFSM :: FSM sy -> Bool \end{haskell} \subsection{\texttt{Data.FsmActions.WellFormed}} \label{sec:wellformedness} In our implementation, an FSM is well-formed provided: \begin{itemize} \item Every action is the same length (the number of states in the machine). \item None of those destination sets contain out-of-range destination state values (i.e. negative or too high). \item It is (at least) \emph{weakly connected} (see \secref{sec:weakly_connected_components}); otherwise, it is \emph{disconnected}. (Note that an FSM with no nodes is considered to be disconnected.) \end{itemize} An FSM should be checked for well-formedness after construction (which typically involves some I/O) using the \texttt{isWellFormed} function, which yields a \texttt{WellFormed} value encoding any problems found. \begin{haskell} data WellFormed sy = BadLengths [(sy, Int)] | BadActions [(sy, Action)] | Disconnected [[State]] | WellFormed deriving (Eq, Show) isWellFormed :: Ord sy => FSM sy -> WellFormed sy \end{haskell} If all actions do not have the same length, the \texttt{BadLengths} constructor contains a full list of (symbol, action length) pairs so discrepancies may be identified. Similarly, if some actions contain out-of-range destinations, the \texttt{BadActions} constructor lists the offending actions and their corresponding symbols. If the FSM is not at least weakly-connected, the \texttt{Disconnected} constructor lists its weakly-connected components. Finally, if all is well, the \texttt{WellFormed} constructor is used. \subsection{\texttt{Data.FsmActions.FsmMatrix}} Matrix-based serialisation/deserialisation of FSMs. Here an FSM is represented as a single matrix, with one (newline-separated) row per state, and one (whitespace-separated) column per symbol. The first row contains symbol names. Subsequent rows contain destination sets as comma-separated lists of states. State/row numbering starts at 0. Note that this representation currently suffers from the restriction that symbol names may not contain whitespace. TODO: check, and then consider fixing this (or at least providing a workaround, e.g. allowing double-quoted symbol names). TODO: Say more here, and give examples. \subsection{\texttt{Data.FsmActions.ActionMatrix}} Actionmatrix-based serialisation/deserialisation of FSMs. Here an FSM is represented as a collection of binary adjacency matrices, one per action. TODO: Say more here, and give examples. \subsection{\texttt{Data.FsmActions.Graph}} \label{sec:weakly_connected_components} \texttt{fsmToFGL} converts an \texttt{FSM} into an \texttt{fgl}\footnote{Functional Graph Library: \texttt{http://hackage.haskell.org/package/fgl}} graph with labelled edges and unlabelled nodes. The \texttt{SelfLoops} data type encodes whether to keep all self-loops, or trim all those which are not sources of nondeterminism --- see \secref{sec:nondeterminism_and_self_loops}. \begin{haskell} data SelfLoops = Keep | Trim deriving Eq fsmToFGL :: FSM sy -> SelfLoops -> Gr () sy \end{haskell} \texttt{strongCCs} and \texttt{weakCCs} compute an \texttt{FSM}'s strongly-connected and weakly-connected components respectively, where the WCCs are the SCCs of an \emph{undirected} graph of the machine. \begin{haskell} strongCCs :: Eq sy => FSM sy -> [[State]] weakCCs :: Eq sy => FSM sy -> [[State]] \end{haskell} \begin{figure} \centering \subfloat[\texttt{strong}]{ \begin{minipage}[b]{0.25\textwidth} \label{fig:strongly_connected_fsm} \centering \begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=2.8cm, semithick] \tikzstyle{every state}=[fill=blue,draw=none,text=white] \node[state] (A) {$0$}; \node[state] (B) [below of=A] {$1$}; \node[state] (C) [right of=A] {$2$}; \node[state] (D) [below of=C] {$3$}; \path (A) edge [bend right] node {x} (B) edge [bend right] node {y} (C) (B) edge [bend right] node {x} (A) (C) edge [bend right] node {x} (D) edge [bend right] node {y} (A) (D) edge [bend right] node {x} (C); \end{tikzpicture} \end{minipage}} \hspace{0.08\textwidth} \subfloat[\texttt{weak}]{ \begin{minipage}[b]{0.25\textwidth} \label{fig:weakly_connected_fsm} \centering \begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=2.8cm, semithick] \tikzstyle{every state}=[fill=blue,draw=none,text=white] \node[state] (A) {$0$}; \node[state] (B) [below of=A] {$1$}; \node[state] (C) [fill=red,right of=A] {$2$}; \node[state] (D) [fill=red,below of=C] {$3$}; \path (A) edge [bend right] node {x} (B) edge node {y} (C) (B) edge [bend right] node {x} (A) (C) edge [bend right] node {x} (D) (D) edge [bend right] node {x} (C); \end{tikzpicture} \end{minipage}} \hspace{0.08\textwidth} \subfloat[\texttt{disc}]{ \begin{minipage}[b]{0.25\textwidth} \label{fig:disconnected_fsm} \centering \begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=2.8cm, semithick] \tikzstyle{every state}=[fill=blue,draw=none,text=white] \node[state] (A) {$0$}; \node[state] (B) [below of=A] {$1$}; \node[state] (C) [fill=red,right of=A] {$2$}; \node[state] (D) [fill=red,below of=C] {$3$}; \path (A) edge [bend right] node {x} (B) (B) edge [bend right] node {x} (A) (C) edge [bend right] node {x} (D) (D) edge [bend right] node {x} (C); \end{tikzpicture} \end{minipage}} \caption{Strongly connected, weakly connected, and disconnected FSMs} \label{fig:sccs} \end{figure} Consider figure \ref{fig:sccs}. \texttt{strong} is strongly-connected; \texttt{weak} is weakly connected but not strongly connected; \texttt{disc} is not even weakly-connected (it is \emph{disconnected}): \begin{math} \begin{array}{rcccccl} \textrm{strongCCs}(\textrm{strong}) &=& \textrm{weakCCs}(\textrm{strong}) &=& \textrm{weakCCs}(\textrm{weak}) &=& \{\{0,1,2,3\}\} \\ \textrm{strongCCs}(\textrm{weak}) &=& \textrm{strongCCs}(\textrm{disc}) &=& \textrm{weakCCs}(\textrm{disc}) &=& \{\{0,1\},\{2,3\}\} \end{array} \end{math} For graph output, \texttt{fsmToDot} converts an \texttt{FSM} to a \texttt{DotGraph}\footnote{From the \texttt{graphviz} library: \texttt{http://hackage.haskell.org/package/graphviz}} with labelled edges and integer-labelled nodes, and all self-loops removed except sources of nondeterminism (see \secref{sec:wellformedness}). It's fairly trivial; more sophisticated graph-drawing could be achieved by rolling your own based on this code. Similarly, \texttt{fsmToGML} converts an \texttt{FSM} to a GML\footnote{Graph Modelling Language: \texttt{http://en.wikipedia.org/wiki/Graph\_Modelling\_Language}} format graph. \begin{haskell} fsmToDot :: (Ord sy, CleanShow sy) => FSM sy -> DotGraph fsmToGML :: CleanShow sy => FSM sy -> Doc \end{haskell} Note that both of these functions require the symbol type to be an instance of the \texttt{CleanShow} typeclass. Defined in this same module, this subclasses the standard \texttt{Show} typeclass, providing a \texttt{cleanShow} function which acts like \texttt{show} except that it special-cases \texttt{String} and \texttt{Char} so they are not quoted. For example, while \texttt{show "s"} is \texttt{"s"}, \texttt{cleanShow "s"} is just \texttt{s}, which is more like what you want for graph labels. Anyway, labels of any type which is an instance of \texttt{Show} should `just work' with the default implementation. \section{Future work} \label{sec:future_work} \subsection{More examples} Add more examples of the various representations. \subsection{Quickcheck tests} We currently have some HUnit-based unit tests, but there are some properties which could usefully be QuickChecked, for example: \begin{quote} $\forall \word, \wordAlt, \wordAltAlt \in \strings \suchthat w = xy \implies \action{w} = append(\action{x}, \action{y})$ \end{quote} \subsection{Faster representations} Plain Haskell lists are surely not the fastest representation we could use; in particular, appending actions is based on many lookups of destination sets within actions, via \texttt{(!!)}, which is $O(n)$. A tree-based representation should give us $O(\log n)$. An unboxed representation (since, ultimately, we're just looking up integers) would be even better --- but as destination sets vary in size, it's not currently clear how to implement that. Memoization may also have a role to play. \subsection{Interfaces to other packages} \label{sec:future_work_interfaces} \texttt{halex}? \section{History} \label{sec:history} \subsection{version 0.1 -- June 30, 2009} First version of the library, Cabal-ised and released to Hackage. Naive implementation based on plain Haskell lists. Support for \texttt{ActionMatrix} and \texttt{FsmMatrix} serialisation formats. HUnit for unit tests. \subsection{version 0.2.0 -- July 18, 2009} Cleaned up \texttt{WellFormed}, and broke it out into its own module. Added \texttt{ActionMatrix} output and some test cases. Added \texttt{fgl} interface, including computation of strongly/weakly-connected components. Added \texttt{graphviz} interface. Conform to Haskell package versioning policy\footnote{\texttt{http://www.haskell.org/haskellwiki/Package\_versioning\_policy}}. \subsection{version 0.3.0 -- July 20, 2009} Added GML (Graph Modelling Language) output. Unified FGL, GraphViz and GML modules into \texttt{Data.FsmActions.Graph}. Fixed for latest \texttt{graphviz} library. \subsection{version 0.4.0 -- October 21, 2009} Added FGL (Functional Graph Library) input. Added \texttt{FsmEdges} input/output (graph format produced by Mathematica). Added `ActionSpecs' to \texttt{FsmActions} I/O formats, so that individual \texttt{ActionMatrix} files don't have to be explicitly identified. Added intelligent/unified load/save (in \texttt{Data.FsmActions.IO}). Fixed for latest \texttt{graphviz} library. Improved error handling. Section \secref{sec:implementation} of this documentation is now falling behind, however. \subsection{version 0.4.3 -- July 20, 2011} Alterations tracking updates to the \texttt{graphviz} library. \end{document} \endinput