The ppFm functor

Synopsis

functor ppFm (LABEL) : sig ... end


This functor generates from an alphabet of labels a structure with functions to create, transform, and display finite machines over the alphabet.

The display-function assumes that the graph-drawing program dot of ATT is available in /usr/local/bin. (Some error messgages need to be added to the code.)

Functor result interface

include FM
eqtype label = Alphabet.label
val dot : label machine -> string -> unit
val viewgraph : string -> OS.Process.status
val display : label machine -> string -> OS.Process.status
val displayMinimize : label machine
                        -> string -> OS.Process.status
val displayDetermine : label machine
                         -> string -> OS.Process.status
val displayDetermineMinimize : label machine
                                 -> string
                                   -> OS.Process.status
val displayMinimizeHistory : label machine
                               -> string
                                 -> OS.Process.status


Description

eqtype label = Alphabet.label


the alphabet of instructions, resp. the labels of transitions, for finite machines.

dot m s

writes a description of m in the format of ATT's graph-drawing program dot to file s.tmp.dot.

viewgraph s

calls dot on file s.tmp.dot to produce a file s.tmp.ps, and then calls ghostview to preview s.tmp.ps. The filename is relative to the directory where SML was called.

display m s

uses dot and viewgraph to display the machine on the standard output. Writes files s.tmp.dot and s.tmp.ps and leaves these for possible further use.

States are displayed with an elliptic shape, except that the shape of initial states is a diamond, and the final states have a double border line.

displayMinimize m s

minimizes the deterministic(!) machine m, displays m and the minimal deterministic machine equivalent to m, using state sets of m and numbered states. Writes files s.tmp.dot and s.tmp.ps.

displayDetermine m s

constructs a deterministic machine equivalent to m and displays it. Writes to files s.tmp.dot and s.tmp.ps.

displayDetermineMinimize m s

writes files s.tmp.dot and s.tmp.ps and displays in the following order: a) the automaton m, b) the deterministic version m2 of m obtained by the powerset construction, using sets of states of m to represent states of m2 c) the deterministic automation m2 with states renamed by numbers d) the minimal automaton m3 with states as sets of states of m2 e) the minimal automaton equivalent to m with states renamed by numbers. Leaves the files s.tmp.dot and s.tmp.ps for possible later use.

displayMinimizeHistory m s

writes files s.tmp.dot and s.tmp.ps and displays a history of the minimization of m, as a sequence of transition graphs (not showing initial and final states). Nodes i in a graph contain the member of a set Q.i of states of m, while arcs between Q.i and Q.j are labelled with a label a of m, paired with the list of states in Q.i that have in m a transition labelled a to a state in Q.j. The first graph has two nodes containing the final and non-final states of m, while the last graph is the minimal automaton equivalent to m, if initial and final states are indicated. Again, the files s.tmp.dot and s.tmp.ps are left for possible later use.

If a state i is split, a new state j is created that contains some of m's state numbers contained in i. The sequence of graphs does this in two steps: first, a graph is shown in which some arcs leaving i (namely, those whose source in m has been moved to j) are replaced by arcs leaving state j, but some arcs leading to state i still have to be redirected to j. This is done in the next graph.

See Also

LABEL, FM, ppRegExpFm

Discussion

Example:

Define a deterministic machine (with unreachable state 4) and display its graph:

structure sM = ppFm(StringLabels); 

val M = sM.make{start = [1],
                final = [3], 
                trans = [(1,"a",2),(1,"b",6),(2,"a",7),(2,"b",3),
                         (3,"a",1),(3,"b",3),(4,"a",3),(4,"b",7),
                         (5,"a",8),(5,"b",6),(6,"a",3),(6,"b",7),
                         (7,"a",7),(7,"b",5),(8,"a",7),(8,"b",3)]};

sM.display M "Mdet";

Since M was deterministic, making it deterministic shows that each equivalence class of states has a single member, but the unreachable state 4 is removed:

val (Md,EquivStates) = sM.determineWithStateAssoc M;

val Md = - : string machine
val EquivStates = [(0,[1]),(1,[6]),(2,[2]),(3,[7]),(4,[3]),(5,[5]),(6,[8])]
  : (int * int list) list

To relate states of M to states of the minimal automaton equivalent to M, inspect the sequence of graphs produced by:

sM.displayDetermineMinimize M "Mmin";