diff --git a/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.cpp b/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.cpp new file mode 100644 index 000000000..bda4ac15e --- /dev/null +++ b/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 diff --git a/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.h b/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.h new file mode 100644 index 000000000..6a9830e8b --- /dev/null +++ b/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 diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp index 0a61ac323..c16354973 100644 --- a/src/storm-pomdp-cli/storm-pomdp.cpp +++ b/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."); } diff --git a/src/storm-pomdp/analysis/MemlessStrategySearchQualitative.h b/src/storm-pomdp/analysis/MemlessStrategySearchQualitative.h index d1388d8e2..c3a07e6dd 100644 --- a/src/storm-pomdp/analysis/MemlessStrategySearchQualitative.h +++ b/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;