options for searching for qualitative schedulers

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

@@ -0,0 +1,47 @@
+#include "storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.h"
+
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/SettingMemento.h"
+#include "storm/settings/Option.h"
+#include "storm/settings/OptionBuilder.h"
+#include "storm/settings/ArgumentBuilder.h"
+
+#include "storm/exceptions/InvalidArgumentException.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+
+            const std::string QualitativePOMDPAnalysisSettings::moduleName = "pomdpQualitative";
+            const std::string exportSATCallsOption = "exportSATCallsPath";
+            const std::string lookaheadHorizonOption = "lookaheadHorizon";
+
+
+            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, 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());
+            }
+
+            uint64_t QualitativePOMDPAnalysisSettings::getLookahead() const {
+                return this->getOption(lookaheadHorizonOption).getArgumentByName("bound").getValueAsUnsignedInteger();
+            }
+            bool QualitativePOMDPAnalysisSettings::isExportSATCallsSet() const {
+                return this->getOption(exportSATCallsOption).getHasOptionBeenSet();
+            }
+
+            std::string QualitativePOMDPAnalysisSettings::getExportSATCallsPath() const {
+                return this->getOption(exportSATCallsOption).getArgumentByName("path").getValueAsString();
+            }
+
+
+
+            void QualitativePOMDPAnalysisSettings::finalize() {
+            }
+
+            bool QualitativePOMDPAnalysisSettings::check() const {
+                return true;
+            }
+
+        } // namespace modules
+    } // namespace settings
+} // namespace storm

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

@@ -0,0 +1,43 @@
+#pragma once
+
+
+#include "storm-config.h"
+#include "storm/settings/modules/ModuleSettings.h"
+#include "storm-pomdp/storage/PomdpMemory.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+
+            /*!
+             * This class represents the settings for POMDP model checking.
+             */
+            class QualitativePOMDPAnalysisSettings : public ModuleSettings {
+            public:
+
+                /*!
+                 * Creates a new set of POMDP settings.
+                 */
+                QualitativePOMDPAnalysisSettings();
+
+                uint64_t getLookahead() const;
+                bool isExportSATCallsSet() const;
+                std::string getExportSATCallsPath() const;
+
+
+                virtual ~QualitativePOMDPAnalysisSettings() = default;
+
+                bool check() const override;
+                void finalize() override;
+
+                // The name of the module.
+                static const std::string moduleName;
+
+            private:
+
+
+            };
+
+        } // namespace modules
+    } // namespace settings
+} // namespace storm

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

@@ -26,10 +26,11 @@
 #include "storm/settings/modules/TopologicalEquationSolverSettings.h"
 #include "storm/settings/modules/ModelCheckerSettings.h"
 #include "storm/settings/modules/MultiplierSettings.h"
-
 #include "storm/settings/modules/TransformationSettings.h"
 #include "storm/settings/modules/MultiObjectiveSettings.h"
 #include "storm-pomdp-cli/settings/modules/POMDPSettings.h"
+#include "storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.h"
+
 #include "storm/analysis/GraphConditions.h"
 
 #include "storm-cli-utilities/cli.h"
@@ -78,8 +79,8 @@ void initializeSettings() {
     storm::settings::addModule<storm::settings::modules::ModelCheckerSettings>();
     storm::settings::addModule<storm::settings::modules::MultiplierSettings>();
 
-
     storm::settings::addModule<storm::settings::modules::POMDPSettings>();
+    storm::settings::addModule<storm::settings::modules::QualitativePOMDPAnalysisSettings>();
 }
 
 template<typename ValueType>
@@ -196,6 +197,7 @@ int main(const int argc, const char** argv) {
         auto const& pomdpSettings = storm::settings::getModule<storm::settings::modules::POMDPSettings>();
         auto const &general = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
         auto const &debug = storm::settings::getModule<storm::settings::modules::DebugSettings>();
+        auto const& pomdpQualSettings = storm::settings::getModule<storm::settings::modules::QualitativePOMDPAnalysisSettings>();
 
         if (general.isVerboseSet()) {
             storm::utility::setLogLevel(l3pp::LogLevel::INFO);
@@ -295,12 +297,21 @@ int main(const int argc, const char** argv) {
 //                    std::cout << std::endl;
                     storm::expressions::ExpressionManager expressionManager;
                     std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
+
+                    uint64_t lookahead = pomdpQualSettings.getLookahead();
+                    if (lookahead == 0) {
+                        lookahead = pomdp->getNumberOfStates();
+                    }
+
+                    storm::pomdp::MemlessSearchOptions options;
+
+
                     if (pomdpSettings.getMemlessSearchMethod() == "ccd16memless") {
                         storm::pomdp::QualitativeStrategySearchNaive<double> memlessSearch(*pomdp, targetObservationSet, targetStates, badStates, smtSolverFactory);
-                        memlessSearch.findNewStrategyForSomeState(5);
+                        memlessSearch.findNewStrategyForSomeState(lookahead);
                     } else if (pomdpSettings.getMemlessSearchMethod() == "iterative") {
                         storm::pomdp::MemlessStrategySearchQualitative<double> memlessSearch(*pomdp, targetObservationSet, targetStates, badStates, smtSolverFactory);
-                        memlessSearch.findNewStrategyForSomeState(5);
+                        memlessSearch.findNewStrategyForSomeState(lookahead);
                     } else {
                         STORM_LOG_ERROR("This method is not implemented.");
                     }

src/storm-pomdp/analysis/MemlessStrategySearchQualitative.h

@@ -8,6 +8,25 @@
 namespace storm {
 namespace pomdp {
 
+    class MemlessSearchOptions {
+
+    public:
+        void setExportSATCalls(std::string const& path) {
+            exportSATcalls = path;
+        }
+
+        std::string const& getExportSATCallsPath() const {
+            return exportSATcalls;
+        }
+
+        bool isExportSATSet() const {
+            return exportSATcalls == "";
+        }
+    private:
+        std::string exportSATcalls = "";
+
+    };
+
     struct InternalObservationScheduler {
         std::vector<std::set<uint64_t>> actions;
         std::vector<uint64_t> schedulerRef;