Namespace mata¶

namespace mata

Main namespace including structs and algorithms for all automata.

In particular, this includes:

Alphabets,
Formula graphs and nodes,
Mintermization,
Closed sets.

Typedefs

using Symbol = unsigned

using Word = std::vector<Symbol>

using WordName = std::vector<std::string>

template<typename T> using OrdVec = mata::utils::OrdVector<T>

Enums

enum class ClosedSetType

Values:

enumerator upward_closed_set

enumerator downward_closed_set

Functions

Word encode_word_utf8(const Word &word)

Encode a word using UTF-8 encoding.

Parameters:: word – [in] The word to encode.
Returns:: The UTF-8 encoded word.

Word decode_word_utf8(const Word &word)

Decode a word using UTF-8 encoding.

Parameters:: word – [in] The word to decode.
Returns:: The UTF-8 decoded word.

template<typename T> std::ostream &operator<<(std::ostream &os, const ClosedSet<T> &cs)

Variables

unsigned LOG_VERBOSITY: log verbosity

const std::string g_GIT_SHA1: git sha

class Alphabet

#include <alphabet.hh>

The abstract interface for NFA alphabets.

Subclassed by EnumAlphabet, IntAlphabet, OnTheFlyAlphabet

Public Functions

virtual Symbol translate_symb(const std::string &symb) = 0: translates a string into a symbol

inline virtual Word translate_word(const WordName &word_name) const: Translate sequence of symbol names to sequence of their respective values.

virtual std::string reverse_translate_symbol(Symbol symbol) const = 0

Translate internal symbol representation back to its original string name.

Throws an exception when the symbol is missing in the alphabet.

Parameters:: symbol – [in] Symbol to translate.
Returns:: symbol original name.

inline Symbol operator[](const std::string &symb): also translates strings to symbols

inline virtual utils::OrdVector<Symbol> get_alphabet_symbols() const

Get a set of all symbols in the alphabet.

The result does not have to equal the list of symbols in the automaton using this alphabet.

inline virtual utils::OrdVector<Symbol> get_complement(const utils::OrdVector<Symbol> &symbols) const: complement of a set of symbols wrt the alphabet

inline virtual bool is_equal(const Alphabet &other_alphabet) const

Check whether two alphabets are equal.

In general, two alphabets are equal if and only if they are of the same class instance.

Parameters:: other_alphabet – The other alphabet to compare with for equality.
Returns:: True if equal, false otherwise.

inline virtual bool is_equal(const Alphabet *const other_alphabet) const

Check whether two alphabets are equal.

In general, two alphabets are equal if and only if they are of the same class instance.

Parameters:: other_alphabet – The other alphabet to compare with for equality.
Returns:: True if equal, false otherwise.

virtual bool empty() const = 0: Checks whether the alphabet has any symbols.

class BoolVector : public std::vector<uint8_t>

#include <utils.hh>

Representation of bool vector by a vector of uint8_t.

Public Functions

inline size_t count() const: Count the number of set elements.

template<typename T> struct ClosedSet

#include <closed-set.hh>

Closed set.

Contains discrete range borders, its type and the corresponding anti-chain. It is necessary to be able to evaluate relation operators <, <=, >, >=, ==, != over instances of this datatype T.

Template Parameters:: T – Datatype the closed set contains.

Public Functions

bool operator==(const ClosedSet<T> &rhs) const = default: Two closed sets are equivalent iff their type, borders and corresponding antichains are the same. They are not equivalent otherwise.

bool contains(const Node &node) const

This function decides whether a set of elements is part of the closed set by subset-compraring the input with all elements of the antichain.

decides whether the closed set contains a given element

Parameters:: node – a given ordered vector of elements of the type T
Returns:: true iff the given ordered vector belongs to the current closed set

bool contains(const Nodes &nodes) const

This function decides whether a set of sets of elements is a part of the closed set by subset-compraring the input with all elements of the antichain.

decides whether the closed set contains a given set of sets of elements

Parameters:: nodes – a given ordered vector of ordered vectors of elements of the type T
Returns:: true iff the given ordered vector of ordered vectors belongs to the current closed set

bool in_interval(const Node &node) const

This function decides whether a given ordered vector of elements of the datatype T belongs to the discrete interval of the current closed set.

decides whether the given vector respects the borders

Parameters:: node – a given ordered vector of elements of the type T which will be inspected
Returns:: true iff the given ordered vector respects the borders

void insert(const Node &node)

Adds a new element to the closed set.

If the element is already contained in the closed set, the closed set remains unchanged. Otherwise, the antichain will be recomputed.

inserts a new element to the closed set

Parameters:: node – a given node which will be added to the closed set

ClosedSet set_union(const ClosedSet &rhs) const

Performs an union over two closed sets with the same type and carrier.

This function simply adds all the elements of the antichain of the first closed set to the second closed set

performs an union over closed sets

Parameters:: rhs – a given closed set which will be unioned with the current one
Returns:: an union of the given closed sets

ClosedSet intersection(const ClosedSet &rhs) const

Performs an intersection over two closed sets with the same type and carrier.

performs an intersection over closed sets

Parameters:: rhs – a given closed set which will be intersectioned with the current one
Returns:: an intersection of the given closed sets

ClosedSet complement() const

Performs a complementation over a closed set.

The result will contain nodes which are not elements of the former closed set. The complement of an upward-closed set is always downward-closed and vice versa.

performs a complementation over a closed set

Returns:: a complement of a closed set

class EnumAlphabet : public Alphabet

#include <alphabet.hh>

Enumerated alphabet using a set of integers as symbols maintaining a set of specified symbols.

EnumAlphabet is a version of direct (identity) alphabet (does not give names to symbols, their name is their integer value directly). However, unlike IntAlphabet, EnumAlphabet maintains an ordered set of symbols in the alphabet.

Therefore, calling member functions get_complement() and get_alphabet_symbols() makes sense in the context of EnumAlphabet and the functions give the expected results.

Example:

Alphabet alph{ EnumAlphabet{ 0, 4, 6, 8, 9 } };
CHECK(alph.translate_symb("6") == 6);
CHECK_THROWS(alph.translate_symb("5")); // Throws an exception about an unknown symbol.
CHECK(alph.get_complement({ utils::OrdVector<Symbol>{ 0, 6, 9 } }) == utils::OrdVector<Symbol>{ 4, 8 });

Public Functions

inline virtual utils::OrdVector<Symbol> get_alphabet_symbols() const override

Get a set of all symbols in the alphabet.

The result does not have to equal the list of symbols in the automaton using this alphabet.

inline virtual utils::OrdVector<Symbol> get_complement(const utils::OrdVector<Symbol> &symbols) const override: complement of a set of symbols wrt the alphabet

virtual std::string reverse_translate_symbol(Symbol symbol) const override

Translate internal symbol representation back to its original string name.

Throws an exception when the symbol is missing in the alphabet.

Parameters:: symbol – [in] Symbol to translate.
Returns:: symbol original name.

inline void add_symbols_from(const mata::utils::OrdVector<Symbol> &symbols)

Expand alphabet by symbols from the passed symbols.

Adding a symbol name which already exists will throw an exception.

Parameters:: symbols – [in] Vector of symbols to add.

inline void add_symbols_from(const EnumAlphabet &alphabet)

Expand alphabet by symbols from the passed alphabet.

Parameters:: symbols_to_add – [in] Vector of symbols to add.

virtual Symbol translate_symb(const std::string &str) override: translates a string into a symbol

virtual Word translate_word(const WordName &word_name) const override: Translate sequence of symbol names to sequence of their respective values.

void add_new_symbol(const std::string &symbol)

Add new symbol to the alphabet with the value identical to its string representation.

Parameters:: symbol – [in] User-space representation of the symbol.
Returns:: Result of the insertion as InsertionResult.

void add_new_symbol(Symbol symbol)

Add new symbol to the alphabet.

Parameters:

key – [in] User-space representation of the symbol.
symbol – [in] Number of the symbol to be used on transitions.

Returns:

Result of the insertion as InsertionResult.

inline Symbol get_next_value() const

Get the next value for a potential new symbol.

Returns:: Next Symbol value.

inline size_t get_number_of_symbols() const

Get the number of existing symbols, epsilon symbols excluded.

Returns:: The number of symbols.

inline virtual bool empty() const override: Checks whether the alphabet has any symbols.

void update_next_symbol_value(Symbol value)

Update next symbol value when appropriate.

When the newly inserted value is larger or equal to the current next symbol value, update the next symbol value to a value one larger than the new value.

Parameters:: value – The value of the newly added symbol.

size_t erase(const Symbol symbol)

Erase a symbol from the alphabet.

Returns:: Number of symbols erased (0 or 1).

inline void erase(utils::OrdVector<Symbol>::const_iterator pos)

Remove a symbol name value pair from the position pos from the alphabet.

Returns:: Iterator following the last removed element.

inline void erase(utils::OrdVector<Symbol>::const_iterator first, utils::OrdVector<Symbol>::const_iterator last)

Remove a symbol name value pair from the positions between first and last from the alphabet.

Returns:: Iterator following the last removed element.

inline Symbol operator[](const std::string &symb): also translates strings to symbols

inline virtual bool is_equal(const Alphabet &other_alphabet) const

Check whether two alphabets are equal.

In general, two alphabets are equal if and only if they are of the same class instance.

Parameters:: other_alphabet – The other alphabet to compare with for equality.
Returns:: True if equal, false otherwise.

inline virtual bool is_equal(const Alphabet *const other_alphabet) const

Check whether two alphabets are equal.

In general, two alphabets are equal if and only if they are of the same class instance.

Parameters:: other_alphabet – The other alphabet to compare with for equality.
Returns:: True if equal, false otherwise.

class FormulaGraph

#include <inter-aut.hh>

Structure representing a transition formula using a graph.

