#include <SmallProgressMeasures.h>

Inheritance diagram for SmallProgressMeasures:

Public Member Functions
	SmallProgressMeasures (const ParityGame &game, ParityGame::Player player, LiftingStatistics stats=0, const verti vmap=0, verti vmap_size=0)

virtual	~SmallProgressMeasures ()

long long	solve_some (LiftingStrategy &ls, long long attempts=work_size)

long long	solve_some (LiftingStrategy2 &ls, long long attempts=work_size)

std::pair< verti, bool >	solve_one (LiftingStrategy &ls)

verti	solve_one (LiftingStrategy2 &ls)

verti	get_strategy (verti v) const

void	get_strategy (ParityGame::Strategy &strat) const

template<class OutputIterator >
void	get_winning_set (ParityGame::Player player, OutputIterator result)

bool	lift_to_top (verti v)

bool	lift_to (verti v, const verti vec2[], bool carry=0)

bool	less_than (verti v, const verti vec2[], bool carry=0)

void	debug_print () const

void	debug_print_vertex (int v) const

bool	verify_solution ()

const ParityGame &	game () const

ParityGame::Player	player () const

int	len () const

const verti *	M () const

void	set_M (const verti *new_M)

void	decr_M (int i)

int	len (verti v) const

bool	is_top (const verti vec[]) const

bool	is_top (verti v) const

virtual const verti *	vec (verti v) const =0

virtual void	set_vec (verti v, const verti src[], bool carry)=0

virtual void	set_vec_to_top (verti v)=0

void	initialize_lifting_strategy (LiftingStrategy2 &ls)

Static Public Attributes
static const int	work_size = 10000
	Maximum number of lifting attempts in a row before checking timer.

Protected Member Functions
void	initialize_loops ()

void	set_top (verti v)

Protected Attributes
const ParityGame &	game_
	the game being solved

const std::size_t	p_
	the player to solve for

LiftingStatistics *	stats_
	statistics object to record lifts

const verti *	vmap_
	active vertex map (if any)

verti	vmap_size_
	size of vertex map

std::size_t	len_
	length of SPM vectors

verti *	M_
	bounds on the SPM vector components

ParityGame::Strategy	strategy_
	current strategy

bool *	dirty_
	marks unstable vertices

Private Member Functions
	SmallProgressMeasures (const SmallProgressMeasures &)

SmallProgressMeasures &	operator= (const SmallProgressMeasures &)

int	vector_cmp (const verti vec1[], const verti vec2[], int N) const

int	vector_cmp (verti v, verti w, int N) const

bool	take_max (verti v) const

bool	compare_strict (verti v) const

verti	get_ext_succ (verti v, bool take_max) const

verti	get_ext_succ (verti v) const

verti	get_min_succ (verti v) const

verti	get_max_succ (verti v) const

verti	get_successor (verti v) const

bool	is_dirty (verti v) const

Friends
class	PredecessorLiftingStrategy

class	MaxMeasureLiftingStrategy2

class	OldMaxMeasureLiftingStrategy

Detailed Description

Implements the core of the Small Progress Measures algorithm, which keeps track of progress measure vectors, and allows lifting at vertices.

Note that besides these vectors, it tracks the current lifting strategy and (optionally) a statistics object. All public methods of this class notify the lifting strategy whenever vectors change (due to one of the solve..() lift..() methods), but only when vertices are lifted through one of the solve..() methods, are lifting attempts recording in the statistics object.

As a result, the lift..() methods can be used to introduce information from external sources into the game, without affecting the statistics for updates that result from local lifting attempts. These methods are thus used in the two-way approach to propagate information from the dual game, and the MPI recursive solver.

Note that this is an abstract base class: subclasses may implement different storage formats for the progress measure vectors.

Definition at line 84 of file SmallProgressMeasures.h.

Constructor & Destructor Documentation

◆ SmallProgressMeasures() [1/2]

SmallProgressMeasures::SmallProgressMeasures	(	const ParityGame &	game,
		ParityGame::Player	player,
		LiftingStatistics *	stats = `0`,
		const verti *	vmap = `0`,
		verti	vmap_size = `0`
	)

Definition at line 37 of file SmallProgressMeasures.cpp.

◆ ~SmallProgressMeasures()

SmallProgressMeasures::~SmallProgressMeasures ( )

virtual

Definition at line 110 of file SmallProgressMeasures.cpp.

◆ SmallProgressMeasures() [2/2]

SmallProgressMeasures::SmallProgressMeasures ( const SmallProgressMeasures & )

private

Member Function Documentation

◆ compare_strict()

bool SmallProgressMeasures::compare_strict ( verti v ) const

inlineprivate

