Nondeterministic Finite automata

page Nondeterministic Finite Automata (NFAs)

The design of NFAs in Mata

NFAs in Mata are represented using the mata::nfa::Nfa class. The transition relation is represented using the mata::nfa::Delta class, which provides an efficient way to store and manipulate transitions. The states of the NFA are represented as integers, starting from 0 up to the number of states minus one. The initial and final states are represented using the mata::utils::SparseSet class, which allows for efficient storage and manipulation of sets of states.

mata::nfa::Delta is a key component of the NFA representation. It stores transitions in a three-level data structure:

1. A vector indexed by source states, where each entry mata::nfa::StatePost contains a vector of symbol posts mata::nfa::SymbolPost.

2. Each mata::nfa::SymbolPost represents a set of transitions labeled with a specific symbol from the source state to a set of target states.

3. Each mata::nfa::SymbolPost object contains a set of target states std::OrdVector<State> that can be reached from the source state via the corresponding symbol.

The main idea behind mata::nfa::Nfa is that the members (mata::nfa::Nfa::delta, mata::nfa::Nfa::initial, mata::nfa::Nfa::alphabet, …) do not depend on each other. This allows for some well-optimized implementations as well as easy replacement of individual members, or extensions to the NFA structure (e.g., adding levels for NFT), if needed. However, this also poses a risk of inconsistency between the members (e.g., having initial states that do not exist in the delta). The high-level functions in mata::nfa namespace and mata::nfa::Nfa class are designed to maintain the consistency of the NFA structure, but the individual members can be modified directly by the user, which may lead to inconsistencies, yet there are often useful when implementing highly-optimized algorithms.

The main operation on NFAs is BFS/DFS through mata::nfa::Delta structure, which is used in most algorithms. The data structure is designed such that direct access to a specific transition is less efficient, but iterating through all transitions from a given source state, for all source states is efficient (e.g., mata::utils::SynchronizedIterator). When designing algorithms for Mata, be sure utilize iteration through mata::nfa::Delta structure as much as possible.

Working with NFAs

The library provides various functions to create, manipulate, and analyze NFAs. The core operations on NFAs, such as union, intersection, complement, determinization, and minimization, are implemented in mata::nfa namespace and as methods of the mata::nfa::Nfa class. More advanced algorithms and utilities are available in the mata::nfa::algorithms and mata::nfa::plumbing namespaces. Users can create NFAs manually by adding states and transitions using the methods provided in the mata::nfa::Nfa and mata::nfa::Delta classes, or they can use higher-level functions to construct NFAs from regular expressions, words, or other NFAs using the functions in the mata::nfa::builder and mata::parser namespaces.

Note

The algorithms provided in Mata for NFAs are designed to perform only the core operations on NFAs, such as union, intersection, complement, determinization, minimization, etc., but do not by default optimize the NFAs during these operations. Users can apply optimization algorithms separately after performing the core operations, such as using the mata::nfa::reduce() function to reduce the resulting NFA, mata::nfa::minimize() to minimize the resulting NFA, or mata::nfa::trim() to remove unreachable and non-terminating states.

Types

Basic types used in the mata::nfa module for NFAs.

namespace mata

Main namespace including structs and algorithms for all automata.

In particular, this includes:

1. Alphabets,

2. Formula graphs and nodes,

3. Mintermization,

4. Closed sets.

namespace nfa

Typedefs

using State = unsigned long

using StateSet = utils::OrdVector<State>

using StateRenaming = std::unordered_map<State, State>

using ParameterMap = std::unordered_map<std::string, std::string>

Map of additional parameter name and value pairs.

Used by certain functions for specifying some additional parameters in the following format:

ParameterMap {
    { "algorithm", "classical" },
    { "minimize", "true" }
}

Enums

enum class EpsilonClosureOpt : unsigned

Values:

enumerator None

No epsilon closure.

enumerator Before

Epsilon closure before the transition.

enumerator After

Epsilon closure after the transition.

enumerator BeforeAndAfter

Epsilon closure before and after the transition.

enum class ProductFinalStateCondition

Values:

enumerator And

Both original states have to be final.

enumerator Or

At least one of the original states has to be final.

Variables

const std::string TYPE_NFA

Symbol EPSILON = {Limits::max_symbol}

A non-deterministic finite automaton.

An epsilon symbol which is now defined as the maximal value of data type used for symbols.

struct Limits

#include <types.hh>

Public Static Attributes

static State min_state = std::numeric_limits<State>::min()

static State max_state = std::numeric_limits<State>::max()

static Symbol min_symbol = std::numeric_limits<Symbol>::min()

static Symbol max_symbol = std::numeric_limits<Symbol>::max()

struct Run

#include <types.hh>

Public Members

Word word = {}

A finite-length word.

std::vector<State> path = {}

A finite-length path through automaton.

NFA

Nondeterministic Finite Automata including structures, transitions and algorithms.

In particular, this includes:

1. Structures (Automaton, Transitions, Results, Delta),

2. Algorithms (operations, checks, tests),

3. Constructions.

Other algorithms are included in mata::nfa::plumbing (simplified API for, e.g., bindings) and mata::nfa::algorithms (concrete implementations of algorithms, such as for complement).

namespace mata

Main namespace including structs and algorithms for all automata.

In particular, this includes:

1. Alphabets,

2. Formula graphs and nodes,

3. Mintermization,

4. Closed sets.

namespace nfa

Typedefs

template<typename ...Ts>
using conjunction = std::is_same<bool_pack<true, Ts::value...>, bool_pack<Ts::value..., true>>

Check that for all values in a pack Ts are ‘true’.

template<typename T, typename ...Ts>
using AreAllOfType = conjunction<std::is_same<Ts, T>...>::type

Check that all types in a sequence of parameters Ts are of type T.

Functions

template<typename ...Nfas, typename = AreAllOfType<const Nfa&, Nfas...>>
OnTheFlyAlphabet create_alphabet(const Nfas&... nfas)

Create alphabet from variadic number of NFAs given as arguments.

in] Nfas Type Nfa.

Tparam :

Parameters:

nfas – [in] NFAs to create alphabet from.

Returns:

Created alphabet.

OnTheFlyAlphabet create_alphabet(const std::vector<std::reference_wrapper<const Nfa>> &nfas)

Create alphabet from a vector of NFAs.

Parameters:

nfas – [in] Vector of NFAs to create alphabet from.

Returns:

Created alphabet.

OnTheFlyAlphabet create_alphabet(const std::vector<std::reference_wrapper<Nfa>> &nfas)

Create alphabet from a vector of NFAs.

Parameters:

nfas – [in] Vector of NFAs to create alphabet from.

Returns:

Created alphabet.

OnTheFlyAlphabet create_alphabet(const std::vector<Nfa*> &nfas)

Create alphabet from a vector of NFAs.

Parameters:

nfas – [in] Vector of pointers to NFAs to create alphabet from.

Returns:

Created alphabet.

OnTheFlyAlphabet create_alphabet(const std::vector<const Nfa*> &nfas)

Create alphabet from a vector of NFAs.

Parameters:

nfas – [in] Vector of pointers to NFAs to create alphabet from.