A node of graph consists of node itself and set of children nodes. Nodes are operators and operands of the formula. E.g., a formula q1 & s1 will be transformed to a tree with & as a root node and q1 and s2 being children nodes of the root.

struct FormulaNode

#include <inter-aut.hh>

A node of graph representing transition formula.

A node could be operator (!,&,|) or operand (symbol, state, node). Each node has a name (in case of marking naming, an initial character defining type of node is removed and stored in name), raw (name including potential type marker), and information about its type.

Public Members

Type type: Define whether a node is operand or operator.

std::string raw: Raw name of node as it was specified in input text, i.e., including type marker.

std::string name: Parsed name, i.e., a potential type marker (first character) is removed.

OperatorType operator_type: if a node is operator, it defines which one

OperandType operand_type: if a node is operand, it defines which one

class IntAlphabet : public Alphabet

#include <alphabet.hh>

Direct alphabet (also identity alphabet or integer alphabet) using integers as symbols.

This alphabet presumes that all integers are valid symbols. Therefore, calling member functions get_complement() and get_alphabet_symbols() makes no sense in this context and the methods will throw exceptions warning about the inappropriate use of IntAlphabet. If one needs these functions, they should use OnTheFlyAlphabet instead of IntAlphabet.

Public Functions

virtual Symbol translate_symb(const std::string &symb) override: translates a string into a symbol

inline virtual std::string reverse_translate_symbol(Symbol symbol) const override

Translate internal symbol representation back to its original string name.

Throws an exception when the symbol is missing in the alphabet.

Parameters:: symbol – [in] Symbol to translate.
Returns:: symbol original name.

inline virtual utils::OrdVector<Symbol> get_alphabet_symbols() const override

Get a set of all symbols in the alphabet.

The result does not have to equal the list of symbols in the automaton using this alphabet.

inline virtual utils::OrdVector<Symbol> get_complement(const utils::OrdVector<Symbol> &symbols) const override: complement of a set of symbols wrt the alphabet

inline virtual bool empty() const override: Checks whether the alphabet has any symbols.

inline virtual Word translate_word(const WordName &word_name) const: Translate sequence of symbol names to sequence of their respective values.

inline Symbol operator[](const std::string &symb): also translates strings to symbols

inline virtual bool is_equal(const Alphabet &other_alphabet) const

Check whether two alphabets are equal.

In general, two alphabets are equal if and only if they are of the same class instance.

Parameters:: other_alphabet – The other alphabet to compare with for equality.
Returns:: True if equal, false otherwise.

inline virtual bool is_equal(const Alphabet *const other_alphabet) const

Check whether two alphabets are equal.

In general, two alphabets are equal if and only if they are of the same class instance.

Parameters:: other_alphabet – The other alphabet to compare with for equality.
Returns:: True if equal, false otherwise.

class IntermediateAut

#include <inter-aut.hh>

Structure for a general intermediate representation of parsed automaton.

It contains information about type of automata, type of naming of nodes, symbols and states and type of alphabet. It contains also the transitions formula and formula for initial and final states. The formulas are represented as tree where nodes are either operands or operators.

Public Types

enum class AutomatonType

Type of automaton.

So far we support nondeterministic finite automata (NFA) and alternating finite automata (AFA)

Values:

enumerator NFA

enumerator AFA

enumerator NFT

enum class Naming

The possible kinds of naming of items in sets of states, nodes, or symbols.

It implies how the given set is defined. Naming could be automatic (all things in formula not belonging to other sets will be assigned to a set with automatic naming), marker based (everything beginning with q is a state, with s is a symbol, with n is a node), or enumerated (the given set is defined by enumeration). There are two special cases used for alphabet - symbols could be any character (CHARS) or anything from utf (UTF).

Values:

enumerator AUTO

enumerator MARKED

enumerator ENUM

enumerator CHARS

enumerator UTF

enum class AlphabetType

Type of alphabet.

We can have explicit alphabet (containing explicit symbols), or bitvector, or class of symbols (e.g., alphabet is everything in utf), or intervals. So far, only explicit representation is supported.

Values:

enumerator EXPLICIT

enumerator BITVECTOR

enumerator CLASS

enumerator INTERVALS

Public Functions

const FormulaGraph &get_symbol_part_of_transition(const std::pair<FormulaNode, FormulaGraph> &trans) const

Returns symbolic part of transition.

That may be just a symbol or bitvector formula. This function is supported only for NFA where transitions have a rhs state at the end of right handed side of transition.

Parameters:: transition – Transition from which symbol is returned
Returns:: Graph representing symbol. It maybe just an explicit symbol or graph representing bitvector formula

std::unordered_set<std::string> get_positive_finals() const

Method returns a set of final states in the case that they were entered as a conjunction of negated states.

It collects all negated states and subtracts them from set of all states.

Public Static Functions

static std::vector<IntermediateAut> parse_from_mf(const mata::parser::Parsed &parsed)

A method for building a vector of IntermediateAut for a parsed input.

For each section in input is created one IntermediateAut. It parses basic information about type of automata, its naming conventions etc. Then it parses input and final formula of automaton. Finally, transition formulas are transformed to graph representation by turning an input stream of tokens to postfix notation and then a tree representing the formula is built from it.

Parameters:: parsed – Parsed input in MATA format.
Returns:: A vector of InterAutomata from each section in parsed input.

struct transitions: #include <inter-aut.hh>

Transitions are pairs where the first member is left-hand side of transition (i.e., a state) and the second item is a graph representing transition formula (which can contain symbols, nodes, and states).

class Mintermization

#include <mintermization.hh>

Public Functions

std::unordered_set<BDD> compute_minterms(const std::unordered_set<BDD> &source_bdds)

Takes a set of BDDs and build a minterm tree over it.

The leaves of BDDs, which are minterms of input set, are returned

Parameters:: source_bdds – BDDs for which minterms are computed
Returns:: Computed minterms

BDD graph_to_bdd_nfa(const FormulaGraph &graph)

Transforms a graph representing formula at transition to bdd.

Parameters:: graph – Graph to be transformed
Returns:: Resulting BDD

OptionalBdd graph_to_bdd_afa(const FormulaGraph &graph)

Transforms a graph representing formula at transition to bdd.

This version of method is a more general one and accepts also formula including states.

Parameters:: graph – Graph to be transformed
Returns:: Resulting BDD

mata::IntermediateAut mintermize(const mata::IntermediateAut &aut)

Method mintermizes given automaton which has bitvector alphabet.

It transforms its transitions to BDDs, then build a minterm tree over the BDDs and finally transforms automaton to explicit one.

Parameters:: aut – Automaton to be mintermized.
Returns:: Mintermized automaton

std::vector<mata::IntermediateAut> mintermize(const std::vector<const mata::IntermediateAut*> &auts)

Methods mintermize given automata which have bitvector alphabet.

It transforms transitions of all automata to BDDs, then build a minterm tree over the BDDs and finally transforms automata to explicit one (sharing the same minterms).

Parameters:: auts – Automata to be mintermized.
Returns:: Mintermized automata corresponding to the input autamata

void minterms_to_aut_nfa(mata::IntermediateAut &res, const mata::IntermediateAut &aut, const std::unordered_set<BDD> &minterms)

The method performs the mintermization over @aut with given @minterms.

It is method specialized for NFA.

Parameters:

res – The resulting mintermized automaton
aut – Automaton to be mintermized
minterms – Set of minterms for mintermization

void minterms_to_aut_afa(mata::IntermediateAut &res, const mata::IntermediateAut &aut, const std::unordered_set<BDD> &minterms)

The method for mintermization of alternating finite automaton using a given set of minterms.

Parameters:

res – The resulting mintermized automaton
aut – Automaton to be mintermized
minterms – Set of minterms for mintermization

class OnTheFlyAlphabet : public Alphabet

#include <alphabet.hh>

An alphabet constructed ‘on the fly’.

Should be use anytime the automata have a specific names for the symbols.

Public Types

using InsertionResult = std::pair<StringToSymbolMap::const_iterator, bool>: Result of the insertion of a new symbol.

Public Functions

inline explicit OnTheFlyAlphabet(const std::vector<std::string> &symbol_names, Symbol init_symbol = 0)

Create alphabet from a list of symbol names.

Parameters:

symbol_names – Names for symbols on transitions.
init_symbol – Start of a sequence of values to use for new symbols.

virtual utils::OrdVector<Symbol> get_alphabet_symbols() const override

Get a set of all symbols in the alphabet.

The result does not have to equal the list of symbols in the automaton using this alphabet.

virtual utils::OrdVector<Symbol> get_complement(const utils::OrdVector<Symbol> &symbols) const override: complement of a set of symbols wrt the alphabet

virtual std::string reverse_translate_symbol(Symbol symbol) const override

Translate internal symbol representation back to its original string name.

Throws an exception when the symbol is missing in the alphabet.

Parameters:: symbol – [in] Symbol to translate.
Returns:: symbol original name.

void add_symbols_from(const std::vector<std::string> &symbol_names)

Expand alphabet by symbols from the passed symbol_names.

Adding a symbol name which already exists will throw an exception.

Parameters:: symbol_names – [in] Vector of symbol names.

void add_symbols_from(const StringToSymbolMap &new_symbol_map)

Expand alphabet by symbols from the passed symbol_map.

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

Parameters:: new_symbol_map – [in] Map of strings to symbols.

virtual Symbol translate_symb(const std::string &str) override: translates a string into a symbol

virtual Word translate_word(const WordName &word_name) const override: Translate sequence of symbol names to sequence of their respective values.

InsertionResult add_new_symbol(const std::string &key)

Add new symbol to the alphabet with the value of next_symbol_value.

Throws an exception when the adding fails.

Parameters:: key – [in] User-space representation of the symbol.
Returns:: Result of the insertion as InsertionResult.

InsertionResult add_new_symbol(const std::string &key, Symbol value)

