A class representing the interface that all game solvers shall implement. More...

#include <GameSolver.h>

Inheritance diagram for storm::solver::GameSolver< ValueType >:

[legend]

Collaboration diagram for storm::solver::GameSolver< ValueType >:

Public Member Functions
virtual	~GameSolver ()=default

virtual bool	solveGame (Environment const &env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector< ValueType > &x, std::vector< ValueType > const &b, std::vector< uint64_t > player1Choices=nullptr, std::vector< uint64_t > player2Choices=nullptr) const =0
	Solves the equation system defined by the game matrices.

virtual void	repeatedMultiply (Environment const &env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector< ValueType > &x, std::vector< ValueType > const *b, uint_fast64_t n=1) const =0
	Performs (repeated) matrix-vector multiplication with the given parameters, i.e.

void	setTrackSchedulers (bool value=true)
	Sets whether schedulers are generated when solving equation systems.

bool	isTrackSchedulersSet () const
	Retrieves whether this solver is set to generate schedulers.

bool	hasSchedulers () const
	Retrieves whether the solver generated a scheduler.

storm::storage::Scheduler< ValueType >	computePlayer1Scheduler () const
	Retrieves the generated scheduler.

storm::storage::Scheduler< ValueType >	computePlayer2Scheduler () const

std::vector< uint_fast64_t > const &	getPlayer1SchedulerChoices () const
	Retrieves the generated (deterministic) choices of the optimal scheduler.

std::vector< uint_fast64_t > const &	getPlayer2SchedulerChoices () const

void	setSchedulerHints (std::vector< uint_fast64_t > &&player1Choices, std::vector< uint_fast64_t > &&player2Choices)
	Sets scheduler hints that might be considered by the solver as an initial guess.

bool	hasSchedulerHints () const
	Returns whether Scheduler hints are available.

void	setCachingEnabled (bool value)
	Sets whether some of the generated data during solver calls should be cached.

bool	isCachingEnabled () const
	Retrieves whether some of the generated data during solver calls should be cached.

virtual void	clearCache () const

void	setHasUniqueSolution (bool value=true)
	Sets whether the solution to the min max equation system is known to be unique.

bool	hasUniqueSolution () const
	Retrieves whether the solution to the min max equation system is assumed to be unique.

Public Member Functions inherited from storm::solver::AbstractEquationSolver< ValueType >
	AbstractEquationSolver ()

void	setTerminationCondition (std::unique_ptr< TerminationCondition< ValueType > > terminationCondition)
	Sets a custom termination condition that is used together with the regular termination condition of the solver.

void	resetTerminationCondition ()
	Removes a previously set custom termination condition.

bool	hasCustomTerminationCondition () const
	Retrieves whether a custom termination condition has been set.

bool	terminateNow (std::vector< ValueType > const &values, SolverGuarantee const &guarantee) const
	Checks whether the solver can terminate wrt.

bool	hasRelevantValues () const
	Retrieves whether this solver has particularly relevant values.

storm::storage::BitVector const &	getRelevantValues () const
	Retrieves the relevant values (if there are any).

boost::optional< storm::storage::BitVector > const &	getOptionalRelevantValues () const

void	setRelevantValues (storm::storage::BitVector &&valuesOfInterest)
	Sets the relevant values.

void	setRelevantValues (storm::storage::BitVector const &valuesOfInterest)
	Sets the relevant values.

void	clearRelevantValues ()
	Removes the values of interest (if there were any).

bool	hasLowerBound (BoundType const &type=BoundType::Any) const
	Retrieves whether this solver has a lower bound.

bool	hasUpperBound (BoundType const &type=BoundType::Any) const
	Retrieves whether this solver has an upper bound.

void	setLowerBound (ValueType const &value)
	Sets a lower bound for the solution that can potentially be used by the solver.

void	setUpperBound (ValueType const &value)
	Sets an upper bound for the solution that can potentially be used by the solver.

void	setBounds (ValueType const &lower, ValueType const &upper)
	Sets bounds for the solution that can potentially be used by the solver.

ValueType const &	getLowerBound () const
	Retrieves the lower bound (if there is any).

ValueType const &	getLowerBound (uint64_t const &index) const
	Retrieves the lower bound for the variable with the given index (if there is any lower bound).

ValueType	getLowerBound (bool convertLocalBounds) const
	Retrieves the lower bound (if there is any).

ValueType const &	getUpperBound () const
	Retrieves the upper bound (if there is any).

