From 48dc03846eeba4185ac7f42e1e926a41d6ab2dbe Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 29 Oct 2017 13:45:25 +0100 Subject: [PATCH] extended partial bisimulation model checker by games as quotients --- src/storm/abstraction/MenuGameRefiner.cpp | 16 +- src/storm/abstraction/QualitativeGameResult.h | 14 +- .../abstraction/QualitativeGameResultMinMax.h | 29 ++- src/storm/abstraction/QualitativeMdpResult.h | 16 +- .../abstraction/QualitativeMdpResultMinMax.h | 25 ++- src/storm/abstraction/QualitativeResult.cpp | 3 + src/storm/abstraction/QualitativeResult.h | 21 ++ .../abstraction/QualitativeResultMinMax.cpp | 32 +++ .../abstraction/QualitativeResultMinMax.h | 31 +++ .../abstraction/QuantitativeGameResult.h | 44 +++- .../modelchecker/AbstractModelChecker.cpp | 5 + .../abstraction/GameBasedMdpModelChecker.cpp | 31 ++- .../PartialBisimulationMdpModelChecker.cpp | 193 +++++++++++++++--- .../PartialBisimulationMdpModelChecker.h | 27 ++- .../SymbolicPropositionalModelChecker.cpp | 5 + src/storm/solver/SymbolicGameSolver.cpp | 7 + src/storm/solver/SymbolicGameSolver.h | 6 + .../dd/bisimulation/SignatureRefiner.cpp | 2 - src/storm/utility/solver.cpp | 9 +- src/storm/utility/solver.h | 6 - 20 files changed, 429 insertions(+), 93 deletions(-) create mode 100644 src/storm/abstraction/QualitativeResult.cpp create mode 100644 src/storm/abstraction/QualitativeResult.h create mode 100644 src/storm/abstraction/QualitativeResultMinMax.cpp create mode 100644 src/storm/abstraction/QualitativeResultMinMax.h diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index 9dc6de4d6..642cb83fb 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -133,10 +133,10 @@ namespace storm { maxPlayer1Strategy = qualitativeResult.get().prob1Max.getPlayer1Strategy(); maxPlayer2Strategy = qualitativeResult.get().prob1Max.getPlayer2Strategy(); } else if (quantitativeResult) { - minPlayer1Strategy = quantitativeResult.get().min.player1Strategy; - minPlayer2Strategy = quantitativeResult.get().min.player2Strategy; - maxPlayer1Strategy = quantitativeResult.get().max.player1Strategy; - maxPlayer2Strategy = quantitativeResult.get().max.player2Strategy; + minPlayer1Strategy = quantitativeResult.get().min.getPlayer1Strategy(); + minPlayer2Strategy = quantitativeResult.get().min.getPlayer2Strategy(); + maxPlayer1Strategy = quantitativeResult.get().max.getPlayer1Strategy(); + maxPlayer2Strategy = quantitativeResult.get().max.getPlayer2Strategy(); } else { STORM_LOG_ASSERT(false, "Either qualitative or quantitative result is required."); } @@ -619,10 +619,10 @@ namespace storm { bool MenuGameRefiner::refine(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, QuantitativeGameResultMinMax const& quantitativeResult) const { STORM_LOG_TRACE("Refining after quantitative check."); // Get all relevant strategies. - storm::dd::Bdd minPlayer1Strategy = quantitativeResult.min.player1Strategy; - storm::dd::Bdd minPlayer2Strategy = quantitativeResult.min.player2Strategy; - storm::dd::Bdd maxPlayer1Strategy = quantitativeResult.max.player1Strategy; - storm::dd::Bdd maxPlayer2Strategy = quantitativeResult.max.player2Strategy; + storm::dd::Bdd minPlayer1Strategy = quantitativeResult.min.getPlayer1Strategy(); + storm::dd::Bdd minPlayer2Strategy = quantitativeResult.min.getPlayer2Strategy(); + storm::dd::Bdd maxPlayer1Strategy = quantitativeResult.max.getPlayer1Strategy(); + storm::dd::Bdd maxPlayer2Strategy = quantitativeResult.max.getPlayer2Strategy(); // Compute all reached pivot states. PivotStateCandidatesResult pivotStateCandidatesResult = computePivotStates(game, transitionMatrixBdd, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy); diff --git a/src/storm/abstraction/QualitativeGameResult.h b/src/storm/abstraction/QualitativeGameResult.h index 2de6ef0ef..ff3c6e44c 100644 --- a/src/storm/abstraction/QualitativeGameResult.h +++ b/src/storm/abstraction/QualitativeGameResult.h @@ -1,12 +1,24 @@ #pragma once #include "storm/utility/graph.h" +#include "storm/abstraction/QualitativeResult.h" namespace storm { namespace abstraction { template - using QualitativeGameResult = storm::utility::graph::GameProb01Result; + struct QualitativeGameResult : public storm::utility::graph::GameProb01Result, public QualitativeResult { + QualitativeGameResult() = default; + + QualitativeGameResult(storm::utility::graph::GameProb01Result const& prob01Result) : storm::utility::graph::GameProb01Result(prob01Result) { + // Intentionally left empty. + } + + virtual storm::dd::Bdd const& getStates() const override { + return this->getPlayer1States(); + } + + }; } } diff --git a/src/storm/abstraction/QualitativeGameResultMinMax.h b/src/storm/abstraction/QualitativeGameResultMinMax.h index c028b9ddb..39d139767 100644 --- a/src/storm/abstraction/QualitativeGameResultMinMax.h +++ b/src/storm/abstraction/QualitativeGameResultMinMax.h @@ -2,20 +2,37 @@ #include "storm/storage/dd/DdType.h" -#include "storm/utility/graph.h" +#include "storm/abstraction/QualitativeResultMinMax.h" +#include "storm/abstraction/QualitativeGameResult.h" namespace storm { namespace abstraction { template - struct QualitativeGameResultMinMax { + struct QualitativeGameResultMinMax : public QualitativeResultMinMax { public: QualitativeGameResultMinMax() = default; - storm::utility::graph::GameProb01Result prob0Min; - storm::utility::graph::GameProb01Result prob1Min; - storm::utility::graph::GameProb01Result prob0Max; - storm::utility::graph::GameProb01Result prob1Max; + virtual QualitativeResult const& getProb0(storm::OptimizationDirection const& dir) const override { + if (dir == storm::OptimizationDirection::Minimize) { + return prob0Min; + } else { + return prob0Max; + } + } + + virtual QualitativeResult const& getProb1(storm::OptimizationDirection const& dir) const override { + if (dir == storm::OptimizationDirection::Minimize) { + return prob1Min; + } else { + return prob1Max; + } + } + + QualitativeGameResult prob0Min; + QualitativeGameResult prob1Min; + QualitativeGameResult prob0Max; + QualitativeGameResult prob1Max; }; } diff --git a/src/storm/abstraction/QualitativeMdpResult.h b/src/storm/abstraction/QualitativeMdpResult.h index ce97bd1e2..9fc1fcc0e 100644 --- a/src/storm/abstraction/QualitativeMdpResult.h +++ b/src/storm/abstraction/QualitativeMdpResult.h @@ -1,12 +1,24 @@ #pragma once -#include "storm/utility/graph.h" +#include "storm/abstraction/QualitativeResult.h" namespace storm { namespace abstraction { template - using QualitativeMdpResult = std::pair, storm::dd::Bdd>; + struct QualitativeMdpResult : public QualitativeResult { + QualitativeMdpResult() = default; + + QualitativeMdpResult(storm::dd::Bdd const& states) : states(states) { + // Intentionally left empty. + } + + virtual storm::dd::Bdd const& getStates() const override { + return states; + } + + storm::dd::Bdd states; + }; } } diff --git a/src/storm/abstraction/QualitativeMdpResultMinMax.h b/src/storm/abstraction/QualitativeMdpResultMinMax.h index b701167b2..3c1979afc 100644 --- a/src/storm/abstraction/QualitativeMdpResultMinMax.h +++ b/src/storm/abstraction/QualitativeMdpResultMinMax.h @@ -2,18 +2,37 @@ #include "storm/storage/dd/DdType.h" +#include "storm/abstraction/QualitativeResultMinMax.h" #include "storm/abstraction/QualitativeMdpResult.h" namespace storm { namespace abstraction { template - struct QualitativeMdpResultMinMax { + struct QualitativeMdpResultMinMax : public QualitativeResultMinMax { public: QualitativeMdpResultMinMax() = default; - QualitativeMdpResult min; - QualitativeMdpResult max; + virtual QualitativeResult const& getProb0(storm::OptimizationDirection const& dir) const override { + if (dir == storm::OptimizationDirection::Minimize) { + return prob0Min; + } else { + return prob0Max; + } + } + + virtual QualitativeResult const& getProb1(storm::OptimizationDirection const& dir) const override { + if (dir == storm::OptimizationDirection::Minimize) { + return prob1Min; + } else { + return prob1Max; + } + } + + QualitativeMdpResult prob0Min; + QualitativeMdpResult prob1Min; + QualitativeMdpResult prob0Max; + QualitativeMdpResult prob1Max; }; } diff --git a/src/storm/abstraction/QualitativeResult.cpp b/src/storm/abstraction/QualitativeResult.cpp new file mode 100644 index 000000000..68a50d1e5 --- /dev/null +++ b/src/storm/abstraction/QualitativeResult.cpp @@ -0,0 +1,3 @@ +#include "storm/abstraction/QualitativeResult.h" + + diff --git a/src/storm/abstraction/QualitativeResult.h b/src/storm/abstraction/QualitativeResult.h new file mode 100644 index 000000000..49f4b29ad --- /dev/null +++ b/src/storm/abstraction/QualitativeResult.h @@ -0,0 +1,21 @@ +#pragma once + +#include "storm/storage/dd/DdType.h" + +namespace storm { + namespace dd { + template + class Bdd; + } + + namespace abstraction { + + template + struct QualitativeResult { + virtual storm::dd::Bdd const& getStates() const = 0; + }; + + } +} + + diff --git a/src/storm/abstraction/QualitativeResultMinMax.cpp b/src/storm/abstraction/QualitativeResultMinMax.cpp new file mode 100644 index 000000000..4bda4dc50 --- /dev/null +++ b/src/storm/abstraction/QualitativeResultMinMax.cpp @@ -0,0 +1,32 @@ +#include "storm/abstraction/QualitativeResultMinMax.h" + +#include "storm/abstraction/QualitativeResult.h" + +namespace storm { + namespace abstraction { + + template + QualitativeResult const& QualitativeResultMinMax::getProb0Min() const { + return getProb0(storm::OptimizationDirection::Minimize); + } + + template + QualitativeResult const& QualitativeResultMinMax::getProb1Min() const { + return getProb1(storm::OptimizationDirection::Minimize); + } + + template + QualitativeResult const& QualitativeResultMinMax::getProb0Max() const { + return getProb0(storm::OptimizationDirection::Maximize); + } + + template + QualitativeResult const& QualitativeResultMinMax::getProb1Max() const { + return getProb1(storm::OptimizationDirection::Maximize); + } + + template struct QualitativeResultMinMax; + template struct QualitativeResultMinMax; + + } +} diff --git a/src/storm/abstraction/QualitativeResultMinMax.h b/src/storm/abstraction/QualitativeResultMinMax.h new file mode 100644 index 000000000..5375f5880 --- /dev/null +++ b/src/storm/abstraction/QualitativeResultMinMax.h @@ -0,0 +1,31 @@ +#pragma once + +#include "storm/solver/OptimizationDirection.h" + +#include "storm/storage/dd/DdType.h" + +namespace storm { + namespace dd { + template + class Bdd; + } + + namespace abstraction { + template + struct QualitativeResult; + + template + struct QualitativeResultMinMax { + public: + QualitativeResultMinMax() = default; + + QualitativeResult const& getProb0Min() const; + QualitativeResult const& getProb1Min() const; + QualitativeResult const& getProb0Max() const; + QualitativeResult const& getProb1Max() const; + + virtual QualitativeResult const& getProb0(storm::OptimizationDirection const& dir) const = 0; + virtual QualitativeResult const& getProb1(storm::OptimizationDirection const& dir) const = 0; + }; + } +} diff --git a/src/storm/abstraction/QuantitativeGameResult.h b/src/storm/abstraction/QuantitativeGameResult.h index accfcb499..2d76a8618 100644 --- a/src/storm/abstraction/QuantitativeGameResult.h +++ b/src/storm/abstraction/QuantitativeGameResult.h @@ -10,15 +10,51 @@ namespace storm { template struct QuantitativeGameResult { QuantitativeGameResult() = default; + + QuantitativeGameResult(storm::dd::Add const& values) : values(values) { + // Intentionally left empty. + } - QuantitativeGameResult(std::pair initialStatesRange, storm::dd::Add const& values, storm::dd::Bdd const& player1Strategy, storm::dd::Bdd const& player2Strategy) : initialStatesRange(initialStatesRange), values(values), player1Strategy(player1Strategy), player2Strategy(player2Strategy) { + QuantitativeGameResult(boost::optional> const& initialStatesRange, storm::dd::Add const& values, boost::optional> const& player1Strategy, boost::optional> const& player2Strategy) : initialStatesRange(initialStatesRange), values(values), player1Strategy(player1Strategy), player2Strategy(player2Strategy) { // Intentionally left empty. } - std::pair initialStatesRange; + bool hasPlayer1Strategy() const { + return static_cast(player1Strategy); + } + + storm::dd::Bdd const& getPlayer1Strategy() const { + return player1Strategy.get(); + } + + storm::dd::Bdd& getPlayer1Strategy() { + return player1Strategy.get(); + } + + bool hasPlayer2Strategy() const { + return static_cast(player2Strategy); + } + + storm::dd::Bdd const& getPlayer2Strategy() const { + return player2Strategy.get(); + } + + storm::dd::Bdd& getPlayer2Strategy() { + return player2Strategy.get(); + } + + bool hasInitialStatesRange() const { + return static_cast(initialStatesRange); + } + + std::pair const& getInitialStatesRange() const { + return initialStatesRange.get(); + } + + boost::optional> initialStatesRange; storm::dd::Add values; - storm::dd::Bdd player1Strategy; - storm::dd::Bdd player2Strategy; + boost::optional> player1Strategy; + boost::optional> player2Strategy; }; } diff --git a/src/storm/modelchecker/AbstractModelChecker.cpp b/src/storm/modelchecker/AbstractModelChecker.cpp index 1a12a89b7..69693bee2 100644 --- a/src/storm/modelchecker/AbstractModelChecker.cpp +++ b/src/storm/modelchecker/AbstractModelChecker.cpp @@ -15,6 +15,7 @@ #include "storm/models/symbolic/Dtmc.h" #include "storm/models/symbolic/Ctmc.h" #include "storm/models/symbolic/Mdp.h" +#include "storm/models/symbolic/StochasticTwoPlayerGame.h" #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/models/symbolic/StandardRewardModel.h" @@ -330,5 +331,9 @@ namespace storm { template class AbstractModelChecker>; template class AbstractModelChecker>; template class AbstractModelChecker>; + template class AbstractModelChecker>; + template class AbstractModelChecker>; + template class AbstractModelChecker>; + template class AbstractModelChecker>; } } diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 7574aea14..516b0dc1a 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -34,7 +34,6 @@ #include "storm/settings/modules/CoreSettings.h" #include "storm/settings/modules/AbstractionSettings.h" -#include "storm/utility/solver.h" #include "storm/utility/prism.h" #include "storm/utility/macros.h" @@ -257,10 +256,10 @@ namespace storm { } // Create the solver and solve the equation system. - storm::utility::solver::SymbolicGameSolverFactory solverFactory; + storm::solver::SymbolicGameSolverFactory solverFactory; std::unique_ptr> solver = solverFactory.create(submatrix, maybeStates, game.getIllegalPlayer1Mask(), game.getIllegalPlayer2Mask(), game.getRowVariables(), game.getColumnVariables(), game.getRowColumnMetaVariablePairs(), game.getPlayer1Variables(), game.getPlayer2Variables()); solver->setGeneratePlayersStrategies(true); - auto values = solver->solveGame(player1Direction, player2Direction, startVector, subvector, startInfo ? boost::make_optional(startInfo.get().player1Strategy) : boost::none, startInfo ? boost::make_optional(startInfo.get().player2Strategy) : boost::none); + auto values = solver->solveGame(player1Direction, player2Direction, startVector, subvector, startInfo ? boost::make_optional(startInfo.get().getPlayer1Strategy()) : boost::none, startInfo ? boost::make_optional(startInfo.get().getPlayer2Strategy()) : boost::none); return QuantitativeGameResult(std::make_pair(storm::utility::zero(), storm::utility::one()), values, solver->getPlayer1Strategy(), solver->getPlayer2Strategy()); } @@ -294,8 +293,8 @@ namespace storm { result = solveMaybeStates(player1Direction, player2Direction, game, maybeStates, min ? qualitativeResult.prob1Min.getPlayer1States() : qualitativeResult.prob1Max.getPlayer1States(), startInfo); // Cut the obtained strategies to the reachable states of the game. - result.player1Strategy &= game.getReachableStates(); - result.player2Strategy &= game.getReachableStates(); + result.getPlayer1Strategy() &= game.getReachableStates(); + result.getPlayer2Strategy() &= game.getReachableStates(); // Extend the values of the maybe states by the qualitative values. result.values += min ? qualitativeResult.prob1Min.getPlayer1States().template toAdd() : qualitativeResult.prob1Max.getPlayer1States().template toAdd(); @@ -315,11 +314,11 @@ namespace storm { result.initialStatesRange = std::make_pair(minValueOverInitialStates, maxValueOverInitialStates); - result.player1Strategy = combinedPlayer1QualitativeStrategies.existsAbstract(game.getPlayer1Variables()).ite(combinedPlayer1QualitativeStrategies, result.player1Strategy); - result.player2Strategy = combinedPlayer2QualitativeStrategies.existsAbstract(game.getPlayer2Variables()).ite(combinedPlayer2QualitativeStrategies, result.player2Strategy); + result.player1Strategy = combinedPlayer1QualitativeStrategies.existsAbstract(game.getPlayer1Variables()).ite(combinedPlayer1QualitativeStrategies, result.getPlayer1Strategy()); + result.player2Strategy = combinedPlayer2QualitativeStrategies.existsAbstract(game.getPlayer2Variables()).ite(combinedPlayer2QualitativeStrategies, result.getPlayer2Strategy()); auto end = std::chrono::high_resolution_clock::now(); - STORM_LOG_TRACE("Obtained quantitative " << (min ? "lower" : "upper") << " bound " << (min ? result.initialStatesRange.first : result.initialStatesRange.second) << " in " << std::chrono::duration_cast(end - start).count() << "ms."); + STORM_LOG_TRACE("Obtained quantitative " << (min ? "lower" : "upper") << " bound " << (min ? result.getInitialStatesRange().first : result.getInitialStatesRange().second) << " in " << std::chrono::duration_cast(end - start).count() << "ms."); return result; } @@ -431,7 +430,7 @@ namespace storm { // (7) Solve the min values and check whether we can give the answer already. quantitativeResult.min = computeQuantitativeResult(player1Direction, storm::OptimizationDirection::Minimize, game, qualitativeResult, initialStatesAdd, maybeMin, reuseQuantitativeResults ? previousMinQuantitativeResult : boost::none); previousMinQuantitativeResult = quantitativeResult.min; - result = checkForResultAfterQuantitativeCheck(checkTask, storm::OptimizationDirection::Minimize, quantitativeResult.min.initialStatesRange); + result = checkForResultAfterQuantitativeCheck(checkTask, storm::OptimizationDirection::Minimize, quantitativeResult.min.getInitialStatesRange()); if (result) { printStatistics(*abstractor, game); return result; @@ -439,27 +438,27 @@ namespace storm { // (8) Solve the max values and check whether we can give the answer already. quantitativeResult.max = computeQuantitativeResult(player1Direction, storm::OptimizationDirection::Maximize, game, qualitativeResult, initialStatesAdd, maybeMax, boost::make_optional(quantitativeResult.min)); - result = checkForResultAfterQuantitativeCheck(checkTask, storm::OptimizationDirection::Maximize, quantitativeResult.max.initialStatesRange); + result = checkForResultAfterQuantitativeCheck(checkTask, storm::OptimizationDirection::Maximize, quantitativeResult.max.getInitialStatesRange()); if (result) { printStatistics(*abstractor, game); return result; } auto quantitativeEnd = std::chrono::high_resolution_clock::now(); - STORM_LOG_DEBUG("Obtained quantitative bounds [" << quantitativeResult.min.initialStatesRange.first << ", " << quantitativeResult.max.initialStatesRange.second << "] on the actual value for the initial states in " << std::chrono::duration_cast(quantitativeEnd - quantitativeStart).count() << "ms."); + STORM_LOG_DEBUG("Obtained quantitative bounds [" << quantitativeResult.min.getInitialStatesRange().first << ", " << quantitativeResult.max.getInitialStatesRange().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.initialStatesRange.first, quantitativeResult.max.initialStatesRange.second, comparator); + result = checkForResultAfterQuantitativeCheck(quantitativeResult.min.getInitialStatesRange().first, quantitativeResult.max.getInitialStatesRange().second, comparator); if (result) { printStatistics(*abstractor, game); return result; } // Make sure that all strategies are still valid strategies. - STORM_LOG_ASSERT(quantitativeResult.min.player1Strategy.isZero() || quantitativeResult.min.player1Strategy.template toAdd().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for min is illegal."); - STORM_LOG_ASSERT(quantitativeResult.max.player1Strategy.isZero() || quantitativeResult.max.player1Strategy.template toAdd().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for max is illegal."); - STORM_LOG_ASSERT(quantitativeResult.min.player2Strategy.isZero() || quantitativeResult.min.player2Strategy.template toAdd().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for min is illegal."); - STORM_LOG_ASSERT(quantitativeResult.max.player2Strategy.isZero() || quantitativeResult.max.player2Strategy.template toAdd().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for max is illegal."); + 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 diff --git a/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp index bd7f8c100..3a2686398 100644 --- a/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp @@ -18,10 +18,14 @@ #include "storm/storage/dd/BisimulationDecomposition.h" #include "storm/abstraction/QualitativeMdpResultMinMax.h" +#include "storm/abstraction/QualitativeGameResultMinMax.h" +#include "storm/abstraction/QuantitativeGameResult.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/AbstractionSettings.h" +#include "storm/solver/SymbolicGameSolver.h" + #include "storm/utility/macros.h" #include "storm/exceptions/NotSupportedException.h" #include "storm/exceptions/InvalidPropertyException.h" @@ -119,7 +123,7 @@ namespace storm { if (!converged) { STORM_LOG_TRACE("Performing bisimulation step."); - bisimulation.compute(10); + bisimulation.compute(1); } } @@ -184,7 +188,10 @@ namespace storm { } template - bool PartialBisimulationMdpModelChecker::boundsSufficient(storm::models::Model const& quotient, bool lowerBounds, QuantitativeCheckResult const& result, storm::logic::ComparisonType comparisonType, ValueType const& threshold) { + bool PartialBisimulationMdpModelChecker::checkForResult(storm::models::Model const& quotient, bool lowerBounds, QuantitativeCheckResult const& result, CheckTask const& checkTask) { + storm::logic::ComparisonType comparisonType = checkTask.getBoundComparisonType(); + ValueType threshold = checkTask.getBoundThreshold(); + if (lowerBounds) { if (storm::logic::isLowerBound(comparisonType)) { ValueType minimalLowerBound = getExtremalBound(storm::OptimizationDirection::Minimize, result); @@ -222,10 +229,11 @@ namespace storm { } template - std::pair::DdType>, storm::dd::Bdd::DdType>> PartialBisimulationMdpModelChecker::getConstraintAndTargetStates(storm::models::symbolic::Mdp const& quotient, CheckTask const& checkTask) { + template + std::pair::DdType>, storm::dd::Bdd::DdType>> PartialBisimulationMdpModelChecker::getConstraintAndTargetStates(QuotientModelType const& quotient, CheckTask const& checkTask) { std::pair, storm::dd::Bdd> result; - SymbolicPropositionalModelChecker> checker(quotient); + SymbolicPropositionalModelChecker checker(quotient); if (checkTask.getFormula().isUntilFormula()) { std::unique_ptr subresult = checker.check(checkTask.getFormula().asUntilFormula().getLeftSubformula()); result.first = subresult->asSymbolicQualitativeCheckResult().getTruthValuesVector(); @@ -246,18 +254,24 @@ namespace storm { template storm::abstraction::QualitativeMdpResultMinMax::DdType> PartialBisimulationMdpModelChecker::computeQualitativeResult(storm::models::symbolic::Mdp const& quotient, CheckTask const& checkTask, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates) { - STORM_LOG_DEBUG("Computing qualitative solution."); + STORM_LOG_DEBUG("Computing qualitative solution for quotient MDP."); storm::abstraction::QualitativeMdpResultMinMax result; auto start = std::chrono::high_resolution_clock::now(); bool isRewardFormula = checkTask.getFormula().isEventuallyFormula() && checkTask.getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward; storm::dd::Bdd transitionMatrixBdd = quotient.getTransitionMatrix().notZero(); if (isRewardFormula) { - result.min.second = storm::utility::graph::performProb1E(quotient, transitionMatrixBdd, constraintStates, targetStates, storm::utility::graph::performProbGreater0E(quotient, transitionMatrixBdd, constraintStates, targetStates)); - result.max.second = storm::utility::graph::performProb1A(quotient, transitionMatrixBdd, targetStates, storm::utility::graph::performProbGreater0A(quotient, transitionMatrixBdd, constraintStates, targetStates)); + auto prob1 = storm::utility::graph::performProb1E(quotient, transitionMatrixBdd, constraintStates, targetStates, storm::utility::graph::performProbGreater0E(quotient, transitionMatrixBdd, constraintStates, targetStates)); + result.prob1Min = storm::abstraction::QualitativeMdpResult(prob1); + prob1 = storm::utility::graph::performProb1A(quotient, transitionMatrixBdd, targetStates, storm::utility::graph::performProbGreater0A(quotient, transitionMatrixBdd, constraintStates, targetStates)); + result.prob1Max = storm::abstraction::QualitativeMdpResult(prob1); } else { - result.min = storm::utility::graph::performProb01Min(quotient, transitionMatrixBdd, constraintStates, targetStates); - result.max = storm::utility::graph::performProb01Max(quotient, transitionMatrixBdd, constraintStates, targetStates); + auto prob01 = storm::utility::graph::performProb01Min(quotient, transitionMatrixBdd, constraintStates, targetStates); + result.prob0Min = storm::abstraction::QualitativeMdpResult(prob01.first); + result.prob1Min = storm::abstraction::QualitativeMdpResult(prob01.second); + prob01 = storm::utility::graph::performProb01Max(quotient, transitionMatrixBdd, constraintStates, targetStates); + result.prob0Max = storm::abstraction::QualitativeMdpResult(prob01.first); + result.prob1Max = storm::abstraction::QualitativeMdpResult(prob01.second); } auto end = std::chrono::high_resolution_clock::now(); @@ -266,25 +280,57 @@ namespace storm { return result; } - + template - std::unique_ptr PartialBisimulationMdpModelChecker::checkForResult(storm::models::symbolic::Mdp const& quotient, storm::abstraction::QualitativeMdpResultMinMax const& qualitativeResults, CheckTask const& checkTask) { + storm::abstraction::QualitativeGameResultMinMax::DdType> PartialBisimulationMdpModelChecker::computeQualitativeResult(storm::models::symbolic::StochasticTwoPlayerGame const& quotient, CheckTask const& checkTask, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, storm::OptimizationDirection optimizationDirectionInModel) { + + STORM_LOG_DEBUG("Computing qualitative solution for quotient game."); + storm::abstraction::QualitativeGameResultMinMax result; + + auto start = std::chrono::high_resolution_clock::now(); + bool isRewardFormula = checkTask.getFormula().isEventuallyFormula() && checkTask.getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward; + storm::dd::Bdd transitionMatrixBdd = quotient.getTransitionMatrix().notZero(); + if (isRewardFormula) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Rewards are currently not supported for quotient stochastic games."); + } else { + result.prob0Min = storm::utility::graph::performProb0(quotient, quotient.getQualitativeTransitionMatrix(), constraintStates, targetStates, storm::OptimizationDirection::Minimize, optimizationDirectionInModel); + result.prob1Min = storm::utility::graph::performProb1(quotient, quotient.getQualitativeTransitionMatrix(), constraintStates, targetStates, storm::OptimizationDirection::Minimize, optimizationDirectionInModel); + result.prob0Max = storm::utility::graph::performProb0(quotient, quotient.getQualitativeTransitionMatrix(), constraintStates, targetStates, storm::OptimizationDirection::Maximize, optimizationDirectionInModel); + result.prob1Max = storm::utility::graph::performProb1(quotient, quotient.getQualitativeTransitionMatrix(), constraintStates, targetStates, storm::OptimizationDirection::Maximize, optimizationDirectionInModel); + } + auto end = std::chrono::high_resolution_clock::now(); + + auto timeInMilliseconds = std::chrono::duration_cast(end - start).count(); + STORM_LOG_DEBUG("Computed qualitative solution in " << timeInMilliseconds << "ms."); + + return result; + } + + template + std::unique_ptr PartialBisimulationMdpModelChecker::checkForResult(storm::models::symbolic::Model const& quotient, storm::abstraction::QualitativeResultMinMax const& qualitativeResults, CheckTask const& checkTask) { std::unique_ptr result; bool isRewardFormula = checkTask.getFormula().isEventuallyFormula() && checkTask.getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward; if (isRewardFormula) { // In the reachability reward case, we can give an answer if all initial states of the system are infinity // states in the min result. - if ((quotient.getInitialStates() && !qualitativeResults.min.second) == quotient.getInitialStates()) { + if ((quotient.getInitialStates() && !qualitativeResults.getProb1Min().getStates()) == quotient.getInitialStates()) { result = std::make_unique>(quotient.getReachableStates(), quotient.getInitialStates(), quotient.getInitialStates().ite(quotient.getManager().getConstant(storm::utility::infinity()), quotient.getManager().template getAddZero())); } } else { // In the reachability probability case, we can give the answer if all initial states are prob1 states // in the min result or if all initial states are prob0 in the max case. - if ((quotient.getInitialStates() && qualitativeResults.min.second) == quotient.getInitialStates()) { + // Furthermore, we can give the answer if there are initial states with probability > 0 in the min case + // and the probability bound was 0 or if there are initial states with probability < 1 in the max case + // and the probability bound was 1. + if ((quotient.getInitialStates() && qualitativeResults.getProb1Min().getStates()) == quotient.getInitialStates()) { result = std::make_unique>(quotient.getReachableStates(), quotient.getInitialStates(), quotient.getManager().template getAddOne()); - } else if ((quotient.getInitialStates() && qualitativeResults.max.first) == quotient.getInitialStates()) { + } else if ((quotient.getInitialStates() && qualitativeResults.getProb0Max().getStates()) == quotient.getInitialStates()) { result = std::make_unique>(quotient.getReachableStates(), quotient.getInitialStates(), quotient.getManager().template getAddZero()); + } else if (checkTask.isBoundSet() && checkTask.getBoundThreshold() == storm::utility::zero() && (quotient.getInitialStates() && qualitativeResults.getProb0Min().getStates()) != quotient.getInitialStates()) { + result = std::make_unique>(quotient.getReachableStates(), quotient.getInitialStates(), (quotient.getInitialStates() && qualitativeResults.getProb0Min().getStates()).ite(quotient.getManager().template getConstant(0.5), quotient.getManager().template getAddZero())); + } else if (checkTask.isBoundSet() && checkTask.getBoundThreshold() == storm::utility::one() && (quotient.getInitialStates() && qualitativeResults.getProb1Max().getStates()) != quotient.getInitialStates()) { + result = std::make_unique>(quotient.getReachableStates(), quotient.getInitialStates(), (quotient.getInitialStates() && qualitativeResults.getProb1Max().getStates()).ite(quotient.getManager().template getConstant(0.5), quotient.getManager().template getAddZero()) + qualitativeResults.getProb1Max().getStates().template toAdd()); } } @@ -292,17 +338,17 @@ namespace storm { } template - bool PartialBisimulationMdpModelChecker::skipQuantitativeSolution(storm::models::symbolic::Mdp const& quotient, storm::abstraction::QualitativeMdpResultMinMax const& qualitativeResults, CheckTask const& checkTask) { + bool PartialBisimulationMdpModelChecker::skipQuantitativeSolution(storm::models::symbolic::Model const& quotient, storm::abstraction::QualitativeResultMinMax const& qualitativeResults, CheckTask const& checkTask) { bool isRewardFormula = checkTask.getFormula().isEventuallyFormula() && checkTask.getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward; if (isRewardFormula) { - if ((quotient.getInitialStates() && qualitativeResults.min.second) != (quotient.getInitialStates() && qualitativeResults.max.second)) { + if ((quotient.getInitialStates() && qualitativeResults.getProb1Min().getStates()) != (quotient.getInitialStates() && qualitativeResults.getProb1Max().getStates())) { return true; } } else { - if ((quotient.getInitialStates() && qualitativeResults.min.first) != (quotient.getInitialStates() && qualitativeResults.max.first)) { + if ((quotient.getInitialStates() && qualitativeResults.getProb0Min().getStates()) != (quotient.getInitialStates() && qualitativeResults.getProb0Max().getStates())) { return true; - } else if ((quotient.getInitialStates() && qualitativeResults.min.second) != (quotient.getInitialStates() && qualitativeResults.max.second)) { + } else if ((quotient.getInitialStates() && qualitativeResults.getProb1Min().getStates()) != (quotient.getInitialStates() && qualitativeResults.getProb1Max().getStates())) { return true; } } @@ -310,31 +356,75 @@ namespace storm { } template - std::pair, std::unique_ptr> PartialBisimulationMdpModelChecker::computeQuantitativeResult(storm::models::symbolic::Mdp const& quotient, CheckTask const& checkTask, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, storm::abstraction::QualitativeMdpResultMinMax const& qualitativeResults) { + std::pair, std::unique_ptr> PartialBisimulationMdpModelChecker::computeQuantitativeResult(storm::models::symbolic::Mdp const& quotient, CheckTask const& checkTask, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, storm::abstraction::QualitativeResultMinMax const& qualitativeResults) { std::pair, std::unique_ptr> result; bool isRewardFormula = checkTask.getFormula().isEventuallyFormula() && checkTask.getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward; if (isRewardFormula) { - storm::dd::Bdd maybeMin = qualitativeResults.min.second && quotient.getReachableStates(); - result.first = storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeReachabilityRewards(storm::OptimizationDirection::Minimize, quotient, quotient.getTransitionMatrix(), quotient.getTransitionMatrix().notZero(), checkTask.isRewardModelSet() ? quotient.getRewardModel(checkTask.getRewardModel()) : quotient.getRewardModel(""), maybeMin, targetStates, !qualitativeResults.min.second && quotient.getReachableStates(), storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory(), quotient.getManager().template getAddZero()); + storm::dd::Bdd maybeMin = qualitativeResults.getProb1Min().getStates() && quotient.getReachableStates(); + result.first = storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeReachabilityRewards(storm::OptimizationDirection::Minimize, quotient, quotient.getTransitionMatrix(), quotient.getTransitionMatrix().notZero(), checkTask.isRewardModelSet() ? quotient.getRewardModel(checkTask.getRewardModel()) : quotient.getRewardModel(""), maybeMin, targetStates, !qualitativeResults.getProb1Min().getStates() && quotient.getReachableStates(), storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory(), quotient.getManager().template getAddZero()); - storm::dd::Bdd maybeMax = qualitativeResults.max.second && quotient.getReachableStates(); - result.second = storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeReachabilityRewards(storm::OptimizationDirection::Maximize, quotient, quotient.getTransitionMatrix(), quotient.getTransitionMatrix().notZero(), checkTask.isRewardModelSet() ? quotient.getRewardModel(checkTask.getRewardModel()) : quotient.getRewardModel(""), maybeMin, targetStates, !qualitativeResults.min.second && quotient.getReachableStates(), storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory(), maybeMax.ite(result.first->asSymbolicQuantitativeCheckResult().getValueVector(), quotient.getManager().template getAddZero())); + storm::dd::Bdd maybeMax = qualitativeResults.getProb1Max().getStates() && quotient.getReachableStates(); + result.second = storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeReachabilityRewards(storm::OptimizationDirection::Maximize, quotient, quotient.getTransitionMatrix(), quotient.getTransitionMatrix().notZero(), checkTask.isRewardModelSet() ? quotient.getRewardModel(checkTask.getRewardModel()) : quotient.getRewardModel(""), maybeMin, targetStates, !qualitativeResults.getProb1Max().getStates() && quotient.getReachableStates(), storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory(), maybeMax.ite(result.first->asSymbolicQuantitativeCheckResult().getValueVector(), quotient.getManager().template getAddZero())); } else { - storm::dd::Bdd maybeMin = !(qualitativeResults.min.first || qualitativeResults.min.second) && quotient.getReachableStates(); - result.first = storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeUntilProbabilities(storm::OptimizationDirection::Minimize, quotient, quotient.getTransitionMatrix(), maybeMin, qualitativeResults.min.second, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory(), quotient.getManager().template getAddZero()); + storm::dd::Bdd maybeMin = !(qualitativeResults.getProb0Min().getStates() || qualitativeResults.getProb1Min().getStates()) && quotient.getReachableStates(); + result.first = storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeUntilProbabilities(storm::OptimizationDirection::Minimize, quotient, quotient.getTransitionMatrix(), maybeMin, qualitativeResults.getProb1Min().getStates(), storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory(), quotient.getManager().template getAddZero()); - storm::dd::Bdd maybeMax = !(qualitativeResults.max.first || qualitativeResults.max.second) && quotient.getReachableStates(); - result.second = storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeUntilProbabilities(storm::OptimizationDirection::Maximize, quotient, quotient.getTransitionMatrix(), maybeMax, qualitativeResults.max.second, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory(), maybeMax.ite(result.first->asSymbolicQuantitativeCheckResult().getValueVector(), quotient.getManager().template getAddZero())); + storm::dd::Bdd maybeMax = !(qualitativeResults.getProb0Max().getStates() || qualitativeResults.getProb1Max().getStates()) && quotient.getReachableStates(); + result.second = storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeUntilProbabilities(storm::OptimizationDirection::Maximize, quotient, quotient.getTransitionMatrix(), maybeMax, qualitativeResults.getProb1Max().getStates(), storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory(), maybeMax.ite(result.first->asSymbolicQuantitativeCheckResult().getValueVector(), quotient.getManager().template getAddZero())); } return result; } + + template + std::unique_ptr computeReachabilityProbabilitiesHelper(storm::models::symbolic::StochasticTwoPlayerGame const& quotient, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::dd::Bdd const& maybeStates, storm::dd::Bdd const& prob1States) { + + STORM_LOG_TRACE("Performing quantative solution step. Player 1: " << player1Direction << ", player 2: " << player2Direction << "."); + + // Compute the ingredients of the equation system. + storm::dd::Add maybeStatesAdd = maybeStates.template toAdd(); + storm::dd::Add submatrix = maybeStatesAdd * quotient.getTransitionMatrix(); + storm::dd::Add prob1StatesAsColumn = prob1States.template toAdd().swapVariables(quotient.getRowColumnMetaVariablePairs()); + storm::dd::Add subvector = submatrix * prob1StatesAsColumn; + subvector = subvector.sumAbstract(quotient.getColumnVariables()); + + // Cut away all columns targeting non-maybe states. + submatrix *= maybeStatesAdd.swapVariables(quotient.getRowColumnMetaVariablePairs()); + + // Cut the starting vector to the maybe states of this query. + storm::dd::Add startVector = quotient.getManager().template getAddZero(); + + // Create the solver and solve the equation system. + storm::solver::SymbolicGameSolverFactory solverFactory; + std::unique_ptr> solver = solverFactory.create(submatrix, maybeStates, quotient.getIllegalPlayer1Mask(), quotient.getIllegalPlayer2Mask(), quotient.getRowVariables(), quotient.getColumnVariables(), quotient.getRowColumnMetaVariablePairs(), quotient.getPlayer1Variables(), quotient.getPlayer2Variables()); + auto values = solver->solveGame(player1Direction, player2Direction, startVector, subvector); + + return std::make_unique>(quotient.getReachableStates(), prob1States.template toAdd() + values); + } template - std::pair, std::unique_ptr> PartialBisimulationMdpModelChecker::computeBoundsPartialQuotient(storm::models::symbolic::Mdp const& quotient, CheckTask const& checkTask) { + std::pair, std::unique_ptr> PartialBisimulationMdpModelChecker::computeQuantitativeResult(storm::models::symbolic::StochasticTwoPlayerGame const& quotient, CheckTask const& checkTask, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, storm::abstraction::QualitativeResultMinMax const& qualitativeResults) { + + std::pair, std::unique_ptr> result; + + bool isRewardFormula = checkTask.getFormula().isEventuallyFormula() && checkTask.getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward; + if (isRewardFormula) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Computing rewards for stochastic games is currently unsupported."); + } else { + storm::dd::Bdd maybeMin = !(qualitativeResults.getProb0Min().getStates() || qualitativeResults.getProb1Min().getStates()) && quotient.getReachableStates(); + result.first = computeReachabilityProbabilitiesHelper(quotient, storm::OptimizationDirection::Minimize, checkTask.getOptimizationDirection(), maybeMin, qualitativeResults.getProb1Min().getStates()); + + storm::dd::Bdd maybeMax = !(qualitativeResults.getProb0Max().getStates() || qualitativeResults.getProb1Max().getStates()) && quotient.getReachableStates(); + result.second = computeReachabilityProbabilitiesHelper(quotient, storm::OptimizationDirection::Maximize, checkTask.getOptimizationDirection(), maybeMin, qualitativeResults.getProb1Max().getStates()); + } + + return result; + } + template + std::pair, std::unique_ptr> PartialBisimulationMdpModelChecker::computeBoundsPartialQuotient(storm::models::symbolic::Mdp const& quotient, CheckTask const& checkTask) { std::pair, std::unique_ptr> result; // We go through two phases. In phase (1) we are solving the qualitative part and in phase (2) the quantitative part. @@ -364,13 +454,58 @@ namespace storm { result.first->filter(initialStateFilter); result.second->filter(initialStateFilter); printBoundsInformation(result); + + // Check whether the answer can be given after the quantitative solution. + if (checkForResult(quotient, true, result.first->asQuantitativeCheckResult(), checkTask)) { + result.second = nullptr; + } + if (checkForResult(quotient, false, result.second->asQuantitativeCheckResult(), checkTask)) { + result.first = nullptr; + } } return result; } template std::pair, std::unique_ptr> PartialBisimulationMdpModelChecker::computeBoundsPartialQuotient(storm::models::symbolic::StochasticTwoPlayerGame const& quotient, CheckTask const& checkTask) { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Currently not implemented."); + std::pair, std::unique_ptr> result; + + // We go through two phases. In phase (1) we are solving the qualitative part and in phase (2) the quantitative part. + + // Preparation: determine the constraint states and the target states of the reachability objective. + std::pair, storm::dd::Bdd> constraintTargetStates = getConstraintAndTargetStates(quotient, checkTask); + + // Phase (1): solve qualitatively. + storm::abstraction::QualitativeGameResultMinMax qualitativeResults = computeQualitativeResult(quotient, checkTask, constraintTargetStates.first, constraintTargetStates.second, checkTask.getOptimizationDirection()); + + // Check whether the answer can be given after the qualitative solution. + result.first = checkForResult(quotient, qualitativeResults, checkTask); + if (result.first) { + return result; + } + + // Check whether we should skip the quantitative solution (for example if there are initial states for which + // the value is already known to be different at this point. + bool doSkipQuantitativeSolution = skipQuantitativeSolution(quotient, qualitativeResults, checkTask); + STORM_LOG_TRACE("" << (doSkipQuantitativeSolution ? "Skipping" : "Not skipping") << " quantitative solution."); + + // Phase (2): solve quantitatively. + if (!doSkipQuantitativeSolution) { + result = computeQuantitativeResult(quotient, checkTask, constraintTargetStates.first, constraintTargetStates.second, qualitativeResults); + + storm::modelchecker::SymbolicQualitativeCheckResult initialStateFilter(quotient.getReachableStates(), quotient.getInitialStates()); + result.first->filter(initialStateFilter); + result.second->filter(initialStateFilter); + printBoundsInformation(result); + + // Check whether the answer can be given after the quantitative solution. + if (checkForResult(quotient, true, result.first->asQuantitativeCheckResult(), checkTask)) { + result.second = nullptr; + } else if (checkForResult(quotient, false, result.second->asQuantitativeCheckResult(), checkTask)) { + result.first = nullptr; + } + } + return result; } template diff --git a/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h b/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h index 0502870fe..0916bb930 100644 --- a/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h +++ b/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h @@ -17,6 +17,9 @@ namespace storm { class Model; namespace symbolic { + template + class Model; + template class Dtmc; @@ -29,8 +32,14 @@ namespace storm { } namespace abstraction { + template + struct QualitativeResultMinMax; + template struct QualitativeMdpResultMinMax; + + template + struct QualitativeGameResultMinMax; } namespace modelchecker { @@ -67,21 +76,23 @@ namespace storm { // Methods related to the qualitative solution. storm::abstraction::QualitativeMdpResultMinMax computeQualitativeResult(storm::models::symbolic::Mdp const& quotient, CheckTask const& checkTask, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates); - std::unique_ptr checkForResult(storm::models::symbolic::Mdp const& quotient, storm::abstraction::QualitativeMdpResultMinMax const& qualitativeResults, CheckTask const& checkTask); - bool skipQuantitativeSolution(storm::models::symbolic::Mdp const& quotient, storm::abstraction::QualitativeMdpResultMinMax const& qualitativeResults, CheckTask const& checkTask); + storm::abstraction::QualitativeGameResultMinMax computeQualitativeResult(storm::models::symbolic::StochasticTwoPlayerGame const& quotient, CheckTask const& checkTask, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, storm::OptimizationDirection optimizationDirectionInModel); + std::unique_ptr checkForResult(storm::models::symbolic::Model const& quotient, storm::abstraction::QualitativeResultMinMax const& qualitativeResults, CheckTask const& checkTask); + bool skipQuantitativeSolution(storm::models::symbolic::Model const& quotient, storm::abstraction::QualitativeResultMinMax const& qualitativeResults, CheckTask const& checkTask); // Methods related to the quantitative solution. - std::pair, std::unique_ptr> computeQuantitativeResult(storm::models::symbolic::Mdp const& quotient, CheckTask const& checkTask, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, storm::abstraction::QualitativeMdpResultMinMax const& qualitativeResults); - + std::pair, std::unique_ptr> computeQuantitativeResult(storm::models::symbolic::Mdp const& quotient, CheckTask const& checkTask, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, storm::abstraction::QualitativeResultMinMax const& qualitativeResults); + std::pair, std::unique_ptr> computeQuantitativeResult(storm::models::symbolic::StochasticTwoPlayerGame const& quotient, CheckTask const& checkTask, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, storm::abstraction::QualitativeResultMinMax const& qualitativeResults); + // Retrieves the constraint and target states of the quotient wrt. to the formula in the check task. - std::pair, storm::dd::Bdd> getConstraintAndTargetStates(storm::models::symbolic::Mdp const& quotient, CheckTask const& checkTask); + template + std::pair, storm::dd::Bdd> getConstraintAndTargetStates(QuotientModelType const& quotient, CheckTask const& checkTask); // Retrieves the extremal bound (wrt. to the optimization direction) of the quantitative check result. ValueType getExtremalBound(storm::OptimizationDirection dir, QuantitativeCheckResult const& result); - // Retrieves whether the quantitative bounds are sufficient to answer the the query given by the bound (comparison - // type and threshold). - bool boundsSufficient(storm::models::Model const& quotient, bool lowerBounds, QuantitativeCheckResult const& result, storm::logic::ComparisonType comparisonType, ValueType const& threshold); + // Checks whether the quantitative result is sufficient for answering the query. + bool checkForResult(storm::models::Model const& quotient, bool lowerBounds, QuantitativeCheckResult const& result, CheckTask const& checkTask); // Methods to compute bounds on the partial quotient. std::unique_ptr computeBoundsPartialQuotient(SymbolicMdpPrctlModelChecker>& checker, storm::models::symbolic::Mdp const& quotient, storm::OptimizationDirection const& dir, CheckTask& checkTask); diff --git a/src/storm/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp b/src/storm/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp index 9b063e7ea..75b7d58e4 100644 --- a/src/storm/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp +++ b/src/storm/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp @@ -6,6 +6,7 @@ #include "storm/models/symbolic/Dtmc.h" #include "storm/models/symbolic/Ctmc.h" #include "storm/models/symbolic/Mdp.h" +#include "storm/models/symbolic/StochasticTwoPlayerGame.h" #include "storm/models/symbolic/StandardRewardModel.h" #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" @@ -61,18 +62,22 @@ namespace storm { template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; + template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; + template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; + template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; + template class SymbolicPropositionalModelChecker>; } } diff --git a/src/storm/solver/SymbolicGameSolver.cpp b/src/storm/solver/SymbolicGameSolver.cpp index 9f9c54ac7..1cc80a599 100644 --- a/src/storm/solver/SymbolicGameSolver.cpp +++ b/src/storm/solver/SymbolicGameSolver.cpp @@ -150,9 +150,16 @@ namespace storm { return player2Strategy.get(); } + template + std::unique_ptr> SymbolicGameSolverFactory::create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, storm::dd::Bdd const& illegalPlayer1Mask, storm::dd::Bdd const& illegalPlayer2Mask, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables) const { + return std::unique_ptr>(new storm::solver::SymbolicGameSolver(A, allRows, illegalPlayer1Mask, illegalPlayer2Mask, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs, player1Variables, player2Variables)); + } template class SymbolicGameSolver; template class SymbolicGameSolver; + template class SymbolicGameSolverFactory; + template class SymbolicGameSolverFactory; + } } diff --git a/src/storm/solver/SymbolicGameSolver.h b/src/storm/solver/SymbolicGameSolver.h index f4154b00b..adcec325d 100644 --- a/src/storm/solver/SymbolicGameSolver.h +++ b/src/storm/solver/SymbolicGameSolver.h @@ -130,6 +130,12 @@ namespace storm { bool relative; }; + template + class SymbolicGameSolverFactory { + public: + virtual std::unique_ptr> create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, storm::dd::Bdd const& illegalPlayer1Mask, storm::dd::Bdd const& illegalPlayer2Mask, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables) const; + }; + } // namespace solver } // namespace storm diff --git a/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp b/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp index f9df015bd..d6d674c4a 100644 --- a/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp @@ -183,8 +183,6 @@ namespace storm { bool skipped = true; DdNode* partitionThen; DdNode* partitionElse; - DdNode* signatureThen; - DdNode* signatureElse; short offset; bool isNondeterminismVariable = false; while (skipped && !Cudd_IsConstant(nonBlockVariablesNode)) { diff --git a/src/storm/utility/solver.cpp b/src/storm/utility/solver.cpp index 763bc9826..6955f5eed 100644 --- a/src/storm/utility/solver.cpp +++ b/src/storm/utility/solver.cpp @@ -21,12 +21,7 @@ namespace storm { namespace utility { namespace solver { - - template - std::unique_ptr> SymbolicGameSolverFactory::create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, storm::dd::Bdd const& illegalPlayer1Mask, storm::dd::Bdd const& illegalPlayer2Mask, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables) const { - return std::unique_ptr>(new storm::solver::SymbolicGameSolver(A, allRows, illegalPlayer1Mask, illegalPlayer2Mask, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs, player1Variables, player2Variables)); - } - + template std::unique_ptr> LpSolverFactory::create(std::string const& name, storm::solver::LpSolverTypeSelection solvT) const { storm::solver::LpSolverType t; @@ -111,8 +106,6 @@ namespace storm { return factory->create(manager); } - template class SymbolicGameSolverFactory; - template class SymbolicGameSolverFactory; template class LpSolverFactory; template class LpSolverFactory; template class GlpkLpSolverFactory; diff --git a/src/storm/utility/solver.h b/src/storm/utility/solver.h index 757305e29..2dd77f1d6 100644 --- a/src/storm/utility/solver.h +++ b/src/storm/utility/solver.h @@ -56,12 +56,6 @@ namespace storm { namespace utility { namespace solver { - template - class SymbolicGameSolverFactory { - public: - virtual std::unique_ptr> create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, storm::dd::Bdd const& illegalPlayer1Mask, storm::dd::Bdd const& illegalPlayer2Mask, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables) const; - }; - template class LpSolverFactory { public: