Added new minmax settings: force computation of a priori bouds and tweak the qvi restart heuristic

src/storm/environment/solver/MinMaxSolverEnvironment.cpp

@@ -17,13 +17,15 @@ namespace storm {
         considerRelativeTerminationCriterion = minMaxSettings.getConvergenceCriterion() == storm::settings::modules::MinMaxEquationSolverSettings::ConvergenceCriterion::Relative;
         STORM_LOG_ASSERT(considerRelativeTerminationCriterion || minMaxSettings.getConvergenceCriterion() == storm::settings::modules::MinMaxEquationSolverSettings::ConvergenceCriterion::Absolute, "Unknown convergence criterion");
         multiplicationStyle = minMaxSettings.getValueIterationMultiplicationStyle();
+        forceBounds = minMaxSettings.isForceBoundsSet();
+        qviRestartThreshold = minMaxSettings.getQviRestartThreshold();
+        qviRestartMaxIterations = minMaxSettings.getQviRestartMaxIterations();
     }
 
     MinMaxSolverEnvironment::~MinMaxSolverEnvironment() {
         // Intentionally left empty
     }
     
-    
     storm::solver::MinMaxMethod const& MinMaxSolverEnvironment::getMethod() const {
         return minMaxMethod;
     }
@@ -69,6 +71,30 @@ namespace storm {
         multiplicationStyle = value;
     }
     
+    bool MinMaxSolverEnvironment::isForceBoundsSet() const {
+        return forceBounds;
+    }
+    
+    void MinMaxSolverEnvironment::setForceBounds(bool value) {
+        forceBounds = value;
+    }
+    
+    storm::RationalNumber MinMaxSolverEnvironment::getQviRestartThreshold() const {
+        return qviRestartThreshold;
+    }
+    
+    void MinMaxSolverEnvironment::setQviRestartThreshold(storm::RationalNumber value) {
+        qviRestartThreshold = value;
+    }
+    
+    uint64_t MinMaxSolverEnvironment::getQviRestartMaxIterations() const {
+        return qviRestartMaxIterations;
+    }
+    
+    void MinMaxSolverEnvironment::setQviRestartMaxIterations(uint64_t value) {
+        qviRestartMaxIterations = value;
+    }
+    
 
 
 }

src/storm/environment/solver/MinMaxSolverEnvironment.h

@@ -25,6 +25,12 @@ namespace storm {
         void setRelativeTerminationCriterion(bool value);
         storm::solver::MultiplicationStyle const& getMultiplicationStyle() const;
         void setMultiplicationStyle(storm::solver::MultiplicationStyle value);
+        bool isForceBoundsSet() const;
+        void setForceBounds(bool value);
+        storm::RationalNumber getQviRestartThreshold() const;
+        void setQviRestartThreshold(storm::RationalNumber value);
+        uint64_t getQviRestartMaxIterations() const;
+        void setQviRestartMaxIterations(uint64_t value);
         
     private:
         storm::solver::MinMaxMethod minMaxMethod;
@@ -33,7 +39,9 @@ namespace storm {
         storm::RationalNumber precision;
         bool considerRelativeTerminationCriterion;
         storm::solver::MultiplicationStyle multiplicationStyle;
-    
+        bool forceBounds;
+        storm::RationalNumber qviRestartThreshold;
+        uint64_t qviRestartMaxIterations;
     };
 }
 

src/storm/settings/modules/MinMaxEquationSolverSettings.cpp