Add new symbol to the alphabet.

Throws an exception when the adding fails.

Parameters:

key – [in] User-space representation of the symbol.
value – [in] Number of the symbol to be used on transitions.

Returns:

Result of the insertion as InsertionResult.

inline InsertionResult try_add_new_symbol(const std::string &key, Symbol value)

Try to add symbol to the alphabet map.

Does not throw an exception when the adding fails.

Parameters:

key – [in] User-space representation of the symbol.
value – [in] Number of the symbol to be used on transitions.

Returns:

Result of the insertion as InsertionResult.

inline Symbol get_next_value() const

Get the next value for a potential new symbol.

Returns:: Next Symbol value.

inline size_t get_number_of_symbols() const

Get the number of existing symbols, epsilon symbols excluded.

Returns:: The number of symbols.

inline const StringToSymbolMap &get_symbol_map() const

Get the symbol map used in the alphabet.

Returns:: Map mapping strings to symbols used internally in Mata.

inline virtual bool empty() const override: Checks whether the alphabet has any symbols.

void update_next_symbol_value(Symbol value)

Update next symbol value when appropriate.

When the newly inserted value is larger or equal to the current next symbol value, update the next symbol value to a value one larger than the new value.

Parameters:: value – The value of the newly added symbol.

size_t erase(Symbol symbol)

Remove a symbol name value pair specified by its symbol from the alphabet.

Warning

Complexity: O(n), where n is the number of symbols in the alphabet.

Returns:: Number of symbols removed (0 or 1).

size_t erase(const std::string &symbol_name)

Remove a symbol name value pair specified by its symbol_name from the alphabet.

Returns:: Number of symbols removed (0 or 1).

inline void erase(StringToSymbolMap::const_iterator pos): Remove a symbol name value pair from the position pos from the alphabet.

inline void erase(StringToSymbolMap::const_iterator first, StringToSymbolMap::const_iterator last): Remove a symbol name value pair from the positions between first and last from the alphabet.

inline Symbol operator[](const std::string &symb): also translates strings to symbols

inline virtual bool is_equal(const Alphabet &other_alphabet) const

Check whether two alphabets are equal.

In general, two alphabets are equal if and only if they are of the same class instance.

Parameters:: other_alphabet – The other alphabet to compare with for equality.
Returns:: True if equal, false otherwise.

inline virtual bool is_equal(const Alphabet *const other_alphabet) const

Check whether two alphabets are equal.

In general, two alphabets are equal if and only if they are of the same class instance.

Parameters:: other_alphabet – The other alphabet to compare with for equality.
Returns:: True if equal, false otherwise.

namespace applications

namespace strings

Operations on NFAs/NFTs used for string constraint solving.

Typedefs

using Nfa = nfa::Nfa

using State = nfa::State

using StateSet = nfa::StateSet

using Transition = nfa::Transition

using ParameterMap = nfa::ParameterMap

using SymbolPost = nfa::SymbolPost

using Nft = nft::Nft

Functions

std::set<Word> get_shortest_words(const Nfa &nfa)

Get shortest words (regarding their length) of the automaton using BFS.

Returns:: Set of shortest words.

std::optional<std::vector<Word>> get_words_of_lengths(const Nft &nft, std::vector<unsigned> lengths)

Get the accepting words for each tape of nft with specific lengths.

This function finds such an accepting word of nft that for each tape i, the word on this tape (on the ith index of resulting vector) has the length lengths[i].

Parameters:

nft – Transducer whose accepting words we are looking for
lengths – The lengths of the words of each tape (size of lengths == the levels of nft)

Returns:

std::optional<std::vector<Word>> Either the resulting words of tapes, or std::nullopt if such words of specific lengths do not exist

std::set<Symbol> get_accepted_symbols(const Nfa &nfa): Get all the one symbol words accepted by nfa.

std::set<std::pair<int, int>> get_word_lengths(const Nfa &aut)

Get the lengths of all words in the automaton aut.

The function returns a set of pairs <u,v> where for each such a pair there is a word with length u+k*v for all ks. The disjunction of such formulae of all pairs hence precisely describe lengths of all words in the automaton.

Parameters:: aut – Input automaton
Returns:: Set of pairs describing lengths

bool is_lang_eps(const Nfa &nfa)

Checks if the automaton nfa accepts only a single word \eps.

Parameters:: nfa – Input automaton
Returns:: true iff L(nfa) = {\eps}

class ShortestWordsMap

#include <strings.hh>

Class mapping states to the shortest words accepted by languages of the states.

Public Functions

inline explicit ShortestWordsMap(const Nfa &aut)

Maps states in the automaton aut to shortest words accepted by languages of the states.

Parameters:: aut – Automaton to compute shortest words for.

std::set<Word> get_shortest_words_from(const StateSet &states) const

Gets shortest words for the given states.

Parameters:: states – [in] States to map shortest words for.
Returns:: Set of shortest words.

std::set<Word> get_shortest_words_from(State state) const

Gets shortest words for the given state.

Parameters:: state – [in] State to map shortest words for.
Returns:: Set of shortest words.

namespace replace

Enums

enum class ReplaceMode

How many occurrences of the regex to replace, in order from left to right?

Values:

enumerator Single: Replace only the first occurrence of the regex.

enumerator All: Replace all occurrences of the regex.

Functions

Nfa reluctant_nfa(Nfa nfa)

Modify nfa in-place to remove outgoing transitions from final states.

If nfa accepts empty string, returned NFA will accept only the empty string.

Parameters:: nfa – NFA to modify.
Returns:: The reluctant version of nfa.

Nft create_identity(Alphabet const *const alphabet, size_t num_of_levels = 2): Create identity transducer over the alphabet with num_of_levels levels.

Nft create_identity_with_single_symbol_replace(Alphabet const *const alphabet, Symbol from_symbol, Symbol replacement, ReplaceMode replace_mode = ReplaceMode::All): Create identity input/output transducer with 2 levels over the alphabet with level_cnt levels with single symbol from_symbol replaced with @to_symbol.

Nft create_identity_with_single_symbol_replace(Alphabet const *const alphabet, Symbol from_symbol, const Word &replacement, ReplaceMode replace_mode = ReplaceMode::All): Create identity input/output transducer with 2 levels over the alphabet with level_cnt levels with single symbol from_symbol replaced with word replacement.

Nft replace_reluctant_regex(const std::string &regex, const Word &replacement, Alphabet const *const alphabet, ReplaceMode replace_mode = ReplaceMode::All, Symbol begin_marker = BEGIN_MARKER)

Create NFT modelling a reluctant leftmost replace of regex regex to replacement.

The most general replace operation, handling any regex as the part to be replaced.

Parameters:

regex – A string containing regex to be replaced.
replacement – Literal to be replaced with.
alphabet – Alphabet over which to create the NFT.
replace_mode – Whether to replace all or just the single (the leftmost) occurrence of regex.
begin_marker – Symbol to be used internally as a begin marker of replaced regex.

Returns:

The reluctant leftmost replace NFT.

Nft replace_reluctant_regex(nfa::Nfa aut, const Word &replacement, Alphabet const *const alphabet, ReplaceMode replace_mode = ReplaceMode::All, Symbol begin_marker = BEGIN_MARKER)

Create NFT modelling a reluctant leftmost replace of regex represented by deterministic automaton aut to replacement.

The most general replace operation, handling any regex as the part to be replaced.

Parameters:

aut – deterministic automaton representing regex to be replaced.
replacement – Literal to replace with.
alphabet – Alphabet over which to create the NFT.
replace_mode – Whether to replace all or just the single (the leftmost) occurrence of regex.
begin_marker – Symbol to be used internally as a begin marker of replaced regex.

Returns:

The reluctant leftmost replace NFT.

Nft replace_reluctant_literal(const Word &literal, const Word &replacement, Alphabet const *const alphabet, ReplaceMode replace_mode = ReplaceMode::All, Symbol end_marker = END_MARKER)

Create NFT modelling a reluctant leftmost replace of literal literal to replacement.

Parameters:

literal – Literal to replace.
replacement – Literal to replace with.
alphabet – Alphabet over which to create the NFT.
replace_mode – Whether to replace all or just the single (the leftmost) occurrence of literal.
end_marker – Symbol to be used internally as an end marker marking the end of the replaced literal.

Returns:

The reluctant leftmost replace NFT.

Nft replace_reluctant_single_symbol(Symbol from_symbol, Symbol replacement, Alphabet const *const alphabet, ReplaceMode replace_mode = ReplaceMode::All)

Create NFT modelling a reluctant leftmost replace of symbol from_symbol to replacement.

Parameters:

from_symbol – Symbol to replace.
replacement – Symbol to replace with.
alphabet – Alphabet over which to create the NFT.
replace_mode – Whether to replace all or just the single (the leftmost) occurrence of from_symbol.

Returns:

The reluctant leftmost replace NFT.

Nft replace_reluctant_single_symbol(Symbol from_symbol, const Word &replacement, Alphabet const *const alphabet, ReplaceMode replace_mode = ReplaceMode::All)

Create NFT modelling a reluctant leftmost replace of symbol from_symbol to replacement.

Parameters:

from_symbol – Symbol to replace.
replacement – Literal to replace with.
alphabet – Alphabet over which to create the NFT.
replace_mode – Whether to replace all or just the single (the leftmost) occurrence of from_symbol.

Returns:

The reluctant leftmost replace NFT.

Variables

Symbol BEGIN_MARKER = {mata::nft::EPSILON - 100}: Marker marking the beginning of the regex to be replaced.

Symbol END_MARKER = {mata::nft::EPSILON - 99}: Marker marking the end of the regex to be replaced.

class ReluctantReplace

#include <strings.hh>

Implementation of all reluctant replace versions.

Public Static Functions