ValueType const &	getUpperBound (uint64_t const &index) const
	Retrieves the upper bound for the variable with the given index (if there is any upper bound).

ValueType	getUpperBound (bool convertLocalBounds) const
	Retrieves the upper bound (if there is any).

std::vector< ValueType > const &	getLowerBounds () const
	Retrieves a vector containing the lower bounds (if there are any).

std::vector< ValueType > const &	getUpperBounds () const
	Retrieves a vector containing the upper bounds (if there are any).

void	setLowerBounds (std::vector< ValueType > const &values)
	Sets lower bounds for the solution that can potentially be used by the solver.

void	setLowerBounds (std::vector< ValueType > &&values)
	Sets lower bounds for the solution that can potentially be used by the solver.

void	setUpperBounds (std::vector< ValueType > const &values)
	Sets upper bounds for the solution that can potentially be used by the solver.

void	setUpperBounds (std::vector< ValueType > &&values)
	Sets upper bounds for the solution that can potentially be used by the solver.

void	setBounds (std::vector< ValueType > const &lower, std::vector< ValueType > const &upper)
	Sets bounds for the solution that can potentially be used by the solver.

void	setBoundsFromOtherSolver (AbstractEquationSolver< ValueType > const &other)

void	clearBounds ()
	Removes all specified solution bounds.

bool	isShowProgressSet () const
	Retrieves whether progress is to be shown.

uint64_t	getShowProgressDelay () const
	Retrieves the delay between progress emissions.

void	startMeasureProgress (uint64_t startingIteration=0) const
	Starts to measure progress.

void	showProgressIterative (uint64_t iterations, boost::optional< uint64_t > const &bound=boost::none) const
	Shows progress if this solver is asked to do so.

Protected Member Functions
	GameSolver ()

Protected Member Functions inherited from storm::solver::AbstractEquationSolver< ValueType >
TerminationCondition< ValueType > const &	getTerminationCondition () const
	Retrieves the custom termination condition (if any was set).

std::unique_ptr< TerminationCondition< ValueType > > const &	getTerminationConditionPointer () const

void	createUpperBoundsVector (std::vector< ValueType > &upperBoundsVector) const

void	createUpperBoundsVector (std::unique_ptr< std::vector< ValueType > > &upperBoundsVector, uint64_t length) const

void	createLowerBoundsVector (std::vector< ValueType > &lowerBoundsVector) const

void	reportStatus (SolverStatus status, boost::optional< uint64_t > const &iterations=boost::none) const
	Report the current status of the solver.

SolverStatus	updateStatus (SolverStatus status, std::vector< ValueType > const &x, SolverGuarantee const &guarantee, uint64_t iterations, uint64_t maximalNumberOfIterations) const
	Update the status of the solver with respect to convergence, early termination, abortion, etc.

SolverStatus	updateStatus (SolverStatus status, bool earlyTermination, uint64_t iterations, uint64_t maximalNumberOfIterations) const
	Update the status of the solver with respect to convergence, early termination, abortion, etc.

Protected Attributes
bool	trackSchedulers
	Whether we generate schedulers during solving.

boost::optional< std::vector< uint_fast64_t > >	player1SchedulerChoices
	The scheduler choices that induce the optimal values (if they could be successfully generated).

boost::optional< std::vector< uint_fast64_t > >	player2SchedulerChoices

boost::optional< std::vector< uint_fast64_t > >	player1ChoicesHint

boost::optional< std::vector< uint_fast64_t > >	player2ChoicesHint

Protected Attributes inherited from storm::solver::AbstractEquationSolver< ValueType >
std::unique_ptr< TerminationCondition< ValueType > >	terminationCondition

boost::optional< storm::storage::BitVector >	relevantValues

boost::optional< ValueType >	lowerBound

boost::optional< ValueType >	upperBound

boost::optional< std::vector< ValueType > >	lowerBounds

boost::optional< std::vector< ValueType > >	upperBounds

Additional Inherited Members
Public Types inherited from storm::solver::AbstractEquationSolver< ValueType >
enum class	BoundType { Global , Local , Any }

Detailed Description

template<class ValueType>
class storm::solver::GameSolver< ValueType >

A class representing the interface that all game solvers shall implement.

Definition at line 30 of file GameSolver.h.

Constructor & Destructor Documentation

◆ ~GameSolver()

template<class ValueType >

virtual storm::solver::GameSolver< ValueType >::~GameSolver ( )

virtualdefault

◆ GameSolver()

