Nondeterministic Finite Transducers¶

page Nondeterministic Finite Transducers (NFTs): The design of NFTs in Mata¶

The classical transducers from textbook definitions (where a transition is a tuple of (initial state, input symbol, final state, output string)) are encoded using a simpler data structure for the transition relation, mata::nft::Delta The data structures can directly represent only transitions of the form p -a-> s where a is a single symbol or epsilon. A “high-level” transitions of the form p -abc/def-> q where ‘abc’ is an input word and def is an output word are encoded as a sequence of these ‘low level’ transitions: p -a- p’ -d-> q -b-> q -e-> r -c-> r’ -f-> s (odd transitions read letters of the input track, even transitions read letters of the output track, a transition can have epsilon instead of a letter). The primed states are a sort of internal states, to where the automaton gets after reading a letter on the input tape (in Mata called level). States are distinguished by their “level”. “Normal” states p,q,r,s have level 0, the internal states p’,q’,r’ have in this case the levels 1 (and you could have n-tape transducers where level can be larger than 1). In Mata, the mata::nft::Delta interface is used only for the manual handling of the internal delta representation, taking only (initial state, input symbol, final state) We find it useful to think about NFTs in Mata as normal NFAs with a single symbol on a transition (because Mata uses the same underlying data structure for NFTs as for NFAs) where states are annotated with levels. The ‘NFT states are the states with levels 0, the other levels are for the internal states. Each NFT transition is a sequence of NFA transitions, one per tape, between two states with levels 0. Each NFA transition performs a single symbol read on the tape of the source state. A sequence of symbols on transitions is not a single word on any tape, but an interleaved description of a single NFT transition over multiple tapes, e.g., q1(l:0)-{a}->q2(l:1)-{b}->q3(l:2)-{c}->q4(l:0) (where (l:X) describes the level of the state) is a single ‘NFT’ transition (from a state with level 0 to another state with level 0) where the NFT symbol read is a 3-tape symbol (‘a’, ‘b’, ‘c’), interpreted as ‘read ‘a’ on tape 0, read ‘b’ on tape 1, and read ‘c’ on tape 2.’ When you want to read ‘af’ on a single tape, you need to construct two such transitions where on the remaining tapes, you read an epsilon symbol.

Working with NFTs¶

There are some utility functions to simplify creating this NFA-like Delta data structure for NFTs such as mata::nft::Nft::insert_word() (inserting the NFA-like sequence of transitions on different tapes: ‘abcd’ which means to read ‘ac’ on tape 0 and ‘bd’ on tape 1), and mata::nft::Nft::insert_word_by_levels() (inserting word for each tape separately: {‘ac’, ‘bd’} to achieve the same as in the previous). If you however want precise control over the created transitions, you can omit using the utility NFT functions and build your NFT like an NFA using the Nft::Delta::* operations directly, adding a single symbol on a single tape per add() call. You will have to correctly specify the levels for the states. When working with 2-tape NFTs modelling a replace operation, we use mata::applications::strings::replace namespace with utility functions such as mata::applications::strings::replace::replace_reluctant_regex() (accepting parameters: regex as the input for the tape 0, and a word as a replacement on tape 1), etc. The notion of jumps (in the jump mode RepeatSymbol, a mode designed for NFTs) is just an optimization to reduce the size of the NFT. It is an approach to simplify the data structure for NFTs where you can say that you jump over several internal states and NFA-like transitions to up to the next state with level 0, each transition in the sequence reading the same single symbol of the jump. That is useful when, for example, having a NFT reading string ‘abc’ on all tapes. You can encode it as a sequence of jumps between states with level 0 as q0(l:0)-{a}->q1(l:0)-{b}->q2(l:0)-{c}->q3(l:0). Notice that the internal states are not present, but they are implied by the jump. Ideally, one should not even have to think about the levels and the intermediate states when properly using the utility functions (from the mata::nft::Nft class and the mata::nft namespace in general).

Representing words in NFTs¶