static Nft replace_regex(nfa::Nfa aut, const Word &replacement, Alphabet const *const alphabet, ReplaceMode replace_mode = ReplaceMode::All, Symbol begin_marker = BEGIN_MARKER)

Create NFT modelling a reluctant leftmost replace of regex represented by deterministic automaton aut to replacement.

The most general replace operation, handling any regex as the part to be replaced.

Parameters:

aut – Deterministic automaton representing regex to be replaced.
replacement – Literal to replace with.
alphabet – Alphabet over which to create the NFT.
replace_mode – Whether to replace all or just the single (the leftmost) occurrence of regex.
begin_marker – Symbol to be used internally as a begin marker of replaced regex.

Returns:

The reluctant leftmost replace NFT.

static Nft replace_literal(const Word &literal, const Word &replacement, Alphabet const *const alphabet, ReplaceMode replace_mode = ReplaceMode::All, Symbol end_marker = END_MARKER)

Create NFT modelling a reluctant leftmost replace of literal literal to replacement.

Parameters:

literal – Literal to replace.
replacement – Literal to replace with.
alphabet – Alphabet over which to create the NFT.
replace_mode – Whether to replace all or just the single (the leftmost) occurrence of literal.
end_marker – Symbol to be used internally as an end marker marking the end of the replaced literal.

Returns:

The reluctant leftmost replace NFT.

static Nft replace_symbol(Symbol from_symbol, Symbol replacement, Alphabet const *const alphabet, ReplaceMode replace_mode = ReplaceMode::All)

Create NFT modelling a reluctant leftmost replace of symbol from_symbol to replacement.

Parameters:

from_symbol – Symbol to replace.
replacement – Symbol to replace with.
alphabet – Alphabet over which to create the NFT.
replace_mode – Whether to replace all or just the single (the leftmost) occurrence of from_symbol.

Returns:

The reluctant leftmost replace NFT.

static Nft replace_symbol(Symbol from_symbol, const Word &replacement, Alphabet const *const alphabet, ReplaceMode replace_mode = ReplaceMode::All)

Create NFT modelling a reluctant leftmost replace of symbol from_symbol to replacement.

Parameters:

from_symbol – Symbol to replace.
replacement – Literal to replace with.
alphabet – Alphabet over which to create the NFT.
replace_mode – Whether to replace all or just the single (the leftmost) occurrence of from_symbol.

Returns:

The reluctant leftmost replace NFT.

namespace seg_nfa

Segment Automata including structs and algorithms.

These are automata whose state space can be split into several segments connected by ε-transitions in a chain. No other ε-transitions are allowed. As a consequence, no ε-transitions can appear in a cycle. Segment automaton can have initial states only in the first segment and final states only in the last segment.

Typedefs

using SegNfa = Nfa

using VisitedEpsMap = std::map<State, std::map<Symbol, unsigned>>

using VisitedEpsilonsCounterMap = std::map<Symbol, unsigned>: Number of visited epsilons.

using VisitedEpsilonsCounterVector = std::vector<unsigned>: Projection of VisitedEpsilonsNumberMap to sorted keys (in descending order).

using Noodle = std::vector<std::shared_ptr<SegNfa>>: A noodle is represented as a sequence of segments (a copy of the segment automata) created as if there was exactly one ε-transition between each two consecutive segments.

using SegmentWithEpsilonsCounter = std::pair<std::shared_ptr<Nfa>, VisitedEpsilonsCounterVector>: Segment with a counter of visited epsilons.

using NoodleWithEpsilonsCounter = std::vector<SegmentWithEpsilonsCounter>: Noodles as segments enriched with EpsCntMap.

using TransducerNoodle = std::vector<TransducerNoodleElement>

Functions

void segs_one_initial_final(const std::vector<Nfa> &segments, bool include_empty, const State &unused_state, std::map<std::pair<State, State>, std::shared_ptr<Nfa>> &out)

segs_one_initial_final

segments_one_initial_final[init, final] is the pointer to automaton created from one of the segments such that init and final are one of the initial and final states of the segment and the created automaton takes this segment, sets initial={init}, final={final} and trims it; also segments_one_initial_final[unused_state, final] is used for the first segment (where we always want all initial states, only final state changes) and segments_one_initial_final[init, unused_state] is similarly for the last segment TODO: should we use unordered_map? then we need hash

std::vector<Noodle> noodlify(const SegNfa &aut, Symbol epsilon, bool include_empty = false)

Create noodles from segment automaton aut.

Segment automaton is a chain of finite automata (segments) connected via ε-transitions. A noodle is a vector of pointers to copy of the segments automata created as if there was exactly one ε-transition between each two consecutive segments.

Parameters:

automaton – [in] Segment automaton to noodlify.
epsilon – [in] Epsilon symbol to noodlify for.
include_empty – [in] Whether to also include empty noodles.

Returns:

A list of all (non-empty) noodles.

std::vector<NoodleWithEpsilonsCounter> noodlify_mult_eps(const SegNfa &aut, const std::set<Symbol> &epsilons, bool include_empty = false)

Create noodles from segment automaton aut.

Segment automaton is a chain of finite automata (segments) connected via ε-transitions. A noodle is a vector of pointers to copy of the segments automata created as if there was exactly one ε-transition between each two consecutive segments.

Parameters:

automaton – [in] Segment automaton to noodlify.
epsilons – [in] Epsilon symbols to noodlify for.
include_empty – [in] Whether to also include empty noodles.

Returns:

A list of all (non-empty) noodles.

std::vector<Noodle> noodlify_for_equation(const std::vector<std::reference_wrapper<Nfa>> &lhs_automata, const Nfa &rhs_automaton, bool include_empty = false, const ParameterMap &params = {{"reduce", "false"}})

Create noodles for left and right side of equation.

Segment automaton is a chain of finite automata (segments) connected via ε-transitions. A noodle is a copy of the segment automaton with exactly one ε-transition between each two consecutive segments.

Mata cannot work with equations, queries etc. Hence, we compute the noodles for the equation, but represent the equation in a way that libMata understands. The left side automata represent the left side of the equation and the right automaton represents the right side of the equation. To create noodles, we need a segment automaton representing the intersection. That can be achieved by computing a product of both sides. First, the left side has to be concatenated over an epsilon transitions into a single automaton to compute the intersection on, though.

Parameters:

lhs_automata – [in] Sequence of segment automata for left side of an equation to noodlify.
rhs_automaton – [in] Segment automaton for right side of an equation to noodlify.
include_empty – [in] Whether to also include empty noodles.
params – [in] Additional parameters for the noodlification:
- ”reduce”: “false”, “forward”, “backward”, “bidirectional”; Execute forward, backward or bidirectional simulation minimization before noodlification.

Returns:

A list of all (non-empty) noodles.

std::vector<Noodle> noodlify_for_equation(const std::vector<Nfa*> &lhs_automata, const Nfa &rhs_automaton, bool include_empty = false, const ParameterMap &params = {{"reduce", "false"}})

Create noodles for left and right side of equation.

Segment automaton is a chain of finite automata (segments) connected via ε-transitions. A noodle is a copy of the segment automaton with exactly one ε-transition between each two consecutive segments.

Mata cannot work with equations, queries etc. Hence, we compute the noodles for the equation, but represent the equation in a way that libMata understands. The left side automata represent the left side of the equation and the right automaton represents the right side of the equation. To create noodles, we need a segment automaton representing the intersection. That can be achieved by computing a product of both sides. First, the left side has to be concatenated over an epsilon transitions into a single automaton to compute the intersection on, though.

Parameters:

lhs_automata – [in] Sequence of pointers to segment automata for left side of an equation to noodlify.
rhs_automaton – [in] Segment automaton for right side of an equation to noodlify.
include_empty – [in] Whether to also include empty noodles.
params – [in] Additional parameters for the noodlification:
- ”reduce”: “false”, “forward”, “backward”, “bidirectional”; Execute forward, backward or bidirectional simulation minimization before noodlification.

Returns:

A list of all (non-empty) noodles.

std::vector<NoodleWithEpsilonsCounter> noodlify_for_equation(const std::vector<std::shared_ptr<Nfa>> &lhs_automata, const std::vector<std::shared_ptr<Nfa>> &rhs_automata, bool include_empty = false, const ParameterMap &params = {{"reduce", "false"}})

Create noodles for left and right side of equation (both sides are given as a sequence of automata).

Parameters:

lhs_automata – [in] Sequence of pointers to segment automata for left side of an equation to noodlify.
rhs_automaton – [in] Sequence of pointers to segment automata for right side of an equation to noodlify.
include_empty – [in] Whether to also include empty noodles.
params – [in] Additional parameters for the noodlification:
- ”reduce”: “false”, “forward”, “backward”, “bidirectional”; Execute forward, backward or bidirectional simulation minimization before noodlification.

Returns:

A list of all (non-empty) noodles together with the positions reached from the beginning of left/right side.

std::vector<TransducerNoodle> noodlify_for_transducer(std::shared_ptr<Nft> nft, const std::vector<std::shared_ptr<Nfa>> &input_automata, const std::vector<std::shared_ptr<Nfa>> &output_automata, bool reduce_intersection = true, bool use_homomorphic_heuristic = true)

VisitedEpsilonsCounterVector process_eps_map(const VisitedEpsilonsCounterMap &eps_cnt)

Process epsilon map to a sequence of values (sorted according to key desc)

Parameters:: eps_cnt – Epsilon count
Returns:: Vector of keys (count of epsilons)

class Segmentation

#include <strings.hh>

Class executing segmentation operations for a given segment automaton.

Works only with segment automata.

Public Types

using EpsilonDepth = size_t: Depth of ε-transitions. Dictionary of lists of ε-transitions grouped by their depth. For each depth ‘i’ we have ‘depths[i]’ which contains a list of ε-transitions of depth ‘i’.

Public Functions

inline explicit Segmentation(const SegNfa &aut, const std::set<Symbol> &epsilons)

