Class mata::nft::Nft

class Nft : public Nfa

A class representing an NFT.

Public Functions

inline explicit Nft(Delta delta = {}, utils::SparseSet<State> initial_states = {}, utils::SparseSet<State> final_states = {}, Levels levels = {}, Alphabet *alphabet = nullptr)

Key value store for additional attributes for the NFT. Keys are attribute names as strings and the value types are up to the user. For example, we can set up attributes such as “state_dict” for state dictionary attribute mapping states to their respective names, or “transition_dict” for transition dictionary adding a human-readable meaning to each transition.

inline explicit Nft(const size_t num_of_states, utils::SparseSet<State> initial_states = {}, utils::SparseSet<State> final_states = {}, Levels levels = {}, Alphabet *alphabet = nullptr)

Construct a new explicit NFT with num_of_states states and optionally set initial and final states.

Parameters:

• num_of_states – [in] Number of states for which to preallocate Delta.

• initial_states – Initial states of the NFT.

• final_states – Final states of the NFT.

• levels – Levels of the states.

• alphabet – Alphabet of the NFT.

Nft(const Nft &other) = default

Construct a new explicit NFT from other NFT.

inline explicit Nft(const mata::nfa::Nfa &other, const size_t num_of_levels = 1, const Level default_level = DEFAULT_LEVEL)

Construct a new NFT with num_of_levels levels from NFA.

All states levels are set to the default_level. The transition function remains the same as in the NFA.

Note: Constructor functions with more options are available in mata::nft::builder.

Parameters:

• other – NFA to be converted to NFT.

• num_of_levels – Number of levels for the NFT. (default: 1)

• default_level – Default level for the states. (default: 0)

inline explicit Nft(Nfa &&other, const size_t num_of_levels = 1, const Level default_level = DEFAULT_LEVEL)

Construct a new NFT with num_of_levels levels from NFA.

All states levels are set to the default_level. The transition function remains the same as in the NFA.

Note: Constructor functions with more options are available in mata::nft::builder.

Parameters:

• other – NFA to be converted to NFT.

• num_of_levels – Number of levels for the NFT. (default: 1)

• default_level – Default level for the states. (default: 0)

inline explicit Nft(const Nfa &other, Levels levels)

Construct a new NFT with num_of_levels levels from NFA.

All states levels are set to the default_level. The transition function remains the same as in the NFA.

Note: Constructor functions with more options are available in mata::nft::builder.

Parameters:

• other – NFA to be converted to NFT.

• levels – Levels for the states of the NFA other.

inline explicit Nft(Nfa &&other, Levels levels)

Construct a new NFT with num_of_levels levels from NFA.

All states levels are set to the default_level. The transition function remains the same as in the NFA.

Note: Constructor functions with more options are available in mata::nft::builder.

Parameters:

• other – NFA to be converted to NFT.

• levels – Levels for the states of the NFA other.

State add_state()

Add a new (fresh) state to the automaton.

Returns:

The newly created state.

State add_state(State state)

Add state state to this if state is not in this yet.

Returns:

The requested state.

State add_state_with_level(Level level)

Add a new (fresh) state to the automaton with level level.

Returns:

The newly created state.

State add_state_with_level(State state, Level level)

Add state state to this with level level if state is not in this yet.

Returns:

The requested state.

size_t num_of_states_with_level(Level level) const

Get the number of states with level level.

Returns:

The number of states with level level.

State insert_word(State source, const Word &word, State target)

Inserts a word into the NFT from a source state source to a target state target.

Creates new states along the path of the word.

If the length of word is less than num_of_levels, then the last symbol of word will form a transition going directly from the last inner state to target.

Parameters:

• source – The source state where the word begins. source must already exist.

• word – The nonempty word to be inserted into the NFA.

• target – The target state where the word ends. target must already exist.

Returns:

The state target where the inserted word ends.

State insert_word(State source, const Word &word)

Inserts a word into the NFT from a source state source to a newly created target state, creating new states along the path of the word.

If the length of word is less than num_of_levels, then the last symbol of word will form a transition going directly from the last inner state to the newly created target.

Parameters:

• source – The source state where the word begins. source must already exist.

• word – The nonempty word to be inserted into the NFA.

Returns:

The newly created target where the inserted word ends.

State add_transition(State source, const std::vector<Symbol> &symbols, State target)

Add a single NFT transition.

The transition leads from a source state source to a target state target, creating new inner states for all tapes.

