diff --git a/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.cpp b/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.cpp index 85bfd78dc..86a5e5ee8 100644 --- a/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.cpp +++ b/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.cpp @@ -17,6 +17,7 @@ namespace storm { const std::string lookaheadHorizonOption = "lookaheadhorizon"; const std::string onlyDeterministicOption = "onlydeterministic"; const std::string winningRegionOption = "winningregion"; + const std::string validationLevel = "validate"; QualitativePOMDPAnalysisSettings::QualitativePOMDPAnalysisSettings() : ModuleSettings(moduleName) { @@ -24,6 +25,7 @@ namespace storm { 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, 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()); } uint64_t QualitativePOMDPAnalysisSettings::getLookahead() const { @@ -45,6 +47,13 @@ namespace storm { return this->getOption(winningRegionOption).getHasOptionBeenSet(); } + bool QualitativePOMDPAnalysisSettings::validateIntermediateSteps() const { + return this->getOption(validationLevel).getArgumentByName("level").getValueAsUnsignedInteger() >= 2; + } + bool QualitativePOMDPAnalysisSettings::validateFinalResult() const { + return this->getOption(validationLevel).getArgumentByName("level").getValueAsUnsignedInteger() >= 1; + } + void QualitativePOMDPAnalysisSettings::finalize() { } diff --git a/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.h b/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.h index 62ab3357e..6f0fb3ebc 100644 --- a/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.h +++ b/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.h @@ -25,6 +25,8 @@ namespace storm { std::string getExportSATCallsPath() const; bool isOnlyDeterministicSet() const; bool isWinningRegionSet() const; + bool validateIntermediateSteps() const; + bool validateFinalResult() const; virtual ~QualitativePOMDPAnalysisSettings() = default; diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp index 41b07c351..1b3cda866 100644 --- a/src/storm-pomdp-cli/storm-pomdp.cpp +++ b/src/storm-pomdp-cli/storm-pomdp.cpp @@ -99,7 +99,7 @@ namespace storm { options.onlyDeterministicStrategies = qualSettings.isOnlyDeterministicSet(); uint64_t loglevel = 0; - // TODO a big ugly, but we have our own loglevels. + // TODO a big ugly, but we have our own loglevels (for technical reasons) if(storm::utility::getLogLevel() == l3pp::LogLevel::INFO) { loglevel = 1; } @@ -108,9 +108,10 @@ namespace storm { } else if(storm::utility::getLogLevel() == l3pp::LogLevel::TRACE) { loglevel = 3; - options.validateEveryStep = true; } options.setDebugLevel(loglevel); + options.validateEveryStep = qualSettings.validateIntermediateSteps(); + options.validateResult = qualSettings.validateFinalResult(); if (qualSettings.isExportSATCallsSet()) { options.setExportSATCalls(qualSettings.getExportSATCallsPath()); diff --git a/src/storm-pomdp/analysis/MemlessStrategySearchQualitative.h b/src/storm-pomdp/analysis/MemlessStrategySearchQualitative.h index c7fcae2e8..6106844e1 100644 --- a/src/storm-pomdp/analysis/MemlessStrategySearchQualitative.h +++ b/src/storm-pomdp/analysis/MemlessStrategySearchQualitative.h @@ -47,6 +47,7 @@ namespace pomdp { bool onlyDeterministicStrategies = false; bool forceLookahead = true; bool validateEveryStep = false; + bool validateResult = false; private: std::string exportSATcalls = "";