Forlan Manual


The EFA Module


Synopsis

signature EFA
structure EFA :> EFA

This module defines the abstract type of empty-string finite automata (EFAs).


Interface

type efa
val injToFA : efa -> FA.fa
val valid : FA.fa -> bool
val projFromFA : FA.fa -> efa
val fromString : string -> efa
val input : string -> efa
val toPP : efa -> PP.pp
val toString : efa -> string
val output : string * efa -> unit
val states : efa -> Sym.sym Set.set
val startState : efa -> Sym.sym
val acceptingStates : efa -> Sym.sym Set.set
val transitions : efa -> Tran.tran Set.set
val compare : efa Sort.total_ordering
val equal : efa * efa -> bool
val numStates : efa -> int
val numTransitions : efa -> int
val alphabet : efa -> Sym.sym Set.set
val sub : efa * efa -> bool
val transitionFun : efa -> Sym.sym * Str.str -> Sym.sym Set.set
val transitionFunBackwards : efa -> Sym.sym * Str.str -> Sym.sym Set.set
val processStr : efa -> Sym.sym Set.set * Str.str -> Sym.sym Set.set
val accepted : efa -> Str.str -> bool
val emptyClose : efa -> Sym.sym Set.set -> Sym.sym Set.set
val emptyCloseBackwards : efa -> Sym.sym Set.set -> Sym.sym Set.set
val reachableStates : efa -> Sym.sym Set.set
val liveStates : efa -> Sym.sym Set.set
val deadStates : efa -> Sym.sym Set.set
val renameStates : efa * SymRel.sym_rel -> efa
val renameStatesCanonically : efa -> efa
val isomorphism : efa * efa * SymRel.sym_rel -> bool
val findIsomorphismOpt : efa * efa -> SymRel.sym_rel option
val findIsomorphism : efa * efa -> SymRel.sym_rel
val isomorphic : efa * efa -> bool
val renameAlphabet : efa * SymRel.sym_rel -> efa
val checkLP : efa -> LP.lp -> unit
val validLP : efa -> LP.lp -> bool
val findLPOpt : efa -> Sym.sym Set.set * Str.str * Sym.sym Set.set -> LP.lp option
val findLP : efa -> Sym.sym Set.set * Str.str * Sym.sym Set.set -> LP.lp
val findAcceptingLPOpt : efa -> Str.str -> LP.lp option
val findAcceptingLP : efa -> Str.str -> LP.lp
val emptyStr : efa
val emptySet : efa
val fromSym : Sym.sym -> efa
val simplify : efa -> efa
val simplified : efa -> bool
val union : efa * efa -> efa
val concat : efa * efa -> efa
val closure : efa -> efa
val genUnion : efa list -> efa
val genConcat : efa list -> efa
val rev : efa -> efa
val inter : efa * efa -> efa
val genInter : efa list -> efa
val prefix : efa -> efa
val fromFA : FA.fa -> efa

Description

type efa
The abstract type of EFAs, which is a proper subset of the set of FAs.

injToFA efa
inject efa to have type FA.fa.

valid fa
tests whether fa is an EFA.

projFromFA fa
projects fa to have type efa. Issues an error message if fa is not an EFA.

fromString s
inputs an EFA from a string.

input fil
inputs an EFA from the file named fil.

toPP fa
returns a pretty-printing expression for efa. (Inherited from FA.)

toString efa
pretty-prints efa to a string. (Inherited from FA.)

output(fil, efa)
pretty-prints efa to the file fil. (Inherited from FA.)

states efa
returns the states of efa. (Inherited from FA.)

startState efa
returns the start state of efa. (Inherited from FA.)

acceptingStates efa
returns the accepting states of efa. (Inherited from FA.)

transitions efa
returns the transitions of efa. (Inherited from FA.)

compare(efa1, efa2)
compares efa1 and efa2 in the total ordering on FAs. (Inherited from FA.)

equal(efa1, efa2)
tests whether efa1 and efa2 are equal. (Inherited from FA.)

numStates efa
returns the number of states of efa. (Inherited from FA.)