If the length of symbols is less than num_of_levels, then the last symbol of symbols will form a jump transition going directly from the last inner state to target.

Parameters:

• source – The source state where the NFT transition begins. source must already exist.

• symbols – The nonempty set of symbols, one for each tape to be inserted into the NFT.

• target – The target state where the NFT transition ends. target must already exist.

Returns:

The target state target.

State add_transition(State source, const std::vector<Symbol> &symbols)

Add a single NFT transition to the NFT from a source state source to a newly created target state, creating new inner states for all tapes.

If the length of symbols is less than num_of_levels, the last symbol of symbols will form a transition going directly from the last inner state to the newly created target.

Parameters:

• source – The source state where the transition begins. source must already exist.

• symbols – The nonempty set of symbols, one for each tape to be inserted into the NFT.

Returns:

The target state target.

State insert_word_by_parts(State source, const std::vector<Word> &word_parts_on_levels, State target)

Inserts a word, which is created by interleaving parts from word_parts_on_levels, into the NFT from a source state source to a target state target, creating new states along the path of word.

The length of the inserted word equals num_of_levels * the maximum word length in the vector word_parts_on_levels. At least one Word in word_parts_on_levels must be nonempty. The vector word_parts_on_levels must have a size equal to num_of_levels. Words shorter than the maximum word length are interpreted as words followed by a sequence of epsilons to match the maximum length.

Parameters:

• source – The source state where the word begins. source must already exist and be of a level 0.

• word_parts_on_levels – The vector of word parts, with each part corresponding to a different level.

• target – The target state where the word ends. target must already exist and be of a level 0.

Returns:

The state target where the inserted word_parts_on_levels ends.

State insert_word_by_parts(State source, const std::vector<Word> &word_parts_on_levels)

Inserts a word, which is created by interleaving parts from word_parts_on_levels, into the NFT from a source state source to a target state target, creating new states along the path of word.

The length of the inserted word equals num_of_levels * the maximum word length in the vector word_parts_on_levels. At least one Word in word_parts_on_levels must be nonempty. The vector word_parts_on_levels must have a size equal to num_of_levels. Words shorter than the maximum word length are interpreted as words followed by a sequence of epsilons to match the maximum length.

Parameters:

• source – The source state where the word begins. source must already exist be of a level 0.

• word_parts_on_levels – The vector of word parts, with each part corresponding to a different level.

Returns:

The newly created target where the inserted word_parts_on_levels ends.

Nft &insert_identity(State state, const std::vector<Symbol> &symbols, JumpMode jump_mode = JumpMode::RepeatSymbol)

Inserts identity transitions into the NFT.

Parameters:

• state – The state where the identity transition will be inserted. state server as both the source and target state.

• symbols – The vector of symbols used for the identity transition. Identity will be created for each symbol in the vector.

• jump_mode – Specifies if the symbol on a jump transition (a transition with a length greater than 1) is interpreted as a sequence repeating the same symbol or as a single instance of the symbol followed by a sequence of DONT_CARE symbols.

Returns:

Self with inserted identity.

Nft &insert_identity(State state, const Alphabet *alphabet, JumpMode jump_mode = JumpMode::RepeatSymbol)

Inserts identity transitions into the NFT.

Parameters:

• state – The state where the identity transition will be inserted. state server as both the source and target state.

• alpahbet – The alphabet with symbols used for the identity transition. Identity will be created for each symbol in the alphabet.

• jump_mode – Specifies if the symbol on a jump transition (a transition with a length greater than 1) is interpreted as a sequence repeating the same symbol or as a single instance of the symbol followed by a sequence of DONT_CARE symbols.

Returns:

Self with inserted identity.

Nft &insert_identity(State state, Symbol symbol, JumpMode jump_mode = JumpMode::RepeatSymbol)

Inserts an identity transition into the NFT.

Parameters:

• state – The state where the identity transition will be inserted. state server as both the source and target state.

• symbol – The symbol used for the identity transition.

• jump_mode – Specifies if the symbol on a jump transition (a transition with a length greater than 1) is interpreted as a sequence repeating the same symbol or as a single instance of the symbol followed by a sequence of DONT_CARE symbols.

Returns:

Self with inserted identity.

bool contains_jump_transitions() const

Checks if the transducer contains any jump transition.

void clear()

Clear the underlying NFT to a blank NFT.

The whole NFT is cleared, each member is set to its zero value.

bool is_identical(const Nft &aut) const

Check if this is exactly identical to aut.

