cleaning code

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<typename ValueType>
-std::set<uint32_t> extractObservations(storm::models::sparse::Pomdp<ValueType> const& pomdp, storm::storage::BitVector const& states) {
-    // TODO move.
-    std::set<uint32_t> 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<ValueType> qualitativeAnalysis(*pomdp);
+                    storm::analysis::QualitativeAnalysisOnGraphs<ValueType> 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<typename ValueType>
-            void performQualitativeAnalysis(std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> const& pomdp, storm::pomdp::analysis::FormulaInformation const& formulaInfo, storm::logic::Formula const& formula) {
-                auto const& pomdpSettings = storm::settings::getModule<storm::settings::modules::POMDPSettings>();
+            MemlessSearchOptions fillMemlessSearchOptionsFromSettings() {
+                storm::pomdp::MemlessSearchOptions options;
                 auto const& qualSettings = storm::settings::getModule<storm::settings::modules::QualitativePOMDPAnalysisSettings>();
 
-                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<ValueType> 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<uint32_t> targetObservationSet = extractObservations(*pomdp, targetStates);
-
-                storm::expressions::ExpressionManager expressionManager;
-                std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
-
-                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<typename ValueType>
+            void performQualitativeAnalysis(std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> const& pomdp, storm::pomdp::analysis::FormulaInformation const& formulaInfo, storm::logic::Formula const& formula) {
+                auto const& pomdpSettings = storm::settings::getModule<storm::settings::modules::POMDPSettings>();
+                auto const& qualSettings = storm::settings::getModule<storm::settings::modules::QualitativePOMDPAnalysisSettings>();
+
+                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<ValueType> 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<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
+
+                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<ValueType> memlessSearch(*pomdp, targetObservationSet, targetStates, surelyNotAlmostSurelyReachTarget, smtSolverFactory);
+                    storm::pomdp::QualitativeStrategySearchNaive<ValueType> 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<ValueType> search(*pomdp, targetObservationSet, targetStates, surelyNotAlmostSurelyReachTarget, smtSolverFactory, options);
+                    storm::pomdp::MemlessStrategySearchQualitative<ValueType> search(*pomdp, targetStates, surelyNotAlmostSurelyReachTarget, smtSolverFactory, options);
                     if (qualSettings.isWinningRegionSet()) {
-                        search.findNewStrategyForSomeState(lookahead);
+                        search.computeWinningRegion(lookahead);
                     } else {
                         search.analyzeForInitialStates(lookahead);
                     }

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 <typename ValueType>
         MemlessStrategySearchQualitative<ValueType>::MemlessStrategySearchQualitative(storm::models::sparse::Pomdp<ValueType> const& pomdp,
-                                                                                      std::set<uint32_t> const& targetObservationSet,
                     storm::storage::BitVector const& targetStates,
                     storm::storage::BitVector const& surelyReachSinkStates,
                     std::shared_ptr<storm::utility::solver::SmtSolverFactory>& 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 <typename ValueType>
         void MemlessStrategySearchQualitative<ValueType>::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<uint64_t>::max()) {
                 // not initialized at all.
                 // Create some data structures.

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<ValueType> const& pomdp,
-                                         std::set<uint32_t> 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;

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<typename ValueType>
-        QualitativeAnalysis<ValueType>::QualitativeAnalysis(storm::models::sparse::Pomdp<ValueType> const& pomdp) : pomdp(pomdp) {
-            // Intentionally left empty
-        }
-    
-        template<typename ValueType>
-        storm::storage::BitVector QualitativeAnalysis<ValueType>::analyseProb0(storm::logic::ProbabilityOperatorFormula const& formula) const {
-            return analyseProb0or1(formula, true);
-        }
-        
-        template<typename ValueType>
-        storm::storage::BitVector QualitativeAnalysis<ValueType>::analyseProb1(storm::logic::ProbabilityOperatorFormula const& formula) const {
-            return analyseProb0or1(formula, false);
-        }
-
-        template<typename ValueType>
-        storm::storage::BitVector QualitativeAnalysis<ValueType>::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<storm::logic::Formula const> subformula = formula.getSubformula().asSharedPointer();
-            std::shared_ptr<storm::logic::UntilFormula> untilSubformula;
-            // If necessary, convert the subformula to a more general case
-            if (subformula->isEventuallyFormula()) {
-                untilSubformula = std::make_shared<storm::logic::UntilFormula>(storm::logic::Formula::getTrueFormula(), subformula->asEventuallyFormula().getSubformula().asSharedPointer());
-            } else if(subformula->isUntilFormula()) {
-                untilSubformula = std::make_shared<storm::logic::UntilFormula>(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<typename ValueType>
-        storm::storage::BitVector QualitativeAnalysis<ValueType>::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<storm::logic::Formula const> subformula = formula.getSubformula().asSharedPointer();
-            // If necessary, convert the subformula to a more general case
-            if (subformula->isEventuallyFormula()) {
-                subformula = std::make_shared<storm::logic::UntilFormula>(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<typename ValueType>
-        storm::storage::BitVector QualitativeAnalysis<ValueType>::analyseProb0Max(storm::logic::UntilFormula const& formula) const {
-            return storm::utility::graph::performProb0A(pomdp.getBackwardTransitions(), checkPropositionalFormula(formula.getLeftSubformula()), checkPropositionalFormula(formula.getRightSubformula()));
-        }
-        
-        template<typename ValueType>
-        storm::storage::BitVector QualitativeAnalysis<ValueType>::analyseProb0Min(storm::logic::UntilFormula const& formula) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Prob0 analysis is currently not implemented for minimizing properties.");
-        }
-        
-        template<typename ValueType>
-        storm::storage::BitVector QualitativeAnalysis<ValueType>::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<typename ValueType>
-        storm::storage::BitVector QualitativeAnalysis<ValueType>::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<typename ValueType>
-        storm::storage::BitVector QualitativeAnalysis<ValueType>::checkPropositionalFormula(storm::logic::Formula const& propositionalFormula) const {
-            storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Mdp<ValueType>> 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<storm::RationalNumber>;
-
-        template
-        class QualitativeAnalysis<double>;
-    }
-}

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<typename ValueType>
-        class QualitativeAnalysis {
-        public:
+#include "storm/utility/graph.h"
 
-            QualitativeAnalysis(storm::models::sparse::Pomdp<ValueType> 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<ValueType> const& pomdp;
-        };
+namespace storm {
+    namespace pomdp {
+        namespace qualitative {
+            template<typename ValueType>
+            bool isLookaheadRequired(storm::models::sparse::Pomdp<ValueType> 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;
+                }
+            }
+        }
     }
 }
-

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<typename ValueType>
+        QualitativeAnalysisOnGraphs<ValueType>::QualitativeAnalysisOnGraphs(storm::models::sparse::Pomdp<ValueType> const& pomdp) : pomdp(pomdp) {
+            // Intentionally left empty
+        }
+
+        template<typename ValueType>
+        storm::storage::BitVector QualitativeAnalysisOnGraphs<ValueType>::analyseProb0(storm::logic::ProbabilityOperatorFormula const& formula) const {
+            return analyseProb0or1(formula, true);
+        }
+
+        template<typename ValueType>
+        storm::storage::BitVector QualitativeAnalysisOnGraphs<ValueType>::analyseProb1(storm::logic::ProbabilityOperatorFormula const& formula) const {
+            return analyseProb0or1(formula, false);
+        }
+
+        template<typename ValueType>
+        storm::storage::BitVector QualitativeAnalysisOnGraphs<ValueType>::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<storm::logic::Formula const> subformula = formula.getSubformula().asSharedPointer();
+            std::shared_ptr<storm::logic::UntilFormula> untilSubformula;
+            // If necessary, convert the subformula to a more general case
+            if (subformula->isEventuallyFormula()) {
+                untilSubformula = std::make_shared<storm::logic::UntilFormula>(storm::logic::Formula::getTrueFormula(), subformula->asEventuallyFormula().getSubformula().asSharedPointer());
+            } else if(subformula->isUntilFormula()) {
+                untilSubformula = std::make_shared<storm::logic::UntilFormula>(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<typename ValueType>
+        storm::storage::BitVector QualitativeAnalysisOnGraphs<ValueType>::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<storm::logic::Formula const> subformula = formula.getSubformula().asSharedPointer();
+            // If necessary, convert the subformula to a more general case
+            if (subformula->isEventuallyFormula()) {
+                subformula = std::make_shared<storm::logic::UntilFormula>(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<typename ValueType>
+        storm::storage::BitVector QualitativeAnalysisOnGraphs<ValueType>::analyseProb0Max(storm::logic::UntilFormula const& formula) const {
+            return storm::utility::graph::performProb0A(pomdp.getBackwardTransitions(), checkPropositionalFormula(formula.getLeftSubformula()), checkPropositionalFormula(formula.getRightSubformula()));
+        }
+
+        template<typename ValueType>
+        storm::storage::BitVector QualitativeAnalysisOnGraphs<ValueType>::analyseProb0Min(storm::logic::UntilFormula const& formula) const {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Prob0 analysis is currently not implemented for minimizing properties.");
+        }
+
+        template<typename ValueType>
+        storm::storage::BitVector QualitativeAnalysisOnGraphs<ValueType>::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<typename ValueType>
+        storm::storage::BitVector QualitativeAnalysisOnGraphs<ValueType>::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<typename ValueType>
+        storm::storage::BitVector QualitativeAnalysisOnGraphs<ValueType>::checkPropositionalFormula(storm::logic::Formula const& propositionalFormula) const {
+            storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Mdp<ValueType>> 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<storm::RationalNumber>;
+
+        template
+        class QualitativeAnalysisOnGraphs<double>;
+    }
+}

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<typename ValueType>
+        class QualitativeAnalysisOnGraphs {
+        public:
+
+            QualitativeAnalysisOnGraphs(storm::models::sparse::Pomdp<ValueType> 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<ValueType> const& pomdp;
+        };
+    }
+}
+

src/storm-pomdp/analysis/QualitativeStrategySearchNaive.h

@@ -9,6 +9,16 @@
 namespace storm {
     namespace pomdp {
 
+        template<typename ValueType>
+        std::set<uint32_t> extractObservations(storm::models::sparse::Pomdp<ValueType> const& pomdp, storm::storage::BitVector const& states) {
+            // TODO move.
+            std::set<uint32_t> observations;
+            for(auto state : states) {
+                observations.insert(pomdp.getObservation(state));
+            }
+            return observations;
+        }
+
         template<typename ValueType>
         class QualitativeStrategySearchNaive {
             // Implements  to the Chatterjee, Chmelik, Davies (AAAI-16) paper.
@@ -23,12 +33,11 @@ namespace storm {
 
         public:
             QualitativeStrategySearchNaive(storm::models::sparse::Pomdp<ValueType> const& pomdp,
-                                             std::set<uint32_t> const& targetObservationSet,
                                              storm::storage::BitVector const& targetStates,
                                              storm::storage::BitVector const& surelyReachSinkStates,
                                              std::shared_ptr<storm::utility::solver::SmtSolverFactory>& smtSolverFactory) :
                     pomdp(pomdp),
-                    targetObservations(targetObservationSet),
+                    targetObservations(extractObservations(pomdp, targetStates)),
                     targetStates(targetStates),
                     surelyReachSinkStates(surelyReachSinkStates) {
                 this->expressionManager = std::make_shared<storm::expressions::ExpressionManager>();