Struct NFA 

pub struct NFA { /* private fields */ }

A nondeterministic finite automaton. The automaton consists of a collection of states, an initial state, and a set of final states.

Implementations

impl NFA

pub fn new() -> Self

Create a new, empty nondeterministic finite automaton.

pub fn new_state(&mut self) -> StateId

Add a new state to the automaton and return its index.

pub fn set_initial(&mut self, state: StateId) -> Result<(), StateNotFound>

Set the initial state of the automaton. The index must be a valid state index, otherwise an error is returned.

pub fn initial(&self) -> Option<StateId>

Returns the initial state of the automaton, if it exists.

pub fn add_final(&mut self, state: StateId) -> Result<(), StateNotFound>

Add a state to the set of final states. The index must be a valid state index, otherwise an error is returned.

pub fn finals(&self) -> impl Iterator<Item = StateId> + '_

Returns an iterator over the final states of the automaton.

pub fn is_final(&self, state: StateId) -> bool

Returns if a state is a final state. Invalid indices are not considered final states.

pub fn add_transition( &mut self, from: StateId, to: StateId, label: TransitionType, ) -> Result<(), StateNotFound>

Add a transition from one state to another. The indices must be valid state indices, otherwise an error is returned.

pub fn num_states(&self) -> usize

Returns the number of states in the automaton.

pub fn num_transitions(&self) -> usize

Returns the number of transitions in the automaton. This is the sum of the number of transitions of each state. Note that this require a linear scan over all states and transitions.

pub fn states(&self) -> impl Iterator<Item = StateId>

Returns an iterator over the states of the automaton.

pub fn transitions(&self) -> impl Iterator<Item = (StateId, &Vec<Transition>)>

Returns an iterator over the transitions of the automaton. The iterator yields pairs of a state and its outgoing transitions.

pub fn transitions_from( &self, state: StateId, ) -> Result<impl Iterator<Item = &Transition>, StateNotFound>

Returns an iterator over the transitions from a state. If the state is not a valid state index, an error is returned.

pub fn consume( &self, state: StateId, c: SmtChar, ) -> Result<HashSet<StateId>, StateNotFound>

Consumes an SmtChar from the given state. Returns all states reached when reading c in state state. If the set is empty, then the NFA cannot proceed from the given state by reading the given character.

Returns a StateNotFound error if the given state is not a state in the NFA.

pub fn predecessors(&self) -> HashMap<StateId, HashSet<StateId>>

Returns a map from states to the set of their predecessors. A state p has predecessor q if there is a transition from q to p.

pub fn is_det(&self) -> bool

Checks if the automaton is deterministic. An automaton is deterministic if all states are deterministic. A state is deterministic if it has at most one transition for each input character and no epsilon transitions. Checking for determinism is done in O(|V| + |E|) time, where |V| is the number of states and |E| is the number of transitions.

pub fn trim(&self) -> Self

Trims the automaton by removing unreachable and dead states. This ensures that all states are reachable from the initial state AND can reach a final state. Runs in O(V + E) time using two BFS traversals.

pub fn compress_ranges(&mut self)

Compresesses transitions from a state if they have the same destination but their ranges overlap or are adjacent. If there are two transitions from state q to state p with ranges r1 and r2 and the ranges can be merged into a single range r, then the transitions are replaced by a single transition from q to p with range r.

pub fn epsilon_closure( &self, state: StateId, ) -> Result<HashSet<StateId>, StateNotFound>

Returns the epsilon closure of a state. The epsilon closure of a state is the set of states that can be reached from the state by following epsilon transitions. If the state is not a valid state index, an error is returned.

pub fn eliminate_epsilon(self) -> Self

Performs the standard epsilon removal algorithm on the automaton. The result is a new automaton that accepts the same language as this automaton but has no epsilon transitions. If the automaton is already epsilon-free, this is a no-op. The resulting automaton is also trim as a side effect.

The algorithm works as follows: We do a breadth-first search starting from the initial state and compute the epsilon closure of each state. The epsilon closure of a state is the set of states that can be reached from the state by following epsilon transitions. We then add transitions for all non-epsilon transitions from the state to the destination states of the epsilon closure. If any state in the epsilon closure is a final state, we mark the new state as final.

The algorithm runs in O(|V| + |E|) time, where |V| is the number of states and |E| is the number of transitions.

pub fn longest_path(&self) -> Option<usize>

Returns the longest non-cyclic path in the automaton from the initial state to a final state, if it exists. The length of the path is the number of transitions in the path and, therefore, the number of characters in the longest word accepted by the automaton. Epsilon transitions are not counted in the path length. If the automaton is empty or contains a cycle on an accepting path, this returns None.