This is exact equality of automata, including state numbering (so even stronger than isomorphism), essentially only useful for testing purposes.

Returns:

True if automata are exactly identical, false otherwise.

Nft &trim(StateRenaming *state_renaming = nullptr)

Remove inaccessible (unreachable) and not co-accessible (non-terminating) states in-place.

Remove states which are not accessible (unreachable; state is accessible when the state is the endpoint of a path starting from an initial state) or not co-accessible (non-terminating; state is co-accessible when the state is the starting point of a path ending in a final state).

Parameters:

state_renaming – [out] Mapping of trimmed states to new states.

Returns:

this after trimming.

void remove_epsilon(Symbol epsilon = EPSILON)

Remove simple epsilon transitions from the automaton.

See also

mata::nft::remove_epsilon()

Nft &concatenate(const Nft &aut)

In-place concatenation.

Nft &unite_nondet_with(const Nft &aut)

In-place union.

Nft get_one_letter_aut(const std::set<Level> &levels_to_keep = {}, Symbol abstract_symbol = 'x') const

Unify transitions to create a directed graph with at most a single transition between two states.

Get NFT where transitions of this are replaced with transitions over one symbol abstract_symbol

The transitions over EPSILON are not replaced, neither are the transitions coming from a state with a level from levels_to_keep.

Parameters:

• abstract_symbol – [in] Abstract symbol to use for transitions in digraph.

• levels_to_keep – [in] Transitions coming from states with any of these levels are not replaced.

• abstract_symbol – [in] The symbol to replace with.

Returns:

An automaton representing a directed graph.

Returns:

Nft

void get_one_letter_aut(Nft &result) const

Unify transitions to create a directed graph with at most a single transition between two states.

Parameters:

result – [out] An automaton representing a directed graph.

void unwind_jumps_inplace(const utils::OrdVector<Symbol> &dont_care_symbol_replacements = {DONT_CARE}, JumpMode jump_mode = JumpMode::RepeatSymbol)

Unwinds jump transitions in the transducer.

Parameters:

• dont_care_symbol_replacements – [in] Vector of symbols to replace DONT_CARE symbols with.

• jump_mode – [in] Specifies if the symbol on a jump transition (a transition with a length greater than 1) is interpreted as a sequence repeating the same symbol or as a single instance of the symbol followed by a sequence of DONT_CARE symbols.

Nft unwind_jumps(const utils::OrdVector<Symbol> &dont_care_symbol_replacements = {DONT_CARE}, JumpMode jump_mode = JumpMode::RepeatSymbol) const

Creates a transducer with unwinded jump transitions from the current one.

Parameters:

• dont_care_symbol_replacements – [in] Vector of symbols to replace DONT_CARE symbols with.

• jump_mode – [in] Specifies if the symbol on a jump transition (a transition with a length greater than 1) is interpreted as a sequence repeating the same symbol or as a single instance of the symbol followed by a sequence of DONT_CARE symbols.

void unwind_jumps(Nft &result, const utils::OrdVector<Symbol> &dont_care_symbol_replacements = {DONT_CARE}, JumpMode jump_mode = JumpMode::RepeatSymbol) const

Unwinds jump transitions in the given transducer.

Parameters:

• result – [out] A transducer with only one level.

• dont_care_symbol_replacements – [in] Vector of symbols to replace DONT_CARE symbols with.

• jump_mode – [in] Specifies if the symbol on a jump transition (a transition with a length greater than 1) is interpreted as a sequence repeating the same symbol or as a single instance of the symbol followed by a sequence of DONT_CARE symbols.

std::string print_to_dot(bool decode_ascii_chars = false, bool use_intervals = false, int max_label_length = -1) const

Prints the automaton in DOT format.

Parameters:

• decode_ascii_chars – [in] Whether to use ASCII characters for the output.

• use_intervals – [in] Whether to use intervals (e.g. [1-3] instead of 1,2,3) for labels.

• max_label_length – [in] Maximum label length for the output (-1 means no limit, 0 means no labels). If the label is longer than max_label_length, it will be truncated, with full label displayed on hover.

Returns:

automaton in DOT format

void print_to_dot(std::ostream &output, bool decode_ascii_chars = false, bool use_intervals = false, int max_label_length = -1) const

Prints the automaton to the output stream in DOT format.

Parameters:

• decode_ascii_chars – [in] Whether to use ASCII characters for the output.

• use_intervals – [in] Whether to use intervals (e.g. [1-3] instead of 1,2,3) for labels.