@@ -19,6 +19,8 @@ namespace storm {
             const std::string MinMaxEquationSolverSettings::absoluteOptionName = "absolute";
             const std::string MinMaxEquationSolverSettings::lraMethodOptionName = "lramethod";
             const std::string MinMaxEquationSolverSettings::valueIterationMultiplicationStyleOptionName = "vimult";
+            const std::string MinMaxEquationSolverSettings::forceBoundsOptionName = "forcebounds";
+            const std::string MinMaxEquationSolverSettings::quickValueIterationRestartOptionName = "qvirestart";
 
             MinMaxEquationSolverSettings::MinMaxEquationSolverSettings() : ModuleSettings(moduleName) {
                 std::vector<std::string> minMaxSolvingTechniques = {"vi", "value-iteration", "pi", "policy-iteration", "linear-programming", "lp", "ratsearch", "qvi", "quick-value-iteration"};
@@ -38,6 +40,12 @@ namespace storm {
                 std::vector<std::string> multiplicationStyles = {"gaussseidel", "regular", "gs", "r"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, valueIterationMultiplicationStyleOptionName, false, "Sets which method multiplication style to prefer for value iteration.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of a multiplication style.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(multiplicationStyles)).setDefaultValueString("gaussseidel").build()).build());
+                
+                this->addOption(storm::settings::OptionBuilder(moduleName, forceBoundsOptionName, false, "If set, minmax solver always require that a priori bounds for the solution are computed.").build());
+                
+                this->addOption(storm::settings::OptionBuilder(moduleName, quickValueIterationRestartOptionName, false, "Controls when a restart of quick value iteration is triggered.")
+                                .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("threshold", "The minimal (relative) bound improvement that triggers a restart").addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorIncluding(0.0, 1.0)).setDefaultValueDouble(0.5).build())
+                                .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("maxiters", "The maximal number of iterations within which a restart can be triggered.").setDefaultValueUnsignedInteger(300).build()).build());
             }
             
             storm::solver::MinMaxMethod MinMaxEquationSolverSettings::getMinMaxEquationSolvingMethod() const {
@@ -108,6 +116,18 @@ namespace storm {
                 STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown multiplication style '" << multiplicationStyleString << "'.");
             }
             
+            bool MinMaxEquationSolverSettings::isForceBoundsSet() const {
+                return this->getOption(forceBoundsOptionName).getHasOptionBeenSet();
+            }
+            
+            double MinMaxEquationSolverSettings::getQviRestartThreshold() const {
+                return this->getOption(quickValueIterationRestartOptionName).getArgumentByName("threshold").getValueAsDouble();
+            }
+            
+            uint_fast64_t MinMaxEquationSolverSettings::getQviRestartMaxIterations() const {
+                return this->getOption(quickValueIterationRestartOptionName).getArgumentByName("maxiters").getValueAsUnsignedInteger();
+            }
+            
         }
     }
 }

src/storm/settings/modules/MinMaxEquationSolverSettings.h

@@ -97,6 +97,21 @@ namespace storm {
                  */
                 storm::solver::MultiplicationStyle getValueIterationMultiplicationStyle() const;
                 
+                /*!
+                 * Retrieves whether the  force bounds option has been set.
+                 */
+                bool isForceBoundsSet() const;
+                
+                /*!
+                 * Retrieves the restart threshold for quick value iteration
+                 */
+                double getQviRestartThreshold() const;
+                
+                /*!
+                 * Retrieves the maximal number of iterations within which a restart of quick value iteration can be triggered.
+                 */
+                uint_fast64_t getQviRestartMaxIterations() const;
+                
                 // The name of the module.
                 static const std::string moduleName;
                 
@@ -108,6 +123,8 @@ namespace storm {
                 static const std::string absoluteOptionName;
                 static const std::string lraMethodOptionName;
                 static const std::string valueIterationMultiplicationStyleOptionName;
+                static const std::string forceBoundsOptionName;
+                static const std::string quickValueIterationRestartOptionName;
             };
             
         }

src/storm/solver/LpMinMaxLinearEquationSolver.cpp

@@ -120,6 +120,10 @@ namespace storm {
                 requirements.requireNoEndComponents();
             }
             
+            if (env.solver().minMax().isForceBoundsSet()) {
+                requirements.requireBounds();
+            }
+            
             return  requirements;
         }
         

src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp

@@ -458,6 +458,10 @@ namespace storm {
                 STORM_LOG_THROW(false, storm::exceptions::InvalidEnvironmentException, "The selected min max technique is not supported by this solver.");
             }
 
+            if (env.solver().minMax().isForceBoundsSet()) {
+                requirements.requireBounds();
+            }
+            
             return requirements;
         }