#include <ParityGame.h>

Public Types
typedef player_t	Player

typedef std::vector< verti >	Strategy

Public Member Functions
	ParityGame ()

	~ParityGame ()

void	clear ()

void	assign (const ParityGame &game)

void	assign (const StaticGraph &g, ParityGameVertex *na)

bool	empty () const

void	swap (ParityGame &pg)

void	assign_pbes (mcrl2::pbes_system::pbes &pbes, verti *goal_vertex=0, StaticGraph::EdgeDirection edge_dir=StaticGraph::EDGE_BIDIRECTIONAL, const std::string &rewrite_strategy="jitty")

Generation
void	make_random (verti V, unsigned clustersize, unsigned outdeg, StaticGraph::EdgeDirection edge_dir, int d)

template<class ForwardIterator >
void	make_subgame (const ParityGame &game, ForwardIterator vertices_begin, ForwardIterator vertices_end, bool proper, StaticGraph::EdgeDirection edge_dir=StaticGraph::EDGE_NONE)

Transformation
void	make_dual ()

void	shuffle (const std::vector< verti > &perm)

void	compress_priorities (const verti cardinality[]=0, bool preserve_parity=true)

long long	propagate_priorities ()

Input/Output
void	read_pgsolver (std::istream &is, StaticGraph::EdgeDirection edge_dir=StaticGraph::EDGE_BIDIRECTIONAL)

void	write_pgsolver (std::ostream &os) const

void	read_pbes (const std::string &file_path, verti *goal_vertex=0, StaticGraph::EdgeDirection edge_dir=StaticGraph::EDGE_BIDIRECTIONAL, const std::string &rewrite_strategy="jitty")

void	read_raw (std::istream &is)

void	write_raw (std::ostream &os) const

void	write_dot (std::ostream &os) const

void	write_debug (const Strategy &s=Strategy(), std::ostream &os=std::cerr) const

Data access
priority_t	d () const

const StaticGraph &	graph () const

priority_t	priority (verti v) const

Player	player (verti v) const

verti	cardinality (int p) const

template<class StrategyT >
Player	winner (const StrategyT &s, verti v) const

Verification
bool	proper () const

bool	verify (const Strategy &s, verti *error) const

Protected Member Functions
void	reset (verti V, int d)

void	recalculate_cardinalities (verti num_vertices)

int	propagate_priority (verti v, StaticGraph::const_iterator it, StaticGraph::const_iterator end)

Private Member Functions
	ParityGame (const ParityGame &game)

ParityGame &	operator= (const ParityGame &game)

Private Attributes
int	d_

StaticGraph	graph_

ParityGameVertex *	vertex_

verti *	cardinality_

Detailed Description

A parity game extends a directed graph by assigning a player (Even or Odd) and an integer priority to every vertex. Priorities are between 0 and d (exclusive).

Definition at line 84 of file ParityGame.h.

Member Typedef Documentation

◆ Player

typedef player_t ParityGame::Player

Definition at line 87 of file ParityGame.h.

◆ Strategy

typedef std::vector<verti> ParityGame::Strategy

A strategy determines the partitioning of the game's vertices into winning sets for both players and provides a deterministic strategy for the vertices controlled by a player in its winning set.

For each vertex v owned by player p:

strategy[v] == NO_VERTEX if vertex v is not in p's winning set
strategy[v] == w if vertex v is in p's winning set, (v,w) is an edge in the game graph, and (v,w) is a winning move for player p.

Definition at line 97 of file ParityGame.h.

Constructor & Destructor Documentation

◆ ParityGame() [1/2]

ParityGame::ParityGame ( )

Construct an empty parity game

Definition at line 16 of file ParityGame.cpp.

◆ ~ParityGame()

ParityGame::~ParityGame ( )

Destroy a parity game

Definition at line 21 of file ParityGame.cpp.

◆ ParityGame() [2/2]

ParityGame::ParityGame ( const ParityGame & game )

explicitprivate

Member Function Documentation

◆ assign() [1/2]

void ParityGame::assign ( const ParityGame & game )

Reset the game to a copy of game.

Definition at line 38 of file ParityGame.cpp.

◆ assign() [2/2]

void ParityGame::assign	(	const StaticGraph &	g,
		ParityGameVertex *	na
	)

Reset the game with the given graph and node attributes.

Definition at line 49 of file ParityGame.cpp.

◆ assign_pbes()

void ParityGame::assign_pbes	(	mcrl2::pbes_system::pbes &	pbes,
		verti *	goal_vertex = `0`,
		StaticGraph::EdgeDirection	edge_dir = `StaticGraph::EDGE_BIDIRECTIONAL`,
		const std::string &	rewrite_strategy = `"jitty"`
	)

Generate a parity game from an mCRL2 PBES.

Definition at line 180 of file ParityGame_IO.cpp.

◆ cardinality()

verti ParityGame::cardinality ( int p ) const

inline

Returns the number of vertices with priority p. p must be between 0 and d (exclusive).

Definition at line 266 of file ParityGame.h.

◆ clear()

void ParityGame::clear ( )