Returns:

Created alphabet.

Nfa union_nondet(const Nfa &lhs, const Nfa &rhs)

Compute non-deterministic union.

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

Returns:

Non-deterministic union of lhs and rhs.

Nfa union_det_complete(const Nfa &lhs, const Nfa &rhs)

Compute union of two complete deterministic NFAs.

Perserves determinism.

The union is computed by product construction with OR condition on the final states.

Parameters:

• lhs – First complete deterministic automaton.

• rhs – Second complete deterministic automaton.

Nfa product(const Nfa &lhs, const Nfa &rhs, ProductFinalStateCondition final_condition = ProductFinalStateCondition::And, Symbol first_epsilon = EPSILON, std::unordered_map<std::pair<State, State>, State> *prod_map = nullptr)

Compute product of two NFAs with OR condition on the final states.

Automata must share alphabets. //TODO: this is not implemented yet.

Parameters:

• lhs – First NFA.

• rhs – Second NFA.

• final_condition – Condition for a product state to be final.

  • AND: both original states have to be final.

  • OR: at least one of the original states has to be final.

• first_epsilon – Smallest epsilon symbol. //TODO: this should eventually be taken from the alphabet as anything larger than the largest symbol?

• prod_map – Mapping of pairs of the original states (lhs_state, rhs_state) to new product states (not used internally, allocated only when !=nullptr, expensive).

Nfa lang_difference(const Nfa &nfa_included, const Nfa &nfa_excluded, std::optional<std::function<bool(const Nfa&, const Nfa&, const StateSet&, const StateSet&, State, const Nfa&)>> macrostate_discover = std::nullopt)

Compute a language difference as nfa_included \ nfa_excluded.

Computed as a lazy intersection of nfa_included and a complement of nfa_excluded. The NFAs are lazily determinized and the complement is constructed lazily as well, guided by nfa_included.

Todo:

: TODO: Add support for specifying first epsilon symbol and compute epsilon closure during determinization.

Parameters:

• nfa_included – [in] NFA to include in the difference.

• nfa_excluded – [in] NFA to exclude from the difference.

• macrostate_discover – [in] Callback event handler for discovering a new macrostate in the language difference automaton for the first time. Return true if the computation should continue, and false if the computation should stop and return only the NFA for the language difference constructed so far. The parameters are: const Nfa& nfa_included, const Nfa& nfa_excluded, const StateSet& macrostate_included_state_set, const StateSet& macrostate_excluded_state_set, const State macrostate, const Nfa& nfa_lang_difference.

Nfa intersection(const Nfa &lhs, const Nfa &rhs, Symbol first_epsilon = EPSILON, std::unordered_map<std::pair<State, State>, State> *prod_map = nullptr)

Compute intersection of two NFAs.

Both automata can contain ε-transitions. The product preserves the ε-transitions, i.e., for each each product state (s, t) withs -ε-> p, (s, t) -ε-> (p, t) is created, and vice versa.

Automata must share alphabets. //TODO: this is not implemented yet.

Parameters:

• lhs – [in] First NFA to compute intersection for.

• rhs – [in] Second NFA to compute intersection for.

• first_epsilon – [in] smallest epsilon. //TODO: this should eventually be taken from the alphabet as anything larger than the largest symbol?

• prod_map – [out] Mapping of pairs of the original states (lhs_state, rhs_state) to new product states (not used internally, allocated only when !=nullptr, expensive).

Returns:

NFA as a product of NFAs lhs and rhs with ε-transitions preserved.

Nfa concatenate(const Nfa &lhs, const Nfa &rhs, bool use_epsilon = false, StateRenaming *lhs_state_renaming = nullptr, StateRenaming *rhs_state_renaming = nullptr)

Concatenate two NFAs.

Supports epsilon symbols when use_epsilon is set to true.

Parameters:

• lhs – [in] First automaton to concatenate.

• rhs – [in] Second automaton to concatenate.

• use_epsilon – [in] Whether to concatenate over epsilon symbol.

• lhs_state_renaming – [out] Map mapping lhs states to result states.

• rhs_state_renaming – [out] Map mapping rhs states to result states.

Returns:

Concatenated automaton.

Nfa complement(const Nfa &aut, const Alphabet &alphabet, const ParameterMap &params = {{"algorithm", "classical"}})

Compute automaton accepting complement of aut.

Parameters:

• aut – [in] Automaton whose complement to compute.

• alphabet – [in] Alphabet used for complementation.

• params – [in] Optional parameters to control the complementation algorithm:

  • ”algorithm”:

    • ”classical”: The classical algorithm determinizes the automaton, makes it complete, and swaps final and non-final states.

    • ”brzozowski”: The Brzozowski algorithm determinizes the automaton using Brzozowski minimization, makes it complete, and swaps final and non-final states.

Returns:

Complemented automaton.

Nfa complement(const Nfa &aut, const utils::OrdVector<Symbol> &symbols, const ParameterMap &params = {{"algorithm", "classical"}})

Compute automaton accepting complement of aut.

This overloaded version complements over an already created ordered set of symbols instead of an alphabet. This is a more efficient solution in case you already have symbols precomputed or want to complement multiple automata over the same set of symbols: the function does not need to compute the ordered set of symbols from the alphabet again (and for each automaton).

Parameters:

• aut – [in] Automaton whose complement to compute.

• symbols – [in] Symbols to complement over.

• params – [in] Optional parameters to control the complementation algorithm:

  • ”algorithm”:

    • ”classical”: The classical algorithm determinizes the automaton, makes it complete, and swaps final and non-final states.

    • ”brzozowski”: The Brzozowski algorithm determinizes the automaton using Brzozowski minimization, makes it complete, and swaps final and non-final states.

Returns:

Complemented automaton.

Nfa minimize(const Nfa &aut, const ParameterMap &params = {{"algorithm", "brzozowski"}})

Compute minimal deterministic automaton.

Parameters:

• aut – [in] Automaton whose minimal version to compute.

• params – [in] Optional parameters to control the minimization algorithm:

  • ”algorithm”: “brzozowski”

Returns:

Minimal deterministic automaton.

Nfa determinize(const Nfa &aut, std::unordered_map<StateSet, State> *subset_map = nullptr, std::optional<std::function<bool(const Nfa&, State, const StateSet&)>> macrostate_discover = std::nullopt)

Determinize automaton.

Todo:

: TODO: Add support for specifying first epsilon symbol and compute epsilon closure during determinization.

Parameters:

• aut – [in] Automaton to determinize.

• subset_map – [out] Map that maps sets of states of input automaton to states of determinized automaton.

• macrostate_discover – [in] Callback event handler for discovering a new macrostate for the first time. The parameters are the determinized NFA constructed so far, the current macrostate, and the set of the original states corresponding to the macrostate. Return true if the determinization should continue, and false if the determinization should stop and return only the determinized NFA constructed so far.

Returns:

Determinized automaton.

Nfa reduce(const Nfa &aut, StateRenaming *state_renaming = nullptr, const ParameterMap &params = {{"algorithm", "simulation"}, {"type", "after"}, {"direction", "forward"}})

Reduce the size of the automaton.

Parameters:

