mcrl2::pbes_system::symbolic_pbessolve_algorithm

Include file:

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

Private attributes

symbolic_parity_game mcrl2::pbes_system::symbolic_pbessolve_algorithm::m_G

Public member functions

std::pair<ldd, ldd> detect_fatal_attractors(const ldd &initial_vertex, const ldd &V, const ldd &I, bool safe_variant, const ldd &Vsinks, const ldd &W0 = sylvan::ldds::empty_set(), const ldd &W1 = sylvan::ldds::empty_set())

Returns: Partial solve using the fatal attractors.

std::pair<const ldd, const ldd> detect_forced_cycles(const ldd &initial_vertex, const ldd &V, const ldd &I, bool safe_variant, const ldd &Vsinks, const ldd &W0 = sylvan::ldds::empty_set(), const ldd &W1 = sylvan::ldds::empty_set())

Detect forced winning cycles for the given incomplete parity game (m_G, I) restricted to V. The remaining parameters are sinks, vertices won by even and odd respectively. Terminates early when initial_vertex has been solved.

Parameters:

  • safe Whether to use the safe attractor variant (as opposed to computing safe vertices first).

std::pair<const ldd, const ldd> detect_solitair_cycles(const ldd &initial_vertex, const ldd &V, const ldd &I, bool safe_variant, const ldd &Vsinks, const ldd &W0 = sylvan::ldds::empty_set(), const ldd &W1 = sylvan::ldds::empty_set())

Detect solitair winning cycles for the given incomplete parity game (m_G, I) restricted to V. The remaining parameters are sinks, vertices won by even and odd respectively. Terminates early when initial_vertex has been solved.

Parameters:

  • safe Whether to use the safe attractor variant (as opposed to computing safe vertices first).

std::pair<const ldd, const ldd> partial_solve(const ldd &initial_vertex, const ldd &V, const ldd &I, const ldd &Vsinks = sylvan::ldds::empty_set(), const ldd &W0 = sylvan::ldds::empty_set(), const ldd &W1 = sylvan::ldds::empty_set())

Solve the given incomplete parity game (m_G, I) restricted to V. The remaining parameters are sinks, vertices won by even and odd respectively. Terminates early when initial_vertex has been solved.

bool solve(const ldd &initial_vertex, const ldd &V, const ldd &Vsinks = sylvan::ldds::empty_set(), const ldd &W0 = sylvan::ldds::empty_set(), const ldd &W1 = sylvan::ldds::empty_set())

Solve the given game restricted to V with Zielonka’s recursive algorithm as solver. The remaining parameters are sinks, vertices won by even and odd respectively. Terminates early when initial_vertex has been solved.

symbolic_pbessolve_algorithm(symbolic_parity_game G)
std::pair<ldd, ldd> zielonka(const ldd &V)