Storm
A Modern Probabilistic Model Checker
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
storm::solver::StandardGameSolver< ValueType > Class Template Reference

#include <StandardGameSolver.h>

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

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::BitVectorrelevantValues
 
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
player1DirSets whether player 1 wants to minimize or maximize.
player2DirSets whether player 2 wants to minimize or maximize.
xThe 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.
bIf not null, this vector is added after each multiplication.
nSpecifies 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
player1DirSets whether player 1 wants to minimize or maximize.
player2DirSets whether player 2 wants to minimize or maximize.
xThe initial guess of the solution. For correctness, the guess has to be less (or equal) to the final solution (unless both players minimize)
bThe vector to add after matrix-vector multiplication.
player1ChoicesIf provided along with the storage for player 2 choices, the scheduler decisions are tracked within these two vectors.
player2ChoicesIf 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: