diff --git a/src/storm/abstraction/ExplicitGameStrategy.cpp b/src/storm/abstraction/ExplicitGameStrategy.cpp new file mode 100644 index 000000000..642c274b7 --- /dev/null +++ b/src/storm/abstraction/ExplicitGameStrategy.cpp @@ -0,0 +1,39 @@ +#include "storm/abstraction/ExplicitGameStrategy.h" + +namespace storm { + namespace abstraction { + + const uint64_t ExplicitGameStrategy::UNDEFINED = std::numeric_limits::max(); + + ExplicitGameStrategy::ExplicitGameStrategy(uint64_t numberOfStates) : choices(numberOfStates, UNDEFINED) { + // Intentionally left empty. + } + + ExplicitGameStrategy::ExplicitGameStrategy(std::vector&& choices) : choices(std::move(choices)) { + // Intentionally left empty. + } + + uint64_t ExplicitGameStrategy::getNumberOfStates() const { + return choices.size(); + } + + uint64_t ExplicitGameStrategy::getChoice(uint64_t state) const { + return choices[state]; + } + + void ExplicitGameStrategy::setChoice(uint64_t state, uint64_t choice) { + choices[state] = choice; + } + + bool ExplicitGameStrategy::hasDefinedChoice(uint64_t state) const { + return choices[state] != UNDEFINED; + } + + void ExplicitGameStrategy::undefineAll() { + for (auto& e : choices) { + e = UNDEFINED; + } + } + + } +} diff --git a/src/storm/abstraction/ExplicitGameStrategy.h b/src/storm/abstraction/ExplicitGameStrategy.h new file mode 100644 index 000000000..8315e9101 --- /dev/null +++ b/src/storm/abstraction/ExplicitGameStrategy.h @@ -0,0 +1,27 @@ +#pragma once + +#include +#include + +namespace storm { + namespace abstraction { + + class ExplicitGameStrategy { + public: + static const uint64_t UNDEFINED; + + ExplicitGameStrategy(uint64_t numberOfStates); + ExplicitGameStrategy(std::vector&& choices); + + uint64_t getNumberOfStates() const; + uint64_t getChoice(uint64_t state) const; + void setChoice(uint64_t state, uint64_t choice); + bool hasDefinedChoice(uint64_t state) const; + void undefineAll(); + + private: + std::vector choices; + }; + + } +} diff --git a/src/storm/abstraction/ExplicitGameStrategyPair.cpp b/src/storm/abstraction/ExplicitGameStrategyPair.cpp new file mode 100644 index 000000000..d773f9ec5 --- /dev/null +++ b/src/storm/abstraction/ExplicitGameStrategyPair.cpp @@ -0,0 +1,31 @@ +#include "storm/abstraction/ExplicitGameStrategyPair.h" + +namespace storm { + namespace abstraction { + + ExplicitGameStrategyPair::ExplicitGameStrategyPair(uint64_t numberOfPlayer1States, uint64_t numberOfPlayer2States) : player1Strategy(numberOfPlayer1States), player2Strategy(numberOfPlayer2States) { + // Intentionally left empty. + } + + ExplicitGameStrategyPair::ExplicitGameStrategyPair(ExplicitGameStrategy&& player1Strategy, ExplicitGameStrategy&& player2Strategy) : player1Strategy(std::move(player1Strategy)), player2Strategy(std::move(player2Strategy)) { + // Intentionally left empty. + } + + ExplicitGameStrategy& ExplicitGameStrategyPair::getPlayer1Strategy() { + return player1Strategy; + } + + ExplicitGameStrategy const& ExplicitGameStrategyPair::getPlayer1Strategy() const { + return player1Strategy; + } + + ExplicitGameStrategy& ExplicitGameStrategyPair::getPlayer2Strategy() { + return player2Strategy; + } + + ExplicitGameStrategy const& ExplicitGameStrategyPair::getPlayer2Strategy() const { + return player2Strategy; + } + + } +} diff --git a/src/storm/abstraction/ExplicitGameStrategyPair.h b/src/storm/abstraction/ExplicitGameStrategyPair.h new file mode 100644 index 000000000..6449c3ddd --- /dev/null +++ b/src/storm/abstraction/ExplicitGameStrategyPair.h @@ -0,0 +1,26 @@ +#pragma once + +#include + +#include "storm/abstraction/ExplicitGameStrategy.h" + +namespace storm { + namespace abstraction { + + class ExplicitGameStrategyPair { + public: + ExplicitGameStrategyPair(uint64_t numberOfPlayer1States, uint64_t numberOfPlayer2States); + ExplicitGameStrategyPair(ExplicitGameStrategy&& player1Strategy, ExplicitGameStrategy&& player2Strategy); + + ExplicitGameStrategy& getPlayer1Strategy(); + ExplicitGameStrategy const& getPlayer1Strategy() const; + ExplicitGameStrategy& getPlayer2Strategy(); + ExplicitGameStrategy const& getPlayer2Strategy() const; + + private: + ExplicitGameStrategy player1Strategy; + ExplicitGameStrategy player2Strategy; + }; + + } +} diff --git a/src/storm/abstraction/ExplicitQualitativeGameResultMinMax.cpp b/src/storm/abstraction/ExplicitQualitativeGameResultMinMax.cpp index ef1538c50..7a5456bd5 100644 --- a/src/storm/abstraction/ExplicitQualitativeGameResultMinMax.cpp +++ b/src/storm/abstraction/ExplicitQualitativeGameResultMinMax.cpp @@ -19,6 +19,21 @@ namespace storm { } } + ExplicitQualitativeGameResult& ExplicitQualitativeGameResultMinMax::getProb0(storm::OptimizationDirection const& dir) { + if (dir == storm::OptimizationDirection::Minimize) { + return prob0Min; + } else { + return prob0Max; + } + } + + ExplicitQualitativeGameResult& ExplicitQualitativeGameResultMinMax::getProb1(storm::OptimizationDirection const& dir) { + if (dir == storm::OptimizationDirection::Minimize) { + return prob1Min; + } else { + return prob1Max; + } + } } } diff --git a/src/storm/abstraction/ExplicitQualitativeGameResultMinMax.h b/src/storm/abstraction/ExplicitQualitativeGameResultMinMax.h index 8551a3c47..5612ac9e7 100644 --- a/src/storm/abstraction/ExplicitQualitativeGameResultMinMax.h +++ b/src/storm/abstraction/ExplicitQualitativeGameResultMinMax.h @@ -12,7 +12,9 @@ namespace storm { virtual ExplicitQualitativeGameResult const& getProb0(storm::OptimizationDirection const& dir) const override; virtual ExplicitQualitativeGameResult const& getProb1(storm::OptimizationDirection const& dir) const override; - + virtual ExplicitQualitativeGameResult& getProb0(storm::OptimizationDirection const& dir) override; + virtual ExplicitQualitativeGameResult& getProb1(storm::OptimizationDirection const& dir) override; + ExplicitQualitativeGameResult prob0Min; ExplicitQualitativeGameResult prob1Min; ExplicitQualitativeGameResult prob0Max; diff --git a/src/storm/abstraction/ExplicitQualitativeResult.cpp b/src/storm/abstraction/ExplicitQualitativeResult.cpp new file mode 100644 index 000000000..b1237350e --- /dev/null +++ b/src/storm/abstraction/ExplicitQualitativeResult.cpp @@ -0,0 +1,17 @@ +#include "storm/abstraction/ExplicitQualitativeResult.h" + +#include "storm/abstraction/ExplicitQualitativeGameResult.h" + +namespace storm { + namespace abstraction { + + ExplicitQualitativeGameResult& ExplicitQualitativeResult::asExplicitQualitativeGameResult() { + return static_cast(*this); + } + + ExplicitQualitativeGameResult const& ExplicitQualitativeResult::asExplicitQualitativeGameResult() const { + return static_cast(*this); + } + + } +} diff --git a/src/storm/abstraction/ExplicitQualitativeResult.h b/src/storm/abstraction/ExplicitQualitativeResult.h index 8f8e6a151..d275fe91c 100644 --- a/src/storm/abstraction/ExplicitQualitativeResult.h +++ b/src/storm/abstraction/ExplicitQualitativeResult.h @@ -10,11 +10,16 @@ namespace storm { } namespace abstraction { + + class ExplicitQualitativeGameResult; class ExplicitQualitativeResult : public QualitativeResult { public: virtual ~ExplicitQualitativeResult() = default; + ExplicitQualitativeGameResult& asExplicitQualitativeGameResult(); + ExplicitQualitativeGameResult const& asExplicitQualitativeGameResult() const; + virtual storm::storage::BitVector const& getStates() const = 0; }; diff --git a/src/storm/abstraction/ExplicitQualitativeResultMinMax.cpp b/src/storm/abstraction/ExplicitQualitativeResultMinMax.cpp index 8d3a630f2..382a435f6 100644 --- a/src/storm/abstraction/ExplicitQualitativeResultMinMax.cpp +++ b/src/storm/abstraction/ExplicitQualitativeResultMinMax.cpp @@ -25,5 +25,21 @@ namespace storm { return getProb1(storm::OptimizationDirection::Maximize); } + ExplicitQualitativeResult& ExplicitQualitativeResultMinMax::getProb0Min() { + return getProb0(storm::OptimizationDirection::Minimize); + } + + ExplicitQualitativeResult& ExplicitQualitativeResultMinMax::getProb1Min() { + return getProb1(storm::OptimizationDirection::Minimize); + } + + ExplicitQualitativeResult& ExplicitQualitativeResultMinMax::getProb0Max() { + return getProb0(storm::OptimizationDirection::Maximize); + } + + ExplicitQualitativeResult& ExplicitQualitativeResultMinMax::getProb1Max() { + return getProb1(storm::OptimizationDirection::Maximize); + } + } } diff --git a/src/storm/abstraction/ExplicitQualitativeResultMinMax.h b/src/storm/abstraction/ExplicitQualitativeResultMinMax.h index 2eabe123b..acccab839 100644 --- a/src/storm/abstraction/ExplicitQualitativeResultMinMax.h +++ b/src/storm/abstraction/ExplicitQualitativeResultMinMax.h @@ -7,6 +7,7 @@ namespace storm { namespace abstraction { class ExplicitQualitativeResult; + class ExplicitQualitativeGameResultMinMax; class ExplicitQualitativeResultMinMax : public QualitativeResultMinMax { public: @@ -18,9 +19,15 @@ namespace storm { ExplicitQualitativeResult const& getProb1Min() const; ExplicitQualitativeResult const& getProb0Max() const; ExplicitQualitativeResult const& getProb1Max() const; - + ExplicitQualitativeResult& getProb0Min(); + ExplicitQualitativeResult& getProb1Min(); + ExplicitQualitativeResult& getProb0Max(); + ExplicitQualitativeResult& getProb1Max(); + virtual ExplicitQualitativeResult const& getProb0(storm::OptimizationDirection const& dir) const = 0; virtual ExplicitQualitativeResult const& getProb1(storm::OptimizationDirection const& dir) const = 0; + virtual ExplicitQualitativeResult& getProb0(storm::OptimizationDirection const& dir) = 0; + virtual ExplicitQualitativeResult& getProb1(storm::OptimizationDirection const& dir) = 0; }; } diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index d97973bd6..6b83338e7 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -4,8 +4,11 @@ #include "storm/abstraction/MenuGameAbstractor.h" #include "storm/storage/BitVector.h" +#include "storm/abstraction/ExplicitQualitativeGameResultMinMax.h" +#include "storm/abstraction/ExplicitGameStrategyPair.h" #include "storm/storage/dd/DdManager.h" +#include "storm/storage/dd/Odd.h" #include "storm/utility/dd.h" #include "storm/utility/solver.h" @@ -42,7 +45,7 @@ namespace storm { } template - MostProbablePathsResult::MostProbablePathsResult(storm::dd::Add const& maxProbabilities, storm::dd::Bdd const& spanningTree) : maxProbabilities(maxProbabilities), spanningTree(spanningTree) { + SymbolicMostProbablePathsResult::SymbolicMostProbablePathsResult(storm::dd::Add const& maxProbabilities, storm::dd::Bdd const& spanningTree) : maxProbabilities(maxProbabilities), spanningTree(spanningTree) { // Intentionally left empty. } @@ -54,7 +57,7 @@ namespace storm { }; template - PivotStateResult::PivotStateResult(storm::dd::Bdd const& pivotState, storm::OptimizationDirection fromDirection, boost::optional> const& mostProbablePathsResult) : pivotState(pivotState), fromDirection(fromDirection), mostProbablePathsResult(mostProbablePathsResult) { + SymbolicPivotStateResult::SymbolicPivotStateResult(storm::dd::Bdd const& pivotState, storm::OptimizationDirection fromDirection, boost::optional> const& symbolicMostProbablePathsResult) : pivotState(pivotState), fromDirection(fromDirection), symbolicMostProbablePathsResult(symbolicMostProbablePathsResult) { // Intentionally left empty. } @@ -89,7 +92,7 @@ namespace storm { } template - MostProbablePathsResult getMostProbablePathSpanningTree(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionFilter) { + SymbolicMostProbablePathsResult getMostProbablePathSpanningTree(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionFilter) { storm::dd::Add maxProbabilities = game.getInitialStates().template toAdd(); storm::dd::Bdd border = game.getInitialStates(); @@ -120,11 +123,11 @@ namespace storm { border = updateStates; } - return MostProbablePathsResult(maxProbabilities, spanningTree); + return SymbolicMostProbablePathsResult(maxProbabilities, spanningTree); } template - PivotStateResult pickPivotState(AbstractionSettings::PivotSelectionHeuristic const& heuristic, storm::abstraction::MenuGame const& game, PivotStateCandidatesResult const& pivotStateCandidateResult, boost::optional> const& qualitativeResult, boost::optional> const& quantitativeResult) { + SymbolicPivotStateResult pickPivotState(AbstractionSettings::PivotSelectionHeuristic const& heuristic, storm::abstraction::MenuGame const& game, PivotStateCandidatesResult const& pivotStateCandidateResult, boost::optional> const& qualitativeResult, boost::optional> const& quantitativeResult) { // Get easy access to strategies. storm::dd::Bdd minPlayer1Strategy; @@ -163,7 +166,7 @@ namespace storm { bool foundPivotState = !frontierPivotStates.isZero(); if (foundPivotState) { STORM_LOG_TRACE("Picked pivot state from " << frontierPivotStates.getNonZeroCount() << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total."); - return PivotStateResult(frontierPivotStates.existsAbstractRepresentative(rowVariables), storm::OptimizationDirection::Minimize); + return SymbolicPivotStateResult(frontierPivotStates.existsAbstractRepresentative(rowVariables), storm::OptimizationDirection::Minimize); } else { // Otherwise, we perform a simulatenous BFS in the sense that we make one step in both the min and max // transitions and check for pivot states we encounter. @@ -195,7 +198,7 @@ namespace storm { } STORM_LOG_TRACE("Picked pivot state with difference " << diffValue << " from " << numberOfPivotStateCandidatesOnLevel << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total."); - return PivotStateResult(direction == storm::OptimizationDirection::Minimize ? diffMin.maxAbstractRepresentative(rowVariables) : diffMax.maxAbstractRepresentative(rowVariables), direction); + return SymbolicPivotStateResult(direction == storm::OptimizationDirection::Minimize ? diffMin.maxAbstractRepresentative(rowVariables) : diffMax.maxAbstractRepresentative(rowVariables), direction); } else { STORM_LOG_TRACE("Picked pivot state from " << numberOfPivotStateCandidatesOnLevel << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total."); @@ -206,18 +209,18 @@ namespace storm { direction = storm::OptimizationDirection::Maximize; } - return PivotStateResult(direction == storm::OptimizationDirection::Minimize ? frontierMinPivotStates.existsAbstractRepresentative(rowVariables) : frontierMaxPivotStates.existsAbstractRepresentative(rowVariables), direction); + return SymbolicPivotStateResult(direction == storm::OptimizationDirection::Minimize ? frontierMinPivotStates.existsAbstractRepresentative(rowVariables) : frontierMaxPivotStates.existsAbstractRepresentative(rowVariables), direction); } } } } } else { // Compute the most probable paths to the reachable states and the corresponding spanning trees. - MostProbablePathsResult minMostProbablePathsResult = getMostProbablePathSpanningTree(game, minPlayer1Strategy && minPlayer2Strategy); - MostProbablePathsResult maxMostProbablePathsResult = getMostProbablePathSpanningTree(game, maxPlayer1Strategy && maxPlayer2Strategy); + SymbolicMostProbablePathsResult minSymbolicMostProbablePathsResult = getMostProbablePathSpanningTree(game, minPlayer1Strategy && minPlayer2Strategy); + SymbolicMostProbablePathsResult maxSymbolicMostProbablePathsResult = getMostProbablePathSpanningTree(game, maxPlayer1Strategy && maxPlayer2Strategy); storm::dd::Bdd selectedPivotState; - storm::dd::Add score = pivotStates.template toAdd() * minMostProbablePathsResult.maxProbabilities.maximum(maxMostProbablePathsResult.maxProbabilities); + storm::dd::Add score = pivotStates.template toAdd() * minSymbolicMostProbablePathsResult.maxProbabilities.maximum(maxSymbolicMostProbablePathsResult.maxProbabilities); if (heuristic == AbstractionSettings::PivotSelectionHeuristic::MaxWeightedDeviation && quantitativeResult) { score = score * (quantitativeResult.get().max.values - quantitativeResult.get().min.values); @@ -227,15 +230,15 @@ namespace storm { storm::OptimizationDirection fromDirection = storm::OptimizationDirection::Minimize; storm::dd::Add selectedPivotStateAsAdd = selectedPivotState.template toAdd(); - if ((selectedPivotStateAsAdd * maxMostProbablePathsResult.maxProbabilities).getMax() > (selectedPivotStateAsAdd * minMostProbablePathsResult.maxProbabilities).getMax()) { + if ((selectedPivotStateAsAdd * maxSymbolicMostProbablePathsResult.maxProbabilities).getMax() > (selectedPivotStateAsAdd * minSymbolicMostProbablePathsResult.maxProbabilities).getMax()) { fromDirection = storm::OptimizationDirection::Maximize; } - return PivotStateResult(selectedPivotState, fromDirection, fromDirection == storm::OptimizationDirection::Minimize ? minMostProbablePathsResult : maxMostProbablePathsResult); + return SymbolicPivotStateResult(selectedPivotState, fromDirection, fromDirection == storm::OptimizationDirection::Minimize ? minSymbolicMostProbablePathsResult : maxSymbolicMostProbablePathsResult); } STORM_LOG_ASSERT(false, "This point must not be reached, because then no pivot state could be found."); - return PivotStateResult(storm::dd::Bdd(), storm::OptimizationDirection::Minimize); + return SymbolicPivotStateResult(storm::dd::Bdd(), storm::OptimizationDirection::Minimize); } template @@ -522,23 +525,23 @@ namespace storm { } template - boost::optional MenuGameRefiner::derivePredicatesFromInterpolation(storm::abstraction::MenuGame const& game, PivotStateResult const& pivotStateResult, storm::dd::Bdd const& minPlayer1Strategy, storm::dd::Bdd const& minPlayer2Strategy, storm::dd::Bdd const& maxPlayer1Strategy, storm::dd::Bdd const& maxPlayer2Strategy) const { + 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. - MostProbablePathsResult mostProbablePathsResult; - if (!pivotStateResult.mostProbablePathsResult) { - mostProbablePathsResult = getMostProbablePathSpanningTree(game, pivotStateResult.fromDirection == storm::OptimizationDirection::Minimize ? minPlayer1Strategy && minPlayer2Strategy : maxPlayer1Strategy && maxPlayer2Strategy); + SymbolicMostProbablePathsResult symbolicMostProbablePathsResult; + if (!symbolicPivotStateResult.symbolicMostProbablePathsResult) { + symbolicMostProbablePathsResult = getMostProbablePathSpanningTree(game, symbolicPivotStateResult.fromDirection == storm::OptimizationDirection::Minimize ? minPlayer1Strategy && minPlayer2Strategy : maxPlayer1Strategy && maxPlayer2Strategy); } else { - mostProbablePathsResult = pivotStateResult.mostProbablePathsResult.get(); + 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, mostProbablePathsResult.spanningTree, pivotStateResult.pivotState); + std::pair>, std::map> traceAndVariableSubstitution = buildTrace(*interpolationManager, game, symbolicMostProbablePathsResult.spanningTree, symbolicPivotStateResult.pivotState); auto const& trace = traceAndVariableSubstitution.first; auto const& variableSubstitution = traceAndVariableSubstitution.second; @@ -615,11 +618,11 @@ namespace storm { STORM_LOG_ASSERT(!pivotStateCandidatesResult.pivotStates.isZero(), "Unable to proceed without pivot state candidates."); // Now that we have the pivot state candidates, we need to pick one. - PivotStateResult pivotStateResult = pickPivotState(pivotSelectionHeuristic, game, pivotStateCandidatesResult, qualitativeResult, boost::none); + SymbolicPivotStateResult SymbolicPivotStateResult = pickPivotState(pivotSelectionHeuristic, game, pivotStateCandidatesResult, qualitativeResult, boost::none); // // SANITY CHECK TO MAKE SURE OUR STRATEGIES ARE NOT BROKEN. // // FIXME. -// auto min1ChoiceInPivot = pivotStateResult.pivotState && game.getExtendedTransitionMatrix().toBdd() && minPlayer1Strategy; +// auto min1ChoiceInPivot = SymbolicPivotStateResult.pivotState && game.getExtendedTransitionMatrix().toBdd() && minPlayer1Strategy; // STORM_LOG_ASSERT(!min1ChoiceInPivot.isZero(), "wth?"); // bool min1ChoiceInPivotIsProb0Min = !(min1ChoiceInPivot && qualitativeResult.prob0Min.getPlayer2States()).isZero(); // bool min1ChoiceInPivotIsProb0Max = !(min1ChoiceInPivot && qualitativeResult.prob0Max.getPlayer2States()).isZero(); @@ -643,7 +646,7 @@ namespace storm { // std::cout << "max/min choice there? " << min1MinPlayer2Choice << std::endl; // std::cout << "max/max choice there? " << min1MaxPlayer2Choice << std::endl; // -// auto max1ChoiceInPivot = pivotStateResult.pivotState && game.getExtendedTransitionMatrix().toBdd() && maxPlayer1Strategy; +// auto max1ChoiceInPivot = SymbolicPivotStateResult.pivotState && game.getExtendedTransitionMatrix().toBdd() && maxPlayer1Strategy; // STORM_LOG_ASSERT(!max1ChoiceInPivot.isZero(), "wth?"); // bool max1ChoiceInPivotIsProb0Min = !(max1ChoiceInPivot && qualitativeResult.prob0Min.getPlayer2States()).isZero(); // bool max1ChoiceInPivotIsProb0Max = !(max1ChoiceInPivot && qualitativeResult.prob0Max.getPlayer2States()).isZero(); @@ -661,12 +664,12 @@ namespace storm { boost::optional predicates; if (useInterpolation) { - predicates = derivePredicatesFromInterpolation(game, pivotStateResult, 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, pivotStateResult.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."); @@ -676,6 +679,130 @@ namespace storm { return true; } + 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) { + + // 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(); + + 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)); + + // 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; + } + + distances[initialState] = zeroDistance; + dijkstraQueue.emplace(zeroDistance, initialState); + } + + while (!dijkstraQueue.empty()) { + uint64_t currentState = (*dijkstraQueue.begin()).second; + dijkstraQueue.erase(dijkstraQueue.begin()); + + // 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)) { + isPivotState = true; + } + } else if (maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(currentState)) { + uint64_t player2Successor = maxStrategyPair.getPlayer1Strategy().getChoice(currentState); + if (minStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2Successor) && maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2Successor)) { + isPivotState = true; + } + } + + // If it is indeed a pivot state, we can abort the search here. + if (isPivotState) { + explicitPivotStateResult.pivotState = currentState; + return explicitPivotStateResult; + } + + // Otherwise, we explore all its relevant successors. + if (minStrategyPair.getPlayer1Strategy().hasDefinedChoice(currentState)) { + uint64_t minPlayer2Successor = minStrategyPair.getPlayer1Strategy().getChoice(currentState); + uint64_t minPlayer2Choice = minStrategyPair.getPlayer2Strategy().getChoice(minPlayer2Successor); + + for (auto const& entry : transitionMatrix.getRow(minPlayer2Choice)) { + uint64_t player1Successor = entry.getColumn(); + if (!relevantStates.get(player1Successor)) { + continue; + } + + ValueType alternateDistance = probabilityDistances ? distances[currentState] * entry.getValue() : distances[currentState] + storm::utility::one(); + if ((probabilityDistances && alternateDistance > distances[player1Successor]) || (!probabilityDistances && alternateDistance < distances[player1Successor])) { + distances[player1Successor] = alternateDistance; + explicitMostProbablePathsResult.predecessors[player1Successor] = std::make_pair(currentState, minPlayer2Successor); + dijkstraQueue.emplace(alternateDistance, player1Successor); + } + } + } + if (maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(currentState)) { + uint64_t maxPlayer2Successor = maxStrategyPair.getPlayer1Strategy().getChoice(currentState); + uint64_t maxPlayer2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(maxPlayer2Successor); + + for (auto const& entry : transitionMatrix.getRow(maxPlayer2Choice)) { + uint64_t player1Successor = entry.getColumn(); + if (!relevantStates.get(player1Successor)) { + continue; + } + + ValueType alternateDistance = probabilityDistances ? distances[currentState] * entry.getValue() : distances[currentState] + storm::utility::one(); + if ((probabilityDistances && alternateDistance > distances[player1Successor]) || (!probabilityDistances && alternateDistance < distances[player1Successor])) { + distances[player1Successor] = alternateDistance; + explicitMostProbablePathsResult.predecessors[player1Successor] = std::make_pair(currentState, maxPlayer2Successor); + dijkstraQueue.emplace(alternateDistance, player1Successor); + } + } + } + } + + // 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; + } + + 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 { + + // 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); + + // If there was no pivot state, continue the search. + if (!pivotStateResult.pivotState) { + return false; + } + + // Otherwise, we can refine. + storm::dd::Bdd pivotState = storm::dd::Bdd::getEncoding(game.getManager(), pivotStateResult.pivotState.get(), odd, game.getRowVariables()); + } + template bool MenuGameRefiner::refine(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, SymbolicQuantitativeGameResultMinMax const& quantitativeResult) const { STORM_LOG_TRACE("Refining after quantitative check."); @@ -691,16 +818,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. - PivotStateResult pivotStateResult = pickPivotState(pivotSelectionHeuristic, game, pivotStateCandidatesResult, boost::none, quantitativeResult); + SymbolicPivotStateResult SymbolicPivotStateResult = pickPivotState(pivotSelectionHeuristic, game, pivotStateCandidatesResult, boost::none, quantitativeResult); boost::optional predicates; if (useInterpolation) { - predicates = derivePredicatesFromInterpolation(game, pivotStateResult, 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, pivotStateResult.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 ed3589ac6..7a912e947 100644 --- a/src/storm/abstraction/MenuGameRefiner.h +++ b/src/storm/abstraction/MenuGameRefiner.h @@ -21,6 +21,14 @@ #include "storm/utility/solver.h" namespace storm { + namespace dd { + class Odd; + } + + namespace storage { + class BitVector; + } + namespace abstraction { template @@ -48,23 +56,48 @@ namespace storm { }; template - struct MostProbablePathsResult { - MostProbablePathsResult() = default; - MostProbablePathsResult(storm::dd::Add const& maxProbabilities, storm::dd::Bdd const& spanningTree); + struct SymbolicMostProbablePathsResult { + SymbolicMostProbablePathsResult() = default; + SymbolicMostProbablePathsResult(storm::dd::Add const& maxProbabilities, storm::dd::Bdd const& spanningTree); storm::dd::Add maxProbabilities; storm::dd::Bdd spanningTree; }; template - struct PivotStateResult { - PivotStateResult(storm::dd::Bdd const& pivotState, storm::OptimizationDirection fromDirection, boost::optional> const& mostProbablePathsResult = boost::none); + struct SymbolicPivotStateResult { + SymbolicPivotStateResult(storm::dd::Bdd const& pivotState, storm::OptimizationDirection fromDirection, boost::optional> const& symbolicMostProbablePathsResult = boost::none); storm::dd::Bdd pivotState; storm::OptimizationDirection fromDirection; - boost::optional> mostProbablePathsResult; + 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; }; + class ExplicitQualitativeGameResultMinMax; + class ExplicitGameStrategyPair; + template class MenuGameRefiner { public: @@ -86,7 +119,14 @@ namespace storm { * @param True if predicates for refinement could be derived, false otherwise. */ bool refine(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, SymbolicQualitativeGameResultMinMax const& qualitativeResult) 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, ExplicitQualitativeGameResultMinMax const& qualitativeResult, ExplicitGameStrategyPair const& minStrategyPair, ExplicitGameStrategyPair const& maxStrategyPair) const; + /*! * Refines the abstractor based on the quantitative result by trying to derive suitable predicates. * @@ -113,7 +153,7 @@ namespace storm { */ std::vector createGlobalRefinement(std::vector const& predicates) const; - boost::optional derivePredicatesFromInterpolation(storm::abstraction::MenuGame const& game, PivotStateResult const& pivotStateResult, storm::dd::Bdd const& minPlayer1Strategy, storm::dd::Bdd const& minPlayer2Strategy, storm::dd::Bdd const& maxPlayer1Strategy, storm::dd::Bdd const& maxPlayer2Strategy) const; + 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; void performRefinement(std::vector const& refinementCommands) const; diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp index 09782e9fd..215aeb780 100644 --- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp +++ b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp @@ -61,10 +61,10 @@ namespace storm { totalNumberOfCommands += automaton.getNumberOfEdges(); } - // NOTE: currently we assume that 100 player 2 variables suffice, which corresponds to 2^100 possible + // NOTE: currently we assume that 64 player 2 variables suffice, which corresponds to 2^64 possible // choices. If for some reason this should not be enough, we could grow this vector dynamically, but // odds are that it's impossible to treat such models in any event. - abstractionInformation.createEncodingVariables(static_cast(std::ceil(std::log2(totalNumberOfCommands))), 100, static_cast(std::ceil(std::log2(maximalUpdateCount)))); + abstractionInformation.createEncodingVariables(static_cast(std::ceil(std::log2(totalNumberOfCommands))), 64, static_cast(std::ceil(std::log2(maximalUpdateCount)))); // For each module of the concrete program, we create an abstract counterpart. bool useDecomposition = storm::settings::getModule().isUseDecompositionSet(); diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp index 9da47fee3..99dc2c5a2 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp @@ -58,10 +58,10 @@ namespace storm { totalNumberOfCommands += module.getNumberOfCommands(); } - // NOTE: currently we assume that 100 player 2 variables suffice, which corresponds to 2^100 possible + // NOTE: currently we assume that 64 player 2 variables suffice, which corresponds to 2^64 possible // choices. If for some reason this should not be enough, we could grow this vector dynamically, but // odds are that it's impossible to treat such models in any event. - abstractionInformation.createEncodingVariables(static_cast(std::ceil(std::log2(totalNumberOfCommands))), 100, static_cast(std::ceil(std::log2(maximalUpdateCount)))); + abstractionInformation.createEncodingVariables(static_cast(std::ceil(std::log2(totalNumberOfCommands))), 64, static_cast(std::ceil(std::log2(maximalUpdateCount)))); // For each module of the concrete program, we create an abstract counterpart. bool useDecomposition = storm::settings::getModule().isUseDecompositionSet(); diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 9119c498f..2b2980e95 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -24,6 +24,7 @@ #include "storm/abstraction/prism/PrismMenuGameAbstractor.h" #include "storm/abstraction/jani/JaniMenuGameAbstractor.h" #include "storm/abstraction/MenuGameRefiner.h" +#include "storm/abstraction/ExplicitGameStrategyPair.h" #include "storm/abstraction/ExplicitQualitativeGameResultMinMax.h" @@ -174,6 +175,53 @@ namespace storm { } return result; } + + template + std::unique_ptr checkForResultAfterQualitativeCheck(CheckTask const& checkTask, storm::OptimizationDirection player2Direction, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& prob0, storm::storage::BitVector const& prob1) { + std::unique_ptr result; + + if (checkTask.isBoundSet()) { + // Despite having a bound, we create a quantitative result so that the next layer can perform the comparison. + + if (player2Direction == storm::OptimizationDirection::Minimize) { + if (storm::logic::isLowerBound(checkTask.getBoundComparisonType())) { + if (initialStates.isSubsetOf(prob1)) { + result = std::make_unique>(storm::storage::sparse::state_type(0), storm::utility::one()); + } + } else { + if (!initialStates.isDisjointFrom(prob1)) { + result = std::make_unique>(storm::storage::sparse::state_type(0), storm::utility::one()); + } + } + } else if (player2Direction == storm::OptimizationDirection::Maximize) { + if (!storm::logic::isLowerBound(checkTask.getBoundComparisonType())) { + if (initialStates.isSubsetOf(prob0)) { + result = std::make_unique>(storm::storage::sparse::state_type(0), storm::utility::zero()); + } + } else { + if (!initialStates.isDisjointFrom(prob0)) { + result = std::make_unique>(storm::storage::sparse::state_type(0), storm::utility::zero()); + } + } + } + } + + return result; + } + + template + std::unique_ptr checkForResultAfterQualitativeCheck(CheckTask const& checkTask, storm::storage::BitVector const& initialStates, ExplicitQualitativeGameResultMinMax const& qualitativeResult) { + // Check whether we can already give the answer based on the current information. + std::unique_ptr result = checkForResultAfterQualitativeCheck(checkTask, storm::OptimizationDirection::Minimize, initialStates, qualitativeResult.prob0Min.getPlayer1States(), qualitativeResult.prob1Min.getPlayer1States()); + if (result) { + return result; + } + result = checkForResultAfterQualitativeCheck(checkTask, storm::OptimizationDirection::Maximize, initialStates, qualitativeResult.prob0Max.getPlayer1States(), qualitativeResult.prob1Max.getPlayer1States()); + if (result) { + return result; + } + return result; + } template std::unique_ptr checkForResultAfterQuantitativeCheck(CheckTask const& checkTask, storm::OptimizationDirection const& player2Direction, std::pair const& initialValueRange) { @@ -506,7 +554,7 @@ namespace storm { // Return null to indicate no result has been found yet. return nullptr; } - + template std::unique_ptr GameBasedMdpModelChecker::performExplicitAbstractionSolutionStep(Environment const& env, CheckTask const& checkTask, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& initialStatesBdd, storm::dd::Bdd const& constraintStatesBdd, storm::dd::Bdd const& targetStatesBdd, storm::abstraction::MenuGameRefiner const& refiner, boost::optional& previousQualitativeResult) { STORM_LOG_TRACE("Using sparse solving."); @@ -514,22 +562,24 @@ namespace storm { // (0) Start by transforming the necessary symbolic elements to explicit ones. storm::dd::Odd odd = game.getReachableStates().createOdd(); - std::pair, std::vector> transitionMatrixAndLabeling = game.getTransitionMatrix().toLabeledMatrix(game.getRowVariables(), game.getColumnVariables(), game.getNondeterminismVariables(), game.getPlayer1Variables(), odd, odd, true); - auto& transitionMatrix = transitionMatrixAndLabeling.first; - auto& labeling = transitionMatrixAndLabeling.second; - + std::vector> labelingVariableSets = {game.getPlayer1Variables(), game.getPlayer2Variables()}; + typename storm::dd::Add::MatrixAndLabeling matrixAndLabeling = game.getTransitionMatrix().toLabeledMatrix(game.getRowVariables(), game.getColumnVariables(), game.getNondeterminismVariables(), odd, odd, labelingVariableSets); + auto& transitionMatrix = matrixAndLabeling.matrix; + auto& player1Labeling = matrixAndLabeling.labelings.front(); + auto& player2Labeling = matrixAndLabeling.labelings.back(); + // Create the player 2 row grouping from the labeling. std::vector tmpPlayer2RowGrouping; for (uint64_t player1State = 0; player1State < transitionMatrix.getRowGroupCount(); ++player1State) { uint64_t lastLabel = std::numeric_limits::max(); for (uint64_t row = transitionMatrix.getRowGroupIndices()[player1State]; row < transitionMatrix.getRowGroupIndices()[player1State + 1]; ++row) { - if (labeling[row] != lastLabel) { + if (player1Labeling[row] != lastLabel) { tmpPlayer2RowGrouping.emplace_back(row); - lastLabel = labeling[row]; + lastLabel = player1Labeling[row]; } } } - tmpPlayer2RowGrouping.emplace_back(labeling.size()); + tmpPlayer2RowGrouping.emplace_back(player1Labeling.size()); std::vector player1RowGrouping = transitionMatrix.swapRowGroupIndices(std::move(tmpPlayer2RowGrouping)); auto const& player2RowGrouping = transitionMatrix.getRowGroupIndices(); @@ -548,17 +598,22 @@ namespace storm { player1Groups[player1State + 1] = player2State; } + // Create explicit representations of important state sets. storm::storage::BitVector initialStates = initialStatesBdd.toVector(odd); storm::storage::BitVector constraintStates = constraintStatesBdd.toVector(odd); storm::storage::BitVector targetStates = targetStatesBdd.toVector(odd); + // Prepare the two strategies. + abstraction::ExplicitGameStrategyPair minStrategyPair(initialStates.size(), transitionMatrix.getRowGroupCount()); + abstraction::ExplicitGameStrategyPair maxStrategyPair(initialStates.size(), transitionMatrix.getRowGroupCount()); + // (1) compute all states with probability 0/1 wrt. to the two different player 2 goals (min/max). auto qualitativeStart = std::chrono::high_resolution_clock::now(); - ExplicitQualitativeGameResultMinMax qualitativeResult = computeProb01States(previousQualitativeResult, player1Direction, transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates); -// std::unique_ptr result = checkForResultAfterQualitativeCheck(checkTask, initialStates, qualitativeResult); -// if (result) { -// return result; -// } + ExplicitQualitativeGameResultMinMax qualitativeResult = computeProb01States(previousQualitativeResult, player1Direction, transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, minStrategyPair, maxStrategyPair); + std::unique_ptr result = checkForResultAfterQualitativeCheck(checkTask, initialStates, qualitativeResult); + if (result) { + return result; + } auto qualitativeEnd = std::chrono::high_resolution_clock::now(); STORM_LOG_DEBUG("Qualitative computation completed in " << std::chrono::duration_cast(qualitativeEnd - qualitativeStart).count() << "ms."); @@ -568,6 +623,31 @@ namespace storm { // 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()); + storm::storage::BitVector maybeMax = ~(qualitativeResult.getProb0Max().getStates() | qualitativeResult.getProb1Max().getStates()); + + // (3) if the initial states are not maybe states, then we can refine at this point. + storm::storage::BitVector initialMaybeStates = initialStates & (maybeMin | maybeMax); + bool qualitativeRefinement = false; + if (initialMaybeStates.empty()) { + // In this case, we know the result for the initial states for both player 2 minimizing and maximizing. + STORM_LOG_TRACE("No initial state is a 'maybe' state."); + + STORM_LOG_DEBUG("Obtained qualitative bounds [0, 1] on the actual value for the initial states. Refining abstraction based on qualitative check."); + + // If we get here, the initial states were all identified as prob0/1 states, but the value (0 or 1) + // depends on whether player 2 is minimizing or maximizing. Therefore, we need to find a place to refine. + auto qualitativeRefinementStart = std::chrono::high_resolution_clock::now(); + qualitativeRefinement = refiner.refine(game, odd, transitionMatrix, player1Groups, player1Labeling, player2Labeling, initialStates, constraintStates, targetStates, qualitativeResult, minStrategyPair, maxStrategyPair); + auto qualitativeRefinementEnd = std::chrono::high_resolution_clock::now(); + STORM_LOG_DEBUG("Qualitative refinement completed in " << std::chrono::duration_cast(qualitativeRefinementEnd - qualitativeRefinementStart).count() << "ms."); + } else if (initialStates.isSubsetOf(initialMaybeStates) && checkTask.isQualitativeSet()) { + // If all initial states are 'maybe' states and the property we needed to check is a qualitative one, + // we can return the result here. + return std::make_unique>(storm::storage::sparse::state_type(0), ValueType(0.5)); + } + return nullptr; } @@ -630,7 +710,7 @@ namespace storm { } template - ExplicitQualitativeGameResultMinMax GameBasedMdpModelChecker::computeProb01States(boost::optional const& previousQualitativeResult, storm::OptimizationDirection player1Direction, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Groups, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates) { + ExplicitQualitativeGameResultMinMax GameBasedMdpModelChecker::computeProb01States(boost::optional const& previousQualitativeResult, storm::OptimizationDirection player1Direction, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Groups, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, abstraction::ExplicitGameStrategyPair& minStrategyPair, abstraction::ExplicitGameStrategyPair& maxStrategyPair) { ExplicitQualitativeGameResultMinMax result; @@ -679,10 +759,10 @@ namespace storm { // result.prob1Min = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true, boost::make_optional(prob1MaxMaxMdp)); // } // } else { - result.prob0Min = storm::utility::graph::performProb0(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true); - result.prob1Min = storm::utility::graph::performProb1(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true); - result.prob0Max = storm::utility::graph::performProb0(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true); - result.prob1Max = storm::utility::graph::performProb1(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true); + result.prob0Min = storm::utility::graph::performProb0(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, &minStrategyPair.getPlayer1Strategy(), &minStrategyPair.getPlayer2Strategy()); + result.prob1Min = storm::utility::graph::performProb1(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, &minStrategyPair.getPlayer1Strategy(), &minStrategyPair.getPlayer2Strategy()); + result.prob0Max = storm::utility::graph::performProb0(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, &maxStrategyPair.getPlayer1Strategy(), &maxStrategyPair.getPlayer2Strategy()); + result.prob1Max = storm::utility::graph::performProb1(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, &maxStrategyPair.getPlayer1Strategy(), &maxStrategyPair.getPlayer2Strategy()); // } STORM_LOG_TRACE("Qualitative precomputation completed."); diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h index 933e0bf5d..a2f4e53f0 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h @@ -39,6 +39,8 @@ namespace storm { class ExplicitQualitativeGameResult; class ExplicitQualitativeGameResultMinMax; + class ExplicitGameStrategy; + class ExplicitGameStrategyPair; } namespace modelchecker { @@ -92,7 +94,7 @@ namespace storm { */ SymbolicQualitativeGameResultMinMax computeProb01States(boost::optional> const& previousQualitativeResult, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& transitionMatrixBdd, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates); - ExplicitQualitativeGameResultMinMax computeProb01States(boost::optional const& previousQualitativeResult, storm::OptimizationDirection player1Direction, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1RowGrouping, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates); + ExplicitQualitativeGameResultMinMax computeProb01States(boost::optional const& previousQualitativeResult, storm::OptimizationDirection player1Direction, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1RowGrouping, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, abstraction::ExplicitGameStrategyPair& minStrategyPair, abstraction::ExplicitGameStrategyPair& maxStrategyPair); void printStatistics(storm::abstraction::MenuGameAbstractor const& abstractor, storm::abstraction::MenuGame const& game) const; diff --git a/src/storm/storage/dd/Add.cpp b/src/storm/storage/dd/Add.cpp index 75552108e..7f1cb1517 100644 --- a/src/storm/storage/dd/Add.cpp +++ b/src/storm/storage/dd/Add.cpp @@ -704,16 +704,18 @@ namespace storm { } // Create the canonical row group sizes and build the matrix. - return toLabeledMatrix(rowMetaVariables, columnMetaVariables, groupMetaVariables, groupMetaVariables, rowOdd, columnOdd).first; + return toLabeledMatrix(rowMetaVariables, columnMetaVariables, groupMetaVariables, rowOdd, columnOdd).matrix; } template - std::pair, std::vector> Add::toLabeledMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, std::set const& labelMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd, bool buildLabeling) const { + typename Add::MatrixAndLabeling Add::toLabeledMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd, std::vector> const& labelMetaVariables) const { std::vector ddRowVariableIndices; std::vector ddColumnVariableIndices; std::vector ddGroupVariableIndices; - storm::storage::BitVector ddLabelVariableIndices; + std::vector ddLabelVariableIndicesVector; std::set rowAndColumnMetaVariables; + bool buildLabeling = !labelMetaVariables.empty(); + MatrixAndLabeling result; for (auto const& variable : rowMetaVariables) { DdMetaVariable const& metaVariable = this->getDdManager().getMetaVariable(variable); @@ -739,21 +741,23 @@ namespace storm { } std::sort(ddGroupVariableIndices.begin(), ddGroupVariableIndices.end()); if (buildLabeling) { - std::set ddLabelVariableIndicesSet; - for (auto const& variable : labelMetaVariables) { - DdMetaVariable const& metaVariable = this->getDdManager().getMetaVariable(variable); - for (auto const& ddVariable : metaVariable.getDdVariables()) { - ddLabelVariableIndicesSet.insert(ddVariable.getIndex()); + for (auto const& labelMetaVariableSet : labelMetaVariables) { + std::set ddLabelVariableIndicesSet; + for (auto const& variable : labelMetaVariableSet) { + DdMetaVariable const& metaVariable = this->getDdManager().getMetaVariable(variable); + for (auto const& ddVariable : metaVariable.getDdVariables()) { + ddLabelVariableIndicesSet.insert(ddVariable.getIndex()); + } } - } - - ddLabelVariableIndices = storm::storage::BitVector(ddGroupVariableIndices.size()); - uint64_t position = 0; - for (auto const& index : ddGroupVariableIndices) { - if (ddLabelVariableIndicesSet.find(index) != ddLabelVariableIndicesSet.end()) { - ddLabelVariableIndices.set(position); + + ddLabelVariableIndicesVector.emplace_back(ddGroupVariableIndices.size()); + uint64_t position = 0; + for (auto const& index : ddGroupVariableIndices) { + if (ddLabelVariableIndicesSet.find(index) != ddLabelVariableIndicesSet.end()) { + ddLabelVariableIndicesVector.back().set(position); + } + ++position; } - ++position; } } @@ -781,10 +785,12 @@ namespace storm { } // Create the group labelings if requested. - std::vector groupLabels; + std::vector> groupLabelings; if (buildLabeling) { - groupLabels = internalAdd.decodeGroupLabels(ddGroupVariableIndices, ddLabelVariableIndices); - STORM_LOG_ASSERT(groupLabels.size() == groups.size(), "Mismatching label sizes."); + for (auto const& ddLabelVariableIndices : ddLabelVariableIndicesVector) { + groupLabelings.emplace_back(internalAdd.decodeGroupLabels(ddGroupVariableIndices, ddLabelVariableIndices)); + STORM_LOG_ASSERT(groupLabelings.back().size() == groups.size(), "Mismatching label sizes."); + } } // Create the actual storage for the non-zero entries. @@ -793,9 +799,10 @@ namespace storm { // Now compute the indices at which the individual rows start. std::vector rowIndications(rowGroupIndices.back() + 1); - std::vector labeling; if (buildLabeling) { - labeling.resize(rowGroupIndices.back()); + for (uint64_t i = 0; i < labelMetaVariables.size(); ++i) { + result.labelings.emplace_back(rowGroupIndices.back()); + } } std::vector> statesWithGroupEnabled(groups.size()); @@ -811,8 +818,10 @@ namespace storm { statesWithGroupEnabled[i] = groupNotZero.existsAbstract(columnMetaVariables).template toAdd(); if (buildLabeling) { - uint64_t currentLabel = groupLabels[i]; - statesWithGroupEnabled[i].forEach(rowOdd, ddRowVariableIndices, [currentLabel, &rowGroupIndices, &labeling] (uint64_t const& offset, uint_fast64_t const& value) { labeling[rowGroupIndices[offset]] = currentLabel; }); + for (uint64_t j = 0; j < labelMetaVariables.size(); ++j) { + uint64_t currentLabel = groupLabelings[j][i]; + statesWithGroupEnabled[i].forEach(rowOdd, ddRowVariableIndices, [currentLabel, &rowGroupIndices, &result, j] (uint64_t const& offset, uint_fast64_t const& value) { result.labelings[j][rowGroupIndices[offset]] = currentLabel; }); + } } statesWithGroupEnabled[i].composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, std::plus()); } @@ -847,8 +856,10 @@ namespace storm { rowIndications[i] = rowIndications[i - 1]; } rowIndications[0] = 0; - - return std::make_pair(storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices)), labeling); + + // Move-construct matrix and return. + result.matrix = storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices)); + return result; } template diff --git a/src/storm/storage/dd/Add.h b/src/storm/storage/dd/Add.h index ba6b5644d..94a512482 100644 --- a/src/storm/storage/dd/Add.h +++ b/src/storm/storage/dd/Add.h @@ -655,7 +655,22 @@ namespace storm { * @return The matrix that is represented by this ADD and a vector corresponding to row labeling * (if requested). */ - std::pair, std::vector> toLabeledMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, std::set const& labelMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd, bool buildLabeling = false) const; + struct MatrixAndLabeling { + MatrixAndLabeling() = default; + + MatrixAndLabeling(storm::storage::SparseMatrix const& matrix) : matrix(matrix) { + // Intentionally left empty. + } + + MatrixAndLabeling(storm::storage::SparseMatrix&& matrix) : matrix(std::move(matrix)) { + // Intentionally left empty. + } + + storm::storage::SparseMatrix matrix; + std::vector> labelings; + }; + + MatrixAndLabeling toLabeledMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd, std::vector> const& labelMetaVariables = std::vector>()) const; /*! * Converts the ADD to a row-grouped (sparse) matrix and the given vector to a row-grouped vector. diff --git a/src/storm/storage/dd/Bdd.cpp b/src/storm/storage/dd/Bdd.cpp index c2452ed3b..5271a628a 100644 --- a/src/storm/storage/dd/Bdd.cpp +++ b/src/storm/storage/dd/Bdd.cpp @@ -63,6 +63,11 @@ namespace storm { return Bdd(ddManager, InternalBdd::fromVector(&ddManager.getInternalDdManager(), odd, ddManager.getSortedVariableIndices(metaVariables), [&truthValues] (uint64_t offset) { return truthValues[offset]; } ), metaVariables); } + template + Bdd Bdd::getEncoding(DdManager const& ddManager, uint64_t targetOffset, storm::dd::Odd const& odd, std::set const& metaVariables) { + return Bdd(ddManager, InternalBdd::fromVector(&ddManager.getInternalDdManager(), odd, ddManager.getSortedVariableIndices(metaVariables), [targetOffset] (uint64_t offset) { return offset == targetOffset; }), metaVariables); + } + template bool Bdd::operator==(Bdd const& other) const { return internalBdd == other.internalBdd; diff --git a/src/storm/storage/dd/Bdd.h b/src/storm/storage/dd/Bdd.h index bfb845c70..9e36ba52b 100644 --- a/src/storm/storage/dd/Bdd.h +++ b/src/storm/storage/dd/Bdd.h @@ -45,6 +45,16 @@ namespace storm { Bdd(Bdd&& other) = default; Bdd& operator=(Bdd&& other) = default; + /*! + * Constructs the BDD representation of the encoding with the given offset. + * + * @param ddManager The DD manager responsible for the resulting BDD. + * @param targetOffset The offset to encode (interpreted within the ODD). + * @param odd The ODD used for the translation from the explicit representation to a symbolic one. + * @param metaVariables The meta variables to use for the symbolic encoding. + */ + static Bdd getEncoding(DdManager const& ddManager, uint64_t targetOffset, storm::dd::Odd const& odd, std::set const& metaVariables); + /*! * Constructs a BDD representation of all encodings whose value is true in the given list of truth values. * diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index 423641dc2..9fcd19b74 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -9,6 +9,7 @@ #include "storm/storage/dd/Add.h" #include "storm/storage/dd/DdManager.h" +#include "storm/abstraction/ExplicitGameStrategy.h" #include "storm/storage/StronglyConnectedComponentDecomposition.h" #include "storm/models/symbolic/DeterministicModel.h" @@ -1084,7 +1085,7 @@ namespace storm { } template - ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Groups, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy) { + ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Groups, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategy* player1Strategy, storm::abstraction::ExplicitGameStrategy* player2Strategy) { ExplicitGameProb01Result result(psiStates, storm::storage::BitVector(transitionMatrix.getRowGroupCount())); @@ -1102,7 +1103,7 @@ namespace storm { uint64_t player2Predecessor = player2PredecessorEntry.getColumn(); if (!result.player2States.get(player2Predecessor)) { bool addPlayer2State = false; - if (player2Strategy == OptimizationDirection::Minimize) { + if (player2Direction == OptimizationDirection::Minimize) { bool allChoicesHavePlayer1State = true; for (uint64_t row = transitionMatrix.getRowGroupIndices()[player2Predecessor]; row < transitionMatrix.getRowGroupIndices()[player2Predecessor + 1]; ++row) { bool choiceHasPlayer1State = false; @@ -1132,7 +1133,7 @@ namespace storm { if (!result.player1States.get(player1Predecessor)) { bool addPlayer1State = false; - if (player1Strategy == OptimizationDirection::Minimize) { + if (player1Direction == OptimizationDirection::Minimize) { bool allPlayer2Successors = true; for (uint64_t player2State = player1Groups[player1Predecessor]; player2State < player1Groups[player1Predecessor + 1]; ++player2State) { if (!result.player2States.get(player2State)) { @@ -1162,36 +1163,31 @@ namespace storm { result.player2States.complement(); // Generate player 1 strategy if required. - if (producePlayer1Strategy) { - result.player1Strategy = std::vector(result.player1States.size()); - + if (player1Strategy) { for (auto player1State : result.player1States) { - if (player1Strategy == storm::OptimizationDirection::Minimize) { + if (player1Direction == storm::OptimizationDirection::Minimize) { // At least one player 2 successor is a state with probability 0, find it. bool foundProb0Successor = false; uint64_t player2State; for (player2State = player1Groups[player1State]; player2State < player1Groups[player1State + 1]; ++player2State) { if (result.player2States.get(player2State)) { - result.player1Strategy.get()[player1State] = player2State; foundProb0Successor = true; break; } } STORM_LOG_ASSERT(foundProb0Successor, "Expected at least one state 2 successor with probability 0."); - result.player1Strategy.get()[player1State] = player2State; + player1Strategy->setChoice(player1State, player2State); } else { // Since all player 2 successors are states with probability 0, just pick any. - result.player1Strategy.get()[player1State] = player1Groups[player1State]; + player1Strategy->setChoice(player1State, player1Groups[player1State]); } } } // Generate player 2 strategy if required. - if (producePlayer2Strategy) { - result.player2Strategy = std::vector(result.player2States.size()); - + if (player2Strategy) { for (auto player2State : result.player2States) { - if (player2Strategy == storm::OptimizationDirection::Minimize) { + if (player2Direction == storm::OptimizationDirection::Minimize) { // At least one distribution only has successors with probability 0, find it. bool foundProb0SuccessorDistribution = false; @@ -1211,10 +1207,10 @@ namespace storm { } STORM_LOG_ASSERT(foundProb0SuccessorDistribution, "Expected at least one distribution with only successors with probability 0."); - result.player2Strategy.get()[player2State] = row; + player2Strategy->setChoice(player2State, row); } else { // Since all player 1 successors are states with probability 0, just pick any. - result.player2Strategy.get()[player2State] = transitionMatrix.getRowGroupIndices()[player2State]; + player2Strategy->setChoice(player2State, transitionMatrix.getRowGroupIndices()[player2State]); } } } @@ -1290,7 +1286,7 @@ namespace storm { } template - ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Groups, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy, boost::optional const& player1Candidates) { + ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Groups, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategy* player1Strategy, storm::abstraction::ExplicitGameStrategy* player2Strategy, boost::optional const& player1Candidates) { // During the execution, the two state sets in the result hold the potential player 1/2 states. ExplicitGameProb01Result result; @@ -1314,16 +1310,6 @@ namespace storm { stack.clear(); stack.insert(stack.end(), psiStates.begin(), psiStates.end()); - // If we are to produce strategies in this iteration, we prepare some storage. - if (produceStrategiesInIteration) { - if (producePlayer1Strategy) { - result.player1Strategy = std::vector(result.player1States.size()); - } - if (producePlayer2Strategy) { - result.player2Strategy = std::vector(result.player2States.size()); - } - } - // Perform the actual DFS. uint_fast64_t currentState; while (!stack.empty()) { @@ -1333,7 +1319,7 @@ namespace storm { for (auto player2PredecessorEntry : player1BackwardTransitions.getRow(currentState)) { uint64_t player2Predecessor = player2PredecessorEntry.getColumn(); if (!player2Solution.get(player2PredecessorEntry.getColumn())) { - bool addPlayer2State = player2Strategy == storm::OptimizationDirection::Minimize ? true : false; + bool addPlayer2State = player2Direction == storm::OptimizationDirection::Minimize ? true : false; uint64_t validChoice = transitionMatrix.getRowGroupIndices()[player2Predecessor]; for (uint64_t row = validChoice; row < transitionMatrix.getRowGroupIndices()[player2Predecessor + 1]; ++row) { @@ -1350,12 +1336,12 @@ namespace storm { } if (choiceHasSolutionSuccessor && choiceStaysInMaybeStates) { - if (player2Strategy == storm::OptimizationDirection::Maximize) { + if (player2Direction == storm::OptimizationDirection::Maximize) { validChoice = row; addPlayer2State = true; break; } - } else if (player2Strategy == storm::OptimizationDirection::Minimize) { + } else if (player2Direction == storm::OptimizationDirection::Minimize) { addPlayer2State = false; break; } @@ -1363,8 +1349,8 @@ namespace storm { if (addPlayer2State) { player2Solution.set(player2Predecessor); - if (produceStrategiesInIteration && producePlayer2Strategy) { - result.player2Strategy.get()[player2Predecessor] = validChoice; + if (produceStrategiesInIteration && player2Strategy) { + player2Strategy->setChoice(player2Predecessor, validChoice); } // Check whether the addition of the player 2 state changes the state of the (single) @@ -1372,17 +1358,17 @@ namespace storm { uint64_t player1Predecessor = player2BackwardTransitions[player2Predecessor]; if (!player1Solution.get(player1Predecessor)) { - bool addPlayer1State = player1Strategy == storm::OptimizationDirection::Minimize ? true : false; + bool addPlayer1State = player1Direction == storm::OptimizationDirection::Minimize ? true : false; validChoice = player1Groups[player1Predecessor]; for (uint64_t player2Successor = validChoice; player2Successor < player1Groups[player1Predecessor + 1]; ++player2Successor) { if (player2Solution.get(player2Successor)) { - if (player1Strategy == storm::OptimizationDirection::Maximize) { + if (player1Direction == storm::OptimizationDirection::Maximize) { validChoice = player2Successor; addPlayer1State = true; break; } - } else if (player1Strategy == storm::OptimizationDirection::Minimize) { + } else if (player1Direction == storm::OptimizationDirection::Minimize) { addPlayer1State = false; break; } @@ -1391,8 +1377,8 @@ namespace storm { if (addPlayer1State) { player1Solution.set(player1Predecessor); - if (produceStrategiesInIteration && producePlayer1Strategy) { - result.player1Strategy.get()[player1Predecessor] = validChoice; + if (produceStrategiesInIteration && player1Strategy) { + player1Strategy->setChoice(player1Predecessor, validChoice); } stack.emplace_back(player1Predecessor); @@ -1690,9 +1676,9 @@ namespace storm { template std::pair performProb01Min(storm::models::sparse::NondeterministicModel> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); #endif - template ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1RowGrouping, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy); + template ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1RowGrouping, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategy* player1Strategy, storm::abstraction::ExplicitGameStrategy* player2Strategy); - template ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1RowGrouping, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy, boost::optional const& player1Candidates); + template ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1RowGrouping, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategy* player1Strategy, storm::abstraction::ExplicitGameStrategy* player2Strategy, boost::optional const& player1Candidates); template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix) ; diff --git a/src/storm/utility/graph.h b/src/storm/utility/graph.h index 2e37d0318..e99fd0ba6 100644 --- a/src/storm/utility/graph.h +++ b/src/storm/utility/graph.h @@ -49,6 +49,9 @@ namespace storm { } + namespace abstraction { + class ExplicitGameStrategy; + } namespace utility { namespace graph { @@ -621,34 +624,10 @@ namespace storm { // Intentionally left empty. } - ExplicitGameProb01Result(storm::storage::BitVector const& player1States, storm::storage::BitVector const& player2States, boost::optional> const& player1Strategy = boost::none, boost::optional> const& player2Strategy = boost::none) : player1States(player1States), player2States(player2States), player1Strategy(player1Strategy), player2Strategy(player2Strategy) { + ExplicitGameProb01Result(storm::storage::BitVector const& player1States, storm::storage::BitVector const& player2States) : player1States(player1States), player2States(player2States) { // Intentionally left empty. } - bool hasPlayer1Strategy() const { - return static_cast(player1Strategy); - } - - std::vector const& getPlayer1Strategy() const { - return player1Strategy.get(); - } - - boost::optional> const& getOptionalPlayer1Strategy() { - return player1Strategy; - } - - bool hasPlayer2Strategy() const { - return static_cast(player2Strategy); - } - - std::vector const& getPlayer2Strategy() const { - return player2Strategy.get(); - } - - boost::optional> const& getOptionalPlayer2Strategy() { - return player2Strategy; - } - storm::storage::BitVector const& getPlayer1States() const { return player1States; } @@ -659,8 +638,6 @@ namespace storm { storm::storage::BitVector player1States; storm::storage::BitVector player2States; - boost::optional> player1Strategy; - boost::optional> player2Strategy; }; /*! @@ -672,11 +649,15 @@ namespace storm { * @param player2BackwardTransitions The backward transitions (player 2 to player 1). * @param phiStates The phi states of the model. * @param psiStates The psi states of the model. - * @param producePlayer1Strategy A flag indicating whether the strategy of player 1 shall be produced. - * @param producePlayer2Strategy A flag indicating whether the strategy of player 2 shall be produced. + * @param player1Direction The optimization direction of player 1. + * @param player2Direction The optimization direction of player 2. + * @param player1Strategy If not null, a player 1 strategy is synthesized and the corresponding choices + * are written to this strategy. + * @param player2Strategy If not null, a player 2 strategy is synthesized and the corresponding choices + * are written to this strategy. */ template - ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Groups, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy = false, bool producePlayer2Strategy = false); + ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Groups, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategy* player1Strategy = nullptr, storm::abstraction::ExplicitGameStrategy* player2Strategy = nullptr); /*! * Computes the set of states that have probability 1 given the strategies of the two players. @@ -687,12 +668,16 @@ namespace storm { * @param player2BackwardTransitions The backward transitions (player 2 to player 1). * @param phiStates The phi states of the model. * @param psiStates The psi states of the model. - * @param producePlayer1Strategy A flag indicating whether the strategy of player 1 shall be produced. - * @param producePlayer2Strategy A flag indicating whether the strategy of player 2 shall be produced. + * @param player1Direction The optimization direction of player 1. + * @param player2Direction The optimization direction of player 2. + * @param player1Strategy If not null, a player 1 strategy is synthesized and the corresponding choices + * are written to this strategy. + * @param player2Strategy If not null, a player 2 strategy is synthesized and the corresponding choices + * are written to this strategy. * @param player1Candidates If given, this set constrains the candidates of player 1 states that are considered. */ template - ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Groups, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy = false, bool producePlayer2Strategy = false, boost::optional const& player1Candidates = boost::none); + ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Groups, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategy* player1Strategy = nullptr, storm::abstraction::ExplicitGameStrategy* player2Strategy = nullptr, boost::optional const& player1Candidates = boost::none); /*! * Performs a topological sort of the states of the system according to the given transitions.