Forlan Manual

The `FA` Module

Synopsis

signature FA structure FA :> FA

This module defines the abstract type of finite automata (FAs).

Interface

type concr = { stats : Sym.sym Set.set, start : Sym.sym, accepting : Sym.sym Set.set, trans : Tran.tran Set.set } type fa val valid : concr -> bool val fromConcr : concr -> fa val toConcr : fa -> concr val fromString : string -> fa val input : string -> fa val toPP : fa -> PP.pp val toString : fa -> string val output : string * fa -> unit val states : fa -> Sym.sym Set.set val startState : fa -> Sym.sym val acceptingStates : fa -> Sym.sym Set.set val transitions : fa -> Tran.tran Set.set val compare : fa Sort.total_ordering val equal : fa * fa -> bool val numStates : fa -> int val numTransitions : fa -> int val alphabet : fa -> Sym.sym Set.set val sub : fa * fa -> bool val transitionFun : fa -> Sym.sym * Str.str -> Sym.sym Set.set val transitionFunBackwards : fa -> Sym.sym * Str.str -> Sym.sym Set.set val processStr : fa -> Sym.sym Set.set * Str.str -> Sym.sym Set.set val accepted : fa -> Str.str -> bool val reachableStates : fa -> Sym.sym Set.set val liveStates : fa -> Sym.sym Set.set val deadStates : fa -> Sym.sym Set.set val reachified : fa -> bool val emptyClose : fa -> Sym.sym Set.set -> Sym.sym Set.set val emptyCloseBackwards : fa -> Sym.sym Set.set -> Sym.sym Set.set val renameStates : fa * SymRel.sym_rel -> fa val renameStatesCanonically : fa -> fa val isomorphism : fa * fa * SymRel.sym_rel -> bool val findIsomorphismOpt : fa * fa -> SymRel.sym_rel option val findIsomorphism : fa * fa -> SymRel.sym_rel val isomorphic : fa * fa -> bool val renameAlphabet : fa * SymRel.sym_rel -> fa val checkLP : fa -> LP.lp -> unit val validLP : fa -> LP.lp -> bool val findLPOpt : fa -> Sym.sym Set.set * Str.str * Sym.sym Set.set -> LP.lp option val findLP : fa -> Sym.sym Set.set * Str.str * Sym.sym Set.set -> LP.lp val findAcceptingLPOpt : fa -> Str.str -> LP.lp option val findAcceptingLP : fa -> Str.str -> LP.lp val emptyStr : fa val emptySet : fa val fromSym : Sym.sym -> fa val simplify : fa -> fa val simplified : fa -> bool val union : fa * fa -> fa val concat : fa * fa -> fa val closure : fa -> fa val genUnion : fa list -> fa val genConcat : fa list -> fa val rev : fa -> fa val fromStr : Str.str -> fa val fromReg : Reg.reg -> fa val jforlanNew : unit -> fa val jforlanEdit : fa -> fa 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 : Tran.tran Set.set }

The concrete type of pre-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 transitions.

type fa

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

#start concr is an element of #stats concr;
#accepting concr is a subset of #stats concr; and
for all elements (q, x, r) of #trans concr, q and r are elements of #stats 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 isn't valid.

toConcr fa

returns fa.

fromString s

inputs an FA from s.

input fil

inputs an FA from the file named fil.

toPP fa

returns a pretty-printing expression for fa.

toString fa

pretty-prints fa to a string.

output(fil, fa)

pretty-prints fa to the file fil.

states fa

returns the states of fa.

startState fa

returns the start state of fa.

acceptingStates fa

returns the accepting states of fa.

transitions fa

returns the transitions of fa.

compare(fa1, fa2)

returns

  case SymSet.compare(states fa1, states fa2) of
       LESS    => LESS
     | EQUAL   =>
         (case Sym.compare(startState fa1, startState fa2) of
               LESS    => LESS
             | EQUAL   =>
                 (case SymSet.compare(acceptingStates fa1, acceptingStates fa2) of
                       LESS    => LESS
                     | EQUAL   =>
                         TranSet.compare(transitions fa1, transitions fa2)
                     | GREATER => GREATER)
             | GREATER => GREATER)
     | GREATER => GREATER