• max_label_length – [in] Maximum label length for the output (-1 means no limit, 0 means no labels). If the label is longer than max_label_length, it will be truncated, with full label displayed on hover.

void print_to_dot(const std::string &filename, bool decode_ascii_chars = false, bool use_intervals = false, int max_label_length = -1) const

Prints the automaton to the file in DOT format.

Parameters:

• filename – Name of the file to print the automaton to

• decode_ascii_chars – [in] Whether to use ASCII characters for the output.

• use_intervals – [in] Whether to use intervals (e.g. [1-3] instead of 1,2,3) for labels.

• max_label_length – [in] Maximum label length for the output (-1 means no limit, 0 means no labels). If the label is longer than max_label_length, it will be truncated, with full label displayed on hover.

std::string print_to_mata() const

Prints the automaton in mata format.

If you need to parse the automaton again, use IntAlphabet in construct()

Returns:

automaton in mata format TODO handle alphabet of the automaton, currently we print the exact value of the symbols

void print_to_mata(std::ostream &output) const

Prints the automaton to the output stream in mata format.

If you need to parse the automaton again, use IntAlphabet in construct()

TODO handle alphabet of the automaton, currently we print the exact value of the symbols

void print_to_mata(const std::string &filename) const

Prints the automaton to the file in mata format.

If you need to parse the automaton again, use IntAlphabet in construct()

TODO handle alphabet of the automaton, currently we print the exact value of the symbols

Parameters:

filename – Name of the file to print the automaton to

StateSet post(const StateSet &states, const Symbol symbol, EpsilonClosureOpt epsilon_closure_opt = EpsilonClosureOpt::NONE) const

Get the set of states reachable from the given set of states over the given symbol.

TODO: Relict from VATA. What to do with inclusion/ universality/ this post function? Revise all of them.

Parameters:

• states – Set of states to compute the post set from.

• symbol – Symbol to compute the post set for.

• epsilon_closure_opt – Epsilon closure option. Perform epsilon closure before and/or after the post operation.

Returns:

Set of states reachable from the given set of states over the given symbol.

inline StateSet post(const State state, const Symbol symbol, EpsilonClosureOpt epsilon_closure_opt) const

Get the set of states reachable from the given state over the given symbol.

Parameters:

• state – A state to compute the post set from.

• symbol – Symbol to compute the post set for.

• epsilon_closure_opt – Epsilon closure option. Perform epsilon closure before and/or after the post operation.

Returns:

Set of states reachable from the given state over the given symbol.

inline const StateSet &post(const State state, Symbol symbol) const

Returns a reference to targets (states) reachable from the given state over the given symbol.

This is an optimized shortcut for post(state, symbol, EpsilonClosureOpt::NONE).

Parameters:

• state – A state to compute the post set from.

• symbol – Symbol to compute the post set for.

Returns:

Set of states reachable from the given state over the given symbol.

bool is_universal(const Alphabet &alphabet, Run *cex = nullptr, const ParameterMap &params = {{"algorithm", "antichains"}}) const

Is the language of the automaton universal?

bool is_universal(const Alphabet &alphabet, const ParameterMap &params) const

Is the language of the automaton universal?

bool is_in_lang(const Run &word, bool use_epsilon = false, bool match_prefix = false) const

Check whether a run over the word (or its prefix) is in the language of an automaton.

Parameters:

• word – The run to check.

• use_epsilon – Whether the automaton uses epsilon transitions.

• match_prefix – Whether to also match the prefix of the word.

Returns:

True if the run (or its prefix) is in the language of the automaton, false otherwise.

inline bool is_in_lang(const Word &word, const bool use_epsilon = false, const bool match_prefix = false)

Check whether a word (or its prefix) is in the language of an automaton.

Parameters:

• word – The word to check.

• use_epsilon – Whether the automaton uses epsilon transitions.

• match_prefix – Whether to also match the prefix of the word.

Returns:

True if the word (or its prefix) is in the language of the automaton, false otherwise.

inline bool is_prefix_in_lang(const Run &word, const bool use_epsilon = false) const

Check whether a prefix of a run is in the language of an automaton.

Parameters:

• word – The run to check.

• use_epsilon – Whether the automaton uses epsilon transitions.

Returns:

True if the prefix of the run is in the language of the automaton, false otherwise.

inline bool is_prefix_in_lang(const Word &word, const bool use_epsilon = false) const

