Forlan Manual

The DFA Module

Synopsis

signature DFA
structure DFA :> DFA


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

Interface

type dfa
val injToFA : dfa -> FA.fa
val injToEFA : dfa -> EFA.efa
val injToNFA : dfa -> NFA.nfa
val valid : FA.fa -> bool
val projFromFA : FA.fa -> dfa
val projFromEFA : EFA.efa -> dfa
val projFromNFA : NFA.nfa -> dfa
val fromString : string -> dfa
val input : string -> dfa
val toPP : dfa -> PP.pp
val toString : dfa -> string
val output : string * dfa -> unit
val states : dfa -> Sym.sym Set.set
val startState : dfa -> Sym.sym
val acceptingStates : dfa -> Sym.sym Set.set
val transitions : dfa -> Tran.tran Set.set
val compare : dfa Sort.total_ordering
val equal : dfa * dfa -> bool
val numStates : dfa -> int
val numTransitions : dfa -> int
val alphabet : dfa -> Sym.sym Set.set
val sub : dfa * dfa -> bool
val transitionFun : dfa -> Sym.sym * Str.str -> Sym.sym Set.set
val transitionFunBackwards : dfa -> Sym.sym * Str.str -> Sym.sym Set.set
val processStr : dfa -> Sym.sym Set.set * Str.str -> Sym.sym Set.set
val accepted : dfa -> Str.str -> bool
val reachableStates : dfa -> Sym.sym Set.set
val liveStates : dfa -> Sym.sym Set.set
val deadStates : dfa -> Sym.sym Set.set
val renameStates : dfa * SymRel.sym_rel -> dfa
val renameStatesCanonically : dfa -> dfa
val isomorphism : dfa * dfa * SymRel.sym_rel -> bool
val findIsomorphismOpt : dfa * dfa -> SymRel.sym_rel option
val findIsomorphism : dfa * dfa -> SymRel.sym_rel
val isomorphic : dfa * dfa -> bool
val renameAlphabet : dfa * SymRel.sym_rel -> dfa
val checkLP : dfa -> LP.lp -> unit
val validLP : dfa -> LP.lp -> bool
val findLPOpt : dfa -> Sym.sym Set.set * Str.str * Sym.sym Set.set -> LP.lp option
val findLP : dfa -> Sym.sym Set.set * Str.str * Sym.sym Set.set -> LP.lp
val findAcceptingLPOpt : dfa -> Str.str -> LP.lp option
val findAcceptingLP : dfa -> Str.str -> LP.lp
val emptyStr : dfa
val emptySet : dfa
val inter : dfa * dfa -> dfa
val genInter : dfa list -> dfa
val determTransitionFun : dfa -> Sym.sym * Sym.sym -> Sym.sym
val determProcessStr : dfa -> Sym.sym * Str.str -> Sym.sym
val determAccepted : dfa -> Str.str -> bool
val fromNFA : NFA.nfa -> dfa
val determSimplified : dfa -> bool
val determSimplify : dfa * Sym.sym Set.set -> dfa
val minimize : dfa -> dfa
val complement : dfa * Sym.sym Set.set -> dfa
val minus : dfa * dfa -> dfa
datatype relationship
  = Equal
  | ProperSub of Str.str
  | ProperSup of Str.str
  | Incomp of Str.str * Str.str
val relation : dfa * dfa -> relationship
val relationship : dfa * dfa -> unit
val subset : dfa * dfa -> bool
val equivalent : dfa * dfa -> bool

Description

type dfa

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

injToFA dfa

inject dfa to have type FA.fa.

injToEFA df

inject dfa to have type EFA.efa.

injToNFA dfa

inject dfa to have type NFA.nfa.

valid fa

tests whether fa is a DFA.

projFromFA fa

projects fa to have type dfa. Issues an error message if fa is not a DFA.

projFromEFA efa

projects efa to have type dfa. Issues an error message if efa is not a DFA.

projFromNFA nfa

projects nfa to have type nfa. Issues an error message if nfa is not a DFA.

fromString s

inputs a DFA from s.

input fil

inputs a DFA from the file named fil.

toPP fa

returns a pretty-printing expression for dfa. (Inherited from FA.)

toString dfa

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

output(fil, dfa)

pretty-prints dfa to the file fil. (Inherited from FA.)

states dfa

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

startState dfa

returns the start state of dfa. (Inherited from FA.)

acceptingStates dfa

returns the accepting states of dfa. (Inherited from FA.)

