Preparation for minimum upper and aux benchmarking

This temporary option has not yet been implemented in OVI

src/storm/environment/solver/OviSolverEnvironment.cpp

@@ -14,6 +14,7 @@ namespace storm {
         relevantValuesForPrecisionUpdate = oviSettings.useRelevantValuesForPrecisionUpdate();
         upperBoundGuessingFactor = storm::utility::convertNumber<storm::RationalNumber>(oviSettings.getUpperBoundGuessingFactor());
         upperBoundOnlyIterations = oviSettings.getUpperBoundOnlyIterations();
+        useTerminationGuaranteedMinimumMethod = oviSettings.getUseTerminationGuaranteedMinimumMethod();
     }
     
     OviSolverEnvironment::~OviSolverEnvironment() {
@@ -39,5 +40,9 @@ namespace storm {
     uint64_t OviSolverEnvironment::getUpperBoundOnlyIterations() const {
         return upperBoundOnlyIterations;
     }
+
+    bool OviSolverEnvironment::getUseTerminationGuaranteedMinimumMethod() const {
+        return useTerminationGuaranteedMinimumMethod;
+    }
     
 }

src/storm/environment/solver/OviSolverEnvironment.h

@@ -17,6 +17,7 @@ namespace storm {
         bool useRelevantValuesForPrecisionUpdate() const;
         storm::RationalNumber getUpperBoundGuessingFactor() const;
         uint64_t getUpperBoundOnlyIterations() const;
+        bool getUseTerminationGuaranteedMinimumMethod() const;
         
     private:
         storm::RationalNumber precisionUpdateFactor;
@@ -24,6 +25,7 @@ namespace storm {
         bool relevantValuesForPrecisionUpdate;
         storm::RationalNumber upperBoundGuessingFactor;
         uint64_t upperBoundOnlyIterations;
+        bool useTerminationGuaranteedMinimumMethod;
     };
 }
 

src/storm/settings/modules/OviSolverSettings.cpp

@@ -17,7 +17,8 @@ namespace storm {
             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";
-            
+            const std::string OviSolverSettings::useTerminationGuaranteedMinimumMethodOptionName = "termination-guarantee";
+
             OviSolverSettings::OviSolverSettings() : ModuleSettings(moduleName) {
                 
                 this->addOption(storm::settings::OptionBuilder(moduleName, precisionUpdateFactorOptionName, false, "Sets with which factor the precision of the inner value iteration is updated.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("factor", "The factor.").setDefaultValueDouble(0.4).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
@@ -29,6 +30,8 @@ namespace storm {
                 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());
+
+                this->addOption(storm::settings::OptionBuilder(moduleName, useTerminationGuaranteedMinimumMethodOptionName, false, "Sets whether to perform calculations on element-wise minimum of iterated and old upper bound.").setIsAdvanced().build());
             }
             
             double OviSolverSettings::getPrecisionUpdateFactor() const {
@@ -50,6 +53,10 @@ namespace storm {
             uint64_t OviSolverSettings::getUpperBoundOnlyIterations() const {
                 return this->getOption(upperBoundOnlyIterationsOptionName).getArgumentByName("iter").getValueAsInteger();
             }
+
+            bool OviSolverSettings::getUseTerminationGuaranteedMinimumMethod() const {
+                return this->getOption(useTerminationGuaranteedMinimumMethodOptionName).getHasOptionBeenSet();
+            }
            
         }
     }

src/storm/settings/modules/OviSolverSettings.h

@@ -24,7 +24,8 @@ namespace storm {
                 double getUpperBoundGuessingFactor() const;
 
                 uint64_t getUpperBoundOnlyIterations() const;
-                
+
+                bool getUseTerminationGuaranteedMinimumMethod() const;
                 
                 // The name of the module.
                 static const std::string moduleName;
@@ -35,6 +36,7 @@ namespace storm {
                 static const std::string useRelevantValuesForPrecisionUpdateOptionName;
                 static const std::string upperBoundGuessingFactorOptionName;
                 static const std::string upperBoundOnlyIterationsOptionName;
+                static const std::string useTerminationGuaranteedMinimumMethodOptionName;
             };
             
         }

src/storm/solver/helper/OptimisticValueIterationHelper.h

@@ -163,16 +163,17 @@ namespace storm {
     
                             // Upper bound iteration
                             singleIterationCallback(upperX, auxVector, overallIterations);
-                            // At this point, auxVector contains the old values for the upper bound whereas upperX contains the new ones.
+                            // At this point,h auxVector contains the old values for the upper bound whereas upperX contains the new ones.
                             
                             // Compare the new upper bound candidate with the old one
                             bool newUpperBoundAlwaysHigherEqual = true;
                             bool newUpperBoundAlwaysLowerEqual = true;
                             for (uint64_t i = 0; i < upperX->size(); ++i) {
-                                if ((*auxVector)[i] > (*upperX)[i]) {
-                                    newUpperBoundAlwaysHigherEqual = false;
-                                } else if ((*auxVector)[i] != (*upperX)[i]) {
+                                if ((*upperX)[i] < (*auxVector)[i]) {
+				                    newUpperBoundAlwaysHigherEqual = false;
+                                } else if ((*upperX)[i] != (*auxVector)[i]) {
                                     newUpperBoundAlwaysLowerEqual = false;
+                                    //std::swap((*upperX)[i], (*auxVector)[i]);
                                 }
                             }
                             if (newUpperBoundAlwaysHigherEqual &! newUpperBoundAlwaysLowerEqual) {