mcrl2::pbes_system::bdd_parity_game

Include file:

#include "mcrl2/pbes/pbesbddsolve1.h

class mcrl2::pbes_system::bdd_parity_game

public-static-attrib

constexpr bool mcrl2::pbes_system::bdd_parity_game::even

constexpr bool mcrl2::pbes_system::bdd_parity_game::odd

Private attributes

const bdd &mcrl2::pbes_system::bdd_parity_game::m_all_variables

std::vector<bdd> mcrl2::pbes_system::bdd_parity_game::m_E

bdd mcrl2::pbes_system::bdd_parity_game::m_even

bdd mcrl2::pbes_system::bdd_parity_game::m_initial_state

const bdd_substitution &mcrl2::pbes_system::bdd_parity_game::m_next_substitution

const bdd &mcrl2::pbes_system::bdd_parity_game::m_next_variables

bdd mcrl2::pbes_system::bdd_parity_game::m_odd

const bdd_substitution &mcrl2::pbes_system::bdd_parity_game::m_prev_substitution

std::map<std::uint32_t, bdd> mcrl2::pbes_system::bdd_parity_game::m_priorities

bool mcrl2::pbes_system::bdd_parity_game::m_use_sylvan_optimization

bdd mcrl2::pbes_system::bdd_parity_game::m_V

const bdd &mcrl2::pbes_system::bdd_parity_game::m_variables

Private member functions

void info(const bdd &x, const std::string &msg, const bdd &variables) const

Public member functions

const bdd &all_variables() const

bdd attractor(bool player, const bdd &A)

bdd_parity_game(const bdd &variables, const bdd &next_variables, const bdd &all_variables, const bdd_substitution &next_substitution, const bdd_substitution &prev_substitution, const bdd &V, const std::vector<bdd> &E, const bdd &even_nodes, const bdd &odd_nodes, const std::map<std::uint32_t, bdd> &priorities, const bdd &initial_state, bool use_sylvan_optimization = false)

const std::vector<bdd> &edges() const

const bdd &even_nodes() const

std::size_t game_size() const

const bdd &initial_state() const

std::uint32_t maximum() const

const bdd &next_variables() const

const bdd &nodes() const

const bdd &odd_nodes() const

bdd predecessor(bool player, const bdd &U, bool optimized = false)

void print() const

const std::map<std::uint32_t, bdd> &priorities() const

bdd reachable_vertices(const bdd &U)

bdd reachable_vertices_default(const bdd &U)

void remove(const bdd &A)

const bdd_substitution &reverse_substitution() const

const bdd_substitution &substitution() const

const bdd &variables() const

std::pair<bdd, bdd> zielonka()