diff --git a/.github/workflows/buildtest.yml b/.github/workflows/buildtest.yml index 07ecdeede..e4b173fbb 100644 --- a/.github/workflows/buildtest.yml +++ b/.github/workflows/buildtest.yml @@ -186,7 +186,6 @@ jobs: config: - {name: "GCC", buildType: "Debug", - disable_gmm: "ON", # TOOD: enable again if GMM was fixed Developer: "ON", cmakeArgs: "-DCMAKE_C_COMPILER=gcc -DCMAKE_CXX_COMPILER=g++ -DSTORM_WARNING_AS_ERROR=ON", packages: "", @@ -194,7 +193,6 @@ jobs: } - {name: "Clang", buildType: "Debug", - disable_gmm: "ON", # TOOD: enable again if GMM was fixed Developer: "ON", cmakeArgs: "-DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++ -DSTORM_WARNING_AS_ERROR=ON", packages: "clang", @@ -202,7 +200,6 @@ jobs: } - { name: "musl", buildType: "Debug", - disable_gmm: "ON", # TOOD: enable again if GMM was fixed Developer: "ON", cmakeArgs: "-DCMAKE_C_COMPILER=gcc -DCMAKE_CXX_COMPILER=g++ -DSTORM_WARNING_AS_ERROR=ON", packages: "", diff --git a/CMakeLists.txt b/CMakeLists.txt index e763b6065..43600316d 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -420,6 +420,7 @@ endif() export_option(STORM_HAVE_CUDD) export_option(STORM_HAVE_GMM) +export_option(STORM_HAVE_GMM_ILU) export_option(STORM_HAVE_GLPK) export_option(STORM_HAVE_GUROBI) export_option(STORM_HAVE_MATHSAT) diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index 0bfa0dace..f3f2b58f9 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -70,6 +70,12 @@ if(NOT STORM_DISABLE_GMM) FILES_MATCHING PATTERN "*.h" PATTERN ".git" EXCLUDE) list(APPEND STORM_DEP_TARGETS gmm) set(STORM_HAVE_GMM ON) + set(STORM_HAVE_GMM_ILU ON) + if((STORM_COMPILER_CLANG AND CMAKE_CXX_COMPILER_VERSION VERSION_GREATER 21.0) OR (STORM_COMPILER_GCC AND CMAKE_CXX_COMPILER_VERSION VERSION_GREATER 15.0)) + # GMM ILU preconditioner accesses out-of-bounds values and throws debug assertions in latest compiler versions + message(WARNING "Storm - Disabling Ilu preconditioner for Gmm due to current issues") + set(STORM_HAVE_GMM_ILU OFF) + endif() else() message(STATUS "Storm - Not linking with gmm.") set(STORM_HAVE_GMM OFF) diff --git a/src/storm-config.h.in b/src/storm-config.h.in index ff59e8354..2d5060056 100644 --- a/src/storm-config.h.in +++ b/src/storm-config.h.in @@ -78,6 +78,7 @@ // Whether the libraries are available and to be used #cmakedefine STORM_HAVE_CUDD #cmakedefine STORM_HAVE_GMM +#cmakedefine STORM_HAVE_GMM_ILU // Disable ilu preconditioner due to current issues #cmakedefine STORM_HAVE_GLPK #cmakedefine STORM_HAVE_GUROBI #cmakedefine STORM_HAVE_MATHSAT diff --git a/src/storm/solver/GmmxxLinearEquationSolver.cpp b/src/storm/solver/GmmxxLinearEquationSolver.cpp index c4f744163..94f56404a 100644 --- a/src/storm/solver/GmmxxLinearEquationSolver.cpp +++ b/src/storm/solver/GmmxxLinearEquationSolver.cpp @@ -70,7 +70,11 @@ bool GmmxxLinearEquationSolver::internalSolveEquations(Environment co method == GmmxxLinearEquationSolverMethod::Gmres) { // Make sure that the requested preconditioner is available if (preconditioner == GmmxxLinearEquationSolverPreconditioner::Ilu && !iluPreconditioner) { +#ifdef STORM_HAVE_GMM_ILU iluPreconditioner = std::make_unique>>(*gmmxxA); +#else + diagonalPreconditioner = std::make_unique>>(*gmmxxA); +#endif } else if (preconditioner == GmmxxLinearEquationSolverPreconditioner::Diagonal) { diagonalPreconditioner = std::make_unique>>(*gmmxxA); } @@ -91,7 +95,12 @@ bool GmmxxLinearEquationSolver::internalSolveEquations(Environment co // Invoke gmm with the corresponding settings if (method == GmmxxLinearEquationSolverMethod::Bicgstab) { if (preconditioner == GmmxxLinearEquationSolverPreconditioner::Ilu) { +#ifdef STORM_HAVE_GMM_ILU gmm::bicgstab(*gmmxxA, x, b, *iluPreconditioner, iter); +#else + STORM_LOG_WARN("Preconditioner Ilu not available, using diagonal preconditioner instead."); + gmm::bicgstab(*gmmxxA, x, b, *diagonalPreconditioner, iter); +#endif } else if (preconditioner == GmmxxLinearEquationSolverPreconditioner::Diagonal) { gmm::bicgstab(*gmmxxA, x, b, *diagonalPreconditioner, iter); } else if (preconditioner == GmmxxLinearEquationSolverPreconditioner::None) { @@ -99,7 +108,12 @@ bool GmmxxLinearEquationSolver::internalSolveEquations(Environment co } } else if (method == GmmxxLinearEquationSolverMethod::Qmr) { if (preconditioner == GmmxxLinearEquationSolverPreconditioner::Ilu) { +#ifdef STORM_HAVE_GMM_ILU gmm::qmr(*gmmxxA, x, b, *iluPreconditioner, iter); +#else + STORM_LOG_WARN("Preconditioner Ilu not available, using diagonal preconditioner instead."); + gmm::qmr(*gmmxxA, x, b, *diagonalPreconditioner, iter); +#endif } else if (preconditioner == GmmxxLinearEquationSolverPreconditioner::Diagonal) { gmm::qmr(*gmmxxA, x, b, *diagonalPreconditioner, iter); } else if (preconditioner == GmmxxLinearEquationSolverPreconditioner::None) { @@ -107,7 +121,12 @@ bool GmmxxLinearEquationSolver::internalSolveEquations(Environment co } } else if (method == GmmxxLinearEquationSolverMethod::Gmres) { if (preconditioner == GmmxxLinearEquationSolverPreconditioner::Ilu) { +#ifdef STORM_HAVE_GMM_ILU gmm::gmres(*gmmxxA, x, b, *iluPreconditioner, env.solver().gmmxx().getRestartThreshold(), iter); +#else + STORM_LOG_WARN("Preconditioner Ilu not available, using diagonal preconditioner instead."); + gmm::gmres(*gmmxxA, x, b, *diagonalPreconditioner, env.solver().gmmxx().getRestartThreshold(), iter); +#endif } else if (preconditioner == GmmxxLinearEquationSolverPreconditioner::Diagonal) { gmm::gmres(*gmmxxA, x, b, *diagonalPreconditioner, env.solver().gmmxx().getRestartThreshold(), iter); } else if (preconditioner == GmmxxLinearEquationSolverPreconditioner::None) { @@ -151,7 +170,9 @@ LinearEquationSolverProblemFormat GmmxxLinearEquationSolver::getEquat template void GmmxxLinearEquationSolver::clearCache() const { #ifdef STORM_HAVE_GMM +#ifdef STORM_HAVE_GMM_ILU iluPreconditioner.reset(); +#endif diagonalPreconditioner.reset(); LinearEquationSolver::clearCache(); #else