From d3c593fe74b14ceee94faa80d1fee3deea86fa43 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@gmail.com>
Date: Fri, 8 May 2020 17:25:36 -0700
Subject: [PATCH] set validation level from command line

---
 .../modules/QualitativePOMDPAnalysisSettings.cpp         | 9 +++++++++
 .../settings/modules/QualitativePOMDPAnalysisSettings.h  | 2 ++
 src/storm-pomdp-cli/storm-pomdp.cpp                      | 5 +++--
 .../analysis/MemlessStrategySearchQualitative.h          | 1 +
 4 files changed, 15 insertions(+), 2 deletions(-)

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 = "";