• aut – [in] Automaton to reduce.

• state_renaming – [out] Mapping of original states to reduced states.

• params – [in] Optional parameters to control the reduction algorithm:

  • ”algorithm”: “simulation”, “residual”, and options to parametrize residual reduction, not utilized in simulation

  • ”type”: “after”, “with”,

  • ”direction”: “forward”, “backward”.

Returns:

Reduced automaton.

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

Checks inclusion of languages of two NFAs: smaller and bigger (smaller <= bigger).

Parameters:

• smaller – [in] First automaton to concatenate.

• bigger – [in] Second automaton to concatenate.

• cex – [out] Counterexample for the inclusion.

• alphabet – [in] Alphabet of both NFAs to compute with.

• params – [in] Optional parameters to control the equivalence check algorithm:

  • ”algorithm”: “naive”, “antichains” (Default: “antichains”)

Returns:

True if smaller is included in bigger, false otherwise.

inline bool is_included(const Nfa &smaller, const Nfa &bigger, const Alphabet *const alphabet = nullptr, const ParameterMap &params = {{"algorithm", "antichains"}})

Checks inclusion of languages of two NFAs: smaller and bigger (smaller <= bigger).

Parameters:

• smaller – [in] First automaton to concatenate.

• bigger – [in] Second automaton to concatenate.

• alphabet – [in] Alphabet of both NFAs to compute with.

• params – [in] Optional parameters to control the equivalence check algorithm:

  • ”algorithm”: “naive”, “antichains” (Default: “antichains”)

Returns:

True if smaller is included in bigger, false otherwise.

bool are_equivalent(const Nfa &lhs, const Nfa &rhs, const Alphabet *alphabet, const ParameterMap &params = {{"algorithm", "antichains"}})

Perform equivalence check of two NFAs: lhs and rhs.

Parameters:

• lhs – [in] First automaton to concatenate.

• rhs – [in] Second automaton to concatenate.

• alphabet – [in] Alphabet of both NFAs to compute with.

• params[ – [in] Optional parameters to control the equivalence check algorithm:

  • ”algorithm”: “naive”, “antichains” (Default: “antichains”)

Returns:

True if lhs and rhs are equivalent, false otherwise.

bool are_equivalent(const Nfa &lhs, const Nfa &rhs, const ParameterMap &params = {{"algorithm", "antichains"}})

Perform equivalence check of two NFAs: lhs and rhs.

The current implementation of Nfa does not accept input alphabet. For this reason, an alphabet has to be created from all transitions each time an operation on alphabet is called. When calling this function, the alphabet has to be computed first.

Hence, this function is less efficient than its alternative taking already defined alphabet as its parameter. That way, alphabet has to be computed only once, as opposed to the current ad-hoc construction of the alphabet. The use of the alternative with defined alphabet should be preferred.

Parameters:

• lhs – [in] First automaton to concatenate.

• rhs – [in] Second automaton to concatenate.

• params – [in] Optional parameters to control the equivalence check algorithm:

  • ”algorithm”: “naive”, “antichains” (Default: “antichains”)

Returns:

True if lhs and rhs are equivalent, false otherwise.

Nfa revert(const Nfa &aut)

Reverting the automaton by one of the three functions below, currently simple_revert seems best (however, not tested enough).

Nfa fragile_revert(const Nfa &aut)

This revert algorithm is fragile, uses low level accesses to Nfa and static data structures, and is potentially dangerous when there are used symbols with large numbers (allocates an array indexed by symbols). It is asymptotically faster, however. For somewhat dense automata, the performance is the same or a little bit slower than simple_revert otherwise. Not affected by pre-reserving vectors.

Nfa simple_revert(const Nfa &aut)

Reverting the automaton by a simple algorithm, which does a lot of random access addition to Post and Move. Much affected by pre-reserving vectors.

Nfa somewhat_simple_revert(const Nfa &aut)

Reverting the automaton by a modification of the simple algorithm. It replaces random access addition to SymbolPost by push_back and sorting later, so far seems the slowest of all, except on dense automata, where it is almost as slow as simple_revert. Candidate for removal.

Nfa remove_epsilon(const Nfa &aut, Symbol epsilon = EPSILON)

Removing epsilon transitions.

Run encode_word(const Alphabet *alphabet, const std::vector<std::string> &input)

Encodes a vector of strings (each corresponding to one symbol) into a Word instance.

utils::OrdVector<Symbol> get_symbols_to_work_with(const nfa::Nfa &nfa, const Alphabet *shared_alphabet = nullptr)

Get the set of symbols to work with during operations.

Parameters:

• nfa – NFA to get symbols from.

• shared_alphabet – [in] Optional alphabet shared between NFAs passed as an argument to a function.

std::optional<Word> get_word_from_lang_difference(const Nfa &nfa_included, const Nfa &nfa_excluded)

Get any arbitrary accepted word in the language difference of nfa_included without nfa_excluded.

The language difference automaton is lazily constructed without computing the whole determinized automata and the complememt of nfa_excluded. The algorithm returns an arbitrary word from the language difference constructed until the first macrostate with a final state in the original states in nfa_included and without any corresponding final states in nfa_excluded is encountered.

Parameters:

• nfa_included – [in] NFA to include in the language difference.

• nfa_excluded – [in] NFA to exclude in the language difference. TODO: Support lazy epsilon closure?

Pre:

The automaton does not contain any epsilon transitions.

Returns:

An arbitrary word from the language difference, or std::nullopt if the language difference automaton is universal on the set of symbols from transitions of nfa_included.

template<bool...>
struct bool_pack

#include <nfa.hh>

Pack of bools for reasoning about a sequence of parameters.

class Nfa

#include <nfa.hh>

A class representing an NFA.

Subclassed by Nft

Public Functions

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

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

Construct a new explicit NFA 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 – [in] Initial states of the NFA.

• final_states – [in] Final states of the NFA.

• alphabet – [in] Pointer to the alphabet used by the NFA.

Nfa(const Nfa &other) = default

Construct a new explicit NFA from other NFA.

inline Nfa(Nfa &&other) noexcept

Nfa &operator=(const Nfa &other) = default

Nfa &operator=(Nfa &&other) noexcept

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 delta if state is not in delta yet.

Returns:

The requested state.

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

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

Creates new states along the path of the word.

Parameters:

• source – The source state where the word begins. It must already be a part of the automaton.

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

• target – The target state where the word ends.

Returns:

The state target where the inserted word ends.

State insert_word(State source, const Word &word)

Inserts a word into the NFA from a source state source to a new target state.

Creates new states along the path of the word.

Parameters:

• source – The source state where the word begins. It must already be a part of the automaton.

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

Returns:

The newly created target state where the inserted word ends.

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.

inline bool is_state(const State &state_to_check) const

void clear()

Clear the underlying NFA to a blank NFA.

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

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 std::function<bool(State)> &filter = nullptr) 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 i-th value is true iff the state i is useful.

void tarjan_scc_discover(const TarjanDiscoverCallback &callback) const

Tarjan’s SCC discover algorithm.

Parameters:

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

Nfa &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.

Nfa decode_utf8() const

Decodes automaton from UTF-8 encoding.

