mcrl2::pbes_system::bdd::bdd_parity_game

Include file:

#include "mcrl2/pbes/pbesbddsolve.h

class mcrl2::pbes_system::bdd::bdd_parity_game

Public types

type mcrl2::pbes_system::bdd::bdd_parity_game::bdd_substitution

typedef for bdd_sylvan::bdd_substitution

type mcrl2::pbes_system::bdd::bdd_parity_game::bdd_type

typedef for bdd_sylvan::bdd_type

type mcrl2::pbes_system::bdd::bdd_parity_game::bdd_variable_set

typedef for bdd_sylvan::bdd_variable_set

public-static-attrib

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

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

Private attributes

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

bdd_sylvan &mcrl2::pbes_system::bdd::bdd_parity_game::m_bdd

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

bdd_type mcrl2::pbes_system::bdd::bdd_parity_game::m_even

bdd_type mcrl2::pbes_system::bdd::bdd_parity_game::m_initial_state

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

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

bdd_type mcrl2::pbes_system::bdd::bdd_parity_game::m_odd

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

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

bool mcrl2::pbes_system::bdd::bdd_parity_game::m_use_sylvan_optimization

bdd_type mcrl2::pbes_system::bdd::bdd_parity_game::m_V

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

Private member functions

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

Public member functions

const bdd_variable_set &all_variables() const

bdd_type attractor(bool player, const bdd_type &A)

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

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

const bdd_type &even_nodes() const

std::size_t game_size() const

const bdd_type &initial_state() const

std::uint32_t maximum() const

const bdd_variable_set &next_variables() const

const bdd_type &nodes() const

const bdd_type &odd_nodes() const

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

void print() const

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

bdd_type reachable_vertices(const bdd_type &U)

bdd_type reachable_vertices_default(const bdd_type &U)

void remove(const bdd_type &A)

const bdd_substitution &reverse_substitution() const

const bdd_substitution &substitution() const

const bdd_variable_set &variables() const

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