Prepare automaton aut for segmentation.

Parameters:

aut – [in] Segment automaton to make segments for.
epsilon – [in] Symbol to execute segmentation for.

inline const EpsilonDepthTransitions &get_epsilon_depths() const

Get segmentation depths for ε-transitions.

Returns:: Map of depths to lists of ε-transitions.

inline const EpsilonDepthTransitionMap &get_epsilon_depth_trans_map() const

Get the epsilon depth trans map object (mapping of depths and states to eps-successors)

Returns:: Map of depths to a map of states to transitions

const std::vector<Nfa> &get_segments()

Get segment automata.

Returns:: A vector of segments for the segment automaton in the order from the left (initial state in segment automaton) to the right (final states of segment automaton).

const std::vector<Nfa> &get_untrimmed_segments()

Get raw segment automata.

Returns:: A vector of segments for the segment automaton in the order from the left (initial state in segment automaton) to the right (final states of segment automaton) without trimming (the states are same as in the original automaton).

struct TransducerNoodleElement: #include <strings.hh>

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 = typename conjunction<std::is_same<Ts, T>...>::type: Check that all types in a sequence of parameters Ts are of type T.

using State = unsigned long¶

using StateSet = mata::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 BEFORE_AND_AFTER¶: 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.

Functions

template<typename ...Nfas, typename = AreAllOfType<const Nfa&, Nfas...>> inline 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&, const 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, 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. //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&, const 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)

Nfa fragile_revert(const Nfa &aut)

Nfa simple_revert(const Nfa &aut)

Nfa somewhat_simple_revert(const Nfa &aut)

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

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 *const shared_alphabet = nullptr)

Get the set of symbols to work with during operations.

Parameters:: 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.

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.

template<bool...> struct bool_pack: #include <nfa.hh>

Pack of bools for reasoning about a sequence of parameters.

class Delta

#include <delta.hh>

Delta is a data structure for representing transition relation.

Transition is represented as a triple Trans(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 Functions

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.

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.

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(const State source, const Symbol symbol, const StateSet &targets)

Add transitions to multiple destinations.

Parameters:

source – From
symbol – Symbol
targets – Set of states to

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.

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.

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.

class Transitions

#include <delta.hh>

Iterator over transitions represented as Transition instances.

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

class const_iterator: #include <delta.hh>

Iterator over transitions.

struct Limits¶: #include <types.hh>

class Move: #include <delta.hh>

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

class Nfa

#include <nfa.hh>

A class representing an NFA.

Subclassed by Nft

Public Functions

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.

Nfa(const Nfa &other) = default: Construct a new explicit NFA from other NFA.

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.

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

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

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())

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.

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.

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

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

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

nfa – [in] NFA with symbols to fill alphabet_to_fill with.
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 &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.

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.

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.

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(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

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.

struct TarjanDiscoverCallback: #include <nfa.hh>

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

struct Run¶

#include <types.hh>

Public Members

Word word = {}¶: A finite-length word.

std::vector<State> path = {}¶: A finite-length path through automaton.

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

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.

inline virtual reference back()

Get reference to the last element in the vector.

Modifying the underlying value in the reference could break sortedness.

inline size_t erase(const SymbolPost &k)

Remove k from sorted vector.

This function expects the vector to be sorted.

Private Functions

inline OrdVector difference(const OrdVector &rhs) const

Compute set difference as this minus rhs.

Parameters:: rhs – Other vector with symbols to be excluded.
Returns:: this minus rhs.

inline bool contains(const SymbolPost &key) const: Check whether key exists in the ordered vector.

Private Static Functions

static inline OrdVector with_reserved(const size_t capacity)

Create OrdVector with reserved capacity.

Parameters:: capacity – [in] Capacity of OrdVector to reserve.
Returns:: Newly create OrdVector.

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(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).

class const_iterator

#include <delta.hh>

Iterator over moves.

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_it_end): Construct iterator from symbol_post_it (including) to symbol_post_it_end (excluding).

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.

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.

inline virtual bool advance() override

Advances all positions just above current_minimum, that is, to or above next_minimum.

Those at next_minimum are added to currently_synchronized. Since next_minimum becomes the current minimum, new next_minimum must be updated too.

inline virtual const std::vector<utils::OrdVector<SymbolPost>::const_iterator> &get_current() const override

Returns the vector of current still active positions.

Beware, they will be ordered differently from how there were input into the iterator. This is due to swapping of the emptied positions with positions at the end.

inline virtual void push_back(const utils::OrdVector<SymbolPost>::const_iterator &begin, const utils::OrdVector<SymbolPost>::const_iterator &end) override

This is supposed to be called only before an iteration, after constructor of reset.

Calling after advance breaks the iterator. Specifies begin and end of one vector, to initialise before the iteration starts.

struct Transition¶

#include <delta.hh>

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

Public Members

State source¶: Source state.

Symbol symbol¶: Transition symbol.

State target¶: Target state.

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.
minimize_during_determinization – [in] Whether the determinized automaton is computed by (brzozowski) minimization.

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)¶

Universality check implemented by checking emptiness of complemented automaton.

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)¶

Universality checking based on subset construction with antichain.

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, const Symbol first_epsilon = EPSILON, std::unordered_map<std::pair<State, State>, State> *prod_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_epsilons – [in] The smallest epsilon.
final_condition – [in] The predicate that tells whether a pair of states is final (conjunction for intersection).
prod_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.

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(const size_t num_of_states, const size_t alphabet_size, const double states_trans_ratio_per_symbol, const 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

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, 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 *unionAutomaton, const Nfa &lhs, const Nfa &rhs)¶

inline void intersection(Nfa *res, 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.

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, 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.

namespace nft

Typedefs

using Transition = mata::nfa::Transition ¶

using Move = mata::nfa::Move ¶

using SymbolPost = mata::nfa::SymbolPost ¶

using StatePost = mata::nfa::StatePost ¶

using SynchronizedExistentialSymbolPostIterator = mata::nfa::SynchronizedExistentialSymbolPostIterator ¶

using Delta = mata::nfa::Delta ¶

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 = typename conjunction<std::is_same<Ts, T>...>::type: Check that all types in a sequence of parameters Ts are of type T.

using Level = unsigned¶

using State = mata::nfa::State ¶

using StateSet = mata::nfa::StateSet ¶

using Run = mata::nfa::Run ¶

using EpsilonClosureOpt = mata::nfa::EpsilonClosureOpt ¶

using StateRenaming = mata::nfa::StateRenaming ¶

using ParameterMap = mata::nfa::ParameterMap ¶

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" }
}

using Limits = mata::nfa::Limits ¶

using ProductFinalStateCondition = mata::nfa::ProductFinalStateCondition ¶

Enums

enum class JumpMode¶

A non-deterministic finite transducer.

Values:

enumerator RepeatSymbol¶: Repeat the symbol on the jump.

enumerator AppendDontCares¶: Append a sequence of DONT_CAREs to the symbol on the jump.

Functions

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

Compute non-deterministic union.

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

Returns:: Non-deterministic union of lhs and rhs.

Nft union_det_complete(const Nft &lhs, const Nft &rhs) = delete

Nft product(const Nft &lhs, const Nft &rhs, ProductFinalStateCondition final_condition, Symbol first_epsilon, std::unordered_map<std::pair<State, State>, State> *prod_map) = delete

Nft intersection(const Nft &lhs, const Nft &rhs, std::unordered_map<std::pair<State, State>, State> *prod_map = nullptr, JumpMode jump_mode = JumpMode::RepeatSymbol, State lhs_first_aux_state = Limits::max_state, State rhs_first_aux_state = Limits::max_state)

Compute intersection of two NFTs.

Both automata can contain ε-transitions. Epsilons will be handled as alphabet symbols.

Automata must share alphabets. //TODO: this is not implemented yet. Transducers must have equal values of num_of_levels.

Parameters:

lhs – [in] First NFT to compute intersection for.
rhs – [in] Second NFT to compute intersection for.
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).
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.
lhs_first_aux_state – [in] The first auxiliary state in lhs. Two auxiliary states does not form a product state.
rhs_first_aux_state – [in] The first auxiliary state in rhs. Two auxiliary states does not form a product state.

Returns:

NFT as a product of NFTs lhs and rhs.

Nft compose(const Nft &lhs, const Nft &rhs, const utils::OrdVector<Level> &lhs_sync_levels, const utils::OrdVector<Level> &rhs_sync_levels, bool project_out_sync_levels = true, JumpMode jump_mode = JumpMode::RepeatSymbol)

Composes two NFTs (lhs || rhs; read as “rhs after lhs”).

This function computes the composition of two NFTs, lhs and rhs, by aligning their synchronization levels. Transitions between two synchronization levels are ordered as follows: first the transitions of lhs, then the transitions of rhs followed by next synchronization level (if exists). By default, synchronization levels are projected out from the resulting NFT.

Vectors of synchronization levels have to be non-empty and of the same size.

Parameters:

lhs – [in] First transducer to compose.
rhs – [in] Second transducer to compose.
lhs_sync_levels – [in] Ordered vector of synchronization levels of the lhs.
rhs_sync_levels – [in] Ordered vector of synchronization levels of the rhs.
project_out_sync_levels – [in] Whether we want to project out the synchronization levels.
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.

Returns:

A new NFT after the composition.

Nft compose(const Nft &lhs, const Nft &rhs, Level lhs_sync_level = 1, Level rhs_sync_level = 0, bool project_out_sync_levels = true, JumpMode jump_mode = JumpMode::RepeatSymbol)

Composes two NFTs (lhs || rhs; read as “rhs after lhs”).

This function computes the composition of two NFTs, lhs and rhs, by aligning their synchronization levels. Transitions between two synchronization levels are ordered as follows: first the transitions of lhs, then the transitions of rhs followed by next synchronization level (if exists). By default, synchronization levels are projected out from the resulting NFT.

