set validation level from command line

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() {
             }
 

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;

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());

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