Check whether a prefix of a word is in the language of an automaton.

Parameters:

• word – The word to check.

• use_epsilon – Whether the automaton uses epsilon transitions.

Returns:

True if the prefix of the word is in the language of the automaton, false otherwise.

bool is_tuple_in_lang(const std::vector<Word> &track_words)

Checks whether track words are in the language of the transducer.

That is, the function checks whether a tuple track_words (word1, word2, word3, …, wordn) is in the regular relation accepted by the transducer with ‘n’ levels (tracks).

std::set<Word> get_words(size_t max_length = std::numeric_limits<size_t>::max()) const

Get the set of all words in the language of the automaton whose length is <= max_length.

If you have an automaton with finite language (can be checked using is_acyclic), you can get all words by calling aut.get_words(aut.num_of_states())

Parameters:

max_length – Maximum length of words to be returned. Default: “no limit”; will infinitely loop if the language is infinite.

Returns:

Set of all words in the language of the automaton whose length is <= max_length.

Nft apply(const nfa::Nfa &nfa, Level level_to_apply_on = 0, bool project_out_applied_level = true, JumpMode jump_mode = JumpMode::RepeatSymbol) const

Apply nfa to this.

Intersects nfa with level level_to_apply_on of this. For 2-level NFT, the default values returns the image of nfa, where you can use to_nfa_copy() or to_nfa_move() to get NFA representation of this language. If you need pre-image of nfa for 2-level NFT, set level_to_apply_on to 1.

Parameters:

• nfa – NFA to apply.

• level_to_apply_on – Which level to apply the nfa on.

• project_out_applied_level – Whether the level_to_apply_on is projected out from final NFT.

• jump_mode – [in] Specifies if the symbol on a jump transition (a transition with a length greater than 1) is interpreted as a sequence repeating the same symbol, or as a single instance of the symbol followed by a sequence of DONT_CARE symbols.

Returns:

Nft apply(const Word &word, Level level_to_apply_on = 0, bool project_out_applied_level = true, JumpMode jump_mode = JumpMode::RepeatSymbol) const

Apply word to this.

Intersects { word } with level level_to_apply_on of this. For 2-level NFT, the default values returns the image of word, where you can use to_nfa_copy() or to_nfa_move() to get NFA representation of this language. If you need pre-image of word for 2-level NFT, set level_to_apply_on to 1.

Parameters:

• word – Word to apply.

• level_to_apply_on – Which level to apply the nfa on.

• project_out_applied_level – Whether the level_to_apply_on is projected out from final NFT.

• jump_mode – [in] Specifies if the symbol on a jump transition (a transition with a length greater than 1) is interpreted as a sequence repeating the same symbol, or as a single instance of the symbol followed by a sequence of DONT_CARE symbols.

Returns:

inline Nfa to_nfa_copy() const

Copy NFT as NFA.

Transitions are not updated to only have one level.

Returns:

A newly created NFA with copied members from NFT.

inline Nfa to_nfa_move()

Move NFT as NFA.

The NFT can no longer be used. Transitions are not updated to only have one level.

Returns:

A newly created NFA with moved members from NFT.

Nfa to_nfa_update_copy(const utils::OrdVector<Symbol> &dont_care_symbol_replacements = {DONT_CARE}, JumpMode jump_mode = JumpMode::RepeatSymbol) const

Copy NFT as NFA updating the transitions to have one level only.

Parameters:

• dont_care_symbol_replacements – [in] Vector of symbols to replace DONT_CARE symbols with.

• jump_mode – [in] Specifies if the symbol on a jump transition (a transition with a length greater than 1) is interpreted as a sequence repeating the same symbol or as a single instance of the symbol followed by a sequence of DONT_CARE symbols.

Returns:

A newly created NFA with copied members from NFT with updated transitions.

Nfa to_nfa_update_move(const utils::OrdVector<Symbol> &dont_care_symbol_replacements = {DONT_CARE}, JumpMode jump_mode = JumpMode::RepeatSymbol)

Move NFT as NFA updating the transitions to have one level only.

The NFT can no longer be used.

Parameters:

• dont_care_symbol_replacements – [in] Vector of symbols to replace DONT_CARE symbols with.

• jump_mode – [in] Specifies if the symbol on a jump transition (a transition with a length greater than 1) is interpreted as a sequence repeating the same symbol or as a single instance of the symbol followed by a sequence of DONT_CARE symbols.

Returns:

A newly created NFA with moved members from NFT with updated transitions.