Parameters:

lhs – [in] First transducer to compose.
rhs – [in] Second transducer to compose.
lhs_sync_level – [in] The synchronization level of the lhs.
rhs_sync_level – [in] The synchronization level of the rhs.
project_out_sync_levels – [in] Whether we wont to project out the synchronization levels.
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.

Returns:

A new NFT after the composition.

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

Concatenate two NFTs.

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.

Nft determinize(const Nft &nft, std::unordered_map<StateSet, State> *subset_map = nullptr)

Determinize automaton.

Parameters:

nft – [in] Automaton to determinize.
subset_map – [out] Map that maps sets of states of input automaton to states of determinized automaton.

Returns:

Determinized automaton.

Nft reduce(const Nft &aut, StateRenaming *state_renaming = nullptr, const ParameterMap &params = {{"algorithm", "simulation"}})

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”.

Returns:

Reduced automaton.

bool is_included(const Nft &smaller, const Nft &bigger, Run *cex, const Alphabet *alphabet = nullptr, JumpMode jump_mode = JumpMode::RepeatSymbol, const ParameterMap &params = {{"algorithm", "antichains"}})

Checks inclusion of languages of two NFTs: 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 NFTs to compute 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.
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 Nft &smaller, const Nft &bigger, const Alphabet *const alphabet = nullptr, JumpMode jump_mode = JumpMode::RepeatSymbol, const ParameterMap &params = {{"algorithm", "antichains"}})

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

Parameters:

smaller – [in] First automaton to concatenate.
bigger – [in] Second automaton to concatenate.
alphabet – [in] Alphabet of both NFTs to compute 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.
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 Nft &lhs, const Nft &rhs, const Alphabet *alphabet, JumpMode jump_mode = JumpMode::RepeatSymbol, const ParameterMap &params = {{"algorithm", "antichains"}})

Perform equivalence check of two NFTs: lhs and rhs.

Parameters:

lhs – [in] First automaton to concatenate.
rhs – [in] Second automaton to concatenate.
alphabet – [in] Alphabet of both NFTs to compute 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.
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 Nft &lhs, const Nft &rhs, JumpMode JumpMode = JumpMode::RepeatSymbol, const ParameterMap &params = {{"algorithm", "antichains"}})

Perform equivalence check of two NFTs: lhs and rhs.

The current implementation of Nft 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.
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.
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.

Nft revert(const Nft &aut)

Nft fragile_revert(const Nft &aut)

Nft simple_revert(const Nft &aut)

Nft somewhat_simple_revert(const Nft &aut)

Nft invert_levels(const Nft &aut, JumpMode jump_mode = JumpMode::RepeatSymbol)

Inverts the levels of the given transducer aut.

The function inverts the levels of the transducer, i.e., the level 0 becomes the last level, level 1 becomes the second last level, and so on.

Parameters:

aut – [in] The transducer for inverting levels.
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 new transducer with inverted levels.

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

Remove simple epsilon transitions.

Simple epsilon transitions are the transitions of the form q0 -epsilon-> q1 -epsilon-> q2 -epsilon-> … -epsilon-> qn where q0 and qn are level 0 states, the states in-between are states with level 1, 2, …, num_of_levels and for each qi, for 0 < i < n, there is only 1 transition going to qi (the transition qi-1 -epsilon-> qi) and only 1 transition going from qi (the transition qi -epsilon -> qi+1). This means that if there was some state p0 going with epsilon to q1, these to epsilon transitions would not be removed.

Furthermore, this assumes that the NFT aut does not have jump transitions.

The resulting automaton has the same number of states as aut, just the transitions can change. It is recommended to run trim() after this function.

Parameters:

aut – NFT without jump transitions
epsilon – symbol representing epsilon

Returns:

NFT whose language is same as aut but does not contain simple epsilon transitions

Nft project_out(const Nft &nft, const utils::OrdVector<Level> &levels_to_project, JumpMode jump_mode = JumpMode::RepeatSymbol)

Projects out specified levels levels_to_project in the given transducer nft.

Parameters:

nft – [in] The transducer for projection.
levels_to_project – [in] A non-empty ordered vector of levels to be projected out from the transducer. It must contain only values that are greater than or equal to 0 and smaller than num_of_levels.
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 new projected transducer.

Nft project_out(const Nft &nft, Level level_to_project, JumpMode jump_mode = JumpMode::RepeatSymbol)

Projects out specified level level_to_project in the given transducer nft.

Parameters:

nft – [in] The transducer for projection.
level_to_project – [in] A level that is going to be projected out from the transducer. It has to be greater than or equal to 0 and smaller than num_of_levels.
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 new projected transducer.

Nft project_to(const Nft &nft, const utils::OrdVector<Level> &levels_to_project, JumpMode jump_mode = JumpMode::RepeatSymbol)

Projects to specified levels levels_to_project in the given transducer nft.

Parameters:

nft – [in] The transducer for projection.
levels_to_project – [in] A non-empty ordered vector of levels the transducer is going to be projected to. It must contain only values greater than or equal to 0 and smaller than num_of_levels.
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 new projected transducer.

Nft project_to(const Nft &nft, Level level_to_project, JumpMode jump_mode = JumpMode::RepeatSymbol)

Projects to a specified level level_to_project in the given transducer nft.

Parameters:

nft – [in] The transducer for projection.
level_to_project – [in] A level the transducer is going to be projected to. It has to be greater than or equal to 0 and smaller than num_of_levels.
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 new projected transducer.

Nft insert_levels(const Nft &nft, const BoolVector &new_levels_mask, JumpMode jump_mode = JumpMode::RepeatSymbol)

Inserts new levels, as specified by the mask new_levels_mask, into the given transducer nft.

num_of_levels must be greater than 0. The vector new_levels_mask must be nonempty, its length must be greater than num_of_levels, and it must contain exactly num_of_levels occurrences of false.

Parameters:

nft – [in] The original transducer.
new_levels_mask – [in] A mask representing the old and new levels. The vector {1, 0, 1, 1, 0} indicates that one level is inserted before level 0 and two levels are inserted before level 1.
jump_mode – [in] Specifies whether 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 insert_level(const Nft &nft, Level new_level, JumpMode jump_mode = JumpMode::RepeatSymbol)

Inserts a new level new_level into the given transducer nft.

num_of_levels must be greater than 0.

Parameters:

nft – [in] The original transducer.
new_level – [in] Specifies the new level to be inserted into the transducer. If new_level is 0, then it is inserted before the 0-th level. If new_level is less than num_of_levels, then it is inserted before the level new_level-1. If new_level is greater than or equal to num_of_levels, then all levels from num_of_levels through new_level are appended after the last level.
jump_mode – [in] Specifies whether 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.

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.

Variables

const std::string TYPE_NFT¶

Symbol EPSILON = mata::nfa::EPSILON ¶: An epsilon symbol which is now defined as the maximal value of data type used for symbols.

Symbol DONT_CARE = EPSILON - 1¶

Level DEFAULT_LEVEL = {0}¶

Level DEFAULT_NUM_OF_LEVELS = {2}¶

template<bool...> struct bool_pack: #include <nft.hh>

Pack of bools for reasoning about a sequence of parameters.

class Levels : private std::vector<Level>

#include <types.hh>

Public Functions

void append(const Levels &levels_vector)

Append levels_vector to the end of this.

Parameters:: levels_vector – [in] Vector of levels to be appended.

inline size_t count(const Level level) const

Count the number of occurrences of a level in this.

Parameters:: level – [in] Level to be counted.

std::vector<Level> get_levels_of(const utils::SparseSet<State> &states) const: Get levels of states in states.

std::vector<Level> get_levels_of(const StateSet &states) const: Get levels of states in states.

std::optional<Level> get_minimal_level_of(const StateSet &states, Ordering::Compare levels_ordering = Ordering::Minimal) const

Get the minimal level for the states in states.

“Minimal level” is defined as the level with the lowest numerical value, i.e., 0 < 1 < 2 < ... < num_of_levels-1. “Minimal” often relates to the current states (“What is the current state with minimal level?”)

std::optional<Level> get_minimal_next_level_of(const StateSet &states) const

Get the minimal next level for the states in states.

“Minimal next level” is defined as the minimal level in the next transition (that may follow another level), i.e., 1 < 2 < ... < num_of_levels-1 < 0. “Minimal next” relates to the next target states (“What is the next minimal level to target in a transition?”).

bool can_follow_for_states(State source, State target) const

Check whether a transition can be made from source to target.

A transition can be made if the level of target is higher than the level of source, or if the level of target is 0.

Parameters:

source – [in] Source state.
target – [in] Target state.

Returns:

true if the transition can be made, false otherwise.

Public Members

size_t num_of_levels = {DEFAULT_NUM_OF_LEVELS}

Number of levels (tracks) the transducer recognizes.

Each transducer transition will comprise num_of_levels of NFA transitions.

Note

The number of levels has to be at least 1.

Public Static Functions

static bool can_follow(Level source_level, Level target_level)

Check whether a transition can be made from a state with level source_level to a state with level target_level.

A transition can be made if the target level is higher than the source level, or we can always jump to a state with level 0.

Parameters:

source_level – [in] Level of the source state.
target_level – [in] Level of the target state.

Returns:

true if the transition can be made, false otherwise.

class Ordering

#include <types.hh>

Orderings of levels.

Public Static Functions

static inline bool Minimal(const Level lhs, const Level rhs)

Ordering for Levels in NFTs where lower levels precede higher levels.

That is, levels are ordered as follows: 0 < 1 < 2 < … < num_of_levels-1.

static inline bool Next(const Level lhs, const Level rhs)

Ordering for levels in NFTs where lower levels precede higher levels, except for 0 which is the highest level.

That is, levels are ordered as follows: 1 < 2 < … < num_of_levels-1 < 0. This ordering is used when handling intermediate states (with non-zero levels) in NFTs for determining the next lowest level of the next state.

