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::data_expression &x) const¶

std::vector<bdd_type> to_bdd(const data::data_expression_list &v) const¶

bdd_type to_bdd(const data::variable &x) 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)