Added an option that enforces updating both bounds in interval iteration

src/storm/environment/solver/MinMaxSolverEnvironment.cpp

@@ -18,6 +18,7 @@ namespace storm {
         STORM_LOG_ASSERT(considerRelativeTerminationCriterion || minMaxSettings.getConvergenceCriterion() == storm::settings::modules::MinMaxEquationSolverSettings::ConvergenceCriterion::Absolute, "Unknown convergence criterion");
         multiplicationStyle = minMaxSettings.getValueIterationMultiplicationStyle();
         forceBounds = minMaxSettings.isForceBoundsSet();
+        symmetricUpdates = minMaxSettings.isForceIntervalIterationSymmetricUpdatesSet();
         qviRestartThreshold = minMaxSettings.getQviRestartThreshold();
         qviRestartMaxIterations = minMaxSettings.getQviRestartMaxIterations();
     }
@@ -78,6 +79,14 @@ namespace storm {
     void MinMaxSolverEnvironment::setForceBounds(bool value) {
         forceBounds = value;
     }
+
+    bool MinMaxSolverEnvironment::isSymmetricUpdatesSet() const {
+        return symmetricUpdates;
+    }
+    
+    void MinMaxSolverEnvironment::setSymmetricUpdates(bool value) {
+        symmetricUpdates = value;
+    }
     
     storm::RationalNumber MinMaxSolverEnvironment::getQviRestartThreshold() const {
         return qviRestartThreshold;

src/storm/environment/solver/MinMaxSolverEnvironment.h

@@ -27,6 +27,8 @@ namespace storm {
         void setMultiplicationStyle(storm::solver::MultiplicationStyle value);
         bool isForceBoundsSet() const;
         void setForceBounds(bool value);
+        bool isSymmetricUpdatesSet() const;
+        void setSymmetricUpdates(bool value);
         storm::RationalNumber getQviRestartThreshold() const;
         void setQviRestartThreshold(storm::RationalNumber value);
         uint64_t getQviRestartMaxIterations() const;
@@ -40,6 +42,7 @@ namespace storm {
         bool considerRelativeTerminationCriterion;
         storm::solver::MultiplicationStyle multiplicationStyle;
         bool forceBounds;
+        bool symmetricUpdates;
         storm::RationalNumber qviRestartThreshold;
         uint64_t qviRestartMaxIterations;
     };

src/storm/environment/solver/NativeSolverEnvironment.cpp

@@ -19,6 +19,8 @@ namespace storm {
         powerMethodMultiplicationStyle = nativeSettings.getPowerMethodMultiplicationStyle();
         sorOmega = storm::utility::convertNumber<storm::RationalNumber>(nativeSettings.getOmega());
         forceBounds = nativeSettings.isForceBoundsSet();
+        symmetricUpdates = nativeSettings.isForcePowerMethodSymmetricUpdatesSet();
+
     }
 
     NativeSolverEnvironment::~NativeSolverEnvironment() {
@@ -86,5 +88,12 @@ namespace storm {
         forceBounds = value;
     }
 
+    bool NativeSolverEnvironment::isSymmetricUpdatesSet() const {
+        return symmetricUpdates;
+    }
     
+    void NativeSolverEnvironment::setSymmetricUpdates(bool value) {
+        symmetricUpdates = value;
+    }
+  
 }

src/storm/environment/solver/NativeSolverEnvironment.h

@@ -29,6 +29,8 @@ namespace storm {
         void setSorOmega(storm::RationalNumber const& value);
         bool isForceBoundsSet() const;
         void setForceBounds(bool value);
+        bool isSymmetricUpdatesSet() const;
+        void setSymmetricUpdates(bool value);
         
     private:
         storm::solver::NativeLinearEquationSolverMethod method;
@@ -39,6 +41,7 @@ namespace storm {
         storm::solver::MultiplicationStyle powerMethodMultiplicationStyle;
         storm::RationalNumber sorOmega;
         bool forceBounds;
+        bool symmetricUpdates;
     };
 }
 

src/storm/settings/modules/MinMaxEquationSolverSettings.cpp

@@ -19,6 +19,7 @@ namespace storm {
             const std::string MinMaxEquationSolverSettings::absoluteOptionName = "absolute";
             const std::string MinMaxEquationSolverSettings::lraMethodOptionName = "lramethod";
             const std::string MinMaxEquationSolverSettings::valueIterationMultiplicationStyleOptionName = "vimult";
+            const std::string MinMaxEquationSolverSettings::intervalIterationSymmetricUpdatesOptionName = "symmetricupdates";
             const std::string MinMaxEquationSolverSettings::forceBoundsOptionName = "forcebounds";
             const std::string MinMaxEquationSolverSettings::quickValueIterationRestartOptionName = "qvirestart";
 
@@ -41,6 +42,8 @@ namespace storm {
                 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, intervalIterationSymmetricUpdatesOptionName, false, "If set, interval iteration performs an update on both, lower and upper bound in each iteration").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.")
@@ -118,6 +121,10 @@ namespace storm {
                 STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown multiplication style '" << multiplicationStyleString << "'.");
             }
             
+            bool MinMaxEquationSolverSettings::isForceIntervalIterationSymmetricUpdatesSet() const {
+                return this->getOption(intervalIterationSymmetricUpdatesOptionName).getHasOptionBeenSet();
+            }
+            
             bool MinMaxEquationSolverSettings::isForceBoundsSet() const {
                 return this->getOption(forceBoundsOptionName).getHasOptionBeenSet();
             }

src/storm/settings/modules/MinMaxEquationSolverSettings.h

@@ -97,6 +97,11 @@ namespace storm {
                  */
                 storm::solver::MultiplicationStyle getValueIterationMultiplicationStyle() const;
                 
+                /*!
+                 * Retrievew whether updates in interval iteration have to be made symmetrically
+                 */
+                bool isForceIntervalIterationSymmetricUpdatesSet() const;
+                
                 /*!
                  * Retrieves whether the  force bounds option has been set.
                  */
@@ -123,6 +128,7 @@ namespace storm {
                 static const std::string absoluteOptionName;
                 static const std::string lraMethodOptionName;
                 static const std::string valueIterationMultiplicationStyleOptionName;
+                static const std::string intervalIterationSymmetricUpdatesOptionName;
                 static const std::string forceBoundsOptionName;
                 static const std::string quickValueIterationRestartOptionName;
             };

src/storm/settings/modules/NativeEquationSolverSettings.cpp

@@ -24,6 +24,7 @@ namespace storm {
             const std::string NativeEquationSolverSettings::absoluteOptionName = "absolute";
             const std::string NativeEquationSolverSettings::powerMethodMultiplicationStyleOptionName = "powmult";
             const std::string NativeEquationSolverSettings::forceBoundsOptionName = "forcebounds";
+            const std::string NativeEquationSolverSettings::powerMethodSymmetricUpdatesOptionName = "symmetricupdates";
 
             NativeEquationSolverSettings::NativeEquationSolverSettings() : ModuleSettings(moduleName) {
                 std::vector<std::string> methods = { "jacobi", "gaussseidel", "sor", "walkerchae", "power", "ratsearch", "qpower" };
@@ -43,6 +44,7 @@ namespace storm {
                                 
                 this->addOption(storm::settings::OptionBuilder(moduleName, forceBoundsOptionName, false, "If set, the equation solver always require that a priori bounds for the solution are computed.").build());
                 
+                this->addOption(storm::settings::OptionBuilder(moduleName, powerMethodSymmetricUpdatesOptionName, false, "If set, interval iteration performs an update on both, lower and upper bound in each iteration").build());
             }
             
             bool NativeEquationSolverSettings::isLinearEquationSystemTechniqueSet() const {
@@ -111,6 +113,10 @@ namespace storm {
                 STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown multiplication style '" << multiplicationStyleString << "'.");
             }
             
+            bool NativeEquationSolverSettings::isForcePowerMethodSymmetricUpdatesSet() const {
+                return this->getOption(powerMethodSymmetricUpdatesOptionName).getHasOptionBeenSet();
+            }
+
             bool NativeEquationSolverSettings::isForceBoundsSet() const {
                 return this->getOption(forceBoundsOptionName).getHasOptionBeenSet();
             }

src/storm/settings/modules/NativeEquationSolverSettings.h

@@ -93,6 +93,11 @@ namespace storm {
                  */
                 ConvergenceCriterion getConvergenceCriterion() const;
                 
+                /*!
+                 * Retrievew whether updates in power method have to be made symmetrically
+                 */
+                bool isForcePowerMethodSymmetricUpdatesSet() const;
+                
                 /*!
                  * Retrieves the multiplication style to use in the power method.
                  *
@@ -118,6 +123,7 @@ namespace storm {
                 static const std::string maximalIterationsOptionShortName;
                 static const std::string precisionOptionName;
                 static const std::string absoluteOptionName;
+                static const std::string powerMethodSymmetricUpdatesOptionName;
                 static const std::string powerMethodMultiplicationStyleOptionName;
                 static const std::string forceBoundsOptionName;
 

src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp

@@ -465,7 +465,7 @@ namespace storm {
             
             SolverStatus status = SolverStatus::InProgress;
             bool doConvergenceCheck = true;
-            bool useDiffs = this->hasRelevantValues();
+            bool useDiffs = this->hasRelevantValues() && !env.solver().minMax().isSymmetricUpdatesSet();
             std::vector<ValueType> oldValues;
             if (useGaussSeidelMultiplication && useDiffs) {
                 oldValues.resize(this->getRelevantValues().getNumberOfSetBits());

src/storm/solver/NativeLinearEquationSolver.cpp

@@ -417,7 +417,7 @@ namespace storm {
             bool terminate = false;
             uint64_t iterations = 0;
             bool doConvergenceCheck = true;
-            bool useDiffs = this->hasRelevantValues();
+            bool useDiffs = this->hasRelevantValues() && !env.solver().native().isSymmetricUpdatesSet();
             std::vector<ValueType> oldValues;
             if (useGaussSeidelMultiplication && useDiffs) {
                 oldValues.resize(this->getRelevantValues().getNumberOfSetBits());