From 2aa385905b5d4c38e89ea1bd6c6721323de28190 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Fri, 26 Jul 2019 08:39:20 +0200
Subject: [PATCH] DetSchedsLpChecker: Switch to gurobi by default (if
 installed)

---
 .../DeterministicSchedsLpChecker.cpp          | 37 ++++++++++++-------
 1 file changed, 23 insertions(+), 14 deletions(-)

diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp
index 3b712b271..bb54033e9 100644
--- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp
+++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp
@@ -6,7 +6,7 @@
 #include "storm/models/sparse/Mdp.h"
 #include "storm/models/sparse/StandardRewardModel.h"
 #include "storm/settings/SettingsManager.h"
-#include "storm/settings/modules/MultiObjectiveSettings.h"
+#include "storm/settings/modules/CoreSettings.h"
 #include "storm/storage/SparseMatrix.h"
 #include "storm/storage/MaximalEndComponentDecomposition.h"
 #include "storm/storage/Scheduler.h"
@@ -31,17 +31,6 @@ namespace storm {
             template <typename ModelType, typename GeometryValueType>
             void DeterministicSchedsLpChecker<ModelType, GeometryValueType>::initialize(Environment const& env) {
                 if (!lpModel) {
-                    if (env.modelchecker().multi().getEncodingType() == storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Auto) {
-                        flowEncoding = true;
-                        for (auto const& helper : objectiveHelper) {
-                            if (!helper.isTotalRewardObjective()) {
-                                flowEncoding = false;
-                            }
-                        }
-                    } else {
-                        flowEncoding = env.modelchecker().multi().getEncodingType() == storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Flow;
-                    }
-                    STORM_PRINT_AND_LOG("Using " << (flowEncoding ? "flow" : "classical") << " encoding." << std::endl);
                     swInit.start();
                     initializeLpModel(env);
                     swInit.stop();
@@ -354,10 +343,30 @@ namespace storm {
             template <typename ModelType, typename GeometryValueType>
             void DeterministicSchedsLpChecker<ModelType, GeometryValueType>::initializeLpModel(Environment const& env) {
                 STORM_LOG_INFO("Initializing LP model with " << model.getNumberOfStates() << " states.");
+                if (env.modelchecker().multi().getEncodingType() == storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Auto) {
+                    flowEncoding = true;
+                    for (auto const& helper : objectiveHelper) {
+                        if (!helper.isTotalRewardObjective()) {
+                            flowEncoding = false;
+                        }
+                    }
+                } else {
+                    flowEncoding = env.modelchecker().multi().getEncodingType() == storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Flow;
+                }
+                STORM_PRINT_AND_LOG("Using " << (flowEncoding ? "flow" : "classical") << " encoding." << std::endl);
+
                 uint64_t numStates = model.getNumberOfStates();
                 uint64_t initialState = *model.getInitialStates().begin();
-
-                lpModel = storm::utility::solver::getLpSolver<ValueType>("model");
+                if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isLpSolverSetFromDefaultValue()) {
+#ifdef STORM_HAVE_GUROBI
+                    STORM_LOG_INFO("Using Gurobi as LPSolver");
+                    lpModel = storm::utility::solver::getLpSolver<ValueType>("model", storm::solver::LpSolverTypeSelection::Gurobi);
+#else
+                    STORM_LOG_WARN("Selected LP-solver might not support incremental solving. Consider installing Gurobi.");
+#endif
+                } else {
+                    lpModel = storm::utility::solver::getLpSolver<ValueType>("model");
+                }
                 gurobiLpModel = dynamic_cast<storm::solver::GurobiLpSolver<ValueType>*>(lpModel.get());
                 
                 lpModel->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize);