mcrl2::pbes_system::symbolic_pbessolve_algorithm

Include file:

#include "mcrl2/pbes/symbolic_pbessolve.h
class mcrl2::pbes_system::symbolic_pbessolve_algorithm

Protected attributes

ldd mcrl2::pbes_system::symbolic_pbessolve_algorithm::m_all_nodes
bool mcrl2::pbes_system::symbolic_pbessolve_algorithm::m_chaining
const std::vector<lps::data_expression_index> &mcrl2::pbes_system::symbolic_pbessolve_algorithm::m_data_index
bool mcrl2::pbes_system::symbolic_pbessolve_algorithm::m_no_relprod
std::map<std::size_t, ldd> mcrl2::pbes_system::symbolic_pbessolve_algorithm::m_rank_map
const std::vector<summand_group> &mcrl2::pbes_system::symbolic_pbessolve_algorithm::m_summand_groups
ldd mcrl2::pbes_system::symbolic_pbessolve_algorithm::m_V

Public member functions

ldd attractor(const ldd &U, std::size_t alpha, ldd V, const ldd &W, const std::array<const ldd, 2> &Vplayer)

Compute the attractor set for U.

Parameters:

  • alpha the current player

  • V is the set of states

  • W is a set of vertices which is considered for forced vertices, but is never added to the attractor set itself.

  • Vplayer a partitioning of the nodes into the sets of even nodes V[0] and odd V[1].

ldd compute_total_graph(const ldd &V, const ldd &todo, const ldd &Vdeadlock, std::array<ldd, 2> &won)
std::pair<ldd, ldd> detect_cycles(const ldd &V, const ldd &todo, const ldd &Vdeadlock, const ldd &W0 = sylvan::ldds::empty_set(), const ldd &W1 = sylvan::ldds::empty_set())
std::pair<ldd, ldd> detect_fatal_attractors(const ldd &V, const ldd &todo, const ldd &Vdeadlock, const ldd &W0 = sylvan::ldds::empty_set(), const ldd &W1 = sylvan::ldds::empty_set())
std::pair<std::size_t, ldd> get_min_rank(const ldd &V)
ldd monotone_attractor(const ldd &U, std::size_t alpha, std::size_t c, const ldd &V, const std::array<const ldd, 2> &Vplayer)

Compute the monotone attractor set for U.

Parameters:

  • alpha the current player.

  • c priority.

  • V the set of all vertices.

  • Vplayer a partitioning of the nodes into the sets of even nodes V[0] and odd V[1].

ldd predecessors(const ldd &U, const ldd &V, const summand_group &group)

Returns: The set { u in U | exists v in V: u -> v }, where -> is described by the given group.

ldd predecessors(const ldd &U, const ldd &V)

Returns: The set { u in U | exists v in V: u -> v }

bool solve(const ldd &initial_vertex, const ldd &V, const ldd &Vdeadlock = sylvan::ldds::empty_set(), const ldd &W0 = sylvan::ldds::empty_set(), const ldd &W1 = sylvan::ldds::empty_set())
std::pair<ldd, ldd> solve_impl(const ldd &V, const ldd &todo, const ldd &Vdeadlock = sylvan::ldds::empty_set(), const ldd &W0 = sylvan::ldds::empty_set(), const ldd &W1 = sylvan::ldds::empty_set())

Returns: The winning partition where first is the set won by player even.

symbolic_pbessolve_algorithm(const ldd &V, const std::vector<summand_group> &summand_groups, const std::map<std::size_t, std::pair<std::size_t, bool>> &equation_info, bool no_relprod, bool chaining, const std::vector<lps::data_expression_index> &data_index)
std::pair<ldd, ldd> zielonka(const ldd &V)