bool make_complete(const Alphabet *alphabet = nullptr, const utils::OrdVector<Symbol> &epsilons = {}, const std::optional<std::vector<State>> &sink_states = std::nullopt)

Make NFT complete in place.

For each state state, add transitions with “missing” symbols from alphabet (symbols that do not occur on transitions from given state) to sink_states[next_level(level)] where level == this->levels[state]. If NFT does not contain any states, this function does nothing.

Parameters:

• alphabet – [in] Alphabet to use for computing “missing” symbols. If nullptr, use this->alphabet when defined, otherwise use this->delta.get_used_symbols().

• epsilons – Epsilon symbols to include when computing “missing” symbols. Epsilon symbols are handled as normal alphabet symbols.

• sink_states – [in] The level-indexed vector of sink states, one per level, already existing in the NFT, into which new transitions are added. If std::nullopt, add new sink states.

Returns:

true if a new transition was added to the NFA, false otherwise.

bool make_complete(const utils::OrdVector<Symbol> &symbols, const utils::OrdVector<Symbol> &epsilons = {}, const std::optional<std::vector<State>> &sink_states = std::nullopt)

Make NFT complete in place.

For each state state, add transitions with “missing” symbols from alphabet (symbols that do not occur on transitions from given state) to sink_states[next_level(level)] where level == this->levels[state]. If NFT does not contain any states, this function does nothing.

Note

This overloaded version is a more efficient version which does not need to compute the set of symbols to complete to from the alphabet. Prefer this version when you already have the set of symbols precomputed or plan to complete multiple automata over the same set of symbols.

Parameters:

• symbols – [in] Symbols to compute “missing” symbols from.

• epsilons – Epsilon symbols to include when computing “missing” symbols. Epsilon symbols are handled as normal alphabet symbols.

• sink_states – [in] The level-indexed vector of sink states, one per level, already existing in the NFT, into which new transitions are added. If std::nullopt, add new sink states.

Returns:

true if a new transition was added to the NFA, false otherwise.

bool is_complete(Alphabet const *alphabet = nullptr) const

Test for automaton completeness with regard to an alphabet.

An automaton is complete if every reachable state has at least one outgoing transition over every symbol.

bool is_complete(const utils::OrdVector<Symbol> &symbols) const

Test for automaton completeness with regard to an alphabet.

An automaton is complete if every reachable state has at least one outgoing transition over every symbol.

bool is_deterministic() const

Test whether an automaton is deterministic.

I.e., whether it has exactly one initial state and every state has at most one outgoing transition over every symbol. Checks the whole automaton, not only the reachable part

size_t num_of_states() const

Get the current number of states in the whole automaton.

This includes the initial and final states as well as states in the transition relation.

Returns:

The number of states.

Nfa &unify_initial(bool force_new_state = false)

Unify initial states into a single new initial state.

Parameters:

force_new_state – [in] Whether to force creating a new state even when initial states are already unified.

Returns:

this after unification.

Nfa &unify_final(bool force_new_state = false)

Unify final states into a single new final state.

Parameters:

force_new_state – [in] Whether to force creating a new state even when final states are already unified.

Returns:

this after unification.

inline Nfa &swap_final_nonfinal()

Swap final and non-final states in-place.

bool is_identical(const Nfa &aut) const

Check if this is exactly identical to aut.

This is exact equality of automata, including state numbering (so even stronger than isomorphism), essentially only useful for testing purposes.

Returns:

True if automata are exactly identical, false otherwise.

StateSet get_reachable_states() const

Get set of reachable states.

Reachable states are states accessible from any initial state.

Returns:

Set of reachable states. TODO: with the new get_useful_states, it might be useless now.

StateSet get_terminating_states() const

Get set of terminating states.

Terminating states are states leading to any final state.

Returns:

Set of terminating states. TODO: with the new get_useful_states, it might be useless now.

BoolVector get_useful_states() const

Get the useful states using a modified Tarjan’s algorithm.

A state is useful if it is reachable from an initial state and can reach a final state.

Returns:

BoolVector Bool vector whose ith value is true iff the state i is useful.

void tarjan_scc_discover(const TarjanDiscoverCallback &callback) const

Tarjan’s SCC discover algorihm.

Parameters:

callback – Callbacks class to instantiate callbacks for the Tarjan’s algorithm.

Nfa decode_utf8() const

Decodes automaton from UTF-8 encoding.

Method removes unreachable states from delta.

Returns:

Decoded automaton.

std::vector<State> distances_from_initial() const

Returns vector ret where ret[q] is the length of the shortest path from any initial state to q.

std::vector<State> distances_to_final() const

Returns vector ret where ret[q] is the length of the shortest path from q to any final state.

Run get_shortest_accepting_run_from_state(State q, const std::vector<State> &distances_to_final) const

Get some shortest accepting run from state q.

Assumes that q is a state of this automaton and that there is some accepting run from q

Parameters:

distances_to_final – Vector of the lengths of the shortest runs from states (can be computed using distances_to_final())

Nfa &concatenate(const Nfa &aut)

In-place concatenation.

Nfa &unite_nondet_with(const Nfa &aut)

In-place nondeterministic union with aut.

Does not add epsilon transitions, just unites initial and final states.

Nfa get_one_letter_aut(Symbol abstract_symbol = 'x') const

Unify transitions to create a directed graph with at most a single transition between two states.

Parameters:

abstract_symbol – [in] Abstract symbol to use for transitions in digraph.

Returns:

An automaton representing a directed graph.

void get_one_letter_aut(Nfa &result) const

Unify transitions to create a directed graph with at most a single transition between two states.

Parameters:

result – [out] An automaton representing a directed graph.

inline bool is_epsilon(Symbol symbol) const

Check whether symbol is epsilon symbol or not.

Parameters:

symbol – Symbol to check.

Returns:

True if the passed symbol is epsilon, false otherwise.

std::string print_to_mata(const Alphabet *alphabet = nullptr) const

Prints the automaton in mata format.

If you need to parse the automaton again, use IntAlphabet in construct()

Parameters:

alphabet – [in] If specified, translates the symbols to their symbol names in the alphabet.

Returns:

automaton in mata format

void print_to_mata(std::ostream &output, const Alphabet *alphabet = nullptr) const

Prints the automaton to the output stream in mata format.

If you need to parse the automaton again, use IntAlphabet in construct()

Parameters:

alphabet – [in] If specified, translates the symbols to their symbol names in the alphabet.

void print_to_mata(const std::string &filename, const Alphabet *alphabet = nullptr) const

Prints the automaton to the file in mata format.

If you need to parse the automaton again, use IntAlphabet in construct()

Parameters:

• alphabet – [in] If specified, translates the symbols to their symbol names in the alphabet.

• filename – Name of the file to print the automaton to

bool is_lang_empty(Run *cex = nullptr) const

Check whether the language of NFA is empty.

Currently calls is_lang_empty_scc if cex is null

Parameters:

cex – [out] Counter-example path for a case the language is not empty.

Returns:

True if the language is empty, false otherwise.

bool is_lang_empty_scc() const

Check if the language is empty using Tarjan’s SCC discover algorithm.

Returns:

Language empty <-> True

bool is_acyclic() const

Is the automaton graph acyclic?

Used for checking language finiteness.

Returns:

true <-> Automaton graph is acyclic.

bool is_flat() const

Is the automaton flat?

Flat automaton is an NFA whose every SCC is a simple loop. Basically each state in an SCC has at most one successor within this SCC.

Returns:

true <-> Automaton graph is flat.

void fill_alphabet(mata::OnTheFlyAlphabet &alphabet_to_fill) const

Fill alphabet_to_fill with symbols from nfa.

Parameters:

• nfa – [in] NFA with symbols to fill alphabet_to_fill with.

• alphabet_to_fill – [out] Alphabet to be filled with symbols from nfa.

StateSet read_word(const Run &word, const bool use_epsilon = false) const

Read a word and return the set of states the automaton ends up in.

Parameters:

• word – The word to read.

• use_epsilon – Whether the automaton uses epsilon transitions.

Returns:

Set of all reachable states after reading the word. Note: This returns all reachable states, not just final states. Use is_in_lang() if you need to check language membership, or intersect the result with final states manually if needed. Note: The returned set is empty if the word cannot be read.

inline StateSet read_word(const Word &word, const bool use_epsilon = false) const

Read a word and return the set of states the automaton ends up in.

Parameters:

• word – The word to read.

• use_epsilon – Whether the automaton uses epsilon transitions.

Returns:

Set of all reachable states after reading the word. Note: This returns all reachable states, not just final states. Use is_in_lang() if you need to check language membership, or intersect the result with final states manually if needed. Note: The returned set is empty if the word cannot be read.

std::optional<State> read_word_det(const Run &word) const

