mcrl2::pbes_system::pbesbddsolve¶
Include file:
#include "mcrl2/pbes/pbesbddsolve1.h
-
class
mcrl2::pbes_system::pbesbddsolve¶
Private attributes¶
-
bdd_granularity
mcrl2::pbes_system::pbesbddsolve::m_granularity¶
-
const srf_pbes &
mcrl2::pbes_system::pbesbddsolve::m_pbes¶
-
pbes_equation_index
mcrl2::pbes_system::pbesbddsolve::m_pbes_index¶
-
utilities::execution_timer *
mcrl2::pbes_system::pbesbddsolve::m_timer¶
-
bool
mcrl2::pbes_system::pbesbddsolve::m_unary_encoding¶
-
variable_manager
mcrl2::pbes_system::pbesbddsolve::m_variable_manager¶
Private member functions¶
-
std::vector<bdd>
compute_edge_relation(const std::vector<srf_equation> &equations, const std::vector<bdd> &equation_ids, const std::vector<bdd> &equation_ids_next, const std::vector<bdd> ¶meters_next) const¶
-
std::vector<data::variable>
compute_id_variables(std::size_t n, bool unary_encoding)
-
bdd
compute_initial_state(const std::vector<bdd> &ids) const¶
-
std::vector<bdd>
compute_nodes(std::size_t equation_count, const std::vector<bdd> &id_variables, bool unary_encoding)¶
-
std::tuple<bdd, bdd, bdd, bdd_substitution, bdd_substitution, bdd, std::vector<bdd>, bdd, bdd, bdd, std::map<std::uint32_t, bdd>>
compute_parity_game()
-
std::map<std::size_t, std::vector<bdd>>
compute_priority_map(const std::vector<bdd> &equation_ids) const¶
-
void
finish_timer(const std::string &msg) const
-
std::vector<bdd>
make_bdd_variables(const std::vector<data::variable> &v)
-
bdd
parameter_updates(const std::vector<bdd> ¶meters, const std::vector<bdd> &values) const¶
-
void
start_timer(const std::string &msg) const
-
bdd
to_bdd(const data::data_expression &x) const
-
std::vector<bdd>
to_bdd(const data::data_expression_list &v) const
-
bdd
to_bdd(const data::variable &x) const
-
std::vector<bdd>
to_bdd(const data::variable_list &v) const
-
std::vector<bdd>
to_bdd(const std::vector<data::variable> &v) const
