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> &parameters_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> &parameters, const std::vector<bdd> &values) const
void start_timer(const std::string &msg) const
bdd to_bdd(const data::variable &x) const
bdd to_bdd(const data::data_expression &x) const
std::vector<bdd> to_bdd(const data::data_expression_list &v) const
std::vector<bdd> to_bdd(const data::variable_list &v) const
std::vector<bdd> to_bdd(const std::vector<data::variable> &v) const

Public member functions

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