Read a word and return the state the deterministic automaton ends up in.

If the automaton is nondeterministic, the result is undefined.

Parameters:

word – The word to read.

Returns:

The reachable state after reading the word or std::nullopt if the word cannot be read.

inline std::optional<State> read_word_det(const Word &word) const

Read a word and return the state the deterministic automaton ends up in.

If the automaton is nondeterministic, the result is undefined.

Parameters:

word – The word to read.

Returns:

The reachable state after reading the word or std::nullopt if the word cannot be read.

std::optional<Word> get_word(const std::optional<Symbol> first_epsilon = EPSILON) const

Get any arbitrary accepted word in the language of the automaton.

The automaton is searched using DFS, returning a word for the first reached final state.

Parameters:

first_epsilon – If defined, all symbols >=first_epsilon are assumed to be epsilon and therefore are not in the returned word.

Returns:

std::optional<Word> Some word from the language. If the language is empty, returns std::nullopt.

std::optional<Word> get_word_from_complement(const Alphabet *alphabet = nullptr) const

Get any arbitrary accepted word in the language of the complement of the automaton.

The automaton is lazily determinized and made complete. The algorithm returns an arbitrary word from the complemented NFA constructed until the first macrostate without any final states in the original automaton is encountered.

Parameters:

alphabet – [in] Alphabet to use for computing the complement. If nullptr, uses this->alphabet when defined, otherwise uses this->delta.get_used_symbols().

Pre:

The automaton does not contain any epsilon transitions. TODO: Support lazy epsilon closure?

Returns:

An arbitrary word from the complemented automaton, or std::nullopt if the automaton is universal on the chosen set of symbols for the complement.

bool make_complete(const Alphabet *alphabet = nullptr, std::optional<State> sink_state = std::nullopt)

Make NFA complete in place.

For each state 0,…,this->num_of_states()-1, add transitions with “missing” symbols from alphabet (symbols that do not occur on transitions from given state) to sink_state. If sink_state does not belong to the NFA, it is added to it, but only in the case that some transition to sink_state was added. In the case that NFA does not contain any states, this function does nothing.

Parameters:

• alphabet – [in] Alphabet to use for computing “missing” symbols. If nullptr, use this->alphabet when defined, otherwise use this->delta.get_used_symbols().

• sink_state – [in] The state into which new transitions are added. If std::nullopt, add a new sink state.

Returns:

true if a new transition was added to the NFA.

bool make_complete(const utils::OrdVector<Symbol> &symbols, std::optional<State> sink_state = std::nullopt)

Make NFA complete in place.

For each state 0,…,this->num_of_states()-1, add transitions with “missing” symbols from alphabet (symbols that do not occur on transitions from given state) to sink_state. If sink_state does not belong to the NFA, it is added to it, but only in the case that some transition to sink_state was added. In the case that NFA does not contain any states, this function does nothing.

This overloaded version is a more efficient version which does not need to compute the set of symbols to complete to from the alphabet. Prefer this version when you already have the set of symbols precomputed or plan to complete multiple automata over the same set of symbols.

Parameters:

• symbols – [in] Symbols to compute “missing” symbols from.

• sink_state – [in] The state into which new transitions are added. If std::nullopt, add a new sink state.

Returns:

true if a new transition was added to the NFA.

Nfa &complement_deterministic(const mata::utils::OrdVector<Symbol> &symbols, std::optional<State> sink_state = std::nullopt)

Complement deterministic automaton in-place by adding a sink state and swapping final and non-final states.

Parameters:

• symbols – [in] Symbols needed to make the automaton complete.

• sink_state – [in] State to be used as a sink state. Adds a new sink state when not specified.

Returns:

DFA complemented in-place.

Pre:

this is a deterministic automaton.

Public Members

Levels levels = {}

Vector of levels giving each state a level in range from 0 to levels.num_of_levels - 1.

For state q, levels[q] gives the state q a level.

Also holds the number of levels in the NFT in levels.num_of_levels.

Delta delta

For state q, delta[q] keeps the list of transitions ordered by symbols.

The set of states of this automaton are the numbers from 0 to the number of states minus one.

Alphabet *alphabet = nullptr

The alphabet which can be shared between multiple automata. Key value store for additional attributes for the NFA. Keys are attribute names as strings and the value types are up to the user. For example, we can set up attributes such as “state_dict” for state dictionary attribute mapping states to their respective names, or “transition_dict” for transition dictionary adding a human-readable meaning to each transition.