template<typename ValueType >

storm::solver::GameSolver< ValueType >::GameSolver ( )

protected

Definition at line 14 of file GameSolver.cpp.

Member Function Documentation

◆ clearCache()

template<typename ValueType >

void storm::solver::GameSolver< ValueType >::clearCache ( ) const

virtual

Reimplemented in storm::solver::StandardGameSolver< ValueType >.

Definition at line 101 of file GameSolver.cpp.

◆ computePlayer1Scheduler()

template<typename ValueType >

storm::storage::Scheduler< ValueType > storm::solver::GameSolver< ValueType >::computePlayer1Scheduler ( ) const

Retrieves the generated scheduler.

Note: it is only legal to call this function if schedulers were generated.

Definition at line 38 of file GameSolver.cpp.

◆ computePlayer2Scheduler()

template<typename ValueType >

storm::storage::Scheduler< ValueType > storm::solver::GameSolver< ValueType >::computePlayer2Scheduler ( ) const

Definition at line 50 of file GameSolver.cpp.

◆ getPlayer1SchedulerChoices()

template<typename ValueType >

std::vector< uint_fast64_t > const & storm::solver::GameSolver< ValueType >::getPlayer1SchedulerChoices ( ) const

Retrieves the generated (deterministic) choices of the optimal scheduler.

Note: it is only legal to call this function if schedulers were generated.

Definition at line 62 of file GameSolver.cpp.

◆ getPlayer2SchedulerChoices()

template<typename ValueType >

std::vector< uint_fast64_t > const & storm::solver::GameSolver< ValueType >::getPlayer2SchedulerChoices ( ) const

Definition at line 69 of file GameSolver.cpp.

◆ hasSchedulerHints()

template<typename ValueType >

bool storm::solver::GameSolver< ValueType >::hasSchedulerHints ( ) const

Returns whether Scheduler hints are available.

Definition at line 82 of file GameSolver.cpp.

◆ hasSchedulers()

template<typename ValueType >

bool storm::solver::GameSolver< ValueType >::hasSchedulers ( ) const

Retrieves whether the solver generated a scheduler.

Definition at line 33 of file GameSolver.cpp.

◆ hasUniqueSolution()

template<typename ValueType >

bool storm::solver::GameSolver< ValueType >::hasUniqueSolution ( ) const

Retrieves whether the solution to the min max equation system is assumed to be unique.

Definition at line 111 of file GameSolver.cpp.

◆ isCachingEnabled()

template<typename ValueType >

bool storm::solver::GameSolver< ValueType >::isCachingEnabled ( ) const

Retrieves whether some of the generated data during solver calls should be cached.

Definition at line 96 of file GameSolver.cpp.

◆ isTrackSchedulersSet()

template<typename ValueType >

bool storm::solver::GameSolver< ValueType >::isTrackSchedulersSet ( ) const

Retrieves whether this solver is set to generate schedulers.

Definition at line 28 of file GameSolver.cpp.

◆ repeatedMultiply()

template<class ValueType >

virtual void storm::solver::GameSolver< ValueType >::repeatedMultiply	(	Environment const &	env,
		OptimizationDirection	player1Dir,
		OptimizationDirection	player2Dir,
		std::vector< ValueType > &	x,
		std::vector< ValueType > const *	b,
		uint_fast64_t	n = `1`
	)		const

pure virtual

Performs (repeated) matrix-vector multiplication with the given parameters, i.e.

computes x[i+1] = min/max(player1Matrix*(min/max(player2Matrix*x[i] + b))) until x[n], where x[0] = x. After each multiplication and addition, the minimal/maximal value out of each row group is selected to reduce the resulting vector to obtain the vector for the next iteration. Note that the player1Matrix and the player2Matrix has to be given upon construction time of the solver object.

Parameters

player1Dir	Sets whether player 1 wants to minimize or maximize.
player2Dir	Sets whether player 2 wants to minimize or maximize.
x	The initial vector that is to be multiplied with the matrix. This is also the output parameter, i.e. after the method returns, this vector will contain the computed values.
b	If not null, this vector is added after each multiplication.
n	Specifies the number of iterations the matrix-vector multiplication is performed.

Implemented in storm::solver::StandardGameSolver< ValueType >.

◆ setCachingEnabled()

template<typename ValueType >

void storm::solver::GameSolver< ValueType >::setCachingEnabled ( bool value )

Sets whether some of the generated data during solver calls should be cached.

This possibly decreases the runtime of subsequent calls but also increases memory consumption.

