#include <StandardGameSolver.h>

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

[legend]

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

[legend]

Public Member Functions
	StandardGameSolver (storm::storage::SparseMatrix< storm::storage::sparse::state_type > const &player1Matrix, storm::storage::SparseMatrix< ValueType > const &player2Matrix, std::unique_ptr< LinearEquationSolverFactory< ValueType > > &&linearEquationSolverFactory)
	StandardGameSolver (storm::storage::SparseMatrix< storm::storage::sparse::state_type > &&player1Matrix, storm::storage::SparseMatrix< ValueType > &&player2Matrix, std::unique_ptr< LinearEquationSolverFactory< ValueType > > &&linearEquationSolverFactory)
	StandardGameSolver (std::vector< uint64_t > const &player1Groups, storm::storage::SparseMatrix< ValueType > const &player2Matrix, std::unique_ptr< LinearEquationSolverFactory< ValueType > > &&linearEquationSolverFactory)
	StandardGameSolver (std::vector< uint64_t > &&player1Groups, storm::storage::SparseMatrix< ValueType > &&player2Matrix, std::unique_ptr< LinearEquationSolverFactory< ValueType > > &&linearEquationSolverFactory)
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 override
	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 override
	Performs (repeated) matrix-vector multiplication with the given parameters, i.e.
virtual void	clearCache () const override
Public Member Functions inherited from storm::solver::GameSolver< ValueType >
virtual	~GameSolver ()=default
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.
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	setShowProgress (bool verbose, uint64_t delay=5)
	Configures whether this solver should show progress during iterative solving.
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	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 &	getUpperBound () 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	setUpperBounds (std::vector< ValueType > const &values)
	Sets upper 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	hasSolutionLowerBounds () const
	Retrieves whether the last call to this solver computed a sound lower resp.
bool	hasSolutionUpperBounds () const
bool	hasExactSolutionBounds () const
	Retrieves whether the bounds computed by the last call to this solver coincide.
std::vector< ValueType > const &	getSolutionLowerBounds () const
	Retrieves sound bounds on the solution that the last call to this solver computed.
std::vector< ValueType > const &	getSolutionUpperBounds () const
SolutionBounds< ValueType > const &	getSolutionBounds () const
	Retrieves both bounds at once, either of which may be unset.
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.

Additional Inherited Members
Public Types inherited from storm::solver::AbstractEquationSolver< ValueType >
enum	BoundType
Protected Member Functions inherited from storm::solver::GameSolver< ValueType >
	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	setSolutionBounds (SolutionBounds< ValueType > bounds) const
	Stores sound bounds on the solution that were obtained while solving.
void	setSolutionBoundsExact (std::vector< ValueType > const &x) const
	Reports the given solution as an exact one, i.e.
void	finalizeSolutionBounds (std::vector< ValueType > const &x) const
	Settles the bounds to report once solving is over: the ones handed to this solver beforehand are folded into the ones it computed itself, and both are widened until they enclose the solution that is handed back.
void	clearSolutionBounds () const
	Discards any bounds on the solution obtained by a previous call.
void	setSolutionBoundsFromPrecision (std::vector< ValueType > const &x, ValueType const &precision, bool relative) const
	Turns a precision that the solving procedure is known to have achieved into sound bounds on the solution, i.e.
void	createUpperBoundsVector (std::vector< ValueType > &upperBoundsVector) 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.
Protected Attributes inherited from storm::solver::GameSolver< ValueType >
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

Detailed Description

template<typename ValueType>
class storm::solver::StandardGameSolver< ValueType >

Definition at line 13 of file StandardGameSolver.h.

Constructor & Destructor Documentation

◆ StandardGameSolver() [1/4]

template<typename ValueType>

storm::solver::StandardGameSolver< ValueType >::StandardGameSolver	(	storm::storage::SparseMatrix< storm::storage::sparse::state_type > const &	player1Matrix,
		storm::storage::SparseMatrix< ValueType > const &	player2Matrix,
		std::unique_ptr< LinearEquationSolverFactory< ValueType > > &&	linearEquationSolverFactory )

Definition at line 23 of file StandardGameSolver.cpp.

◆ StandardGameSolver() [2/4]

template<typename ValueType>

storm::solver::StandardGameSolver< ValueType >::StandardGameSolver	(	storm::storage::SparseMatrix< storm::storage::sparse::state_type > &&	player1Matrix,
		storm::storage::SparseMatrix< ValueType > &&	player2Matrix,
		std::unique_ptr< LinearEquationSolverFactory< ValueType > > &&	linearEquationSolverFactory )

Definition at line 35 of file StandardGameSolver.cpp.

◆ StandardGameSolver() [3/4]

template<typename ValueType>

storm::solver::StandardGameSolver< ValueType >::StandardGameSolver	(	std::vector< uint64_t > const &	player1Groups,
		storm::storage::SparseMatrix< ValueType > const &	player2Matrix,
		std::unique_ptr< LinearEquationSolverFactory< ValueType > > &&	linearEquationSolverFactory )

Definition at line 47 of file StandardGameSolver.cpp.

◆ StandardGameSolver() [4/4]

template<typename ValueType>

storm::solver::StandardGameSolver< ValueType >::StandardGameSolver	(	std::vector< uint64_t > &&	player1Groups,
		storm::storage::SparseMatrix< ValueType > &&	player2Matrix,
		std::unique_ptr< LinearEquationSolverFactory< ValueType > > &&	linearEquationSolverFactory )

Definition at line 58 of file StandardGameSolver.cpp.

Member Function Documentation

◆ clearCache()

template<typename ValueType>

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

overridevirtual

Reimplemented from storm::solver::GameSolver< ValueType >.

Definition at line 604 of file StandardGameSolver.cpp.

◆ repeatedMultiply()

template<typename ValueType>

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

overridevirtual

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.

Implements storm::solver::GameSolver< ValueType >.

Definition at line 387 of file StandardGameSolver.cpp.

◆ solveGame()

template<typename ValueType>

bool storm::solver::StandardGameSolver< 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

overridevirtual

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.

Implements storm::solver::GameSolver< ValueType >.

Definition at line 90 of file StandardGameSolver.cpp.

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

src/storm/solver/StandardGameSolver.h
src/storm/solver/StandardGameSolver.cpp

Public Member Functions

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ StandardGameSolver() [1/4]

◆ StandardGameSolver() [2/4]

◆ StandardGameSolver() [3/4]

◆ StandardGameSolver() [4/4]

Member Function Documentation

◆ clearCache()

◆ repeatedMultiply()

◆ solveGame()