Merge branch 'ovi-implementation'

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();
+        noTerminationGuaranteeMinimumMethod = oviSettings.useNoTerminationGuaranteeMinimumMethod();
     }
     
     OviSolverEnvironment::~OviSolverEnvironment() {
@@ -33,11 +34,15 @@ namespace storm {
     }
 
     storm::RationalNumber OviSolverEnvironment::getUpperBoundGuessingFactor() const {
-        return maxVerificationIterationFactor;
+        return upperBoundGuessingFactor;
     }
 
     uint64_t OviSolverEnvironment::getUpperBoundOnlyIterations() const {
         return upperBoundOnlyIterations;
     }
+
+    bool OviSolverEnvironment::useNoTerminationGuaranteeMinimumMethod() const {
+        return noTerminationGuaranteeMinimumMethod;
+    }
     
 }

src/storm/environment/solver/OviSolverEnvironment.h

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

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::useNoTerminationGuaranteeMinimumMethodOptionName = "no-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, useNoTerminationGuaranteeMinimumMethodOptionName, false, "Sets whether to perform element-wise minimum of iterated and old upper bound. If this option is set, that will be skipped, slightly increasing performance but giving no termination guarantee.").setShortName("ntg").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::useNoTerminationGuaranteeMinimumMethod() const {
+                return this->getOption(useNoTerminationGuaranteeMinimumMethodOptionName).getHasOptionBeenSet();
+            }
            
         }
     }

src/storm/settings/modules/OviSolverSettings.h

@@ -24,7 +24,8 @@ namespace storm {
                 double getUpperBoundGuessingFactor() const;
 
                 uint64_t getUpperBoundOnlyIterations() const;
-                
+
+                bool useNoTerminationGuaranteeMinimumMethod() 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 useNoTerminationGuaranteeMinimumMethodOptionName;
             };
             
         }

src/storm/solver/helper/OptimisticValueIterationHelper.h

@@ -82,7 +82,7 @@ namespace storm {
                 void guessUpperBoundAbsolute(std::vector<ValueType> const& x, std::vector<ValueType> &target, ValueType const& precision) {
                     storm::utility::vector::applyPointwise<ValueType, ValueType>(x, target, [&precision] (ValueType const& argument) -> ValueType { return argument + precision; });
                 }
-            
+
             }
             
             