Method removes unreachable states from delta.

Returns:

Decoded automaton.

StateSet mk_epsilon_closure(const StateSet &source_states, const std::vector<Symbol> &epsilons = {EPSILON}) const

Get the epsilon closure of the given set of states.

Parameters:

• source_states – Set of source states.

• epsilons – Set of symbols to consider as epsilons when computing the closure.

Returns:

Epsilon closure of the given set of states.

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 state, const std::vector<State> &distances_to_final) const

Get some shortest accepting run from state state.

Parameters:

• state – State from which the accepting run starts.

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

void remove_epsilon(Symbol epsilon = EPSILON)

Remove epsilon transitions from the automaton.

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.

std::string print_to_dot(bool decode_ascii_chars = false, bool use_intervals = false, int max_label_length = -1, const Alphabet *alphabet = nullptr) 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 Alphabet *alphabet = nullptr) const

Prints the automaton to the output stream in DOT format.

Parameters:

• output – [out] Output stream 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.

void print_to_dot(const std::string &filename, bool decode_ascii_chars = false, bool use_intervals = false, int max_label_length = -1, const Alphabet *alphabet = nullptr) 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 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:

• output – [out] Output stream to print the automaton to.

• 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

StateSet post(const StateSet &states, 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, const 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, const 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_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_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

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_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:

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

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

Check whether the language of the automaton is universal.

Parameters:

• alphabet – Alphabet to use for checking the universality.

• cex – Counterexample path for a case the language is not universal.

• params – Optional parameters to control the universality check algorithm:

  • ”algorithm”:

    • ”antichains”: The algorithm uses antichains to check the universality.

    • ”naive”: The algorithm uses the naive approach to check the universality.

Returns:

True if the language of the automaton is universal, false otherwise.

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

Check whether the language of the automaton is universal.

Parameters:

• alphabet – Alphabet to use for checking the universality.

• params – Optional parameters to control the universality check algorithm:

  • ”algorithm”:

    • ”antichains”: The algorithm uses antichains to check the universality.

    • ”naive”: The algorithm uses the naive approach to check the universality.

Returns:

True if the language of the automaton is universal, false otherwise.

bool is_in_lang(const Run &run, 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:

• run – 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) const

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.

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

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

Parameters:

• run – 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.

inline bool is_in_lang_prefix(const Run &run, const bool use_epsilon = false) const

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

Parameters:

• run – 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_in_lang_prefix(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.

std::pair<Run, bool> get_word_for_path(const Run &run) const

std::set<Word> get_words(size_t max_length) 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 get_words(aut.num_of_states())

std::optional<Word> get_word(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

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.

utils::SparseSet<State> initial = {}

utils::SparseSet<State> final = {}

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.

std::unordered_map<std::string, void*> attributes = {}

Public Static Functions

static inline bool is_epsilon(const Symbol symbol)

Check whether symbol is epsilon symbol or not.

Parameters:

symbol – Symbol to check.

Returns:

True if the passed symbol is epsilon, false otherwise.

struct TarjanDiscoverCallback

#include <nfa.hh>

Structure for storing callback functions (event handlers) utilizing Tarjan’s SCC discover algorithm.

Public Members

std::function<bool(State)> state_discover

std::function<bool(const std::vector<State>&, const std::vector<State>&)> scc_discover

std::function<void(State)> scc_state_discover

std::function<void(State, State)> succ_state_discover

namespace std

Functions

std::ostream &operator<<(std::ostream &os, const mata::nfa::Transition &trans)

std::ostream &operator<<(std::ostream &os, const mata::nfa::Nfa &nfa)

template<>
struct hash<mata::nfa::Transition>

#include <nfa.hh>

Public Functions

inline size_t operator()(const mata::nfa::Transition &trans) const noexcept

Delta

Data structures representing the delta (transition function) of an NFA, mapping states and input symbols to sets of states.

namespace mata

Main namespace including structs and algorithms for all automata.

In particular, this includes:

1. Alphabets,

2. Formula graphs and nodes,

3. Mintermization,

4. Closed sets.

namespace nfa

class Delta

#include <delta.hh>

Delta is a data structure for representing transition relation.

Transition is represented as a triple Transition(source state, symbol, target state). Move is the part (symbol, target state), specified for a single source state. Its underlying data structure is vector of StatePost classes. Each index to the vector corresponds to one source state, that is, a number for a certain state is an index to the vector of state posts. Transition relation (delta) in Mata stores a set of transitions in a four-level hierarchical structure: Delta, StatePost, SymbolPost, and a set of target states. A vector of ‘StatePost’s indexed by a source states on top, where the StatePost for a state ‘q’ (whose number is ‘q’ and it is the index to the vector of ‘StatePost’s) stores a set of ‘Move’s from the source state ‘q’. Namely, ‘StatePost’ has a vector of ‘SymbolPost’s, where each ‘SymbolPost’ stores a symbol ‘a’ and a vector of target states of ‘a’-moves from state ‘q’. ‘SymbolPost’s are ordered by the symbol, target states are ordered by the state number.

Public Types

using const_iterator = std::vector<StatePost>::const_iterator

Public Functions

inline Delta()

Delta(const Delta &other) = default

Delta(Delta &&other) = default

inline explicit Delta(const size_t n)

Delta &operator=(const Delta &other) = default

Delta &operator=(Delta &&other) = default

bool operator==(const Delta &other) const

inline void reserve(const size_t n)

inline const StatePost &state_post(const State source) const

Get constant reference to the state post of source.

If we try to access a state post of a source which is present in the automaton as an initial/final state, yet does not have allocated space in Delta, an empty_post is returned. Hence, the function has no side effects (no allocation is performed; iterators remain valid).

Parameters:

source[in] – Source state of a state post to access.

Returns:

State post of source.

inline const StatePost &operator[](const State source) const

Get constant reference to the state post of source.

If we try to access a state post of a source which is present in the automaton as an initial/final state, yet does not have allocated space in Delta, an empty_post is returned. Hence, the function has no side effects (no allocation is performed; iterators remain valid).

Parameters:

source[in] – Source state of a state post to access.

Returns:

State post of source.

StatePost &mutable_state_post(State source)

Get mutable (non-constant) reference to the state post of source.

The function allows modifying the state post.

BEWARE, IT HAS A SIDE EFFECT.

If we try to access a state post of a source which is present in the automaton as an initial/final state, yet does not have allocated space in Delta, a new state post for source will be allocated along with all state posts for all previous states. This in turn may cause that the entire post data structure is re-allocated. Iterators to Delta will get invalidated. Use the constant ‘state_post()’ is possible. Or, to prevent the side effect from causing issues, one might want to make sure that posts of all states in the automaton are allocated, e.g., write an NFA method that allocate Delta for all states of the NFA.

Parameters:

source[in] – Source state of a state post to access.

Returns:

State post of source.

void defragment(const BoolVector &is_staying, const std::vector<State> &renaming)

template<typename ...Args>
inline StatePost &emplace_back(Args&&... args)

inline void clear()

inline void allocate(const size_t num_of_states)

Allocate state posts up to num_of_states states, creating empty StatePost for yet unallocated state posts.

Parameters:

num_of_states – [in] Number of states in Delta to allocate state posts for. Have to be at least num_of_states() + 1.

inline size_t num_of_states() const

Returns:

Number of states in the whole Delta, including both source and target states.

inline bool uses_state(const State state) const

Check whether the state is used in Delta.

size_t num_of_transitions() const

Returns:

Number of transitions in Delta.

void add(State source, Symbol symbol, State target)

inline void add(const Transition &trans)

void remove(State source, Symbol symbol, State target)

inline void remove(const Transition &transition)

bool contains(State source, Symbol symbol, State target) const

Check whether Delta contains a passed transition.

bool contains(const Transition &transition) const

Check whether Delta contains a transition passed as a triple.

bool empty() const

Check whether automaton contains no transitions.

Returns:

True if there are no transitions in the automaton, false otherwise.

inline void append(const std::vector<StatePost> &post_vector)

Append post vector to the delta.

Parameters:

post_vector – Vector of posts to be appended.

std::vector<StatePost> renumber_targets(const std::function<State(State)> &target_renumberer) const

Copy posts of delta and apply a lambda update function on each state from targets.

IMPORTANT: In order to work properly, the lambda function needs to be monotonic, that is, the order of states in targets cannot change.

Parameters:

target_renumberer – Monotonic lambda function mapping states to different states.

Returns:

std::vector<Post> Copied posts.

void add(State source, Symbol symbol, const StateSet &targets)

Add transitions to multiple destinations.

Parameters:

• source – From

• symbol – Symbol

• targets – Set of states to

inline const_iterator cbegin() const

inline const_iterator cend() const

inline const_iterator begin() const

inline const_iterator end() const

Transitions transitions() const

Iterator over transitions represented as Transition instances.

std::vector<Transition> get_transitions_to(State state_to) const

Get transitions leading to state_to.

Operation is slow, traverses over all symbol posts.

Parameters:

state_to[in] – Target state for transitions to get.

Returns:

Transitions leading to state_to.

std::vector<Transition> get_transitions_between(State state_from, State state_to) const

Get transitions from state_from to state_to.

Operation is slow, traverses over all symbol posts.

Parameters:

• state_from[in] – Source state.

• state_from[in] – Target state.

Returns:

Transitions from source to state_to.

StateSet get_successors(State state) const

Get the set of states that are successors of the given state.

Parameters:

state – [in] State from which successors are checked.

Returns:

Set of states that are successors of the given state.

const StateSet &get_successors(State state, Symbol symbol) const

StateSet get_successors(State state, Symbol symbol, EpsilonClosureOpt epsilon_closure_opt) const

StatePost::const_iterator epsilon_symbol_posts(State state, Symbol epsilon = EPSILON) const

Iterate over epsilon symbol posts under the given state.

Parameters:

• state – [in] State from which epsilon transitions are checked.

• epsilon – [in] User can define his favourite epsilon or used default.

Returns:

An iterator to SymbolPost with epsilon symbol. End iterator when there are no epsilon transitions.

void add_symbols_to(OnTheFlyAlphabet &target_alphabet) const

Expand target_alphabet by symbols from this delta.

The value of the already existing symbols will NOT be overwritten.

utils::OrdVector<Symbol> get_used_symbols() const

Get the set of symbols used on the transitions in the automaton.

Does not necessarily have to equal the set of symbols in the alphabet used by the automaton.

Returns:

Set of symbols used on the transitions.

utils::OrdVector<Symbol> get_used_symbols_vec() const

std::set<Symbol> get_used_symbols_set() const

utils::SparseSet<Symbol> get_used_symbols_sps() const

std::vector<bool> get_used_symbols_bv() const

BoolVector get_used_symbols_chv() const

Symbol get_max_symbol() const

Get the maximum non-epsilon used symbol.

Public Static Functions

static StatePost::const_iterator epsilon_symbol_posts(const StatePost &state_post, Symbol epsilon = EPSILON)

Iterate over epsilon symbol posts under the given state_post.

Parameters:

• state_post – [in] State post from which epsilon transitions are checked.

• epsilon – [in] User can define his favourite epsilon or used default.

Returns:

An iterator to SymbolPost with epsilon symbol. End iterator when there are no epsilon transitions.

Public Static Attributes

static const StatePost empty_state_post

Protected Attributes

std::vector<StatePost> state_posts_

class Transitions

#include <delta.hh>

Iterator over transitions represented as Transition instances.

It iterates over triples (State source, Symbol symbol, State target).

Public Functions

Transitions() = default

inline explicit Transitions(const Delta *delta)

Transitions(Transitions&&) = default

Transitions(const Transitions&) = default

Transitions &operator=(Transitions&&) = default

Transitions &operator=(const Transitions&) = default

const_iterator begin() const

Public Static Functions

static const_iterator end()

Private Members

const Delta *delta_

class const_iterator

#include <delta.hh>

Iterator over transitions.

Public Types

using iterator_category = std::forward_iterator_tag

using value_type = Transition

using difference_type = size_t

using pointer = Transition*

using reference = Transition&

Public Functions

inline const_iterator()

explicit const_iterator(const Delta &delta)

const_iterator(const Delta &delta, State current_state)

const_iterator(const const_iterator &other) noexcept = default

const_iterator(const_iterator&&) = default

inline const Transition &operator*() const

inline const Transition *operator->() const

const_iterator &operator++()

const_iterator operator++(int)

const_iterator &operator=(const const_iterator &other) noexcept = default

const_iterator &operator=(const_iterator&&) = default

bool operator==(const const_iterator &other) const

Private Members

const Delta *delta_ = nullptr

size_t current_state_ = {}

StatePost::const_iterator state_post_it_ = {}

StateSet::const_iterator symbol_post_it_ = {}

bool is_end_ = {false}

Transition transition_ = {}

class Move

#include <delta.hh>

Move from a StatePost for a single source state, represented as a pair of symbol and target state target.

Public Functions

bool operator==(const Move&) const = default

Public Members

Symbol symbol

State target

class StatePost : private OrdVector<SymbolPost>

#include <delta.hh>

A data structure representing possible transitions over different symbols from a source state.

It is an ordered vector containing possible SymbolPost (i.e., pair of symbol and target states). SymbolPosts in the vector are ordered by symbols in SymbolPosts.

Public Functions

StatePost(const StatePost&) = default

StatePost(StatePost&&) = default

StatePost &operator=(const StatePost&) = default

StatePost &operator=(StatePost&&) = default

bool operator==(const StatePost&) const = default

inline iterator find(const Symbol symbol)

inline const_iterator find(const Symbol symbol) const

const_iterator first_epsilon_it(Symbol first_epsilon) const

returns an iterator to the smallest epsilon, or end() if there is no epsilon

StateSet get_successors() const

Get the set of all target states in the StatePost.

Returns:

Set of all target states in the StatePost.

const StateSet &get_successors(Symbol symbol) const

Returns a reference to target states for a given symbol in the StatePost.

If there is no such symbol, a static empty set is returned.

Parameters:

symbol – Symbol to get the successors for.

Returns:

Set of target states for the given symbol.

inline Moves moves() const

Iterator over all moves (over all labels) in StatePost represented as Move instances.

Moves moves(StatePost::const_iterator symbol_post_it, StatePost::const_iterator symbol_post_end) const

Iterator over specified moves in StatePost represented as Move instances.

Parameters:

• symbol_post_it – [in] First iterator over symbol posts to iterate over.

• symbol_post_end – [in] End iterator over symbol posts (which functions as an sentinel, is not iterated over).

Moves moves_epsilons(Symbol first_epsilon = EPSILON) const

Iterator over epsilon moves in StatePost represented as Move instances.

Moves moves_symbols(Symbol last_symbol = EPSILON - 1) const

Iterator over alphabet (normal) symbols (not over epsilons) in StatePost represented as Move instances.

size_t num_of_moves() const

Count the number of all moves in StatePost.

Private Types

using super = OrdVector<SymbolPost>

class Moves

#include <delta.hh>

Iterator over moves represented as Move instances.

It iterates over pairs (symbol, target) for the given StatePost.

Public Functions

Moves() = default

Moves(const StatePost &state_post, StatePost::const_iterator symbol_post_it, StatePost::const_iterator symbol_post_end)

construct moves iterating over a range symbol_post_it (including) to symbol_post_end (excluding).

Parameters:

• state_post – [in] State post to iterate over.

• symbol_post_it – [in] First iterator over symbol posts to iterate over.

• symbol_post_end – [in] End iterator over symbol posts (which functions as an sentinel; is not iterated over).

Moves(Moves&&) = default

Moves(Moves&) = default

Moves &operator=(Moves &&other) noexcept

Moves &operator=(const Moves &other) noexcept

const_iterator begin() const

Public Static Functions

static const_iterator end()

Private Members

const StatePost *state_post_ = {nullptr}

StatePost::const_iterator symbol_post_it_ = {}

Current symbol post iterator to iterate over. End symbol post iterator which is no longer iterated over (one after the last symbol post iterated over or end()).

StatePost::const_iterator symbol_post_end_ = {}

class const_iterator

#include <delta.hh>

Iterator over moves.

Public Types

using iterator_category = std::forward_iterator_tag

using value_type = Move

using difference_type = size_t

using pointer = Move*

using reference = Move&

Public Functions

inline const_iterator()

Construct end iterator.

const_iterator(const StatePost &state_post)

Const all moves iterator.

const_iterator(const StatePost &state_post, StatePost::const_iterator symbol_post_it, StatePost::const_iterator symbol_post_end)

Construct iterator from symbol_post_it (including) to symbol_post_it_end (excluding).

const_iterator(const const_iterator &other) noexcept = default

const_iterator(const_iterator&&) = default

inline const Move &operator*() const

inline const Move *operator->() const

const_iterator &operator++()

const_iterator operator++(int)

const_iterator &operator=(const const_iterator &other) noexcept = default

const_iterator &operator=(const_iterator&&) = default

bool operator==(const const_iterator &other) const

Private Members

const StatePost *state_post_ = {nullptr}

StatePost::const_iterator symbol_post_it_ = {}

StateSet::const_iterator target_it_ = {}

StatePost::const_iterator symbol_post_end_ = {}

bool is_end_ = {false}

Move move_ = {}

Internal allocated instance of Move which is set for the move currently iterated over and returned as a reference with operator*().

class SymbolPost

#include <delta.hh>

Structure represents a post of a single symbol: a set of target states in transitions.

A set of SymbolPost, called StatePost, is describing the automata transitions from a single source state.

Public Functions

SymbolPost() = default

inline explicit SymbolPost(const Symbol symbol)

inline SymbolPost(const Symbol symbol, const State state_to)

inline SymbolPost(const Symbol symbol, StateSet states_to)

inline SymbolPost(SymbolPost &&rhs) noexcept

SymbolPost(const SymbolPost &rhs) = default

SymbolPost &operator=(SymbolPost &&rhs) noexcept

SymbolPost &operator=(const SymbolPost &rhs) = default

inline std::weak_ordering operator<=>(const SymbolPost &other) const

inline bool operator==(const SymbolPost &other) const

inline StateSet::iterator begin()

inline StateSet::iterator end()

inline StateSet::const_iterator cbegin() const

inline StateSet::const_iterator cend() const

inline size_t count(const State s) const

inline bool empty() const

inline size_t num_of_targets() const

void insert(State s)

void insert(const StateSet &states)

inline void push_back(const State s)

template<typename ...Args>
inline StateSet &emplace_back(Args&&... args)

inline void erase(const State s)

inline std::vector<State>::const_iterator find(const State s) const

inline std::vector<State>::iterator find(const State s)

Public Members

Symbol symbol = {}

StateSet targets = {}

class SynchronizedExistentialSymbolPostIterator : public SynchronizedExistentialIterator<utils::OrdVector<SymbolPost>::const_iterator>

#include <delta.hh>

Specialization of utils::SynchronizedExistentialIterator for iterating over SymbolPosts.

Public Functions

StateSet unify_targets() const

Get union of all targets.

bool synchronize_with(const SymbolPost &sync)

Synchronize with the given SymbolPost sync.

Alignes the synchronized iterator to the same symbol as sync.

Returns:

True iff the synchronized iterator points to the same symbol as sync.

bool synchronize_with(Symbol sync_symbol)

Synchronize with the given symbol sync_symbol.

Alignes the synchronized iterator to the same symbol as sync_symbol.

Returns:

True iff the synchronized iterator points to the same symbol as sync.

struct Transition

#include <delta.hh>

A single transition in Delta represented as a triple(source, symbol, target).

Public Functions

inline Transition()

Transition(const Transition&) = default

Transition(Transition&&) = default

Transition &operator=(const Transition&) = default

Transition &operator=(Transition&&) = default

inline Transition(const State source, const Symbol symbol, const State target)

auto operator<=>(const Transition&) const = default

Public Members

State source

Source state.

Symbol symbol

Transition symbol.

State target

Target state.

Builder

namespace mata

Main namespace including structs and algorithms for all automata.

In particular, this includes:

1. Alphabets,

2. Formula graphs and nodes,

3. Mintermization,

4. Closed sets.

namespace nfa

namespace builder

Namespace providing options to build NFAs.

Typedefs

using NameStateMap = std::unordered_map<std::string, State>

Functions

Nfa create_single_word_nfa(const std::vector<Symbol> &word)

Create an automaton accepting only a single word.

Nfa create_single_word_nfa(const std::vector<std::string> &word, Alphabet *alphabet = nullptr)

Create an automaton accepting only a single word.

Parameters:

• word – Word to accept.

• alphabet – Alphabet to use in NFA for translating word into symbols. If specified, the alphabet has to contain translations for all of the word symbols. If left empty, a new alphabet with only the symbols of the word will be created.

Nfa create_empty_string_nfa()

Create automaton accepting only epsilon string.

Nfa create_sigma_star_nfa(Alphabet *alphabet = new OnTheFlyAlphabet{})

Create automaton accepting sigma star over the passed alphabet.

Parameters:

alphabet – [in] Alphabet to construct sigma star automaton with. When alphabet is left empty, the default empty alphabet is used, creating an automaton accepting only the empty string.

Nfa create_random_nfa_tabakov_vardi(size_t num_of_states, size_t alphabet_size, double states_transitions_ratio_per_symbol, double final_state_density, const std::optional<unsigned int> &seed = std::nullopt)

Creates Tabakov-Vardi random NFA.

The implementation is based on the paper “Experimental Evaluation of Classical Automata Constructions” by Tabakov and Vardi.

Parameters:

• num_of_states – Number of states in the automaton.

• alphabet_size – Size of the alphabet.

• states_transitions_ratio_per_symbol – Ratio between number of transitions and number of states for each symbol. The value must be in range [0, num_of_states]. A value of 1 means that there will be num_of_states transitions for each symbol. A value of num_of_states means that there will be a transition between every pair of states for each symbol.

• final_state_density – Density of final states in the automaton. The value must be in range [0, 1]. The state 0 is always final. If the density is 1, every state will be final.

• seed – Seed for the PRNG used. If no seed is given, the algorithm chooses one uniformly at random.

Nfa construct(const mata::parser::ParsedSection &parsec, Alphabet *alphabet, NameStateMap *state_map = nullptr)

Loads an automaton from Parsed object.

Nfa construct(const mata::IntermediateAut &inter_aut, Alphabet *alphabet, NameStateMap *state_map = nullptr)

Loads an automaton from Parsed object.

void construct(Nfa *result, const mata::IntermediateAut &inter_aut, Alphabet *alphabet, NameStateMap *state_map = nullptr)

Loads an automaton from Parsed object; version for python binding.

template<class ParsedObject>
Nfa construct(const ParsedObject &parsed, Alphabet *alphabet = nullptr, NameStateMap *state_map = nullptr)

Nfa parse_from_mata(std::istream &nfa_stream)

Parse NFA from the mata format in an input stream.

Parameters:

nfa_stream – Input stream containing NFA in mata format.

Throws:

std::runtime_error – Parsing of NFA fails.

Nfa parse_from_mata(const std::string &nfa_in_mata)

Parse NFA from the mata format in a string.

Parameters:

nfa_stream – String containing NFA in mata format.

Throws:

std::runtime_error – Parsing of NFA fails.

Nfa parse_from_mata(const std::filesystem::path &nfa_file)

Parse NFA from the mata format in a file.

Parameters:

nfa_stream – Path to the file containing NFA in mata format.

Throws:

• std::runtime_error – nfa_file does not exist.

• std::runtime_error – Parsing of NFA fails.

Nfa create_from_regex(const std::string &regex)

Create NFA from regex.

The created NFA does not contain epsilons, is trimmed and reduced. It uses the parser from RE2, see mata/parser/re2praser.hh for more details and options.

At https://github.com/google/re2/wiki/Syntax, you can find the syntax of regex with following futher limitations: 1) The allowed characters are the first 256 characters of Unicode, i.e., Latin1 encoding (ASCII + 128 more characters). For the full Unicode, check mata/parser/re2praser.hh. 2) The created automaton represents the language of the regex and is not expected to be used in regex matching. Therefore, stuff like ^, $, , etc. are ignored in the regex. For example, the regular expressions a*b and ^a*b will both result in the same NFA accepting the language of multiple ‘a’s followed by one ‘b’. See also issue #494.

See also

mata::parser::create_nfa()

Parameters:

regex – regular expression

Algorithms

Concrete NFA implementations of algorithms, such as complement, inclusion, or universality checking.

This is a separation of the implementation from the interface defined in mata::nfa.

Note

In mata::nfa interface, there are particular dispatch functions calling these function according to parameters provided by a user. E.g., we can call the following function: is_universal(aut, alph, {{‘algorithm, ‘antichains’}})` to check for universality based on antichain-based algorithm.

namespace mata

Main namespace including structs and algorithms for all automata.

In particular, this includes:

1. Alphabets,

2. Formula graphs and nodes,

3. Mintermization,

4. Closed sets.

namespace nfa

namespace algorithms

Concrete NFA implementations of algorithms, such as complement, inclusion, or universality checking.

Functions

Nfa minimize_brzozowski(const Nfa &aut)

Brzozowski minimization of automata (revert -> determinize -> revert -> determinize).

Parameters:

aut – [in] Automaton to be minimized.

Returns:

Minimized automaton.

Nfa minimize_hopcroft(const Nfa &dfa_trimmed)

Hopcroft minimization of automata.

Based on the algorithm from the paper: “Efficient Minimization of DFAs With Partial Transition Functions” by Antti Valmari and Petri Lehtinen. The algorithm works in O(a*n*log(n)) time and O(m+n+a) space, where: n is the number of states, a is the size of the alphabet, and m is the number of transitions. [https://dl.acm.org/doi/10.1016/j.ipl.2011.12.004]

Parameters:

dfa_trimmed – [in] Deterministic automaton without useless states. Perform trimming before calling this function.

Returns:

Minimized deterministic automaton.

Nfa complement_classical(const Nfa &aut, const mata::utils::OrdVector<Symbol> &symbols)

Complement implemented by determization, adding sink state and making automaton complete.

Then it adds final states which were non-final in the original automaton.

Parameters:

• aut – [in] Automaton to be complemented.

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

Returns:

Complemented automaton.

Nfa complement_brzozowski(const Nfa &aut, const mata::utils::OrdVector<Symbol> &symbols)

Complement implemented by determization using Brzozowski minimization, adding a sink state and making the automaton complete.

Then it swaps final and non-final states.

Parameters:

• aut – [in] Automaton to be complemented.

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

Returns:

Complemented automaton.

bool is_included_naive(const Nfa &smaller, const Nfa &bigger, const Alphabet *alphabet = nullptr, Run *cex = nullptr)

Inclusion implemented by complementation of bigger automaton, intersecting it with smaller and then it checks emptiness of intersection.

Parameters:

• smaller – [in] Automaton which language should be included in the bigger one.

• bigger – [in] Automaton which language should include the smaller one.

• alphabet – [in] Alphabet of both automata (it is computed automatically, but it is more efficient to set it if you have it).

• cex – [out] A potential counterexample word which breaks inclusion

Returns:

True if smaller language is included, i.e., if the final intersection of smaller complement of bigger is empty.

bool is_included_antichains(const Nfa &smaller, const Nfa &bigger, const Alphabet *alphabet = nullptr, Run *cex = nullptr)

Inclusion implemented by antichain algorithms.

Parameters:

• smaller – [in] Automaton which language should be included in the bigger one

• bigger – [in] Automaton which language should include the smaller one

• alphabet – [in] Alphabet of both automata (not needed for antichain algorithm)

• cex – [out] A potential counterexample word which breaks inclusion

Returns:

True if smaller language is included, i.e., if the final intersection of smaller complement of bigger is empty.

bool is_universal_naive(const Nfa &aut, const Alphabet &alphabet, Run *cex)

Check universality by checking the emptiness of a complement of aut.

Parameters:

• aut – [in] Automaton which universality is checked

• alphabet – [in] Alphabet of the automaton

• cex – [out] Counterexample word which eventually breaks the universality

Returns:

True if the complemented automaton has non-empty language, i.e., the original one is not universal

bool is_universal_antichains(const Nfa &aut, const Alphabet &alphabet, Run *cex)

check universality based on subset construction with antichains.

Parameters:

• aut – [in] Automaton which universality is checked

• alphabet – [in] Alphabet of the automaton

• cex – [out] Counterexample word which eventually breaks the universality

Returns:

True if the automaton is universal, otherwise false.

Simlib::Util::BinaryRelation compute_relation(const Nfa &aut, const ParameterMap &params = {{"relation", "simulation"}, {"direction", "forward"}})

Nfa product(const Nfa &lhs, const Nfa &rhs, const std::function<bool(State, State)> &&final_condition, Symbol first_epsilon = EPSILON, std::unordered_map<std::pair<State, State>, State> *product_map = nullptr)

Compute product of two NFAs, final condition is to be specified, with a possibility of using multiple epsilons.

Parameters:

• lhs – [in] First NFA to compute intersection for.

• rhs – [in] Second NFA to compute intersection for.

• first_epsilon – [in] The smallest epsilon.

• final_condition – [in] The predicate that tells whether a pair of states is final (conjunction for intersection).

• product_map – [out] Can be used to get the mapping of the pairs of the original states to product states. Mostly useless, it is only filled in and returned if !=nullptr, but the algorithm internally uses another data structures, because this one is too slow.

Returns:

NFA as a product of NFAs lhs and rhs with ε-transitions preserved.

Nfa concatenate_eps(const Nfa &lhs, const Nfa &rhs, const Symbol &epsilon, bool use_epsilon = false, StateRenaming *lhs_state_renaming = nullptr, StateRenaming *rhs_state_renaming = nullptr)

Concatenate two NFAs.

Supports epsilon symbols when use_epsilon is set to true.

Parameters:

• lhs – [in] First automaton to concatenate.

• rhs – [in] Second automaton to concatenate.

• epsilon – [in] Epsilon to be used for concatenation (provided use_epsilon is true)

• use_epsilon – [in] Whether to concatenate over epsilon symbol.

• lhs_state_renaming – [out] Map mapping lhs states to result states.

• rhs_state_renaming – [out] Map mapping rhs states to result states.

Returns:

Concatenated automaton.

Nfa reduce_simulation(const Nfa &nfa, StateRenaming &state_renaming)

Reduce NFA using (forward) simulation.

Parameters:

• nfa – [in] NFA to reduce

• state_renaming – [out] Map mapping original states to the reduced states.

Nfa reduce_residual(const Nfa &nfa, StateRenaming &state_renaming, const std::string &type, const std::string &direction)

Reduce NFA using residual construction.

Parameters:

• nfa – [in] NFA to reduce.

• state_renaming – [out] Map mapping original states to the reduced states.

• type – [in] Type of the residual construction (values: “after”, “with”).

• direction – [in] Direction of the residual construction (values: “forward”, “backward”).

Nfa reduce_residual_with(const Nfa &nfa)

Reduce NFA using residual construction.

The residual construction of the residual automaton and the removal of the covering states is done during the last determinization.

Similar performance to reduce_residual_after(). The output is almost the same except the transitions: transitions may slightly differ, but the number of states is the same for both algorithm types.

Nfa reduce_residual_after(const Nfa &nfa)

Reduce NFA using residual construction.

The residual construction of the residual automaton and the removal of the covering states is done after the final determinization.

Similar performance to reduce_residual_with(). The output is almost the same except the transitions: transitions may slightly differ, but the number of states is the same for both algorithm types.

Plumbing

Wrappers around various support functions.

Simplified NFA API, used in binding to call NFA algorithms.

In particular, this mostly includes operations and checks, that do not return Automaton, but instead take resulting automaton as pointer (e.g. void f(Nfa* result, const Nfa& lhs, const Nfa& rhs)).

namespace mata

Main namespace including structs and algorithms for all automata.

In particular, this includes:

1. Alphabets,

2. Formula graphs and nodes,

3. Mintermization,

4. Closed sets.

namespace nfa

namespace plumbing

Wrappers around various support functions.

Functions

inline void get_elements(StateSet *element_set, const BoolVector &bool_vec)

inline void complement(Nfa *result, const Nfa &aut, const Alphabet &alphabet, const ParameterMap &params = {{"algorithm", "classical"}, {"minimize", "false"}})

inline void minimize(Nfa *res, const Nfa &aut, const ParameterMap &params = {{"algorithm", "brzozowski"}})

inline void determinize(Nfa *result, const Nfa &aut, std::unordered_map<StateSet, State> *subset_map = nullptr)

inline void reduce(Nfa *result, const Nfa &aut, StateRenaming *state_renaming = nullptr, const ParameterMap &params = {{"algorithm", "simulation"}})

inline void revert(Nfa *result, const Nfa &aut)

inline void remove_epsilon(Nfa *result, const Nfa &aut, const Symbol epsilon = EPSILON)

template<class ParsedObject>
void construct(Nfa *result, const ParsedObject &parsed, Alphabet *alphabet = nullptr, NameStateMap *state_map = nullptr)

Loads an automaton from Parsed object.

inline void union_nondet(Nfa *union_automaton, const Nfa &lhs, const Nfa &rhs)

inline void intersection(Nfa *res, const Nfa &lhs, const Nfa &rhs, const Symbol first_epsilon = EPSILON, std::unordered_map<std::pair<State, State>, State> *prod_map = nullptr)

Compute intersection of two NFAs.

Both automata can contain ε-transitions. The product preserves the ε-transitions, i.e., for each each product state (s, t) withs -ε-> p, (s, t) -ε-> (p, t) is created, and vice versa.

Automata must share alphabets.

Parameters:

• res – [out] The resulting intersection NFA.

• lhs – [in] Input NFA.

• rhs – [in] Input NFA.

• first_epsilon – [in] smallest epsilon.

• prod_map – [out] Mapping of pairs of the original states (lhs_state, rhs_state) to new product states (not used internally, allocated only when !=nullptr, expensive).

Returns:

NFA as a product of NFAs lhs and rhs with ε-transitions preserved.

inline void concatenate(Nfa *res, const Nfa &lhs, const Nfa &rhs, const bool use_epsilon = false, StateRenaming *lhs_result_state_renaming = nullptr, StateRenaming *rhs_result_state_renaming = nullptr)

Concatenate two NFAs.

Parameters:

• lhs_result_state_renaming – [out] Map mapping lhs states to result states.

• rhs_result_state_renaming – [out] Map mapping rhs states to result states.

inline void reduce_residual_with(Nfa *res, const Nfa &nfa)

Reduce NFA using residual construction.

The residual construction of the residual automaton and the removal of the covering states is done during the last determinization.

Similar performance to reduce_residual_after(). The output is almost the same except the transitions: transitions may slightly differ, but the number of states is the same for both algorithm types.

inline void reduce_residual_after(Nfa *res, const Nfa &nfa)

Reduce NFA using residual construction.

The residual construction of the residual automaton and the removal of the covering states is done after the final determinization.

Similar performance to reduce_residual_with(). The output is almost the same except the transitions: transitions may slightly differ, but the number of states is the same for both algorithm types.