From d3bbe4df10637ae50afc6449cce2a4be841e348b Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 27 Mar 2018 16:44:19 +0200 Subject: [PATCH] explicit interpolation and started on explicit quantitative solution --- .../abstraction/AbstractionInformation.cpp | 16 ++ .../abstraction/AbstractionInformation.h | 8 +- .../ExplicitQuantiativeResultMinMax.cpp | 48 +++++ .../ExplicitQuantitativeResult.cpp | 54 ++++++ .../abstraction/ExplicitQuantitativeResult.h | 31 +++ .../ExplicitQuantitativeResultMinMax.cpp | 61 ++++++ .../ExplicitQuantitativeResultMinMax.h | 32 ++++ src/storm/abstraction/MenuGameAbstractor.cpp | 9 + src/storm/abstraction/MenuGameAbstractor.h | 2 + src/storm/abstraction/MenuGameRefiner.cpp | 177 ++++++++++++++++-- src/storm/abstraction/MenuGameRefiner.h | 5 + .../abstraction/jani/AutomatonAbstractor.cpp | 5 + .../abstraction/jani/AutomatonAbstractor.h | 5 + src/storm/abstraction/jani/EdgeAbstractor.cpp | 5 + src/storm/abstraction/jani/EdgeAbstractor.h | 5 + .../jani/JaniMenuGameAbstractor.cpp | 5 + .../abstraction/jani/JaniMenuGameAbstractor.h | 5 + .../abstraction/prism/CommandAbstractor.cpp | 5 + .../abstraction/prism/CommandAbstractor.h | 5 + .../abstraction/prism/ModuleAbstractor.cpp | 5 + .../abstraction/prism/ModuleAbstractor.h | 5 + .../prism/PrismMenuGameAbstractor.cpp | 5 + .../prism/PrismMenuGameAbstractor.h | 5 + .../abstraction/GameBasedMdpModelChecker.cpp | 89 ++++++++- .../abstraction/GameBasedMdpModelChecker.h | 7 + .../symbolic/StochasticTwoPlayerGame.cpp | 5 + .../models/symbolic/StochasticTwoPlayerGame.h | 5 + 27 files changed, 585 insertions(+), 24 deletions(-) create mode 100644 src/storm/abstraction/ExplicitQuantiativeResultMinMax.cpp create mode 100644 src/storm/abstraction/ExplicitQuantitativeResult.cpp create mode 100644 src/storm/abstraction/ExplicitQuantitativeResult.h create mode 100644 src/storm/abstraction/ExplicitQuantitativeResultMinMax.cpp create mode 100644 src/storm/abstraction/ExplicitQuantitativeResultMinMax.h diff --git a/src/storm/abstraction/AbstractionInformation.cpp b/src/storm/abstraction/AbstractionInformation.cpp index 5e25b5530..d6d375544 100644 --- a/src/storm/abstraction/AbstractionInformation.cpp +++ b/src/storm/abstraction/AbstractionInformation.cpp @@ -138,6 +138,22 @@ namespace storm { return result; } + template + std::vector AbstractionInformation::getPredicatesExcludingBottom(storm::storage::BitVector const& predicateValuation) const { + STORM_LOG_ASSERT(predicateValuation.size() == this->getNumberOfPredicates() + 1, "Size of predicate valuation does not match number of predicates."); + + std::vector result; + for (uint64_t index = 0; index < this->getNumberOfPredicates(); ++index) { + if (predicateValuation[index + 1]) { + result.push_back(this->getPredicateByIndex(index)); + } else { + result.push_back(!this->getPredicateByIndex(index)); + } + } + + return result; + } + template storm::expressions::Expression const& AbstractionInformation::getPredicateByIndex(uint_fast64_t index) const { return predicates[index]; diff --git a/src/storm/abstraction/AbstractionInformation.h b/src/storm/abstraction/AbstractionInformation.h index 093342993..fa1a1927a 100644 --- a/src/storm/abstraction/AbstractionInformation.h +++ b/src/storm/abstraction/AbstractionInformation.h @@ -139,7 +139,13 @@ namespace storm { * Retrieves a list of expression that corresponds to the given predicate valuation. */ std::vector getPredicates(storm::storage::BitVector const& predicateValuation) const; - + + /*! + * Retrieves a list of expression that corresponds to the given predicate valuation that mentions all of the + * predicates' truth values *and* the value of the bottom variable (at the first index). + */ + std::vector getPredicatesExcludingBottom(storm::storage::BitVector const& predicateValuation) const; + /*! * Retrieves the predicate with the given index. * diff --git a/src/storm/abstraction/ExplicitQuantiativeResultMinMax.cpp b/src/storm/abstraction/ExplicitQuantiativeResultMinMax.cpp new file mode 100644 index 000000000..35237f4d5 --- /dev/null +++ b/src/storm/abstraction/ExplicitQuantiativeResultMinMax.cpp @@ -0,0 +1,48 @@ +#include "storm/abstraction/ExplicitQuantitativeResultMinMax.h" + +namespace storm { + namespace abstraction { + + template + ExplicitQuantitativeResultMinMax::ExplicitQuantitativeResultMinMax(uint64_t numberOfStates) = default; + + template + ExplicitQuantitativeResult const& ExplicitQuantitativeResultMinMax::getMin() const { + return min; + } + + template + ExplicitQuantitativeResult& ExplicitQuantitativeResultMinMax::getMin() { + return min; + } + + template + ExplicitQuantitativeResult const& ExplicitQuantitativeResultMinMax::getMax() const { + return max; + } + + template + ExplicitQuantitativeResult& ExplicitQuantitativeResultMinMax::getMax() { + return max; + } + + template + ExplicitQuantitativeResult const& ExplicitQuantitativeResultMinMax::get(storm::OptimizationDirection const& dir) const { + if (dir == storm::OptimizationDirection::Minimize) { + return this->getMin(); + } else { + return this->getMax(); + } + } + + template + ExplicitQuantitativeResult& ExplicitQuantitativeResultMinMax::get(storm::OptimizationDirection const& dir) { + if (dir == storm::OptimizationDirection::Minimize) { + return this->getMin(); + } else { + return this->getMax(); + } + } + + } +} diff --git a/src/storm/abstraction/ExplicitQuantitativeResult.cpp b/src/storm/abstraction/ExplicitQuantitativeResult.cpp new file mode 100644 index 000000000..4b996483d --- /dev/null +++ b/src/storm/abstraction/ExplicitQuantitativeResult.cpp @@ -0,0 +1,54 @@ +#include "storm/abstraction/ExplicitQuantitativeResult.h" + +#include "storm/storage/BitVector.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/InvalidArgumentException.h" + +namespace storm { + namespace abstraction { + + template + ExplicitQuantitativeResult::ExplicitQuantitativeResult(uint64_t numberOfStates) : values(numberOfStates) { + // Intentionally left empty. + } + + template + std::vector const& ExplicitQuantitativeResult::getValues() const { + return values; + } + + template + std::vector& ExplicitQuantitativeResult::getValues() { + return values; + } + + template + void ExplicitQuantitativeResult::setValue(uint64_t state, ValueType const& value) { + values[state] = value; + } + + template + std::pair ExplicitQuantitativeResult::getRange(storm::storage::BitVector const& states) const { + STORM_LOG_THROW(!states.empty(), storm::exceptions::InvalidArgumentException, "Expected non-empty set of states."); + + auto stateIt = states.begin(); + std::pair result = std::make_pair(values[*stateIt], values[*stateIt]); + ++stateIt; + + while (stateIt != states.end()) { + if (values[*stateIt] < result.first) { + result.first = values[*stateIt]; + } else if (values[*stateIt] < result.first) { + result.second = values[*stateIt]; + } + + ++stateIt; + } + + return result; + } + + template class ExplicitQuantitativeResult; + } +} diff --git a/src/storm/abstraction/ExplicitQuantitativeResult.h b/src/storm/abstraction/ExplicitQuantitativeResult.h new file mode 100644 index 000000000..7604655d8 --- /dev/null +++ b/src/storm/abstraction/ExplicitQuantitativeResult.h @@ -0,0 +1,31 @@ +#pragma once + +#include +#include + +namespace storm { + namespace storage { + class BitVector; + } + + namespace abstraction { + + template + class ExplicitQuantitativeResult { + public: + ExplicitQuantitativeResult() = default; + ExplicitQuantitativeResult(uint64_t numberOfStates); + + std::vector const& getValues() const; + std::vector& getValues(); + void setValue(uint64_t state, ValueType const& value); + + std::pair getRange(storm::storage::BitVector const& states) const; + + private: + std::vector values; + }; + + } +} + diff --git a/src/storm/abstraction/ExplicitQuantitativeResultMinMax.cpp b/src/storm/abstraction/ExplicitQuantitativeResultMinMax.cpp new file mode 100644 index 000000000..fe8799a9f --- /dev/null +++ b/src/storm/abstraction/ExplicitQuantitativeResultMinMax.cpp @@ -0,0 +1,61 @@ +#include "storm/abstraction/ExplicitQuantitativeResultMinMax.h" + +namespace storm { + namespace abstraction { + + template + ExplicitQuantitativeResultMinMax::ExplicitQuantitativeResultMinMax(uint64_t numberOfStates) : min(numberOfStates), max(numberOfStates) { + // Intentionally left empty. + } + + template + ExplicitQuantitativeResult const& ExplicitQuantitativeResultMinMax::getMin() const { + return min; + } + + template + ExplicitQuantitativeResult& ExplicitQuantitativeResultMinMax::getMin() { + return min; + } + + template + ExplicitQuantitativeResult const& ExplicitQuantitativeResultMinMax::getMax() const { + return max; + } + + template + ExplicitQuantitativeResult& ExplicitQuantitativeResultMinMax::getMax() { + return max; + } + + template + void ExplicitQuantitativeResultMinMax::setMin(ExplicitQuantitativeResult&& newMin) { + min = std::move(newMin); + } + + template + void ExplicitQuantitativeResultMinMax::setMax(ExplicitQuantitativeResult&& newMax) { + max = std::move(newMax); + } + + template + ExplicitQuantitativeResult const& ExplicitQuantitativeResultMinMax::get(storm::OptimizationDirection const& dir) const { + if (dir == storm::OptimizationDirection::Minimize) { + return this->getMin(); + } else { + return this->getMax(); + } + } + + template + ExplicitQuantitativeResult& ExplicitQuantitativeResultMinMax::get(storm::OptimizationDirection const& dir) { + if (dir == storm::OptimizationDirection::Minimize) { + return this->getMin(); + } else { + return this->getMax(); + } + } + + template class ExplicitQuantitativeResultMinMax; + } +} diff --git a/src/storm/abstraction/ExplicitQuantitativeResultMinMax.h b/src/storm/abstraction/ExplicitQuantitativeResultMinMax.h new file mode 100644 index 000000000..f22ff4edb --- /dev/null +++ b/src/storm/abstraction/ExplicitQuantitativeResultMinMax.h @@ -0,0 +1,32 @@ +#pragma once + +#include "storm/abstraction/ExplicitQuantitativeResult.h" + +#include "storm/solver/OptimizationDirection.h" + +namespace storm { + namespace abstraction { + + template + class ExplicitQuantitativeResultMinMax { + public: + ExplicitQuantitativeResultMinMax() = default; + ExplicitQuantitativeResultMinMax(uint64_t numberOfStates); + + ExplicitQuantitativeResult const& getMin() const; + ExplicitQuantitativeResult& getMin(); + ExplicitQuantitativeResult const& getMax() const; + ExplicitQuantitativeResult& getMax(); + ExplicitQuantitativeResult const& get(storm::OptimizationDirection const& dir) const; + ExplicitQuantitativeResult& get(storm::OptimizationDirection const& dir); + + void setMin(ExplicitQuantitativeResult&& newMin); + void setMax(ExplicitQuantitativeResult&& newMax); + + private: + ExplicitQuantitativeResult min; + ExplicitQuantitativeResult max; + }; + + } +} diff --git a/src/storm/abstraction/MenuGameAbstractor.cpp b/src/storm/abstraction/MenuGameAbstractor.cpp index f68694c30..c999b9316 100644 --- a/src/storm/abstraction/MenuGameAbstractor.cpp +++ b/src/storm/abstraction/MenuGameAbstractor.cpp @@ -23,6 +23,15 @@ namespace storm { // Intentionally left empty. } + template + std::vector> MenuGameAbstractor::getVariableUpdates(uint64_t player1Choice) const { + std::vector> result(this->getNumberOfUpdates(player1Choice)); + for (uint64_t i = 0; i < result.size(); ++i) { + result[i] = this->getVariableUpdates(player1Choice, i); + } + return result; + } + template std::string getStateName(std::pair const& stateValue, std::set const& locationVariables, std::set const& predicateVariables, storm::expressions::Variable const& bottomVariable) { std::stringstream stateName; diff --git a/src/storm/abstraction/MenuGameAbstractor.h b/src/storm/abstraction/MenuGameAbstractor.h index 35fc75c42..ee753bebc 100644 --- a/src/storm/abstraction/MenuGameAbstractor.h +++ b/src/storm/abstraction/MenuGameAbstractor.h @@ -34,6 +34,8 @@ namespace storm { virtual AbstractionInformation const& getAbstractionInformation() const = 0; virtual storm::expressions::Expression const& getGuard(uint64_t player1Choice) const = 0; virtual std::pair getPlayer1ChoiceRange() const = 0; + virtual uint64_t getNumberOfUpdates(uint64_t player1Choice) const = 0; + std::vector> getVariableUpdates(uint64_t player1Choice) const; virtual std::map getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const = 0; virtual storm::expressions::Expression getInitialExpression() const = 0; diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index a5d1f647e..76e528ee7 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -526,6 +526,112 @@ namespace storm { predicates.back().push_back(initialExpression.changeManager(expressionManager).substitute(lastSubstitution)); return std::make_pair(predicates, stepVariableToCopiedVariableMap); } + + template + const uint64_t ExplicitPivotStateResult::NO_PREDECESSOR = std::numeric_limits::max(); + + template + std::pair>, std::map> MenuGameRefiner::buildTrace(storm::expressions::ExpressionManager& expressionManager, storm::abstraction::MenuGame const& game, ExplicitPivotStateResult const& pivotStateResult, storm::dd::Odd const& odd) const { + + std::vector> predicates; + + AbstractionInformation const& abstractionInformation = abstractor.get().getAbstractionInformation(); + storm::expressions::Expression initialExpression = abstractor.get().getInitialExpression(); + + std::set oldVariables = initialExpression.getVariables(); + for (auto const& predicate : abstractionInformation.getPredicates()) { + std::set usedVariables = predicate.getVariables(); + oldVariables.insert(usedVariables.begin(), usedVariables.end()); + } + + std::map oldToNewVariables; + for (auto const& variable : oldVariables) { + oldToNewVariables[variable] = expressionManager.getVariable(variable.getName()); + } + std::map lastSubstitution; + for (auto const& variable : oldToNewVariables) { + lastSubstitution[variable.second] = variable.second; + } + std::map stepVariableToCopiedVariableMap; + + // The state valuation also includes the bottom state, so we need to reserve one more than the number of + // predicates here. + storm::storage::BitVector extendedPredicateValuation = odd.getEncoding(pivotStateResult.pivotState, abstractionInformation.getNumberOfPredicates() + 1); + + // Decode pivot state. + predicates.emplace_back(abstractionInformation.getPredicatesExcludingBottom(extendedPredicateValuation)); + for (auto& predicate : predicates.back()) { + predicate = predicate.changeManager(expressionManager); + } + + // Perform a backward traversal from the pivot state along the chosen predecessors until there is no more + // predecessors. + uint64_t currentState = pivotStateResult.predecessors[pivotStateResult.pivotState].first; + uint64_t currentAction = pivotStateResult.predecessors[pivotStateResult.pivotState].second; + while (currentState != ExplicitPivotStateResult::NO_PREDECESSOR) { + // Create a new copy of each variable to use for this step. + std::map substitution; + for (auto const& variablePair : oldToNewVariables) { + storm::expressions::Variable variableCopy = expressionManager.declareVariableCopy(variablePair.second); + substitution[variablePair.second] = variableCopy; + stepVariableToCopiedVariableMap[variableCopy] = variablePair.second; + } + + // Retrieve the variable updates that the predecessor needs to perform to get to the current state. + auto variableUpdateVector = abstractor.get().getVariableUpdates(currentAction); + storm::expressions::Expression allVariableUpdateExpression; + for (auto const& variableUpdates : variableUpdateVector) { + storm::expressions::Expression variableUpdateExpression; + for (auto const& oldNewVariablePair : oldToNewVariables) { + storm::expressions::Variable const& newVariable = oldNewVariablePair.second; + + // If the variable was set, use its update expression. + auto updateIt = variableUpdates.find(oldNewVariablePair.first); + if (updateIt != variableUpdates.end()) { + auto const& update = *updateIt; + + if (update.second.hasBooleanType()) { + variableUpdateExpression = variableUpdateExpression && storm::expressions::iff(lastSubstitution.at(newVariable), update.second.changeManager(expressionManager).substitute(substitution)); + } else { + variableUpdateExpression = variableUpdateExpression && lastSubstitution.at(newVariable) == update.second.changeManager(expressionManager).substitute(substitution); + } + } else { + // Otherwise, make sure that the new variable maintains the old value. + if (newVariable.hasBooleanType()) { + variableUpdateExpression = variableUpdateExpression && storm::expressions::iff(lastSubstitution.at(newVariable), substitution.at(newVariable)); + } else { + variableUpdateExpression = variableUpdateExpression && lastSubstitution.at(newVariable) == substitution.at(newVariable); + } + } + } + + allVariableUpdateExpression = allVariableUpdateExpression || variableUpdateExpression; + } + + // Add variable update expression. + predicates.back().emplace_back(allVariableUpdateExpression); + + // Add the guard of the choice. + predicates.back().emplace_back(abstractor.get().getGuard(currentAction).changeManager(expressionManager).substitute(substitution)); + + // Retrieve the predicate valuation in the predecessor. + extendedPredicateValuation = odd.getEncoding(currentState, abstractionInformation.getNumberOfPredicates() + 1); + predicates.emplace_back(abstractionInformation.getPredicatesExcludingBottom(extendedPredicateValuation)); + for (auto& predicate : predicates.back()) { + predicate = predicate.changeManager(expressionManager).substitute(substitution); + } + + // Move backwards one step. + lastSubstitution = std::move(substitution); + + std::pair predecessorPair = pivotStateResult.predecessors[currentState]; + currentState = predecessorPair.first; + currentAction = predecessorPair.second; + } + + predicates.back().push_back(initialExpression.changeManager(expressionManager).substitute(lastSubstitution)); + return std::make_pair(predicates, stepVariableToCopiedVariableMap); + } template boost::optional derivePredicatesFromInterpolation(storm::expressions::ExpressionManager& interpolationManager, AbstractionInformation const& abstractionInformation, std::vector> const& trace, std::map const& variableSubstitution) { @@ -579,8 +685,6 @@ namespace storm { 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) { @@ -590,6 +694,7 @@ namespace storm { } // Create a new expression manager that we can use for the interpolation. + AbstractionInformation const& abstractionInformation = abstractor.get().getAbstractionInformation(); std::shared_ptr interpolationManager = abstractionInformation.getExpressionManager().clone(); // Build the trace of the most probable path in terms of which predicates hold in each step. @@ -600,7 +705,15 @@ namespace storm { template boost::optional MenuGameRefiner::derivePredicatesFromInterpolation(storm::abstraction::MenuGame const& game, ExplicitPivotStateResult const& pivotStateResult, storm::dd::Odd const& odd) const { - // TODO. + + // Create a new expression manager that we can use for the interpolation. + AbstractionInformation const& abstractionInformation = abstractor.get().getAbstractionInformation(); + 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, pivotStateResult, odd); + + return storm::abstraction::derivePredicatesFromInterpolation(*interpolationManager, abstractionInformation, traceAndVariableSubstitution.first, traceAndVariableSubstitution.second); } template @@ -631,7 +744,7 @@ 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. - SymbolicPivotStateResult SymbolicPivotStateResult = 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. @@ -677,12 +790,12 @@ namespace storm { 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."); @@ -693,8 +806,11 @@ namespace storm { } template - 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) { + boost::optional> pickPivotState(bool generatePredecessors, AbstractionSettings::PivotSelectionHeuristic pivotSelectionHeuristic, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Grouping, std::vector const& player1Labeling, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& relevantStates, storm::storage::BitVector const& targetStates, ExplicitQualitativeGameResultMinMax const& qualitativeResult, ExplicitGameStrategyPair const& minStrategyPair, ExplicitGameStrategyPair const& maxStrategyPair, std::vector const* lowerValues = nullptr, std::vector const* upperValues = nullptr) { + STORM_LOG_ASSERT(!lowerValues || upperValues, "Expected none or both value results."); + STORM_LOG_ASSERT(!upperValues || lowerValues, "Expected none or both value results."); + // 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 result; @@ -705,7 +821,7 @@ namespace storm { ValueType zeroDistance = probabilityDistances ? storm::utility::one() : storm::utility::zero(); std::vector distances(numberOfStates, inftyDistance); if (generatePredecessors) { - result.predecessors.resize(numberOfStates, std::make_pair(0, 0)); + result.predecessors.resize(numberOfStates, std::make_pair(ExplicitPivotStateResult::NO_PREDECESSOR, ExplicitPivotStateResult::NO_PREDECESSOR)); } // Use set as priority queue with unique membership; default comparison on pair works fine if distance is @@ -722,8 +838,9 @@ namespace storm { } // For some heuristics, we need to potentially find more than just one pivot. + bool considerDeviation = (pivotSelectionHeuristic == storm::settings::modules::AbstractionSettings::PivotSelectionHeuristic::NearestMaximalDeviation || pivotSelectionHeuristic == storm::settings::modules::AbstractionSettings::PivotSelectionHeuristic::MaxWeightedDeviation) && lowerValues && upperValues; bool foundPivotState = false; - ValueType maximalDeviation = storm::utility::zero(); + ValueType pivotStateDeviation = storm::utility::zero(); while (!dijkstraQueue.empty()) { auto distanceStatePair = *dijkstraQueue.begin(); @@ -731,8 +848,17 @@ namespace storm { ValueType currentDistance = distanceStatePair.first; dijkstraQueue.erase(dijkstraQueue.begin()); - if (foundPivotState && currentDistance > result.distance) { - return result; + if (foundPivotState && (probabilityDistances ? currentDistance < result.distance : currentDistance > result.distance)) { + if (pivotSelectionHeuristic != storm::settings::modules::AbstractionSettings::PivotSelectionHeuristic::MaxWeightedDeviation) { + // For the nearest maximal deviation and most probable path heuristics, future pivot states are + // not important any more, because their distance will be strictly larger, so we can return the + // current pivot state. + return result; + } else if (pivotStateDeviation >= currentDistance) { + // If the heuristic is maximal weighted deviation and the weighted deviation for any future pivot + // state is necessarily at most as high as the current one, we can abort the search. + return result; + } } // Determine whether the current state is a pivot state. @@ -751,14 +877,26 @@ namespace storm { // If it is indeed a pivot state, we can abort the search here. if (isPivotState) { - if (foundPivotState && haveQuantitativeResults && deviationOfCurrentState > currentPivotState) { - result.pivotState = currentState; - maximalDeviation = deviationForCurrentState; + if (considerDeviation && foundPivotState) { + ValueType deviationOfCurrentState = (*upperValues)[currentState] - (*lowerValues)[currentState]; + if (deviationOfCurrentState > pivotStateDeviation) { + result.pivotState = currentState; + pivotStateDeviation = deviationOfCurrentState; + if (pivotSelectionHeuristic == storm::settings::modules::AbstractionSettings::PivotSelectionHeuristic::MaxWeightedDeviation) { + // Scale the deviation with the distance (probability) for this heuristic. + pivotStateDeviation *= currentDistance; + } + } } else if (!foundPivotState) { result.pivotState = currentState; result.distance = distances[currentState]; foundPivotState = true; } + + // If there is no need to look at other deviations, stop here. + if (!considerDeviation) { + return result; + } } // Otherwise, we explore all its relevant successors. @@ -776,7 +914,7 @@ namespace storm { if ((probabilityDistances && alternateDistance > distances[player1Successor]) || (!probabilityDistances && alternateDistance < distances[player1Successor])) { distances[player1Successor] = alternateDistance; if (generatePredecessors) { - result.predecessors[player1Successor] = std::make_pair(currentState, minPlayer2Successor); + result.predecessors[player1Successor] = std::make_pair(currentState, player1Labeling[minPlayer2Successor]); } dijkstraQueue.emplace(alternateDistance, player1Successor); } @@ -812,12 +950,10 @@ namespace storm { 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()); - boost::optional> optionalPivotStateResult = pickPivotState(useInterpolation, pivotSelectionHeuristic, transitionMatrix, player1Grouping, initialStates, relevantStates, targetStates, qualitativeResult, minStrategyPair, maxStrategyPair); + boost::optional> optionalPivotStateResult = pickPivotState(useInterpolation, pivotSelectionHeuristic, transitionMatrix, player1Grouping, player1Labeling, initialStates, relevantStates, targetStates, qualitativeResult, minStrategyPair, maxStrategyPair); // If there was no pivot state, continue the search. if (!optionalPivotStateResult) { @@ -866,7 +1002,6 @@ namespace storm { boost::optional predicates; if (useInterpolation) { predicates = derivePredicatesFromInterpolation(game, pivotStateResult, odd); - } if (!predicates) { predicates = derivePredicatesFromPivotState(game, symbolicPivotState, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy); @@ -972,7 +1107,9 @@ namespace storm { for (auto const& predicate : command.getPredicates()) { STORM_LOG_TRACE(predicate); } - abstractor.get().refine(command); + if (!command.getPredicates().empty()) { + abstractor.get().refine(command); + } } STORM_LOG_TRACE("Current set of predicates:"); diff --git a/src/storm/abstraction/MenuGameRefiner.h b/src/storm/abstraction/MenuGameRefiner.h index d4d913a1f..5e7be4d2d 100644 --- a/src/storm/abstraction/MenuGameRefiner.h +++ b/src/storm/abstraction/MenuGameRefiner.h @@ -82,6 +82,9 @@ namespace storm { /// The distance with which the state in question is reached. ValueType distance; + /// The value filled in for states without predecessors in the search. + static const uint64_t NO_PREDECESSOR; + /// The predecessors for the states to obtain the given distance. std::vector> predecessors; }; @@ -146,6 +149,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; + + std::pair>, std::map> buildTrace(storm::expressions::ExpressionManager& expressionManager, storm::abstraction::MenuGame const& game, ExplicitPivotStateResult const& pivotStateResult, storm::dd::Odd const& odd) 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; diff --git a/src/storm/abstraction/jani/AutomatonAbstractor.cpp b/src/storm/abstraction/jani/AutomatonAbstractor.cpp index b97ad6002..5ab326657 100644 --- a/src/storm/abstraction/jani/AutomatonAbstractor.cpp +++ b/src/storm/abstraction/jani/AutomatonAbstractor.cpp @@ -51,6 +51,11 @@ namespace storm { return edges[player1Choice].getGuard(); } + template + uint64_t AutomatonAbstractor::getNumberOfUpdates(uint64_t player1Choice) const { + return edges[player1Choice].getNumberOfUpdates(player1Choice); + } + template std::map AutomatonAbstractor::getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const { return edges[player1Choice].getVariableUpdates(auxiliaryChoice); diff --git a/src/storm/abstraction/jani/AutomatonAbstractor.h b/src/storm/abstraction/jani/AutomatonAbstractor.h index ac010a0d9..e9ff1d76a 100644 --- a/src/storm/abstraction/jani/AutomatonAbstractor.h +++ b/src/storm/abstraction/jani/AutomatonAbstractor.h @@ -57,6 +57,11 @@ namespace storm { */ storm::expressions::Expression const& getGuard(uint64_t player1Choice) const; + /*! + * Retrieves the number of updates of the specified player 1 choice. + */ + uint64_t getNumberOfUpdates(uint64_t player1Choice) const; + /*! * Retrieves a mapping from variables to expressions that define their updates wrt. to the given player * 1 choice and auxiliary choice. diff --git a/src/storm/abstraction/jani/EdgeAbstractor.cpp b/src/storm/abstraction/jani/EdgeAbstractor.cpp index eaaafe266..8f0ab300e 100644 --- a/src/storm/abstraction/jani/EdgeAbstractor.cpp +++ b/src/storm/abstraction/jani/EdgeAbstractor.cpp @@ -65,6 +65,11 @@ namespace storm { return edge.get().getGuard(); } + template + uint64_t EdgeAbstractor::getNumberOfUpdates(uint64_t player1Choice) const { + return edge.get().getNumberOfDestinations(); + } + template std::map EdgeAbstractor::getVariableUpdates(uint64_t auxiliaryChoice) const { return edge.get().getDestination(auxiliaryChoice).getAsVariableToExpressionMap(); diff --git a/src/storm/abstraction/jani/EdgeAbstractor.h b/src/storm/abstraction/jani/EdgeAbstractor.h index ac88b6b04..f3dfa531c 100644 --- a/src/storm/abstraction/jani/EdgeAbstractor.h +++ b/src/storm/abstraction/jani/EdgeAbstractor.h @@ -72,6 +72,11 @@ namespace storm { */ storm::expressions::Expression const& getGuard() const; + /*! + * Retrieves the number of updates of this edge. + */ + uint64_t getNumberOfUpdates(uint64_t player1Choice) const; + /*! * Retrieves a mapping from variables to expressions that define their updates wrt. to the given * auxiliary choice. diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp index 215aeb780..a5bc90ed0 100644 --- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp +++ b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp @@ -119,6 +119,11 @@ namespace storm { return automata.front().getGuard(player1Choice); } + template + uint64_t JaniMenuGameAbstractor::getNumberOfUpdates(uint64_t player1Choice) const { + return automata.front().getNumberOfUpdates(player1Choice); + } + template std::map JaniMenuGameAbstractor::getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const { return automata.front().getVariableUpdates(player1Choice, auxiliaryChoice); diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.h b/src/storm/abstraction/jani/JaniMenuGameAbstractor.h index 0ef49f908..0a366c625 100644 --- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.h +++ b/src/storm/abstraction/jani/JaniMenuGameAbstractor.h @@ -75,6 +75,11 @@ namespace storm { */ storm::expressions::Expression const& getGuard(uint64_t player1Choice) const override; + /*! + * Retrieves the number of updates of the specified player 1 choice. + */ + virtual uint64_t getNumberOfUpdates(uint64_t player1Choice) const override; + /*! * Retrieves a mapping from variables to expressions that define their updates wrt. to the given player * 1 choice and auxiliary choice. diff --git a/src/storm/abstraction/prism/CommandAbstractor.cpp b/src/storm/abstraction/prism/CommandAbstractor.cpp index afc859e01..15b68685e 100644 --- a/src/storm/abstraction/prism/CommandAbstractor.cpp +++ b/src/storm/abstraction/prism/CommandAbstractor.cpp @@ -65,6 +65,11 @@ namespace storm { return command.get().getGuardExpression(); } + template + uint64_t CommandAbstractor::getNumberOfUpdates(uint64_t player1Choice) const { + return command.get().getNumberOfUpdates(); + } + template std::map CommandAbstractor::getVariableUpdates(uint64_t auxiliaryChoice) const { return command.get().getUpdate(auxiliaryChoice).getAsVariableToExpressionMap(); diff --git a/src/storm/abstraction/prism/CommandAbstractor.h b/src/storm/abstraction/prism/CommandAbstractor.h index b26492125..d5c725921 100644 --- a/src/storm/abstraction/prism/CommandAbstractor.h +++ b/src/storm/abstraction/prism/CommandAbstractor.h @@ -70,6 +70,11 @@ namespace storm { */ storm::expressions::Expression const& getGuard() const; + /*! + * Retrieves the number of updates of this command. + */ + uint64_t getNumberOfUpdates(uint64_t player1Choice) const; + /*! * Retrieves a mapping from variables to expressions that define their updates wrt. to the given * auxiliary choice. diff --git a/src/storm/abstraction/prism/ModuleAbstractor.cpp b/src/storm/abstraction/prism/ModuleAbstractor.cpp index 6ba51b062..b5180ecf4 100644 --- a/src/storm/abstraction/prism/ModuleAbstractor.cpp +++ b/src/storm/abstraction/prism/ModuleAbstractor.cpp @@ -45,6 +45,11 @@ namespace storm { return commands[player1Choice].getGuard(); } + template + uint64_t ModuleAbstractor::getNumberOfUpdates(uint64_t player1Choice) const { + return commands[player1Choice].getNumberOfUpdates(player1Choice); + } + template std::map ModuleAbstractor::getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const { return commands[player1Choice].getVariableUpdates(auxiliaryChoice); diff --git a/src/storm/abstraction/prism/ModuleAbstractor.h b/src/storm/abstraction/prism/ModuleAbstractor.h index 3cfb21ca7..8aef43562 100644 --- a/src/storm/abstraction/prism/ModuleAbstractor.h +++ b/src/storm/abstraction/prism/ModuleAbstractor.h @@ -60,6 +60,11 @@ namespace storm { */ storm::expressions::Expression const& getGuard(uint64_t player1Choice) const; + /*! + * Retrieves the number of updates of the specified player 1 choice. + */ + uint64_t getNumberOfUpdates(uint64_t player1Choice) const; + /*! * Retrieves a mapping from variables to expressions that define their updates wrt. to the given player * 1 choice and auxiliary choice. diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp index 99dc2c5a2..718207120 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp @@ -115,6 +115,11 @@ namespace storm { return modules.front().getGuard(player1Choice); } + template + uint64_t PrismMenuGameAbstractor::getNumberOfUpdates(uint64_t player1Choice) const { + return modules.front().getNumberOfUpdates(player1Choice); + } + template std::map PrismMenuGameAbstractor::getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const { return modules.front().getVariableUpdates(player1Choice, auxiliaryChoice); diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.h b/src/storm/abstraction/prism/PrismMenuGameAbstractor.h index 55845f134..ce5f7ac42 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.h +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.h @@ -74,6 +74,11 @@ namespace storm { * @return The guard of the player 1 choice. */ storm::expressions::Expression const& getGuard(uint64_t player1Choice) const override; + + /*! + * Retrieves the number of updates of the specified player 1 choice. + */ + virtual uint64_t getNumberOfUpdates(uint64_t player1Choice) const override; /*! * Retrieves a mapping from variables to expressions that define their updates wrt. to the given player diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 25b110e06..004d7993d 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -27,6 +27,7 @@ #include "storm/abstraction/ExplicitGameStrategyPair.h" #include "storm/abstraction/ExplicitQualitativeGameResultMinMax.h" +#include "storm/abstraction/ExplicitQuantitativeResultMinMax.h" #include "storm/logic/FragmentSpecification.h" @@ -49,7 +50,10 @@ namespace storm { using storm::abstraction::SymbolicQuantitativeGameResult; using storm::abstraction::SymbolicQuantitativeGameResultMinMax; - + using storm::abstraction::ExplicitQuantitativeResult; + using storm::abstraction::ExplicitQuantitativeResultMinMax; + using storm::abstraction::ExplicitGameStrategyPair; + template GameBasedMdpModelChecker::GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, std::shared_ptr const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), comparator(storm::settings::getModule().getPrecision()), reuseQualitativeResults(false), reuseQuantitativeResults(false), solveMode(storm::settings::getModule().getSolveMode()) { model.requireNoUndefinedConstants(); @@ -385,6 +389,35 @@ namespace storm { return result; } + template + ExplicitQuantitativeResult computeQuantitativeResult(Environment const& env, storm::OptimizationDirection player1Direction, storm::OptimizationDirection player2Direction, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Groups, ExplicitQualitativeGameResultMinMax const& qualitativeResult, storm::storage::BitVector const& maybeStates, ExplicitGameStrategyPair& minStrategyPair) { + + bool player2Min = player2Direction == storm::OptimizationDirection::Minimize; + auto const& player2Prob0States = player2Min ? qualitativeResult.getProb0Min().asExplicitQualitativeGameResult().getPlayer2States() : qualitativeResult.getProb0Max().asExplicitQualitativeGameResult().getPlayer2States(); + auto const& player2Prob1States = player2Min ? qualitativeResult.getProb1Min().asExplicitQualitativeGameResult().getPlayer2States() : qualitativeResult.getProb1Max().asExplicitQualitativeGameResult().getPlayer2States(); + + // Determine which rows to keep. + storm::storage::BitVector rows(transitionMatrix.getRowCount()); + for (uint64_t player2State = 0; player2State < transitionMatrix.getRowGroupCount(); ++player2State) { + if (!player2Prob0States.get(player2State) && !player2Prob1States.get(player2State)) { + // Mark all rows that have a maybe state as a successor. + for (uint64_t row = transitionMatrix.getRowGroupIndices()[player2State]; row < transitionMatrix.getRowGroupIndices()[player2State + 1]; ++row) { + bool hasMaybeStateSuccessor = false; + for (auto const& entry : transitionMatrix.getRow(row)) { + if (maybeStates.get(entry.getColumn())) { + hasMaybeStateSuccessor = true; + } + } + if (!hasMaybeStateSuccessor) { + rows.set(row); + } + } + } + } + + storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, player2MaybeStates, <#const storm::storage::BitVector &columnConstraint#>) + } + template std::unique_ptr GameBasedMdpModelChecker::performGameBasedAbstractionRefinement(Environment const& env, CheckTask const& checkTask, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression) { STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidPropertyException, "The game-based abstraction refinement model checker can only compute the result for the initial states."); @@ -430,7 +463,7 @@ namespace storm { auto abstractionStart = std::chrono::high_resolution_clock::now(); storm::abstraction::MenuGame game = abstractor->abstract(); auto abstractionEnd = std::chrono::high_resolution_clock::now(); - STORM_LOG_DEBUG("Abstraction in iteration " << iterations << " has " << game.getNumberOfStates() << " (player 1) states, " << game.getNumberOfTransitions() << " transitions, " << game.getBottomStates().getNonZeroCount() << " bottom states (computed in " << std::chrono::duration_cast(abstractionEnd - abstractionStart).count() << "ms)."); + STORM_LOG_DEBUG("Abstraction in iteration " << iterations << " has " << game.getNumberOfStates() << " player 1 states, " << game.getNumberOfPlayer2States() << " player 2 states, " << game.getNumberOfTransitions() << " transitions, " << game.getBottomStates().getNonZeroCount() << " bottom states (computed in " << std::chrono::duration_cast(abstractionEnd - abstractionStart).count() << "ms)."); // (2) Prepare initial, constraint and target state BDDs for later use. storm::dd::Bdd initialStates = game.getInitialStates(); @@ -517,7 +550,6 @@ namespace storm { // At this point, we know that we cannot answer the query without further numeric computation. STORM_LOG_TRACE("Starting numerical solution step."); - STORM_LOG_TRACE("Using dd-based solving."); storm::dd::Add initialStatesAdd = initialStates.template toAdd(); auto quantitativeStart = std::chrono::high_resolution_clock::now(); @@ -660,6 +692,57 @@ namespace storm { return std::make_unique>(storm::storage::sparse::state_type(0), ValueType(0.5)); } + // (4) if we arrived at this point and no refinement was made, we need to compute the quantitative solution. + if (!qualitativeRefinement) { + // At this point, we know that we cannot answer the query without further numeric computation. + STORM_LOG_TRACE("Starting numerical solution step."); + + auto quantitativeStart = std::chrono::high_resolution_clock::now(); + + ExplicitQuantitativeResultMinMax quantitativeResult; + quantitativeResult.setMin(computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Minimize, transitionMatrix, player1Groups, qualitativeResult, maybeMin, minStrategyPair)); + +// SymbolicQuantitativeGameResultMinMax quantitativeResult; +// +// // (7) Solve the min values and check whether we can give the answer already. +// quantitativeResult.min = computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Minimize, game, qualitativeResult, initialStatesAdd, maybeMin, reuseQuantitativeResults ? previousMinQuantitativeResult : boost::none); +// previousMinQuantitativeResult = quantitativeResult.min; +// result = checkForResultAfterQuantitativeCheck(checkTask, storm::OptimizationDirection::Minimize, quantitativeResult.min.getInitialStatesRange()); +// if (result) { +// return result; +// } +// +// // (8) Solve the max values and check whether we can give the answer already. +// quantitativeResult.max = computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Maximize, game, qualitativeResult, initialStatesAdd, maybeMax, boost::make_optional(quantitativeResult.min)); +// result = checkForResultAfterQuantitativeCheck(checkTask, storm::OptimizationDirection::Maximize, quantitativeResult.max.getInitialStatesRange()); +// if (result) { +// return result; +// } +// + auto quantitativeEnd = std::chrono::high_resolution_clock::now(); + STORM_LOG_DEBUG("Obtained quantitative bounds [" << quantitativeResult.getMin().getRange(initialStates).first << ", " << quantitativeResult.getMax().getRange(initialStates).second << "] on the actual value for the initial states in " << std::chrono::duration_cast(quantitativeEnd - quantitativeStart).count() << "ms."); +// +// // (9) Check whether the lower and upper bounds are close enough to terminate with an answer. +// result = checkForResultAfterQuantitativeCheck(quantitativeResult.min.getInitialStatesRange().first, quantitativeResult.max.getInitialStatesRange().second, comparator); +// if (result) { +// return result; +// } +// +// // Make sure that all strategies are still valid strategies. +// STORM_LOG_ASSERT(quantitativeResult.min.getPlayer1Strategy().isZero() || quantitativeResult.min.getPlayer1Strategy().template toAdd().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for min is illegal."); +// STORM_LOG_ASSERT(quantitativeResult.max.getPlayer1Strategy().isZero() || quantitativeResult.max.getPlayer1Strategy().template toAdd().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for max is illegal."); +// STORM_LOG_ASSERT(quantitativeResult.min.getPlayer2Strategy().isZero() || quantitativeResult.min.getPlayer2Strategy().template toAdd().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for min is illegal."); +// STORM_LOG_ASSERT(quantitativeResult.max.getPlayer2Strategy().isZero() || quantitativeResult.max.getPlayer2Strategy().template toAdd().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for max is illegal."); +// + auto quantitativeRefinementStart = std::chrono::high_resolution_clock::now(); +// +// // (10) If we arrived at this point, it means that we have all qualitative and quantitative +// // information about the game, but we could not yet answer the query. In this case, we need to refine. +// refiner.refine(game, transitionMatrixBdd, quantitativeResult); + auto quantitativeRefinementEnd = std::chrono::high_resolution_clock::now(); + STORM_LOG_DEBUG("Quantitative refinement completed in " << std::chrono::duration_cast(quantitativeRefinementEnd - quantitativeRefinementStart).count() << "ms."); + } + return nullptr; } diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h index a2f4e53f0..b54a510c8 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h @@ -39,6 +39,13 @@ namespace storm { class ExplicitQualitativeGameResult; class ExplicitQualitativeGameResultMinMax; + + template + class ExplicitQuantitativeResult; + + template + class ExplicitQuantitativeResultMinMax; + class ExplicitGameStrategy; class ExplicitGameStrategyPair; } diff --git a/src/storm/models/symbolic/StochasticTwoPlayerGame.cpp b/src/storm/models/symbolic/StochasticTwoPlayerGame.cpp index 677d80912..8695c57d8 100644 --- a/src/storm/models/symbolic/StochasticTwoPlayerGame.cpp +++ b/src/storm/models/symbolic/StochasticTwoPlayerGame.cpp @@ -100,6 +100,11 @@ namespace storm { } + template + uint64_t StochasticTwoPlayerGame::getNumberOfPlayer2States() const { + return this->getQualitativeTransitionMatrix().existsAbstract(this->getColumnVariables()).getNonZeroCount(); + } + // Explicitly instantiate the template class. template class StochasticTwoPlayerGame; template class StochasticTwoPlayerGame; diff --git a/src/storm/models/symbolic/StochasticTwoPlayerGame.h b/src/storm/models/symbolic/StochasticTwoPlayerGame.h index 569d258dd..1a243eff5 100644 --- a/src/storm/models/symbolic/StochasticTwoPlayerGame.h +++ b/src/storm/models/symbolic/StochasticTwoPlayerGame.h @@ -120,6 +120,11 @@ namespace storm { template std::shared_ptr> toValueType() const; + /*! + * Retrieves the number of player 2 states in the game. + */ + uint64_t getNumberOfPlayer2States() const; + private: /*! * Prepare all illegal masks.