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

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

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	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 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 24 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 40 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 56 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 71 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 621 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 404 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 107 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()