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

bdd_variable_set mcrl2::pbes_system::bdd::bdd_parity_game::m_all_variables
bdd_sylvan &mcrl2::pbes_system::bdd::bdd_parity_game::m_bdd
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
bdd_variable_set mcrl2::pbes_system::bdd::bdd_parity_game::m_next_variables
bdd_type mcrl2::pbes_system::bdd::bdd_parity_game::m_odd
std::map<uint32_t, bdd_type> mcrl2::pbes_system::bdd::bdd_parity_game::m_priorities
bdd_substitution mcrl2::pbes_system::bdd::bdd_parity_game::m_reverse_substitution
bdd_substitution mcrl2::pbes_system::bdd::bdd_parity_game::m_substitution
bdd_type mcrl2::pbes_system::bdd::bdd_parity_game::m_V
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 &substitution, const bdd_substitution &reverse_substitution, const bdd_type &V, const bdd_type &E, const bdd_type &even_nodes, const bdd_type &odd_nodes, std::map<uint32_t, bdd_type> priorities, const bdd_type &initial_state)
std::size_t game_size() const
bool has_successor(const bdd_type &U) const
const bdd_type &initial_state() const
uint32_t maximum() const
const bdd_variable_set &next_variables() const
bdd_type predecessor(bool player, const bdd_type &U)
void print() const
void remove(const bdd_type &A)
bdd_type successor(const bdd_type &U)
const bdd_variable_set &variables() const
std::pair<bdd_type, bdd_type> zielonka(bool debug = false)