Returns whether the progress measure for vertex v must be strictly greater than its successors or not (which is true if its priority has parity different from the current player).

Definition at line 233 of file SmallProgressMeasures.h.

◆ debug_print()

void SmallProgressMeasures::debug_print ( ) const

For debugging: print current state to stdout

◆ debug_print_vertex()

void SmallProgressMeasures::debug_print_vertex ( int v ) const

◆ decr_M()

void SmallProgressMeasures::decr_M ( int i )

inline

Decrements the i'th element of M.

Definition at line 170 of file SmallProgressMeasures.h.

◆ game()

const ParityGame & SmallProgressMeasures::game ( ) const

inline

Return the parity to be solved.

Definition at line 154 of file SmallProgressMeasures.h.

◆ get_ext_succ() [1/2]

verti SmallProgressMeasures::get_ext_succ ( verti v ) const

inlineprivate

Returns the minimum or maximum successor for vertex v depending on whether it is owned by player p_ or not.

◆ get_ext_succ() [2/2]

verti SmallProgressMeasures::get_ext_succ	(	verti	v,
		bool	take_max
	)		const

inlineprivate

Returns the minimum or maximum successor for vertex v, depending on whether take_max is false or true (respectively).

Definition at line 39 of file SmallProgressMeasures_impl.h.

◆ get_max_succ()

verti SmallProgressMeasures::get_max_succ ( verti v ) const

inlineprivate

Returns the maximum successor for vertex v.

Definition at line 247 of file SmallProgressMeasures.h.

◆ get_min_succ()

verti SmallProgressMeasures::get_min_succ ( verti v ) const

inlineprivate

Returns the minimum successor for vertex v.

Definition at line 244 of file SmallProgressMeasures.h.

◆ get_strategy() [1/2]

void SmallProgressMeasures::get_strategy ( ParityGame::Strategy & strat ) const

Takes an initialized strategy vector and updates it for the current player. The result is valid only after the game is solved.

Definition at line 235 of file SmallProgressMeasures.cpp.

◆ get_strategy() [2/2]

verti SmallProgressMeasures::get_strategy ( verti v ) const

After the game is solved, this returns the strategy at vertex v for the current player, or NO_VERTEX if the vertex is controlled by his opponent (in that case, any move is winning) or if it is won by his opponent (in that case, all moves are losing).

Definition at line 230 of file SmallProgressMeasures.cpp.

◆ get_successor()

verti SmallProgressMeasures::get_successor ( verti v ) const

inlineprivate

Returns whether the succesor with the extreme progress measure for the given vertex. (Extreme means minimal for even-controlled vertices, and maximal for odd-controlled vertices.)

Definition at line 252 of file SmallProgressMeasures.h.

◆ get_winning_set()

template<class OutputIterator >

void SmallProgressMeasures::get_winning_set	(	ParityGame::Player	player,
		OutputIterator	result
	)

Returns the winning set for the given player by assigning the vertices in the set to the given output iterator. If the game is not completely solved yet, then this returns a subset of the winning set.

Definition at line 57 of file SmallProgressMeasures_impl.h.

◆ initialize_lifting_strategy()

void SmallProgressMeasures::initialize_lifting_strategy ( LiftingStrategy2 & ls )

Recalculates the set of dirty vertices, and pushes them into the given lifting strategy (which is assumed to be freshly allocated).

Definition at line 88 of file SmallProgressMeasures.cpp.

◆ initialize_loops()

void SmallProgressMeasures::initialize_loops ( )

protected

Sets odd-controlled vertices with (only) loops to top. Should be called by derived classes after allocating SPM data.

Definition at line 57 of file SmallProgressMeasures.cpp.

◆ is_dirty()

bool SmallProgressMeasures::is_dirty ( verti v ) const

inlineprivate

Returns whether the given vertex is dirty; i.e. its progress measure is less than its successor (or less than or equal to, if its priority is odd).

Definition at line 257 of file SmallProgressMeasures.h.

◆ is_top() [1/2]

bool SmallProgressMeasures::is_top ( const verti vec[] ) const

inline

Return whether the given SPM vector has top value.

Definition at line 177 of file SmallProgressMeasures.h.

◆ is_top() [2/2]

bool SmallProgressMeasures::is_top ( verti v ) const

inline

Return whether the SPM vector for vertex v has top value.

Definition at line 180 of file SmallProgressMeasures.h.

◆ len() [1/2]

int SmallProgressMeasures::len ( ) const

inline

Return the length of the SPM vectors (a positive integer).

Definition at line 160 of file SmallProgressMeasures.h.

◆ len() [2/2]

int SmallProgressMeasures::len ( verti v ) const

inline

Return the number of odd priorities less than or equal to the priority of v. This is the length of the SPM vector for v.

