Namespace mata::nft::plumbing

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.