Forlan Manual

The `RFA` Module

Synopsis

signature RFA structure RFA :> RFA

This module defines the abstract type of regular expression finite automata (RFAs).

Interface

type concr = { stats : Sym.sym Set.set, start : Sym.sym, accepting : Sym.sym Set.set, trans : TranReg.tran_reg Set.set } type rfa val valid : concr -> bool val fromConcr : concr -> rfa val toConcr : rfa -> concr val fromString : string -> rfa val input : string -> rfa val toPP : rfa -> PP.pp val toString : rfa -> string val output : string * rfa -> unit val states : rfa -> Sym.sym Set.set val startState : rfa -> Sym.sym val acceptingStates : rfa -> Sym.sym Set.set val transitions : rfa -> TranReg.tran_reg Set.set val compare : rfa Sort.total_ordering val equal : rfa * rfa -> bool val numStates : rfa -> int val numTransitions : rfa -> int val alphabet : rfa -> Sym.sym Set.set val sub : rfa * rfa -> bool val checkLP : (Str.str * Reg.reg -> bool) * rfa -> LP.lp -> unit val validLP : (Str.str * Reg.reg -> bool) * rfa -> LP.lp -> bool val fromFA : (Reg.reg -> Reg.reg) -> FA.fa -> rfa val eliminateState : (Reg.reg -> Reg.reg) -> rfa * Sym.sym -> rfa val faToReg : (Reg.reg -> Reg.reg) -> FA.fa -> Reg.reg val faToRegPerms : int option * (Reg.reg -> Reg.reg) -> FA.fa -> Reg.reg val faToRegPermsTrace : int option * (Reg.reg -> Reg.reg) -> FA.fa -> Reg.reg val jforlanNew : unit -> rfa val jforlanEdit : rfa -> rfa val jforlanValidate : string -> unit val jforlanPretty : string -> unit

Description

type concr = { stats : Sym.sym Set.set, start : Sym.sym, accepting : Sym.sym Set.set, trans : TranReg.tran_reg Set.set }

The concrete type of pre-regular expression finite automata, records consisting of a finite set stats ("states") of symbols, a symbol start ("start state"), a finite set accepting ("accepting states") of symbols, and a finite set trans ("transitions") of RFA transitions.

type rfa

The abstract type of regular expression finite automata, consisting of those pre-regular expression finite automata concr of type concr such that:

#start concr is an element of #stats concr;
#accepting concr is a subset of #stats concr;
for all elements (q, reg, r) of #trans concr, q and r are elements of #stats concr; and
for all elements q and r of #stats concr, there is at most one regular expression reg such that (q, reg, r) is an element of #trans concr.

We say that concr is valid iff concr satisfies the above conditions.

valid concr

tests whether concr is valid.

fromConcr concr

returns concr. Issues an error message if concr is not valid.

toConcr rfa

returns rfa.

fromString s

inputs an RFA from s.

input fil

inputs an RFA from the file named fil.

toPP rfa

returns a pretty-printing expression for rfa.

toString rfa

pretty-prints rfa to a string.

output(fil, rfa)

pretty-prints rfa to the file fil.

states rfa

returns the states of rfa.

startState rfa

returns the start state of rfa.

acceptingStates rfa

returns the accepting states of rfa.

transitions rfa

returns the transitions of rfa.

compare(rfa1, rfa2)

returns

  case SymSet.compare(states rfa1, states rfa2) of
       LESS    => LESS
     | EQUAL   =>
         (case Sym.compare(startState rfa1, startState rfa2) of
               LESS    => LESS
             | EQUAL   =>
                 (case SymSet.compare(acceptingStates rfa1, acceptingStates rfa2) of
                       LESS    => LESS
                     | EQUAL   =>
                         TranRegSet.compare
                         (transitions rfa1, transitions rfa2)
                     | GREATER => GREATER)
             | GREATER => GREATER)
     | GREATER => GREATER

equal(rfa1, rfa2)

tests whether rfa1 and rfa2 are equal.

numStates rfa

returns the number of states of rfa.

numTransitions rfa

returns the number of transitions of rfa.

alphabet rfa

returns the alphabet of rfa.

sub(rfa1, rfa2)

tests whether rfa1 is a sub-RFA of rfa2.

checkLP (memb, rfa) lp

checks whether lp is valid for rfa, using memb for testing whether the strings of lp are generated by regular expressions of rfa. checkLP silently returns (), if lp is valid, and explains why it isn't valid, if it's not valid.

checkLP (memb, rfa) lp

tests whether lp is valid for rfa, using memb for testing whether the strings of lp are generated by regular expressions of rfa.

fromFA simp fa

Converts fa to an RFA, using simp to simplify the regular expressions of transitions.

eliminateState simp (rfa, q)

eliminates the state q from rfa, using simp for regular expression simplification. Issues an error message if q is not a state of rfa, q is the start state of rfa, or q is one of the accepting states of rfa.

faToReg simp fa

converts fa to a regular expression by the state elimination algorithm, using simp for regular expression simplification.

faToRegPerms (NONE, simp) fa

works through all the bijections (permutations) rel on the states of fa, evaluating

faToReg simp
(FA.renameStates(fa, rel))

, and selecting the simplest answer (judged using Reg.compareComplexityTotal).

faToRegPerms (SOME n, simp) fa

works through the first n bijections (ordered by SymRel.compare) rel on the states of fa, evaluating

faToReg simp
(FA.renameStates(fa, rel))

, and selecting the simplest answer (judged using Reg.compareComplexityTotal). Issues an error message if n is negative.

val faToRegPermsTrace : int option * (Reg.reg -> Reg.reg) -> FA.fa -> Reg.reg

is like faToRegPerms, but issues tracing messages, explaining its operation.

jforlanNew()

invokes JForlan, and returns the RFA that the user creates and commits. Issues an error message if the user aborts, instead.

jforlanEdit rfa

invokes JForlan, letting the user edit rfa, and returning the resulting RFA that the user commits. Issues an error message if the user aborts, instead.

jforlanValidate

is a low-level function used by JForlan. See the code for more information.

jforlanPretty