mcrl2::pbes_system::symbolic_parity_game

Include file:

#include "mcrl2/pbes/symbolic_parity_game.h
class mcrl2::pbes_system::symbolic_parity_game

This class represents a symbolic (incomplete) parity game with sinks. Many functions have a parameter V that restricts operations to that set of vertices.

Protected attributes

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

Public member functions

ldd compute_safe_vertices(std::size_t alpha, const ldd &V, const ldd &I) const

Computes the set of vertices for which partial solving is safe w.r.t. alpha.

ldd compute_total_graph(const ldd &V, const ldd &I, const ldd &Vsinks, std::array<ldd, 2> &winning) const

Removes all winning states (and updates winning partition).

std::pair<std::size_t, ldd> get_min_rank(const ldd &V) const

Returns: (min, Vmin) where min is the minimum rank in V and Vmin is the set of vertices with the minimum rank in V

std::array<const ldd, 2> parity(const ldd &V) const

Computes the vertices with even parity priority that are not sinks and the same for odd.

std::array<const ldd, 2> players(const ldd &V) const

Computes the pair of even and odd vertices.

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

Returns: The set { u in U | exists v in V: u ->* v } where with chaining ->* only visits states in V (if U subseteq V)

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

Returns: A set of vertices { u in U | exists v in V: u ->* v } where ->* only visits intermediate vertices in W (without chaining ->* = ->)

Pre: U,W subseteq V.

std::string print_graph(const ldd &V) const

Returns: A string representing the graph restricted to V.

void print_information()

Returns: Prints basic parity game information such as number of vertices per priority and per owners.

std::string print_nodes(const ldd &V) const

Returns: A string representing the given vertex set in human readable form.

ldd prio_above(const ldd &V, std::size_t c) const

Computes all vertices above priority c.

const std::map<std::size_t, ldd> &ranks() const

Returns the mapping from priorities (ranks) to vertex sets.

ldd safe_attractor(const ldd &U, std::size_t alpha, const ldd &V, const std::array<const ldd, 2> &Vplayer, const ldd &I = sylvan::ldds::empty_set(), const ldd &T = sylvan::ldds::empty_set()) const

Compute the attractor set for U assuming that sinks(V) = emptyset.

Parameters:

  • alpha the current player
  • V is the set of states
  • Vplayer a partitioning of the nodes into the sets of even nodes V[0] and odd V[1].
  • I is a set of incomplete vertices.
  • T A set of states such that iteration stops when one of them occurs in the attractor.
ldd safe_control_predecessors(std::size_t alpha, const ldd &U, const ldd &V, const ldd &W, const std::array<const ldd, 2> &Vplayer, const ldd &I = sylvan::ldds::empty_set()) const

Compute the safe control attractor set for U w.r.t. vertices in V. The set W is a set of vertices that restrict chaining.

ldd safe_monotone_attractor(const ldd &U, std::size_t alpha, std::size_t c, const ldd &V, const std::array<const ldd, 2> &Vplayer, const ldd &I = sylvan::ldds::empty_set(), const ldd &T = sylvan::ldds::empty_set()) const

Compute the monotone attractor set for U assuming that sinks(V) = emptyset.

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 sinks(const ldd &U, const ldd &V) const

Computes the set of vertices in U subseteq V that are sinks (no outgoing edges into V).

symbolic_parity_game(const srf_pbes &pbes, const std::vector<symbolic::summand_group> summand_groups, const std::vector<symbolic::data_expression_index> &data_index, const ldd &V, bool no_relprod, bool chaining)

Determine a symbolic parity game from the given pbes, transition groups and index.

Parameters:

  • V the set of reachable vertices.
symbolic_parity_game(const std::vector<symbolic::summand_group> &summand_groups, const std::vector<symbolic::data_expression_index> &data_index, const ldd &V, const ldd &Veven, const std::vector<ldd> &prio, bool no_relprod, bool chaining)

Determine a symbolic parity game from the given pbes, transition groups and index.

Parameters:

  • V the set of reachable vertices.

Private member functions

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

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

ldd safe_control_predecessors_impl(std::size_t alpha, const ldd &U, const ldd &V, const ldd &outside, const ldd &W, const std::array<const ldd, 2> &Vplayer, const ldd &I = sylvan::ldds::empty_set()) const

Compute the safe control attractor set for todo where chaining is restricted to W. The set outside should be minus(V, U)