diff --git a/src/modelchecker/region/ApproximationModel.cpp b/src/modelchecker/region/ApproximationModel.cpp index 4acd5377d..919c4c9f4 100644 --- a/src/modelchecker/region/ApproximationModel.cpp +++ b/src/modelchecker/region/ApproximationModel.cpp @@ -277,8 +277,6 @@ namespace storm { //TODO: at this point, set policy to the one stored in the region. invokeSolver(computeLowerBounds, policy); - //TODO: policy for games. - if(policy.empty()) return this->solverData.result[this->solverData.initialStateIndex]; //This can be deleted as soon as policy for games is supported //TODO: (maybe) when a few parameters are mapped to another value, build a "nicer" scheduler and check whether it induces values that are more optimal. //Get the set of parameters which are (according to the policy) always mapped to the same region boundary. //First, collect all (relevant) parameters, i.e., the ones that are set to the lower or upper boundary. @@ -403,7 +401,10 @@ namespace storm { void ApproximationModel, double>::invokeSolver(bool computeLowerBounds, Policy& policy){ storm::solver::SolveGoal player2Goal(computeLowerBounds); std::unique_ptr> solver = storm::utility::solver::GameSolverFactory().create(this->solverData.player1Matrix, this->matrixData.matrix); - solver->solveGame(this->solverData.player1Goal.direction(), player2Goal.direction(), this->solverData.result, this->vectorData.vector); + solver->setPolicyTracking(); + solver->solveGame(this->solverData.player1Goal.direction(), player2Goal.direction(), this->solverData.result, this->vectorData.vector, &this->solverData.lastPlayer1Policy, &policy); + this->solverData.lastPlayer1Policy = solver->getPlayer1Policy(); + policy = solver->getPlayer2Policy(); } diff --git a/src/solver/AbstractGameSolver.cpp b/src/solver/AbstractGameSolver.cpp index 76ea87bd1..56f6e0974 100644 --- a/src/solver/AbstractGameSolver.cpp +++ b/src/solver/AbstractGameSolver.cpp @@ -18,5 +18,19 @@ namespace storm { AbstractGameSolver::AbstractGameSolver(double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : precision(precision), maximalNumberOfIterations(maximalNumberOfIterations), relative(relative) { // Intentionally left empty. } + + void AbstractGameSolver::setPolicyTracking(bool setToTrue) { + this->trackPolicies = setToTrue; + } + + std::vector AbstractGameSolver::getPlayer1Policy() const { + assert(!this->player1Policy.empty()); + return player1Policy; + } + + std::vector AbstractGameSolver::getPlayer2Policy() const { + assert(!this->player2Policy.empty()); + return player2Policy; + } } } \ No newline at end of file diff --git a/src/solver/AbstractGameSolver.h b/src/solver/AbstractGameSolver.h index 693b4defa..05f420a80 100644 --- a/src/solver/AbstractGameSolver.h +++ b/src/solver/AbstractGameSolver.h @@ -2,6 +2,8 @@ #define STORM_SOLVER_ABSTRACTGAMESOLVER_H_ #include +#include "src/storage/sparse/StateType.h" +#include "src/utility/vector.h" namespace storm { namespace solver { @@ -23,6 +25,11 @@ namespace storm { * @param relative A flag indicating whether a relative or an absolute stopping criterion is to be used. */ AbstractGameSolver(double precision, uint_fast64_t maximalNumberOfIterations, bool relative); + + void setPolicyTracking(bool setToTrue=true); + + std::vector getPlayer1Policy() const; + std::vector getPlayer2Policy() const; protected: // The precision to achieve. @@ -33,6 +40,14 @@ namespace storm { // A flag indicating whether a relative or an absolute stopping criterion is to be used. bool relative; + + // Whether we track the policies we generate. + bool trackPolicies; + + // The policies for the different players + mutable std::vector player1Policy; + mutable std::vector player2Policy; + }; } } diff --git a/src/solver/GameSolver.cpp b/src/solver/GameSolver.cpp index 752328e11..29201ad99 100644 --- a/src/solver/GameSolver.cpp +++ b/src/solver/GameSolver.cpp @@ -1,7 +1,8 @@ #include "src/solver/GameSolver.h" +#include "src/solver/LinearEquationSolver.h" +#include "src/utility/solver.h" #include "src/storage/SparseMatrix.h" - #include "src/utility/vector.h" namespace storm { @@ -17,10 +18,30 @@ namespace storm { } template - void GameSolver::solveGame(OptimizationDirection player1Goal, OptimizationDirection player2Goal, std::vector& x, std::vector const& b) const { - // Set up the environment for value iteration. + void GameSolver::solveGame(OptimizationDirection player1Goal, OptimizationDirection player2Goal, std::vector& x, std::vector const& b, std::vector* initialPlayer1Policy, std::vector* initialPlayer2Policy) const { uint_fast64_t numberOfPlayer1States = x.size(); - + + if(initialPlayer1Policy != nullptr || initialPlayer2Policy != nullptr){ + //Either we work with both policies or none of them + assert(initialPlayer1Policy != nullptr && initialPlayer2Policy != nullptr); + //The policies select certain rows in the matrix of player2. + //However, note that rows can be selected more then once and in an arbitrary order. + std::vector selectedRows(numberOfPlayer1States); + for (uint_fast64_t pl1State = 0; pl1State < numberOfPlayer1States; ++pl1State){ + auto const& pl1Choice = player1Matrix.getRow(player1Matrix.getRowGroupIndices()[pl1State] + (*initialPlayer1Policy)[pl1State]); + assert(pl1Choice.getNumberOfEntries()==1); + uint_fast64_t pl2State = pl1Choice.begin()->getColumn(); + selectedRows[pl1State] = player2Matrix.getRowGroupIndices()[pl2State] + (*initialPlayer2Policy)[pl2State]; + } + storm::storage::SparseMatrix eqSysMatrix = player2Matrix.selectRowsFromRowIndexSequence(selectedRows, true); + eqSysMatrix.convertToEquationSystem(); + std::unique_ptr> solver = storm::utility::solver::LinearEquationSolverFactory().create(eqSysMatrix); + std::vector subB(numberOfPlayer1States); + storm::utility::vector::selectVectorValues(subB, selectedRows, b); + solver->solveEquationSystem(x, subB); + } + + // Set up the environment for value iteration. bool converged = false; std::vector tmpResult(numberOfPlayer1States); std::vector nondetResult(player2Matrix.getRowCount()); @@ -69,6 +90,44 @@ namespace storm { ++iterations; } while (!converged && iterations < maximalNumberOfIterations); + + STORM_LOG_WARN_COND(converged, "Iterative solver for stochastic two player games did not converge after " << iterations << "iterations."); + + if(this->trackPolicies){ + this->player2Policy = std::vector(player2Matrix.getRowGroupCount()); + storm::utility::vector::reduceVectorMinOrMax(player2Goal, nondetResult, player2Result, player2Matrix.getRowGroupIndices(), &this->player2Policy); + + this->player1Policy = std::vector(numberOfPlayer1States, 0); + for (uint_fast64_t pl1State = 0; pl1State < numberOfPlayer1States; ++pl1State) { + storm::storage::SparseMatrix::const_rows relevantRows = player1Matrix.getRowGroup(pl1State); + if (relevantRows.getNumberOfEntries() > 0) { + storm::storage::SparseMatrix::const_iterator it = relevantRows.begin(); + storm::storage::SparseMatrix::const_iterator ite = relevantRows.end(); + // Set the first value. + tmpResult[pl1State] = player2Result[it->getColumn()]; + ++it; + storm::storage::sparse::state_type localChoice = 1; + // Now iterate through the different values and pick the extremal one. + if (player1Goal == OptimizationDirection::Minimize) { + for (; it != ite; ++it, ++localChoice) { + if(player2Result[it->getColumn()] < tmpResult[pl1State]){ + tmpResult[pl1State] = player2Result[it->getColumn()]; + this->player1Policy[pl1State] = localChoice; + } + } + } else { + for (; it != ite; ++it, ++localChoice) { + if(player2Result[it->getColumn()] > tmpResult[pl1State]){ + tmpResult[pl1State] = player2Result[it->getColumn()]; + this->player1Policy[pl1State] = localChoice; + } + } + } + } else { + STORM_LOG_ERROR("There is no choice for Player 1 at state " << pl1State << " in the stochastic two player game. This is not expected!"); + } + } + } } template class GameSolver; diff --git a/src/solver/GameSolver.h b/src/solver/GameSolver.h index 8218768cc..06a906836 100644 --- a/src/solver/GameSolver.h +++ b/src/solver/GameSolver.h @@ -45,9 +45,11 @@ namespace storm { * @param player2Goal Sets whether player 2 wants to minimize or maximize. * @param x The initial guess of the solution. * @param b The vector to add after matrix-vector multiplication. + * @param initialPlayer1Policy A policy that selects rows in every rowgroup of player1. This will be used as an initial guess + * @param initialPlayer2Policy A policy that selects rows in every rowgroup of player2. This will be used as an initial guess * @return The solution vector in the for of the vector x. */ - virtual void solveGame(OptimizationDirection player1Goal, OptimizationDirection player2Goal, std::vector& x, std::vector const& b) const; + virtual void solveGame(OptimizationDirection player1Goal, OptimizationDirection player2Goal, std::vector& x, std::vector const& b, std::vector* initialPlayer1Policy = nullptr, std::vector* initialPlayer2Policy = nullptr) const; private: // The matrix defining the choices of player 1. @@ -55,6 +57,7 @@ namespace storm { // The matrix defining the choices of player 2. storm::storage::SparseMatrix const& player2Matrix; + }; } } diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index 015809dfb..ba2ff746a 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -718,6 +718,48 @@ namespace storm { return matrixBuilder.build(); } + template + SparseMatrix SparseMatrix::selectRowsFromRowIndexSequence(std::vector const& rowIndexSequence, bool insertDiagonalEntries) const{ + // First, we need to count how many non-zero entries the resulting matrix will have and reserve space for + // diagonal entries if requested. + index_type newEntries = 0; + for(index_type row = 0, rowEnd = rowIndexSequence.size(); row < rowEnd; ++row) { + bool foundDiagonalElement = false; + for (const_iterator it = this->begin(rowIndexSequence[row]), ite = this->end(rowIndexSequence[row]); it != ite; ++it) { + if (it->getColumn() == row) { + foundDiagonalElement = true; + } + ++newEntries; + } + if (insertDiagonalEntries && !foundDiagonalElement) { + ++newEntries; + } + } + + // Now create the matrix to be returned with the appropriate size. + SparseMatrixBuilder matrixBuilder(rowIndexSequence.size(), columnCount, newEntries); + + // Copy over the selected rows from the source matrix. + for(index_type row = 0, rowEnd = rowIndexSequence.size(); row < rowEnd; ++row) { + bool insertedDiagonalElement = false; + for (const_iterator it = this->begin(rowIndexSequence[row]), ite = this->end(rowIndexSequence[row]); it != ite; ++it) { + if (it->getColumn() == row) { + insertedDiagonalElement = true; + } else if (insertDiagonalEntries && !insertedDiagonalElement && it->getColumn() > row) { + matrixBuilder.addNextValue(row, row, storm::utility::zero()); + insertedDiagonalElement = true; + } + matrixBuilder.addNextValue(row, it->getColumn(), it->getValue()); + } + if (insertDiagonalEntries && !insertedDiagonalElement) { + matrixBuilder.addNextValue(row, row, storm::utility::zero()); + } + } + + // Finally create matrix and return result. + return matrixBuilder.build(); + } + template SparseMatrix SparseMatrix::transpose(bool joinGroups, bool keepZeros) const { index_type rowCount = this->getColumnCount(); diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index c31e0b344..68417d22d 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -633,6 +633,17 @@ namespace storm { */ SparseMatrix selectRowsFromRowGroups(std::vector const& rowGroupToRowIndexMapping, bool insertDiagonalEntries = true) const; + /*! + * Selects the rows that are given by the sequence of row indices, allowing to select rows arbitrarily often and with an arbitrary order + * The resulting matrix will have a trivial row grouping + * + * @param rowIndexSequence the sequence of row indices which specifies, which rows are contained in the new matrix + * @param insertDiagonalEntries If set to true, the resulting matrix will have zero entries in column i for + * each row. This can then be used for inserting other values later. + * @return A matrix which rows are selected from this matrix according to the given index sequence + */ + SparseMatrix selectRowsFromRowIndexSequence(std::vector const& rowIndexSequence, bool insertDiagonalEntries = true) const; + /*! * Transposes the matrix. * diff --git a/src/utility/vector.h b/src/utility/vector.h index 38d5459f0..ff2770677 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -149,6 +149,20 @@ namespace storm { } } + /*! + * Selects values from a vector at the specified sequence of indices and writes them into another vector + * + * @param vector The vector into which the selected elements are written. + * @param indexSequence a sequence of indices at which the desired values can be found + * @param values the values from which to select + */ + template + void selectVectorValues(std::vector& vector, std::vector const& indexSequence, std::vector const& values) { + for (uint_fast64_t vectorIndex = 0; vectorIndex < vector.size(); ++vectorIndex){ + vector[vectorIndex] = values[indexSequence[vectorIndex]]; + } + } + /*! * Selects values from a vector at the specified positions and writes them into another vector as often as given by * the size of the corresponding group of elements.