OVI: Added a few settings to tweak ovi

src/storm/environment/SubEnvironment.cpp

@@ -6,12 +6,13 @@
 
 #include "storm/environment/solver/SolverEnvironment.h"
 #include "storm/environment/solver/EigenSolverEnvironment.h"
+#include "storm/environment/solver/GameSolverEnvironment.h"
 #include "storm/environment/solver/GmmxxSolverEnvironment.h"
 #include "storm/environment/solver/NativeSolverEnvironment.h"
 #include "storm/environment/solver/LongRunAverageSolverEnvironment.h"
 #include "storm/environment/solver/MinMaxSolverEnvironment.h"
 #include "storm/environment/solver/MultiplierEnvironment.h"
-#include "storm/environment/solver/GameSolverEnvironment.h"
+#include "storm/environment/solver/OviSolverEnvironment.h"
 #include "storm/environment/solver/TopologicalSolverEnvironment.h"
 
 namespace storm {
@@ -67,6 +68,7 @@ namespace storm {
     template class SubEnvironment<LongRunAverageSolverEnvironment>;
     template class SubEnvironment<MinMaxSolverEnvironment>;
     template class SubEnvironment<MultiplierEnvironment>;
+    template class SubEnvironment<OviSolverEnvironment>;
     template class SubEnvironment<GameSolverEnvironment>;
     template class SubEnvironment<TopologicalSolverEnvironment>;
     

src/storm/environment/solver/OviSolverEnvironment.cpp

@@ -0,0 +1,33 @@
+#include "storm/environment/solver/OviSolverEnvironment.h"
+
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/OviSolverSettings.h"
+#include "storm/utility/constants.h"
+#include "storm/utility/macros.h"
+
+namespace storm {
+    
+    OviSolverEnvironment::OviSolverEnvironment() {
+        auto const& oviSettings = storm::settings::getModule<storm::settings::modules::OviSolverSettings>();
+        precisionUpdateFactor = storm::utility::convertNumber<storm::RationalNumber>(oviSettings.getPrecisionUpdateFactor());
+        maxVerificationIterationFactor = storm::utility::convertNumber<storm::RationalNumber>(oviSettings.getMaxVerificationIterationFactor());
+        relevantValuesForPrecisionUpdate = oviSettings.useRelevantValuesForPrecisionUpdate();
+    };
+    
+    OviSolverEnvironment::~OviSolverEnvironment() {
+        // Intentionally left empty
+    }
+    
+    storm::RationalNumber OviSolverEnvironment::getPrecisionUpdateFactor() const {
+        return precisionUpdateFactor;
+    }
+    
+    storm::RationalNumber OviSolverEnvironment::getMaxVerificationIterationFactor() const {
+        return maxVerificationIterationFactor;
+    }
+    
+    bool OviSolverEnvironment::useRelevantValuesForPrecisionUpdate() const {
+        return relevantValuesForPrecisionUpdate;
+    }
+    
+}

src/storm/environment/solver/OviSolverEnvironment.h

@@ -0,0 +1,25 @@
+#pragma once
+
+#include "storm/environment/solver/SolverEnvironment.h"
+
+#include "storm/adapters/RationalNumberAdapter.h"
+
+namespace storm {
+    
+    class OviSolverEnvironment {
+    public:
+        
+        OviSolverEnvironment();
+        ~OviSolverEnvironment();
+        
+        storm::RationalNumber getPrecisionUpdateFactor() const;
+        storm::RationalNumber getMaxVerificationIterationFactor() const;
+        bool useRelevantValuesForPrecisionUpdate() const;
+        
+    private:
+        storm::RationalNumber precisionUpdateFactor;
+        storm::RationalNumber maxVerificationIterationFactor;
+        bool relevantValuesForPrecisionUpdate;
+    };
+}
+

src/storm/environment/solver/SolverEnvironment.cpp

@@ -8,6 +8,7 @@
 #include "storm/environment/solver/NativeSolverEnvironment.h"
 #include "storm/environment/solver/GameSolverEnvironment.h"
 #include "storm/environment/solver/TopologicalSolverEnvironment.h"
+#include "storm/environment/solver/OviSolverEnvironment.h"
 
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/GeneralSettings.h"
@@ -94,6 +95,14 @@ namespace storm {
         return topologicalSolverEnvironment.get();
     }
 
+    OviSolverEnvironment& SolverEnvironment::ovi() {
+        return oviSolverEnvironment.get();
+    }
+    
+    OviSolverEnvironment const& SolverEnvironment::ovi() const {
+        return oviSolverEnvironment.get();
+    }
+
     bool SolverEnvironment::isForceSoundness() const {
         return forceSoundness;
     }

src/storm/environment/solver/SolverEnvironment.h

@@ -19,6 +19,7 @@ namespace storm {
     class MultiplierEnvironment;
     class GameSolverEnvironment;
     class TopologicalSolverEnvironment;
+    class OviSolverEnvironment;
     
     class SolverEnvironment {
     public:
@@ -38,6 +39,8 @@ namespace storm {
         MinMaxSolverEnvironment const& minMax() const;
         MultiplierEnvironment& multiplier();
         MultiplierEnvironment const& multiplier() const;
+        OviSolverEnvironment const& ovi() const;
+        OviSolverEnvironment& ovi();
         GameSolverEnvironment& game();
         GameSolverEnvironment const& game() const;
         TopologicalSolverEnvironment& topological();
@@ -62,6 +65,7 @@ namespace storm {
         SubEnvironment<LongRunAverageSolverEnvironment> longRunAverageSolverEnvironment;
         SubEnvironment<MinMaxSolverEnvironment> minMaxSolverEnvironment;
         SubEnvironment<MultiplierEnvironment> multiplierEnvironment;
+        SubEnvironment<OviSolverEnvironment> oviSolverEnvironment;
       
         storm::solver::EquationSolverType linearEquationSolverType;
         bool linearEquationSolverTypeSetFromDefault;

src/storm/settings/SettingsManager.cpp

@@ -40,6 +40,7 @@
 #include "storm/settings/modules/MultiplierSettings.h"
 #include "storm/settings/modules/TransformationSettings.h"
 #include "storm/settings/modules/HintSettings.h"
+#include "storm/settings/modules/OviSolverSettings.h"
 #include "storm/utility/macros.h"
 #include "storm/utility/file.h"
 #include "storm/utility/string.h"
@@ -672,6 +673,7 @@ namespace storm {
             storm::settings::addModule<storm::settings::modules::MultiplierSettings>();
             storm::settings::addModule<storm::settings::modules::TransformationSettings>();
             storm::settings::addModule<storm::settings::modules::HintSettings>();
+            storm::settings::addModule<storm::settings::modules::OviSolverSettings>();
         }
 
     }

src/storm/settings/modules/OviSolverSettings.cpp

@@ -0,0 +1,42 @@
+#include "storm/settings/modules/OviSolverSettings.h"
+
+#include "storm/settings/Option.h"
+#include "storm/settings/ArgumentBuilder.h"
+#include "storm/settings/OptionBuilder.h"
+
+#include "storm/utility/macros.h"
+#include "storm/exceptions/IllegalArgumentValueException.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+            
+            const std::string OviSolverSettings::moduleName = "ovi";
+            const std::string OviSolverSettings::precisionUpdateFactorOptionName = "precision-update-factor";
+            const std::string OviSolverSettings::maxVerificationIterationFactorOptionName = "max-verification-iter-factor";
+            const std::string OviSolverSettings::useRelevantValuesForPrecisionUpdateOptionName = "use-relevant-values";
+            
+            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.5).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
+                
+                this->addOption(storm::settings::OptionBuilder(moduleName, useRelevantValuesForPrecisionUpdateOptionName, false, "Sets whether the precision of the inner value iteration is only based on the relevant values (i.e. initial states).").setIsAdvanced().build());
+                
+                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());
+            }
+            
+            double OviSolverSettings::getPrecisionUpdateFactor() const {
+                return this->getOption(precisionUpdateFactorOptionName).getArgumentByName("factor").getValueAsDouble();
+            }
+            
+            double OviSolverSettings::getMaxVerificationIterationFactor() const {
+                return this->getOption(maxVerificationIterationFactorOptionName).getArgumentByName("factor").getValueAsDouble();
+            }
+            
+            bool OviSolverSettings::useRelevantValuesForPrecisionUpdate() const {
+                return this->getOption(useRelevantValuesForPrecisionUpdateOptionName).getHasOptionBeenSet();
+            }
+           
+        }
+    }
+}

