LP solver support improvements (#536)

* update soplex cmake script to show version * gurobi version 11.0.2 support * add --nogurobi flag to tests * Dockerfile with platform argument which is important when building local images on a mac and options to build with soplex/gurobi * check for gurobi license at start of tests * Enable Gurobi in CI again --------- Co-authored-by: Matthias Volk <[email protected]>
moves-rwth · Jun 1, 2024 · 7390f75 · 7390f75
1 parent 859167d
commit 7390f75
Show file tree

Hide file tree

Showing 22 changed files with 112 additions and 23 deletions.
diff --git a/.github/workflows/buildtest.yml b/.github/workflows/buildtest.yml
@@ -25,7 +25,7 @@ jobs:
           - {name: "GMP exact; GMP rational functions; All dependencies",
              baseImg: "storm-dependencies:latest-debug",
              buildType: "Debug",
-             Gurobi: "OFF",
+             Gurobi: "ON",
              Soplex: "ON",
              Spot: "ON",
              Developer: "ON",
@@ -37,7 +37,7 @@ jobs:
           - {name: "CLN exact; GMP rational functions; All dependencies",
              baseImg: "storm-dependencies:latest-debug",
              buildType: "Debug",
-             Gurobi: "OFF",
+             Gurobi: "ON",
              Soplex: "ON",
              Spot: "ON",
              Developer: "ON",
@@ -49,7 +49,7 @@ jobs:
           - {name: "CLN exact; CLN rational functions; All dependencies",
              baseImg: "storm-dependencies:latest-debug",
              buildType: "Debug",
-             Gurobi: "OFF",
+             Gurobi: "ON",
              Soplex: "ON",
              Spot: "ON",
              Developer: "ON",
@@ -217,13 +217,11 @@ jobs:
           - {name: "Debug",
              dockerTag: "ci-debug",
              baseImg: "storm-dependencies:latest-debug",
-             Gurobi: "OFF",
              Developer: "ON"
             }
           - {name: "Release",
              dockerTag: "ci",
              baseImg: "storm-dependencies:latest",
-             Gurobi: "OFF",
              Developer: "OFF"
             }
     steps:
@@ -240,7 +238,6 @@ jobs:
             --build-arg BASE_IMG=movesrwth/${{ matrix.buildType.baseImg }} \
             --build-arg build_type="${{ matrix.buildType.name }}" \
             --build-arg developer="${{ matrix.buildType.Developer }}" \
-            --build-arg gurobi_support="${{ matrix.config.Gurobi }}" \
             --build-arg cmake_args="${{ matrix.buildType.cmakeArgs }}" \
             --build-arg no_threads=${NR_JOBS}
             # Omitting arguments gurobi_support, soplex_support, spot_support, cln_exact, cln_ratfunc, all_sanitizers

diff --git a/Dockerfile b/Dockerfile
@@ -7,7 +7,8 @@
 
 # Set base image
 ARG BASE_IMG=movesrwth/storm-dependencies:latest
-FROM $BASE_IMG
+ARG BASE_PLATFORM=linux/amd64
+FROM --platform=$BASE_PLATFORM  $BASE_IMG
 MAINTAINER Matthias Volk <[email protected]>
 
 # Specify configurations

diff --git a/resources/3rdparty/include_soplex.cmake b/resources/3rdparty/include_soplex.cmake
@@ -4,7 +4,7 @@ if (STORM_USE_SOPLEX)
     IF(SOPLEX_FOUND)
         get_target_property(soplexLOC libsoplex-pic LOCATION)
         get_target_property(soplexINCLUDE libsoplex-pic INTERFACE_INCLUDE_DIRECTORIES)
-        MESSAGE(STATUS "Storm - Linking with SoPlex: (libary: ${soplexLOC}; include: ${soplexINCLUDE})")
+        MESSAGE(STATUS "Storm - Linking with SoPlex version ${soplex_VERSION}: (libary: ${soplexLOC}; include: ${soplexINCLUDE})")
         list(APPEND STORM_DEP_TARGETS libsoplex-pic)
     ELSE(SOPLEX_FOUND)
         MESSAGE(WARNING "Storm not linking with SoPlex!")

diff --git a/resources/cmake/find_modules/FindGUROBI.cmake b/resources/cmake/find_modules/FindGUROBI.cmake
@@ -18,6 +18,7 @@ else (GUROBI_INCLUDE_DIR)
 find_path(GUROBI_INCLUDE_DIR 
           NAMES gurobi_c++.h
           PATHS "$ENV{GUROBI_HOME}/include"
+                    "/Library/gurobi1102/macos_universal2/include"
                     "/Library/gurobi1100/macos_universal2/include"
                     "/Library/gurobi1000/macos_universal2/include"
                     "/Library/gurobi951/macos_universal2/include"
@@ -60,6 +61,7 @@ find_library( GUROBI_LIBRARY
         gurobi46
         gurobi45
               PATHS "$ENV{GUROBI_HOME}/lib"
+                    "/Library/gurobi1102/macos_universal2/lib"
                     "/Library/gurobi1100/macos_universal2/lib"
                     "/Library/gurobi1000/macos_universal2/lib"
                     "/Library/gurobi951/macos_universal2/lib"
@@ -84,6 +86,7 @@ find_library( GUROBI_LIBRARY
 find_library( GUROBI_CXX_LIBRARY 
               NAMES gurobi_c++
               PATHS "$ENV{GUROBI_HOME}/lib"
+                    "/Library/gurobi1102/macos_universal2/lib"
                     "/Library/gurobi1100/macos_universal2/lib"
                     "/Library/gurobi951/macos_universal2/lib"
                     "/Library/gurobi950/mac64/lib"

diff --git a/src/storm/exceptions/GurobiLicenseException.h b/src/storm/exceptions/GurobiLicenseException.h
@@ -0,0 +1,10 @@
+#pragma once
+
+#include "storm/exceptions/BaseException.h"
+#include "storm/exceptions/ExceptionMacros.h"
+
+namespace storm::exceptions {
+// An exception that occurs if there is a problem with the gurubi license.
+STORM_NEW_EXCEPTION(GurobiLicenseException)
+
+}  // namespace storm::exceptions
diff --git a/src/storm/solver/GurobiLpSolver.cpp b/src/storm/solver/GurobiLpSolver.cpp
@@ -15,6 +15,7 @@
 #include "storm/storage/expressions/Expression.h"
 #include "storm/storage/expressions/ExpressionManager.h"
 
+#include "storm/exceptions/GurobiLicenseException.h"
 #include "storm/exceptions/InvalidAccessException.h"
 #include "storm/exceptions/InvalidArgumentException.h"
 #include "storm/exceptions/InvalidStateException.h"
@@ -43,6 +44,11 @@ void GurobiEnvironment::initialize() {
     // Create the environment.
     int error = GRBloadenv(&env, "");
     if (error || env == nullptr) {
+        if (error == 10009) {
+            STORM_LOG_ERROR("Gurobi License Issue. " << GRBgeterrormsg(env) << ", error code " << error << ").");
+            throw storm::exceptions::GurobiLicenseException()
+                << "Could not initialize Gurobi environment (" << GRBgeterrormsg(env) << ", error code " << error << ").";
+        }
         STORM_LOG_ERROR("Could not initialize Gurobi (" << GRBgeterrormsg(env) << ", error code " << error << ").");
         throw storm::exceptions::InvalidStateException()
             << "Could not initialize Gurobi environment (" << GRBgeterrormsg(env) << ", error code " << error << ").";

diff --git a/src/test/storm-dft/CMakeLists.txt b/src/test/storm-dft/CMakeLists.txt
@@ -12,7 +12,7 @@ include_directories(${GMOCK_INCLUDE_DIR})
 
 foreach (testsuite api bdd simulator storage transformations)
 
-	  file(GLOB_RECURSE TEST_${testsuite}_FILES ${STORM_TESTS_BASE_PATH}/${testsuite}/*.h ${STORM_TESTS_BASE_PATH}/${testsuite}/*.cpp)
+	  file(GLOB_RECURSE TEST_${testsuite}_FILES ${STORM_TESTS_BASE_PATH}/${testsuite}/*.h ${STORM_TESTS_BASE_PATH}/${testsuite}/*.cpp ${STORM_TESTS_BASE_PATH}/../storm_gtest.cpp)
       add_executable (test-dft-${testsuite} ${TEST_${testsuite}_FILES} ${STORM_TESTS_BASE_PATH}/storm-test.cpp)
 	  target_link_libraries(test-dft-${testsuite} storm-dft storm-parsers)
 	  target_link_libraries(test-dft-${testsuite} ${STORM_TEST_LINK_LIBRARIES})

diff --git a/src/test/storm-dft/storm-test.cpp b/src/test/storm-dft/storm-test.cpp
@@ -3,7 +3,7 @@
 
 int main(int argc, char **argv) {
     storm::dft::settings::initializeDftSettings("Storm-dft (Functional) Testing Suite", "test-dft");
-    storm::test::initialize();
     ::testing::InitGoogleTest(&argc, argv);
+    storm::test::initialize(&argc, argv);
     return RUN_ALL_TESTS();
 }
diff --git a/src/test/storm-gamebased-ar/CMakeLists.txt b/src/test/storm-gamebased-ar/CMakeLists.txt
@@ -10,7 +10,7 @@ register_source_groups_from_filestructure("${ALL_FILES}" test)
 include_directories(${GTEST_INCLUDE_DIR})
 
 foreach (testsuite modelchecker abstraction)
-    file(GLOB_RECURSE TEST_${testsuite}_FILES ${STORM_TESTS_BASE_PATH}/${testsuite}/*.h ${STORM_TESTS_BASE_PATH}/${testsuite}/*.cpp)
+    file(GLOB_RECURSE TEST_${testsuite}_FILES ${STORM_TESTS_BASE_PATH}/${testsuite}/*.h ${STORM_TESTS_BASE_PATH}/${testsuite}/*.cpp ${STORM_TESTS_BASE_PATH}/../storm_gtest.cpp)
     add_executable(test-gamebased-ar-${testsuite} ${TEST_${testsuite}_FILES} ${STORM_TESTS_BASE_PATH}/storm-test.cpp)
     target_link_libraries(test-gamebased-ar-${testsuite} storm-gamebased-ar storm-parsers)
     target_link_libraries(test-gamebased-ar-${testsuite} ${STORM_TEST_LINK_LIBRARIES})

diff --git a/src/test/storm-gamebased-ar/storm-test.cpp b/src/test/storm-gamebased-ar/storm-test.cpp
@@ -3,7 +3,7 @@
 
 int main(int argc, char **argv) {
     storm::settings::initializeAll("Storm-gamebased-ar (Functional) Testing Suite", "test-gamebased-ar");
-    storm::test::initialize();
     ::testing::InitGoogleTest(&argc, argv);
+    storm::test::initialize(&argc, argv);
     return RUN_ALL_TESTS();
 }
diff --git a/src/test/storm-pars/CMakeLists.txt b/src/test/storm-pars/CMakeLists.txt
@@ -11,7 +11,7 @@ include_directories(${GTEST_INCLUDE_DIR})
 
 foreach (testsuite analysis modelchecker utility derivative transformer)
 
-	  file(GLOB_RECURSE TEST_${testsuite}_FILES ${STORM_TESTS_BASE_PATH}/${testsuite}/*.h ${STORM_TESTS_BASE_PATH}/${testsuite}/*.cpp)
+	  file(GLOB_RECURSE TEST_${testsuite}_FILES ${STORM_TESTS_BASE_PATH}/${testsuite}/*.h ${STORM_TESTS_BASE_PATH}/${testsuite}/*.cpp ${STORM_TESTS_BASE_PATH}/../storm_gtest.cpp)
       add_executable (test-pars-${testsuite} ${TEST_${testsuite}_FILES} ${STORM_TESTS_BASE_PATH}/storm-test.cpp analysis/MonotonicityCheckerTest.cpp)
 	  target_link_libraries(test-pars-${testsuite} storm-pars storm-parsers)
 	  target_link_libraries(test-pars-${testsuite} ${STORM_TEST_LINK_LIBRARIES})

diff --git a/src/test/storm-pars/storm-test.cpp b/src/test/storm-pars/storm-test.cpp
@@ -3,7 +3,7 @@
 
 int main(int argc, char **argv) {
     storm::settings::initializeParsSettings("Storm-pars (Functional) Testing Suite", "test-pars");
-    storm::test::initialize();
     ::testing::InitGoogleTest(&argc, argv);
+    storm::test::initialize(&argc, argv);
     return RUN_ALL_TESTS();
 }
diff --git a/src/test/storm-permissive/CMakeLists.txt b/src/test/storm-permissive/CMakeLists.txt
@@ -11,7 +11,7 @@ include_directories(${GTEST_INCLUDE_DIR})
 
 foreach (testsuite analysis)
     file(GLOB_RECURSE TEST_${testsuite}_FILES ${STORM_TESTS_BASE_PATH}/${testsuite}/*.h ${STORM_TESTS_BASE_PATH}/${testsuite}/*.cpp)
-    add_executable(test-permissive-${testsuite} ${TEST_${testsuite}_FILES} ${STORM_TESTS_BASE_PATH}/storm-test.cpp)
+    add_executable(test-permissive-${testsuite} ${TEST_${testsuite}_FILES} ${STORM_TESTS_BASE_PATH}/storm-test.cpp ${STORM_TESTS_BASE_PATH}/../storm_gtest.cpp)
     target_link_libraries(test-permissive-${testsuite} storm-permissive storm-parsers)
     target_link_libraries(test-permissive-${testsuite} ${STORM_TEST_LINK_LIBRARIES})
 

diff --git a/src/test/storm-permissive/analysis/MilpPermissiveSchedulerTest.cpp b/src/test/storm-permissive/analysis/MilpPermissiveSchedulerTest.cpp
@@ -15,6 +15,9 @@
 #ifdef STORM_HAVE_GUROBI
 
 TEST(MilpPermissiveSchedulerTest, DieSelection) {
+    if (storm::test::noGurobi) {
+        GTEST_SKIP();
+    }
     storm::Environment env;
 
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/die_c1.nm");

diff --git a/src/test/storm-permissive/storm-test.cpp b/src/test/storm-permissive/storm-test.cpp
@@ -3,7 +3,7 @@
 
 int main(int argc, char **argv) {
     storm::settings::initializeAll("Storm-permissive (Functional) Testing Suite", "test-permissive");
-    storm::test::initialize();
     ::testing::InitGoogleTest(&argc, argv);
+    storm::test::initialize(&argc, argv);
     return RUN_ALL_TESTS();
 }
diff --git a/src/test/storm-pomdp/CMakeLists.txt b/src/test/storm-pomdp/CMakeLists.txt
@@ -11,7 +11,7 @@ include_directories(${GTEST_INCLUDE_DIR})
 
 foreach (testsuite analysis transformation modelchecker tracking api)
 
-	  file(GLOB_RECURSE TEST_${testsuite}_FILES ${STORM_TESTS_BASE_PATH}/${testsuite}/*.h ${STORM_TESTS_BASE_PATH}/${testsuite}/*.cpp)
+	  file(GLOB_RECURSE TEST_${testsuite}_FILES ${STORM_TESTS_BASE_PATH}/${testsuite}/*.h ${STORM_TESTS_BASE_PATH}/${testsuite}/*.cpp ${STORM_TESTS_BASE_PATH}/../storm_gtest.cpp)
       add_executable (test-pomdp-${testsuite} ${TEST_${testsuite}_FILES} ${STORM_TESTS_BASE_PATH}/storm-test.cpp)
 	  target_link_libraries(test-pomdp-${testsuite} storm-pomdp storm-parsers)
 	  target_link_libraries(test-pomdp-${testsuite} ${STORM_TEST_LINK_LIBRARIES})

diff --git a/src/test/storm-pomdp/storm-test.cpp b/src/test/storm-pomdp/storm-test.cpp
@@ -3,7 +3,7 @@
 
 int main(int argc, char **argv) {
     storm::settings::initializeAll("Storm-pomdp (Functional) Testing Suite", "test-pomdp");
-    storm::test::initialize();
     ::testing::InitGoogleTest(&argc, argv);
+    storm::test::initialize(&argc, argv);
     return RUN_ALL_TESTS();
 }
diff --git a/src/test/storm/CMakeLists.txt b/src/test/storm/CMakeLists.txt
@@ -26,7 +26,7 @@ endfunction()
 
 set(REUSE_PCH_FROM "")
 foreach(testsuite ${NON_SPLIT_TESTS})
-	file(GLOB_RECURSE TEST_${testsuite}_FILES ${STORM_TESTS_BASE_PATH}/${testsuite}/*.h ${STORM_TESTS_BASE_PATH}/${testsuite}/*.cpp)
+	file(GLOB_RECURSE TEST_${testsuite}_FILES ${STORM_TESTS_BASE_PATH}/${testsuite}/*.h ${STORM_TESTS_BASE_PATH}/${testsuite}/*.cpp ${STORM_TESTS_BASE_PATH}/../storm_gtest.cpp)
 	add_executable(test-${testsuite} ${TEST_${testsuite}_FILES} ${STORM_TESTS_BASE_PATH}/storm-test.cpp)
 	if (REUSE_PCH_FROM STREQUAL  "")
 		# note that reusing from storm main leads to errors on arch linux (late 2023).
@@ -40,15 +40,15 @@ endforeach()
 
 # Modelchecker testsuite split
 foreach(modelchecker_split ${MODELCHECKER_TEST_SPLITS})
-	file(GLOB_RECURSE TEST_MODELCHECKER_${modelchecker_split}_FILES ${STORM_TESTS_BASE_PATH}/modelchecker/${modelchecker_split}/*.h ${STORM_TESTS_BASE_PATH}/modelchecker/${modelchecker_split}/*.cpp)
+	file(GLOB_RECURSE TEST_MODELCHECKER_${modelchecker_split}_FILES ${STORM_TESTS_BASE_PATH}/modelchecker/${modelchecker_split}/*.h ${STORM_TESTS_BASE_PATH}/modelchecker/${modelchecker_split}/*.cpp ${STORM_TESTS_BASE_PATH}/../storm_gtest.cpp)
 	add_executable(test-modelchecker-${modelchecker_split} ${TEST_MODELCHECKER_${modelchecker_split}_FILES} ${STORM_TESTS_BASE_PATH}/storm-test.cpp)
 	configure_testsuite_target(modelchecker-${modelchecker_split})
 	target_precompile_headers(test-modelchecker-${modelchecker_split} REUSE_FROM ${REUSE_PCH_FROM})
 endforeach()
 
 # Modelchecker-Prctl testsuite split
 foreach(prctl_split ${MODELCHECKER_PRCTL_TEST_SPLITS})
-	file(GLOB_RECURSE TEST_MODELCHECKER_PRCTL_${prctl_split}_FILES ${STORM_TESTS_BASE_PATH}/modelchecker/prctl/${prctl_split}/*.h ${STORM_TESTS_BASE_PATH}/modelchecker/prctl/${prctl_split}/*.cpp)
+	file(GLOB_RECURSE TEST_MODELCHECKER_PRCTL_${prctl_split}_FILES ${STORM_TESTS_BASE_PATH}/modelchecker/prctl/${prctl_split}/*.h ${STORM_TESTS_BASE_PATH}/modelchecker/prctl/${prctl_split}/*.cpp ${STORM_TESTS_BASE_PATH}/../storm_gtest.cpp)
 	add_executable(test-modelchecker-prctl-${prctl_split} ${TEST_MODELCHECKER_PRCTL_${prctl_split}_FILES} ${STORM_TESTS_BASE_PATH}/storm-test.cpp)
 	configure_testsuite_target(modelchecker-prctl-${prctl_split})
 	target_precompile_headers(test-modelchecker-prctl-${prctl_split} REUSE_FROM ${REUSE_PCH_FROM})

diff --git a/src/test/storm/solver/LpSolverTest.cpp b/src/test/storm/solver/LpSolverTest.cpp
@@ -20,6 +20,10 @@ class DefaultEnvironment {
     static const bool IntegerSupport = true;
     static const bool IncrementalSupport = true;
     static const bool strictRelationSupport = true;
+
+    static bool skip() {
+        return false;
+    }
 };
 
 class GlpkEnvironment {
@@ -30,6 +34,10 @@ class GlpkEnvironment {
     static const bool IntegerSupport = true;
     static const bool IncrementalSupport = true;
     static const bool strictRelationSupport = true;
+
+    static bool skip() {
+        return false;
+    }
 };
 
 #ifdef STORM_HAVE_GUROBI
@@ -41,6 +49,10 @@ class GurobiEnvironment {
     static const bool IntegerSupport = true;
     static const bool IncrementalSupport = true;
     static const bool strictRelationSupport = true;
+
+    static bool skip() {
+        return storm::test::noGurobi;
+    }
 };
 #endif
 
@@ -52,6 +64,10 @@ class Z3Environment {
     static const bool IntegerSupport = true;
     static const bool IncrementalSupport = true;
     static const bool strictRelationSupport = true;
+
+    static bool skip() {
+        return false;
+    }
 };
 
 #ifdef STORM_HAVE_SOPLEX
@@ -63,6 +79,10 @@ class SoplexEnvironment {
     static const bool IntegerSupport = false;
     static const bool IncrementalSupport = false;
     static const bool strictRelationSupport = false;
+
+    static bool skip() {
+        return false;
+    }
 };
 
 class SoplexExactEnvironment {
@@ -73,6 +93,10 @@ class SoplexExactEnvironment {
     static const bool IntegerSupport = false;
     static const bool IncrementalSupport = false;
     static const bool strictRelationSupport = false;
+
+    static bool skip() {
+        return false;
+    }
 };
 #endif
 
@@ -81,6 +105,12 @@ class LpSolverTest : public ::testing::Test {
    public:
     typedef typename TestType::ValueType ValueType;
 
+    void SetUp() override {
+        if (skipped()) {
+            GTEST_SKIP();
+        }
+    }
+
     storm::solver::LpSolverTypeSelection solverSelection() const {
         return TestType::solverSelection;
     }
@@ -108,6 +138,10 @@ class LpSolverTest : public ::testing::Test {
     bool supportsStrictRelation() const {
         return TestType::strictRelationSupport;
     }
+
+    bool skipped() const {
+        return TestType::skip();
+    }
 };
 
 typedef ::testing::Types<DefaultEnvironment

diff --git a/src/test/storm/storm-test.cpp b/src/test/storm/storm-test.cpp
@@ -3,7 +3,7 @@
 
 int main(int argc, char **argv) {
     storm::settings::initializeAll("Storm (Functional) Testing Suite", "test");
-    storm::test::initialize();
     ::testing::InitGoogleTest(&argc, argv);
+    storm::test::initialize(&argc, argv);
     return RUN_ALL_TESTS();
 }
diff --git a/src/test/storm_gtest.cpp b/src/test/storm_gtest.cpp
@@ -0,0 +1,22 @@
+#include "test/storm_gtest.h"
+
+#include "storm/exceptions/GurobiLicenseException.h"
+#include "storm/solver/GurobiLpSolver.h"
+#include "storm/utility/solver.h"
+
+namespace storm::test {
+bool noGurobi = false;
+
+bool testGurobiLicense() {
+#ifdef STORM_HAVE_GUROBI
+    try {
+        auto lpSolver = storm::utility::solver::getLpSolver<double>("test", storm::solver::LpSolverTypeSelection::Gurobi);
+    } catch (storm::exceptions::GurobiLicenseException) {
+        return false;
+    }
+    return true;
+#else
+    return false;
+#endif
+}
+}  // namespace storm::test
diff --git a/src/test/storm_gtest.h b/src/test/storm_gtest.h
@@ -42,10 +42,23 @@ inline GTEST_API_ AssertionResult DoubleNearPredFormat(const char* expr1, const
 
 namespace storm {
 namespace test {
-inline void initialize() {
+extern bool noGurobi;
+
+bool testGurobiLicense();
+
+inline void initialize(int* argc, char** argv) {
+    // GoogleTest-specific commandline arguments should already be processed before and removed from argc/argv
     storm::utility::initializeLogger();
     // Only enable error output by default.
     storm::utility::setLogLevel(l3pp::LogLevel::ERR);
+    noGurobi = !storm::test::testGurobiLicense();
+    for (int i = 1; i < *argc; ++i) {
+        if (std::string(argv[i]) == "--nogurobi") {
+            noGurobi = true;
+        } else {
+            STORM_LOG_WARN("Unknown argument: " << argv[i]);
+        }
+    }
 }
 
 inline void enableErrorOutput() {