From c2e646b887c05dda312a498360f360dbe76ecc4d Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 26 Mar 2018 22:30:36 +0200 Subject: [PATCH] working towards predicate synthesis from explicit (qualitative) result for game-based abstraction --- .../abstraction/ExplicitGameStrategy.cpp | 19 ++ src/storm/abstraction/ExplicitGameStrategy.h | 5 +- .../abstraction/ExplicitGameStrategyPair.cpp | 6 + .../abstraction/ExplicitGameStrategyPair.h | 3 + src/storm/abstraction/MenuGameRefiner.cpp | 189 ++++++++++++------ src/storm/abstraction/MenuGameRefiner.h | 26 +-- .../abstraction/GameBasedMdpModelChecker.cpp | 12 ++ src/storm/storage/dd/Odd.cpp | 22 ++ src/storm/storage/dd/Odd.h | 13 ++ src/storm/utility/graph.cpp | 6 +- 10 files changed, 225 insertions(+), 76 deletions(-) diff --git a/src/storm/abstraction/ExplicitGameStrategy.cpp b/src/storm/abstraction/ExplicitGameStrategy.cpp index 642c274b7..2703ac3a5 100644 --- a/src/storm/abstraction/ExplicitGameStrategy.cpp +++ b/src/storm/abstraction/ExplicitGameStrategy.cpp @@ -35,5 +35,24 @@ namespace storm { } } + std::ostream& operator<<(std::ostream& out, ExplicitGameStrategy const& strategy) { + std::vector undefinedStates; + for (uint64_t state = 0; state < strategy.getNumberOfStates(); ++state) { + uint64_t choice = strategy.getChoice(state); + if (choice == ExplicitGameStrategy::UNDEFINED) { + undefinedStates.emplace_back(state); + } else { + out << state << " -> " << choice << std::endl; + } + } + out << "undefined states: "; + for (auto state : undefinedStates) { + out << state << ", "; + } + out << std::endl; + + return out; + } + } } diff --git a/src/storm/abstraction/ExplicitGameStrategy.h b/src/storm/abstraction/ExplicitGameStrategy.h index 8315e9101..aabe6226f 100644 --- a/src/storm/abstraction/ExplicitGameStrategy.h +++ b/src/storm/abstraction/ExplicitGameStrategy.h @@ -2,6 +2,7 @@ #include #include +#include namespace storm { namespace abstraction { @@ -18,10 +19,12 @@ namespace storm { void setChoice(uint64_t state, uint64_t choice); bool hasDefinedChoice(uint64_t state) const; void undefineAll(); - + private: std::vector choices; }; + std::ostream& operator<<(std::ostream& out, ExplicitGameStrategy const& strategy); + } } diff --git a/src/storm/abstraction/ExplicitGameStrategyPair.cpp b/src/storm/abstraction/ExplicitGameStrategyPair.cpp index d773f9ec5..9f42ea642 100644 --- a/src/storm/abstraction/ExplicitGameStrategyPair.cpp +++ b/src/storm/abstraction/ExplicitGameStrategyPair.cpp @@ -27,5 +27,11 @@ namespace storm { return player2Strategy; } + std::ostream& operator<<(std::ostream& out, ExplicitGameStrategyPair const& strategyPair) { + out << "player 1 strategy: " << std::endl << strategyPair.getPlayer1Strategy() << std::endl; + out << "player 2 strategy: " << std::endl << strategyPair.getPlayer2Strategy() << std::endl; + return out; + } + } } diff --git a/src/storm/abstraction/ExplicitGameStrategyPair.h b/src/storm/abstraction/ExplicitGameStrategyPair.h index 6449c3ddd..e5774d7e1 100644 --- a/src/storm/abstraction/ExplicitGameStrategyPair.h +++ b/src/storm/abstraction/ExplicitGameStrategyPair.h @@ -1,6 +1,7 @@ #pragma once #include +#include #include "storm/abstraction/ExplicitGameStrategy.h" @@ -22,5 +23,7 @@ namespace storm { ExplicitGameStrategy player2Strategy; }; + std::ostream& operator<<(std::ostream& out, ExplicitGameStrategyPair const& strategyPair); + } } diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index 6b83338e7..a5d1f647e 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -394,9 +394,12 @@ namespace storm { // Derive predicates from lower choice. storm::dd::Bdd lowerChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && minPlayer1Strategy; + lowerChoice.template toAdd().exportToDot("lower.dot"); storm::dd::Bdd lowerChoice1 = (lowerChoice && minPlayer2Strategy).existsAbstract(variablesToAbstract); + lowerChoice1.template toAdd().exportToDot("lower1.dot"); storm::dd::Bdd lowerChoice2 = (lowerChoice && maxPlayer2Strategy).existsAbstract(variablesToAbstract); - + lowerChoice2.template toAdd().exportToDot("lower2.dot"); + bool lowerChoicesDifferent = !lowerChoice1.exclusiveOr(lowerChoice2).isZero() && !lowerChoice1.isZero() && !lowerChoice2.isZero(); if (lowerChoicesDifferent) { STORM_LOG_TRACE("Deriving predicate based on lower choice."); @@ -523,30 +526,12 @@ namespace storm { predicates.back().push_back(initialExpression.changeManager(expressionManager).substitute(lastSubstitution)); return std::make_pair(predicates, stepVariableToCopiedVariableMap); } - - template - boost::optional MenuGameRefiner::derivePredicatesFromInterpolation(storm::abstraction::MenuGame const& game, SymbolicPivotStateResult const& symbolicPivotStateResult, storm::dd::Bdd const& minPlayer1Strategy, storm::dd::Bdd const& minPlayer2Strategy, storm::dd::Bdd const& maxPlayer1Strategy, storm::dd::Bdd const& maxPlayer2Strategy) const { - - AbstractionInformation const& abstractionInformation = abstractor.get().getAbstractionInformation(); - - // Compute the most probable path from any initial state to the pivot state. - SymbolicMostProbablePathsResult symbolicMostProbablePathsResult; - if (!symbolicPivotStateResult.symbolicMostProbablePathsResult) { - symbolicMostProbablePathsResult = getMostProbablePathSpanningTree(game, symbolicPivotStateResult.fromDirection == storm::OptimizationDirection::Minimize ? minPlayer1Strategy && minPlayer2Strategy : maxPlayer1Strategy && maxPlayer2Strategy); - } else { - symbolicMostProbablePathsResult = symbolicPivotStateResult.symbolicMostProbablePathsResult.get(); - } - - // Create a new expression manager that we can use for the interpolation. - std::shared_ptr interpolationManager = abstractionInformation.getExpressionManager().clone(); - - // Build the trace of the most probable path in terms of which predicates hold in each step. - std::pair>, std::map> traceAndVariableSubstitution = buildTrace(*interpolationManager, game, symbolicMostProbablePathsResult.spanningTree, symbolicPivotStateResult.pivotState); - auto const& trace = traceAndVariableSubstitution.first; - auto const& variableSubstitution = traceAndVariableSubstitution.second; + + template + boost::optional derivePredicatesFromInterpolation(storm::expressions::ExpressionManager& interpolationManager, AbstractionInformation const& abstractionInformation, std::vector> const& trace, std::map const& variableSubstitution) { // Create solver and interpolation groups. - storm::solver::MathsatSmtSolver interpolatingSolver(*interpolationManager, storm::solver::MathsatSmtSolver::Options(true, false, true)); + storm::solver::MathsatSmtSolver interpolatingSolver(interpolationManager, storm::solver::MathsatSmtSolver::Options(true, false, true)); uint64_t stepCounter = 0; auto traceIt = trace.rbegin(); auto traceIte = trace.rend(); @@ -559,7 +544,7 @@ namespace storm { interpolatingSolver.add(predicate); } ++stepCounter; - + storm::solver::SmtSolver::CheckResult result = interpolatingSolver.check(); // If the result already became unsatisfiable if (result == storm::solver::SmtSolver::CheckResult::Unsat) { @@ -591,6 +576,33 @@ namespace storm { return boost::none; } + template + boost::optional MenuGameRefiner::derivePredicatesFromInterpolation(storm::abstraction::MenuGame const& game, SymbolicPivotStateResult const& symbolicPivotStateResult, storm::dd::Bdd const& minPlayer1Strategy, storm::dd::Bdd const& minPlayer2Strategy, storm::dd::Bdd const& maxPlayer1Strategy, storm::dd::Bdd const& maxPlayer2Strategy) const { + + AbstractionInformation const& abstractionInformation = abstractor.get().getAbstractionInformation(); + + // Compute the most probable path from any initial state to the pivot state. + SymbolicMostProbablePathsResult symbolicMostProbablePathsResult; + if (!symbolicPivotStateResult.symbolicMostProbablePathsResult) { + symbolicMostProbablePathsResult = getMostProbablePathSpanningTree(game, symbolicPivotStateResult.fromDirection == storm::OptimizationDirection::Minimize ? minPlayer1Strategy && minPlayer2Strategy : maxPlayer1Strategy && maxPlayer2Strategy); + } else { + symbolicMostProbablePathsResult = symbolicPivotStateResult.symbolicMostProbablePathsResult.get(); + } + + // Create a new expression manager that we can use for the interpolation. + std::shared_ptr interpolationManager = abstractionInformation.getExpressionManager().clone(); + + // Build the trace of the most probable path in terms of which predicates hold in each step. + std::pair>, std::map> traceAndVariableSubstitution = buildTrace(*interpolationManager, game, symbolicMostProbablePathsResult.spanningTree, symbolicPivotStateResult.pivotState); + + return storm::abstraction::derivePredicatesFromInterpolation(*interpolationManager, abstractionInformation, traceAndVariableSubstitution.first, traceAndVariableSubstitution.second); + } + + template + boost::optional MenuGameRefiner::derivePredicatesFromInterpolation(storm::abstraction::MenuGame const& game, ExplicitPivotStateResult const& pivotStateResult, storm::dd::Odd const& odd) const { + // TODO. + } + template bool MenuGameRefiner::refine(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, SymbolicQualitativeGameResultMinMax const& qualitativeResult) const { STORM_LOG_TRACE("Trying refinement after qualitative check."); @@ -613,6 +625,7 @@ namespace storm { // strategies and they differ. Hence, it is possible that we arrive at a point where no suitable pivot state // is found. In this case, we abort the qualitative refinement here. if (pivotStateCandidatesResult.pivotStates.isZero()) { + STORM_LOG_TRACE("Did not find pivot state in qualitative fragment."); return false; } STORM_LOG_ASSERT(!pivotStateCandidatesResult.pivotStates.isZero(), "Unable to proceed without pivot state candidates."); @@ -680,35 +693,25 @@ namespace storm { } template - ExplicitMostProbablePathsResult::ExplicitMostProbablePathsResult(ValueType const& maxProbability, std::vector>&& predecessors) : maxProbability(maxProbability), predecessors(std::move(predecessors)) { - // Intentionally left empty. - } - - template - ExplicitPivotStateResult::ExplicitPivotStateResult(uint64_t pivotState, storm::OptimizationDirection fromDirection, boost::optional>&& explicitMostProbablePathsResult) : pivotState(pivotState), fromDirection(fromDirection), explicitMostProbablePathsResult(std::move(explicitMostProbablePathsResult)) { - // Intentionally left empty. - } - - template - ExplicitPivotStateResult pickPivotState(AbstractionSettings::PivotSelectionHeuristic pivotSelectionHeuristic, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Grouping, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& relevantStates, storm::storage::BitVector const& targetStates, ExplicitQualitativeGameResultMinMax const& qualitativeResult, ExplicitGameStrategyPair const& minStrategyPair, ExplicitGameStrategyPair const& maxStrategyPair) { + boost::optional> pickPivotState(bool generatePredecessors, AbstractionSettings::PivotSelectionHeuristic pivotSelectionHeuristic, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Grouping, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& relevantStates, storm::storage::BitVector const& targetStates, ExplicitQualitativeGameResultMinMax const& qualitativeResult, ExplicitGameStrategyPair const& minStrategyPair, ExplicitGameStrategyPair const& maxStrategyPair) { // Perform Dijkstra search that stays within the relevant states and searches for a state in which the // strategies for the (commonly chosen) player 1 action leads to a player 2 state in which the choices differ. - ExplicitPivotStateResult explicitPivotStateResult; - explicitPivotStateResult.explicitMostProbablePathsResult = ExplicitMostProbablePathsResult(); - auto& explicitMostProbablePathsResult = explicitPivotStateResult.explicitMostProbablePathsResult.get(); + ExplicitPivotStateResult result; bool probabilityDistances = pivotSelectionHeuristic == storm::settings::modules::AbstractionSettings::PivotSelectionHeuristic::MostProbablePath; uint64_t numberOfStates = initialStates.size(); ValueType inftyDistance = probabilityDistances ? storm::utility::zero() : storm::utility::infinity(); ValueType zeroDistance = probabilityDistances ? storm::utility::one() : storm::utility::zero(); std::vector distances(numberOfStates, inftyDistance); - explicitMostProbablePathsResult.predecessors.resize(numberOfStates, std::make_pair(0, 0)); + if (generatePredecessors) { + result.predecessors.resize(numberOfStates, std::make_pair(0, 0)); + } // Use set as priority queue with unique membership; default comparison on pair works fine if distance is // the first entry. std::set, std::greater>> dijkstraQueue; - + for (auto initialState : initialStates) { if (!relevantStates.get(initialState)) { continue; @@ -718,28 +721,44 @@ namespace storm { dijkstraQueue.emplace(zeroDistance, initialState); } + // For some heuristics, we need to potentially find more than just one pivot. + bool foundPivotState = false; + ValueType maximalDeviation = storm::utility::zero(); + while (!dijkstraQueue.empty()) { - uint64_t currentState = (*dijkstraQueue.begin()).second; + auto distanceStatePair = *dijkstraQueue.begin(); + uint64_t currentState = distanceStatePair.second; + ValueType currentDistance = distanceStatePair.first; dijkstraQueue.erase(dijkstraQueue.begin()); + if (foundPivotState && currentDistance > result.distance) { + return result; + } + // Determine whether the current state is a pivot state. bool isPivotState = false; if (minStrategyPair.getPlayer1Strategy().hasDefinedChoice(currentState)) { uint64_t player2Successor = minStrategyPair.getPlayer1Strategy().getChoice(currentState); - if (minStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2Successor) && maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2Successor)) { + if (minStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2Successor) && maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2Successor) && minStrategyPair.getPlayer2Strategy().getChoice(player2Successor) != maxStrategyPair.getPlayer2Strategy().getChoice(player2Successor)) { isPivotState = true; } } else if (maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(currentState)) { uint64_t player2Successor = maxStrategyPair.getPlayer1Strategy().getChoice(currentState); - if (minStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2Successor) && maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2Successor)) { + if (minStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2Successor) && maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2Successor) && minStrategyPair.getPlayer2Strategy().getChoice(player2Successor) != maxStrategyPair.getPlayer2Strategy().getChoice(player2Successor)) { isPivotState = true; } } // If it is indeed a pivot state, we can abort the search here. if (isPivotState) { - explicitPivotStateResult.pivotState = currentState; - return explicitPivotStateResult; + if (foundPivotState && haveQuantitativeResults && deviationOfCurrentState > currentPivotState) { + result.pivotState = currentState; + maximalDeviation = deviationForCurrentState; + } else if (!foundPivotState) { + result.pivotState = currentState; + result.distance = distances[currentState]; + foundPivotState = true; + } } // Otherwise, we explore all its relevant successors. @@ -753,10 +772,12 @@ namespace storm { continue; } - ValueType alternateDistance = probabilityDistances ? distances[currentState] * entry.getValue() : distances[currentState] + storm::utility::one(); + ValueType alternateDistance = probabilityDistances ? currentDistance * entry.getValue() : currentDistance + storm::utility::one(); if ((probabilityDistances && alternateDistance > distances[player1Successor]) || (!probabilityDistances && alternateDistance < distances[player1Successor])) { distances[player1Successor] = alternateDistance; - explicitMostProbablePathsResult.predecessors[player1Successor] = std::make_pair(currentState, minPlayer2Successor); + if (generatePredecessors) { + result.predecessors[player1Successor] = std::make_pair(currentState, minPlayer2Successor); + } dijkstraQueue.emplace(alternateDistance, player1Successor); } } @@ -771,10 +792,12 @@ namespace storm { continue; } - ValueType alternateDistance = probabilityDistances ? distances[currentState] * entry.getValue() : distances[currentState] + storm::utility::one(); + ValueType alternateDistance = probabilityDistances ? currentDistance * entry.getValue() : currentDistance + storm::utility::one(); if ((probabilityDistances && alternateDistance > distances[player1Successor]) || (!probabilityDistances && alternateDistance < distances[player1Successor])) { distances[player1Successor] = alternateDistance; - explicitMostProbablePathsResult.predecessors[player1Successor] = std::make_pair(currentState, maxPlayer2Successor); + if (generatePredecessors) { + result.predecessors[player1Successor] = std::make_pair(currentState, maxPlayer2Successor); + } dijkstraQueue.emplace(alternateDistance, player1Successor); } } @@ -783,24 +806,76 @@ namespace storm { // If we arrived at this point, we have explored all relevant states, but none of them was a pivot state, // which can happen when trying to refine using the qualitative result only. - return explicitPivotStateResult; + return boost::none; } 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, ExplicitQualitativeGameResultMinMax const& qualitativeResult, ExplicitGameStrategyPair const& minStrategyPair, ExplicitGameStrategyPair const& maxStrategyPair) const { + STORM_LOG_THROW(heuristic != AbstractionSettings::PivotSelectionHeuristic::MaxWeightedDeviation, storm::exceptions::NotImplementedException, "The pivot selection heuristic 'maximal weighted deviation' is not supported by the sparse solution strategy."); + // 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()); - - ExplicitPivotStateResult pivotStateResult = pickPivotState(pivotSelectionHeuristic, transitionMatrix, player1Grouping, initialStates, relevantStates, targetStates, qualitativeResult, minStrategyPair, maxStrategyPair); + + boost::optional> optionalPivotStateResult = pickPivotState(useInterpolation, pivotSelectionHeuristic, transitionMatrix, player1Grouping, initialStates, relevantStates, targetStates, qualitativeResult, minStrategyPair, maxStrategyPair); // If there was no pivot state, continue the search. - if (!pivotStateResult.pivotState) { + if (!optionalPivotStateResult) { + STORM_LOG_TRACE("Did not find pivot state in qualitative fragment."); return false; } // Otherwise, we can refine. - storm::dd::Bdd pivotState = storm::dd::Bdd::getEncoding(game.getManager(), pivotStateResult.pivotState.get(), odd, game.getRowVariables()); + 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); + minPlayer1Strategy |= symbolicPivotState && abstractionInformation.encodePlayer1Choice(player1Labeling[transitionMatrix.getRowGroupIndices()[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); + maxPlayer1Strategy |= symbolicPivotState && abstractionInformation.encodePlayer1Choice(player1Labeling[transitionMatrix.getRowGroupIndices()[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); + + } + 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 @@ -818,16 +893,16 @@ namespace storm { STORM_LOG_ASSERT(!pivotStateCandidatesResult.pivotStates.isZero(), "Unable to refine without pivot state candidates."); // Now that we have the pivot state candidates, we need to pick one. - SymbolicPivotStateResult SymbolicPivotStateResult = pickPivotState(pivotSelectionHeuristic, game, pivotStateCandidatesResult, boost::none, quantitativeResult); + SymbolicPivotStateResult symbolicPivotStateResult = pickPivotState(pivotSelectionHeuristic, game, pivotStateCandidatesResult, boost::none, quantitativeResult); boost::optional predicates; if (useInterpolation) { - predicates = derivePredicatesFromInterpolation(game, SymbolicPivotStateResult, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy); + predicates = derivePredicatesFromInterpolation(game, symbolicPivotStateResult, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy); } if (predicates) { STORM_LOG_TRACE("Obtained predicates by interpolation."); } else { - predicates = derivePredicatesFromPivotState(game, SymbolicPivotStateResult.pivotState, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy); + predicates = derivePredicatesFromPivotState(game, symbolicPivotStateResult.pivotState, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy); } STORM_LOG_THROW(static_cast(predicates), storm::exceptions::InvalidStateException, "Predicates needed to continue."); diff --git a/src/storm/abstraction/MenuGameRefiner.h b/src/storm/abstraction/MenuGameRefiner.h index 7a912e947..d4d913a1f 100644 --- a/src/storm/abstraction/MenuGameRefiner.h +++ b/src/storm/abstraction/MenuGameRefiner.h @@ -73,26 +73,17 @@ namespace storm { boost::optional> symbolicMostProbablePathsResult; }; - template - struct ExplicitMostProbablePathsResult { - ExplicitMostProbablePathsResult() = default; - ExplicitMostProbablePathsResult(ValueType const& maxProbability, std::vector>&& predecessors); - - /// The maximal probability with which the state in question is reached. - ValueType maxProbability; - - /// The predecessors for the states to obtain this probability. - std::vector> predecessors; - }; - template struct ExplicitPivotStateResult { ExplicitPivotStateResult() = default; - ExplicitPivotStateResult(uint64_t pivotState, storm::OptimizationDirection fromDirection, boost::optional>&& explicitMostProbablePathsResult = boost::none); - boost::optional pivotState; - storm::OptimizationDirection fromDirection; - boost::optional> explicitMostProbablePathsResult; + uint64_t pivotState; + + /// The distance with which the state in question is reached. + ValueType distance; + + /// The predecessors for the states to obtain the given distance. + std::vector> predecessors; }; class ExplicitQualitativeGameResultMinMax; @@ -155,7 +146,8 @@ namespace storm { boost::optional derivePredicatesFromInterpolation(storm::abstraction::MenuGame const& game, SymbolicPivotStateResult const& symbolicPivotStateResult, storm::dd::Bdd const& minPlayer1Strategy, storm::dd::Bdd const& minPlayer2Strategy, storm::dd::Bdd const& maxPlayer1Strategy, storm::dd::Bdd const& maxPlayer2Strategy) const; std::pair>, std::map> buildTrace(storm::expressions::ExpressionManager& expressionManager, storm::abstraction::MenuGame const& game, storm::dd::Bdd const& spanningTree, storm::dd::Bdd const& pivotState) const; - + boost::optional derivePredicatesFromInterpolation(storm::abstraction::MenuGame const& game, ExplicitPivotStateResult const& pivotStateResult, storm::dd::Odd const& odd) const; + void performRefinement(std::vector const& refinementCommands) const; /// The underlying abstractor to refine. diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 2b2980e95..25b110e06 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -157,6 +157,12 @@ namespace storm { } } } + } else { + if (player2Direction == storm::OptimizationDirection::Minimize && (prob1 && initialStates) == initialStates) { + result = std::make_unique>(storm::storage::sparse::state_type(0), storm::utility::one()); + } else if (player2Direction == storm::OptimizationDirection::Maximize && (prob0 && initialStates) == initialStates) { + result = std::make_unique>(storm::storage::sparse::state_type(0), storm::utility::zero()); + } } return result; @@ -204,6 +210,12 @@ namespace storm { } } } + } else { + if (player2Direction == storm::OptimizationDirection::Minimize && initialStates.isSubsetOf(prob1)) { + result = std::make_unique>(storm::storage::sparse::state_type(0), storm::utility::one()); + } else if (player2Direction == storm::OptimizationDirection::Maximize && initialStates.isSubsetOf(prob0)) { + result = std::make_unique>(storm::storage::sparse::state_type(0), storm::utility::zero()); + } } return result; diff --git a/src/storm/storage/dd/Odd.cpp b/src/storm/storage/dd/Odd.cpp index b94295f0e..0a0712b2b 100644 --- a/src/storm/storage/dd/Odd.cpp +++ b/src/storm/storage/dd/Odd.cpp @@ -4,6 +4,8 @@ #include #include +#include "storm/storage/BitVector.h" + #include "storm/utility/macros.h" #include "storm/exceptions/InvalidArgumentException.h" #include "storm/utility/file.h" @@ -130,6 +132,26 @@ namespace storm { storm::utility::closeFile(dotFile); } + void getEncodingRec(Odd const& odd, uint64_t index, uint64_t offset, storm::storage::BitVector& result) { + if (odd.isTerminalNode()) { + return; + } + + bool thenPath = false; + if (odd.getElseOffset() <= offset) { + thenPath = true; + offset -= odd.getElseOffset(); + result.set(index); + } + getEncodingRec(thenPath ? odd.getThenSuccessor() : odd.getElseSuccessor(), index + 1, offset, result); + } + + storm::storage::BitVector Odd::getEncoding(uint64_t offset, uint64_t variableCount) const { + storm::storage::BitVector result(variableCount > 0 ? variableCount : this->getHeight()); + getEncodingRec(*this, 0, offset, result); + return result; + } + void Odd::addToLevelToOddNodesMap(std::map>& levelToOddNodesMap, uint_fast64_t level) const { levelToOddNodesMap[level].emplace(this); if (!this->isTerminalNode()) { diff --git a/src/storm/storage/dd/Odd.h b/src/storm/storage/dd/Odd.h index 0cb4a307c..d62bf1844 100644 --- a/src/storm/storage/dd/Odd.h +++ b/src/storm/storage/dd/Odd.h @@ -7,6 +7,10 @@ #include namespace storm { + namespace storage { + class BitVector; + } + namespace dd { class Odd { public: @@ -119,6 +123,15 @@ namespace storm { */ void exportToDot(std::string const& filename) const; + /*! + * Retrieves the encoding for the given offset. + * + * @param offset The target offset. + * @param variableCount If not null, this indicates how many variables are contained in the encoding. If 0, + * this number is automatically determined. + */ + storm::storage::BitVector getEncoding(uint64_t offset, uint64_t variableCount = 0) const; + private: /*! * Adds all nodes below the current one to the given mapping. diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index 9fcd19b74..eb582f980 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -1315,7 +1315,7 @@ namespace storm { while (!stack.empty()) { currentState = stack.back(); stack.pop_back(); - + for (auto player2PredecessorEntry : player1BackwardTransitions.getRow(currentState)) { uint64_t player2Predecessor = player2PredecessorEntry.getColumn(); if (!player2Solution.get(player2PredecessorEntry.getColumn())) { @@ -1392,6 +1392,10 @@ namespace storm { if (result.player1States == player1Solution) { maybeStatesDone = true; result.player2States = player2Solution; + + // 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)); } else { result.player1States = player1Solution; result.player2States = player2Solution;