make minmax solvers use policy iteration when --exact is set and no other method was explicitly set

src/storm/settings/Argument.cpp

@@ -12,12 +12,12 @@ namespace storm {
     namespace settings {
         
         template<typename T>
-        Argument<T>::Argument(std::string const& name, std::string const& description, std::vector<std::shared_ptr<ArgumentValidator<T>>> const& validators): ArgumentBase(name, description), argumentValue(), argumentType(inferToEnumType<T>()), validators(validators), isOptional(false), defaultValue(), hasDefaultValue(false) {
+        Argument<T>::Argument(std::string const& name, std::string const& description, std::vector<std::shared_ptr<ArgumentValidator<T>>> const& validators): ArgumentBase(name, description), argumentValue(), argumentType(inferToEnumType<T>()), validators(validators), isOptional(false), defaultValue(), hasDefaultValue(false), wasSetFromDefaultValueFlag(false) {
             // Intentionally left empty.
         }
         
         template<typename T>
-        Argument<T>::Argument(std::string const& name, std::string const& description, std::vector<std::shared_ptr<ArgumentValidator<T>>> const& validators, bool isOptional, T defaultValue): ArgumentBase(name, description), argumentValue(), argumentType(inferToEnumType<T>()), validators(validators), isOptional(isOptional), defaultValue(), hasDefaultValue(true) {
+        Argument<T>::Argument(std::string const& name, std::string const& description, std::vector<std::shared_ptr<ArgumentValidator<T>>> const& validators, bool isOptional, T defaultValue): ArgumentBase(name, description), argumentValue(), argumentType(inferToEnumType<T>()), validators(validators), isOptional(isOptional), defaultValue(), hasDefaultValue(true), wasSetFromDefaultValueFlag(false) {
             this->setDefaultValue(defaultValue);
         }
         
@@ -71,6 +71,12 @@ namespace storm {
             STORM_LOG_THROW(this->hasDefaultValue, storm::exceptions::IllegalFunctionCallException, "Unable to set value from default value, because the argument " << name << " has none.");
             bool result = this->setFromTypeValue(this->defaultValue, false);
             STORM_LOG_THROW(result, storm::exceptions::IllegalArgumentValueException, "Unable to assign default value to argument " << name << ", because it was rejected.");
+            this->wasSetFromDefaultValueFlag = true;
+        }
+        
+        template<typename T>
+        bool Argument<T>::wasSetFromDefaultValue() const {
+            return wasSetFromDefaultValueFlag;
         }
         
         template<typename T>

src/storm/settings/Argument.h

@@ -85,6 +85,8 @@ namespace storm {
             
             void setFromDefaultValue() override;
             
+            virtual bool wasSetFromDefaultValue() const override;
+
             virtual std::string getValueAsString() const override;
             
             virtual int_fast64_t getValueAsInteger() const override;
@@ -116,6 +118,9 @@ namespace storm {
             // A flag indicating whether a default value has been provided.
             bool hasDefaultValue;
             
+            // A flag indicating whether the argument was set from the default value.
+            bool wasSetFromDefaultValueFlag;
+            
             /*!
              * Sets the default value of the argument to the provided value.
              *

src/storm/settings/ArgumentBase.h

@@ -80,6 +80,8 @@ namespace storm {
              */
 			virtual void setFromDefaultValue() = 0;
 
+            virtual bool wasSetFromDefaultValue() const = 0;
+            
             /*!
              * Tries to set the value of the argument from the given string.
              *
@@ -134,7 +136,7 @@ namespace storm {
             
             friend std::ostream& operator<<(std::ostream& out, ArgumentBase const& argument);
             
-		protected:            
+		protected:
             // A flag indicating whether the argument has been set.
 			bool hasBeenSet;
 

src/storm/settings/modules/MinMaxEquationSolverSettings.cpp

@@ -50,6 +50,10 @@ namespace storm {
                 STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown min/max equation solving technique '" << minMaxEquationSolvingTechnique << "'.");
             }
             
+            bool MinMaxEquationSolverSettings::isMinMaxEquationSolvingMethodSetFromDefaultValue() const {
+                return !this->getOption(solvingMethodOptionName).getArgumentByName("name").getHasBeenSet() || this->getOption(solvingMethodOptionName).getArgumentByName("name").wasSetFromDefaultValue();
+            }
+            
             bool MinMaxEquationSolverSettings::isMinMaxEquationSolvingMethodSet() const {
                 return this->getOption(solvingMethodOptionName).getHasOptionBeenSet();
             }

src/storm/settings/modules/MinMaxEquationSolverSettings.h

@@ -27,12 +27,19 @@ namespace storm {
                 bool isMinMaxEquationSolvingMethodSet() const;
                 
                 /*!
-                 * Retrieves the selected min/max equation solving technique.
+                 * Retrieves the selected min/max equation solving method.
                  *
-                 * @return The selected min/max equation solving technique.
+                 * @return The selected min/max equation solving method.
                  */
                 storm::solver::MinMaxMethod getMinMaxEquationSolvingMethod() const;
                 
+                /*!
+                 * Retrieves whether the min/max equation solving method is set from its default value.
+                 *
+                 * @return True iff if it is set from its default value.
+                 */
+                bool isMinMaxEquationSolvingMethodSetFromDefaultValue() const;
+                
                 /*!
                  * Retrieves whether the maximal iteration count has been set.
                  *

src/storm/solver/IterativeMinMaxLinearEquationSolver.h

@@ -73,7 +73,7 @@ namespace storm {
             IterativeMinMaxLinearEquationSolverSettings<ValueType> settings;
         };
         
-                template<typename ValueType>
+        template<typename ValueType>
         class IterativeMinMaxLinearEquationSolverFactory : public StandardMinMaxLinearEquationSolverFactory<ValueType> {
         public:
             IterativeMinMaxLinearEquationSolverFactory(MinMaxMethodSelection const& method = MinMaxMethodSelection::FROMSETTINGS, bool trackScheduler = false);

src/storm/solver/MinMaxLinearEquationSolver.cpp

@@ -154,7 +154,19 @@ namespace storm {
         template<typename ValueType>
         void MinMaxLinearEquationSolverFactory<ValueType>::setMinMaxMethod(MinMaxMethodSelection const& newMethod) {
             if (newMethod == MinMaxMethodSelection::FROMSETTINGS) {
-                setMinMaxMethod(storm::settings::getModule<storm::settings::modules::MinMaxEquationSolverSettings>().getMinMaxEquationSolvingMethod());
+                bool wasSet = false;
+                auto const& minMaxSettings = storm::settings::getModule<storm::settings::modules::MinMaxEquationSolverSettings>();
+                if (std::is_same<ValueType, storm::RationalNumber>::value) {
+                    if (minMaxSettings.isMinMaxEquationSolvingMethodSetFromDefaultValue()) {
+                        STORM_LOG_WARN("Selecting policy iteration as the solution method to guarantee exact results. If you want to override this, please explicitly specify a different method.");
+                        this->setMinMaxMethod(MinMaxMethod::PolicyIteration);
+                        wasSet = true;
+                    }
+                }
+                
+                if (!wasSet) {
+                    setMinMaxMethod(minMaxSettings.getMinMaxEquationSolvingMethod());
+                }
             } else {
                 setMinMaxMethod(convert(newMethod));
             }
@@ -162,6 +174,7 @@ namespace storm {
         
         template<typename ValueType>
         void MinMaxLinearEquationSolverFactory<ValueType>::setMinMaxMethod(MinMaxMethod const& newMethod) {
+            STORM_LOG_WARN_COND(!(std::is_same<ValueType, storm::RationalNumber>::value) || newMethod == MinMaxMethod::PolicyIteration, "The selected solution method does not guarantee exact result. Consider using policy iteration.");
             method = newMethod;
         }