Minimize.Minimize
The functor application Minimize(Label)(A)
applies a partition refinement algorithm to minimize the deterministic finite automaton A
. The time complexity of this operation is O(n + m.log m), where n is the number of states of the automaton A
and m is the number of its transitions. This bound is independent of the size of the alphabet of the transition labels.
module Label : sig ... end
module A : sig ... end
A description of the minimized automaton A'
.
A state of the original automaton A
is retained only if it is accessible and co-accessible, that is, only if this state lies on a path from some initial state to some final state.
The states that are retained are then grouped into equivalence classes; these equivalence classes form the states of the minimal automaton A'
.
The equivalence classes are made as coarse as possible (that is, as large as possible), while obeying the following constraints:
A.finals
. That is, if two states are deemed equivalent, then they must be both final or both non-final.A.groups
must similarly be respected.l
, the equivalence classes must be compatible with the transitions that carry the label l
. That is, if two states s1
and s2
are deemed equivalent, and if the state s1
has a transition labeled l
towards some state s'1
, then the state s2
must have a transition labeled l
towards some state s'2
such that s'1
and s'2
are also deemed equivalent.include DFA with type label = Label.t
The type states
is a type-level representation of the number of states of the automaton. Thus, a state number has type states index
. See Indexing
for more information about type-level indices.
val states : states Indexing.cardinal
states
is the number of states of the automaton.
type state = states Indexing.index
A state number is an integer in the range [0, cardinal states)
.
The type transitions
is a type-level representation of the number of transitions of the automaton. Thus, a transition number has type transitions index
. See Indexing
for more information about type-level indices.
val transitions : transitions Indexing.cardinal
transitions
is the number of transitions of the automaton.
type transition = transitions Indexing.index
A transition number is an integer in the range [0, cardinal transitions)
.
type label = Label.t
label
is the type of transition labels.
val label : transition -> label
label t
returns the label of the transition t
.
val source : transition -> state
source t
returns the source state of the transition t
.
val target : transition -> state
target t
returns the target state of the transition t
.
The function transport_state
maps a state of the original automaton A
to the corresponding state of the minimal automaton A'
. It is a partial function: transport_state s
is Some _
if and only if the state s
lies on a path from some initial state to some final state.
val transport_transition : A.transition -> transition option
The function transport_transition
maps a transition of the original automaton A
to the corresponding transition of the minimal automaton A'
. It is a partial function: transport_transition t
is Some _
if and only if the transition t
lies on a path from some initial state to some final state.
The function backport_state_one
maps a state s'
of the minimal automaton A'
to a state s
of the original automaton A
such that transport_state s = Some s'
holds. There may exist several states s
such that this equation holds. A representative state in each equivalence class is chosen, and backport_state_one
always returns a representative state.
The function backport_state_all
maps a state s'
of the minimal automaton A'
to an enumeration of all states s
of the original automaton A
such that transport_state s = Some s'
holds. There exists at least one such state: this enumeration is never empty.
val backport_transition : transition -> A.transition
The function backport_transition
maps a transition t'
of the minimal automaton A'
to a transition t
of the original automaton A
such that transport_transition t = Some t'
holds. There may exist several transitions t
such that this equation holds; backport_transition
returns the transition whose source state is a representative state.