From 48f56081575a6c8a41255b49e3c33ffd140a626a Mon Sep 17 00:00:00 2001 From: dehnert Date: Sat, 9 Jun 2018 21:59:06 +0200 Subject: [PATCH] making policy iteration available for game-based abstraction (prototypical for now) --- .../abstraction/GameBasedMdpModelChecker.cpp | 256 ++++-------------- src/storm/solver/StandardGameSolver.cpp | 86 +++++- src/storm/solver/StandardGameSolver.h | 4 +- src/storm/storage/SparseMatrix.cpp | 12 - src/storm/utility/constants.cpp | 12 + src/storm/utility/constants.h | 7 +- src/storm/utility/vector.h | 5 - 7 files changed, 147 insertions(+), 235 deletions(-) diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 89920bf59..43e1e795c 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -476,37 +476,21 @@ namespace storm { uint64_t maybeStatePosition = 0; previousPlayer2States = 0; for (auto state : maybeStates) { - if (state == 2324 || state == 50377 || state == 50209) { - std::cout << "dealing with problematic state " << state << " whose local offset is " << maybeStatePosition << std::endl; - } uint64_t chosenPlayer2State = startingStrategyPair->getPlayer1Strategy().getChoice(state); uint64_t previousPlayer2MaybeStatesForState = 0; for (uint64_t player2State = player1Groups[state]; player2State < player1Groups[state + 1]; ++player2State) { if (player2MaybeStates.get(player2State)) { - if (state == 2324 || state == 50377 || state == 50209) { - std::cout << "player 2 state " << player2State << " is a player 2 maybe state with local index " << previousPlayer2States << " ranging from row " << submatrix.getRowGroupIndices()[previousPlayer2States] << " to " << submatrix.getRowGroupIndices()[previousPlayer2States + 1] << std::endl; - } - if (player2State == chosenPlayer2State) { player1Scheduler[maybeStatePosition] = previousPlayer2MaybeStatesForState; - if (state == 2324 || state == 50377 || state == 50209) { - std::cout << "player 1 scheduler chooses " << previousPlayer2MaybeStatesForState << " which globally is " << player2State << std::endl; - } } // Copy over the player 2 action (modulo making it local) as all rows for the player 2 state are taken. if (startingStrategyPair->getPlayer2Strategy().hasDefinedChoice(player2State)) { player2Scheduler[previousPlayer2States] = startingStrategyPair->getPlayer2Strategy().getChoice(player2State) - transitionMatrix.getRowGroupIndices() [player2State]; - if (state == 2324 || state == 50377 || state == 50209) { - std::cout << "copied over choice " << player2Scheduler[previousPlayer2States] << " for player 2 (global index " << startingStrategyPair->getPlayer2Strategy().getChoice(player2State) << ")" << std::endl; - } } else { player2Scheduler[previousPlayer2States] = 0; - if (state == 2324 || state == 50377 || state == 50209) { - std::cout << "did not copy (undefined) choice for player 2 (global index " << startingStrategyPair->getPlayer2Strategy().getChoice(player2State) << ")" << std::endl; - } } ++previousPlayer2MaybeStatesForState; @@ -517,37 +501,6 @@ namespace storm { ++maybeStatePosition; } STORM_LOG_ASSERT(previousPlayer2States == submatrix.getRowGroupCount(), "Expected correct number of player 2 states."); - } else { - // If the starting strategy pair was provided, we need to extract the choices of the maybe states here. - uint64_t maybeStatePosition = 0; - previousPlayer2States = 0; - for (auto state : maybeStates) { - if (state == 2324 || state == 50377 || state == 50209) { - std::cout << "dealing with problematic state " << state << " whose local offset is " << maybeStatePosition << std::endl; - } - - if (state == 2324 || state == 50377 || state == 50209) { - std::cout << "player 1 scheduler chooses " << player1Scheduler[maybeStatePosition] << " which globally is " << (player1Groups[state] + player1Scheduler[maybeStatePosition]) << std::endl; - } - - uint64_t previousPlayer2MaybeStatesForState = 0; - for (uint64_t player2State = player1Groups[state]; player2State < player1Groups[state + 1]; ++player2State) { - if (player2MaybeStates.get(player2State)) { - if (state == 2324 || state == 50377 || state == 50209) { - std::cout << "player 2 state " << player2State << " is a player 2 maybe state with local index " << previousPlayer2States << " ranging from row " << submatrix.getRowGroupIndices()[previousPlayer2States] << " to " << submatrix.getRowGroupIndices()[previousPlayer2States + 1] << std::endl; - } - - if (state == 2324 || state == 50377 || state == 50209) { - std::cout << "player 2 scheduler chooses " << player2Scheduler[previousPlayer2States] << " for player 2 (global index " << (transitionMatrix.getRowGroupIndices()[player2State] + player2Scheduler[previousPlayer2States]) << ")" << std::endl; - } - ++previousPlayer2MaybeStatesForState; - ++previousPlayer2States; - } - } - - ++maybeStatePosition; - } - STORM_LOG_ASSERT(previousPlayer2States == submatrix.getRowGroupCount(), "Expected correct number of player 2 states."); } // Solve actual game and track schedulers. @@ -564,24 +517,18 @@ namespace storm { bool madePlayer1Choice = false; for (uint64_t player2State = player1Groups[state]; player2State < player1Groups[state + 1]; ++player2State) { if (player1Scheduler[previousPlayer1MaybeStates] == previousPlayer2MaybeStatesForState) { - if (state == 2324 || state == 50377 || state == 50209) { - std::cout << "player 1 choosing " << player2State << " in " << state << std::endl; - } strategyPair.getPlayer1Strategy().setChoice(state, player2State); madePlayer1Choice = true; } if (player2MaybeStates.get(player2State)) { - if (state == 2324 || state == 50377 || state == 50209) { - std::cout << "player 2 choosing " << (transitionMatrix.getRowGroupIndices()[player2State] + player2Scheduler[previousPlayer2MaybeStates]) << " in " << player2State << " for player 1 state " << state << std::endl; - } strategyPair.getPlayer2Strategy().setChoice(player2State, transitionMatrix.getRowGroupIndices()[player2State] + player2Scheduler[previousPlayer2MaybeStates]); ++previousPlayer2MaybeStatesForState; ++previousPlayer2MaybeStates; } } - STORM_LOG_ASSERT(madePlayer1Choice, "Player 1 state " << state << " did not make a choice, scheduler: " << player1Scheduler[previousPlayer1MaybeStates] << "."); + STORM_LOG_ASSERT(madePlayer1Choice, "[" << player1Direction << "]: player 1 state " << state << " did not make a choice, scheduler: " << player1Scheduler[previousPlayer1MaybeStates] << "."); ++previousPlayer1MaybeStates; } @@ -1088,82 +1035,76 @@ namespace storm { template void postProcessStrategies(uint64_t iteration, storm::OptimizationDirection const& player1Direction, abstraction::ExplicitGameStrategyPair& minStrategyPair, abstraction::ExplicitGameStrategyPair& maxStrategyPair, std::vector const& player1Groups, std::vector const& player2Groups, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, ExplicitQuantitativeResultMinMax const& quantitativeResult, bool redirectPlayer1, bool redirectPlayer2, bool sanityCheck) { - if (!redirectPlayer1 && !redirectPlayer2) { - return; - } - - for (uint64_t state = 0; state < player1Groups.size() - 1; ++state) { - STORM_LOG_ASSERT(targetStates.get(state) || minStrategyPair.getPlayer1Strategy().hasDefinedChoice(state), "Expected lower player 1 choice in state " << state << "."); - STORM_LOG_ASSERT(targetStates.get(state) || maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(state), "Expected upper player 1 choice in state " << state << "."); - - bool hasMinPlayer1Choice = false; - uint64_t lowerPlayer1Choice = 0; - ValueType lowerValueUnderMinChoicePlayer1 = storm::utility::zero(); - bool hasMaxPlayer1Choice = false; - uint64_t upperPlayer1Choice = 0; - ValueType lowerValueUnderMaxChoicePlayer1 = storm::utility::zero(); - - if (minStrategyPair.getPlayer1Strategy().hasDefinedChoice(state)) { - hasMinPlayer1Choice = true; - lowerPlayer1Choice = minStrategyPair.getPlayer1Strategy().getChoice(state); - - STORM_LOG_ASSERT(minStrategyPair.getPlayer2Strategy().hasDefinedChoice(lowerPlayer1Choice), "Expected lower player 2 choice for state " << state << " (lower player 1 choice " << lowerPlayer1Choice << ")."); - uint64_t lowerPlayer2Choice = minStrategyPair.getPlayer2Strategy().getChoice(lowerPlayer1Choice); + if (redirectPlayer1 || redirectPlayer2) { + for (uint64_t state = 0; state < player1Groups.size() - 1; ++state) { + STORM_LOG_ASSERT(targetStates.get(state) || minStrategyPair.getPlayer1Strategy().hasDefinedChoice(state), "Expected lower player 1 choice in state " << state << "."); + STORM_LOG_ASSERT(targetStates.get(state) || maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(state), "Expected upper player 1 choice in state " << state << "."); - ValueType lowerValueUnderLowerChoicePlayer2 = transitionMatrix.multiplyRowWithVector(lowerPlayer2Choice, quantitativeResult.getMin().getValues()); - lowerValueUnderMinChoicePlayer1 = lowerValueUnderLowerChoicePlayer2; + bool hasMinPlayer1Choice = false; + uint64_t lowerPlayer1Choice = 0; + ValueType lowerValueUnderMinChoicePlayer1 = storm::utility::zero(); + bool hasMaxPlayer1Choice = false; + uint64_t upperPlayer1Choice = 0; + ValueType lowerValueUnderMaxChoicePlayer1 = storm::utility::zero(); - if (maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(lowerPlayer1Choice)) { - uint64_t upperPlayer2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(lowerPlayer1Choice); + if (minStrategyPair.getPlayer1Strategy().hasDefinedChoice(state)) { + hasMinPlayer1Choice = true; + lowerPlayer1Choice = minStrategyPair.getPlayer1Strategy().getChoice(state); - if (lowerPlayer2Choice != upperPlayer2Choice) { - ValueType lowerValueUnderUpperChoicePlayer2 = transitionMatrix.multiplyRowWithVector(upperPlayer2Choice, quantitativeResult.getMin().getValues()); + STORM_LOG_ASSERT(minStrategyPair.getPlayer2Strategy().hasDefinedChoice(lowerPlayer1Choice), "Expected lower player 2 choice for state " << state << " (lower player 1 choice " << lowerPlayer1Choice << ")."); + uint64_t lowerPlayer2Choice = minStrategyPair.getPlayer2Strategy().getChoice(lowerPlayer1Choice); + + ValueType lowerValueUnderLowerChoicePlayer2 = transitionMatrix.multiplyRowWithVector(lowerPlayer2Choice, quantitativeResult.getMin().getValues()); + lowerValueUnderMinChoicePlayer1 = lowerValueUnderLowerChoicePlayer2; + + if (maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(lowerPlayer1Choice)) { + uint64_t upperPlayer2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(lowerPlayer1Choice); - if (redirectPlayer2 && lowerValueUnderUpperChoicePlayer2 <= lowerValueUnderLowerChoicePlayer2) { - lowerValueUnderMinChoicePlayer1 = lowerValueUnderUpperChoicePlayer2; - minStrategyPair.getPlayer2Strategy().setChoice(lowerPlayer1Choice, upperPlayer2Choice); + if (lowerPlayer2Choice != upperPlayer2Choice) { + ValueType lowerValueUnderUpperChoicePlayer2 = transitionMatrix.multiplyRowWithVector(upperPlayer2Choice, quantitativeResult.getMin().getValues()); + + if (redirectPlayer2 && lowerValueUnderUpperChoicePlayer2 <= lowerValueUnderLowerChoicePlayer2) { + lowerValueUnderMinChoicePlayer1 = lowerValueUnderUpperChoicePlayer2; + minStrategyPair.getPlayer2Strategy().setChoice(lowerPlayer1Choice, upperPlayer2Choice); + } } } } - } - - if (maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(state)) { - upperPlayer1Choice = maxStrategyPair.getPlayer1Strategy().getChoice(state); - if (upperPlayer1Choice != lowerPlayer1Choice && minStrategyPair.getPlayer2Strategy().hasDefinedChoice(upperPlayer1Choice)) { - hasMaxPlayer1Choice = true; - - uint64_t lowerPlayer2Choice = minStrategyPair.getPlayer2Strategy().getChoice(upperPlayer1Choice); + if (maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(state)) { + upperPlayer1Choice = maxStrategyPair.getPlayer1Strategy().getChoice(state); - ValueType lowerValueUnderLowerChoicePlayer2 = transitionMatrix.multiplyRowWithVector(lowerPlayer2Choice, quantitativeResult.getMin().getValues()); - lowerValueUnderMaxChoicePlayer1 = lowerValueUnderLowerChoicePlayer2; - - STORM_LOG_ASSERT(maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(upperPlayer1Choice), "Expected upper player 2 choice for state " << state << " (upper player 1 choice " << upperPlayer1Choice << ")."); - uint64_t upperPlayer2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(upperPlayer1Choice); - - if (lowerPlayer2Choice != upperPlayer2Choice) { - ValueType lowerValueUnderUpperChoicePlayer2 = transitionMatrix.multiplyRowWithVector(upperPlayer2Choice, quantitativeResult.getMin().getValues()); + if (upperPlayer1Choice != lowerPlayer1Choice && minStrategyPair.getPlayer2Strategy().hasDefinedChoice(upperPlayer1Choice)) { + hasMaxPlayer1Choice = true; + + uint64_t lowerPlayer2Choice = minStrategyPair.getPlayer2Strategy().getChoice(upperPlayer1Choice); + + ValueType lowerValueUnderLowerChoicePlayer2 = transitionMatrix.multiplyRowWithVector(lowerPlayer2Choice, quantitativeResult.getMin().getValues()); + lowerValueUnderMaxChoicePlayer1 = lowerValueUnderLowerChoicePlayer2; + + STORM_LOG_ASSERT(maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(upperPlayer1Choice), "Expected upper player 2 choice for state " << state << " (upper player 1 choice " << upperPlayer1Choice << ")."); + uint64_t upperPlayer2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(upperPlayer1Choice); - if (redirectPlayer2 && lowerValueUnderUpperChoicePlayer2 <= lowerValueUnderLowerChoicePlayer2) { - minStrategyPair.getPlayer2Strategy().setChoice(upperPlayer1Choice, upperPlayer2Choice); + if (lowerPlayer2Choice != upperPlayer2Choice) { + ValueType lowerValueUnderUpperChoicePlayer2 = transitionMatrix.multiplyRowWithVector(upperPlayer2Choice, quantitativeResult.getMin().getValues()); + + if (redirectPlayer2 && lowerValueUnderUpperChoicePlayer2 <= lowerValueUnderLowerChoicePlayer2) { + minStrategyPair.getPlayer2Strategy().setChoice(upperPlayer1Choice, upperPlayer2Choice); + } } } } - } - - if (redirectPlayer1 && player1Direction == storm::OptimizationDirection::Minimize) { - if (hasMinPlayer1Choice && hasMaxPlayer1Choice && lowerPlayer1Choice != upperPlayer1Choice) { - if (lowerValueUnderMaxChoicePlayer1 <= lowerValueUnderMinChoicePlayer1) { - minStrategyPair.getPlayer1Strategy().setChoice(state, upperPlayer1Choice); + + if (redirectPlayer1 && player1Direction == storm::OptimizationDirection::Minimize) { + if (hasMinPlayer1Choice && hasMaxPlayer1Choice && lowerPlayer1Choice != upperPlayer1Choice) { + if (lowerValueUnderMaxChoicePlayer1 <= lowerValueUnderMinChoicePlayer1) { + minStrategyPair.getPlayer1Strategy().setChoice(state, upperPlayer1Choice); + } } } } } -// ExplicitGameExporter exporter; -// exporter.exportToJson("game" + std::to_string(iteration) + ".json", player1Groups, player2Groups, transitionMatrix, initialStates, constraintStates, targetStates, quantitativeResult, &minStrategyPair, &maxStrategyPair); -// exit(-1); - if (sanityCheck) { storm::utility::ConstantsComparator sanityComparator( 1e-6, true); @@ -1196,44 +1137,6 @@ namespace storm { } STORM_LOG_TRACE("Got maximal deviation of " << maxDiff << "."); STORM_LOG_WARN_COND(sanityComparator.isZero(maxDiff), "Deviation " << maxDiff << " between computed value (" << quantitativeResult.getMin().getValues()[maxState] << ") and sanity check value (" << sanityValues[maxState] << ") in state " << maxState << " appears to be too high. (Obtained bounds were [" << quantitativeResult.getMin().getValues()[maxState] << ", " << quantitativeResult.getMax().getValues()[maxState] << "].)"); - if (!sanityComparator.isZero(maxDiff)) { - ExplicitGameExporter exporter; - storm::storage::BitVector newInitialStates(player1Groups.size() - 1); - newInitialStates.set(maxState); - exporter.exportToJson("game" + std::to_string(iteration) + "_min.json", player1Groups, player2Groups, transitionMatrix, newInitialStates, constraintStates, targetStates, quantitativeResult, &minStrategyPair, static_cast(nullptr)); - exporter.exportToJson("game" + std::to_string(iteration) + "_max.json", player1Groups, player2Groups, transitionMatrix, newInitialStates, constraintStates, targetStates, quantitativeResult, static_cast(nullptr), &maxStrategyPair); - - - // Perform DFS from max diff state in upper system. - std::vector stack; - stack.push_back(maxState); - storm::storage::BitVector reachable(dtmcMatrix.getRowCount()); - - while (!stack.empty()) { - uint64_t currentState = stack.back(); - stack.pop_back(); - - std::cout << "exploring player 1 state " << currentState << " with " << (player1Groups[currentState + 1] - player1Groups[currentState]) << " player 2 successors from" << player1Groups[currentState] << " to " << player1Groups[currentState + 1] << std::endl; - uint64_t player2State = minStrategyPair.getPlayer1Strategy().getChoice(currentState); - std::cout << "going to player 2 state " << player2State << " with " << (player2Groups[player2State + 1] - player2Groups[player2State]) << " player 2 choices from " << player2Groups[player2State] << " to " << player2Groups[player2State + 1] << std::endl; - uint64_t player2Choice = minStrategyPair.getPlayer2Strategy().getChoice(player2State); - std::cout << "which takes choice " << player2Choice << " which locally is " << (player2Choice - transitionMatrix.getRowGroupIndices()[player2State]) << std::endl; - for (auto const& entry : transitionMatrix.getRow(player2Choice)) { - std::cout << entry.getColumn() << " -> " << entry.getValue() << std::endl; - auto successor = entry.getColumn(); - if (!reachable.get(successor)) { - if (!targetStates.get(successor)) { - reachable.set(successor); - stack.push_back(successor); - } else { - std::cout << "found target state " << std::endl; - } - } - } - } - - exit(-1); - } ///////// SANITY CHECK: apply upper strategy, obtain DTMC matrix and model check it. the values should ///////// still be the upper ones. @@ -1248,10 +1151,6 @@ namespace storm { for (auto const& entry : transitionMatrix.getRow(player2Choice)) { dtmcMatrixBuilder.addNextValue(state, entry.getColumn(), entry.getValue()); - if (state == 25305) { - std::cout << "entry " << entry.getColumn() << " -> " << entry.getValue() << std::endl; - std::cout << "values [" << quantitativeResult.getMin().getValues()[entry.getColumn()] << ", " << quantitativeResult.getMax().getValues()[entry.getColumn()] << "]" << std::endl; - } } } } @@ -1266,58 +1165,9 @@ namespace storm { maxState = state; maxDiff = diff; } - - if (dtmcMatrix.getRowCount() > 25305 && !targetStates.get(state)) { - uint64_t player2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(maxStrategyPair.getPlayer1Strategy().getChoice(state)); - for (auto const& entry : transitionMatrix.getRow(player2Choice)) { - if (state == 25305) { - std::cout << "entry " << entry.getColumn() << " -> " << entry.getValue() << std::endl; - std::cout << "sanity value " << sanityValues[entry.getColumn()] << std::endl; - } - } - } } STORM_LOG_TRACE("Got maximal deviation of " << maxDiff << "."); STORM_LOG_WARN_COND(sanityComparator.isZero(maxDiff), "Deviation " << maxDiff << " between computed value (" << quantitativeResult.getMax().getValues()[maxState] << ") and sanity check value (" << sanityValues[maxState] << ") in state " << maxState << " appears to be too high. (Obtained bounds were [" << quantitativeResult.getMin().getValues()[maxState] << ", " << quantitativeResult.getMax().getValues()[maxState] << "].)"); - if (!sanityComparator.isZero(maxDiff)) { - - ExplicitGameExporter exporter; - storm::storage::BitVector newInitialStates(player1Groups.size() - 1); - newInitialStates.set(maxState); - exporter.exportToJson("game" + std::to_string(iteration) + "_min.json", player1Groups, player2Groups, transitionMatrix, newInitialStates, constraintStates, targetStates, quantitativeResult, &minStrategyPair, static_cast(nullptr)); - exporter.exportToJson("game" + std::to_string(iteration) + "_max.json", player1Groups, player2Groups, transitionMatrix, newInitialStates, constraintStates, targetStates, quantitativeResult, static_cast(nullptr), &maxStrategyPair); - - - // Perform DFS from max diff state in upper system. - std::vector stack; - stack.push_back(maxState); - storm::storage::BitVector reachable(dtmcMatrix.getRowCount()); - - while (!stack.empty()) { - uint64_t currentState = stack.back(); - stack.pop_back(); - - std::cout << "exploring player 1 state " << currentState << " with " << (player1Groups[currentState + 1] - player1Groups[currentState]) << " player 2 successors from" << player1Groups[currentState] << " to " << player1Groups[currentState + 1] << std::endl; - uint64_t player2State = maxStrategyPair.getPlayer1Strategy().getChoice(currentState); - std::cout << "going to player 2 state " << player2State << " with " << (player2Groups[player2State + 1] - player2Groups[player2State]) << " player 2 choices from " << player2Groups[player2State] << " to " << player2Groups[player2State + 1] << std::endl; - uint64_t player2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(player2State); - std::cout << "which takes choice " << player2Choice << " which locally is " << (player2Choice - transitionMatrix.getRowGroupIndices()[player2State]) << std::endl; - for (auto const& entry : transitionMatrix.getRow(player2Choice)) { - std::cout << entry.getColumn() << " -> " << entry.getValue() << std::endl; - auto successor = entry.getColumn(); - if (!reachable.get(successor)) { - if (!targetStates.get(successor)) { - reachable.set(successor); - stack.push_back(successor); - } else { - std::cout << "found target state " << std::endl; - } - } - } - } - - exit(-1); - } } } diff --git a/src/storm/solver/StandardGameSolver.cpp b/src/storm/solver/StandardGameSolver.cpp index c57ff38b8..8192ba25e 100644 --- a/src/storm/solver/StandardGameSolver.cpp +++ b/src/storm/solver/StandardGameSolver.cpp @@ -7,11 +7,13 @@ #include "storm/environment/solver/GameSolverEnvironment.h" +#include "storm/utility/graph.h" #include "storm/utility/vector.h" #include "storm/utility/macros.h" #include "storm/exceptions/InvalidEnvironmentException.h" #include "storm/exceptions/InvalidStateException.h" #include "storm/exceptions/NotImplementedException.h" + namespace storm { namespace solver { @@ -87,7 +89,7 @@ namespace storm { localPlayer2Choices = std::make_unique>(); player2Choices = localPlayer2Choices.get(); } - + if (this->hasSchedulerHints()) { *player1Choices = this->player1ChoicesHint.get(); } else if (this->player1RepresentedByMatrix()) { @@ -95,7 +97,6 @@ namespace storm { *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); } if (this->hasSchedulerHints()) { @@ -103,12 +104,12 @@ namespace storm { } else if (!(providedPlayer1Choices && providedPlayer2Choices)) { player2Choices->resize(this->player2Matrix.getRowGroupCount()); } - + if (!auxiliaryP2RowGroupVector) { auxiliaryP2RowGroupVector = std::make_unique>(this->player2Matrix.getRowGroupCount()); } if (!auxiliaryP1RowGroupVector) { - auxiliaryP1RowGroupVector = std::make_unique>(this->player1Matrix->getRowGroupCount()); + auxiliaryP1RowGroupVector = std::make_unique>(this->player1RepresentedByMatrix() ? this->player1Matrix->getRowGroupCount() : this->player1Grouping->size() - 1); } std::vector& subB = *auxiliaryP1RowGroupVector; @@ -138,9 +139,29 @@ namespace storm { // Solve the equation system induced by the two schedulers. storm::storage::SparseMatrix submatrix; getInducedMatrixVector(x, b, *player1Choices, *player2Choices, submatrix, subB); + + storm::storage::BitVector targetStates; + storm::storage::BitVector zeroStates; + if (!this->hasUniqueSolution()) { + // If there is no unique solution, we need to compute the states with probability 0 and set their values explicitly. + targetStates = storm::utility::vector::filterGreaterZero(subB); + zeroStates = ~storm::utility::graph::performProbGreater0(submatrix.transpose(), storm::storage::BitVector(targetStates.size(), true), targetStates); + } if (this->linearEquationSolverFactory->getEquationProblemFormat(environmentOfSolver) == LinearEquationSolverProblemFormat::EquationSystem) { submatrix.convertToEquationSystem(); } + if (!this->hasUniqueSolution()) { + for (auto state : zeroStates) { + for (auto& element : submatrix.getRow(state)) { + if (element.getColumn() == state) { + element.setValue(storm::utility::one()); + } else { + element.setValue(storm::utility::zero()); + } + } + subB[state] = storm::utility::zero(); + } + } auto submatrixSolver = linearEquationSolverFactory->create(environmentOfSolver, std::move(submatrix)); if (this->lowerBound) { submatrixSolver->setLowerBound(this->lowerBound.get()); @@ -154,10 +175,8 @@ namespace storm { Status status = Status::InProgress; uint64_t iterations = 0; do { - // Solve the equation system for the 'DTMC'. - // FIXME: we need to remove the 0- and 1- states to make the solution unique. submatrixSolver->solveEquations(environmentOfSolver, x, subB); - + bool schedulerImproved = extractChoices(player1Dir, player2Dir, x, b, *auxiliaryP2RowGroupVector, *player1Choices, *player2Choices); // If the scheduler did not improve, we are done. @@ -166,7 +185,27 @@ namespace storm { } else { // Update the solver. getInducedMatrixVector(x, b, *player1Choices, *player2Choices, submatrix, subB); - submatrix.convertToEquationSystem(); + + if (!this->hasUniqueSolution()) { + // If there is no unique solution, we need to compute the states with probability 0 and set their values explicitly. + targetStates = storm::utility::vector::filterGreaterZero(subB); + zeroStates = ~storm::utility::graph::performProbGreater0(submatrix.transpose(), storm::storage::BitVector(targetStates.size(), true), targetStates); + } + if (this->linearEquationSolverFactory->getEquationProblemFormat(environmentOfSolver) == LinearEquationSolverProblemFormat::EquationSystem) { + submatrix.convertToEquationSystem(); + } + if (!this->hasUniqueSolution()) { + for (auto state : zeroStates) { + for (auto& element : submatrix.getRow(state)) { + if (element.getColumn() == state) { + element.setValue(storm::utility::one()); + } else { + element.setValue(storm::utility::zero()); + } + } + subB[state] = storm::utility::zero(); + } + } submatrixSolver->setMatrix(std::move(submatrix)); } @@ -360,6 +399,29 @@ namespace storm { template bool StandardGameSolver::extractChoices(OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector const& x, std::vector const& b, std::vector& player2ChoiceValues, std::vector& player1Choices, std::vector& player2Choices) const { + if (player1Dir == storm::OptimizationDirection::Minimize) { + if (player2Dir == storm::OptimizationDirection::Minimize) { + return extractChoices, storm::utility::ElementLess>(x, b, player2ChoiceValues, player1Choices, player2Choices); + } else { + return extractChoices, storm::utility::ElementGreater>(x, b, player2ChoiceValues, player1Choices, player2Choices); + } + } else { + if (player2Dir == storm::OptimizationDirection::Minimize) { + return extractChoices, storm::utility::ElementLess>(x, b, player2ChoiceValues, player1Choices, player2Choices); + } else { + return extractChoices, storm::utility::ElementGreater>(x, b, player2ChoiceValues, player1Choices, player2Choices); + } + } + + return false; + } + + template + template + bool StandardGameSolver::extractChoices(std::vector const& x, std::vector const& b, std::vector& player2ChoiceValues, std::vector& player1Choices, std::vector& player2Choices) const { + + ComparePlayer1 comparePlayer1; + ComparePlayer2 comparePlayer2; // get the choices of player 2 and the corresponding values. bool schedulerImproved = false; @@ -387,7 +449,7 @@ namespace storm { } choiceValue += b[firstRowInGroup + p2Choice]; - if (valueImproved(player2Dir, *currentValueIt, choiceValue)) { + if (comparePlayer2(choiceValue, *currentValueIt)) { schedulerImproved = true; player2Choices[p2Group] = p2Choice; *currentValueIt = std::move(choiceValue); @@ -409,7 +471,7 @@ namespace storm { continue; } ValueType const& choiceValue = player2ChoiceValues[this->getPlayer1Matrix().getRow(firstRowInGroup + p1Choice).begin()->getColumn()]; - if (valueImproved(player1Dir, currentValue, choiceValue)) { + if (comparePlayer1(choiceValue, currentValue)) { schedulerImproved = true; player1Choices[p1Group] = p1Choice; currentValue = choiceValue; @@ -429,7 +491,7 @@ namespace storm { } ValueType const& choiceValue = player2ChoiceValues[this->getPlayer1Grouping()[player1State] + player2State]; - if (valueImproved(player1Dir, currentValue, choiceValue)) { + if (comparePlayer1(choiceValue, currentValue)) { schedulerImproved = true; player1Choices[player1State] = player2State; currentValue = choiceValue; @@ -461,7 +523,7 @@ namespace storm { // 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]; + uint64_t player2State = this->getPlayer1Grouping()[player1State] + player1Choices[player1State]; selectedRows.emplace_back(player2Matrix.getRowGroupIndices()[player2State] + player2Choices[player2State]); } } diff --git a/src/storm/solver/StandardGameSolver.h b/src/storm/solver/StandardGameSolver.h index 1af23601f..8f950838b 100644 --- a/src/storm/solver/StandardGameSolver.h +++ b/src/storm/solver/StandardGameSolver.h @@ -39,7 +39,9 @@ namespace storm { // Extracts the choices of the different players for the given solution x. // Returns true iff the newly extracted choices yield "better" values then the given choices for one of the players. bool extractChoices(OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector const& x, std::vector const& b, std::vector& player2ChoiceValues, std::vector& player1Choices, std::vector& player2Choices) const; - + template + bool extractChoices(std::vector const& x, std::vector const& b, std::vector& player2ChoiceValues, std::vector& player1Choices, std::vector& player2Choices) const; + bool valueImproved(OptimizationDirection dir, ValueType const& value1, ValueType const& value2) const; bool player1RepresentedByMatrix() const; diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index 6e8c2333b..a2b23eac9 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -1630,11 +1630,6 @@ namespace storm { currentValue += elementIt->getValue() * vector[elementIt->getColumn()]; } - if (std::distance(result.begin(), resultIt) == 2240 || std::distance(result.begin(), resultIt) == 2241 || std::distance(result.begin(), resultIt) == 8262 || std::distance(result.begin(), resultIt) == 8263 || std::distance(result.begin(), resultIt) == 8266 || std::distance(result.begin(), resultIt) == 8267) { - std::cout << "got initial value " << currentValue << " for state " << std::distance(result.begin(), resultIt) << " in row " << currentRow << std::endl; - } - - if (choices) { selectedChoice = 0; if (*choiceIt == 0) { @@ -1651,10 +1646,6 @@ namespace storm { newValue += elementIt->getValue() * vector[elementIt->getColumn()]; } - if (std::distance(result.begin(), resultIt) == 2240 || std::distance(result.begin(), resultIt) == 2241 || std::distance(result.begin(), resultIt) == 8262 || std::distance(result.begin(), resultIt) == 8263 || std::distance(result.begin(), resultIt) == 8266 || std::distance(result.begin(), resultIt) == 8267) { - std::cout << "got value " << currentValue << " for state " << std::distance(result.begin(), resultIt) << " in row " << currentRow << std::endl; - } - if (choices && currentRow == *choiceIt + *rowGroupIt) { oldSelectedChoiceValue = newValue; } @@ -1673,9 +1664,6 @@ namespace storm { // Finally write value to target vector. *resultIt = currentValue; if (choices && compare(currentValue, oldSelectedChoiceValue)) { - if (std::distance(result.begin(), resultIt) == 2240 || std::distance(result.begin(), resultIt) == 2241 || std::distance(result.begin(), resultIt) == 8262 || std::distance(result.begin(), resultIt) == 8263 || std::distance(result.begin(), resultIt) == 8266 || std::distance(result.begin(), resultIt) == 8267) { - std::cout << "changing choice in " << std::distance(result.begin(), resultIt) << " from " << *choiceIt << " to " << selectedChoice << " because " << currentValue << " is better than " << oldSelectedChoiceValue << std::endl; - } *choiceIt = selectedChoice; } } diff --git a/src/storm/utility/constants.cpp b/src/storm/utility/constants.cpp index 6c0d1c814..d5c48a89b 100644 --- a/src/storm/utility/constants.cpp +++ b/src/storm/utility/constants.cpp @@ -45,6 +45,16 @@ namespace storm { return a == zero(); } + template + bool isNan(ValueType const& value) { + return false; + } + + template<> + bool isNan(double const& value) { + return isnan(value); + } + bool isAlmostZero(double const& a) { return a < 1e-12 && a > -1e-12; } @@ -950,6 +960,7 @@ namespace storm { template bool isZero(NumberTraits::IntegerType const& value); template bool isConstant(storm::ClnRationalNumber const& value); template bool isInfinity(storm::ClnRationalNumber const& value); + template bool isNan(storm::ClnRationalNumber const& value); template storm::NumberTraits::IntegerType convertNumber(storm::NumberTraits::IntegerType const& number); template storm::ClnRationalNumber convertNumber(storm::ClnRationalNumber const& number); template storm::ClnRationalNumber simplify(storm::ClnRationalNumber value); @@ -974,6 +985,7 @@ namespace storm { template bool isZero(NumberTraits::IntegerType const& value); template bool isConstant(storm::GmpRationalNumber const& value); template bool isInfinity(storm::GmpRationalNumber const& value); + template bool isNan(storm::GmpRationalNumber const& value); template storm::NumberTraits::IntegerType convertNumber(storm::NumberTraits::IntegerType const& number); template storm::GmpRationalNumber convertNumber(storm::GmpRationalNumber const& number); template storm::GmpRationalNumber simplify(storm::GmpRationalNumber value); diff --git a/src/storm/utility/constants.h b/src/storm/utility/constants.h index 069303c04..80e1ef336 100644 --- a/src/storm/utility/constants.h +++ b/src/storm/utility/constants.h @@ -38,7 +38,7 @@ namespace storm { struct DoubleLess { bool operator()(double a, double b) const { - return b - a > 1e-17; + return (a == 0.0 && b > 0.0) || (b - a > 1e-17); } }; @@ -54,7 +54,7 @@ namespace storm { struct DoubleGreater { bool operator()(double a, double b) const { - return a - b > 1e-17; + return (b == 0.0 && a > 0.0) || (a - b > 1e-17); } }; @@ -84,6 +84,9 @@ namespace storm { template bool isZero(ValueType const& a); + + template + bool isNan(ValueType const& a); bool isAlmostZero(double const& a); diff --git a/src/storm/utility/vector.h b/src/storm/utility/vector.h index fa1c22cf4..6d3c1d281 100644 --- a/src/storm/utility/vector.h +++ b/src/storm/utility/vector.h @@ -725,10 +725,6 @@ namespace storm { } if (choices && f(*targetIt, oldSelectedChoiceValue)) { - uint64_t distance = std::distance(target.begin(), targetIt); - if (distance == 1693 || distance == 4715 || distance == 4713) { - std::cout << std::setprecision(50) << "improving value at " << distance << ": moving from " << *choiceIt << " to " << selectedChoice << " because " << *targetIt << " is better than " << oldSelectedChoiceValue << std::endl; - } *choiceIt = selectedChoice; } } else { @@ -796,7 +792,6 @@ namespace storm { */ template void reduceVectorMinOrMax(storm::solver::OptimizationDirection dir, std::vector const& source, std::vector& target, std::vector const& rowGrouping, std::vector* choices = nullptr) { - std::cout << "[" << dir << "]: reducing vector " << std::endl; if (dir == storm::solver::OptimizationDirection::Minimize) { reduceVectorMin(source, target, rowGrouping, choices); } else {