src/storm/settings/modules/OviSolverSettings.h

@@ -0,0 +1,36 @@
+#pragma once
+
+#include "storm-config.h"
+#include "storm/settings/modules/ModuleSettings.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+            
+            /*!
+             * This class represents the settings for the optimistic value iteration solver.
+             */
+            class OviSolverSettings : public ModuleSettings {
+            public:
+                
+                OviSolverSettings();
+              
+                double getPrecisionUpdateFactor() const;
+                
+                double getMaxVerificationIterationFactor() const;
+                
+                bool useRelevantValuesForPrecisionUpdate() const;
+                
+                
+                // The name of the module.
+                static const std::string moduleName;
+                
+            private:
+                static const std::string precisionUpdateFactorOptionName;
+                static const std::string maxVerificationIterationFactorOptionName;
+                static const std::string useRelevantValuesForPrecisionUpdateOptionName;
+            };
+            
+        }
+    }
+}

src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp

@@ -6,6 +6,7 @@
 #include "storm/utility/ConstantsComparator.h"
 
 #include "storm/environment/solver/MinMaxSolverEnvironment.h"
+#include "storm/environment/solver/OviSolverEnvironment.h"
 
 #include "storm/utility/KwekMehlhorn.h"
 #include "storm/utility/NumberTraits.h"
@@ -366,6 +367,19 @@ namespace storm {
             }
             return result;
         }