Definition at line 174 of file SmallProgressMeasures.h.

◆ less_than()

bool SmallProgressMeasures::less_than	(	verti	v,
		const verti	vec2[],
		bool	carry = `0`
	)

Returns the same result as lift_to() but without changing any progress measure vectors.

Definition at line 247 of file SmallProgressMeasures.cpp.

◆ lift_to()

bool SmallProgressMeasures::lift_to	(	verti	v,
		const verti	vec2[],
		bool	carry = `0`
	)

Sets the given vertex's progress measure to the given value, if this is greater than the current value, and returns whether it changed. val[] must be an array of length len(v). If carry is set, the new value must be strictly greater (or top).

Definition at line 255 of file SmallProgressMeasures.cpp.

◆ lift_to_top()

bool SmallProgressMeasures::lift_to_top ( verti v )

inline

Sets the given vertex's progress measure to top, if it isn't already, and returns whether it changed:

Definition at line 151 of file SmallProgressMeasures_impl.h.

◆ M()

const verti * SmallProgressMeasures::M ( ) const

inline

Returns the SPM vector space; an array of len() integers.

Definition at line 163 of file SmallProgressMeasures.h.

◆ operator=()

SmallProgressMeasures & SmallProgressMeasures::operator= ( const SmallProgressMeasures & )

private

◆ player()

ParityGame::Player SmallProgressMeasures::player ( ) const

inline

Return the player to solve for.

Definition at line 157 of file SmallProgressMeasures.h.

◆ set_M()

void SmallProgressMeasures::set_M ( const verti * new_M )

inline

Changes the SPM vector space. new_M must be an array of at least len non-negative integers.

Definition at line 167 of file SmallProgressMeasures.h.

◆ set_top()

void SmallProgressMeasures::set_top ( verti v )

inlineprotected

Set the SPM vector for vertex v to top value. This can decrease the vector space, but nothing else; e.g, the lifting strategy is not notified of the lift.

Definition at line 158 of file SmallProgressMeasures_impl.h.

◆ set_vec()

virtual void SmallProgressMeasures::set_vec	(	verti	v,
		const verti	src[],
		bool	carry
	)

pure virtual

Assign the first len(v) elements of the vector for vertex w to the vector for v, or its successor if carry is set.

Implemented in DenseSPM.

◆ set_vec_to_top()

virtual void SmallProgressMeasures::set_vec_to_top ( verti v )

pure virtual

Set the value for vertex v to top.

Implemented in DenseSPM.

◆ solve_one() [1/2]

std::pair< verti, bool > SmallProgressMeasures::solve_one ( LiftingStrategy & ls )

Performs one lifting attempt, and returns the index of the vertex and whether lifting succeeded. Returns NO_VERTEX if no more vertices were candidates for lifting.

Definition at line 130 of file SmallProgressMeasures.cpp.

◆ solve_one() [2/2]

verti SmallProgressMeasures::solve_one ( LiftingStrategy2 & ls )

Definition at line 152 of file SmallProgressMeasures.cpp.

◆ solve_some() [1/2]

long long SmallProgressMeasures::solve_some	(	LiftingStrategy &	ls,
		long long	attempts = `work_size`
	)

Performs some work on the game using the given lifting strategy (which must have been initialized).

Parameters

max_attempts Maximum number of lifts attempted.

Returns: How many attempts remain; i.e. if the result is greater than zero, the game is succesfully solved.

See also: initialize_lifting_strategy

Definition at line 116 of file SmallProgressMeasures.cpp.

◆ solve_some() [2/2]

long long SmallProgressMeasures::solve_some	(	LiftingStrategy2 &	ls,
		long long	attempts = `work_size`
	)

Definition at line 123 of file SmallProgressMeasures.cpp.

◆ take_max()

bool SmallProgressMeasures::take_max ( verti v ) const

inlineprivate

Returns whehter vertex v is lifted to the maximum successor (true) or minimum successor (false), which in turn depends on whether it is controlled by the player p_ we are solving for.

Definition at line 228 of file SmallProgressMeasures.h.

◆ vec()

virtual const verti * SmallProgressMeasures::vec ( verti v ) const

pure virtual

Return the SPM vector for vertex v. This array contains only the components with odd (for Even) or even (for Odd) indices of the vector (since the reset is fixed at zero).

Implemented in DenseSPM.

◆ vector_cmp() [1/2]

int SmallProgressMeasures::vector_cmp	(	const verti	vec1[],
		const verti	vec2[],
		int	N
	)		const

inlineprivate

Compares the first N elements of the given SPM vectors and returns -1, 0 or 1 to indicate that v is smaller than, equal to, or larger than w (respectively).

