From eb856076481329e32de1b2233dd88f318c277e4e Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 7 Mar 2017 14:36:00 +0100 Subject: [PATCH] Extended functionality of game solver: repeated multiply, scheduler hints --- src/storm/solver/AbstractGameSolver.cpp | 23 ++++++++- src/storm/solver/AbstractGameSolver.h | 19 +++++++ src/storm/solver/GameSolver.cpp | 69 ++++++++++++++++++++++++- src/storm/solver/GameSolver.h | 13 ++++- 4 files changed, 121 insertions(+), 3 deletions(-) diff --git a/src/storm/solver/AbstractGameSolver.cpp b/src/storm/solver/AbstractGameSolver.cpp index 0fe18ce9e..b2cd637ba 100644 --- a/src/storm/solver/AbstractGameSolver.cpp +++ b/src/storm/solver/AbstractGameSolver.cpp @@ -60,7 +60,28 @@ namespace storm { bool AbstractGameSolver::getRelative() const { return relative; } - + + template + void AbstractGameSolver::setSchedulerHint(storm::storage::TotalScheduler&& player1Scheduler, storm::storage::TotalScheduler&& player2Scheduler) { + player1SchedulerHint = player1Scheduler; + player2SchedulerHint = player2Scheduler; + } + + template + bool AbstractGameSolver::hasSchedulerHints() const { + return player1SchedulerHint.is_initialized() && player2SchedulerHint.is_initialized(); + } + + template + void AbstractGameSolver::setLowerBound(ValueType const& value) { + this->lowerBound = value; + } + + template + void AbstractGameSolver::setUpperBound(ValueType const& value) { + this->upperBound = value; + } + template class AbstractGameSolver; } diff --git a/src/storm/solver/AbstractGameSolver.h b/src/storm/solver/AbstractGameSolver.h index c5d8c4bc5..37935c911 100644 --- a/src/storm/solver/AbstractGameSolver.h +++ b/src/storm/solver/AbstractGameSolver.h @@ -33,6 +33,15 @@ namespace storm { */ AbstractGameSolver(double precision, uint_fast64_t maximalNumberOfIterations, bool relative); + /*! + * Sets schedulers that might be considered by the solver as an initial guess + */ + void setSchedulerHint(storm::storage::TotalScheduler&& player1Scheduler, storm::storage::TotalScheduler&& player2Scheduler); + bool hasSchedulerHints() const; + + void setLowerBound(ValueType const& value); + void setUpperBound(ValueType const& value); + void setTrackScheduler(bool trackScheduler = true); bool isTrackSchedulerSet() const; bool hasScheduler() const; @@ -59,6 +68,16 @@ namespace storm { // The scheduler for the corresponding players (if it could be successfully generated). mutable boost::optional> player1Scheduler; mutable boost::optional> player2Scheduler; + + // schedulers that might be considered by the solver as an initial guess + boost::optional player1SchedulerHint; + boost::optional player2SchedulerHint; + + boost::optional lowerBound; + boost::optional upperBound; + + + }; } } diff --git a/src/storm/solver/GameSolver.cpp b/src/storm/solver/GameSolver.cpp index d522a5368..599c6721b 100644 --- a/src/storm/solver/GameSolver.cpp +++ b/src/storm/solver/GameSolver.cpp @@ -20,12 +20,34 @@ 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. bool converged = false; uint_fast64_t numberOfPlayer1States = x.size(); std::vector tmpResult(numberOfPlayer1States); std::vector nondetResult(player2Matrix.getRowCount()); std::vector player2Result(player2Matrix.getRowGroupCount()); + + // check if we have a scheduler hint to apply + if(this->hasSchedulerHints()) { + //Get the rows of the player2matrix that are selected by the schedulers + //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& pl1Row = player1Matrix.getRow(pl1State, this->player1SchedulerHint->getChoice(pl1State)); + STORM_LOG_ASSERT(pl1Row.getNumberOfEntries()==1, "We assume that rows of player one have one entry."); + uint_fast64_t pl2State = pl1Row.begin()->getColumn(); + selectedRows[pl1State] = player2Matrix.getRowGroupIndices()[pl2State] + this->player2SchedulerHint->getChoice(pl1State); + } + //Get the matrix and the vector induced by this selection + auto inducedMatrix = player2Matrix.selectRowsFromRowIndexSequence(selectedRows, true); + inducedMatrix.convertToEquationSystem(); + storm::utility::vector::selectVectorValues(tmpResult, selectedRows, b); + auto submatrixSolver = storm::solver::GeneralLinearEquationSolverFactory().create(std::move(inducedMatrix)); + if (this->lowerBound) { submatrixSolver->setLowerBound(this->lowerBound.get()); } + if (this->upperBound) { submatrixSolver->setUpperBound(this->upperBound.get()); } + submatrixSolver->solveEquations(x, tmpResult); + } // Now perform the actual value iteration. uint_fast64_t iterations = 0; @@ -111,6 +133,51 @@ namespace storm { this->player1Scheduler = std::make_unique(std::move(player1Choices)); } } + + template + void GameSolver::repeatedMultiply(OptimizationDirection player1Goal, OptimizationDirection player2Goal, std::vector& x, std::vector const* b, uint_fast64_t n) const { + // Set up the environment for iterations + uint_fast64_t numberOfPlayer1States = x.size(); + std::vector tmpResult(numberOfPlayer1States); + std::vector nondetResult(player2Matrix.getRowCount()); + std::vector player2Result(player2Matrix.getRowGroupCount()); + + for (uint_fast64_t iteration = 0; iteration < n; ++iteration) { + player2Matrix.multiplyWithVector(x, nondetResult); + + if(b != nullptr) { + storm::utility::vector::addVectors(*b, nondetResult, nondetResult); + } + + storm::utility::vector::reduceVectorMinOrMax(player2Goal, nondetResult, player2Result, player2Matrix.getRowGroupIndices()); + + 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; + + // Now iterate through the different values and pick the extremal one. + if (player1Goal == OptimizationDirection::Minimize) { + for (; it != ite; ++it) { + tmpResult[pl1State] = std::min(tmpResult[pl1State], player2Result[it->getColumn()]); + } + } else { + for (; it != ite; ++it) { + tmpResult[pl1State] = std::max(tmpResult[pl1State], player2Result[it->getColumn()]); + } + } + } else { + tmpResult[pl1State] = storm::utility::zero(); + } + } + std::swap(x, tmpResult); + } + } template storm::storage::SparseMatrix const& GameSolver::getPlayer1Matrix() const { @@ -121,7 +188,7 @@ namespace storm { storm::storage::SparseMatrix const& GameSolver::getPlayer2Matrix() const { return player2Matrix; } - + template class GameSolver; } } diff --git a/src/storm/solver/GameSolver.h b/src/storm/solver/GameSolver.h index 458e6c594..f4f3dcf6d 100644 --- a/src/storm/solver/GameSolver.h +++ b/src/storm/solver/GameSolver.h @@ -50,7 +50,18 @@ namespace storm { */ virtual void solveGame(OptimizationDirection player1Goal, OptimizationDirection player2Goal, std::vector& x, std::vector const& b) const; - + /*! + * Performs n multiplications of the form + * reduce(player1Matrix * reduce(player2Matrix * x + b)) + * + * @param player1Goal Sets whether player 1 wants to minimize or maximize. + * @param player2Goal Sets whether player 2 wants to minimize or maximize. + * @param 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) + * @param b The vector to add after matrix-vector multiplication. + * @param n The number of times we perform the multiplication + */ + virtual void repeatedMultiply(OptimizationDirection player1Goal, OptimizationDirection player2Goal, std::vector& x, std::vector const* b, uint_fast64_t n) const; + storm::storage::SparseMatrix const& getPlayer2Matrix() const; storm::storage::SparseMatrix const& getPlayer1Matrix() const;