pub fn shortest_path(&self) -> Option<usize>

Returns the shortest path in the automaton from the initial state to a final state, if it exists. The length of the path is the number of transitions in the path and, therefore, the number of characters in the shortest word accepted by the automaton. Epsilon transitions are not counted in the path length. If the automaton is empty, this returns None.

pub fn lengths_from_initial(&self) -> HashMap<StateId, usize>

Compute the length of the shortest path from the initial state to any state. Returns a map from state indices to the length of the shortest path to that state. Epsilon transitions are not counted in the path length, i.e., an epsilon transition has length 0.

If a state is not reachable from the initial state, it is not included in the map. In particular, if the automaton has no final states, the map is empty.

pub fn lengths_to_final(&self) -> HashMap<StateId, usize>

Compute the length of the shortest path to a final state from any state. Returns a map from state indices to the length of the shortest path to a final state from that state. Epsilon transitions are not counted in the path length, i.e., an epsilon transition has length 0.

If a state cannot reach a final state, it is not included in the map. If the automaton has no final states, the map is empty.

pub fn reversed(&self) -> Self

Reverse the automaton. The resulting automaton

• has all transitions reversed,
• has a new initial state with and epsilon transition to every old final states,
• has all old initial states as final states.

The reversed automaton accepts the reverse of the language of the original automaton.

pub fn is_empty(&self) -> bool

Returns whether the automaton is empty. An automaton is empty if either

• it has no final states,
• it has no initial state, or
• there is no path from the initial state to a final state.

pub fn run(&self, word: &SmtString) -> HashSet<StateId>

Returns the set of states that can be reached from the initial state by consuming the given word.

pub fn accepts(&self, word: &SmtString) -> bool

Returns if the automaton accepts the given word. A word is accepted if there is a path from the initial state to a final state by consuming the word.

pub fn dot(&self) -> String

Returns the DOT representation of the automaton. The DOT representation can be used to visualize the automaton using Graphviz.

Trait Implementations

impl Clone for NFA

fn clone(&self) -> NFA

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for NFA

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for NFA

fn default() -> NFA

Returns the “default value” for a type.

impl Display for NFA

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<'a> GraphWalk<'a, usize, (usize, Transition, usize)> for NFA

fn nodes(&'a self) -> Nodes<'a, StateId>

Returns all the nodes in this graph.

fn edges(&'a self) -> Edges<'a, (StateId, Transition, StateId)>

Returns all of the edges in this graph.

fn source(&'a self, edge: &(StateId, Transition, StateId)) -> StateId

The source node for edge.

fn target(&'a self, edge: &(StateId, Transition, StateId)) -> StateId

The target node for edge.

impl<'a> Labeller<'a, usize, (usize, Transition, usize)> for NFA

fn graph_id(&'a self) -> Id<'a>

Must return a DOT compatible identifier naming the graph.

fn node_id(&'a self, n: &StateId) -> Id<'a>

Maps n to a unique identifier with respect to self. The implementer is responsible for ensuring that the returned name is a valid DOT identifier.

fn node_shape(&'a self, node: &StateId) -> Option<LabelText<'a>>

Maps n to one of the graphviz shape names. If None is returned, no shape attribute is specified.

fn node_label(&'a self, n: &StateId) -> LabelText<'a>

Maps n to a label that will be used in the rendered output. The label need not be unique, and may be the empty string; the default is just the output from node_id.

fn edge_label(&'a self, e: &(StateId, Transition, StateId)) -> LabelText<'a>

Maps e to a label that will be used in the rendered output. The label need not be unique, and may be the empty string; the default is in fact the empty string.

fn node_style(&'a self, _n: &StateId) -> Style

Maps n to a style that will be used in the rendered output.

fn node_color(&'a self, _node: &StateId) -> Option<LabelText<'a>>

Maps n to one of the graphviz color names. If None is returned, no color attribute is specified.

fn kind(&self) -> Kind

The kind of graph, defaults to Kind::Digraph.

fn edge_end_arrow(&'a self, _e: &E) -> Arrow

Maps e to arrow style that will be used on the end of an edge. Defaults to default arrow style.

fn edge_start_arrow(&'a self, _e: &E) -> Arrow

Maps e to arrow style that will be used on the end of an edge. Defaults to default arrow style.

fn edge_style(&'a self, _e: &E) -> Style

Maps e to a style that will be used in the rendered output.

fn edge_color(&'a self, _e: &E) -> Option<LabelText<'a>>

Maps e to one of the graphviz color names. If None is returned, no color attribute is specified.