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: 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
is a low-level function used by JForlan. See the code for more information.


[ Top | Parent | Root | Contents | Index ]

Forlan Version 4.15
Copyright © 2022 Alley Stoughton