Definition at line 24 of file SmallProgressMeasures_impl.h.

◆ vector_cmp() [2/2]

int SmallProgressMeasures::vector_cmp	(	verti	v,
		verti	w,
		int	N
	)		const

inlineprivate

Compares N elements of the SPM vectors for the given vertices.

Definition at line 19 of file SmallProgressMeasures_impl.h.

◆ verify_solution()

bool SmallProgressMeasures::verify_solution ( )

For debugging: verify that the current state describes a valid SPM

Friends And Related Symbol Documentation

◆ MaxMeasureLiftingStrategy2

friend class MaxMeasureLiftingStrategy2

friend

Definition at line 261 of file SmallProgressMeasures.h.

◆ OldMaxMeasureLiftingStrategy

friend class OldMaxMeasureLiftingStrategy

friend

Definition at line 262 of file SmallProgressMeasures.h.

◆ PredecessorLiftingStrategy

friend class PredecessorLiftingStrategy

friend

Definition at line 260 of file SmallProgressMeasures.h.

Member Data Documentation

◆ dirty_

bool* SmallProgressMeasures::dirty_

protected

marks unstable vertices

Definition at line 273 of file SmallProgressMeasures.h.

◆ game_

const ParityGame& SmallProgressMeasures::game_

protected

the game being solved

Definition at line 265 of file SmallProgressMeasures.h.

◆ len_

std::size_t SmallProgressMeasures::len_

protected

length of SPM vectors

Definition at line 270 of file SmallProgressMeasures.h.

◆ M_

verti* SmallProgressMeasures::M_

protected

bounds on the SPM vector components

Definition at line 271 of file SmallProgressMeasures.h.

◆ p_

const std::size_t SmallProgressMeasures::p_

protected

the player to solve for

Definition at line 266 of file SmallProgressMeasures.h.

◆ stats_

LiftingStatistics* SmallProgressMeasures::stats_

protected

statistics object to record lifts

Definition at line 267 of file SmallProgressMeasures.h.

◆ strategy_

ParityGame::Strategy SmallProgressMeasures::strategy_

protected

current strategy

Definition at line 272 of file SmallProgressMeasures.h.

◆ vmap_

const verti* SmallProgressMeasures::vmap_

protected

active vertex map (if any)

Definition at line 268 of file SmallProgressMeasures.h.

◆ vmap_size_

verti SmallProgressMeasures::vmap_size_

protected

size of vertex map

Definition at line 269 of file SmallProgressMeasures.h.

◆ work_size

const int SmallProgressMeasures::work_size = 10000

static

Maximum number of lifting attempts in a row before checking timer.

Definition at line 88 of file SmallProgressMeasures.h.

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

pg/include/mcrl2/pg/SmallProgressMeasures.h
pg/include/mcrl2/pg/SmallProgressMeasures_impl.h
pg/source/SmallProgressMeasures.cpp

Public Member Functions

Static Public Attributes

Protected Member Functions

Protected Attributes

Private Member Functions

Friends

Detailed Description

Constructor & Destructor Documentation

◆ SmallProgressMeasures() [1/2]

◆ ~SmallProgressMeasures()

◆ SmallProgressMeasures() [2/2]

Member Function Documentation

◆ compare_strict()

◆ debug_print()

◆ debug_print_vertex()

◆ decr_M()

◆ game()

◆ get_ext_succ() [1/2]

◆ get_ext_succ() [2/2]

◆ get_max_succ()

◆ get_min_succ()

◆ get_strategy() [1/2]

◆ get_strategy() [2/2]

◆ get_successor()

◆ get_winning_set()

◆ initialize_lifting_strategy()

◆ initialize_loops()

◆ is_dirty()

◆ is_top() [1/2]

◆ is_top() [2/2]

◆ len() [1/2]

◆ len() [2/2]

◆ less_than()

◆ lift_to()

◆ lift_to_top()

◆ M()

◆ operator=()

◆ player()

◆ set_M()

◆ set_top()

◆ set_vec()

◆ set_vec_to_top()

◆ solve_one() [1/2]

◆ solve_one() [2/2]

◆ solve_some() [1/2]

◆ solve_some() [2/2]

◆ take_max()

◆ vec()

◆ vector_cmp() [1/2]

◆ vector_cmp() [2/2]

◆ verify_solution()

Friends And Related Symbol Documentation

◆ MaxMeasureLiftingStrategy2

◆ OldMaxMeasureLiftingStrategy

◆ PredecessorLiftingStrategy

Member Data Documentation

◆ dirty_

◆ game_

◆ len_

◆ M_

◆ p_

◆ stats_

◆ strategy_

◆ vmap_

◆ vmap_size_

◆ work_size