numTransitions efa
returns the number of transitions of efa. (Inherited from FA.)

alphabet efa
returns the alphabet of efa. (Inherited from FA.)

sub(efa1, efa2)
tests whether efa1 is a sub-EFA of efa2. (Inherited from FA.)

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

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

processStr efa (qs, x)
processes x from qs in efa. Issues an error message if qs has an element that's not a state of efa. (Inherited from FA.)

accepted efa x
tests whether x is accepted by efa. (Inherited from FA.)

emptyClose efa qs
returns the empty-closure of qs for efa. Issues an error message if qs has an element that's not a state of efa. (Inherited from FA.)

emptyCloseBackwards efa qs
returns the backwards empty-closure of qs for efa. Issues an error message if qs has an element that's not a state of efa. (Inherited from FA.)

reachableStates efa
returns the set of all reachable states of efa.

liveStates efa
returns the set of all live states of efa.

deadStates efa
returns the set of all dead states of efa.

renameStates(efa, rel)
renames the states of efa using the bijection rel. Issues an error message if rel is not a bijection from the states of efa to some set. (Inherited from FA.)

renameStatesCanonically efa
canonically renames the states of efa. (Inherited from FA.)

isomorphism(efa1, efa2, rel)
tests whether rel is an isomorphism from efa1 to efa2. (Inherited from FA.)

findIsomorphismOpt(efa1, efa2)
returns SOME of an isomorphism from efa1 to efa2, if efa1 and efa2 are isomorphic, and NONE, if efa1 and efa2 are not isomorphic.

findIsomorphism(efa1, efa2)
tries to find an isomorphism from efa1 to efa2. Issues an error message if such an isomorphism doesn't exist. (Inherited from FA.)

isomorphic(efa1, efa2)
tests whether efa1 and efa2 are isomorphic. (Inherited from FA.)

renameAlphabet(efa, rel)
renames the alphabet of efa using the bijection rel. Issues an error message if rel is not a bijection from a superset of the alphabet of efa to some set. (Inherited from FA.)

checkLP efa lp
checks whether lp is valid for efa, silently returning (), if it is, and explaining why it isn't, if it's not. (Inherited from FA.)

validLP efa lp
tests whether lp is valid for efa. (Inherited from FA.)

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

findLP efa (qs, x, rs)
tries to find a minimal labeled path for efa, 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 efa, or such a labeled path doesn't exist. (Inherited from FA.)

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

findAcceptingLP efa x
tries to find a minimal, accepting labeled path for efa and x. Issues an error message if such a labeled path doesn't exist. (Inherited from FA.)

emptyStr
is the canonical EFA for the empty string. (Inherited from FA.)

emptySet
is the canonical EFA for the empty set. (Inherited from FA.)

fromSym a
returns the canonical EFA for a. (Inherited from FA.)

simplify efa
simplifies efa. (Inherited from FA.)

simplified efa
tests whether efa is simplified. (Inherited from FA.)

union(efa1, efa2)
returns the union of efa1 and efa2. (Inherited from FA.)

concat(efa1, efa2)
returns the concatentation of efa1 and efa2. (Inherited from FA.)

closure efa
returns the closure of efa. (Inherited from FA.)

genUnion
is defined by:
  fun genUnion nil           = emptySet
    | genUnion [efa]         = efa
    | genUnion (efa :: efas) = union(efa, genUnion efas)


genConcat
is defined by:
  fun genConcat nil           = emptyStr
    | genConcat [efa]         = efa
    | genConcat (efa :: efas) = concat(efa, genConcat efas)


rev efa
returns the reversal of efa. (Inherited from FA.)

inter(efa1, efa2)
returns the intersection of efa1 and efa2.

genInter
is defined by:
  fun genInter nil           = (* issues an error message *)
    | genInter [efa]         = efa
    | genInter (efa :: efas) = inter(inter, genInter efas)


prefix efa
returns the prefix-closure of efa.

fromFA fa
converts fa to an EFA.


[ Top | Parent | Root | Contents | Index ]

Forlan Version 4.15
Copyright © 2022 Alley Stoughton