Storm
A Modern Probabilistic Model Checker
|
#include <StandardGameSolver.h>
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 |
![]() | |
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. | |
![]() | |
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 | |
![]() | |
enum class | BoundType { Global , Local , Any } |
![]() | |
GameSolver () | |
![]() | |
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. | |
![]() | |
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 |
![]() | |
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 |
Definition at line 13 of file StandardGameSolver.h.
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.
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.
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.
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.
|
overridevirtual |
Reimplemented from storm::solver::GameSolver< ValueType >.
Definition at line 621 of file StandardGameSolver.cpp.
|
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.
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.
|
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.
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.