File mintermization.hh

namespace mata

Main namespace including structs and algorithms for all automata.

In particular, this includes:

1. Alphabets,

2. Formula graphs and nodes,

3. Mintermization,

4. Closed sets.

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

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

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

inline Mintermization()

Private Types

using DisjunctStatesPair = std::pair<const FormulaGraph*, const FormulaGraph*>

Private Functions

void trans_to_bdd_nfa(const IntermediateAut &aut)

void trans_to_bdd_afa(const IntermediateAut &aut)

Private Members

Cudd bdd_mng = {}

std::unordered_map<std::string, BDD> symbol_to_bddvar = {}

std::unordered_map<const FormulaGraph*, BDD> trans_to_bddvar = {}

std::unordered_map<const FormulaNode*, std::vector<DisjunctStatesPair>> lhs_to_disjuncts_and_states = {}

std::unordered_set<BDD> bdds = {}

struct OptionalBdd

Public Types

enum class TYPE

Values:

enumerator NOTHING_E

enumerator BDD_E

Public Functions

OptionalBdd() = default

inline explicit OptionalBdd(TYPE t)

inline explicit OptionalBdd(const BDD &bdd)

inline OptionalBdd(TYPE t, const BDD &bdd)

OptionalBdd operator*(const OptionalBdd &b) const

OptionalBdd operator+(const OptionalBdd &b) const

OptionalBdd operator!() const

Public Members

TYPE type = {}

BDD val = {}