Definition at line 87 of file GameSolver.cpp.

◆ setHasUniqueSolution()

template<typename ValueType >

void storm::solver::GameSolver< ValueType >::setHasUniqueSolution ( bool value = true )

Sets whether the solution to the min max equation system is known to be unique.

Definition at line 106 of file GameSolver.cpp.

◆ setSchedulerHints()

template<typename ValueType >

void storm::solver::GameSolver< ValueType >::setSchedulerHints	(	std::vector< uint_fast64_t > &&	player1Choices,
		std::vector< uint_fast64_t > &&	player2Choices
	)

Sets scheduler hints that might be considered by the solver as an initial guess.

Definition at line 76 of file GameSolver.cpp.

◆ setTrackSchedulers()

template<typename ValueType >

void storm::solver::GameSolver< ValueType >::setTrackSchedulers ( bool value = true )

Sets whether schedulers are generated when solving equation systems.

If the argument is false, the currently stored schedulers (if any) are deleted.

Definition at line 19 of file GameSolver.cpp.

◆ solveGame()

template<class ValueType >

virtual bool storm::solver::GameSolver< ValueType >::solveGame	(	Environment const &	env,
		OptimizationDirection	player1Dir,
		OptimizationDirection	player2Dir,
		std::vector< ValueType > &	x,
		std::vector< ValueType > const &	b,
		std::vector< uint64_t > *	player1Choices = `nullptr`,
		std::vector< uint64_t > *	player2Choices = `nullptr`
	)		const

pure virtual

Solves the equation system defined by the game matrices.

Note that the game matrices have to be given upon construction time of the solver object.

Parameters

player1Dir	Sets whether player 1 wants to minimize or maximize.
player2Dir	Sets whether player 2 wants to minimize or maximize.
x	The initial guess of the solution. For correctness, the guess has to be less (or equal) to the final solution (unless both players minimize)
b	The vector to add after matrix-vector multiplication.
player1Choices	If provided along with the storage for player 2 choices, the scheduler decisions are tracked within these two vectors.
player2Choices	If provided along with the storage for player 1 choices, the scheduler decisions are tracked within these two vectors.

Implemented in storm::solver::StandardGameSolver< ValueType >.

Member Data Documentation

◆ player1ChoicesHint

template<class ValueType >

boost::optional<std::vector<uint_fast64_t> > storm::solver::GameSolver< ValueType >::player1ChoicesHint

protected

Definition at line 143 of file GameSolver.h.

◆ player1SchedulerChoices

template<class ValueType >

boost::optional<std::vector<uint_fast64_t> > storm::solver::GameSolver< ValueType >::player1SchedulerChoices

mutableprotected

The scheduler choices that induce the optimal values (if they could be successfully generated).

Definition at line 139 of file GameSolver.h.

◆ player2ChoicesHint

template<class ValueType >

boost::optional<std::vector<uint_fast64_t> > storm::solver::GameSolver< ValueType >::player2ChoicesHint

protected

Definition at line 144 of file GameSolver.h.

◆ player2SchedulerChoices

template<class ValueType >

boost::optional<std::vector<uint_fast64_t> > storm::solver::GameSolver< ValueType >::player2SchedulerChoices

mutableprotected

Definition at line 140 of file GameSolver.h.

◆ trackSchedulers

template<class ValueType >

bool storm::solver::GameSolver< ValueType >::trackSchedulers

protected

Whether we generate schedulers during solving.

Definition at line 136 of file GameSolver.h.

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

src/storm/solver/GameSolver.h
src/storm/solver/GameSolver.cpp

Public Member Functions

Protected Member Functions

Protected Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ ~GameSolver()

◆ GameSolver()

Member Function Documentation

◆ clearCache()

◆ computePlayer1Scheduler()

◆ computePlayer2Scheduler()

◆ getPlayer1SchedulerChoices()

◆ getPlayer2SchedulerChoices()

◆ hasSchedulerHints()

◆ hasSchedulers()

◆ hasUniqueSolution()

◆ isCachingEnabled()

◆ isTrackSchedulersSet()

◆ repeatedMultiply()

◆ setCachingEnabled()

◆ setHasUniqueSolution()

◆ setSchedulerHints()

◆ setTrackSchedulers()

◆ solveGame()

Member Data Documentation

◆ player1ChoicesHint

◆ player1SchedulerChoices

◆ player2ChoicesHint

◆ player2SchedulerChoices

◆ trackSchedulers