mcrl2::pbes_system::bdd::pbesbddsolve

Include file:

#include "mcrl2/pbes/pbesbddsolve.h
class mcrl2::pbes_system::bdd::pbesbddsolve

Public types

type mcrl2::pbes_system::bdd::pbesbddsolve::bdd_substitution

typedef for bdd_sylvan::bdd_substitution

type mcrl2::pbes_system::bdd::pbesbddsolve::bdd_type

typedef for bdd_sylvan::bdd_type

type mcrl2::pbes_system::bdd::pbesbddsolve::bdd_variable_set

typedef for bdd_sylvan::bdd_variable_set

Private attributes

bdd_sylvan mcrl2::pbes_system::bdd::pbesbddsolve::m_bdd
bdd_granularity mcrl2::pbes_system::bdd::pbesbddsolve::m_granularity
const srf_pbes &mcrl2::pbes_system::bdd::pbesbddsolve::m_pbes
pbes_equation_index mcrl2::pbes_system::bdd::pbesbddsolve::m_pbes_index
utilities::execution_timer *mcrl2::pbes_system::bdd::pbesbddsolve::m_timer
bool mcrl2::pbes_system::bdd::pbesbddsolve::m_unary_encoding

Private member functions

std::vector<bdd_type> compute_edge_relation(const std::vector<srf_equation> &equations, const std::vector<bdd_type> &equation_ids, const std::vector<bdd_type> &equation_ids_next, const std::vector<bdd_type> &parameters_next) const
std::vector<data::variable> compute_id_variables(std::size_t n, bool unary_encoding)
bdd_type compute_initial_state(const std::vector<bdd_type> &ids) const
std::vector<bdd_type> compute_nodes(std::size_t equation_count, const std::vector<bdd_type> &id_variables, bool unary_encoding)
std::tuple<bdd_variable_set, bdd_variable_set, bdd_variable_set, bdd_substitution, bdd_substitution, bdd_type, std::vector<bdd_type>, bdd_type, bdd_type, bdd_type, std::map<std::uint32_t, bdd_type>> compute_parity_game()
std::map<std::size_t, std::vector<bdd_type>> compute_priority_map(const std::vector<bdd_type> &equation_ids) const
void finish_timer(const std::string &msg) const
std::vector<bdd_type> make_bdd_variables(const std::vector<data::variable> &v)
bdd_type parameter_updates(const std::vector<bdd_type> &parameters, const std::vector<bdd_type> &values) const
void start_timer(const std::string &msg) const
bdd_type to_bdd(const data::variable &x) const
bdd_type to_bdd(const data::data_expression &x) const
std::vector<bdd_type> to_bdd(const data::data_expression_list &v) const
std::vector<bdd_type> to_bdd(const data::variable_list &v) const
std::vector<bdd_type> to_bdd(const std::vector<data::variable> &v) const

Public member functions

pbesbddsolve(const srf_pbes &p, bdd_sylvan &bdd, bool unary_encoding = false, bdd::bdd_granularity granularity = bdd::bdd_granularity::per_pbes, utilities::execution_timer *timer = nullptr)
bool run(bool use_sylvan_optimization = true, bool remove_unreachable_vertices = true)