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<lps::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<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)

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)

Removes all winning states (and updates winning partition).

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

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

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)

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)

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)

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

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

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())

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())

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())

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].

symbolic_parity_game(const srf_pbes &pbes, const std::vector<summand_group> &summand_groups, const std::vector<lps::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.

Private member functions

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 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())

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

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

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