When working with NFTs, words on multiple levels need to be represented. We consider an NFT word with n levels as a vector of words of type mata::Word, where the word at index i in the vector represents the word on the level i. Operations on NFT words either work on each level separately (named with _by_levels suffix) or on the interleaved representation of the NFT word. E.g., the NFT word representing reading ‘abc’ on level 0 and ‘def’ on level 1 can be represented as either std::vector<Word>{ Word{ ‘a, ‘b’, ‘c }, Word{ ‘d’, ‘e’, ‘f’ } } (using the _by_levels variant) or as a word Word{ ‘a’, ‘d’, ‘b’, ‘e’, ‘c’, ‘f’ }` (using the interleaved representation). Words may contain DONT_CARE (representing wildcards on the respective level, but not EPSILON) and EPSILON (representing reading an empty string on the respective level ).

See also

examples/nft.cc example.

Warning

Mata provides an experimental (unstable) support for (non-)deterministic finite transducers (NFTs). The provided interface may change.

Note

If you find some expected NFT operation or utility function missing, do not hesitate to let us know and we will implement it. The interface for NFTs is not stable yet, so we are open to any and all feedback.

Types¶

Basic types used in the mata::nft module for NFTs.

namespace mata

Main namespace including structs and algorithms for all automata.

In particular, this includes:

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

namespace nft

Typedefs

using Level = unsigned

using State = nfa::State

using StateSet = nfa::StateSet

using Run = nfa::Run

using EpsilonClosureOpt = nfa::EpsilonClosureOpt

using StateRenaming = 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.

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}

class Levels : private std::vector<Level>

#include <types.hh>

Public Functions

inline explicit Levels(const size_t num_of_levels, std::vector<Level> levels = {})¶

Levels() = default¶

Levels(size_t num_of_levels, size_t count, Level value = DEFAULT_LEVEL)¶

Levels(size_t num_of_levels, std::initializer_list<Level> levels)¶

Levels(size_t num_of_levels, iterator first, iterator last)¶

Levels(const Levels &other) = default¶

Levels(Levels &&other) = default¶

Levels &operator=(const Levels &other) = default¶

Levels &operator=(Levels &&other) = default¶

Levels &operator=(std::initializer_list<value_type> other)

Assign levels from other to this.

After assignment, num_of_levels is set to the minimal number of levels that can accommodate all levels in other.

Parameters:: other – [in] Levels to be assigned.

Levels &operator=(const std::vector<Level> &levels)

Assign levels from levels to this.

After assignment, num_of_levels is set to the minimal number of levels that can accommodate all levels in levels.

Parameters:: levels – [in] Levels to be assigned.

Levels &operator=(std::vector<Level> &&levels)

Assign levels from levels to this.

After assignment, num_of_levels is set to the minimal number of levels that can accommodate all levels in levels.

Parameters:: levels – [in] Levels to be assigned.

std::weak_ordering operator<=>(const Levels &other) const = default¶

bool operator==(const Levels &other) const = default¶

inline bool operator==(const std::vector<Level> &other) const¶

Levels &set(State state, Level level = DEFAULT_LEVEL)

Set level of state to level.

If state is out of range, resize this to accommodate it.

num_of_levels is not changed, in contrast to the behaviour of Levels::operator=.

Parameters:

state – [in] State whose level is to be set.
level – [in] Level to be set for state.

Levels &set(const std::vector<Level> &levels)

Set levels of this to levels.

num_of_levels is not changed, in contrast to the behaviour of Levels::operator=.

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

Levels &set(std::vector<Level> &&levels)

Set levels of this to levels.

num_of_levels is not changed, in contrast to the behaviour of Levels::operator=.

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

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.

template<StatesContainerIterable States> inline std::vector<StateSet> map_levels_to(const States &states) const: Get mapping of levels to sets of states from states.

inline Level next_level_after(const Level level) const

Get the next level that should follow after level.

Parameters:: level – The current level.
Returns:: The next level.

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.

inline std::optional<size_t> num_of_levels_used() const¶

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.

static inline std::optional<size_t> num_of_levels_of(const Levels &levels)¶

static inline std::optional<size_t> num_of_levels_of(const std::vector<Level> &levels)¶

static inline std::optional<size_t> num_of_levels_of(const std::initializer_list<Level> levels)¶

Private Types

using super = std::vector<Level>¶

Private Functions

inline bool check_levels_in_range_() const¶

class Ordering

#include <types.hh>

Orderings of levels.

Public Types

using Compare = std::function<bool(Level, Level)>¶

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.

NFT¶

Nondeterministic Finite Transducers including structures, transitions and algorithms.

In particular, this includes:

Structures (Transducer, Transitions, Results, Delta),
Algorithms (operations, checks, tests),
Constructions.

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

namespace mata

Main namespace including structs and algorithms for all automata.

In particular, this includes:

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

namespace nft

Typedefs

template<typename ...Ts> using conjunction = std::is_same<BoolPack<true, Ts::value...>, BoolPack<Ts::value..., true>>: Check that for all values in a pack Ts are ‘true’.

template<typename T, typename ...Ts> using AreAllOfType = conjunction<std::is_same<Ts, T>...>::type: Check that all types in a sequence of parameters Ts are of type T.

Functions

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 complement(const Nft &nft, const Alphabet &alphabet, const ParameterMap &params = {{"algorithm", "classical"}, {"minimize", "false"}})

Compute automaton accepting a complement of nft.

Warning

This function only supports NFTs without epsilon transitions (length-preserving NFTs).

Parameters:

nft – [in] Automaton whose complement to compute.
alphabet – [in] Alphabet used for complementation.
params – [in] Optional parameters to control the complementation algorithm:
- ”algorithm”: “classical” (classical algorithm determinizes the automaton, makes it complete and swaps final and non-final states);
- ”minimize”: (TODO: unimplemented) “true”/”false” (whether to compute minimal deterministic automaton for classical algorithm);

Returns:

Complemented automaton.

Nft complement(const Nft &nft, const utils::OrdVector<Symbol> &symbols, const ParameterMap &params = {{"algorithm", "classical"}, {"minimize", "false"}})

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

Warning

This function only supports NFTs without epsilon transitions (length-preserving NFTs).

Parameters:

nft – [in] Automaton whose complement to compute.
symbols – [in] Symbols to complement over.
params – [in] Optional parameters to control the complementation algorithm:
- ”algorithm”: “classical” (classical algorithm determinizes the automaton, makes it complete and swaps final and non-final states);
- ”minimize”: (TODO: unimplemented) “true”/”false” (whether to compute minimal deterministic automaton for classical algorithm);

Returns:

Complemented 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, const 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 jump_mode = 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.

bool symbols_match(Symbol a, Symbol b)

Check whether two symbols match.

Two symbols match if they are equal (‘a == ‘a’; also EPSILON == EPSILON`), or if at least one of them is DONT_CARE and the other is not EPSILON.