+        
+        template<typename ValueType>
+        ValueType computeMaxRelDiff(std::vector<ValueType> const& allOldValues, std::vector<ValueType> const& allNewValues, storm::storage::BitVector const& relevantValues) {
+            ValueType result = storm::utility::zero<ValueType>();
+            for (auto const& i : relevantValues) {
+                STORM_LOG_ASSERT(!storm::utility::isZero(allNewValues[i]) || storm::utility::isZero(allOldValues[i]), "Unexpected entry in iteration vector.");
+                if (!storm::utility::isZero(allNewValues[i])) {
+                    result = storm::utility::max<ValueType>(result, storm::utility::abs<ValueType>(allNewValues[i] - allOldValues[i]) / allNewValues[i]);
+                }
+            }
+            return result;
+        }
+        
         template<typename ValueType>
         ValueType computeMaxRelDiff(std::vector<ValueType> const& allOldValues, std::vector<ValueType> const& allNewValues) {
             ValueType result = storm::utility::zero<ValueType>();
@@ -379,11 +393,13 @@ namespace storm {
         }
 
         template<typename ValueType>
-        ValueType updateIterationPrecision(std::vector<ValueType> const& currentX, std::vector<ValueType> const& newX, bool const& relative) {
+        ValueType updateIterationPrecision(storm::Environment const& env, std::vector<ValueType> const& currentX, std::vector<ValueType> const& newX, bool const& relative, boost::optional<storm::storage::BitVector> const& relevantValues) {
+            auto factor = storm::utility::convertNumber<ValueType>(env.solver().ovi().getPrecisionUpdateFactor());
+            bool useRelevant = relevantValues.is_initialized() && env.solver().ovi().useRelevantValuesForPrecisionUpdate();
             if (relative) {
-                return computeMaxRelDiff(newX, currentX) / storm::utility::convertNumber<ValueType>(2);
+                return (useRelevant ? computeMaxRelDiff(newX, currentX, relevantValues.get()) : computeMaxRelDiff(newX, currentX)) * factor;
             } else {
-                return computeMaxAbsDiff(newX, currentX) / storm::utility::convertNumber<ValueType>(2);
+                return (useRelevant ? computeMaxAbsDiff(newX, currentX, relevantValues.get()) : computeMaxAbsDiff(newX, currentX)) * factor;
             }
         }
 
@@ -424,6 +440,11 @@ namespace storm {
             // Relative errors
             bool relative = env.solver().minMax().getRelativeTerminationCriterion();
 
+            boost::optional<storm::storage::BitVector> relevantValues;
+            if (this->hasRelevantValues()) {
+                relevantValues = this->getRelevantValues();
+            }
+            
             // x has to start with a lower bound.
             this->createLowerBoundsVector(x);
 
@@ -502,7 +523,7 @@ namespace storm {
                         std::swap(currentUpperBound, newUpperBound);
 
                         if (newUpperBoundAlwaysHigher) {
-                            iterationPrecision = updateIterationPrecision(*currentX, *newX, relative);
+                            iterationPrecision = updateIterationPrecision(env, *currentX, *newX, relative, relevantValues);
                             // Not all values moved up or stayed the same
                             // If we have a single fixed point, we can safely set the new lower bound, to the wrongly guessed upper bound
                             if (this->hasUniqueSolution()) {
@@ -510,7 +531,7 @@ namespace storm {
                             }
                             break;
                         } else if (valuesCrossed) {
-                            iterationPrecision = updateIterationPrecision(*currentX, *newX, relative);
+                            iterationPrecision = updateIterationPrecision(env, *currentX, *newX, relative, relevantValues);
                             break;
                         } else if (newUpperBoundAlwaysLowerEqual) {
                             // All values moved down or stayed the same and we have a maximum difference of twice the requested precision
@@ -518,7 +539,7 @@ namespace storm {
                             // We can use max_if instead of computeMaxAbsDiff, as x is definitely a lower bound and ub is larger in all elements
                             // Recalculate terminationPrecision if relative error requested
                             bool reachedPrecision = true;
-                            for (auto const& valueIndex : this->hasRelevantValues() ? this->getRelevantValues() : storm::storage::BitVector(x.size(), true)) {
+                            for (auto const& valueIndex : relevantValues ? relevantValues.get() : storm::storage::BitVector(x.size(), true)) {
                                 ValueType absDiff = currentUpperBound[valueIndex] - (*currentX)[valueIndex];
                                 if (relative) {
                                     if (absDiff > doublePrecision * (*currentX)[valueIndex]) {
@@ -539,9 +560,10 @@ namespace storm {
                             }
                         }
                         
-                        if ((currentVerificationIterations / 10) >= lastValueIterationIterations) {
+                        ValueType scaledIterationCount = storm::utility::convertNumber<ValueType>(currentVerificationIterations) * storm::utility::convertNumber<ValueType>(env.solver().ovi().getMaxVerificationIterationFactor());
+                        if (scaledIterationCount >= storm::utility::convertNumber<ValueType>(lastValueIterationIterations)) {
                             cancelGuess = true;
-                            iterationPrecision = updateIterationPrecision(*currentX, *newX, relative);
+                            iterationPrecision = updateIterationPrecision(env, *currentX, *newX, relative, relevantValues);
                         }
                         
                         ++overallIterations;