In exact mode, use LP as LRA Method for nondeterministic models.

src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp

@@ -16,6 +16,7 @@
 #include "storm/utility/macros.h"
 #include "storm/utility/vector.h"
 #include "storm/utility/graph.h"
+#include "storm/utility/NumberTraits.h"
 
 #include "storm/storage/expressions/Variable.h"
 #include "storm/storage/expressions/Expression.h"
@@ -824,7 +825,12 @@ namespace storm {
                 }
                 
                 // Solve MEC with the method specified in the settings
-                storm::solver::LraMethod method = storm::settings::getModule<storm::settings::modules::MinMaxEquationSolverSettings>().getLraMethod();
+                auto minMaxSettings = storm::settings::getModule<storm::settings::modules::MinMaxEquationSolverSettings>();
+                storm::solver::LraMethod method = minMaxSettings.getLraMethod();
+                if (storm::NumberTraits<ValueType>::IsExact && minMaxSettings.isLraMethodSetFromDefaultValue() && method != storm::solver::LraMethod::LinearProgramming) {
+                    STORM_LOG_INFO("Selecting 'LP' as the solution technique for long-run properties to guarantee exact results. If you want to override this, please explicitly specify a different LRA method.");
+                    method = storm::solver::LraMethod::LinearProgramming;
+                }
                 if (method == storm::solver::LraMethod::LinearProgramming) {
                     return computeLraForMaximalEndComponentLP(env, dir, transitionMatrix, exitRateVector, markovianStates, rewardModel, mec);
                 } else if (method == storm::solver::LraMethod::ValueIteration) {

src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp

@@ -34,6 +34,7 @@
 #include "storm/utility/Stopwatch.h"
 #include "storm/utility/ProgressMeasurement.h"
 #include "storm/utility/export.h"
+#include "storm/utility/NumberTraits.h"
 
 #include "storm/transformer/EndComponentEliminator.h"
 
@@ -1478,7 +1479,12 @@ namespace storm {
                 }
                 
                 // Solve MEC with the method specified in the settings
-                storm::solver::LraMethod method = storm::settings::getModule<storm::settings::modules::MinMaxEquationSolverSettings>().getLraMethod();
+                auto minMaxSettings = storm::settings::getModule<storm::settings::modules::MinMaxEquationSolverSettings>();
+                storm::solver::LraMethod method = minMaxSettings.getLraMethod();
+                if (storm::NumberTraits<ValueType>::IsExact && minMaxSettings.isLraMethodSetFromDefaultValue() && method != storm::solver::LraMethod::LinearProgramming) {
+                    STORM_LOG_INFO("Selecting 'LP' as the solution technique for long-run properties to guarantee exact results. If you want to override this, please explicitly specify a different LRA method.");
+                    method = storm::solver::LraMethod::LinearProgramming;
+                }
                 if (method == storm::solver::LraMethod::LinearProgramming) {
                     return computeLraForMaximalEndComponentLP(env, dir, transitionMatrix, rewardModel, mec);
                 } else if (method == storm::solver::LraMethod::ValueIteration) {

src/storm/settings/modules/CoreSettings.cpp

@@ -112,6 +112,10 @@ namespace storm {
                 STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown LP solver '" << lpSolverName << "'.");
             }
             
+            bool CoreSettings::isLpSolverSetFromDefaultValue() const {
+                return !this->getOption(lpSolverOptionName).getHasOptionBeenSet() || this->getOption(lpSolverOptionName).getArgumentByName("name").wasSetFromDefaultValue();
+            }
+            
             storm::solver::SmtSolverType CoreSettings::getSmtSolver() const {
                 std::string smtSolverName = this->getOption(smtSolverOptionName).getArgumentByName("name").getValueAsString();
                 if (smtSolverName == "z3") {

src/storm/settings/modules/CoreSettings.h

@@ -94,6 +94,13 @@ namespace storm {
                  * @return The selected LP solver.
                  */
                 storm::solver::LpSolverType getLpSolver() const;
+                
+                /*!
+                 * Retrieves whether the lp solver has been set from its default value.
+                 *
+                 * @return True iff it has been set from its default value.
+                 */
+                bool isLpSolverSetFromDefaultValue() const;
 
                 /*!
                  * Retrieves the selected SMT solver.

src/storm/settings/modules/MinMaxEquationSolverSettings.cpp

@@ -111,6 +111,10 @@ namespace storm {
                 STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown lra solving technique '" << lraMethodString << "'.");
             }
             
+            bool MinMaxEquationSolverSettings::isLraMethodSetFromDefaultValue() const {
+                return !this->getOption(lraMethodOptionName).getArgumentByName("name").getHasBeenSet() || this->getOption(lraMethodOptionName).getArgumentByName("name").wasSetFromDefaultValue();
+            }
+            
             MinMaxEquationSolverSettings::MarkovAutomatonBoundedReachabilityMethod MinMaxEquationSolverSettings::getMarkovAutomatonBoundedReachabilityMethod() const {
                 std::string techniqueAsString = this->getOption(markovAutomatonBoundedReachabilityMethodOptionName).getArgumentByName("name").getValueAsString();
                 if (techniqueAsString == "imca") {

src/storm/settings/modules/MinMaxEquationSolverSettings.h

@@ -93,6 +93,11 @@ namespace storm {
                  */
                 storm::solver::LraMethod getLraMethod() const;
                 
+                /*!
+                 * Retrieves whether the LraMethod was set from a default value.
+                 */
+                bool isLraMethodSetFromDefaultValue() const;
+                
                 /*!
                  * Retrieves the method to be used for bounded reachability on MAs.
                  *

src/storm/utility/solver.cpp

@@ -15,6 +15,7 @@
 #include "storm/solver/MathsatSmtSolver.h"
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/CoreSettings.h"
+#include "storm/utility/NumberTraits.h"
 
 #include "storm/exceptions/InvalidSettingsException.h"
 
@@ -25,8 +26,11 @@ namespace storm {
             template<typename ValueType>
             std::unique_ptr<storm::solver::LpSolver<ValueType>> LpSolverFactory<ValueType>::create(std::string const& name, storm::solver::LpSolverTypeSelection solvT) const {
                 storm::solver::LpSolverType t;
-                if(solvT == storm::solver::LpSolverTypeSelection::FROMSETTINGS) {
+                if (solvT == storm::solver::LpSolverTypeSelection::FROMSETTINGS) {
                     t = storm::settings::getModule<storm::settings::modules::CoreSettings>().getLpSolver();
+                    if (storm::NumberTraits<ValueType>::IsExact && t != storm::solver::LpSolverType::Z3 && storm::settings::getModule<storm::settings::modules::CoreSettings>().isLpSolverSetFromDefaultValue()) {
+                        t = storm::solver::LpSolverType::Z3;
+                    }
                 } else {
                     t = convert(solvT);
                 }