equal(fa1, fa2)

tests whether fa1 and fa2 are equal.

numStates fa

returns the number of states of fa.

numTransitions fa

returns the number of transitions of fa.

alphabet fa

returns the alphabet of fa.

sub(fa1, fa2)

tests whether fa1 is a sub-FA of fa2.

transitionFun fa (q, x)

returns the set of all states r such that (q, x, r) is a transition of fa. Issues an error message if q is not a state of fa.

transitionFunBackwards fa (r, x)

returns the set of all states q such that (q, x, r) is a transition of fa. Issues an error message if r is not a state of fa.

processStr fa (qs, x)

processes x from qs in fa. Issues an error message if qs has an element that's not a state of fa.

accepted fa x

tests whether x is accepted by fa.

reachableStates fa

returns the set of all reachable states of fa.

liveStates fa

returns the set of all live states of fa.

deadStates fa

returns the set of all dead states of fa.

reachify fa

test whether all the states of fa are reachable.

emptyClose fa qs

returns the empty-closure of qs for fa. Issues an error message if qs has an element that's not a state of fa.

emptyCloseBackwards fa qs

returns the backwards empty-closure of qs for fa. Issues an error message if qs has an element that's not a state of fa.

renameStates(fa, rel)

renames the states of fa using the bijection rel. Issues an error message if rel is not a bijection from the states of fa to some set.

renameStatesCanonically fa

canonically renames the states of fa.

isomorphism(fa1, fa2, rel)

tests whether rel is an isomorphism from fa1 to fa2.

findIsomorphismOpt(fa1, fa2)

returns SOME of an isomorphism from fa1 to fa2, if fa1 and fa2 are isomorphic, and NONE, if fa1 and fa2 are not isomorphic.

findIsomorphism(fa1, fa2)

tries to find an isomorphism from fa1 to fa2. Issues an error message if such an isomorphism doesn't exist.

isomorphic(fa1, fa2)

tests whether fa1 and fa2 are isomorphic.

renameAlphabet(fa, rel)

renames the alphabet of fa using the bijection rel. Issues an error message if rel is not a bijection from a superset of the alphabet of fa to some set.

checkLP fa lp

checks whether lp is valid for fa, silently returning (), if it is, and explaining why it isn't, if it's not.

validLP fa lp

tests whether lp is valid for fa.

findLPOpt fa (qs, x, rs)

returns SOME of a minimal labeled path for fa, taking qs to rs with label x, if such a labeled path exists, and NONE, if such a labeled path does not exist.

findLP fa (qs, x, rs)

tries to find a minimal labeled path for fa, taking qs to rs with label x. Issues an error message if there is an element of qs or rs that isn't a state of fa, or such a labeled path doesn't exist.

findAcceptingLPOpt fa x

returns SOME of a minimal, accepting labeled path for fa and x, if such a labeled path exists, and NONE, if such a labeled path doesn't exist.

findAcceptingLP fa x

tries to find a minimal, accepting labeled path for fa and x. Issues an error message if such a labeled path doesn't exist.

emptyStr

is the canonical FA for the empty string.

emptySet

is the canonical FA for the empty set.

fromSym a

returns the canonical FA for a.

simplify fa

simplifies fa.

simplified fa

tests whether fa is simplified.

union(fa1, fa2)

returns the union of fa1 and fa2.

concat(fa1, fa2)

returns the concatentation of fa1 and fa2.

closure fa

returns the closure of fa.

genUnion

is defined by:

  fun genUnion nil         = emptySet
    | genUnion [fa]        = fa
    | genUnion (fa :: fas) = union(fa, genUnion fas)

genConcat

is defined by:

  fun genConcat nil         = emptyStr
    | genConcat [fa]        = fa
    | genConcat (fa :: fas) = concat(fa, genConcat fas)

rev fa

returns the reversal of fa.

fromStr x

returns the canonical FA for x.

fromReg reg

converts reg to an FA.

jforlanNew()

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

jforlanEdit fa

invokes JForlan, letting the user edit fa, and returning the resulting FA 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