diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index 6a1dd8cdc..aad16cc2d 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -6,6 +6,7 @@ #include "storm/storage/BitVector.h" #include "storm/abstraction/ExplicitQualitativeGameResultMinMax.h" #include "storm/abstraction/ExplicitGameStrategyPair.h" +#include "storm/abstraction/ExplicitQuantitativeResultMinMax.h" #include "storm/storage/dd/DdManager.h" #include "storm/storage/dd/Odd.h" @@ -667,11 +668,12 @@ namespace storm { prefix.push_back(step); storm::expressions::Expression interpolant = interpolatingSolver.getInterpolant(prefix).substitute(variableSubstitution).changeManager(abstractionInformation.getExpressionManager()); if (!interpolant.isTrue() && !interpolant.isFalse()) { - STORM_LOG_DEBUG("Derived new predicate (based on interpolation): " << interpolant); + STORM_LOG_DEBUG("Derived new predicate (based on interpolation at step " << step << " out of " << stepCounter << "): " << interpolant); interpolants.push_back(interpolant); - } else { - STORM_LOG_ASSERT(false, "The found interpolant is '" << interpolant << "', which shouldn't happen."); } +// else { +// STORM_LOG_ASSERT(step == 0false, "The found interpolant (based on interpolation at step " << step << " out of " << stepCounter << ") is '" << interpolant << "', which shouldn't happen."); +// } } return boost::make_optional(RefinementPredicates(RefinementPredicates::Source::Interpolation, interpolants)); } else { @@ -805,7 +807,7 @@ namespace storm { } template - boost::optional> pickPivotState(bool generatePredecessors, AbstractionSettings::PivotSelectionHeuristic pivotSelectionHeuristic, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Grouping, std::vector const& player1Labeling, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& relevantStates, storm::storage::BitVector const& targetStates, ExplicitQualitativeGameResultMinMax const& qualitativeResult, ExplicitGameStrategyPair const& minStrategyPair, ExplicitGameStrategyPair const& maxStrategyPair, std::vector const* lowerValues = nullptr, std::vector const* upperValues = nullptr) { + boost::optional> pickPivotState(bool generatePredecessors, AbstractionSettings::PivotSelectionHeuristic pivotSelectionHeuristic, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Grouping, std::vector const& player1Labeling, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& relevantStates, storm::storage::BitVector const& targetStates, ExplicitGameStrategyPair const& minStrategyPair, ExplicitGameStrategyPair const& maxStrategyPair, std::vector const* lowerValues = nullptr, std::vector const* upperValues = nullptr) { STORM_LOG_ASSERT(!lowerValues || upperValues, "Expected none or both value results."); STORM_LOG_ASSERT(!upperValues || lowerValues, "Expected none or both value results."); @@ -954,7 +956,7 @@ namespace storm { // Compute the set of states whose result we have for the min and max case. storm::storage::BitVector relevantStates = (qualitativeResult.getProb0Min().getStates() | qualitativeResult.getProb1Min().getStates()) & (qualitativeResult.getProb0Max().getStates() | qualitativeResult.getProb1Max().getStates()); - boost::optional> optionalPivotStateResult = pickPivotState(useInterpolation, pivotSelectionHeuristic, transitionMatrix, player1Grouping, player1Labeling, initialStates, relevantStates, targetStates, qualitativeResult, minStrategyPair, maxStrategyPair); + boost::optional> optionalPivotStateResult = pickPivotState(useInterpolation, pivotSelectionHeuristic, transitionMatrix, player1Grouping, player1Labeling, initialStates, relevantStates, targetStates, minStrategyPair, maxStrategyPair); // If there was no pivot state, continue the search. if (!optionalPivotStateResult) { @@ -1002,11 +1004,76 @@ namespace storm { maxPlayer2Strategy |= maxPlayer1Strategy && abstractionInformation.encodePlayer2Choice(player2Labeling[player2Choice], 0, game.getPlayer2Variables().size()); } } -// symbolicPivotState.template toAdd().exportToDot("pivot.dot"); -// minPlayer1Strategy.template toAdd().exportToDot("minpl1.dot"); -// minPlayer2Strategy.template toAdd().exportToDot("minpl2.dot"); -// maxPlayer1Strategy.template toAdd().exportToDot("maxpl1.dot"); -// maxPlayer2Strategy.template toAdd().exportToDot("maxpl2.dot"); + + boost::optional predicates; + if (useInterpolation) { + predicates = derivePredicatesFromInterpolation(game, pivotStateResult, odd); + } + if (!predicates) { + predicates = derivePredicatesFromPivotState(game, symbolicPivotState, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy); + } + STORM_LOG_THROW(static_cast(predicates), storm::exceptions::InvalidStateException, "Predicates needed to continue."); + + std::vector preparedPredicates = preprocessPredicates(predicates.get().getPredicates(), predicates.get().getSource()); + performRefinement(createGlobalRefinement(preparedPredicates)); + return true; + } + + template + bool MenuGameRefiner::refine(storm::abstraction::MenuGame const& game, storm::dd::Odd const& odd, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Grouping, std::vector const& player1Labeling, std::vector const& player2Labeling, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, ExplicitQuantitativeResultMinMax const& quantitativeResult, ExplicitGameStrategyPair const& minStrategyPair, ExplicitGameStrategyPair const& maxStrategyPair) const { + + // Compute the set of states whose result we have for the min and max case. + storm::storage::BitVector relevantStates(odd.getTotalOffset(), true); + + boost::optional> optionalPivotStateResult = pickPivotState(useInterpolation, pivotSelectionHeuristic, transitionMatrix, player1Grouping, player1Labeling, initialStates, relevantStates, targetStates, minStrategyPair, maxStrategyPair, &quantitativeResult.getMin().getValues(), &quantitativeResult.getMax().getValues()); + + // If there was no pivot state, continue the search. + if (!optionalPivotStateResult) { + STORM_LOG_TRACE("Did not find pivot state in qualitative fragment."); + return false; + } + + // Otherwise, we can refine. + auto const& pivotStateResult = optionalPivotStateResult.get(); + STORM_LOG_TRACE("Found pivot state " << pivotStateResult.pivotState << " with distance " << pivotStateResult.distance << "."); + + // Translate the explicit states/choices to the symbolic ones, so we can reuse the predicate derivation techniques. + auto const& abstractionInformation = abstractor.get().getAbstractionInformation(); + uint64_t pivotState = pivotStateResult.pivotState; + storm::dd::Bdd symbolicPivotState = storm::dd::Bdd::getEncoding(game.getManager(), pivotState, odd, game.getRowVariables()); + storm::dd::Bdd minPlayer1Strategy = game.getManager().getBddZero(); + storm::dd::Bdd maxPlayer1Strategy = game.getManager().getBddZero(); + storm::dd::Bdd minPlayer2Strategy = game.getManager().getBddZero(); + storm::dd::Bdd maxPlayer2Strategy = game.getManager().getBddZero(); + if (minStrategyPair.getPlayer1Strategy().hasDefinedChoice(pivotState)) { + uint64_t player2State = minStrategyPair.getPlayer1Strategy().getChoice(pivotState); + STORM_LOG_ASSERT(player1Grouping[pivotState] <= player2State && player2State < player1Grouping[pivotState + 1], "Illegal choice for player 1."); + minPlayer1Strategy |= symbolicPivotState && abstractionInformation.encodePlayer1Choice(player1Labeling[player2State], abstractionInformation.getPlayer1VariableCount()); + + if (minStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2State)) { + uint64_t player2Choice = minStrategyPair.getPlayer2Strategy().getChoice(player2State); + minPlayer2Strategy |= minPlayer1Strategy && abstractionInformation.encodePlayer2Choice(player2Labeling[player2Choice], 0, game.getPlayer2Variables().size()); + } + if (maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2State)) { + uint64_t player2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(player2State); + maxPlayer2Strategy |= minPlayer1Strategy && abstractionInformation.encodePlayer2Choice(player2Labeling[player2Choice], 0, game.getPlayer2Variables().size()); + } + } + if (maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(pivotState)) { + uint64_t player2State = maxStrategyPair.getPlayer1Strategy().getChoice(pivotState); + STORM_LOG_ASSERT(player1Grouping[pivotState] <= player2State && player2State < player1Grouping[pivotState + 1], "Illegal choice for player 1."); + maxPlayer1Strategy |= symbolicPivotState && abstractionInformation.encodePlayer1Choice(player1Labeling[player2State], abstractionInformation.getPlayer1VariableCount()); + + if (minStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2State)) { + uint64_t player2Choice = minStrategyPair.getPlayer2Strategy().getChoice(player2State); + minPlayer2Strategy |= maxPlayer1Strategy && abstractionInformation.encodePlayer2Choice(player2Labeling[player2Choice], 0, game.getPlayer2Variables().size()); + } + if (maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2State)) { + uint64_t player2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(player2State); + maxPlayer2Strategy |= maxPlayer1Strategy && abstractionInformation.encodePlayer2Choice(player2Labeling[player2Choice], 0, game.getPlayer2Variables().size()); + } + } + boost::optional predicates; if (useInterpolation) { predicates = derivePredicatesFromInterpolation(game, pivotStateResult, odd); diff --git a/src/storm/abstraction/MenuGameRefiner.h b/src/storm/abstraction/MenuGameRefiner.h index 5e7be4d2d..a38ec0bf0 100644 --- a/src/storm/abstraction/MenuGameRefiner.h +++ b/src/storm/abstraction/MenuGameRefiner.h @@ -91,7 +91,10 @@ namespace storm { class ExplicitQualitativeGameResultMinMax; class ExplicitGameStrategyPair; - + + template + class ExplicitQuantitativeResultMinMax; + template class MenuGameRefiner { public: @@ -121,6 +124,13 @@ namespace storm { */ bool refine(storm::abstraction::MenuGame const& game, storm::dd::Odd const& odd, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Grouping, std::vector const& player1Labeling, std::vector const& player2Labeling, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, ExplicitQualitativeGameResultMinMax const& qualitativeResult, ExplicitGameStrategyPair const& minStrategyPair, ExplicitGameStrategyPair const& maxStrategyPair) const; + /*! + * Refines the abstractor based on the qualitative result by trying to derive suitable predicates. + * + * @param True if predicates for refinement could be derived, false otherwise. + */ + bool refine(storm::abstraction::MenuGame const& game, storm::dd::Odd const& odd, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Grouping, std::vector const& player1Labeling, std::vector const& player2Labeling, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, ExplicitQuantitativeResultMinMax const& qualitativeResult, ExplicitGameStrategyPair const& minStrategyPair, ExplicitGameStrategyPair const& maxStrategyPair) const; + /*! * Refines the abstractor based on the quantitative result by trying to derive suitable predicates. * diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index eeaffd6c3..bd77c5cd5 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -391,30 +391,34 @@ 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& strategyPair) { + 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& strategyPair, ExplicitQuantitativeResult const* startingQuantitativeResult = nullptr, ExplicitGameStrategyPair const* startingStrategyPair = nullptr) { - 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 row groups to keep. - storm::storage::BitVector player2MaybeStates = ~(player2Prob0States | player2Prob1States); - // Create the sub-game. - storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, player2MaybeStates, maybeStates); - std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(player2MaybeStates, player1Prob1States); + // If there are no maybe states, we construct the quantitative result from the qualitative result alone. + if (maybeStates.empty()) { + ExplicitQuantitativeResult result(maybeStates.size()); + storm::utility::vector::setVectorValues(result.getValues(), player1Prob1States, storm::utility::one()); + return result; + } + + // Otherwise, we need to solve a (sub)game. + + // Create the game by selecting all maybe player 2 states (non-prob0/1) of all maybe player 1 states. std::vector subPlayer1Groups(maybeStates.getNumberOfSetBits() + 1); uint64_t position = 0; uint64_t previousPlayer2States = 0; + storm::storage::BitVector player2MaybeStates(transitionMatrix.getRowGroupCount()); for (auto state : maybeStates) { subPlayer1Groups[position] = previousPlayer2States; bool hasMaybePlayer2Successor = false; for (uint64_t player2State = player1Groups[state]; player2State < player1Groups[state + 1]; ++player2State) { - if (player2MaybeStates.get(player2State)) { + if (!player2Prob0States.get(player2State) && !player2Prob1States.get(player2State)) { + player2MaybeStates.set(player2State); hasMaybePlayer2Successor = true; ++previousPlayer2States; } @@ -423,23 +427,57 @@ namespace storm { ++position; } subPlayer1Groups.back() = previousPlayer2States; - - // Solve the sub-game. + + // Create the player 2 matrix using the maybe player 2 states. + storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, player2MaybeStates, maybeStates); + std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(player2MaybeStates, player1Prob1States); + + // Set up game solver. auto gameSolver = storm::solver::GameSolverFactory().create(env, subPlayer1Groups, submatrix); - gameSolver->setTrackSchedulers(true); - std::vector lowerValues(maybeStates.getNumberOfSetBits()); - gameSolver->solveGame(env, player1Direction, player2Direction, lowerValues, b); + + // Prepare the value storage for the maybe states. If the starting values were given, extract them now. + std::vector values(maybeStates.getNumberOfSetBits()); + if (startingQuantitativeResult) { + storm::utility::vector::selectVectorValues(values, maybeStates, startingQuantitativeResult->getValues()); + } + + // Prepare scheduler storage. + std::vector player1Scheduler(subPlayer1Groups.size() - 1); + std::vector player2Scheduler(submatrix.getRowGroupCount()); + if (startingStrategyPair) { + // 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) { + uint64_t chosenPlayer2State = startingStrategyPair->getPlayer1Strategy().getChoice(state); + + uint64_t previousPlayer2StatesForState = 0; + for (uint64_t player2State = player1Groups[state]; player2State < player1Groups[state + 1]; ++player2State) { + if (player2MaybeStates.get(player2State)) { + if (player2State == chosenPlayer2State) { + player1Scheduler[maybeStatePosition] = previousPlayer2StatesForState; + } + + // Copy over the player 2 action (modulo making it local) as all rows for the state are taken. + player2Scheduler[previousPlayer2States] = startingStrategyPair->getPlayer2Strategy().getChoice(player2State) - transitionMatrix.getRowGroupIndices()[player2State]; + + ++previousPlayer2StatesForState; + ++previousPlayer2States; + } + } + + ++maybeStatePosition; + } + } + + // Solve actual game and track schedulers. + gameSolver->solveGame(env, player1Direction, player2Direction, values, b, &player1Scheduler, &player2Scheduler); // Create combined result for all states. ExplicitQuantitativeResult result(maybeStates.size()); storm::utility::vector::setVectorValues(result.getValues(), player1Prob1States, storm::utility::one()); - storm::utility::vector::setVectorValues(result.getValues(), maybeStates, lowerValues); - - STORM_LOG_ASSERT(gameSolver->hasSchedulers(), "Expected to have schedulers available after solving game."); - - std::vector const& player1Scheduler = gameSolver->getPlayer1SchedulerChoices(); - std::vector const& player2Scheduler = gameSolver->getPlayer2SchedulerChoices(); - + storm::utility::vector::setVectorValues(result.getValues(), maybeStates, values); + // Obtain strategies from solver and fuse them with the pre-existing strategy pair for the qualitative result. uint64_t previousPlayer1MaybeStates = 0; uint64_t previousPlayer2MaybeStates = 0; @@ -650,6 +688,7 @@ namespace storm { STORM_LOG_TRACE("Using sparse solving."); // (0) Start by transforming the necessary symbolic elements to explicit ones. + auto translationStart = std::chrono::high_resolution_clock::now(); storm::dd::Odd odd = game.getReachableStates().createOdd(); std::vector> labelingVariableSets = {game.getPlayer1Variables(), game.getPlayer2Variables()}; @@ -701,6 +740,8 @@ namespace storm { storm::storage::BitVector initialStates = initialStatesBdd.toVector(odd); storm::storage::BitVector constraintStates = constraintStatesBdd.toVector(odd); storm::storage::BitVector targetStates = targetStatesBdd.toVector(odd); + auto translationEnd = std::chrono::high_resolution_clock::now(); + STORM_LOG_DEBUG("Translation to explicit representation completed in " << std::chrono::duration_cast(translationEnd - translationStart).count() << "ms."); // Prepare the two strategies. abstraction::ExplicitGameStrategyPair minStrategyPair(initialStates.size(), transitionMatrix.getRowGroupCount()); @@ -715,12 +756,6 @@ namespace storm { } auto qualitativeEnd = std::chrono::high_resolution_clock::now(); STORM_LOG_DEBUG("Qualitative computation completed in " << std::chrono::duration_cast(qualitativeEnd - qualitativeStart).count() << "ms."); - -// std::cout << transitionMatrix << std::endl; -// std::cout << labeling.size() << std::endl; -// std::cout << initialStates << std::endl; -// std::cout << constraintStates << std::endl; -// std::cout << targetStates << std::endl; // (2) compute the states for which we have to determine quantitative information. storm::storage::BitVector maybeMin = ~(qualitativeResult.getProb0Min().getStates() | qualitativeResult.getProb1Min().getStates()); @@ -751,12 +786,10 @@ namespace storm { if (!qualitativeRefinement) { // At this point, we know that we cannot answer the query without further numeric computation. STORM_LOG_TRACE("Starting numerical solution step."); - - auto quantitativeStart = std::chrono::high_resolution_clock::now(); - ExplicitQuantitativeResultMinMax quantitativeResult; // (7) Solve the min values and check whether we can give the answer already. + auto quantitativeStart = std::chrono::high_resolution_clock::now(); quantitativeResult.setMin(computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Minimize, transitionMatrix, player1Groups, qualitativeResult, maybeMin, minStrategyPair)); result = checkForResultAfterQuantitativeCheck(checkTask, storm::OptimizationDirection::Minimize, quantitativeResult.getMin().getRange(initialStates)); if (result) { @@ -764,12 +797,11 @@ namespace storm { } // (8) Solve the max values and check whether we can give the answer already. - quantitativeResult.setMax(computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Maximize, transitionMatrix, player1Groups, qualitativeResult, maybeMax, maxStrategyPair)); + quantitativeResult.setMax(computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Maximize, transitionMatrix, player1Groups, qualitativeResult, maybeMax, maxStrategyPair, &quantitativeResult.getMin(), &minStrategyPair)); result = checkForResultAfterQuantitativeCheck(checkTask, storm::OptimizationDirection::Maximize, quantitativeResult.getMax().getRange(initialStates)); if (result) { return result; } - auto quantitativeEnd = std::chrono::high_resolution_clock::now(); STORM_LOG_DEBUG("Obtained quantitative bounds [" << quantitativeResult.getMin().getRange(initialStates).first << ", " << quantitativeResult.getMax().getRange(initialStates).second << "] on the actual value for the initial states in " << std::chrono::duration_cast(quantitativeEnd - quantitativeStart).count() << "ms."); @@ -780,15 +812,13 @@ namespace storm { } // Make sure that all strategies are still valid strategies. - STORM_LOG_ASSERT(minStrategyPair.getNumberOfUndefinedPlayer1States() == targetStates.getNumberOfSetBits() && minStrategyPair.getNumberOfUndefinedPlayer2States() == 0, "Minimal strategy pair has undefined choices for some relevant states."); - STORM_LOG_ASSERT(maxStrategyPair.getNumberOfUndefinedPlayer1States() == targetStates.getNumberOfSetBits() && maxStrategyPair.getNumberOfUndefinedPlayer2States() == 0, "Maximal strategy pair has undefined choices for some relevant states."); - - exit(-1); + STORM_LOG_ASSERT(minStrategyPair.getNumberOfUndefinedPlayer1States() <= targetStates.getNumberOfSetBits(), "Expected at most " << targetStates.getNumberOfSetBits() << " (number of target states) player 1 states with undefined choice but got " << minStrategyPair.getNumberOfUndefinedPlayer1States() << "."); + STORM_LOG_ASSERT(maxStrategyPair.getNumberOfUndefinedPlayer1States() <= targetStates.getNumberOfSetBits(), "Expected at most " << targetStates.getNumberOfSetBits() << " (number of target states) player 1 states with undefined choice but got " << maxStrategyPair.getNumberOfUndefinedPlayer1States() << "."); auto quantitativeRefinementStart = std::chrono::high_resolution_clock::now(); -// // (10) If we arrived at this point, it means that we have all qualitative and quantitative -// // information about the game, but we could not yet answer the query. In this case, we need to refine. -// refiner.refine(game, transitionMatrixBdd, quantitativeResult); + // (10) If we arrived at this point, it means that we have all qualitative and quantitative + // information about the game, but we could not yet answer the query. In this case, we need to refine. + refiner.refine(game, odd, transitionMatrix, player1Groups, player1Labeling, player2Labeling, initialStates, constraintStates, targetStates, quantitativeResult, minStrategyPair, maxStrategyPair); auto quantitativeRefinementEnd = std::chrono::high_resolution_clock::now(); STORM_LOG_DEBUG("Quantitative refinement completed in " << std::chrono::duration_cast(quantitativeRefinementEnd - quantitativeRefinementStart).count() << "ms."); } diff --git a/src/storm/solver/GameSolver.h b/src/storm/solver/GameSolver.h index 6c724e33c..68f7c3559 100644 --- a/src/storm/solver/GameSolver.h +++ b/src/storm/solver/GameSolver.h @@ -39,8 +39,12 @@ namespace storm { * @param player2Dir 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 player1Choices If provided along with the storage for player 2 choices, the scheduler decisions + * are tracked within these two vectors. + * @param player2Choices If provided along with the storage for player 1 choices, the scheduler decisions + * are tracked within these two vectors. */ - virtual bool solveGame(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector& x, std::vector const& b) const = 0; + virtual bool solveGame(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector& x, std::vector const& b, std::vector* player1Choices = nullptr, std::vector* player2Choices = nullptr) const = 0; /*! * Performs (repeated) matrix-vector multiplication with the given parameters, i.e. computes diff --git a/src/storm/solver/StandardGameSolver.cpp b/src/storm/solver/StandardGameSolver.cpp index 3d9e4975d..c57ff38b8 100644 --- a/src/storm/solver/StandardGameSolver.cpp +++ b/src/storm/solver/StandardGameSolver.cpp @@ -57,12 +57,12 @@ namespace storm { } template - bool StandardGameSolver::solveGame(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector& x, std::vector const& b) const { + bool StandardGameSolver::solveGame(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector& x, std::vector const& b, std::vector* player1Choices, std::vector* player2Choices) const { switch (getMethod(env, std::is_same::value)) { case GameMethod::ValueIteration: - return solveGameValueIteration(env, player1Dir, player2Dir, x, b); + return solveGameValueIteration(env, player1Dir, player2Dir, x, b, player1Choices, player2Choices); case GameMethod::PolicyIteration: - return solveGamePolicyIteration(env, player1Dir, player2Dir, x, b); + return solveGamePolicyIteration(env, player1Dir, player2Dir, x, b, player1Choices, player2Choices); default: STORM_LOG_THROW(false, storm::exceptions::InvalidEnvironmentException, "This solver does not implement the selected solution method"); } @@ -70,21 +70,39 @@ namespace storm { } template - bool StandardGameSolver::solveGamePolicyIteration(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector& x, std::vector const& b) const { + bool StandardGameSolver::solveGamePolicyIteration(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector& x, std::vector const& b, std::vector* providedPlayer1Choices, std::vector* providedPlayer2Choices) const { // Create the initial choice selections. - std::vector player1Choices; + std::vector* player1Choices; + std::unique_ptr> localPlayer1Choices; + std::vector* player2Choices; + std::unique_ptr> localPlayer2Choices; + + if (providedPlayer1Choices && providedPlayer2Choices) { + player1Choices = providedPlayer1Choices; + player2Choices = providedPlayer2Choices; + } else { + localPlayer1Choices = std::make_unique>(); + player1Choices = localPlayer1Choices.get(); + localPlayer2Choices = std::make_unique>(); + player2Choices = localPlayer2Choices.get(); + } + if (this->hasSchedulerHints()) { - player1Choices = this->player1ChoicesHint.get(); + *player1Choices = this->player1ChoicesHint.get(); } else if (this->player1RepresentedByMatrix()) { // Player 1 represented by matrix. - player1Choices = std::vector(this->getPlayer1Matrix().getRowGroupCount(), 0); + *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); + *player1Choices = this->getPlayer1Grouping(); + player1Choices->resize(player1Choices->size() - 1); + } + if (this->hasSchedulerHints()) { + *player2Choices = this->player2ChoicesHint.get(); + } else if (!(providedPlayer1Choices && providedPlayer2Choices)) { + player2Choices->resize(this->player2Matrix.getRowGroupCount()); } - std::vector player2Choices = this->hasSchedulerHints() ? this->player2ChoicesHint.get() : std::vector(this->player2Matrix.getRowGroupCount(), 0); if (!auxiliaryP2RowGroupVector) { auxiliaryP2RowGroupVector = std::make_unique>(this->player2Matrix.getRowGroupCount()); @@ -119,7 +137,7 @@ namespace storm { // Solve the equation system induced by the two schedulers. storm::storage::SparseMatrix submatrix; - getInducedMatrixVector(x, b, player1Choices, player2Choices, submatrix, subB); + getInducedMatrixVector(x, b, *player1Choices, *player2Choices, submatrix, subB); if (this->linearEquationSolverFactory->getEquationProblemFormat(environmentOfSolver) == LinearEquationSolverProblemFormat::EquationSystem) { submatrix.convertToEquationSystem(); } @@ -140,14 +158,14 @@ namespace storm { // 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); + bool schedulerImproved = extractChoices(player1Dir, player2Dir, x, b, *auxiliaryP2RowGroupVector, *player1Choices, *player2Choices); // If the scheduler did not improve, we are done. if (!schedulerImproved) { status = Status::Converged; } else { // Update the solver. - getInducedMatrixVector(x, b, player1Choices, player2Choices, submatrix, subB); + getInducedMatrixVector(x, b, *player1Choices, *player2Choices, submatrix, subB); submatrix.convertToEquationSystem(); submatrixSolver->setMatrix(std::move(submatrix)); } @@ -160,9 +178,9 @@ namespace storm { reportStatus(status, iterations); // If requested, we store the scheduler for retrieval. - if (this->isTrackSchedulersSet()) { - this->player1SchedulerChoices = std::move(player1Choices); - this->player2SchedulerChoices = std::move(player2Choices); + if (this->isTrackSchedulersSet() && !(providedPlayer1Choices && providedPlayer2Choices)) { + this->player1SchedulerChoices = std::move(*player1Choices); + this->player2SchedulerChoices = std::move(*player2Choices); } if (!this->isCachingEnabled()) { @@ -182,7 +200,7 @@ namespace storm { } template - bool StandardGameSolver::solveGameValueIteration(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector& x, std::vector const& b) const { + bool StandardGameSolver::solveGameValueIteration(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector& x, std::vector const& b, std::vector* player1Choices, std::vector* player2Choices) const { if (!multiplierPlayer2Matrix) { multiplierPlayer2Matrix = storm::solver::MultiplierFactory().create(env, player2Matrix); @@ -202,7 +220,9 @@ namespace storm { std::vector& reducedPlayer2Result = *auxiliaryP2RowGroupVector; - bool trackSchedulersInValueIteration = this->isTrackSchedulersSet() && !this->hasUniqueSolution(); + bool trackingSchedulersInProvidedStorage = player1Choices && player2Choices; + bool trackSchedulers = this->isTrackSchedulersSet() || trackingSchedulersInProvidedStorage; + bool trackSchedulersInValueIteration = trackSchedulers && !this->hasUniqueSolution(); if (this->hasSchedulerHints()) { // Solve the equation system induced by the two schedulers. storm::storage::SparseMatrix submatrix; @@ -221,11 +241,11 @@ namespace storm { submatrixSolver->solveEquations(env, x, *auxiliaryP1RowGroupVector); // If requested, we store the scheduler for retrieval. Initialize the schedulers to the hint we have. - if (trackSchedulersInValueIteration) { + if (trackSchedulersInValueIteration && !trackingSchedulersInProvidedStorage) { this->player1SchedulerChoices = this->player1ChoicesHint.get(); this->player2SchedulerChoices = this->player2ChoicesHint.get(); } - } else if (trackSchedulersInValueIteration) { + } else if (trackSchedulersInValueIteration && !trackingSchedulersInProvidedStorage) { // 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); @@ -240,7 +260,9 @@ namespace storm { Status status = Status::InProgress; while (status == Status::InProgress) { - multiplyAndReduce(env, player1Dir, player2Dir, *currentX, &b, *multiplierPlayer2Matrix, reducedPlayer2Result, *newX, trackSchedulersInValueIteration ? &this->player1SchedulerChoices.get() : nullptr, trackSchedulersInValueIteration ? &this->player2SchedulerChoices.get() : nullptr); + multiplyAndReduce(env, player1Dir, player2Dir, *currentX, &b, *multiplierPlayer2Matrix, reducedPlayer2Result, *newX, + trackSchedulersInValueIteration ? (trackingSchedulersInProvidedStorage ? player1Choices : &this->player1SchedulerChoices.get()) : nullptr, + trackSchedulersInValueIteration ? (trackingSchedulersInProvidedStorage ? player2Choices : &this->player2SchedulerChoices.get()) : nullptr); // Determine whether the method converged. if (storm::utility::vector::equalModuloPrecision(*currentX, *newX, precision, relative)) { @@ -262,10 +284,14 @@ namespace storm { } // If requested, we store the scheduler for retrieval. - 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 (trackSchedulers && this->hasUniqueSolution()) { + if (trackingSchedulersInProvidedStorage) { + extractChoices(player1Dir, player2Dir, x, b, *auxiliaryP2RowGroupVector, *player1Choices, *player2Choices); + } else { + 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()) { diff --git a/src/storm/solver/StandardGameSolver.h b/src/storm/solver/StandardGameSolver.h index 338966d27..1af23601f 100644 --- a/src/storm/solver/StandardGameSolver.h +++ b/src/storm/solver/StandardGameSolver.h @@ -19,7 +19,7 @@ namespace storm { 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 bool solveGame(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector& x, std::vector const& b, std::vector* player1Choices = nullptr, std::vector* player2Choices = nullptr) 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; virtual void clearCache() const override; @@ -27,8 +27,8 @@ namespace storm { private: GameMethod getMethod(Environment const& env, bool isExactMode) const; - bool solveGamePolicyIteration(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector& x, std::vector const& b) const; - bool solveGameValueIteration(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector& x, std::vector const& b) const; + bool solveGamePolicyIteration(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector& x, std::vector const& b, std::vector* player1Choices = nullptr, std::vector* player2Choices = nullptr) const; + bool solveGameValueIteration(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector& x, std::vector const& b, std::vector* player1Choices = nullptr, std::vector* player2Choices = nullptr) 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& player2ReducedResult, std::vector& player1ReducedResult, std::vector* player1SchedulerChoices = nullptr, std::vector* player2SchedulerChoices = nullptr) const; diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index eb582f980..6e4c185ea 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -1395,7 +1395,7 @@ namespace storm { // If we were asked to produce strategies, we propagate that by triggering another iteration. // We only do this if at least one strategy will be produced. - produceStrategiesInIteration = !produceStrategiesInIteration && ((player1Strategy && player1Direction == OptimizationDirection::Maximize) || (player2Strategy && player2Direction == OptimizationDirection::Maximize)); + produceStrategiesInIteration = !produceStrategiesInIteration && (player1Strategy || player2Strategy); } else { result.player1States = player1Solution; result.player2States = player2Solution;