EFA
Module
signature EFA
structure EFA
:> EFA
This module defines the abstract type of empty-string finite automata (EFAs).
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
type efa
injToFA efa
efa
to have type FA.fa
.
valid fa
fa
is an EFA.
projFromFA fa
fa
to have type efa
. Issues an error message if fa
is not an EFA.
fromString s
input fil
fil
.
toPP fa
efa
. (Inherited from FA
.)
toString efa
efa
to a string. (Inherited from FA
.)
output(fil, efa)
efa
to the file fil
. (Inherited from FA
.)
states efa
efa
. (Inherited from FA
.)
startState efa
efa
. (Inherited from FA
.)
acceptingStates efa
efa
. (Inherited from FA
.)
transitions efa
efa
. (Inherited from FA
.)
compare(efa1, efa2)
efa1
and efa2
in the total ordering on FAs. (Inherited from FA
.)
equal(efa1, efa2)
efa1
and efa2
are equal. (Inherited from FA
.)
numStates efa
efa
. (Inherited from FA
.)
numTransitions efa
efa
. (Inherited from FA
.)
alphabet efa
efa
. (Inherited from FA
.)
sub(efa1, efa2)
efa1
is a sub-EFA of efa2
. (Inherited from FA
.)
transitionFun efa (q, x)
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)
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)
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
x
is accepted by efa
. (Inherited from FA
.)
emptyClose efa qs
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
qs
for efa
. Issues an error message if qs
has an element that's not a state of efa
. (Inherited from FA
.)
reachableStates efa
efa
.
liveStates efa
efa
.
deadStates efa
efa
.
renameStates(efa, rel)
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
efa
. (Inherited from FA
.)
isomorphism(efa1, efa2, rel)
rel
is an isomorphism from efa1
to efa2
. (Inherited from FA
.)
findIsomorphismOpt(efa1, efa2)
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)
efa1
to efa2
. Issues an error message if such an isomorphism doesn't exist. (Inherited from FA
.)
isomorphic(efa1, efa2)
efa1
and efa2
are isomorphic. (Inherited from FA
.)
renameAlphabet(efa, rel)
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
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
lp
is valid for efa
. (Inherited from FA
.)
findLPOpt efa (qs, x, rs)
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)
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
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
efa
and x
. Issues an error message if such a labeled path doesn't exist. (Inherited from FA
.)
emptyStr
FA
.)
emptySet
FA
.)
fromSym a
a
. (Inherited from FA
.)
simplify efa
efa
. (Inherited from FA
.)
simplified efa
efa
is simplified. (Inherited from FA
.)
union(efa1, efa2)
efa1
and efa2
. (Inherited from FA
.)
concat(efa1, efa2)
efa1
and efa2
. (Inherited from FA
.)
closure efa
efa
. (Inherited from FA
.)
genUnion
fun genUnion nil = emptySet | genUnion [efa] = efa | genUnion (efa :: efas) = union(efa, genUnion efas)
genConcat
fun genConcat nil = emptyStr | genConcat [efa] = efa | genConcat (efa :: efas) = concat(efa, genConcat efas)
rev efa
efa
. (Inherited from FA
.)
inter(efa1, efa2)
efa1
and efa2
.
genInter
fun genInter nil = (* issues an error message *) | genInter [efa] = efa | genInter (efa :: efas) = inter(inter, genInter efas)
prefix efa
efa
.
fromFA fa
fa
to an EFA.
Forlan Version 4.15
Copyright © 2022 Alley Stoughton