@@ -122,6 +122,8 @@ namespace storm {
                 ValueType two = storm::utility::convertNumber<ValueType>(2.0);
                 // Relative errors
                 bool relative = env.solver().minMax().getRelativeTerminationCriterion();
+                // Use no termination guaranteed upper bound iteration method
+                bool noTerminationGuarantee = env.solver().ovi().useNoTerminationGuaranteeMinimumMethod();
                 // Goal precision
                 ValueType precision = storm::utility::convertNumber<ValueType>(env.solver().minMax().getPrecision());
                 // Desired max difference between upperX and lowerX
@@ -137,54 +139,86 @@ namespace storm {
                 SolverStatus status = SolverStatus::InProgress;
     
                 while (status == SolverStatus::InProgress && overallIterations < maxOverallIterations) {
-    
+
                     // Perform value iteration until convergence
                     ++valueIterationInvocations;
                     auto result = valueIterationCallback(lowerX, auxVector, iterationPrecision, relative, overallIterations, maxOverallIterations);
                     lastValueIterationIterations = result.iterations;
                     overallIterations += result.iterations;
-    
+
                     if (result.status != SolverStatus::Converged) {
                         status = result.status;
                     } else {
                         bool intervalIterationNeeded = false;
                         currentVerificationIterations = 0;
-    
+
                         if (relative) {
                             oviinternal::guessUpperBoundRelative(*lowerX, *upperX, relativeBoundGuessingScaler);
                         } else {
                             oviinternal::guessUpperBoundAbsolute(*lowerX, *upperX, precision);
                         }
-    
+
                         bool cancelGuess = false;
                         while (status == SolverStatus::InProgress && overallIterations < maxOverallIterations) {
                             ++overallIterations;
                             ++currentVerificationIterations;
                             // Perform value iteration stepwise for lower bound and guessed upper bound
-    
+
                             // 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]) {
-                                    newUpperBoundAlwaysLowerEqual = false;
+                            if(noTerminationGuarantee) {
+                                bool cancelOuterScan = false;
+                                for (uint64_t i = 0; i < upperX->size() &! cancelOuterScan; ++i) {
+                                    if ((*upperX)[i] < (*auxVector)[i]) {
+                                        newUpperBoundAlwaysHigherEqual = false;
+                                        ++i;
+                                        while (i < upperX->size()) {
+                                            if ((*upperX)[i] > (*auxVector)[i]) {
+                                                newUpperBoundAlwaysLowerEqual = false;
+                                                cancelOuterScan = true;
+                                                break;
+                                            }
+                                            ++i;
+                                        }
+                                    } else if ((*upperX)[i] != (*auxVector)[i]) {
+                                        newUpperBoundAlwaysLowerEqual = false;
+                                        ++i;
+                                        while (i < upperX->size()) {
+                                            if ((*upperX)[i] < (*auxVector)[i]) {
+                                                newUpperBoundAlwaysHigherEqual = false;
+                                                cancelOuterScan = true;
+                                                break;
+                                            }
+                                            ++i;
+                                        }
+                                    }
+                                }
+                            }
+                            else {
+                                for (uint64_t i = 0; i < upperX->size(); ++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) {
-                                // All values moved up or stayed the same (but are not the same)
+
+                            if (newUpperBoundAlwaysHigherEqual &! newUpperBoundAlwaysLowerEqual) {
+                                // All values moved up or stayed the same
                                 // That means the guess for an upper bound is actually a lower bound
                                 iterationPrecision = oviinternal::updateIterationPrecision(env, *auxVector, *upperX, relative, relevantValues);
                                 // We assume to have a single fixed point. We can thus safely set the new lower bound, to the wrongly guessed upper bound
                                 // Set lowerX to the upper bound candidate
                                 std::swap(lowerX, upperX);
                                 break;
-                            } else if (newUpperBoundAlwaysLowerEqual) {
+                            } else if (newUpperBoundAlwaysLowerEqual &! newUpperBoundAlwaysHigherEqual) {
                                 // All values moved down or stayed the same and we have a maximum difference of twice the requested precision
                                 // We can safely use twice the requested precision, as we calculate the center of both vectors
                                 bool reachedPrecision;
@@ -202,19 +236,19 @@ namespace storm {
                                 }
                             }
                             // At this point, the old upper bounds (auxVector) are not needed anymore.
-                            
+
                             // Check whether we tried this guess for too long
                             ValueType scaledIterationCount = storm::utility::convertNumber<ValueType>(currentVerificationIterations) * storm::utility::convertNumber<ValueType>(env.solver().ovi().getMaxVerificationIterationFactor());
                             if (!intervalIterationNeeded && scaledIterationCount >= storm::utility::convertNumber<ValueType>(lastValueIterationIterations)) {
                                 cancelGuess = true;
                                 // In this case we will make one more iteration on the lower bound (mainly to obtain a new iterationPrecision)
                             }
-                            
+
                             // Lower bound iteration (only if needed)
                             if (cancelGuess || intervalIterationNeeded || currentVerificationIterations > upperBoundOnlyIterations) {
                                 singleIterationCallback(lowerX, auxVector, overallIterations);
                                 // At this point, auxVector contains the old values for the lower bound whereas lowerX contains the new ones.
-    
+
                                 // Check whether the upper and lower bounds have crossed, i.e., the upper bound is smaller than the lower bound.
                                 bool valuesCrossed = false;
                                 for (uint64_t i = 0; i < lowerX->size(); ++i) {
@@ -223,7 +257,7 @@ namespace storm {
                                         break;
                                     }
                                 }
-                                
+
                                 if (cancelGuess || valuesCrossed) {
                                     // A new guess is needed.
                                     iterationPrecision = oviinternal::updateIterationPrecision(env, *auxVector, *lowerX, relative, relevantValues);