Reset to an empty game.

Definition at line 27 of file ParityGame.cpp.

◆ compress_priorities()

void ParityGame::compress_priorities	(	const verti	cardinality[] = `0`,
		bool	preserve_parity = `true`
	)

Compresses the range of priorities such that after compression, cardinality(p) > 0, for 0 < p < d.

If cardinality is 0, then the priorities for the game itself are used. Otherwise, cardinality must be an array of length d and the caller must ensure that all priorities that occur in the game have a positive cardinality count.

If preserve_parity is true, then remapping preserves the parity of priorities and thus players of vertices. In this case, cardinality(0) may be zero afterwards.

If preserve_parity is false, then players as well as priorities are remapped to preserve winning sets. The function returns the parity of the priority that was mapped to zero.

Definition at line 135 of file ParityGame.cpp.

◆ d()

priority_t ParityGame::d ( ) const

inline

Returns the priority limit d; all priorities must be in range [0:d).

Definition at line 253 of file ParityGame.h.

◆ empty()

bool ParityGame::empty ( ) const

inline

Returns whether the game is empty.

Definition at line 115 of file ParityGame.h.

◆ graph()

const StaticGraph & ParityGame::graph ( ) const

inline

Returns the game graph

Definition at line 256 of file ParityGame.h.

◆ make_dual()

void ParityGame::make_dual ( )

Replaces the current game by its dual game, which uses the same game graph, but swaps players and changes priorities, such that the solution to the game is the same except with winners reversed. (A node won by even in the old game, is won by odd in the dual game, and vice versa.)

Definition at line 99 of file ParityGame.cpp.

◆ make_random()

void ParityGame::make_random	(	verti	V,
		unsigned	clustersize,
		unsigned	outdeg,
		StaticGraph::EdgeDirection	edge_dir,
		int	d
	)

Generate a random parity game, with vertices assigned uniformly at random to players, and priority assigned uniformly between 0 and d-1.

The generated game is a clustered random game if clustersize > 0, or an unclustered random game otherwise.

Parameters

V	number of game vertices
clustersize	cluster size (or 0 for no clustering)
outdeg	average outdegree (at least 1)
edge_dir	part of edges to store
d	number of priorities (at least 1)

See also: void StaticGraph::make_random()

Definition at line 84 of file ParityGame.cpp.

◆ make_subgame()

template<class ForwardIterator >

void ParityGame::make_subgame	(	const ParityGame &	game,
		ForwardIterator	vertices_begin,
		ForwardIterator	vertices_end,
		bool	proper,
		StaticGraph::EdgeDirection	edge_dir = `StaticGraph::EDGE_NONE`
	)

Create a subgame containing only the given vertices from the original game. Vertices are renumbered to be in range [0..num_vertices). Edges going out of the vertex subset specified by vertices are removed, so every vertex must have at least one outgoing edge that stays within the vertex subset, or the result is not a valid parity game.

See also: make_subgame(const ParityGame &, const verti *, verti, const Strategy &)

Definition at line 18 of file ParityGame_impl.h.

◆ operator=()

ParityGame & ParityGame::operator= ( const ParityGame & game )

private

◆ player()

Player ParityGame::player ( verti v ) const

inline

Returns the player associated with vertex v

Definition at line 262 of file ParityGame.h.

◆ priority()

priority_t ParityGame::priority ( verti v ) const

inline

Returns the priority associated with vertex v

Definition at line 259 of file ParityGame.h.

◆ propagate_priorities()

long long ParityGame::propagate_priorities ( )

Propagate priorities in the graph, by changing the priority for a vertex to the maximum of the priorities of its successors, if this is less than the vertex's current priority value, and similarly for its predecessors.

This preserves winners and optimal strategies, but usually shifts the distribution of priorities towards lower values, which benefits the performance in some solvers.

Returns the sum of differences between old and new priority values for all vertices.

Definition at line 213 of file ParityGame.cpp.

◆ propagate_priority()

int ParityGame::propagate_priority	(	verti	v,
		StaticGraph::const_iterator	it,
		StaticGraph::const_iterator	end
	)

protected

Helper function for ParityGame::propagate_priorities() that decreases the priority for v to the maximum of those in range [begin:end), if this is less than its current value, and returns the absolute change.

Definition at line 191 of file ParityGame.cpp.

◆ proper()

bool ParityGame::proper ( ) const

Checks if this is a proper game.

A game is proper if every vertex has a successor in the game graph.

Definition at line 277 of file ParityGame.cpp.

◆ read_pbes()

void ParityGame::read_pbes	(	const std::string &	file_path,
		verti *	goal_vertex = `0`,
		StaticGraph::EdgeDirection	edge_dir = `StaticGraph::EDGE_BIDIRECTIONAL`,
		const std::string &	rewrite_strategy = `"jitty"`
	)

Read a game description from an mCRL2 PBES.

Definition at line 171 of file ParityGame_IO.cpp.

◆ read_pgsolver()

void ParityGame::read_pgsolver	(	std::istream &	is,
		StaticGraph::EdgeDirection	edge_dir = `StaticGraph::EDGE_BIDIRECTIONAL`
	)