Parameters:

a – First symbol to compare.
b – Second symbol to compare.

Returns:

true if the symbols match, false otherwise.

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

Pack of bools for reasoning about a sequence of parameters.

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 Nft(Nft &&other) noexcept

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

Nft &operator=(Nft &&other) noexcept

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.

Nft &operator=(const Nfa &other) noexcept

Nft &operator=(Nfa &&other) noexcept

State add_state()

Add a new (fresh) state to the automaton.

Returns:: The newly created state.

State add_state(State state)

Add state state to 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_levels(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_levels(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 serves 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 serves as both the source and target state.
alphabet – 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 serves 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.

Delta¶

Data structures representing the delta (transition function) of an NFT, mapping states and input symbols to sets of states where a single NFT transition comprises a sequence of (NFA) transitions in mata::nft::Delta.

namespace mata

Main namespace including structs and algorithms for all automata.

In particular, this includes:

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

namespace nft

Typedefs

using Transition = nfa::Transition

using Move = nfa::Move

using SymbolPost = nfa::SymbolPost

using StatePost = nfa::StatePost

using SynchronizedExistentialSymbolPostIterator = nfa::SynchronizedExistentialSymbolPostIterator

using Delta = nfa::Delta

Builder¶

Function to build predefined types of NFTs, to create them from regular expressions, and to load them from files.

namespace mata

Main namespace including structs and algorithms for all automata.

In particular, this includes:

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

namespace nft

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

Algorithms¶

Functions to operate on NFTs, such as inclusion and universality checking, etc.

namespace mata

Main namespace including structs and algorithms for all automata.

In particular, this includes:

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

namespace nft

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 utils::OrdVector<Symbol> &symbols, bool minimize_during_determinization = false)

Complement implemented by determinization, 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
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:

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
jump_mode – [out] 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:

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> *product_map = nullptr, JumpMode jump_mode = JumpMode::RepeatSymbol, State lhs_first_aux_state = Limits::max_state, 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).
product_map – [out] Can be used to get the mapping of the pairs of the original states to product states. Mostly useless, it is only filled in and returned if !=nullptr, but the algorithm internally uses another data structures, because this one is too slow.
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.

Plumbing¶

Wrappers around various support functions.

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

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

namespace mata

Main namespace including structs and algorithms for all automata.

In particular, this includes:

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

namespace nfa

namespace plumbing

Wrappers around various support functions.

Functions

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

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

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

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

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

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

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

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

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

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

Compute intersection of two NFAs.

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

Automata must share alphabets.

Parameters:

res – [out] The resulting intersection NFA.
lhs – [in] Input NFA.
rhs – [in] Input NFA.
first_epsilon – [in] smallest epsilon.
prod_map – [out] Mapping of pairs of the original states (lhs_state, rhs_state) to new product states (not used internally, allocated only when !=nullptr, expensive).

Returns:

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

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

Concatenate two NFAs.

Parameters:

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

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

Reduce NFA using residual construction.

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

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

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

Reduce NFA using residual construction.

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

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

Nondeterministic Finite Transducers¶

The design of NFTs in Mata¶

Working with NFTs¶

Representing words in NFTs¶

Types¶

NFT¶

Delta¶

Builder¶

Algorithms¶

Plumbing¶

Mata

Navigation

Related Topics