class Nft : public Nfa

#include <nft.hh>

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.

namespace algorithms¶

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

This is a separation of the implementation from the interface defined in mata::nft. Note, that in mata::nft 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.

In particular, this includes algorithms for:

Complementation,
Inclusion,
Universality checking,
Intersection/concatenation with epsilon transitions, or,
Computing relation.

Functions

Nft minimize_brzozowski(const Nft &aut)¶

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

Parameters:: aut – [in] Automaton to be minimized.
Returns:: Minimized automaton.

Nft complement_classical(const Nft &aut, const mata::utils::OrdVector<Symbol> &symbols, bool minimize_during_determinization = false)¶

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.
minimize_during_determinization – [in] Whether the determinized automaton is computed by (brzozowski) minimization.

Returns:

Complemented automaton.

bool is_included_naive(const Nft &smaller, const Nft &bigger, const Alphabet *alphabet = nullptr, Run *cex = nullptr, JumpMode jump_mode = JumpMode::RepeatSymbol)¶

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 Nft &smaller, const Nft &bigger, const Alphabet *alphabet = nullptr, Run *cex = nullptr, JumpMode jump_mode = JumpMode::RepeatSymbol)¶

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 Nft &aut, const Alphabet &alphabet, Run *cex)¶

Universality check implemented by checking emptiness of complemented automaton.

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 Nft &aut, const Alphabet &alphabet, Run *cex)¶

Universality checking based on subset construction with antichain.

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 Nft &aut, const ParameterMap &params = {{"relation", "simulation"}, {"direction", "forward"}})¶

Nft product(const Nft &lhs, const Nft &rhs, const std::function<bool(State, State)> &&final_condition, std::unordered_map<std::pair<State, State>, State> *prod_map = nullptr, JumpMode jump_mode = JumpMode::RepeatSymbol, const State lhs_first_aux_state = Limits::max_state, const State rhs_first_aux_state = Limits::max_state)¶

Compute product of two NFTs, final condition is to be specified.

Parameters:

lhs – [in] First NFT to compute intersection for.
rhs – [in] Second NFT to compute intersection for.
final_condition – [in] The predicate that tells whether a pair of states is final (conjunction for intersection).
prod_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.
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.
lhs_first_aux_state – [in] The first auxiliary state in lhs. Two auxiliary states can not form a product state.
rhs_first_aux_state – [in] The first auxiliary state in rhs. Two auxiliary states con not form a product state.

Returns:

NFT as a product of NFTs lhs and rhs with ε handled as regular symbols.

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

Concatenate two NFTs.

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.

namespace builder¶

Namespace providing options to build NFAs.

Typedefs

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

Functions

Nft create_single_word_nft(const Word &word)¶: Create an automaton accepting only a single word.

Nft create_single_word_nft(const WordName &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 the word symbols. If left empty, a new alphabet with only the symbols of the word will be created.

Nft create_empty_string_nft(size_t num_of_levels = DEFAULT_NUM_OF_LEVELS)¶: Create automaton accepting only epsilon string.

Nft create_sigma_star_nft(size_t num_of_levels = DEFAULT_NUM_OF_LEVELS)¶

Create automaton accepting sigma star over the passed alphabet using DONT_CARE symbol.

Parameters:: num_of_levels – [in] Number of levels in the created NFT.

Nft create_sigma_star_nft(const Alphabet *alphabet = new OnTheFlyAlphabet{}, size_t num_of_levels = DEFAULT_NUM_OF_LEVELS)¶

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.
num_of_levels – [in] Number of levels in the created NFT.

Nft construct(const parser::ParsedSection &parsec, Alphabet *alphabet, NameStateMap *state_map = nullptr)¶: Loads an automaton from Parsed object.

Nft construct(const IntermediateAut &inter_aut, Alphabet *alphabet, NameStateMap *state_map = nullptr)¶: Loads an automaton from Parsed object.

void construct(Nft *result, const IntermediateAut &inter_aut, Alphabet *alphabet, NameStateMap *state_map = nullptr)¶: Loads an automaton from Parsed object; version for python binding.

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

Nft parse_from_mata(std::istream &nft_stream)¶

Parse NFA from the mata format in an input stream.

Parameters:: nft_stream – Input stream containing NFA in mata format.
Throws:: std::runtime_error – Parsing of NFA fails.

Nft parse_from_mata(const std::string &nft_in_mata)¶

Parse NFA from the mata format in a string.

Parameters:: nft_in_mata – String containing NFA in mata format.
Throws:: std::runtime_error – Parsing of NFA fails.

Nft parse_from_mata(const std::filesystem::path &nft_file)¶

Parse NFA from the mata format in a file.

Parameters:

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

Throws:

std::runtime_error – nft_file does not exist.
std::runtime_error – Parsing of NFA fails.

Nft from_nfa_with_levels_zero(const nfa::Nfa &nfa, size_t num_of_levels = DEFAULT_NUM_OF_LEVELS, bool explicit_transitions = true, std::optional<Symbol> next_levels_symbol = {})¶

Create Nft from nfa with specified num_of_levels.

This function takes transition from nfa as transitions between zero level and the first level of NFT. All transition between the remaining levels are created based on the function parameters: explicit_transitions and next_levels_symbol.

Parameters:

nfa – NFA to create NFT from.
num_of_levels – Number of levels of NFT.
explicit_transitions – If true, the transitions between levels are explicit (i.e., no jump transitions, except for the epsilon transitions over all levels).)
next_levels_symbol – If specified, it is used as a symbol on transitions after the first level. If not specified, the symbol of the transition is reused.

Returns:

NFT representing nfa with num_of_levels number of levels.

Nft from_nfa_with_levels_advancing(mata::nfa::Nfa nfa, size_t num_of_levels)¶

Creates Nft from nfa with specified num_of_levels automatically.

It assumes that nfa is a representation of an nft without jump transitions. It assign to each state the level based on the distance from the initial state. For example, if there are 2 levels, the initial states are level 0, the successor states are level 1, the states after that level 0, etc.

If you only have one level, then it is more efficient to call the constructor that takes Nfa as input.

Throws:: std::runtime_error – if some state should be assigned two different levels or if the final state is not at level 0.

namespace plumbing¶

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(Nft* result, const Nft& lhs, const Nft& rhs)).

Functions

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

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

inline void minimize(Nft *res, const Nft &aut)¶

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

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

inline void revert(Nft *result, const Nft &aut)¶

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

template<class ParsedObject> void construct(Nft *result, const ParsedObject &parsed, Alphabet *alphabet = nullptr, NameStateMap *state_map = nullptr)¶: Loads an automaton from Parsed object.

inline void union_nondet(Nft *unionAutomaton, const Nft &lhs, const Nft &rhs)¶

inline void intersection(Nft *res, const Nft &lhs, const Nft &rhs, std::unordered_map<std::pair<State, State>, State> *prod_map = nullptr, const JumpMode jump_mode = JumpMode::RepeatSymbol, const State lhs_first_aux_state = Limits::max_state, const State rhs_first_aux_state = Limits::max_state)¶

Compute intersection of two NFTs.

Both automata can contain ε-transitions. Epsilons will be handled as alphabet symbols.

Transducers must share alphabets. //TODO: this is not implemented yet. Transducers must have equal values of num_of_levels.

Parameters:

lhs – [in] First NFT to compute intersection for.
rhs – [in] Second NFT to compute intersection for.
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).
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
lhs_first_aux_state – [in] The first auxiliary state in lhs. Two auxiliary states does not form a product state.
rhs_first_aux_state – [in] The first auxiliary state in rhs. Two auxiliary states does not form a product state.

Returns:

NFT as a product of NFTs lhs and rhs.

