From 93ed0224a178dfe4f04e04c5040695c265baec1f Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Sat, 21 Dec 2019 22:03:36 +0100 Subject: [PATCH] options for searching for qualitative schedulers --- .../QualitativePOMDPAnalysisSettings.cpp | 47 +++++++++++++++++++ .../QualitativePOMDPAnalysisSettings.h | 43 +++++++++++++++++ src/storm-pomdp-cli/storm-pomdp.cpp | 19 ++++++-- .../MemlessStrategySearchQualitative.h | 19 ++++++++ 4 files changed, 124 insertions(+), 4 deletions(-) create mode 100644 src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.cpp create mode 100644 src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.h 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::addModule(); - storm::settings::addModule(); + storm::settings::addModule(); } template @@ -196,6 +197,7 @@ int main(const int argc, const char** argv) { auto const& pomdpSettings = storm::settings::getModule(); auto const &general = storm::settings::getModule(); auto const &debug = storm::settings::getModule(); + auto const& pomdpQualSettings = storm::settings::getModule(); 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 smtSolverFactory = std::make_shared(); + + uint64_t lookahead = pomdpQualSettings.getLookahead(); + if (lookahead == 0) { + lookahead = pomdp->getNumberOfStates(); + } + + storm::pomdp::MemlessSearchOptions options; + + if (pomdpSettings.getMemlessSearchMethod() == "ccd16memless") { storm::pomdp::QualitativeStrategySearchNaive memlessSearch(*pomdp, targetObservationSet, targetStates, badStates, smtSolverFactory); - memlessSearch.findNewStrategyForSomeState(5); + memlessSearch.findNewStrategyForSomeState(lookahead); } else if (pomdpSettings.getMemlessSearchMethod() == "iterative") { storm::pomdp::MemlessStrategySearchQualitative 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> actions; std::vector schedulerRef;