automaton.determinize(lazy=False)
Compute the (accessible part of the) determinization of an automaton. When lazy
, determinize on-demand (e.g., only states traversed by an evaluation).
Preconditions:
its labelset is free
its weightset features a division operator (which is the case for ).
Postconditions:
the result is deterministic
the result is equivalent to the input automaton
the result is accessible
the result need not be complete
Caveats:
might not terminate if the weightset is not (see automaton.has_twins_property)
See also:
Examples
Ladybird
Ladybird is a well known example that shows the exponential growth on the number of resulting states.
The resulting automaton has states labeled with subsets of the input automaton set of states. This decoration, like all the others, can be stripped (see automaton.strip):
Empty input
If the input automaton has an empty accessible part (i.e., it has no initial state), then the output is empty (which is genuinely displayed as nothing below).
Weighted automata
The algorithm we use requires a division operator. The following example has weights in (and was chosen because the algorithm terminates on it).
Which is obviously deterministic. Of course they are equivalent:
The next example works in , which features a division: the usual subtraction.
They are equivalent, but we cannot use automaton.is_equivalent here.
Caveats and Lazy Determinization
Some weighted automata cannot be determinized (into a finite automaton). See automaton.has_twins_property for a possible means to detect whether the procedure will terminate.
The following automaton, for example, admits no equivalent deterministic automaton.
You may however use the lazy determinization in this case.
To force the full evaluation of a lazy determinization, use automaton.accessible.