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 ... endmodule A : sig ... endA 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.tThe 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.cardinalstates is the number of states of the automaton.
type state = states Indexing.indexA 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.cardinaltransitions is the number of transitions of the automaton.
type transition = transitions Indexing.indexA transition number is an integer in the range [0, cardinal transitions).
type label = Label.tlabel is the type of transition labels.
val label : transition -> labellabel t returns the label of the transition t.
val source : transition -> statesource t returns the source state of the transition t.
val target : transition -> statetarget 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 optionThe 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.transitionThe 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.