diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp index f2feb619d..ce4ddd951 100644 --- a/src/storm-pomdp-cli/storm-pomdp.cpp +++ b/src/storm-pomdp-cli/storm-pomdp.cpp @@ -19,29 +19,18 @@ #include "storm-pomdp/transformer/BinaryPomdpTransformer.h" #include "storm-pomdp/transformer/MakePOMDPCanonic.h" #include "storm-pomdp/analysis/UniqueObservationStates.h" -#include "storm-pomdp/analysis/QualitativeAnalysis.h" +#include "storm-pomdp/analysis/QualitativeAnalysisOnGraphs.h" #include "storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h" #include "storm-pomdp/analysis/FormulaInformation.h" #include "storm-pomdp/analysis/MemlessStrategySearchQualitative.h" #include "storm-pomdp/analysis/QualitativeStrategySearchNaive.h" -template -std::set extractObservations(storm::models::sparse::Pomdp const& pomdp, storm::storage::BitVector const& states) { - // TODO move. - std::set observations; - for(auto state : states) { - observations.insert(pomdp.getObservation(state)); - } - return observations; -} - #include "storm/api/storm.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/utility/NumberTraits.h" #include "storm/utility/Stopwatch.h" #include "storm/utility/SignalHandler.h" -#include "storm/utility/NumberTraits.h" #include "storm/exceptions/UnexpectedException.h" #include "storm/exceptions/NotSupportedException.h" @@ -70,7 +59,7 @@ namespace storm { } } if (pomdpSettings.isQualitativeReductionSet() && formulaInfo.isNonNestedReachabilityProbability()) { - storm::analysis::QualitativeAnalysis qualitativeAnalysis(*pomdp); + storm::analysis::QualitativeAnalysisOnGraphs qualitativeAnalysis(*pomdp); STORM_PRINT_AND_LOG("Computing states with probability 0 ..."); storm::storage::BitVector prob0States = qualitativeAnalysis.analyseProb0(formula.asProbabilityOperatorFormula()); std::cout << prob0States << std::endl; @@ -103,29 +92,10 @@ namespace storm { } } - template - void performQualitativeAnalysis(std::shared_ptr> const& pomdp, storm::pomdp::analysis::FormulaInformation const& formulaInfo, storm::logic::Formula const& formula) { - auto const& pomdpSettings = storm::settings::getModule(); + MemlessSearchOptions fillMemlessSearchOptionsFromSettings() { + storm::pomdp::MemlessSearchOptions options; auto const& qualSettings = storm::settings::getModule(); - STORM_LOG_THROW(formulaInfo.isNonNestedReachabilityProbability(), storm::exceptions::NotSupportedException, "Qualitative memoryless scheduler search is not implemented for this property type."); - - STORM_LOG_TRACE("Run qualitative preprocessing..."); - storm::analysis::QualitativeAnalysis qualitativeAnalysis(*pomdp); - // After preprocessing, this might be done cheaper. - storm::storage::BitVector targetStates = qualitativeAnalysis.analyseProb1(formula.asProbabilityOperatorFormula()); - STORM_LOG_TRACE("target states: " << targetStates); - storm::storage::BitVector surelyNotAlmostSurelyReachTarget = qualitativeAnalysis.analyseProbSmaller1(formula.asProbabilityOperatorFormula()); - std::set targetObservationSet = extractObservations(*pomdp, targetStates); - - storm::expressions::ExpressionManager expressionManager; - std::shared_ptr smtSolverFactory = std::make_shared(); - - uint64_t lookahead = qualSettings.getLookahead(); - if (lookahead == 0) { - lookahead = pomdp->getNumberOfStates(); - } - storm::pomdp::MemlessSearchOptions options; options.onlyDeterministicStrategies = qualSettings.isOnlyDeterministicSet(); uint64_t loglevel = 0; @@ -145,26 +115,41 @@ namespace storm { options.setExportSATCalls(qualSettings.getExportSATCallsPath()); } - if (storm::utility::graph::checkIfECWithChoiceExists(pomdp->getTransitionMatrix(), pomdp->getBackwardTransitions(), ~targetStates & ~surelyNotAlmostSurelyReachTarget, storm::storage::BitVector(pomdp->getNumberOfChoices(), true))) { - options.lookaheadRequired = true; - STORM_LOG_DEBUG("Lookahead required."); - } else { - options.lookaheadRequired = false; - STORM_LOG_DEBUG("No lookahead required."); - } + return options; + } + + template + void performQualitativeAnalysis(std::shared_ptr> const& pomdp, storm::pomdp::analysis::FormulaInformation const& formulaInfo, storm::logic::Formula const& formula) { + auto const& pomdpSettings = storm::settings::getModule(); + auto const& qualSettings = storm::settings::getModule(); + + STORM_LOG_THROW(formulaInfo.isNonNestedReachabilityProbability(), storm::exceptions::NotSupportedException, "Qualitative memoryless scheduler search is not implemented for this property type."); + STORM_LOG_TRACE("Run qualitative preprocessing..."); + storm::analysis::QualitativeAnalysisOnGraphs qualitativeAnalysis(*pomdp); + // After preprocessing, this might be done cheaper. + storm::storage::BitVector targetStates = qualitativeAnalysis.analyseProb1(formula.asProbabilityOperatorFormula()); + storm::storage::BitVector surelyNotAlmostSurelyReachTarget = qualitativeAnalysis.analyseProbSmaller1(formula.asProbabilityOperatorFormula()); + storm::expressions::ExpressionManager expressionManager; + std::shared_ptr smtSolverFactory = std::make_shared(); + + storm::pomdp::MemlessSearchOptions options = fillMemlessSearchOptionsFromSettings(); + uint64_t lookahead = qualSettings.getLookahead(); + if (lookahead == 0) { + lookahead = pomdp->getNumberOfStates(); + } STORM_LOG_TRACE("target states: " << targetStates); if (pomdpSettings.getMemlessSearchMethod() == "ccd-memless") { - storm::pomdp::QualitativeStrategySearchNaive memlessSearch(*pomdp, targetObservationSet, targetStates, surelyNotAlmostSurelyReachTarget, smtSolverFactory); + storm::pomdp::QualitativeStrategySearchNaive memlessSearch(*pomdp, targetStates, surelyNotAlmostSurelyReachTarget, smtSolverFactory); if (qualSettings.isWinningRegionSet()) { STORM_LOG_ERROR("Computing winning regions is not supported by ccd-memless."); } else { memlessSearch.analyzeForInitialStates(lookahead); } } else if (pomdpSettings.getMemlessSearchMethod() == "iterative") { - storm::pomdp::MemlessStrategySearchQualitative search(*pomdp, targetObservationSet, targetStates, surelyNotAlmostSurelyReachTarget, smtSolverFactory, options); + storm::pomdp::MemlessStrategySearchQualitative search(*pomdp, targetStates, surelyNotAlmostSurelyReachTarget, smtSolverFactory, options); if (qualSettings.isWinningRegionSet()) { - search.findNewStrategyForSomeState(lookahead); + search.computeWinningRegion(lookahead); } else { search.analyzeForInitialStates(lookahead); } diff --git a/src/storm-pomdp/analysis/MemlessStrategySearchQualitative.cpp b/src/storm-pomdp/analysis/MemlessStrategySearchQualitative.cpp index ce94c5113..b8f1e6054 100644 --- a/src/storm-pomdp/analysis/MemlessStrategySearchQualitative.cpp +++ b/src/storm-pomdp/analysis/MemlessStrategySearchQualitative.cpp @@ -1,6 +1,8 @@ #include "storm-pomdp/analysis/MemlessStrategySearchQualitative.h" #include "storm/utility/file.h" +#include "storm-pomdp/analysis/QualitativeStrategySearchNaive.h" +#include "storm-pomdp/analysis/QualitativeAnalysis.h" namespace storm { namespace pomdp { @@ -45,14 +47,13 @@ namespace storm { template MemlessStrategySearchQualitative::MemlessStrategySearchQualitative(storm::models::sparse::Pomdp const& pomdp, - std::set const& targetObservationSet, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& surelyReachSinkStates, std::shared_ptr& smtSolverFactory, MemlessSearchOptions const& options) : pomdp(pomdp), surelyReachSinkStates(surelyReachSinkStates), - targetObservations(targetObservationSet), + targetObservations(storm::pomdp::extractObservations(pomdp, targetStates)), targetStates(targetStates), options(options) { @@ -79,8 +80,12 @@ namespace storm { template void MemlessStrategySearchQualitative::initialize(uint64_t k) { STORM_LOG_INFO("Start intializing solver..."); - // TODO fix this - bool lookaheadConstraintsRequired = options.lookaheadRequired; + bool lookaheadConstraintsRequired; + if (options.forceLookahead) { + lookaheadConstraintsRequired = true; + } else { + lookaheadConstraintsRequired = qualitative::isLookaheadRequired(pomdp, targetStates, surelyReachSinkStates); + } if (maxK == std::numeric_limits::max()) { // not initialized at all. // Create some data structures. diff --git a/src/storm-pomdp/analysis/MemlessStrategySearchQualitative.h b/src/storm-pomdp/analysis/MemlessStrategySearchQualitative.h index 05ed91b8d..08b0ffc04 100644 --- a/src/storm-pomdp/analysis/MemlessStrategySearchQualitative.h +++ b/src/storm-pomdp/analysis/MemlessStrategySearchQualitative.h @@ -44,7 +44,7 @@ namespace pomdp { } bool onlyDeterministicStrategies = false; - bool lookaheadRequired = true; + bool forceLookahead = true; private: std::string exportSATcalls = ""; @@ -123,7 +123,6 @@ namespace pomdp { }; MemlessStrategySearchQualitative(storm::models::sparse::Pomdp const& pomdp, - std::set const& targetObservationSet, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& surelyReachSinkStates, @@ -148,7 +147,7 @@ namespace pomdp { } } - void findNewStrategyForSomeState(uint64_t k) { + void computeWinningRegion(uint64_t k) { std::cout << surelyReachSinkStates << std::endl; std::cout << targetStates << std::endl; std::cout << (~surelyReachSinkStates & ~targetStates) << std::endl; @@ -157,6 +156,10 @@ namespace pomdp { stats.totalTimer.stop(); } + WinningRegion const& getLastWinningRegion() const { + return winningRegion; + } + bool analyze(uint64_t k, storm::storage::BitVector const& oneOfTheseStates, storm::storage::BitVector const& allOfTheseStates = storm::storage::BitVector()); Statistics const& getStatistics() const; diff --git a/src/storm-pomdp/analysis/QualitativeAnalysis.cpp b/src/storm-pomdp/analysis/QualitativeAnalysis.cpp index 177367ddc..e69de29bb 100644 --- a/src/storm-pomdp/analysis/QualitativeAnalysis.cpp +++ b/src/storm-pomdp/analysis/QualitativeAnalysis.cpp @@ -1,113 +0,0 @@ -#include "storm-pomdp/analysis/QualitativeAnalysis.h" - -#include "storm/utility/macros.h" -#include "storm/utility/graph.h" -#include "storm/models/sparse/Pomdp.h" -#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" -#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" - -#include "storm/exceptions/InvalidPropertyException.h" -#include "storm/exceptions/NotImplementedException.h" - -namespace storm { - namespace analysis { - - template - QualitativeAnalysis::QualitativeAnalysis(storm::models::sparse::Pomdp const& pomdp) : pomdp(pomdp) { - // Intentionally left empty - } - - template - storm::storage::BitVector QualitativeAnalysis::analyseProb0(storm::logic::ProbabilityOperatorFormula const& formula) const { - return analyseProb0or1(formula, true); - } - - template - storm::storage::BitVector QualitativeAnalysis::analyseProb1(storm::logic::ProbabilityOperatorFormula const& formula) const { - return analyseProb0or1(formula, false); - } - - template - storm::storage::BitVector QualitativeAnalysis::analyseProbSmaller1(storm::logic::ProbabilityOperatorFormula const &formula) const { - STORM_LOG_THROW(formula.hasOptimalityType() || formula.hasBound(), storm::exceptions::InvalidPropertyException, "The formula " << formula << " does not specify whether to minimize or maximize."); - bool minimizes = (formula.hasOptimalityType() && storm::solver::minimize(formula.getOptimalityType())) || (formula.hasBound() && storm::logic::isLowerBound(formula.getBound().comparisonType)); - STORM_LOG_THROW(!minimizes,storm::exceptions::NotImplementedException, "This operation is only supported when maximizing"); - std::shared_ptr subformula = formula.getSubformula().asSharedPointer(); - std::shared_ptr untilSubformula; - // If necessary, convert the subformula to a more general case - if (subformula->isEventuallyFormula()) { - untilSubformula = std::make_shared(storm::logic::Formula::getTrueFormula(), subformula->asEventuallyFormula().getSubformula().asSharedPointer()); - } else if(subformula->isUntilFormula()) { - untilSubformula = std::make_shared(subformula->asUntilFormula()); - } - // The vector is sound, but not necessarily complete! - return ~storm::utility::graph::performProb1E(pomdp.getTransitionMatrix(), pomdp.getTransitionMatrix().getRowGroupIndices(), pomdp.getBackwardTransitions(), checkPropositionalFormula(untilSubformula->getLeftSubformula()), checkPropositionalFormula(untilSubformula->getRightSubformula())); - } - - template - storm::storage::BitVector QualitativeAnalysis::analyseProb0or1(storm::logic::ProbabilityOperatorFormula const& formula, bool prob0) const { - // check whether the property is minimizing or maximizing - STORM_LOG_THROW(pomdp.isCanonic(), storm::exceptions::IllegalArgumentException, "POMDP needs to be canonic"); - STORM_LOG_THROW(formula.hasOptimalityType() || formula.hasBound(), storm::exceptions::InvalidPropertyException, "The formula " << formula << " does not specify whether to minimize or maximize."); - bool minimizes = (formula.hasOptimalityType() && storm::solver::minimize(formula.getOptimalityType())) || (formula.hasBound() && storm::logic::isLowerBound(formula.getBound().comparisonType)); - - std::shared_ptr subformula = formula.getSubformula().asSharedPointer(); - // If necessary, convert the subformula to a more general case - if (subformula->isEventuallyFormula()) { - subformula = std::make_shared(storm::logic::Formula::getTrueFormula(), subformula->asEventuallyFormula().getSubformula().asSharedPointer()); - } - - if (subformula->isUntilFormula()) { - if (minimizes && prob0) { - return analyseProb0Min(subformula->asUntilFormula()); - } else if (minimizes && !prob0){ - return analyseProb1Min(subformula->asUntilFormula()); - } else if (!minimizes && prob0){ - return analyseProb0Max(subformula->asUntilFormula()); - } else if (!minimizes && !prob0){ - return analyseProb1Max(subformula->asUntilFormula()); - } - } - STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Prob0or1 analysis is not supported for the property " << formula); - } - - - template - storm::storage::BitVector QualitativeAnalysis::analyseProb0Max(storm::logic::UntilFormula const& formula) const { - return storm::utility::graph::performProb0A(pomdp.getBackwardTransitions(), checkPropositionalFormula(formula.getLeftSubformula()), checkPropositionalFormula(formula.getRightSubformula())); - } - - template - storm::storage::BitVector QualitativeAnalysis::analyseProb0Min(storm::logic::UntilFormula const& formula) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Prob0 analysis is currently not implemented for minimizing properties."); - } - - template - storm::storage::BitVector QualitativeAnalysis::analyseProb1Max(storm::logic::UntilFormula const& formula) const { - // We consider the states that satisfy the formula with prob.1 under arbitrary schedulers as goal states. - storm::storage::BitVector goalStates = storm::utility::graph::performProb1A(pomdp.getTransitionMatrix(), pomdp.getTransitionMatrix().getRowGroupIndices(), pomdp.getBackwardTransitions(), checkPropositionalFormula(formula.getLeftSubformula()), checkPropositionalFormula(formula.getRightSubformula())); - STORM_LOG_TRACE("Prob1A states according to MDP: " << goalStates); - // Now find a set of observations such that there is a memoryless scheduler inducing prob. 1 for each state whose observation is in the set. - return goalStates; - - } - - template - storm::storage::BitVector QualitativeAnalysis::analyseProb1Min(storm::logic::UntilFormula const& formula) const { - return storm::utility::graph::performProb1A(pomdp.getTransitionMatrix(), pomdp.getTransitionMatrix().getRowGroupIndices(), pomdp.getBackwardTransitions(), checkPropositionalFormula(formula.getLeftSubformula()), checkPropositionalFormula(formula.getRightSubformula())); - } - - template - storm::storage::BitVector QualitativeAnalysis::checkPropositionalFormula(storm::logic::Formula const& propositionalFormula) const { - storm::modelchecker::SparsePropositionalModelChecker> mc(pomdp); - STORM_LOG_THROW(mc.canHandle(propositionalFormula), storm::exceptions::InvalidPropertyException, "Propositional model checker can not handle formula " << propositionalFormula); - return mc.check(propositionalFormula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); - } - - - template class QualitativeAnalysis; - - template - class QualitativeAnalysis; - } -} \ No newline at end of file diff --git a/src/storm-pomdp/analysis/QualitativeAnalysis.h b/src/storm-pomdp/analysis/QualitativeAnalysis.h index e15f6161d..528b65cae 100644 --- a/src/storm-pomdp/analysis/QualitativeAnalysis.h +++ b/src/storm-pomdp/analysis/QualitativeAnalysis.h @@ -1,27 +1,19 @@ #include "storm/models/sparse/Pomdp.h" -#include "storm/storage/BitVector.h" -#include "storm/logic/Formulas.h" -namespace storm { - namespace analysis { - template - class QualitativeAnalysis { - public: +#include "storm/utility/graph.h" - QualitativeAnalysis(storm::models::sparse::Pomdp const& pomdp); - storm::storage::BitVector analyseProb0(storm::logic::ProbabilityOperatorFormula const& formula) const; - storm::storage::BitVector analyseProb1(storm::logic::ProbabilityOperatorFormula const& formula) const; - storm::storage::BitVector analyseProbSmaller1(storm::logic::ProbabilityOperatorFormula const& formula) const; - private: - storm::storage::BitVector analyseProb0or1(storm::logic::ProbabilityOperatorFormula const& formula, bool prob0) const; - storm::storage::BitVector analyseProb0Max(storm::logic::UntilFormula const& formula) const; - storm::storage::BitVector analyseProb0Min(storm::logic::UntilFormula const& formula) const; - storm::storage::BitVector analyseProb1Max(storm::logic::UntilFormula const& formula) const; - storm::storage::BitVector analyseProb1Min(storm::logic::UntilFormula const& formula) const; - - storm::storage::BitVector checkPropositionalFormula(storm::logic::Formula const& propositionalFormula) const; - - storm::models::sparse::Pomdp const& pomdp; - }; +namespace storm { + namespace pomdp { + namespace qualitative { + template + bool isLookaheadRequired(storm::models::sparse::Pomdp const& pomdp, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& surelyReachSinkStates) { + if (storm::utility::graph::checkIfECWithChoiceExists(pomdp.getTransitionMatrix(), pomdp.getBackwardTransitions(), ~targetStates & ~surelyReachSinkStates, storm::storage::BitVector(pomdp.getNumberOfChoices(), true))) { + STORM_LOG_DEBUG("Lookahead (possibly) required."); + return true; + } else { + STORM_LOG_DEBUG("No lookahead required."); + return false; + } + } + } } } - diff --git a/src/storm-pomdp/analysis/QualitativeAnalysisOnGraphs.cpp b/src/storm-pomdp/analysis/QualitativeAnalysisOnGraphs.cpp new file mode 100644 index 000000000..ade39ada0 --- /dev/null +++ b/src/storm-pomdp/analysis/QualitativeAnalysisOnGraphs.cpp @@ -0,0 +1,113 @@ +#include "storm-pomdp/analysis/QualitativeAnalysisOnGraphs.h" + +#include "storm/utility/macros.h" +#include "storm/utility/graph.h" +#include "storm/models/sparse/Pomdp.h" +#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" +#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" + +#include "storm/exceptions/InvalidPropertyException.h" +#include "storm/exceptions/NotImplementedException.h" + +namespace storm { + namespace analysis { + + template + QualitativeAnalysisOnGraphs::QualitativeAnalysisOnGraphs(storm::models::sparse::Pomdp const& pomdp) : pomdp(pomdp) { + // Intentionally left empty + } + + template + storm::storage::BitVector QualitativeAnalysisOnGraphs::analyseProb0(storm::logic::ProbabilityOperatorFormula const& formula) const { + return analyseProb0or1(formula, true); + } + + template + storm::storage::BitVector QualitativeAnalysisOnGraphs::analyseProb1(storm::logic::ProbabilityOperatorFormula const& formula) const { + return analyseProb0or1(formula, false); + } + + template + storm::storage::BitVector QualitativeAnalysisOnGraphs::analyseProbSmaller1(storm::logic::ProbabilityOperatorFormula const &formula) const { + STORM_LOG_THROW(formula.hasOptimalityType() || formula.hasBound(), storm::exceptions::InvalidPropertyException, "The formula " << formula << " does not specify whether to minimize or maximize."); + bool minimizes = (formula.hasOptimalityType() && storm::solver::minimize(formula.getOptimalityType())) || (formula.hasBound() && storm::logic::isLowerBound(formula.getBound().comparisonType)); + STORM_LOG_THROW(!minimizes,storm::exceptions::NotImplementedException, "This operation is only supported when maximizing"); + std::shared_ptr subformula = formula.getSubformula().asSharedPointer(); + std::shared_ptr untilSubformula; + // If necessary, convert the subformula to a more general case + if (subformula->isEventuallyFormula()) { + untilSubformula = std::make_shared(storm::logic::Formula::getTrueFormula(), subformula->asEventuallyFormula().getSubformula().asSharedPointer()); + } else if(subformula->isUntilFormula()) { + untilSubformula = std::make_shared(subformula->asUntilFormula()); + } + // The vector is sound, but not necessarily complete! + return ~storm::utility::graph::performProb1E(pomdp.getTransitionMatrix(), pomdp.getTransitionMatrix().getRowGroupIndices(), pomdp.getBackwardTransitions(), checkPropositionalFormula(untilSubformula->getLeftSubformula()), checkPropositionalFormula(untilSubformula->getRightSubformula())); + } + + template + storm::storage::BitVector QualitativeAnalysisOnGraphs::analyseProb0or1(storm::logic::ProbabilityOperatorFormula const& formula, bool prob0) const { + // check whether the property is minimizing or maximizing + STORM_LOG_THROW(pomdp.isCanonic(), storm::exceptions::IllegalArgumentException, "POMDP needs to be canonic"); + STORM_LOG_THROW(formula.hasOptimalityType() || formula.hasBound(), storm::exceptions::InvalidPropertyException, "The formula " << formula << " does not specify whether to minimize or maximize."); + bool minimizes = (formula.hasOptimalityType() && storm::solver::minimize(formula.getOptimalityType())) || (formula.hasBound() && storm::logic::isLowerBound(formula.getBound().comparisonType)); + + std::shared_ptr subformula = formula.getSubformula().asSharedPointer(); + // If necessary, convert the subformula to a more general case + if (subformula->isEventuallyFormula()) { + subformula = std::make_shared(storm::logic::Formula::getTrueFormula(), subformula->asEventuallyFormula().getSubformula().asSharedPointer()); + } + + if (subformula->isUntilFormula()) { + if (minimizes && prob0) { + return analyseProb0Min(subformula->asUntilFormula()); + } else if (minimizes && !prob0){ + return analyseProb1Min(subformula->asUntilFormula()); + } else if (!minimizes && prob0){ + return analyseProb0Max(subformula->asUntilFormula()); + } else if (!minimizes && !prob0){ + return analyseProb1Max(subformula->asUntilFormula()); + } + } + STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Prob0or1 analysis is not supported for the property " << formula); + } + + + template + storm::storage::BitVector QualitativeAnalysisOnGraphs::analyseProb0Max(storm::logic::UntilFormula const& formula) const { + return storm::utility::graph::performProb0A(pomdp.getBackwardTransitions(), checkPropositionalFormula(formula.getLeftSubformula()), checkPropositionalFormula(formula.getRightSubformula())); + } + + template + storm::storage::BitVector QualitativeAnalysisOnGraphs::analyseProb0Min(storm::logic::UntilFormula const& formula) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Prob0 analysis is currently not implemented for minimizing properties."); + } + + template + storm::storage::BitVector QualitativeAnalysisOnGraphs::analyseProb1Max(storm::logic::UntilFormula const& formula) const { + // We consider the states that satisfy the formula with prob.1 under arbitrary schedulers as goal states. + storm::storage::BitVector goalStates = storm::utility::graph::performProb1A(pomdp.getTransitionMatrix(), pomdp.getTransitionMatrix().getRowGroupIndices(), pomdp.getBackwardTransitions(), checkPropositionalFormula(formula.getLeftSubformula()), checkPropositionalFormula(formula.getRightSubformula())); + STORM_LOG_TRACE("Prob1A states according to MDP: " << goalStates); + // Now find a set of observations such that there is a memoryless scheduler inducing prob. 1 for each state whose observation is in the set. + return goalStates; + + } + + template + storm::storage::BitVector QualitativeAnalysisOnGraphs::analyseProb1Min(storm::logic::UntilFormula const& formula) const { + return storm::utility::graph::performProb1A(pomdp.getTransitionMatrix(), pomdp.getTransitionMatrix().getRowGroupIndices(), pomdp.getBackwardTransitions(), checkPropositionalFormula(formula.getLeftSubformula()), checkPropositionalFormula(formula.getRightSubformula())); + } + + template + storm::storage::BitVector QualitativeAnalysisOnGraphs::checkPropositionalFormula(storm::logic::Formula const& propositionalFormula) const { + storm::modelchecker::SparsePropositionalModelChecker> mc(pomdp); + STORM_LOG_THROW(mc.canHandle(propositionalFormula), storm::exceptions::InvalidPropertyException, "Propositional model checker can not handle formula " << propositionalFormula); + return mc.check(propositionalFormula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); + } + + + template class QualitativeAnalysisOnGraphs; + + template + class QualitativeAnalysisOnGraphs; + } +} \ No newline at end of file diff --git a/src/storm-pomdp/analysis/QualitativeAnalysisOnGraphs.h b/src/storm-pomdp/analysis/QualitativeAnalysisOnGraphs.h new file mode 100644 index 000000000..f9f14dfd4 --- /dev/null +++ b/src/storm-pomdp/analysis/QualitativeAnalysisOnGraphs.h @@ -0,0 +1,27 @@ +#include "storm/models/sparse/Pomdp.h" +#include "storm/storage/BitVector.h" +#include "storm/logic/Formulas.h" +namespace storm { + namespace analysis { + template + class QualitativeAnalysisOnGraphs { + public: + + QualitativeAnalysisOnGraphs(storm::models::sparse::Pomdp const& pomdp); + storm::storage::BitVector analyseProb0(storm::logic::ProbabilityOperatorFormula const& formula) const; + storm::storage::BitVector analyseProb1(storm::logic::ProbabilityOperatorFormula const& formula) const; + storm::storage::BitVector analyseProbSmaller1(storm::logic::ProbabilityOperatorFormula const& formula) const; + private: + storm::storage::BitVector analyseProb0or1(storm::logic::ProbabilityOperatorFormula const& formula, bool prob0) const; + storm::storage::BitVector analyseProb0Max(storm::logic::UntilFormula const& formula) const; + storm::storage::BitVector analyseProb0Min(storm::logic::UntilFormula const& formula) const; + storm::storage::BitVector analyseProb1Max(storm::logic::UntilFormula const& formula) const; + storm::storage::BitVector analyseProb1Min(storm::logic::UntilFormula const& formula) const; + + storm::storage::BitVector checkPropositionalFormula(storm::logic::Formula const& propositionalFormula) const; + + storm::models::sparse::Pomdp const& pomdp; + }; + } +} + diff --git a/src/storm-pomdp/analysis/QualitativeStrategySearchNaive.h b/src/storm-pomdp/analysis/QualitativeStrategySearchNaive.h index 4fee165f3..8797dfbe5 100644 --- a/src/storm-pomdp/analysis/QualitativeStrategySearchNaive.h +++ b/src/storm-pomdp/analysis/QualitativeStrategySearchNaive.h @@ -9,6 +9,16 @@ namespace storm { namespace pomdp { + template + std::set extractObservations(storm::models::sparse::Pomdp const& pomdp, storm::storage::BitVector const& states) { + // TODO move. + std::set observations; + for(auto state : states) { + observations.insert(pomdp.getObservation(state)); + } + return observations; + } + template class QualitativeStrategySearchNaive { // Implements to the Chatterjee, Chmelik, Davies (AAAI-16) paper. @@ -23,12 +33,11 @@ namespace storm { public: QualitativeStrategySearchNaive(storm::models::sparse::Pomdp const& pomdp, - std::set const& targetObservationSet, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& surelyReachSinkStates, std::shared_ptr& smtSolverFactory) : pomdp(pomdp), - targetObservations(targetObservationSet), + targetObservations(extractObservations(pomdp, targetStates)), targetStates(targetStates), surelyReachSinkStates(surelyReachSinkStates) { this->expressionManager = std::make_shared();