inline void concatenate(Nft *res, const Nft &lhs, const Nft &rhs, 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.

namespace parser

Parser from .mata format to automata (currently Nfa and Afa are supported).

This includes parsing either from files or from other streams (strings, etc.).

Typedefs

using KeyListStore = std::map<std::string, std::vector<std::string>>

using BodyLine = std::vector<std::string>

using Parsed = std::vector<ParsedSection>: Parsed data.

Functions

Parsed parse_mf(const std::string &input, bool keepQuotes = false): Parses a string into an intermediary structure.

Parsed parse_mf(std::istream &input, bool keepQuotes = false): Parses a stream into an intermediary structure.

ParsedSection parse_mf_section(std::istream &input, bool keepQuotes = false): Parses one section from a stream into an intermediary structure.

ParsedSection parse_mf_section(const std::string &input, bool keepQuotes = false): Parses one section from a string into an intermediary structure.

void init(): registers dispatcher

nfa::Nfa create_nfa(const std::string &pattern, bool use_epsilon = false, mata::Symbol epsilon_value = 306, bool use_reduce = true, const Encoding encoding = Encoding::Latin1)

Creates NFA from regular expression using RE2 parser.

At https://github.com/google/re2/wiki/Syntax, you can find the syntax of regular expressions with following futher limitations: 1) If you use UTF8 encoding, the created NFA will have the values of bytes instead of full symbols. For example, the character Ā whose Unicode code point is U+0100 and is represented in UTF8 as two bytes c4 80 will have two transitions, one with c4 followed with by 80, to encode it. 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.

See also

mata::nfa::builder::create_from_regex()

Parameters:

pattern – regex as a string
use_epsilon – whether to keep epsilon transitions in created NFA
epsilon_value – symbol representing epsilon
use_reduce – if set to true the result is trimmed and reduced using simulation reduction
encoding – encoding of the regex, default is Latin1

Returns:

Nfa corresponding to pattern

void create_nfa(nfa::Nfa *nfa, const std::string &pattern, bool use_epsilon = false, mata::Symbol epsilon_value = 306, bool use_reduce = true, const Encoding encoding = Encoding::Latin1)

struct ParsedSection

#include <parser.hh>

Parsed data (single section)

Public Functions

inline bool empty() const: Is the section empty?

bool operator==(const ParsedSection &rhs) const: Equality operator.

const std::vector<std::string> &operator[](const std::string &key) const: subscript operator for the key-value store

inline bool haskey(const std::string &key) const: check whether the key-value store contains a key

namespace utils

SparseSet.h Implements a class template of a sparse set of unsigned integers.

Non-automata-related structures and algorithms.

In particular, this includes:

Predicates,
Ordered Vectors,
Iterators,
Printers,
Other helper functions.

Author: Sam Griffiths www.computist.xyz https://gist.github.com/sjgriffiths/06732c6076b9db8a7cf4dfe3a7aed43a

Functions

template<class T> bool are_disjoint(const utils::OrdVector<T> &lhs, const utils::OrdVector<T> &rhs)

template<class Key> bool is_sorted(const std::vector<Key> &vec)

template<class Container> void push_back(SynchronizedIterator<typename Container::const_iterator> &i, const Container &container)

In order to make initialisation of the sync.

iterator nicer than inputting v.begin() and v.end() as the two parameters of the method push_back, this function wraps the method push_back, takes the iterator and v and extracts the v.begin() and v.end() from v.

inline std::string replace_all(const std::string &input, const std::string &needle, const std::string &replace)

Replace all occurrences of a substring in a string.

Parameters:

input – The input string
needle – The substring to be replaced
replace – The replacement string

Returns:

A new string with all occurrences of the substring replaced.

template<class T> bool are_disjoint(const std::set<T> &lhs, const std::set<T> &rhs): Are two sets disjoint?

template<class T, class Cont> bool is_in(const T &elem, const Cont &cont): Is there an element in a container?

template<class T> inline size_t hash_combine(size_t lhs, const T &rhs)

Combine two hash values.

Values taken from http://www.boost.org/doc/libs/1_64_0/boost/functional/hash/hash.hpp

TODO: fix to be more suitable for 64b

template<typename It> size_t hash_range(It first, It last)

Hashes a range.

Inspired by http://www.boost.org/doc/libs/1_64_0/boost/functional/hash/hash.hpp

template<class T, class K> inline bool haskey(const T &cont, const K &key): checks whether a container with find contains a key

template<template<class, class, class...> class Map, class T1, class T2, class ...Args> Map<T2, T1> invert_map(const Map<T1, T2> &mp): inverts a map (should work for std::map and std::unordered_map)

template<class Vector> inline void reserve_on_insert(Vector &vec, size_t needed_capacity = 0, size_t extension = 32)

template<class Vector, typename Index> void defragment(Vector &vec, const std::vector<Index> &renaming)

template<class Vector, typename Index> void rename(Vector &vec, const std::vector<Index> &renaming)

template<class Vector, typename Fun> void filter_indexes(Vector &vec, const Fun &&is_staying)

template<class Vector, typename Fun> void filter(Vector &vec, const Fun &&is_staying)

template<class Vector> inline void sort_and_rmdupl(Vector &vec)

template<class Key> class OrdVector

#include <ord-vector.hh>

Implementation of a set using ordered vector.

This class implements the interface of a set (the same interface as std::set) using ordered vector as the underlying data structure.

Template Parameters:: Key – Key type: type of the elements contained in the container. Each elements in a set is also its key.

Public Functions

inline OrdVector difference(const OrdVector &rhs) const

Compute set difference as this minus rhs.

Parameters:: rhs – Other vector with symbols to be excluded.
Returns:: this minus rhs.

inline bool contains(const Key &key) const: Check whether key exists in the ordered vector.

inline size_t erase(const Key &k)

Remove k from sorted vector.

This function expects the vector to be sorted.

inline virtual reference back()

Get reference to the last element in the vector.

Modifying the underlying value in the reference could break sortedness.

Public Static Functions

static inline OrdVector with_reserved(const size_t capacity)

Create OrdVector with reserved capacity.

Parameters:: capacity – [in] Capacity of OrdVector to reserve.
Returns:: Newly create OrdVector.

Friends

inline friend std::ostream &operator<<(std::ostream &os, const OrdVector &vec)

Overloaded << operator.

Overloaded << operator for output stream.

See also

to_str()

Parameters:

os – [in] The output stream
vec – [in] Assignment to the variables

Returns:

Modified output stream

template<typename Number> class SparseSet

#include <sparse-set.hh>

Implementation of a set of non-negative numbers using sparse-set.

This class implements the interface of a set (similar to std::set) using sparse-set date structure, that is, a pair of vectors dense and sparse (… google it). Importantly

Insertion and removal are constant time.
Iteration is linear in the number of stored elements.
It takes a lot of space, the sparse and dense vectors allocate as many indexes as the maximal stored number.

Template Parameters:: Number – Number type: type of numbers contained in the container.

Public Functions

inline void erase_nocheck(const Number number)

Erase number from the set without checking for its existence.

Parameters:: number – Number to be erased.
Pre:: number exists in the set.

SparseSet() = default: New Mata code.

inline explicit SparseSet(Number domain_size): Basic constructor where you may reserve a domain size.

inline bool operator[](Number q) const

Returns:: True if predicate for q is set. False otherwise (even if q is out of range of the predicate).

inline Number max()

Maximal Number in set.

Expensive operation as it has to compute the maximal Number in linear time.

template<typename Iterator> class SynchronizedExistentialIterator : public mata::utils::SynchronizedIterator<Iterator>

#include <synchronized-iterator.hh>

Public Functions

inline virtual bool advance() override

Advances all positions just above current_minimum, that is, to or above next_minimum.

Those at next_minimum are added to currently_synchronized. Since next_minimum becomes the current minimum, new next_minimum must be updated too.

inline virtual const std::vector<Iterator> &get_current() const override

Returns the vector of current still active positions.

Beware, they will be ordered differently from how there were input into the iterator. This is due to swapping of the emptied positions with positions at the end.

inline virtual void push_back(const Iterator &begin, const Iterator &end) override

This is supposed to be called only before an iteration, after constructor of reset.

Calling after advance breaks the iterator. Specifies begin and end of one vector, to initialise before the iteration starts.

template<typename Iterator> class SynchronizedIterator

#include <synchronized-iterator.hh>

Synchronized iteration.

Subclassed by SynchronizedExistentialIterator< Iterator >, SynchronizedUniversalIterator< Iterator >

Public Functions

inline explicit SynchronizedIterator(const size_t size = 0)

Parameters:: size – Number of elements to reserve up-front for positions and ends.

inline virtual void push_back(const Iterator &begin, const Iterator &end)

This is supposed to be called only before an iteration, after constructor of reset.

Calling after advance breaks the iterator. Specifies begin and end of one vector, to initialise before the iteration starts.

inline void reset(const size_t size = 0)

Empties positions and ends.

Though they should keep the allocated space.

Parameters:: size – Number of elements to reserve up-front for positions and ends.

template<typename Iterator> class SynchronizedUniversalIterator : public mata::utils::SynchronizedIterator<Iterator>

#include <synchronized-iterator.hh>

Public Functions

inline virtual bool advance()

Advances all positions to the NEXT minimum and returns true (though the next minimum might be the current state if synchronized_at_current_minimum is false), or returns false if positions cannot be synchronized.

If positions are synchronized to start with, then synchronized_at_current_minimum decides whether to stay or advance further. The general of the algorithm is to synchronize everybody with position[0].

inline virtual const std::vector<Iterator> &get_current() const: Returns the vector of current positions.

inline virtual void push_back(const Iterator &begin, const Iterator &end)

This is supposed to be called only before an iteration, after constructor of reset.

Calling after advance breaks the iterator. Specifies begin and end of one vector, to initialise before the iteration starts.

Public Members

bool synchronized_at_current_minimum = false

“minimum” would be the smallest class bounded from below by all positions that appears in all OrdContainers.

Are we sure that all positions at this class? Invariant: it can be true only if all positions are indeed synchronized.

template<class Tuple, size_t N> struct TuplePrinter: #include <utils.hh>

template<class Tuple> struct TuplePrinter<Tuple, 1>: #include <utils.hh>

template<typename T, bool track_inverted = true, size_t MAX_MATRIX_SIZE = 50'000'000> class TwoDimensionalMap

#include <two-dimensional-map.hh>

A two-dimensional map that can be used to store pairs of values and their associated value.

This class can handle both small and large maps efficiently.

The largest matrix of pairs of we are brave enough to allocate is 50’000’000 for 8 Byte values. So ten million cells is close to 100 MB. If the number is larger, then we do not allocate a matrix, but use a vector of unordered maps (vec_map_storage). The unordered_map seems to be about twice slower.

Template Parameters:

T – Type of the values stored in the map. Must be an unsigned type.
track_inverted – Whether to track inverted indices for the first and second dimensions. To use this feature correctly, the mapping has to be reversible.
MAX_MATRIX_SIZE – Maximum size of the matrix before switching to vector of unordered maps.

Public Functions

inline TwoDimensionalMap(const size_t first_dim_size, const size_t second_dim_size)

Constructor for TwoDimensionalMap.

Parameters:

first_dim_size – Size of the first dimension.
second_dim_size – Size of the second dimension.

inline T get(const T first, const T second) const

Get the value associated with a pair of keys.

Parameters:

first – First key.
second – Second key.

Returns:

The value associated with the pair, or std::numeric_limits<T>::max() if not found.

inline void insert(const T first, const T second, const T value)

Insert a value associated with a pair of keys.

Parameters:

first – First key.
second – Second key.
value – Value to associate with the pair.

inline T get_first_inverted(const T value) const

Get the first inverted index for a value.

This is only available if track_inverted is true.

inline T get_second_inverted(const T value) const

Get the second inverted index for a value.

This is only available if track_inverted is true.

Namespace mata¶

Mata

Navigation

Related Topics