Read a game description in PGSolver format.

Definition at line 19 of file ParityGame_IO.cpp.

◆ read_raw()

void ParityGame::read_raw ( std::istream & is )

Read raw parity game data from input stream

Definition at line 233 of file ParityGame_IO.cpp.

◆ recalculate_cardinalities()

void ParityGame::recalculate_cardinalities ( verti num_vertices )

protected

Recalculate cardinalities (priority frequencies) from the first num_vertices elements of vertex_.

Definition at line 75 of file ParityGame.cpp.

◆ reset()

void ParityGame::reset	(	verti	V,
		int	d
	)

protected

Re-allocate memory to store information on V vertices with priorities between 0 and d (exclusive).

Definition at line 65 of file ParityGame.cpp.

◆ shuffle()

void ParityGame::shuffle ( const std::vector< verti > & perm )

Shuffles the nodes in the game. Node n becomes node perm[n], for all n. Requires that perm contains a permuation of 0 through graph().V()-1.

NOTE: this is the reverse of what is normally understood to be a permutation! i.e. (2 3 1) maps 1->2, 2->3, 3->1 (instead of the usual interpretation of 1->3, 2->1, 3->2)

Definition at line 120 of file ParityGame.cpp.

◆ swap()

void ParityGame::swap ( ParityGame & pg )

Efficiently swaps the contents of this parity game with another one.

Definition at line 286 of file ParityGame.cpp.

◆ verify()

bool ParityGame::verify	(	const Strategy &	s,
		verti *	error
	)		const

Verifies that the given strategy is valid in this game.

Parameters

s	the strategy to be verified
error	if non-NULL, then *error is set NO_VERTEX if the strategy is correct, and to the index of an incorrectly classified vertex if the strategy is incorrect.

Definition at line 54 of file ParityGame_verify.cpp.

◆ winner()

template<class StrategyT >

ParityGame::Player ParityGame::winner	(	const StrategyT &	s,
		verti	v
	)		const

Returns the winner for vertex v according to strategy s.

Definition at line 41 of file ParityGame_impl.h.

◆ write_debug()

void ParityGame::write_debug	(	const Strategy &	s = `Strategy()`,
		std::ostream &	os = `std::cerr`
	)		const

Write human-readable description of game to error stream (intended to be used while debugging only) with optional strategy.

Definition at line 285 of file ParityGame_IO.cpp.

◆ write_dot()

void ParityGame::write_dot ( std::ostream & os ) const

Write a game description in Graphviz DOT format

Definition at line 253 of file ParityGame_IO.cpp.

◆ write_pgsolver()

void ParityGame::write_pgsolver ( std::ostream & os ) const

Write a game description in PGSolver format.

Definition at line 151 of file ParityGame_IO.cpp.

◆ write_raw()

void ParityGame::write_raw ( std::ostream & os ) const

Write raw parity game data to output stream

Definition at line 244 of file ParityGame_IO.cpp.

Member Data Documentation

◆ cardinality_

verti* ParityGame::cardinality_

private

Cardinality counts for priorities. cardinality_[p] is equal to the number of vertices with priority p.

Definition at line 325 of file ParityGame.h.

◆ d_

int ParityGame::d_

private

priority limit (max. priority + 1)

Definition at line 317 of file ParityGame.h.

◆ graph_

StaticGraph ParityGame::graph_

private

game graph

Definition at line 318 of file ParityGame.h.

◆ vertex_

ParityGameVertex* ParityGame::vertex_

private

Assignment of players and priorities to vertices (size graph_.V())

Definition at line 321 of file ParityGame.h.

The documentation for this class was generated from the following files:

pg/include/mcrl2/pg/ParityGame.h
pg/include/mcrl2/pg/ParityGame_impl.h
pg/source/ParityGame.cpp
pg/source/ParityGame_IO.cpp
pg/source/ParityGame_verify.cpp

Public Types

Public Member Functions

Protected Member Functions

Private Member Functions

Private Attributes

Detailed Description

Member Typedef Documentation

◆ Player

◆ Strategy

Constructor & Destructor Documentation

◆ ParityGame() [1/2]

◆ ~ParityGame()

◆ ParityGame() [2/2]

Member Function Documentation

◆ assign() [1/2]

◆ assign() [2/2]

◆ assign_pbes()

◆ cardinality()

◆ clear()

◆ compress_priorities()

◆ d()

◆ empty()

◆ graph()

◆ make_dual()

◆ make_random()

◆ make_subgame()

◆ operator=()

◆ player()

◆ priority()

◆ propagate_priorities()

◆ propagate_priority()

◆ proper()

◆ read_pbes()

◆ read_pgsolver()

◆ read_raw()

◆ recalculate_cardinalities()

◆ reset()

◆ shuffle()

◆ swap()

◆ verify()

◆ winner()

◆ write_debug()

◆ write_dot()

◆ write_pgsolver()

◆ write_raw()

Member Data Documentation

◆ cardinality_

◆ d_

◆ graph_

◆ vertex_