transitions dfa

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

compare(dfa1, dfa2)

compares dfa1 and dfa2 in the total ordering on FAs. (Inherited from FA.)

equal(dfa1, dfa2)

tests whether dfa1 and dfa2 are equal. (Inherited from FA.)

numStates dfa

returns the number of states of dfa. (Inherited from FA.)

numTransitions dfa

returns the number of transitions of dfa. (Inherited from FA.)

alphabet dfa

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

sub(dfa1, dfa2)

tests whether dfa1 is a sub-DFA of dfa2. (Inherited from FA.)

transitionFun dfa (q, x)

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

transitionFunBackwards dfa (r, x)

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

processStr dfa (qs, x)

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

accepted dfa x

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

reachableStates dfa

returns the set of all reachable states of dfa.

liveStates dfa

returns the set of all live states of dfa.

deadStates dfa

returns the set of all dead states of dfa.

renameStates(dfa, rel)

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

renameStatesCanonically dfa

canonically renames the states of dfa. (Inherited from FA.)

isomorphism(dfa1, dfa2, rel)

tests whether rel is an isomorphism from dfa1 to dfa2. (Inherited from FA.)

findIsomorphismOpt(dfa1, dfa2)

returns SOME of an isomorphism from dfa1 to dfa2, if dfa1 and dfa2 are isomorphic, and NONE, if dfa1 and dfa2 are not isomorphic.

findIsomorphism(dfa1, dfa2)

tries to find an isomorphism from dfa1 to dfa2. Issues an error message if such an isomorphism doesn't exist. (Inherited from FA.)

isomorphic(dfa1, dfa2)

tests whether dfa1 and dfa2 are isomorphic. (Inherited from FA.)

renameAlphabet(dfa, rel)

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

checkLP dfa lp

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

validLP dfa lp

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

findLPOpt dfa (qs, x, rs)

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

findLP dfa (qs, x, rs)

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

findAcceptingLPOpt dfa x

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

findAcceptingLP dfa x

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

emptyStr

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

emptySet

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

inter(dfa1, dfa2)

returns the intersection of dfa1 and dfa2. (Inherited from EFA.)

genInter

is defined by:

  fun genInter nil           = (* issues an error message *)
    | genInter [dfa]         = dfa
    | genInter (dfa :: dfas) = inter(inter, genInter dfas)

determTransitionFun dfa (q, a)

returns the unique state r such that (q, [a], r) is a transition of dfa. Issues an error message if q is not a state of dfa, or a is not a member of the alphabet of dfa.

determProcessStr dfa (q, x)

uses determTransitionFun to deterministically process x from q in dfa, returning the resulting state. Issues an error message if q is not a state of dfa, or there is a symbol of x that is not in the alphabet of dfa.

determAccepted dfa x

uses determProcessStr to test whether x is accepted by dfa.

fromNFA nfa

converts nfa to a DFA.

determSimplified dfa

tests whether dfa is deterministically simplified.

determSimplify(dfa, bs)

deterministically simplifies dfa, with reference to bs.

minimize dfa

minimizes dfa.

complement(dfa, bs)

returns the complement of dfa, with reference to bs.

minus(dfa1, dfa2)

returns the difference of dfa1 and dfa2.

datatype relationship
  = Equal
  | ProperSub of Str.str
  | ProperSup of Str.str
  | Incomp of Str.str * Str.str

Datatype used by relation function.

relation(dfa1, dfa2)

determines the relationship between the language accepted by dfa1 and the language accepted by dfa2:

• Equal means that the languages are equal;
• ProperSub x means that the first language is a proper subset of the second, x is in the second language but not the first, and there is no shorter element of the second language that's not in the first one;
• ProperSup x means that the first language is a proper superset of the second, x is in the first language but not the second, and there is no shorter element of the first language that's not in the second one;
• Incomp(x, y) means that the two languages are incomparable, i.e., neither is a subset of the other, x is in the first language but not the second, there is no shorter element of the first language that's not in the second one, y is in the second language but not the first, and there is no shorter element of the second language that's not in the first one.

relationship(dfa1, dfa2)

explains the significance of the result of evaluating relation(dfa1, dfa2).

subset(dfa1, dfa2)

uses relation to test whether the language accepted by dfa1 is a subset of the language accepted by dfa2.

equivalent(dfa1, dfa2)

uses relation to test whether dfa1 and dfa2 are equivalent.

Forlan Version 4.15
Copyright © 2022 Alley Stoughton