diff --git a/src/storm/abstraction/ExplicitQualitativeGameResult.cpp b/src/storm/abstraction/ExplicitQualitativeGameResult.cpp new file mode 100644 index 000000000..8ff41f18a --- /dev/null +++ b/src/storm/abstraction/ExplicitQualitativeGameResult.cpp @@ -0,0 +1,16 @@ +#include "storm/abstraction/ExplicitQualitativeGameResult.h" + +namespace storm { + namespace abstraction { + + ExplicitQualitativeGameResult::ExplicitQualitativeGameResult(storm::utility::graph::ExplicitGameProb01Result const& prob01Result) : storm::utility::graph::ExplicitGameProb01Result(prob01Result) { + // Intentionally left empty. + } + + + storm::storage::BitVector const& ExplicitQualitativeGameResult::getStates() const { + return this->getPlayer1States(); + } + + } +} diff --git a/src/storm/abstraction/ExplicitQualitativeGameResult.h b/src/storm/abstraction/ExplicitQualitativeGameResult.h new file mode 100644 index 000000000..45b97964a --- /dev/null +++ b/src/storm/abstraction/ExplicitQualitativeGameResult.h @@ -0,0 +1,20 @@ +#pragma once + +#include "storm/utility/graph.h" +#include "storm/abstraction/ExplicitQualitativeResult.h" + +namespace storm { + namespace abstraction { + + class ExplicitQualitativeGameResult : public storm::utility::graph::ExplicitGameProb01Result, public ExplicitQualitativeResult { + public: + ExplicitQualitativeGameResult() = default; + + ExplicitQualitativeGameResult(storm::utility::graph::ExplicitGameProb01Result const& prob01Result); + + virtual storm::storage::BitVector const& getStates() const override; + }; + + } +} + diff --git a/src/storm/abstraction/ExplicitQualitativeGameResultMinMax.cpp b/src/storm/abstraction/ExplicitQualitativeGameResultMinMax.cpp new file mode 100644 index 000000000..ef1538c50 --- /dev/null +++ b/src/storm/abstraction/ExplicitQualitativeGameResultMinMax.cpp @@ -0,0 +1,25 @@ +#include "storm/abstraction/ExplicitQualitativeGameResultMinMax.h" + +namespace storm { + namespace abstraction { + + ExplicitQualitativeGameResult const& ExplicitQualitativeGameResultMinMax::getProb0(storm::OptimizationDirection const& dir) const { + if (dir == storm::OptimizationDirection::Minimize) { + return prob0Min; + } else { + return prob0Max; + } + } + + ExplicitQualitativeGameResult const& ExplicitQualitativeGameResultMinMax::getProb1(storm::OptimizationDirection const& dir) const { + if (dir == storm::OptimizationDirection::Minimize) { + return prob1Min; + } else { + return prob1Max; + } + } + + } +} + + diff --git a/src/storm/abstraction/ExplicitQualitativeGameResultMinMax.h b/src/storm/abstraction/ExplicitQualitativeGameResultMinMax.h index 7764c3383..8551a3c47 100644 --- a/src/storm/abstraction/ExplicitQualitativeGameResultMinMax.h +++ b/src/storm/abstraction/ExplicitQualitativeGameResultMinMax.h @@ -1,37 +1,22 @@ #pragma once -#include "storm/storage/dd/DdType.h" - -#include "storm/abstraction/SymbolicQualitativeResultMinMax.h" -#include "storm/abstraction/QualitativeGameResult.h" +#include "storm/abstraction/ExplicitQualitativeResultMinMax.h" +#include "storm/abstraction/ExplicitQualitativeGameResult.h" namespace storm { namespace abstraction { - class ExplicitQualitativeGameResultMinMax : public QualitativeResultMinMax { + class ExplicitQualitativeGameResultMinMax : public ExplicitQualitativeResultMinMax { public: ExplicitQualitativeGameResultMinMax() = default; - 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; - } - } + virtual ExplicitQualitativeGameResult const& getProb0(storm::OptimizationDirection const& dir) const override; + virtual ExplicitQualitativeGameResult const& getProb1(storm::OptimizationDirection const& dir) const override; - QualitativeGameResult prob0Min; - QualitativeGameResult prob1Min; - QualitativeGameResult prob0Max; - QualitativeGameResult prob1Max; + ExplicitQualitativeGameResult prob0Min; + ExplicitQualitativeGameResult prob1Min; + ExplicitQualitativeGameResult prob0Max; + ExplicitQualitativeGameResult prob1Max; }; } diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index cd3522ac0..d97973bd6 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -3,6 +3,8 @@ #include "storm/abstraction/AbstractionInformation.h" #include "storm/abstraction/MenuGameAbstractor.h" +#include "storm/storage/BitVector.h" + #include "storm/storage/dd/DdManager.h" #include "storm/utility/dd.h" #include "storm/utility/solver.h" @@ -122,7 +124,7 @@ namespace storm { } template - PivotStateResult pickPivotState(AbstractionSettings::PivotSelectionHeuristic const& heuristic, storm::abstraction::MenuGame const& game, PivotStateCandidatesResult const& pivotStateCandidateResult, boost::optional> const& qualitativeResult, boost::optional> const& quantitativeResult) { + PivotStateResult pickPivotState(AbstractionSettings::PivotSelectionHeuristic const& heuristic, storm::abstraction::MenuGame const& game, PivotStateCandidatesResult const& pivotStateCandidateResult, boost::optional> const& qualitativeResult, boost::optional> const& quantitativeResult) { // Get easy access to strategies. storm::dd::Bdd minPlayer1Strategy; @@ -587,7 +589,7 @@ namespace storm { } template - bool MenuGameRefiner::refine(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, QualitativeGameResultMinMax const& qualitativeResult) const { + bool MenuGameRefiner::refine(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, SymbolicQualitativeGameResultMinMax const& qualitativeResult) const { STORM_LOG_TRACE("Trying refinement after qualitative check."); // Get all relevant strategies. storm::dd::Bdd minPlayer1Strategy = qualitativeResult.prob0Min.getPlayer1Strategy(); @@ -675,7 +677,7 @@ namespace storm { } template - bool MenuGameRefiner::refine(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, QuantitativeGameResultMinMax const& quantitativeResult) const { + bool MenuGameRefiner::refine(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, SymbolicQuantitativeGameResultMinMax const& quantitativeResult) const { STORM_LOG_TRACE("Refining after quantitative check."); // Get all relevant strategies. storm::dd::Bdd minPlayer1Strategy = quantitativeResult.min.getPlayer1Strategy(); diff --git a/src/storm/abstraction/MenuGameRefiner.h b/src/storm/abstraction/MenuGameRefiner.h index c0a4b8f8a..ed3589ac6 100644 --- a/src/storm/abstraction/MenuGameRefiner.h +++ b/src/storm/abstraction/MenuGameRefiner.h @@ -7,8 +7,8 @@ #include #include "storm/abstraction/RefinementCommand.h" -#include "storm/abstraction/QualitativeGameResultMinMax.h" -#include "storm/abstraction/QuantitativeGameResultMinMax.h" +#include "storm/abstraction/SymbolicQualitativeGameResultMinMax.h" +#include "storm/abstraction/SymbolicQuantitativeGameResultMinMax.h" #include "storm/storage/expressions/Expression.h" #include "storm/storage/expressions/FullPredicateSplitter.h" @@ -85,14 +85,14 @@ namespace storm { * * @param True if predicates for refinement could be derived, false otherwise. */ - bool refine(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, QualitativeGameResultMinMax const& qualitativeResult) const; + bool refine(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, SymbolicQualitativeGameResultMinMax const& qualitativeResult) const; /*! * Refines the abstractor based on the quantitative result by trying to derive suitable predicates. * * @param True if predicates for refinement could be derived, false otherwise. */ - bool refine(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, QuantitativeGameResultMinMax const& quantitativeResult) const; + bool refine(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, SymbolicQuantitativeGameResultMinMax const& quantitativeResult) const; /*! * Retrieves whether all guards were added. diff --git a/src/storm/abstraction/SymbolicQualitativeGameResult.h b/src/storm/abstraction/SymbolicQualitativeGameResult.h index 2daea6ae6..968e7d51d 100644 --- a/src/storm/abstraction/SymbolicQualitativeGameResult.h +++ b/src/storm/abstraction/SymbolicQualitativeGameResult.h @@ -8,6 +8,7 @@ namespace storm { template class SymbolicQualitativeGameResult : public storm::utility::graph::SymbolicGameProb01Result, public SymbolicQualitativeResult { + public: SymbolicQualitativeGameResult() = default; SymbolicQualitativeGameResult(storm::utility::graph::SymbolicGameProb01Result const& prob01Result); diff --git a/src/storm/abstraction/SymbolicQualitativeGameResultMinMax.cpp b/src/storm/abstraction/SymbolicQualitativeGameResultMinMax.cpp index 5a9d34ab5..9768cab16 100644 --- a/src/storm/abstraction/SymbolicQualitativeGameResultMinMax.cpp +++ b/src/storm/abstraction/SymbolicQualitativeGameResultMinMax.cpp @@ -21,8 +21,8 @@ namespace storm { } } - template class SymbolicQualitativeResultMinMax; - template class SymbolicQualitativeResultMinMax; + template class SymbolicQualitativeGameResultMinMax; + template class SymbolicQualitativeGameResultMinMax; } } diff --git a/src/storm/abstraction/SymbolicQualitativeGameResultMinMax.h b/src/storm/abstraction/SymbolicQualitativeGameResultMinMax.h index beeadd0b0..4f58660a9 100644 --- a/src/storm/abstraction/SymbolicQualitativeGameResultMinMax.h +++ b/src/storm/abstraction/SymbolicQualitativeGameResultMinMax.h @@ -3,6 +3,7 @@ #include "storm/storage/dd/DdType.h" #include "storm/abstraction/SymbolicQualitativeResultMinMax.h" +#include "storm/abstraction/SymbolicQualitativeGameResult.h" namespace storm { namespace abstraction { @@ -15,10 +16,10 @@ namespace storm { virtual SymbolicQualitativeResult const& getProb0(storm::OptimizationDirection const& dir) const override; virtual SymbolicQualitativeResult const& getProb1(storm::OptimizationDirection const& dir) const override; - SymbolicQualitativeResult prob0Min; - SymbolicQualitativeResult prob1Min; - SymbolicQualitativeResult prob0Max; - SymbolicQualitativeResult prob1Max; + SymbolicQualitativeGameResult prob0Min; + SymbolicQualitativeGameResult prob1Min; + SymbolicQualitativeGameResult prob0Max; + SymbolicQualitativeGameResult prob1Max; }; } diff --git a/src/storm/abstraction/SymbolicQualitativeMdpResult.h b/src/storm/abstraction/SymbolicQualitativeMdpResult.h index ee44a942e..ba854fff7 100644 --- a/src/storm/abstraction/SymbolicQualitativeMdpResult.h +++ b/src/storm/abstraction/SymbolicQualitativeMdpResult.h @@ -9,6 +9,7 @@ namespace storm { template class SymbolicQualitativeMdpResult : public SymbolicQualitativeResult { + public: SymbolicQualitativeMdpResult() = default; SymbolicQualitativeMdpResult(storm::dd::Bdd const& states); diff --git a/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.cpp b/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.cpp index 1fdcf2907..e6cdf6ddd 100644 --- a/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.cpp @@ -25,9 +25,9 @@ #include "storm/abstraction/StateSet.h" #include "storm/abstraction/SymbolicStateSet.h" #include "storm/abstraction/QualitativeResultMinMax.h" -#include "storm/abstraction/QualitativeMdpResult.h" -#include "storm/abstraction/QualitativeMdpResultMinMax.h" -#include "storm/abstraction/QualitativeGameResultMinMax.h" +#include "storm/abstraction/SymbolicQualitativeMdpResult.h" +#include "storm/abstraction/SymbolicQualitativeMdpResultMinMax.h" +#include "storm/abstraction/SymbolicQualitativeGameResultMinMax.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/AbstractionSettings.h" @@ -470,18 +470,18 @@ namespace storm { template std::unique_ptr AbstractAbstractionRefinementModelChecker::computeQualitativeResult(Environment const& env, storm::models::symbolic::Dtmc const& abstractModel, storm::abstraction::SymbolicStateSet const& constraintStates, storm::abstraction::SymbolicStateSet const& targetStates) { STORM_LOG_DEBUG("Computing qualitative solution for DTMC."); - std::unique_ptr> result = std::make_unique>(); + std::unique_ptr> result = std::make_unique>(); 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 = abstractModel.getTransitionMatrix().notZero(); if (isRewardFormula) { auto prob1 = storm::utility::graph::performProb1(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates()); - result->prob1Min = result->prob1Max = storm::abstraction::QualitativeMdpResult(prob1); + result->prob1Min = result->prob1Max = storm::abstraction::SymbolicQualitativeMdpResult(prob1); } else { auto prob01 = storm::utility::graph::performProb01(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates()); - result->prob0Min = result->prob0Max = storm::abstraction::QualitativeMdpResult(prob01.first); - result->prob1Min = result->prob1Max = storm::abstraction::QualitativeMdpResult(prob01.second); + result->prob0Min = result->prob0Max = storm::abstraction::SymbolicQualitativeMdpResult(prob01.first); + result->prob1Min = result->prob1Max = storm::abstraction::SymbolicQualitativeMdpResult(prob01.second); } auto end = std::chrono::high_resolution_clock::now(); @@ -494,7 +494,7 @@ namespace storm { template std::unique_ptr AbstractAbstractionRefinementModelChecker::computeQualitativeResult(Environment const& env, storm::models::symbolic::Mdp const& abstractModel, storm::abstraction::SymbolicStateSet const& constraintStates, storm::abstraction::SymbolicStateSet const& targetStates) { STORM_LOG_DEBUG("Computing qualitative solution for MDP."); - std::unique_ptr> result = std::make_unique>(); + std::unique_ptr> result = std::make_unique>(); auto start = std::chrono::high_resolution_clock::now(); bool isRewardFormula = checkTask->getFormula().isEventuallyFormula() && checkTask->getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward; @@ -505,13 +505,13 @@ namespace storm { bool computedMin = false; if (abstractionPlayer == 1 || checkTask->getOptimizationDirection() == storm::OptimizationDirection::Minimize) { auto states = storm::utility::graph::performProb1E(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(), lastQualitativeResults ? lastQualitativeResults->asSymbolicQualitativeResultMinMax().getProb1Min().getStates() : storm::utility::graph::performProbGreater0E(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates())); - result->prob1Min = storm::abstraction::QualitativeMdpResult(states); + result->prob1Min = storm::abstraction::SymbolicQualitativeMdpResult(states); computedMin = true; } if (abstractionPlayer == 1 || checkTask->getOptimizationDirection() == storm::OptimizationDirection::Maximize) { auto states = storm::utility::graph::performProb1A(abstractModel, transitionMatrixBdd, targetStates.getStates(), storm::utility::graph::performProbGreater0A(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates())); - result->prob1Max = storm::abstraction::QualitativeMdpResult(states); + result->prob1Max = storm::abstraction::SymbolicQualitativeMdpResult(states); if (!computedMin) { result->prob1Min = result->prob1Max; } @@ -523,18 +523,18 @@ namespace storm { bool computedMax = false; if (abstractionPlayer == 1 || checkTask->getOptimizationDirection() == storm::OptimizationDirection::Maximize) { auto states = storm::utility::graph::performProb0A(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates()); - result->prob0Max = storm::abstraction::QualitativeMdpResult(states); + result->prob0Max = storm::abstraction::SymbolicQualitativeMdpResult(states); states = storm::utility::graph::performProb1E(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(), lastQualitativeResults ? lastQualitativeResults->asSymbolicQualitativeResultMinMax().getProb1Min().getStates() : storm::utility::graph::performProbGreater0E(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates())); - result->prob1Max = storm::abstraction::QualitativeMdpResult(states); + result->prob1Max = storm::abstraction::SymbolicQualitativeMdpResult(states); computedMax = true; } if (abstractionPlayer == 1 || checkTask->getOptimizationDirection() == storm::OptimizationDirection::Minimize) { auto states = storm::utility::graph::performProb1A(abstractModel, transitionMatrixBdd, lastQualitativeResults ? lastQualitativeResults->asSymbolicQualitativeResultMinMax().getProb1Min().getStates() : targetStates.getStates(), storm::utility::graph::performProbGreater0A(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates())); - result->prob1Min = storm::abstraction::QualitativeMdpResult(states); + result->prob1Min = storm::abstraction::SymbolicQualitativeMdpResult(states); states = storm::utility::graph::performProb0E(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates()); - result->prob0Min = storm::abstraction::QualitativeMdpResult(states); + result->prob0Min = storm::abstraction::SymbolicQualitativeMdpResult(states); if (!computedMax) { result->prob0Max = result->prob0Min; @@ -550,13 +550,13 @@ namespace storm { bool computedMin = false; if (abstractionPlayer == 1 || checkTask->getOptimizationDirection() == storm::OptimizationDirection::Minimize) { auto prob1 = storm::utility::graph::performProb1E(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(), storm::utility::graph::performProbGreater0E(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates())); - result->prob1Min = storm::abstraction::QualitativeMdpResult(prob1); + result->prob1Min = storm::abstraction::SymbolicQualitativeMdpResult(prob1); computedMin = true; } if (abstractionPlayer == 1 || checkTask->getOptimizationDirection() == storm::OptimizationDirection::Maximize) { auto prob1 = storm::utility::graph::performProb1A(abstractModel, transitionMatrixBdd, targetStates.getStates(), storm::utility::graph::performProbGreater0A(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates())); - result->prob1Max = storm::abstraction::QualitativeMdpResult(prob1); + result->prob1Max = storm::abstraction::SymbolicQualitativeMdpResult(prob1); if (!computedMin) { result->prob1Min = result->prob1Max; } @@ -567,15 +567,15 @@ namespace storm { bool computedMin = false; if (abstractionPlayer == 1 || checkTask->getOptimizationDirection() == storm::OptimizationDirection::Minimize) { auto prob01 = storm::utility::graph::performProb01Min(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates()); - result->prob0Min = storm::abstraction::QualitativeMdpResult(prob01.first); - result->prob1Min = storm::abstraction::QualitativeMdpResult(prob01.second); + result->prob0Min = storm::abstraction::SymbolicQualitativeMdpResult(prob01.first); + result->prob1Min = storm::abstraction::SymbolicQualitativeMdpResult(prob01.second); computedMin = true; } if (abstractionPlayer == 1 || checkTask->getOptimizationDirection() == storm::OptimizationDirection::Maximize) { auto prob01 = storm::utility::graph::performProb01Max(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates()); - result->prob0Max = storm::abstraction::QualitativeMdpResult(prob01.first); - result->prob1Max = storm::abstraction::QualitativeMdpResult(prob01.second); + result->prob0Max = storm::abstraction::SymbolicQualitativeMdpResult(prob01.first); + result->prob1Max = storm::abstraction::SymbolicQualitativeMdpResult(prob01.second); if (!computedMin) { result->prob0Min = result->prob0Max; result->prob1Min = result->prob1Max; @@ -604,7 +604,7 @@ namespace storm { template std::unique_ptr AbstractAbstractionRefinementModelChecker::computeQualitativeResult(Environment const& env, storm::models::symbolic::StochasticTwoPlayerGame const& abstractModel, storm::abstraction::SymbolicStateSet const& constraintStates, storm::abstraction::SymbolicStateSet const& targetStates) { STORM_LOG_DEBUG("Computing qualitative solution for S2PG."); - std::unique_ptr> result; + std::unique_ptr> result; // Obtain the player optimization directions. uint64_t abstractionPlayer = this->getAbstractionPlayer(); @@ -622,7 +622,7 @@ namespace storm { if (this->getReuseQualitativeResults()) { result = computeQualitativeResultReuse(abstractModel, transitionMatrixBdd, constraintStates, targetStates, abstractionPlayer, modelNondeterminismDirection, requiresSchedulers); } else { - result = std::make_unique>(); + result = std::make_unique>(); result->prob0Min = storm::utility::graph::performProb0(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(), abstractionPlayer == 1 ? storm::OptimizationDirection::Minimize : modelNondeterminismDirection, abstractionPlayer == 2 ? storm::OptimizationDirection::Minimize : modelNondeterminismDirection, requiresSchedulers, requiresSchedulers); result->prob1Min = storm::utility::graph::performProb1(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(), abstractionPlayer == 1 ? storm::OptimizationDirection::Minimize : modelNondeterminismDirection, abstractionPlayer == 2 ? storm::OptimizationDirection::Minimize : modelNondeterminismDirection, requiresSchedulers, requiresSchedulers); @@ -648,8 +648,8 @@ namespace storm { } template - std::unique_ptr::DdType>> AbstractAbstractionRefinementModelChecker::computeQualitativeResultReuse(storm::models::symbolic::StochasticTwoPlayerGame const& abstractModel, storm::dd::Bdd const& transitionMatrixBdd, storm::abstraction::SymbolicStateSet const& constraintStates, storm::abstraction::SymbolicStateSet const& targetStates, uint64_t abstractionPlayer, storm::OptimizationDirection const& modelNondeterminismDirection, bool requiresSchedulers) { - std::unique_ptr> result = std::make_unique>(); + std::unique_ptr::DdType>> AbstractAbstractionRefinementModelChecker::computeQualitativeResultReuse(storm::models::symbolic::StochasticTwoPlayerGame const& abstractModel, storm::dd::Bdd const& transitionMatrixBdd, storm::abstraction::SymbolicStateSet const& constraintStates, storm::abstraction::SymbolicStateSet const& targetStates, uint64_t abstractionPlayer, storm::OptimizationDirection const& modelNondeterminismDirection, bool requiresSchedulers) { + std::unique_ptr> result = std::make_unique>(); // Depending on the model nondeterminism direction, we choose a different order of operations. if (modelNondeterminismDirection == storm::OptimizationDirection::Minimize) { diff --git a/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.h b/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.h index 5fdabe05e..83a2d35a6 100644 --- a/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.h +++ b/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.h @@ -41,10 +41,10 @@ namespace storm { class SymbolicQualitativeResultMinMax; template - class QualitativeMdpResultMinMax; + class SymbolicQualitativeMdpResultMinMax; template - class QualitativeGameResultMinMax; + class SymbolicQualitativeGameResultMinMax; class StateSet; @@ -124,7 +124,7 @@ namespace storm { std::unique_ptr computeQualitativeResult(Environment const& env, storm::models::symbolic::Dtmc const& abstractModel, storm::abstraction::SymbolicStateSet const& constraintStates, storm::abstraction::SymbolicStateSet const& targetStates); std::unique_ptr computeQualitativeResult(Environment const& env, storm::models::symbolic::Mdp const& abstractModel, storm::abstraction::SymbolicStateSet const& constraintStates, storm::abstraction::SymbolicStateSet const& targetStates); std::unique_ptr computeQualitativeResult(Environment const& env, storm::models::symbolic::StochasticTwoPlayerGame const& abstractModel, storm::abstraction::SymbolicStateSet const& constraintStates, storm::abstraction::SymbolicStateSet const& targetStates); - std::unique_ptr> computeQualitativeResultReuse(storm::models::symbolic::StochasticTwoPlayerGame const& abstractModel, storm::dd::Bdd const& transitionMatrixBdd, storm::abstraction::SymbolicStateSet const& constraintStates, storm::abstraction::SymbolicStateSet const& targetStates, uint64_t abstractionPlayer, storm::OptimizationDirection const& modelNondeterminismDirection, bool requiresSchedulers); + std::unique_ptr> computeQualitativeResultReuse(storm::models::symbolic::StochasticTwoPlayerGame const& abstractModel, storm::dd::Bdd const& transitionMatrixBdd, storm::abstraction::SymbolicStateSet const& constraintStates, storm::abstraction::SymbolicStateSet const& targetStates, uint64_t abstractionPlayer, storm::OptimizationDirection const& modelNondeterminismDirection, bool requiresSchedulers); std::unique_ptr checkForResultAfterQualitativeCheck(storm::models::Model const& abstractModel); std::unique_ptr checkForResultAfterQualitativeCheck(storm::models::symbolic::Model const& abstractModel); diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 6ba963c63..4b64daac9 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -10,7 +10,6 @@ #include "storm/storage/expressions/ExpressionManager.h" #include "storm/storage/expressions/VariableSetPredicateSplitter.h" - #include "storm/storage/jani/Edge.h" #include "storm/storage/jani/EdgeDestination.h" #include "storm/storage/jani/Model.h" @@ -26,6 +25,8 @@ #include "storm/abstraction/jani/JaniMenuGameAbstractor.h" #include "storm/abstraction/MenuGameRefiner.h" +#include "storm/abstraction/ExplicitQualitativeGameResultMinMax.h" + #include "storm/logic/FragmentSpecification.h" #include "storm/solver/SymbolicGameSolver.h" @@ -45,8 +46,8 @@ namespace storm { namespace modelchecker { - using storm::abstraction::QuantitativeGameResult; - using storm::abstraction::QuantitativeGameResultMinMax; + using storm::abstraction::SymbolicQuantitativeGameResult; + using storm::abstraction::SymbolicQuantitativeGameResultMinMax; 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()) { @@ -71,9 +72,11 @@ namespace storm { preprocessedModel = model.asJaniModel().flattenComposition(); } - storm::settings::modules::AbstractionSettings::ReuseMode reuseMode = storm::settings::getModule().getReuseMode(); + auto const& abstractionSettings = storm::settings::getModule(); + storm::settings::modules::AbstractionSettings::ReuseMode reuseMode = abstractionSettings.getReuseMode(); reuseQualitativeResults = reuseMode == storm::settings::modules::AbstractionSettings::ReuseMode::All || reuseMode == storm::settings::modules::AbstractionSettings::ReuseMode::Qualitative; reuseQuantitativeResults = reuseMode == storm::settings::modules::AbstractionSettings::ReuseMode::All || reuseMode == storm::settings::modules::AbstractionSettings::ReuseMode::Quantitative; + maximalNumberOfAbstractions = abstractionSettings.getMaximalAbstractionCount(); } template @@ -159,7 +162,7 @@ namespace storm { } template - std::unique_ptr checkForResultAfterQualitativeCheck(CheckTask const& checkTask, storm::dd::Bdd const& initialStates, QualitativeGameResultMinMax const& qualitativeResult) { + std::unique_ptr checkForResultAfterQualitativeCheck(CheckTask const& checkTask, storm::dd::Bdd const& initialStates, SymbolicQualitativeGameResultMinMax const& qualitativeResult) { // Check whether we can already give the answer based on the current information. std::unique_ptr result = checkForResultAfterQualitativeCheck(checkTask, storm::OptimizationDirection::Minimize, initialStates, qualitativeResult.prob0Min.getPlayer1States(), qualitativeResult.prob1Min.getPlayer1States()); if (result) { @@ -232,7 +235,7 @@ namespace storm { } template - QuantitativeGameResult solveMaybeStates(Environment const& env, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::MenuGame const& game, storm::dd::Bdd const& maybeStates, storm::dd::Bdd const& prob1States, boost::optional> const& startInfo = boost::none) { + SymbolicQuantitativeGameResult solveMaybeStates(Environment const& env, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::MenuGame const& game, storm::dd::Bdd const& maybeStates, storm::dd::Bdd const& prob1States, boost::optional> const& startInfo = boost::none) { STORM_LOG_TRACE("Performing quantative solution step. Player 1: " << player1Direction << ", player 2: " << player2Direction << "."); @@ -259,14 +262,14 @@ namespace storm { 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(env, 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()); + return SymbolicQuantitativeGameResult(std::make_pair(storm::utility::zero(), storm::utility::one()), values, solver->getPlayer1Strategy(), solver->getPlayer2Strategy()); } template - QuantitativeGameResult computeQuantitativeResult(Environment const& env, storm::OptimizationDirection player1Direction, storm::OptimizationDirection player2Direction, storm::abstraction::MenuGame const& game, QualitativeGameResultMinMax const& qualitativeResult, storm::dd::Add const& initialStatesAdd, storm::dd::Bdd const& maybeStates, boost::optional> const& startInfo = boost::none) { + SymbolicQuantitativeGameResult computeQuantitativeResult(Environment const& env, storm::OptimizationDirection player1Direction, storm::OptimizationDirection player2Direction, storm::abstraction::MenuGame const& game, SymbolicQualitativeGameResultMinMax const& qualitativeResult, storm::dd::Add const& initialStatesAdd, storm::dd::Bdd const& maybeStates, boost::optional> const& startInfo = boost::none) { bool min = player2Direction == storm::OptimizationDirection::Minimize; - QuantitativeGameResult result; + SymbolicQuantitativeGameResult result; // We fix the strategies. That is, we take the decisions of the strategies obtained in the qualitiative // preprocessing if possible. @@ -355,9 +358,11 @@ namespace storm { storm::dd::Bdd globalTargetStates = abstractor->getStates(targetStateExpression); // Enter the main-loop of abstraction refinement. - boost::optional> previousQualitativeResult = boost::none; - boost::optional> previousMinQuantitativeResult = boost::none; - for (uint_fast64_t iterations = 0; iterations < 10000; ++iterations) { + boost::optional> previousSymbolicQualitativeResult = boost::none; + boost::optional> previousSymbolicMinQuantitativeResult = boost::none; + boost::optional previousExplicitQualitativeResult = boost::none; + // boost::optional> previousExplicitMinQuantitativeResult = boost::none; + for (uint_fast64_t iterations = 0; iterations < maximalNumberOfAbstractions; ++iterations) { auto iterationStart = std::chrono::high_resolution_clock::now(); STORM_LOG_TRACE("Starting iteration " << iterations << "."); @@ -384,9 +389,9 @@ namespace storm { std::unique_ptr result; if (solveMode == storm::settings::modules::AbstractionSettings::SolveMode::Dd) { - result = performSymbolicAbstractionSolutionStep(env, checkTask, game, player1Direction, initialStates, constraintStates, targetStates, refiner, previousQualitativeResult, previousMinQuantitativeResult); + result = performSymbolicAbstractionSolutionStep(env, checkTask, game, player1Direction, initialStates, constraintStates, targetStates, refiner, previousSymbolicQualitativeResult, previousSymbolicMinQuantitativeResult); } else { - result = performExplicitAbstractionSolutionStep(env, checkTask, game, player1Direction, initialStates, constraintStates, targetStates, refiner); + result = performExplicitAbstractionSolutionStep(env, checkTask, game, player1Direction, initialStates, constraintStates, targetStates, refiner, previousExplicitQualitativeResult); } if (result) { @@ -397,13 +402,14 @@ namespace storm { auto iterationEnd = std::chrono::high_resolution_clock::now(); STORM_LOG_DEBUG("Iteration " << iterations << " took " << std::chrono::duration_cast(iterationEnd - iterationStart).count() << "ms."); } - - STORM_LOG_ASSERT(false, "This point must not be reached."); + + // If this point is reached, we have given up on abstraction. + STORM_LOG_WARN("Could not derive result, maximal number of abstractions exceeded."); return nullptr; } template - std::unique_ptr GameBasedMdpModelChecker::performSymbolicAbstractionSolutionStep(Environment const& env, CheckTask const& checkTask, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& initialStates, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, storm::abstraction::MenuGameRefiner const& refiner, boost::optional>& previousQualitativeResult, boost::optional>& previousMinQuantitativeResult) { + std::unique_ptr GameBasedMdpModelChecker::performSymbolicAbstractionSolutionStep(Environment const& env, CheckTask const& checkTask, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& initialStates, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, storm::abstraction::MenuGameRefiner const& refiner, boost::optional>& previousQualitativeResult, boost::optional>& previousMinQuantitativeResult) { STORM_LOG_TRACE("Using dd-based solving."); @@ -412,7 +418,7 @@ namespace storm { // (1) compute all states with probability 0/1 wrt. to the two different player 2 goals (min/max). auto qualitativeStart = std::chrono::high_resolution_clock::now(); - QualitativeGameResultMinMax qualitativeResult = computeProb01States(previousQualitativeResult, game, player1Direction, transitionMatrixBdd, constraintStates, targetStates); + SymbolicQualitativeGameResultMinMax qualitativeResult = computeProb01States(previousQualitativeResult, game, player1Direction, transitionMatrixBdd, constraintStates, targetStates); std::unique_ptr result = checkForResultAfterQualitativeCheck(checkTask, initialStates, qualitativeResult); if (result) { return result; @@ -456,7 +462,7 @@ namespace storm { auto quantitativeStart = std::chrono::high_resolution_clock::now(); - QuantitativeGameResultMinMax quantitativeResult; + 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); @@ -502,39 +508,64 @@ namespace storm { } template - std::unique_ptr GameBasedMdpModelChecker::performExplicitAbstractionSolutionStep(Environment const& env, CheckTask const& checkTask, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& initialStatesBdd, storm::dd::Bdd const& constraintStatesBdd, storm::dd::Bdd const& targetStatesBdd, storm::abstraction::MenuGameRefiner const& refiner) { - STORM_LOG_TRACE("Using hybrid solving."); + std::unique_ptr GameBasedMdpModelChecker::performExplicitAbstractionSolutionStep(Environment const& env, CheckTask const& checkTask, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& initialStatesBdd, storm::dd::Bdd const& constraintStatesBdd, storm::dd::Bdd const& targetStatesBdd, storm::abstraction::MenuGameRefiner const& refiner, boost::optional& previousQualitativeResult) { + STORM_LOG_TRACE("Using sparse solving."); // (0) Start by transforming the necessary symbolic elements to explicit ones. storm::dd::Odd odd = game.getReachableStates().createOdd(); std::pair, std::vector> transitionMatrixAndLabeling = game.getTransitionMatrix().toLabeledMatrix(game.getRowVariables(), game.getColumnVariables(), game.getNondeterminismVariables(), game.getPlayer1Variables(), odd, odd, true); - auto const& transitionMatrix = transitionMatrixAndLabeling.first; - auto const& labeling = transitionMatrixAndLabeling.second; - + auto& transitionMatrix = transitionMatrixAndLabeling.first; + auto& labeling = transitionMatrixAndLabeling.second; + + // Create the player 2 row grouping from the labeling. + std::vector tmpPlayer2RowGrouping; + for (uint64_t player1State = 0; player1State < transitionMatrix.getRowGroupCount(); ++player1State) { + uint64_t lastLabel = std::numeric_limits::max(); + for (uint64_t row = transitionMatrix.getRowGroupIndices()[player1State]; row < transitionMatrix.getRowGroupIndices()[player1State + 1]; ++row) { + if (labeling[row] != lastLabel) { + tmpPlayer2RowGrouping.emplace_back(row); + lastLabel = labeling[row]; + } + } + } + tmpPlayer2RowGrouping.emplace_back(labeling.size()); + + std::vector player1RowGrouping = transitionMatrix.swapRowGroupIndices(std::move(tmpPlayer2RowGrouping)); + auto const& player2RowGrouping = transitionMatrix.getRowGroupIndices(); + + // Create the backward transitions for both players. + storm::storage::SparseMatrix player1BackwardTransitions = transitionMatrix.transpose(true); + std::vector player2BackwardTransitions(transitionMatrix.getRowGroupCount()); + uint64_t player2State = 0; + for (uint64_t player1State = 0; player1State < player2RowGrouping.size() - 1; ++player1State) { + while (player1RowGrouping[player1State + 1] > player2RowGrouping[player2State]) { + player2BackwardTransitions[player2State] = player1State; + ++player2State; + } + } + storm::storage::BitVector initialStates = initialStatesBdd.toVector(odd); storm::storage::BitVector constraintStates = constraintStatesBdd.toVector(odd); storm::storage::BitVector targetStates = targetStatesBdd.toVector(odd); // (1) compute all states with probability 0/1 wrt. to the two different player 2 goals (min/max). auto qualitativeStart = std::chrono::high_resolution_clock::now(); - ExplicitQualitativeGameResultMinMax qualitativeResult = computeProb01States(game, player1Direction, transitionMatrix, constraintStates, targetStates); - std::unique_ptr result = checkForResultAfterQualitativeCheck(checkTask, initialStates, qualitativeResult); - if (result) { - return result; - } + ExplicitQualitativeGameResultMinMax qualitativeResult = computeProb01States(previousQualitativeResult, player1Direction, transitionMatrix, player1RowGrouping, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates); +// std::unique_ptr result = checkForResultAfterQualitativeCheck(checkTask, initialStates, qualitativeResult); +// if (result) { +// return result; +// } auto qualitativeEnd = std::chrono::high_resolution_clock::now(); STORM_LOG_DEBUG("Qualitative computation completed in " << std::chrono::duration_cast(qualitativeEnd - qualitativeStart).count() << "ms."); +// std::cout << transitionMatrix << std::endl; +// std::cout << labeling.size() << std::endl; +// std::cout << initialStates << std::endl; +// std::cout << constraintStates << std::endl; +// std::cout << targetStates << std::endl; - - std::cout << transitionMatrix << std::endl; - std::cout << labeling.size() << std::endl; - std::cout << initialStates << std::endl; - std::cout << constraintStates << std::endl; - std::cout << targetStates << std::endl; - - exit(-1); + return nullptr; } template @@ -573,7 +604,7 @@ namespace storm { } template - bool checkQualitativeStrategies(bool prob0, QualitativeGameResult const& result, storm::dd::Bdd const& targetStates) { + bool checkQualitativeStrategies(bool prob0, SymbolicQualitativeGameResult const& result, storm::dd::Bdd const& targetStates) { if (prob0) { STORM_LOG_ASSERT(result.hasPlayer1Strategy() && (result.getPlayer1States().isZero() || !result.getPlayer1Strategy().isZero()), "Unable to proceed without strategy."); } else { @@ -586,7 +617,7 @@ namespace storm { } template - bool checkQualitativeStrategies(QualitativeGameResultMinMax const& qualitativeResult, storm::dd::Bdd const& targetStates) { + bool checkQualitativeStrategies(SymbolicQualitativeGameResultMinMax const& qualitativeResult, storm::dd::Bdd const& targetStates) { bool result = true; result &= checkQualitativeStrategies(true, qualitativeResult.prob0Min, targetStates); result &= checkQualitativeStrategies(false, qualitativeResult.prob1Min, targetStates); @@ -596,9 +627,72 @@ namespace storm { } template - QualitativeGameResultMinMax GameBasedMdpModelChecker::computeProb01States(boost::optional> const& previousQualitativeResult, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& transitionMatrixBdd, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates) { + ExplicitQualitativeGameResultMinMax GameBasedMdpModelChecker::computeProb01States(boost::optional const& previousQualitativeResult, storm::OptimizationDirection player1Direction, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1RowGrouping, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates) { + + ExplicitQualitativeGameResultMinMax result; + +// if (reuseQualitativeResults) { +// // Depending on the player 1 direction, we choose a different order of operations. +// if (player1Direction == storm::OptimizationDirection::Minimize) { +// // (1) min/min: compute prob0 using the game functions +// result.prob0Min = storm::utility::graph::performProb0(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true); +// +// // (2) min/min: compute prob1 using the MDP functions +// storm::dd::Bdd candidates = game.getReachableStates() && !result.prob0Min.player1States; +// storm::dd::Bdd prob1MinMinMdp = storm::utility::graph::performProb1A(game, transitionMatrixBdd, previousQualitativeResult ? previousQualitativeResult.get().prob1Min.player1States : targetStates, candidates); +// +// // (3) min/min: compute prob1 using the game functions +// result.prob1Min = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true, boost::make_optional(prob1MinMinMdp)); +// +// // (4) min/max: compute prob 0 using the game functions +// result.prob0Max = storm::utility::graph::performProb0(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true); +// +// // (5) min/max: compute prob 1 using the game functions +// // We know that only previous prob1 states can now be prob 1 states again, because the upper bound +// // values can only decrease over iterations. +// boost::optional> prob1Candidates; +// if (previousQualitativeResult) { +// prob1Candidates = previousQualitativeResult.get().prob1Max.player1States; +// } +// result.prob1Max = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true, prob1Candidates); +// } else { +// // (1) max/max: compute prob0 using the game functions +// result.prob0Max = storm::utility::graph::performProb0(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true); +// +// // (2) max/max: compute prob1 using the MDP functions, reuse prob1 states of last iteration to constrain the candidate states. +// storm::dd::Bdd candidates = game.getReachableStates() && !result.prob0Max.player1States; +// if (previousQualitativeResult) { +// candidates &= previousQualitativeResult.get().prob1Max.player1States; +// } +// storm::dd::Bdd prob1MaxMaxMdp = storm::utility::graph::performProb1E(game, transitionMatrixBdd, constraintStates, targetStates, candidates); +// +// // (3) max/max: compute prob1 using the game functions, reuse prob1 states from the MDP precomputation +// result.prob1Max = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true, boost::make_optional(prob1MaxMaxMdp)); +// +// // (4) max/min: compute prob0 using the game functions +// result.prob0Min = storm::utility::graph::performProb0(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true); +// +// // (5) max/min: compute prob1 using the game functions, use prob1 from max/max as the candidate set +// result.prob1Min = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true, boost::make_optional(prob1MaxMaxMdp)); +// } +// } else { + result.prob0Min = storm::utility::graph::performProb0(transitionMatrix, player1RowGrouping, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true); + result.prob1Min = storm::utility::graph::performProb1(transitionMatrix, player1RowGrouping, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true); + result.prob0Max = storm::utility::graph::performProb0(transitionMatrix, player1RowGrouping, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true); + result.prob1Max = storm::utility::graph::performProb1(transitionMatrix, player1RowGrouping, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true); +// } + + STORM_LOG_TRACE("Qualitative precomputation completed."); + STORM_LOG_TRACE("[" << player1Direction << ", " << storm::OptimizationDirection::Minimize << "]: " << result.prob0Min.player1States.getNumberOfSetBits()<< " 'no', " << result.prob1Min.player1States.getNumberOfSetBits() << " 'yes'."); + STORM_LOG_TRACE("[" << player1Direction << ", " << storm::OptimizationDirection::Maximize << "]: " << result.prob0Max.player1States.getNumberOfSetBits() << " 'no', " << result.prob1Max.player1States.getNumberOfSetBits() << " 'yes'."); + + return result; + } + + template + SymbolicQualitativeGameResultMinMax GameBasedMdpModelChecker::computeProb01States(boost::optional> const& previousQualitativeResult, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& transitionMatrixBdd, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates) { - QualitativeGameResultMinMax result; + SymbolicQualitativeGameResultMinMax result; if (reuseQualitativeResults) { // Depending on the player 1 direction, we choose a different order of operations. diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h index 8556edc71..933e0bf5d 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h @@ -9,8 +9,8 @@ #include "storm/storage/SymbolicModelDescription.h" -#include "storm/abstraction/QualitativeGameResult.h" -#include "storm/abstraction/QualitativeGameResultMinMax.h" +#include "storm/abstraction/SymbolicQualitativeGameResult.h" +#include "storm/abstraction/SymbolicQualitativeGameResultMinMax.h" #include "storm/logic/Bound.h" @@ -32,16 +32,21 @@ namespace storm { class MenuGameRefiner; template - class QualitativeGameResultMinMax; + class SymbolicQualitativeGameResultMinMax; template - struct QuantitativeGameResult; + class SymbolicQuantitativeGameResult; + + class ExplicitQualitativeGameResult; + class ExplicitQualitativeGameResultMinMax; } namespace modelchecker { - using storm::abstraction::QualitativeGameResult; - using storm::abstraction::QualitativeGameResultMinMax; + using storm::abstraction::SymbolicQualitativeGameResult; + using storm::abstraction::SymbolicQualitativeGameResultMinMax; + using storm::abstraction::ExplicitQualitativeGameResult; + using storm::abstraction::ExplicitQualitativeGameResultMinMax; template class GameBasedMdpModelChecker : public AbstractModelChecker { @@ -68,8 +73,8 @@ namespace storm { */ std::unique_ptr performGameBasedAbstractionRefinement(Environment const& env, CheckTask const& checkTask, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression); - std::unique_ptr performSymbolicAbstractionSolutionStep(Environment const& env, CheckTask const& checkTask, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& initialStates, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, storm::abstraction::MenuGameRefiner const& refiner, boost::optional>& previousQualitativeResult, boost::optional>& previousMinQuantitativeResult); - std::unique_ptr performExplicitAbstractionSolutionStep(Environment const& env, CheckTask const& checkTask, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& initialStates, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, storm::abstraction::MenuGameRefiner const& refiner); + std::unique_ptr performSymbolicAbstractionSolutionStep(Environment const& env, CheckTask const& checkTask, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& initialStates, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, storm::abstraction::MenuGameRefiner const& refiner, boost::optional>& previousQualitativeResult, boost::optional>& previousMinQuantitativeResult); + std::unique_ptr performExplicitAbstractionSolutionStep(Environment const& env, CheckTask const& checkTask, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& initialStates, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, storm::abstraction::MenuGameRefiner const& refiner, boost::optional& previousQualitativeResult); /*! * Retrieves the initial predicates for the abstraction. @@ -85,7 +90,9 @@ namespace storm { * Performs a qualitative check on the the given game to compute the (player 1) states that have probability * 0 or 1, respectively, to reach a target state and only visiting constraint states before. */ - QualitativeGameResultMinMax computeProb01States(boost::optional> const& previousQualitativeResult, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& transitionMatrixBdd, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates); + SymbolicQualitativeGameResultMinMax computeProb01States(boost::optional> const& previousQualitativeResult, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& transitionMatrixBdd, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates); + + ExplicitQualitativeGameResultMinMax computeProb01States(boost::optional const& previousQualitativeResult, storm::OptimizationDirection player1Direction, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1RowGrouping, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates); void printStatistics(storm::abstraction::MenuGameAbstractor const& abstractor, storm::abstraction::MenuGame const& game) const; @@ -110,6 +117,9 @@ namespace storm { /// A flag indicating whether to reuse the quantitative results. bool reuseQuantitativeResults; + /// The maximal number of abstractions to perform. + uint64_t maximalNumberOfAbstractions; + /// The mode selected for solving the abstraction. storm::settings::modules::AbstractionSettings::SolveMode solveMode; }; diff --git a/src/storm/settings/modules/AbstractionSettings.cpp b/src/storm/settings/modules/AbstractionSettings.cpp index 455cb7da8..341571ef6 100644 --- a/src/storm/settings/modules/AbstractionSettings.cpp +++ b/src/storm/settings/modules/AbstractionSettings.cpp @@ -23,6 +23,7 @@ namespace storm { const std::string AbstractionSettings::reuseResultsOptionName = "reuse"; const std::string AbstractionSettings::restrictToRelevantStatesOptionName = "relevant"; const std::string AbstractionSettings::solveModeOptionName = "solve"; + const std::string AbstractionSettings::maximalAbstractionOptionName = "maxabs"; AbstractionSettings::AbstractionSettings() : ModuleSettings(moduleName) { std::vector methods = {"games", "bisimulation", "bisim"}; @@ -31,6 +32,8 @@ namespace storm { .setDefaultValueString("bisim").build()) .build()); + this->addOption(storm::settings::OptionBuilder(moduleName, maximalAbstractionOptionName, false, "The maximal number of abstraction to perform before solving is aborted.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The maximal abstraction count.").setDefaultValueUnsignedInteger(20000).build()).build()); + std::vector onOff = {"on", "off"}; this->addOption(storm::settings::OptionBuilder(moduleName, useDecompositionOptionName, true, "Sets whether to apply decomposition during the abstraction.") @@ -159,6 +162,10 @@ namespace storm { return ReuseMode::All; } + uint_fast64_t AbstractionSettings::getMaximalAbstractionCount() const { + return this->getOption(maximalAbstractionOptionName).getArgumentByName("count").getValueAsUnsignedInteger(); + } + } } } diff --git a/src/storm/settings/modules/AbstractionSettings.h b/src/storm/settings/modules/AbstractionSettings.h index f8b2e5c93..90a7ea668 100644 --- a/src/storm/settings/modules/AbstractionSettings.h +++ b/src/storm/settings/modules/AbstractionSettings.h @@ -109,6 +109,13 @@ namespace storm { */ SolveMode getSolveMode() const; + /*! + * Retrieves the maximal number of abstractions to perform until giving up on converging. + * + * @return The maximal abstraction count. + */ + uint_fast64_t getMaximalAbstractionCount() const; + const static std::string moduleName; private: @@ -122,6 +129,7 @@ namespace storm { const static std::string reuseResultsOptionName; const static std::string restrictToRelevantStatesOptionName; const static std::string solveModeOptionName; + const static std::string maximalAbstractionOptionName; }; } diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index 729b85b46..d909b76b2 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -603,6 +603,16 @@ namespace storm { return rowGroupIndices.get(); } + template + std::vector::index_type> SparseMatrix::swapRowGroupIndices(std::vector&& newRowGrouping) { + std::vector result; + if (this->rowGroupIndices) { + result = std::move(rowGroupIndices.get()); + rowGroupIndices = std::move(newRowGrouping); + } + return result; + } + template void SparseMatrix::setRowGroupIndices(std::vector const& newRowGroupIndices) { trivialRowGrouping = false; diff --git a/src/storm/storage/SparseMatrix.h b/src/storm/storage/SparseMatrix.h index 4013a7cbf..917ed92e2 100644 --- a/src/storm/storage/SparseMatrix.h +++ b/src/storm/storage/SparseMatrix.h @@ -579,6 +579,12 @@ namespace storm { */ std::vector const& getRowGroupIndices() const; + /*! + * Swaps the grouping of rows of this matrix. + * + * @return The old grouping of rows of this matrix. + */ + std::vector swapRowGroupIndices(std::vector&& newRowGrouping); /*! * Sets the row grouping to the given one. diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index c720483fc..d5d2b408b 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -1083,6 +1083,145 @@ namespace storm { return result; } + template + ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1RowGrouping, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy) { + + ExplicitGameProb01Result result(psiStates, storm::storage::BitVector(transitionMatrix.getRowGroupCount())); + + // Initialize the stack used for the DFS with the states + std::vector stack(psiStates.begin(), psiStates.end()); + + // Perform the actual DFS. + uint_fast64_t currentState; + while (!stack.empty()) { + currentState = stack.back(); + stack.pop_back(); + + // Check which player 2 predecessors of the current player 1 state to add. + for (auto const& player2PredecessorEntry : player1BackwardTransitions.getRow(currentState)) { + uint64_t player2Predecessor = player2PredecessorEntry.getColumn(); + if (!result.player2States.get(player2Predecessor)) { + bool addPlayer2State = false; + if (player2Strategy == OptimizationDirection::Minimize) { + bool allChoicesHavePlayer1State = true; + for (uint64_t row = transitionMatrix.getRowGroupIndices()[player2Predecessor]; row < transitionMatrix.getRowGroupIndices()[player2Predecessor + 1]; ++row) { + bool choiceHasPlayer1State = false; + for (auto const& entry : transitionMatrix.getRow(row)) { + if (result.player1States.get(entry.getColumn())) { + choiceHasPlayer1State = true; + break; + } + } + if (!choiceHasPlayer1State) { + allChoicesHavePlayer1State = false; + } + } + if (allChoicesHavePlayer1State) { + addPlayer2State = true; + } + } else { + addPlayer2State = true; + } + + if (addPlayer2State) { + result.player2States.set(player2Predecessor); + + // Now check whether adding the player 2 state changes something with respect to the + // (single) player 1 predecessor. + uint64_t player1Predecessor = player2BackwardTransitions[player2Predecessor]; + + if (!result.player1States.get(player1Predecessor)) { + bool addPlayer1State = false; + if (player1Strategy == OptimizationDirection::Minimize) { + bool allPlayer2Successors = true; + for (uint64_t player2State = player1RowGrouping[player1Predecessor]; player2State < player1RowGrouping[player1Predecessor + 1]; ++player2State) { + if (!result.player2States.get(player2State)) { + allPlayer2Successors = false; + break; + } + } + if (allPlayer2Successors) { + addPlayer1State = true; + } + } else { + addPlayer1State = true; + } + + if (addPlayer1State) { + result.player1States.set(player1Predecessor); + stack.emplace_back(player1Predecessor); + } + } + } + } + } + } + + // Since we have determined the complements of the desired sets, we need to complement it now. + result.player1States.complement(); + result.player2States.complement(); + + // Generate player 1 strategy if required. + if (producePlayer1Strategy) { + result.player1Strategy = std::vector(result.player1States.size()); + + for (auto player1State : result.player1States) { + if (player1Strategy == storm::OptimizationDirection::Minimize) { + // At least one player 2 successor is a state with probability 0, find it. + bool foundProb0Successor = false; + uint64_t player2State; + for (player2State = player1RowGrouping[player1State]; player2State < player1RowGrouping[player1State + 1]; ++player2State) { + if (result.player2States.get(player2State)) { + result.player1Strategy.get()[player1State] = player2State - player1RowGrouping[player1State]; + foundProb0Successor = true; + break; + } + } + STORM_LOG_ASSERT(foundProb0Successor, "Expected at least one state 2 successor with probability 0."); + result.player1Strategy.get()[player1State] = player2State - player1RowGrouping[player1State]; + } else { + // Since all player 2 successors are states with probability 0, just pick any. + result.player1Strategy.get()[player1State] = 0; + } + } + } + + // Generate player 2 strategy if required. + if (producePlayer2Strategy) { + result.player2Strategy = std::vector(result.player2States.size()); + + for (auto player2State : result.player2States) { + if (player2Strategy == storm::OptimizationDirection::Minimize) { + // At least one distribution only has successors with probability 0, find it. + bool foundProb0SuccessorDistribution = false; + + uint64_t row; + for (row = transitionMatrix.getRowGroupIndices()[player2State]; row < transitionMatrix.getRowGroupIndices()[player2State + 1]; ++row) { + bool distributionHasOnlyProb0Successors = true; + for (auto const& player1SuccessorEntry : transitionMatrix.getRow(row)) { + if (!result.player1States.get(player1SuccessorEntry.getColumn())) { + distributionHasOnlyProb0Successors = false; + break; + } + } + if (distributionHasOnlyProb0Successors) { + foundProb0SuccessorDistribution = true; + break; + } + } + + STORM_LOG_ASSERT(foundProb0SuccessorDistribution, "Expected at least one distribution with only successors with probability 0."); + result.player2Strategy.get()[player2State] = row - transitionMatrix.getRowGroupIndices()[player2State]; + } else { + // Since all player 1 successors are states with probability 0, just pick any. + result.player2Strategy.get()[player2State] = 0; + } + } + } + + return result; + } + template SymbolicGameProb01Result performProb0(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy) { @@ -1150,6 +1289,133 @@ namespace storm { return SymbolicGameProb01Result(player1States, player2States, player1StrategyBdd, player2StrategyBdd); } + template + ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1RowGrouping, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy, boost::optional const& player1Candidates) { + + // During the execution, the two state sets in the result hold the potential player 1/2 states. + ExplicitGameProb01Result result; + if (player1Candidates) { + result = ExplicitGameProb01Result(player1Candidates.get(), storm::storage::BitVector(transitionMatrix.getRowGroupCount())); + } else { + result = ExplicitGameProb01Result(storm::storage::BitVector(phiStates.size(), true), storm::storage::BitVector(transitionMatrix.getRowGroupCount())); + } + + // A flag that governs whether strategies are produced in the current iteration. + bool produceStrategiesInIteration = false; + + // Initialize the stack used for the DFS with the states + std::vector stack; + bool maybeStatesDone = false; + uint_fast64_t maybeStateIterations = 0; + while (!maybeStatesDone || produceStrategiesInIteration) { + storm::storage::BitVector player1Solution = psiStates; + storm::storage::BitVector player2Solution(result.player2States.size()); + + stack.clear(); + stack.insert(stack.end(), psiStates.begin(), psiStates.end()); + + // If we are to produce strategies in this iteration, we prepare some storage. + if (produceStrategiesInIteration) { + if (producePlayer1Strategy) { + result.player1Strategy = std::vector(result.player1States.size()); + } + if (producePlayer2Strategy) { + result.player2Strategy = std::vector(result.player2States.size()); + } + } + + // Perform the actual DFS. + uint_fast64_t currentState; + while (!stack.empty()) { + currentState = stack.back(); + stack.pop_back(); + + for (auto player2PredecessorEntry : player1BackwardTransitions.getRow(currentState)) { + uint64_t player2Predecessor = player2PredecessorEntry.getColumn(); + if (!player2Solution.get(player2PredecessorEntry.getColumn())) { + bool addPlayer2State = player2Strategy == storm::OptimizationDirection::Minimize ? true : false; + + uint64_t validChoice = 0; + for (uint64_t row = transitionMatrix.getRowGroupIndices()[player2Predecessor]; row < transitionMatrix.getRowGroupIndices()[player2Predecessor + 1]; ++row) { + bool choiceHasSolutionSuccessor = false; + bool choiceStaysInMaybeStates = true; + for (auto const& entry : transitionMatrix.getRow(row)) { + if (player1Solution.get(entry.getColumn())) { + choiceHasSolutionSuccessor = true; + } + if (!result.player1States.get(entry.getColumn())) { + choiceStaysInMaybeStates = false; + break; + } + } + + if (choiceHasSolutionSuccessor && choiceStaysInMaybeStates) { + if (player2Strategy == storm::OptimizationDirection::Maximize) { + validChoice = row - transitionMatrix.getRowGroupIndices()[player2Predecessor]; + addPlayer2State = true; + break; + } + } else if (player2Strategy == storm::OptimizationDirection::Minimize) { + addPlayer2State = false; + break; + } + } + + if (addPlayer2State) { + player2Solution.set(player2Predecessor); + if (produceStrategiesInIteration && producePlayer2Strategy) { + result.player2Strategy.get()[player2Predecessor] = validChoice; + } + + // Check whether the addition of the player 2 state changes the state of the (single) + // player 1 predecessor. + uint64_t player1Predecessor = player2BackwardTransitions[player2Predecessor]; + + if (!player1Solution.get(player1Predecessor)) { + bool addPlayer1State = player1Strategy == storm::OptimizationDirection::Minimize ? true : false; + + validChoice = 0; + for (uint64_t player2Successor = player1RowGrouping[player1Predecessor]; player2Successor < player1RowGrouping[player1Predecessor + 1]; ++player2Successor) { + if (player2Solution.get(player2Successor)) { + if (player1Strategy == storm::OptimizationDirection::Maximize) { + validChoice = player2Successor - player1RowGrouping[player1Predecessor]; + addPlayer1State = true; + break; + } + } else if (player1Strategy == storm::OptimizationDirection::Minimize) { + addPlayer1State = false; + break; + } + } + + if (addPlayer1State) { + player1Solution.set(player1Predecessor); + + if (produceStrategiesInIteration && producePlayer1Strategy) { + result.player1Strategy.get()[player1Predecessor] = validChoice; + } + + stack.emplace_back(); + } + } + } + } + } + } + + if (result.player1States == player1Solution) { + maybeStatesDone = true; + result.player2States = player2Solution; + } else { + result.player1States = player1Solution; + result.player2States = player2Solution; + } + ++maybeStateIterations; + } + + return result; + } + template SymbolicGameProb01Result performProb1(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy, boost::optional> const& player1Candidates) { @@ -1424,6 +1690,10 @@ namespace storm { template std::pair performProb01Min(storm::models::sparse::NondeterministicModel> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); #endif + template ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1RowGrouping, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy); + + template ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1RowGrouping, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy, boost::optional const& player1Candidates); + template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix) ; // Instantiations for storm::RationalNumber. diff --git a/src/storm/utility/graph.h b/src/storm/utility/graph.h index cff5887fc..5e1fae518 100644 --- a/src/storm/utility/graph.h +++ b/src/storm/utility/graph.h @@ -615,6 +615,85 @@ namespace storm { template SymbolicGameProb01Result performProb1(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy = false, bool producePlayer2Strategy = false, boost::optional> const& player1Candidates = boost::none); + struct ExplicitGameProb01Result { + ExplicitGameProb01Result() = default; + ExplicitGameProb01Result(uint64_t numberOfPlayer1States, uint64_t numberOfPlayer2States) : player1States(numberOfPlayer1States), player2States(numberOfPlayer2States) { + // Intentionally left empty. + } + + ExplicitGameProb01Result(storm::storage::BitVector const& player1States, storm::storage::BitVector const& player2States, boost::optional> const& player1Strategy = boost::none, boost::optional> const& player2Strategy = boost::none) : player1States(player1States), player2States(player2States), player1Strategy(player1Strategy), player2Strategy(player2Strategy) { + // Intentionally left empty. + } + + bool hasPlayer1Strategy() const { + return static_cast(player1Strategy); + } + + std::vector const& getPlayer1Strategy() const { + return player1Strategy.get(); + } + + boost::optional> const& getOptionalPlayer1Strategy() { + return player1Strategy; + } + + bool hasPlayer2Strategy() const { + return static_cast(player2Strategy); + } + + std::vector const& getPlayer2Strategy() const { + return player2Strategy.get(); + } + + boost::optional> const& getOptionalPlayer2Strategy() { + return player2Strategy; + } + + storm::storage::BitVector const& getPlayer1States() const { + return player1States; + } + + storm::storage::BitVector const& getPlayer2States() const { + return player2States; + } + + storm::storage::BitVector player1States; + storm::storage::BitVector player2States; + boost::optional> player1Strategy; + boost::optional> player2Strategy; + }; + + /*! + * Computes the set of states that have probability 0 given the strategies of the two players. + * + * @param transitionMatrix The transition matrix of the model as a BDD. + * @param player1RowGrouping The row grouping of player 1 states. + * @param player1BackwardTransitions The backward transitions (player 1 to player 2). + * @param player2BackwardTransitions The backward transitions (player 2 to player 1). + * @param phiStates The phi states of the model. + * @param psiStates The psi states of the model. + * @param producePlayer1Strategy A flag indicating whether the strategy of player 1 shall be produced. + * @param producePlayer2Strategy A flag indicating whether the strategy of player 2 shall be produced. + */ + template + ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1RowGrouping, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy = false, bool producePlayer2Strategy = false); + + /*! + * Computes the set of states that have probability 1 given the strategies of the two players. + * + * @param transitionMatrix The transition matrix of the model as a BDD. + * @param player1RowGrouping The row grouping of player 1 states. + * @param player1BackwardTransitions The backward transitions (player 1 to player 2). + * @param player2BackwardTransitions The backward transitions (player 2 to player 1). + * @param phiStates The phi states of the model. + * @param psiStates The psi states of the model. + * @param producePlayer1Strategy A flag indicating whether the strategy of player 1 shall be produced. + * @param producePlayer2Strategy A flag indicating whether the strategy of player 2 shall be produced. + * @param player1Candidates If given, this set constrains the candidates of player 1 states that are considered. + */ + template + ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1RowGrouping, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy = false, bool producePlayer2Strategy = false, boost::optional const& player1Candidates = boost::none); + /*! * Performs a topological sort of the states of the system according to the given transitions. *