From d557ef10753a050b0831a7dfd7938be3c9342eb9 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 27 Mar 2018 22:21:02 +0200 Subject: [PATCH] started to make game solver flexible enough to also solve the (explicit) games of game-based abstraction --- .../SparseMdpParameterLiftingModelChecker.cpp | 6 +- .../abstraction/GameBasedMdpModelChecker.cpp | 29 +- src/storm/solver/GameSolver.cpp | 2 +- src/storm/solver/GameSolver.h | 14 +- src/storm/solver/MinMaxLinearEquationSolver.h | 2 +- src/storm/solver/StandardGameSolver.cpp | 266 ++++++++++++------ src/storm/solver/StandardGameSolver.h | 22 +- src/storm/storage/SparseMatrix.h | 2 +- 8 files changed, 233 insertions(+), 110 deletions(-) diff --git a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp index 0aa70d974..c58426f79 100644 --- a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp @@ -275,8 +275,8 @@ namespace storm { } // Invoke the solver - if(stepBound) { - assert(*stepBound > 0); + if (stepBound) { + STORM_LOG_ASSERT(*stepBound > 0, "Expected positive step bound."); solver->repeatedMultiply(env, this->currentCheckTask->getOptimizationDirection(), dirForParameters, x, ¶meterLifter->getVector(), *stepBound); } else { solver->solveGame(env, this->currentCheckTask->getOptimizationDirection(), dirForParameters, x, parameterLifter->getVector()); @@ -293,7 +293,7 @@ namespace storm { // Get the result for the complete model (including maybestates) std::vector result = resultsForNonMaybeStates; auto maybeStateResIt = x.begin(); - for(auto const& maybeState : maybeStates) { + for (auto const& maybeState : maybeStates) { result[maybeState] = *maybeStateResIt; ++maybeStateResIt; } diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 004d7993d..2c10f2f2d 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -391,31 +391,30 @@ namespace storm { template ExplicitQuantitativeResult computeQuantitativeResult(Environment const& env, storm::OptimizationDirection player1Direction, storm::OptimizationDirection player2Direction, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Groups, ExplicitQualitativeGameResultMinMax const& qualitativeResult, storm::storage::BitVector const& maybeStates, ExplicitGameStrategyPair& minStrategyPair) { - + + bool player1Min = player1Direction == storm::OptimizationDirection::Minimize; bool player2Min = player2Direction == storm::OptimizationDirection::Minimize; + auto const& player1Prob0States = player2Min ? qualitativeResult.getProb0Min().asExplicitQualitativeGameResult().getPlayer1States() : qualitativeResult.getProb0Max().asExplicitQualitativeGameResult().getPlayer1States(); + auto const& player1Prob1States = player2Min ? qualitativeResult.getProb1Min().asExplicitQualitativeGameResult().getPlayer1States() : qualitativeResult.getProb1Max().asExplicitQualitativeGameResult().getPlayer1States(); auto const& player2Prob0States = player2Min ? qualitativeResult.getProb0Min().asExplicitQualitativeGameResult().getPlayer2States() : qualitativeResult.getProb0Max().asExplicitQualitativeGameResult().getPlayer2States(); auto const& player2Prob1States = player2Min ? qualitativeResult.getProb1Min().asExplicitQualitativeGameResult().getPlayer2States() : qualitativeResult.getProb1Max().asExplicitQualitativeGameResult().getPlayer2States(); // Determine which rows to keep. - storm::storage::BitVector rows(transitionMatrix.getRowCount()); + storm::storage::BitVector player2MaybeStates(transitionMatrix.getRowCount()); for (uint64_t player2State = 0; player2State < transitionMatrix.getRowGroupCount(); ++player2State) { if (!player2Prob0States.get(player2State) && !player2Prob1States.get(player2State)) { - // Mark all rows that have a maybe state as a successor. - for (uint64_t row = transitionMatrix.getRowGroupIndices()[player2State]; row < transitionMatrix.getRowGroupIndices()[player2State + 1]; ++row) { - bool hasMaybeStateSuccessor = false; - for (auto const& entry : transitionMatrix.getRow(row)) { - if (maybeStates.get(entry.getColumn())) { - hasMaybeStateSuccessor = true; - } - } - if (!hasMaybeStateSuccessor) { - rows.set(row); - } - } + player2MaybeStates.set(player2State); } } - storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, player2MaybeStates, <#const storm::storage::BitVector &columnConstraint#>) + storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, player2MaybeStates, maybeStates); + std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(player2MaybeStates, maybeStates); + + auto multiplier = storm::solver::MultiplierFactory().create(env, submatrix); + multiplier->repeatedMultiplyAndReduce(env, goal.direction(), subresult, &b, stepBound); + + + env. } template diff --git a/src/storm/solver/GameSolver.cpp b/src/storm/solver/GameSolver.cpp index 9c3e5ad8e..0710cc9f2 100644 --- a/src/storm/solver/GameSolver.cpp +++ b/src/storm/solver/GameSolver.cpp @@ -10,7 +10,7 @@ namespace storm { namespace solver { template - GameSolver::GameSolver() : trackSchedulers(false), cachingEnabled(false) { + GameSolver::GameSolver() : trackSchedulers(false), uniqueSolution(false), cachingEnabled(false) { // Intentionally left empty } diff --git a/src/storm/solver/GameSolver.h b/src/storm/solver/GameSolver.h index fd9e63667..07cb16e88 100644 --- a/src/storm/solver/GameSolver.h +++ b/src/storm/solver/GameSolver.h @@ -111,6 +111,16 @@ namespace storm { * Clears the currently cached data that has been stored during previous calls of the solver. */ virtual void clearCache() const; + + /*! + * Sets whether the solution to the min max equation system is known to be unique. + */ + void setHasUniqueSolution(bool value = true); + + /*! + * Retrieves whether the solution to the min max equation system is assumed to be unique + */ + bool hasUniqueSolution() const; protected: @@ -128,9 +138,11 @@ namespace storm { boost::optional> player2ChoicesHint; private: + /// Whether the solver can assume that the min-max equation system has a unique solution + bool uniqueSolution; + /// Whether some of the generated data during solver calls should be cached. bool cachingEnabled; - }; template diff --git a/src/storm/solver/MinMaxLinearEquationSolver.h b/src/storm/solver/MinMaxLinearEquationSolver.h index 00788089c..9ea9ac90a 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.h +++ b/src/storm/solver/MinMaxLinearEquationSolver.h @@ -170,7 +170,7 @@ namespace storm { boost::optional> initialScheduler; private: - // Whether the solver can assume that the min-max equation system has a unique solution + /// Whether the solver can assume that the min-max equation system has a unique solution bool uniqueSolution; /// Whether some of the generated data during solver calls should be cached. diff --git a/src/storm/solver/StandardGameSolver.cpp b/src/storm/solver/StandardGameSolver.cpp index 6140a5c15..07512b23d 100644 --- a/src/storm/solver/StandardGameSolver.cpp +++ b/src/storm/solver/StandardGameSolver.cpp @@ -16,12 +16,22 @@ namespace storm { namespace solver { template - StandardGameSolver::StandardGameSolver(storm::storage::SparseMatrix const& player1Matrix, storm::storage::SparseMatrix const& player2Matrix, std::unique_ptr>&& linearEquationSolverFactory) : linearEquationSolverFactory(std::move(linearEquationSolverFactory)), localP1Matrix(nullptr), localP2Matrix(nullptr), player1Matrix(player1Matrix), player2Matrix(player2Matrix) { + StandardGameSolver::StandardGameSolver(storm::storage::SparseMatrix const& player1Matrix, storm::storage::SparseMatrix const& player2Matrix, std::unique_ptr>&& linearEquationSolverFactory) : linearEquationSolverFactory(std::move(linearEquationSolverFactory)), localPlayer1Grouping(nullptr), localPlayer1Matrix(nullptr), localPlayer2Matrix(nullptr), player1Grouping(nullptr), player1Matrix(&player1Matrix), player2Matrix(player2Matrix) { // Intentionally left empty. } template - StandardGameSolver::StandardGameSolver(storm::storage::SparseMatrix&& player1Matrix, storm::storage::SparseMatrix&& player2Matrix, std::unique_ptr>&& linearEquationSolverFactory) : linearEquationSolverFactory(std::move(linearEquationSolverFactory)), localP1Matrix(std::make_unique>(std::move(player1Matrix))), localP2Matrix(std::make_unique>(std::move(player2Matrix))), player1Matrix(*localP1Matrix), player2Matrix(*localP2Matrix) { + StandardGameSolver::StandardGameSolver(storm::storage::SparseMatrix&& player1Matrix, storm::storage::SparseMatrix&& player2Matrix, std::unique_ptr>&& linearEquationSolverFactory) : linearEquationSolverFactory(std::move(linearEquationSolverFactory)), localPlayer1Grouping(nullptr), localPlayer1Matrix(std::make_unique>(std::move(player1Matrix))), localPlayer2Matrix(std::make_unique>(std::move(player2Matrix))), player1Grouping(nullptr), player1Matrix(localPlayer1Matrix.get()), player2Matrix(*localPlayer2Matrix) { + // Intentionally left empty. + } + + template + StandardGameSolver::StandardGameSolver(std::vector const& player1Grouping, storm::storage::SparseMatrix const& player2Matrix, std::unique_ptr>&& linearEquationSolverFactory) : linearEquationSolverFactory(std::move(linearEquationSolverFactory)), localPlayer1Grouping(nullptr), localPlayer1Matrix(nullptr), localPlayer2Matrix(nullptr), player1Grouping(&player1Grouping), player1Matrix(nullptr), player2Matrix(player2Matrix) { + + } + + template + StandardGameSolver::StandardGameSolver(std::vector&& player1Grouping, storm::storage::SparseMatrix&& player2Matrix, std::unique_ptr>&& linearEquationSolverFactory) : linearEquationSolverFactory(std::move(linearEquationSolverFactory)), localPlayer1Grouping(std::make_unique>(std::move(player1Grouping))), localPlayer1Matrix(nullptr), localPlayer2Matrix(std::make_unique>(std::move(player2Matrix))), player1Grouping(localPlayer1Grouping.get()), player1Matrix(nullptr), player2Matrix(*localPlayer2Matrix) { // Intentionally left empty. } @@ -63,20 +73,30 @@ namespace storm { bool StandardGameSolver::solveGamePolicyIteration(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector& x, std::vector const& b) const { // Create the initial choice selections. - std::vector player1Choices = this->hasSchedulerHints() ? this->player1ChoicesHint.get() : std::vector(this->player1Matrix.getRowGroupCount(), 0); + std::vector player1Choices; + if (this->hasSchedulerHints()) { + player1Choices = this->player1ChoicesHint.get(); + } else if (this->player1RepresentedByMatrix()) { + // Player 1 represented by matrix. + player1Choices = std::vector(this->getPlayer1Matrix().getRowGroupCount(), 0); + } else { + // Player 1 represented by grouping of player 2 states. + player1Choices = this->getPlayer1Grouping(); + player1Choices.resize(player1Choices.size() - 1); + } std::vector player2Choices = this->hasSchedulerHints() ? this->player2ChoicesHint.get() : std::vector(this->player2Matrix.getRowGroupCount(), 0); - if(!auxiliaryP2RowGroupVector) { + if (!auxiliaryP2RowGroupVector) { auxiliaryP2RowGroupVector = std::make_unique>(this->player2Matrix.getRowGroupCount()); } - if(!auxiliaryP1RowGroupVector) { - auxiliaryP1RowGroupVector = std::make_unique>(this->player1Matrix.getRowGroupCount()); + if (!auxiliaryP1RowGroupVector) { + auxiliaryP1RowGroupVector = std::make_unique>(this->player1Matrix->getRowGroupCount()); } std::vector& subB = *auxiliaryP1RowGroupVector; uint64_t maxIter = env.solver().game().getMaximalNumberOfIterations(); - // The linear equation solver should be at least as precise as this solver + // The linear equation solver should be at least as precise as this solver. std::unique_ptr environmentOfSolverStorage; auto precOfSolver = env.solver().getPrecisionOfLinearEquationSolver(env.solver().getLinearEquationSolverType()); if (!storm::NumberTraits::IsExact) { @@ -104,8 +124,13 @@ namespace storm { submatrix.convertToEquationSystem(); } auto submatrixSolver = linearEquationSolverFactory->create(environmentOfSolver, std::move(submatrix)); - if (this->lowerBound) { submatrixSolver->setLowerBound(this->lowerBound.get()); } - if (this->upperBound) { submatrixSolver->setUpperBound(this->upperBound.get()); } + if (this->lowerBound) { + submatrixSolver->setLowerBound(this->lowerBound.get()); + + } + if (this->upperBound) { + submatrixSolver->setUpperBound(this->upperBound.get()); + } submatrixSolver->setCachingEnabled(true); Status status = Status::InProgress; @@ -140,7 +165,7 @@ namespace storm { this->player2SchedulerChoices = std::move(player2Choices); } - if(!this->isCachingEnabled()) { + if (!this->isCachingEnabled()) { clearCache(); } @@ -163,25 +188,21 @@ namespace storm { multiplierPlayer2Matrix = storm::solver::MultiplierFactory().create(env, player2Matrix); } - if (!auxiliaryP2RowVector) { - auxiliaryP2RowVector = std::make_unique>(player2Matrix.getRowCount()); - } - if (!auxiliaryP2RowGroupVector) { auxiliaryP2RowGroupVector = std::make_unique>(player2Matrix.getRowGroupCount()); } if (!auxiliaryP1RowGroupVector) { - auxiliaryP1RowGroupVector = std::make_unique>(player1Matrix.getRowGroupCount()); + auxiliaryP1RowGroupVector = std::make_unique>(this->getNumberOfPlayer1States()); } ValueType precision = storm::utility::convertNumber(env.solver().game().getPrecision()); bool relative = env.solver().game().getRelativeTerminationCriterion(); uint64_t maxIter = env.solver().game().getMaximalNumberOfIterations(); - std::vector& multiplyResult = *auxiliaryP2RowVector; - std::vector& reducedMultiplyResult = *auxiliaryP2RowGroupVector; - + std::vector& reducedPlayer2Result = *auxiliaryP2RowGroupVector; + + bool trackSchedulersInValueIteration = this->isTrackSchedulersSet() && !this->hasUniqueSolution(); if (this->hasSchedulerHints()) { // Solve the equation system induced by the two schedulers. storm::storage::SparseMatrix submatrix; @@ -190,9 +211,25 @@ namespace storm { submatrix.convertToEquationSystem(); } auto submatrixSolver = linearEquationSolverFactory->create(env, std::move(submatrix)); - if (this->lowerBound) { submatrixSolver->setLowerBound(this->lowerBound.get()); } - if (this->upperBound) { submatrixSolver->setUpperBound(this->upperBound.get()); } + if (this->lowerBound) { + submatrixSolver->setLowerBound(this->lowerBound.get()); + + } + if (this->upperBound) { + submatrixSolver->setUpperBound(this->upperBound.get()); + } submatrixSolver->solveEquations(env, x, *auxiliaryP1RowGroupVector); + + // If requested, we store the scheduler for retrieval. Initialize the schedulers to the hint we have. + if (trackSchedulersInValueIteration) { + this->player1SchedulerChoices = this->player1ChoicesHint.get(); + this->player2SchedulerChoices = this->player2ChoicesHint.get(); + } + } else if (trackSchedulersInValueIteration) { + // If requested, we store the scheduler for retrieval. Create empty schedulers here so we can fill them + // during VI. + this->player1SchedulerChoices = std::vector(this->getNumberOfPlayer1States(), 0); + this->player2SchedulerChoices = std::vector(this->getNumberOfPlayer2States(), 0); } std::vector* newX = auxiliaryP1RowGroupVector.get(); @@ -203,7 +240,7 @@ namespace storm { Status status = Status::InProgress; while (status == Status::InProgress) { - multiplyAndReduce(env, player1Dir, player2Dir, *currentX, &b, *multiplierPlayer2Matrix, multiplyResult, reducedMultiplyResult, *newX); + multiplyAndReduce(env, player1Dir, player2Dir, *currentX, &b, *multiplierPlayer2Matrix, reducedPlayer2Result, *newX, trackSchedulersInValueIteration ? &this->getPlayer1SchedulerChoices() : nullptr, trackSchedulersInValueIteration ? &this->getPlayer2SchedulerChoices() : nullptr); // Determine whether the method converged. if (storm::utility::vector::equalModuloPrecision(*currentX, *newX, precision, relative)) { @@ -225,13 +262,13 @@ namespace storm { } // If requested, we store the scheduler for retrieval. - if (this->isTrackSchedulersSet()) { - this->player1SchedulerChoices = std::vector(player1Matrix.getRowGroupCount(), 0); - this->player2SchedulerChoices = std::vector(player2Matrix.getRowGroupCount(), 0); + if (this->isTrackSchedulersSet() && this->hasUniqueSolution()) { + this->player1SchedulerChoices = std::vector(this->getNumberOfPlayer1States(), 0); + this->player2SchedulerChoices = std::vector(this->getNumberOfPlayer2States(), 0); extractChoices(player1Dir, player2Dir, x, b, *auxiliaryP2RowGroupVector, this->player1SchedulerChoices.get(), this->player2SchedulerChoices.get()); } - if(!this->isCachingEnabled()) { + if (!this->isCachingEnabled()) { clearCache(); } @@ -245,54 +282,53 @@ namespace storm { multiplierPlayer2Matrix = storm::solver::MultiplierFactory().create(env, player2Matrix); } - if (!auxiliaryP2RowVector) { - auxiliaryP2RowVector = std::make_unique>(player2Matrix.getRowCount()); - } - if (!auxiliaryP2RowGroupVector) { auxiliaryP2RowGroupVector = std::make_unique>(player2Matrix.getRowGroupCount()); } - std::vector& multiplyResult = *auxiliaryP2RowVector; - std::vector& reducedMultiplyResult = *auxiliaryP2RowGroupVector; + std::vector& reducedPlayer2Result = *auxiliaryP2RowGroupVector; for (uint_fast64_t iteration = 0; iteration < n; ++iteration) { - multiplyAndReduce(env, player1Dir, player2Dir, x, b, *multiplierPlayer2Matrix, multiplyResult, reducedMultiplyResult, x); + multiplyAndReduce(env, player1Dir, player2Dir, x, b, *multiplierPlayer2Matrix, reducedPlayer2Result, x); } - if(!this->isCachingEnabled()) { + if (!this->isCachingEnabled()) { clearCache(); } } template - void StandardGameSolver::multiplyAndReduce(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector& x, std::vector const* b, storm::solver::Multiplier const& multiplier, std::vector& multiplyResult, std::vector& p2ReducedMultiplyResult, std::vector& p1ReducedMultiplyResult) const { + void StandardGameSolver::multiplyAndReduce(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector& x, std::vector const* b, storm::solver::Multiplier const& multiplier, std::vector& player2ReducedResult, std::vector& player1ReducedResult, std::vector* player1SchedulerChoices, std::vector* player2SchedulerChoices) const { - multiplier.multiply(env, x, b, multiplyResult); + multiplier.multiplyAndReduce(env, player2Dir, x, b, player2ReducedResult, player2SchedulerChoices); - storm::utility::vector::reduceVectorMinOrMax(player2Dir, multiplyResult, p2ReducedMultiplyResult, player2Matrix.getRowGroupIndices()); - - uint_fast64_t pl1State = 0; - for (auto& result : p1ReducedMultiplyResult) { - storm::storage::SparseMatrix::const_rows relevantRows = player1Matrix.getRowGroup(pl1State); - STORM_LOG_ASSERT(relevantRows.getNumberOfEntries() != 0, "There is a choice of player 1 that does not lead to any player 2 choice"); - auto it = relevantRows.begin(); - auto ite = relevantRows.end(); - - // Set the first value. - result = p2ReducedMultiplyResult[it->getColumn()]; - ++it; - - // Now iterate through the different values and pick the extremal one. - if (player1Dir == OptimizationDirection::Minimize) { - for (; it != ite; ++it) { - result = std::min(result, p2ReducedMultiplyResult[it->getColumn()]); - } - } else { - for (; it != ite; ++it) { - result = std::max(result, p2ReducedMultiplyResult[it->getColumn()]); + if (this->player1RepresentedByMatrix()) { + // Player 1 represented by matrix. + uint_fast64_t player1State = 0; + for (auto& result : player1ReducedResult) { + storm::storage::SparseMatrix::const_rows relevantRows = this->getPlayer1Matrix().getRowGroup(player1State); + STORM_LOG_ASSERT(relevantRows.getNumberOfEntries() != 0, "There is a choice of player 1 that does not lead to any player 2 choice"); + auto it = relevantRows.begin(); + auto ite = relevantRows.end(); + + // Set the first value. + result = player2ReducedResult[it->getColumn()]; + ++it; + + // Now iterate through the different values and pick the extremal one. + if (player1Dir == OptimizationDirection::Minimize) { + for (; it != ite; ++it) { + result = std::min(result, player2ReducedResult[it->getColumn()]); + } + } else { + for (; it != ite; ++it) { + result = std::max(result, player2ReducedResult[it->getColumn()]); + } } + ++player1State; } - ++pl1State; + } else { + // Player 1 represented by grouping of player 2 states (vector). + storm::utility::vector::reduceVectorMinOrMax(player1Dir, player2ReducedResult, player1ReducedResult, this->getPlayer1Grouping(), player1SchedulerChoices); } } @@ -333,22 +369,45 @@ namespace storm { } } - // Now extract the choices of player 1 - for (uint_fast64_t p1Group = 0; p1Group < this->player1Matrix.getRowGroupCount(); ++p1Group) { - uint_fast64_t firstRowInGroup = this->player1Matrix.getRowGroupIndices()[p1Group]; - uint_fast64_t rowGroupSize = this->player1Matrix.getRowGroupIndices()[p1Group + 1] - firstRowInGroup; - uint_fast64_t currentChoice = player1Choices[p1Group]; - ValueType currentValue = player2ChoiceValues[this->player1Matrix.getRow(firstRowInGroup + currentChoice).begin()->getColumn()]; - for (uint_fast64_t p1Choice = 0; p1Choice < rowGroupSize; ++p1Choice) { - // If the choice is the currently selected one, we can skip it. - if (p1Choice == currentChoice) { - continue; + // Now extract the choices of player 1. + if (this->player1RepresentedByMatrix()) { + // Player 1 represented by matrix. + for (uint_fast64_t p1Group = 0; p1Group < this->getPlayer1Matrix().getRowGroupCount(); ++p1Group) { + uint_fast64_t firstRowInGroup = this->getPlayer1Matrix().getRowGroupIndices()[p1Group]; + uint_fast64_t rowGroupSize = this->getPlayer1Matrix().getRowGroupIndices()[p1Group + 1] - firstRowInGroup; + uint_fast64_t currentChoice = player1Choices[p1Group]; + ValueType currentValue = player2ChoiceValues[this->getPlayer1Matrix().getRow(firstRowInGroup + currentChoice).begin()->getColumn()]; + for (uint_fast64_t p1Choice = 0; p1Choice < rowGroupSize; ++p1Choice) { + // If the choice is the currently selected one, we can skip it. + if (p1Choice == currentChoice) { + continue; + } + ValueType const& choiceValue = player2ChoiceValues[this->getPlayer1Matrix().getRow(firstRowInGroup + p1Choice).begin()->getColumn()]; + if (valueImproved(player1Dir, currentValue, choiceValue)) { + schedulerImproved = true; + player1Choices[p1Group] = p1Choice; + currentValue = choiceValue; + } } - ValueType const& choiceValue = player2ChoiceValues[this->player1Matrix.getRow(firstRowInGroup + p1Choice).begin()->getColumn()]; - if (valueImproved(player1Dir, currentValue, choiceValue)) { - schedulerImproved = true; - player1Choices[p1Group] = p1Choice; - currentValue = choiceValue; + } + } else { + // Player 1 represented by grouping of player 2 states (vector). + for (uint64_t player1State = 0; player1State < this->getPlayer1Grouping().size() - 1; ++player1State) { + uint64_t currentChoice = player1Choices[player1State]; + ValueType currentValue = player2ChoiceValues[currentChoice]; + uint64_t numberOfPlayer2Successors = this->getPlayer1Grouping()[player1State + 1] - this->getPlayer1Grouping()[player1State]; + for (uint64_t player2State = 0; player2State < numberOfPlayer2Successors; ++player2State) { + // If the choice is the currently selected one, we can skip it. + if (currentChoice == player2State + this->getPlayer1Grouping()[player1State]) { + continue; + } + + ValueType const& choiceValue = player2ChoiceValues[this->getPlayer1Grouping()[player1State] + player2State]; + if (valueImproved(player1Dir, currentValue, choiceValue)) { + schedulerImproved = true; + player1Choices[player1State] = player2State; + currentValue = choiceValue; + } } } } @@ -358,25 +417,66 @@ namespace storm { template void StandardGameSolver::getInducedMatrixVector(std::vector& x, std::vector const& b, std::vector const& player1Choices, std::vector const& player2Choices, storm::storage::SparseMatrix& inducedMatrix, std::vector& inducedVector) const { - //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. + // Get the rows of the player 2 matrix that are selected by the schedulers. + // Note that rows can be selected more than once and in an arbitrary order. std::vector selectedRows; - selectedRows.reserve(player1Matrix.getRowGroupCount()); - uint_fast64_t pl1State = 0; - for (auto const& pl1Choice : player1Choices){ - auto const& pl1Row = player1Matrix.getRow(pl1State, pl1Choice); - STORM_LOG_ASSERT(pl1Row.getNumberOfEntries() == 1, "It is assumed that rows of player one have one entry, but this is not the case."); - uint_fast64_t const& pl2State = pl1Row.begin()->getColumn(); - selectedRows.push_back(player2Matrix.getRowGroupIndices()[pl2State] + player2Choices[pl2State]); - ++pl1State; + if (this->player1RepresentedByMatrix()) { + // Player 1 is represented by a matrix. + selectedRows.reserve(this->getPlayer1Matrix().getRowGroupCount()); + uint_fast64_t player1State = 0; + for (auto const& player1Choice : player1Choices) { + auto const& player1Row = this->getPlayer1Matrix().getRow(player1State, player1Choice); + STORM_LOG_ASSERT(player1Row.getNumberOfEntries() == 1, "It is assumed that rows of player one have one entry, but this is not the case."); + uint_fast64_t player2State = player1Row.begin()->getColumn(); + selectedRows.push_back(player2Matrix.getRowGroupIndices()[player2State] + player2Choices[player2State]); + ++player1State; + } + } else { + // Player 1 is represented by the grouping of player 2 states (vector). + selectedRows.reserve(this->player2Matrix.getRowGroupCount()); + for (uint64_t player1State = 0; player1State < this->getPlayer1Grouping().size() - 1; ++player1State) { + uint64_t player2State = player1Choices[player1State]; + selectedRows.emplace_back(player2Matrix.getRowGroupIndices()[player2State] + player2Choices[player2State]); + } } - //Get the matrix and the vector induced by this selection. Note that we add entries at the diagonal + // Get the matrix and the vector induced by this selection and add entries on the diagonal in the process. inducedMatrix = player2Matrix.selectRowsFromRowIndexSequence(selectedRows, true); inducedVector.resize(inducedMatrix.getRowCount()); storm::utility::vector::selectVectorValues(inducedVector, selectedRows, b); } + template + bool StandardGameSolver::player1RepresentedByMatrix() const { + return player1Matrix != nullptr; + } + + template + storm::storage::SparseMatrix const& StandardGameSolver::getPlayer1Matrix() const { + STORM_LOG_ASSERT(player1RepresentedByMatrix(), "Player 1 is represented by a matrix."); + return *player1Matrix; + } + + template + std::vector const& StandardGameSolver::getPlayer1Grouping() const { + STORM_LOG_ASSERT(!player1RepresentedByMatrix(), "Player 1 is represented by a matrix."); + return *player1Grouping; + } + + template + uint64_t StandardGameSolver::getNumberOfPlayer1States() const { + if (this->player1RepresentedByMatrix()) { + return this->getPlayer1Matrix().getRowGroupCount(); + } else { + return this->getPlayer1Grouping().size() - 1; + } + } + + template + uint64_t StandardGameSolver::getNumberOfPlayer2States() const { + return this->player2Matrix.getRowGroupCount(); + } + template typename StandardGameSolver::Status StandardGameSolver::updateStatusIfNotConverged(Status status, std::vector const& x, uint64_t iterations, uint64_t maximalNumberOfIterations) const { if (status != Status::Converged) { diff --git a/src/storm/solver/StandardGameSolver.h b/src/storm/solver/StandardGameSolver.h index e9e8060a7..e0a800ea2 100644 --- a/src/storm/solver/StandardGameSolver.h +++ b/src/storm/solver/StandardGameSolver.h @@ -11,10 +11,14 @@ namespace storm { template class StandardGameSolver : public GameSolver { public: + // Constructors for when the first player is represented using a matrix. StandardGameSolver(storm::storage::SparseMatrix const& player1Matrix, storm::storage::SparseMatrix const& player2Matrix, std::unique_ptr>&& linearEquationSolverFactory); - StandardGameSolver(storm::storage::SparseMatrix&& player1Matrix, storm::storage::SparseMatrix&& player2Matrix, std::unique_ptr>&& linearEquationSolverFactory); + // Constructor for when the first player is represented by a grouping of the player 2 states (row groups). + StandardGameSolver(std::vector const& player1Groups, storm::storage::SparseMatrix const& player2Matrix, std::unique_ptr>&& linearEquationSolverFactory); + StandardGameSolver(std::vector&& player1Groups, storm::storage::SparseMatrix&& player2Matrix, std::unique_ptr>&& linearEquationSolverFactory); + virtual bool solveGame(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector& x, std::vector const& b) const override; virtual void repeatedMultiply(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector& x, std::vector const* b, uint_fast64_t n = 1) const override; @@ -27,7 +31,7 @@ namespace storm { bool solveGameValueIteration(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector& x, std::vector const& b) const; // Computes p2Matrix * x + b, reduces the result w.r.t. player 2 choices, and then reduces the result w.r.t. player 1 choices. - void multiplyAndReduce(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector& x, std::vector const* b, storm::solver::Multiplier const& multiplier, std::vector& multiplyResult, std::vector& p2ReducedMultiplyResult, std::vector& p1ReducedMultiplyResult) const; + void multiplyAndReduce(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector& x, std::vector const* b, storm::solver::Multiplier const& multiplier, std::vector& player2ReducedResult, std::vector& player1ReducedResult, std::vector* player1SchedulerChoices = nullptr, std::vector* player2SchedulerChoices = nullptr) const; // Solves the equation system given by the two choice selections void getInducedMatrixVector(std::vector& x, std::vector const& b, std::vector const& player1Choices, std::vector const& player2Choices, storm::storage::SparseMatrix& inducedMatrix, std::vector& inducedVector) const; @@ -38,6 +42,12 @@ namespace storm { bool valueImproved(OptimizationDirection dir, ValueType const& value1, ValueType const& value2) const; + bool player1RepresentedByMatrix() const; + storm::storage::SparseMatrix const& getPlayer1Matrix() const; + std::vector const& getPlayer1Grouping() const; + uint64_t getNumberOfPlayer1States() const; + uint64_t getNumberOfPlayer2States() const; + enum class Status { Converged, TerminatedEarly, MaximalIterationsExceeded, InProgress }; @@ -56,12 +66,14 @@ namespace storm { // If the solver takes posession of the matrix, we store the moved matrix in this member, so it gets deleted // when the solver is destructed. - std::unique_ptr> localP1Matrix; - std::unique_ptr> localP2Matrix; + std::unique_ptr> localPlayer1Grouping; + std::unique_ptr> localPlayer1Matrix; + std::unique_ptr> localPlayer2Matrix; // A reference to the original sparse matrix given to this solver. If the solver takes posession of the matrix // the reference refers to localA. - storm::storage::SparseMatrix const& player1Matrix; + std::vector const* player1Grouping; + storm::storage::SparseMatrix const* player1Matrix; storm::storage::SparseMatrix const& player2Matrix; }; diff --git a/src/storm/storage/SparseMatrix.h b/src/storm/storage/SparseMatrix.h index 917ed92e2..1ec88e34e 100644 --- a/src/storm/storage/SparseMatrix.h +++ b/src/storm/storage/SparseMatrix.h @@ -756,7 +756,7 @@ namespace storm { /*! * 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 + * 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