OVI: Add upper bound only iterations option

src/storm/environment/solver/OviSolverEnvironment.cpp

@@ -13,6 +13,7 @@ namespace storm {
         maxVerificationIterationFactor = storm::utility::convertNumber<storm::RationalNumber>(oviSettings.getMaxVerificationIterationFactor());
         relevantValuesForPrecisionUpdate = oviSettings.useRelevantValuesForPrecisionUpdate();
         upperBoundGuessingFactor = storm::utility::convertNumber<storm::RationalNumber>(oviSettings.getUpperBoundGuessingFactor());
+        upperBoundOnlyIterations = oviSettings.getUpperBoundOnlyIterations();
     }
     
     OviSolverEnvironment::~OviSolverEnvironment() {
@@ -34,5 +35,9 @@ namespace storm {
     storm::RationalNumber OviSolverEnvironment::getUpperBoundGuessingFactor() const {
         return maxVerificationIterationFactor;
     }
+
+    uint64_t OviSolverEnvironment::getUpperBoundOnlyIterations() const {
+        return upperBoundOnlyIterations;
+    }
     
 }

src/storm/environment/solver/OviSolverEnvironment.h

@@ -16,12 +16,14 @@ namespace storm {
         storm::RationalNumber getMaxVerificationIterationFactor() const;
         bool useRelevantValuesForPrecisionUpdate() const;
         storm::RationalNumber getUpperBoundGuessingFactor() const;
+        uint64_t getUpperBoundOnlyIterations() const;
         
     private:
         storm::RationalNumber precisionUpdateFactor;
         storm::RationalNumber maxVerificationIterationFactor;
         bool relevantValuesForPrecisionUpdate;
         storm::RationalNumber upperBoundGuessingFactor;
+        uint64_t upperBoundOnlyIterations;
     };
 }
 

src/storm/settings/modules/OviSolverSettings.cpp

@@ -16,6 +16,7 @@ namespace storm {
             const std::string OviSolverSettings::maxVerificationIterationFactorOptionName = "max-verification-iter-factor";
             const std::string OviSolverSettings::useRelevantValuesForPrecisionUpdateOptionName = "use-relevant-values";
             const std::string OviSolverSettings::upperBoundGuessingFactorOptionName = "upper-bound-factor";
+            const std::string OviSolverSettings::upperBoundOnlyIterationsOptionName = "check-upper-only-iter";
             
             OviSolverSettings::OviSolverSettings() : ModuleSettings(moduleName) {
                 
@@ -26,6 +27,8 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, maxVerificationIterationFactorOptionName, false, "Controls how many verification iterations are performed before guessing a new upper bound.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("factor", "The factor.").setDefaultValueDouble(0.1).addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterValidator(0.0)).build()).build());
 
                 this->addOption(storm::settings::OptionBuilder(moduleName, upperBoundGuessingFactorOptionName, false, "Sets with which factor the precision is multiplied to guess the upper bound.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("factor", "The factor.").setDefaultValueDouble(1.0).addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterValidator(0.0)).build()).build());
+
+                this->addOption(storm::settings::OptionBuilder(moduleName, upperBoundOnlyIterationsOptionName, false, "Sets the max. iterations OVI will only iterate over the upper bound.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createIntegerArgument("iter", "The iterations.").setDefaultValueInteger(20000).addValidatorInteger(ArgumentValidatorFactory::createIntegerGreaterValidator(0)).build()).build());
             }
             
             double OviSolverSettings::getPrecisionUpdateFactor() const {
@@ -43,6 +46,10 @@ namespace storm {
             double OviSolverSettings::getUpperBoundGuessingFactor() const {
                 return this->getOption(upperBoundGuessingFactorOptionName).getArgumentByName("factor").getValueAsDouble();
             }
+
+            uint64_t OviSolverSettings::getUpperBoundOnlyIterations() const {
+                return this->getOption(upperBoundOnlyIterationsOptionName).getArgumentByName("iter").getValueAsInteger();
+            }
            
         }
     }

src/storm/settings/modules/OviSolverSettings.h

@@ -22,6 +22,8 @@ namespace storm {
                 bool useRelevantValuesForPrecisionUpdate() const;
 
                 double getUpperBoundGuessingFactor() const;
+
+                uint64_t getUpperBoundOnlyIterations() const;
                 
                 
                 // The name of the module.
@@ -32,6 +34,7 @@ namespace storm {
                 static const std::string maxVerificationIterationFactorOptionName;
                 static const std::string useRelevantValuesForPrecisionUpdateOptionName;
                 static const std::string upperBoundGuessingFactorOptionName;
+                static const std::string upperBoundOnlyIterationsOptionName;
             };
             
         }