Module aws_smt_strings::automata
source · [−]Expand description
Deterministic finite-state automata
States are indexed by an integer from 0 to N-1 where N is the number of states.
The alphabet is divided in equivalence classes such that all characters in an equivalence class have the same transitions.
More precisely, a character partition is attached to every state of an automaton.
The partition consists of disjoint character intervals (see character_sets).
If the i-th interval in the partition of state s is interval [ai, bi] then all
character in this interval have the same successors delta(s, i).
In addition, state s may have a default successor, that is, the successor state of s for characters
that do not belong to any interval [ai, bi].
Function combined_char_partition constructs a
partition of the alphabet that is valid for all states of an automaton. If
two characters c1 and c2 are in the same class in the combined partition, then we
have delta(s, c1) = delta(s, c2) for any state s of the automaton.
Function pick_alphabet returns a vector of representative characters (i.e., one element in each class of the combined partition).