reworked the interface to qualitative analysis of POMDPs

CHANGELOG.md

@@ -16,6 +16,7 @@ Version 1.5.x
 - `storm-counterexamples`: fix when computing multiple counterexamples in debug mode
 - `storm-dft`: Renamed setting `--show-dft-stats` to `dft-statistics` and added approximation information to statistics.
 - `storm-pomdp`: Implemented approximation algorithms that explore (a discritization of) the belief MDP, allowing to compute safe lower- and upper bounds for a given property.
+- `storm-pomdp`: Implemented almost-sure reachability computations: graph-based, one-shot SAT-based, and iterative SAT-based
 
 ## Version 1.5.1 (2020/03)
 - Jani models are now parsed using exact arithmetic.

src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp

@@ -28,9 +28,8 @@ namespace storm {
             std::vector<std::string> fscModes = {"standard", "simple-linear", "simple-linear-inverse"};
             const std::string transformBinaryOption = "transformbinary";
             const std::string transformSimpleOption = "transformsimple";
-            const std::string memlessSearchOption = "memlesssearch";
-            std::vector<std::string> memlessSearchMethods = {"none", "ccd-memless", "ccd-memory", "iterative"};
             const std::string checkFullyObservableOption = "check-fully-observable";
+            const std::string isQualitativeOption = "qualitative-analysis";
 
             POMDPSettings::POMDPSettings() : ModuleSettings(moduleName) {
                 this->addOption(storm::settings::OptionBuilder(moduleName, noCanonicOption, false, "If this is set, actions will not be ordered canonically. Could yield incorrect results.").build());
@@ -45,9 +44,8 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, transformBinaryOption, false, "Transforms the pomdp to a binary pomdp.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, transformSimpleOption, false, "Transforms the pomdp to a binary and simple pomdp.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, beliefExplorationOption, false,"Analyze the POMDP by exploring the belief state-space.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "Sets whether lower, upper, or interval result bounds are computed.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(beliefExplorationModes)).setDefaultValueString("both").makeOptional().build()).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, memlessSearchOption, false, "Search for a qualitative memoryless scheuler").addArgument(storm::settings::ArgumentBuilder::createStringArgument("method", "method name").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(memlessSearchMethods)).setDefaultValueString("none").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, checkFullyObservableOption, false, "Performs standard model checking on the underlying MDP").build());
-
+                this->addOption(storm::settings::OptionBuilder(moduleName, isQualitativeOption, false, "Sets the option qualitative analysis").build());
             }
 
             bool POMDPSettings::isNoCanonicSet() const {
@@ -92,18 +90,15 @@ namespace storm {
                 return isBeliefExplorationSet() && (arg == "unfold" || arg == "both");
             }
 
-            bool POMDPSettings::isMemlessSearchSet() const {
-                return this->getOption(memlessSearchOption).getHasOptionBeenSet();
-            }
-
             bool POMDPSettings::isCheckFullyObservableSet() const {
                 return this->getOption(checkFullyObservableOption).getHasOptionBeenSet();
             }
 
-            std::string POMDPSettings::getMemlessSearchMethod() const {
-                return this->getOption(memlessSearchOption).getArgumentByName("method").getValueAsString();
+            bool POMDPSettings::isQualitativeAnalysisSet() const {
+                return this->getOption(isQualitativeOption).getHasOptionBeenSet();
             }
 
+
             uint64_t POMDPSettings::getMemoryBound() const {
                 return this->getOption(memoryBoundOption).getArgumentByName("bound").getValueAsUnsignedInteger();
             }

src/storm-pomdp-cli/settings/modules/POMDPSettings.h

@@ -35,9 +35,8 @@ namespace storm {
                 bool isSelfloopReductionSet() const;
                 bool isTransformSimpleSet() const;
                 bool isTransformBinarySet() const;
-                bool isMemlessSearchSet() const;
                 bool isCheckFullyObservableSet() const;
-                std::string getMemlessSearchMethod() const;
+                bool isQualitativeAnalysisSet() const;
                 std::string getFscApplicationTypeString() const;
                 uint64_t getMemoryBound() const;
 

src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.cpp

@@ -18,19 +18,38 @@ namespace storm {
             const std::string onlyDeterministicOption = "onlydeterministic";
             const std::string winningRegionOption = "winningregion";
             const std::string validationLevel = "validate";
+            const std::string lookaheadTypeOption = "lookaheadtype";
+            const std::string expensiveStatsOption = "allstats";
+            const std::string printWinningRegionOption = "printwinningregion";
+            const std::string exportWinningRegionOption = "exportwinningregion";
+            const std::string preventGraphPreprocessing = "nographprocessing";
+            const std::string memlessSearchOption = "memlesssearch";
+            std::vector<std::string> memlessSearchMethods = {"one-shot", "iterative"};
+
 
 
             QualitativePOMDPAnalysisSettings::QualitativePOMDPAnalysisSettings() : ModuleSettings(moduleName) {
-                this->addOption(storm::settings::OptionBuilder(moduleName, exportSATCallsOption, false, "Export the SAT calls?.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("path", "The name of the file to which to write the model.").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, memlessSearchOption, false, "Search for a qualitative memoryless scheduler").addArgument(storm::settings::ArgumentBuilder::createStringArgument("method", "method name").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(memlessSearchMethods)).setDefaultValueString("iterative").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, exportSATCallsOption, false, "Export the SAT calls?.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createStringArgument("path", "The name of the path to which to write the models.").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, lookaheadHorizonOption, false, "In reachability in combination with a discrete ranking function, a lookahead is necessary.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("bound", "The lookahead. Use 0 for the number of states.").setDefaultValueUnsignedInteger(0).build()).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, onlyDeterministicOption, false, "Search only for deterministic schedulers").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, onlyDeterministicOption, false, "Search only for deterministic schedulers").setIsAdvanced().build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, winningRegionOption, false, "Search for the winning region").build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, validationLevel, false, "Validate algorithm during runtime (for debugging)").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("level", "how regular to apply this validation. Use 0 for never, 1 for the end, and >=2 within computation steps.").setDefaultValueUnsignedInteger(0).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, lookaheadTypeOption, false, "What type to use for the ranking function").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createStringArgument("type", "The type.").setDefaultValueString("real").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator({"bool", "int", "real"})).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, validationLevel, true, "Validate algorithm during runtime (for debugging)").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("level", "how regular to apply this validation. Use 0 for never, 1 for the end, and >=2 within computation steps.").setDefaultValueUnsignedInteger(0).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, expensiveStatsOption, true, "Compute all stats, even if this is expensive.").setIsAdvanced().build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, printWinningRegionOption, false, "Print Winning Region").setIsAdvanced().build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, exportWinningRegionOption, false, "Export the winning region.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createStringArgument("path", "The name of the file to which to write the winning region.").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, preventGraphPreprocessing, true, "Prevent graph preprocessing (for debugging)").setIsAdvanced().build());
             }
 
             uint64_t QualitativePOMDPAnalysisSettings::getLookahead() const {
                 return this->getOption(lookaheadHorizonOption).getArgumentByName("bound").getValueAsUnsignedInteger();
             }
+
+            std::string QualitativePOMDPAnalysisSettings::getLookaheadType() const {
+                return this->getOption(lookaheadTypeOption).getArgumentByName("type").getValueAsString();
+            }
+
             bool QualitativePOMDPAnalysisSettings::isExportSATCallsSet() const {
                 return this->getOption(exportSATCallsOption).getHasOptionBeenSet();
             }
@@ -54,6 +73,30 @@ namespace storm {
                 return this->getOption(validationLevel).getArgumentByName("level").getValueAsUnsignedInteger() >= 1;
             }
 
+            bool QualitativePOMDPAnalysisSettings::computeExpensiveStats() const {
+                return this->getOption(expensiveStatsOption).getHasOptionBeenSet();
+            }
+
+            std::string QualitativePOMDPAnalysisSettings::exportWinningRegionPath() const {
+                return this->getOption(exportWinningRegionOption).getArgumentByName("path").getValueAsString();
+            }
+
+            bool QualitativePOMDPAnalysisSettings::isExportWinningRegionSet() const {
+                return this->getOption(exportWinningRegionOption).getHasOptionBeenSet();
+            }
+
+            bool QualitativePOMDPAnalysisSettings::isPrintWinningRegionSet() const {
+                return this->getOption(printWinningRegionOption).getHasOptionBeenSet();
+            }
+
+            bool QualitativePOMDPAnalysisSettings::isMemlessSearchSet() const {
+                return this->getOption(memlessSearchOption).getHasOptionBeenSet();
+            }
+
+            std::string QualitativePOMDPAnalysisSettings::getMemlessSearchMethod() const {
+                return this->getOption(memlessSearchOption).getArgumentByName("method").getValueAsString();
+            }
+
             void QualitativePOMDPAnalysisSettings::finalize() {
             }
 

src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.h

@@ -21,12 +21,21 @@ namespace storm {
                 QualitativePOMDPAnalysisSettings();
 
                 uint64_t getLookahead() const;
+                std::string getLookaheadType() const;
                 bool isExportSATCallsSet() const;
                 std::string getExportSATCallsPath() const;
                 bool isOnlyDeterministicSet() const;
                 bool isWinningRegionSet() const;
                 bool validateIntermediateSteps() const;
                 bool validateFinalResult() const;
+                bool computeExpensiveStats() const;
+                bool isPrintWinningRegionSet() const;
+                bool isExportWinningRegionSet() const;
+                std::string exportWinningRegionPath() const;
+                bool isGraphPreprocessingAllowed() const;
+                bool isMemlessSearchSet() const;
+                std::string getMemlessSearchMethod() const;
+
 
 
                 virtual ~QualitativePOMDPAnalysisSettings() = default;

src/storm-pomdp-cli/storm-pomdp.cpp

@@ -129,6 +129,8 @@ namespace storm {
                 options.validateEveryStep = qualSettings.validateIntermediateSteps();
                 options.validateResult = qualSettings.validateFinalResult();
 
+                options.pathVariableType = storm::pomdp::pathVariableTypeFromString(qualSettings.getLookaheadType());
+
                 if (qualSettings.isExportSATCallsSet()) {
                     options.setExportSATCalls(qualSettings.getExportSATCallsPath());
                 }
@@ -137,42 +139,79 @@ 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>();
+            void performQualitativeAnalysis(std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> const& origpomdp, storm::pomdp::analysis::FormulaInformation const& formulaInfo, storm::logic::Formula const& formula) {
                 auto const& qualSettings = storm::settings::getModule<storm::settings::modules::QualitativePOMDPAnalysisSettings>();
+                auto const& coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
 
                 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);
+                storm::models::sparse::Pomdp<ValueType> pomdp(*origpomdp);
+                storm::analysis::QualitativeAnalysisOnGraphs<ValueType> qualitativeAnalysis(pomdp);
                 // After preprocessing, this might be done cheaper.
+                storm::storage::BitVector surelyNotAlmostSurelyReachTarget = qualitativeAnalysis.analyseProbSmaller1(
+                        formula.asProbabilityOperatorFormula());
+                pomdp.getTransitionMatrix().makeRowGroupsAbsorbing(surelyNotAlmostSurelyReachTarget);
                 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();
+                    lookahead = pomdp.getNumberOfStates();
                 }
                 STORM_LOG_TRACE("target states: "  << targetStates);
-                if (pomdpSettings.getMemlessSearchMethod() == "ccd-memless") {
-                    storm::pomdp::QualitativeStrategySearchNaive<ValueType> memlessSearch(*pomdp, targetStates, surelyNotAlmostSurelyReachTarget, smtSolverFactory);
+                if (qualSettings.getMemlessSearchMethod() == "one-shot") {
+                    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, targetStates, surelyNotAlmostSurelyReachTarget, smtSolverFactory, options);
+                } else if (qualSettings.getMemlessSearchMethod() == "iterative") {
+                    storm::pomdp::MemlessStrategySearchQualitative<ValueType> search(pomdp, targetStates, surelyNotAlmostSurelyReachTarget, smtSolverFactory, options);
                     if (qualSettings.isWinningRegionSet()) {
                         search.computeWinningRegion(lookahead);
                     } else {
                         search.analyzeForInitialStates(lookahead);
                     }
+
+                    if (qualSettings.isPrintWinningRegionSet()) {
+                        search.getLastWinningRegion().print();
+                        std::cout << std::endl;
+                    }
+                    if (qualSettings.isExportWinningRegionSet()) {
+                        search.getLastWinningRegion().storeToFile(qualSettings.exportWinningRegionPath());
+                    }
+
                     search.finalizeStatistics();
-                    search.getStatistics().print();
+                    if(pomdp.getInitialStates().getNumberOfSetBits() == 1) {
+                        uint64_t initialState = pomdp.getInitialStates().getNextSetIndex(0);
+                        uint64_t initialObservation = pomdp.getObservation(initialState);
+                        // TODO this is inefficient.
+                        uint64_t offset = 0;
+                        for (uint64_t state = 0; state < pomdp.getNumberOfStates(); ++state) {
+                            if (state == initialState) {
+                                break;
+                            }
+                            if (pomdp.getObservation(state) == initialObservation) {
+                                ++offset;
+                            }
+                        }
+                        STORM_PRINT_AND_LOG("Initial state is safe: " << search.getLastWinningRegion().isWinning(initialObservation, offset));
+                    } else {
+                        STORM_LOG_WARN("Output for multiple initial states is incomplete");
+                    }
+                    std::cout << "Number of belief support states: " << search.getLastWinningRegion().beliefSupportStates() << std::endl;
+                    if (coreSettings.isShowStatisticsSet() && qualSettings.computeExpensiveStats()) {
+                        auto wbss = search.getLastWinningRegion().computeNrWinningBeliefs();
+                        STORM_PRINT_AND_LOG( "Number of winning belief support states: [" << wbss.first << "," << wbss.second
+                                  << "]");
+                    }
+                    if (coreSettings.isShowStatisticsSet()) {
+                        search.getStatistics().print();
+                    }
+
                 } else {
                     STORM_LOG_ERROR("This method is not implemented.");
                 }
@@ -199,7 +238,7 @@ namespace storm {
                     STORM_PRINT_AND_LOG(std::endl);
                     analysisPerformed = true;
                 }
-                if (pomdpSettings.isMemlessSearchSet()) {
+                if (pomdpSettings.isQualitativeAnalysisSet()) {
                     performQualitativeAnalysis(pomdp, formulaInfo, formula);
                     analysisPerformed = true;