Namespace mata::nft::algorithms

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:

1. Complementation,

2. Inclusion,

3. Universality checking,

4. Intersection/concatenation with epsilon transitions, or,

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