moves-rwth · volkm · Mar 6, 2025 · Mar 6, 2025 · Mar 6, 2025 · Mar 28, 2025
diff --git a/.github/workflows/Dockerfile.archlinux b/.github/workflows/Dockerfile.archlinux
@@ -15,9 +15,11 @@ ARG build_type=Release
 ARG no_threads=1
 
 # Specify Storm configuration (ON/OFF)
+ARG cudd_support="ON"
 ARG gurobi_support="ON"
 ARG soplex_support="ON"
 ARG spot_support="ON"
+ARG sylvan_support="ON"
 ARG developer="OFF"
 ARG cln_exact="OFF"
 ARG cln_ratfunc="ON"
@@ -50,9 +52,11 @@ WORKDIR /opt/storm/build
 # Configure Storm
 RUN cmake .. -DCMAKE_BUILD_TYPE=$build_type \
              -DSTORM_PORTABLE=ON \
+             -DSTORM_USE_CUDD=$cudd_support \
              -DSTORM_USE_GUROBI=$gurobi_support \
              -DSTORM_USE_SOPLEX=$soplex_support \
              -DSTORM_USE_SPOT_SYSTEM=$spot_support \
+             -DSTORM_USE_SYLVAN=$sylvan_support \
              -DSTORM_DEVELOPER=$developer \
              -DSTORM_USE_CLN_EA=$cln_exact \
              -DSTORM_USE_CLN_RF=$cln_ratfunc \

diff --git a/.github/workflows/buildtest.yml b/.github/workflows/buildtest.yml
@@ -25,9 +25,11 @@ jobs:
           - {name: "GMP exact; GMP rational functions; All dependencies",
              baseImg: "storm-dependencies:latest-debug",
              buildType: "Debug",
+             Cudd: "ON",
              Gurobi: "ON",
              Soplex: "ON",
              Spot: "ON",
+             Sylvan: "ON",
              Developer: "ON",
              ClnExact: "OFF",
              ClnRatfunc: "OFF",
@@ -37,9 +39,11 @@ jobs:
           - {name: "CLN exact; GMP rational functions; All dependencies",
              baseImg: "storm-dependencies:latest-debug",
              buildType: "Debug",
+             Cudd: "ON",
              Gurobi: "ON",
              Soplex: "ON",
              Spot: "ON",
+             Sylvan: "ON",
              Developer: "ON",
              ClnExact: "ON",
              ClnRatfunc: "OFF",
@@ -49,9 +53,11 @@ jobs:
           - {name: "CLN exact; CLN rational functions; All dependencies",
              baseImg: "storm-dependencies:latest-debug",
              buildType: "Debug",
+             Cudd: "ON",
              Gurobi: "ON",
              Soplex: "ON",
              Spot: "ON",
+             Sylvan: "ON",
              Developer: "ON",
              ClnExact: "ON",
              ClnRatfunc: "ON",
@@ -61,9 +67,11 @@ jobs:
           - {name: "GMP exact; CLN rational functions; No dependencies",
              baseImg: "storm-dependencies:latest-debug",
              buildType: "Debug",
+             Cudd: "OFF",
              Gurobi: "OFF",
              Soplex: "OFF",
              Spot: "OFF",
+             Sylvan: "OFF",
              Developer: "ON",
              ClnExact: "OFF",
              ClnRatfunc: "ON",
@@ -73,9 +81,11 @@ jobs:
           - {name: "Minimal dependencies",
             baseImg: "storm-basesystem:minimal_dependencies",
             buildType: "Debug",
+             Cudd: "OFF",
              Gurobi: "OFF",
              Soplex: "OFF",
              Spot: "OFF",
+             Sylvan: "OFF",
              Developer: "ON",
              ClnExact: "OFF",
              ClnRatfunc: "ON",
@@ -90,9 +100,11 @@ jobs:
           docker build -t movesrwth/storm:ci . \
             --build-arg BASE_IMG=movesrwth/${{ matrix.config.baseImg }} \
             --build-arg build_type="${{ matrix.config.buildType }}" \
+            --build-arg cudd_support="${{ matrix.config.Cudd }}" \
             --build-arg gurobi_support="${{ matrix.config.Gurobi }}" \
             --build-arg soplex_support="${{ matrix.config.Soplex }}" \
             --build-arg spot_support="${{ matrix.config.Spot }}" \
+            --build-arg sylvan_support="${{ matrix.config.Sylvan }}" \
             --build-arg developer="${{ matrix.config.Developer }}" \
             --build-arg cln_exact="${{ matrix.config.ClnExact }}" \
             --build-arg cln_ratfunc="${{ matrix.config.ClnRatfunc }}" \
@@ -160,7 +172,7 @@ jobs:
             --build-arg cmake_args="${{ matrix.config.cmakeArgs }}" \
             --build-arg packages="${{ matrix.config.packages }}" \
             --build-arg no_threads=${NR_JOBS}
-            # Omitting arguments cln_exact, cln_ratfunc, all_sanitizers
+            # Omitting arguments cudd_support, sylvan_support, cln_exact, cln_ratfunc, all_sanitizers
       - name: Run Docker
         run: docker run -d -it --name ci movesrwth/storm:ci
 

diff --git a/.github/workflows/release_docker.yml b/.github/workflows/release_docker.yml
@@ -39,7 +39,7 @@ jobs:
             --build-arg developer="${{ matrix.buildType.Developer }}" \
             --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
+            # Omitting arguments cudd_support, gurobi_support, soplex_support, spot_support, sylvan_support, cln_exact, cln_ratfunc, all_sanitizers
       - name: Login to Docker Hub
         # Only login if using original repo
         if: github.repository_owner == 'moves-rwth'

diff --git a/CMakeLists.txt b/CMakeLists.txt
@@ -56,8 +56,10 @@ export_option(STORM_USE_CLN_EA)
 option(STORM_USE_CLN_RF "Sets whether CLN instead of GMP numbers should be used for rational functions." ON)
 export_option(STORM_USE_CLN_RF)
 option(BUILD_SHARED_LIBS "Build the Storm library dynamically" OFF)
+option(STORM_USE_CUDD "Sets whether CUDD should be used." ON)
 option(STORM_DEBUG_CUDD "Build CUDD in debug mode." OFF)
 MARK_AS_ADVANCED(STORM_DEBUG_CUDD)
+option(STORM_USE_SYLVAN "Sets whether Sylvan should be used." ON)
 option(STORM_DEBUG_SYLVAN "Build Sylvan in debug mode." OFF)
 MARK_AS_ADVANCED(STORM_DEBUG_SYLVAN)
 option(STORM_EXCLUDE_TESTS_FROM_ALL "If set, tests will not be compiled by default" OFF )

diff --git a/Dockerfile b/Dockerfile
@@ -20,9 +20,11 @@ ARG build_type=Release
 ARG no_threads=1
 
 # Specify Storm configuration (ON/OFF)
+ARG cudd_support="ON"
 ARG gurobi_support="ON"
 ARG soplex_support="ON"
 ARG spot_support="ON"
+ARG sylvan_support="ON"
 ARG developer="OFF"
 ARG cln_exact="OFF"
 ARG cln_ratfunc="ON"
@@ -47,9 +49,11 @@ WORKDIR /opt/storm/build
 # Configure Storm
 RUN cmake .. -DCMAKE_BUILD_TYPE=$build_type \
              -DSTORM_PORTABLE=ON \
+             -DSTORM_USE_CUDD=$cudd_support \
              -DSTORM_USE_GUROBI=$gurobi_support \
              -DSTORM_USE_SOPLEX=$soplex_support \
              -DSTORM_USE_SPOT_SYSTEM=$spot_support \
+             -DSTORM_USE_SYLVAN=$sylvan_support \
              -DSTORM_DEVELOPER=$developer \
              -DSTORM_USE_CLN_EA=$cln_exact \
              -DSTORM_USE_CLN_RF=$cln_ratfunc \

diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt
@@ -268,11 +268,17 @@ endif()
 
 #############################################################
 ##
-##	CUDD
+##	CUDD (optional)
 ##
 #############################################################
-include(${STORM_3RDPARTY_SOURCE_DIR}/include_cudd.cmake)
 
+if(STORM_USE_CUDD)
+    include(${STORM_3RDPARTY_SOURCE_DIR}/include_cudd.cmake)
+    set(STORM_HAVE_CUDD ON)
+else()
+    message (WARNING "Storm - Building without CUDD support.")
+    set(STORM_HAVE_CUDD OFF)
+endif()
 
 #############################################################
 ##
@@ -550,52 +556,58 @@ include(${STORM_3RDPARTY_SOURCE_DIR}/include_spot.cmake)
 
 #############################################################
 ##
-##	Sylvan
+##	Sylvan (optional)
 ##
 #############################################################
 
-if(STORM_SHIPPED_CARL)
-	set(sylvan_dep carl)
-else()
-	set(sylvan_dep lib_carl)
-endif()
+if(STORM_USE_SYLVAN)
+    if(STORM_SHIPPED_CARL)
+        set(sylvan_dep carl)
+    else()
+        set(sylvan_dep lib_carl)
+    endif()
 
-if (STORM_DEBUG_SYLVAN)
-	set(SYLVAN_BUILD_TYPE "Debug")
-	message(WARNING "Storm - Building Sylvan in DEBUG mode.")
+    if (STORM_DEBUG_SYLVAN)
+        set(SYLVAN_BUILD_TYPE "Debug")
+        message(WARNING "Storm - Building Sylvan in DEBUG mode.")
+    else()
+        set(SYLVAN_BUILD_TYPE "Release")
+    endif()
+
+    ExternalProject_Add(
+            sylvan
+            DOWNLOAD_COMMAND ""
+            PREFIX "sylvan"
+            SOURCE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/sylvan
+            CMAKE_ARGS -DPROJECT_NAME=storm -DCMAKE_C_COMPILER=${CMAKE_C_COMPILER} -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER} -DSYLVAN_BUILD_DOCS=OFF -DSYLVAN_BUILD_EXAMPLES=OFF -DSYLVAN_BUILD_TESTS=OFF -DCMAKE_BUILD_TYPE=${SYLVAN_BUILD_TYPE} -DCMAKE_POSITION_INDEPENDENT_CODE=ON -DSYLVAN_GMP=ON -DUSE_CARL=ON -Dcarl_DIR=${carl_DIR} -DBUILD_SHARED_LIBS=OFF
+            BINARY_DIR ${STORM_3RDPARTY_BINARY_DIR}/sylvan
+            BUILD_IN_SOURCE 0
+            INSTALL_COMMAND ""
+            INSTALL_DIR ${STORM_3RDPARTY_BINARY_DIR}/sylvan
+            LOG_CONFIGURE ON
+            LOG_BUILD ON
+            DEPENDS ${sylvan_dep}
+            BUILD_BYPRODUCTS ${STORM_3RDPARTY_BINARY_DIR}/sylvan/src/libsylvan${STATIC_EXT}
+            BUILD_ALWAYS 1
+    )
+    # BUILD ALWAYS ON due to: https://stackoverflow.com/questions/46708124/cmake-doesnt-rebuild-externalproject-on-changes
+
+    ExternalProject_Get_Property(sylvan source_dir)
+    ExternalProject_Get_Property(sylvan binary_dir)
+    set(sylvan_INCLUDE_DIR "${source_dir}/src")
+    set(sylvan_LIBRARY "${binary_dir}/src/libsylvan${STATIC_EXT}")
+    message(STATUS "Storm - Using shipped version of sylvan.")
+    message(STATUS "Storm - Linking with sylvan.")
+    add_imported_library(sylvan STATIC ${sylvan_LIBRARY} ${sylvan_INCLUDE_DIR})
+    add_dependencies(sylvan_STATIC sylvan)
+
+    list(APPEND STORM_DEP_TARGETS sylvan_STATIC)
+    set(STORM_HAVE_SYLVAN ON)
 else()
-	set(SYLVAN_BUILD_TYPE "Release")
+    message (WARNING "Storm - Building without Sylvan support.")
+    set(STORM_HAVE_SYLVAN OFF)
 endif()
 
-ExternalProject_Add(
-        sylvan
-        DOWNLOAD_COMMAND ""
-        PREFIX "sylvan"
-        SOURCE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/sylvan
-        CMAKE_ARGS -DPROJECT_NAME=storm -DCMAKE_C_COMPILER=${CMAKE_C_COMPILER} -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER} -DSYLVAN_BUILD_DOCS=OFF -DSYLVAN_BUILD_EXAMPLES=OFF -DSYLVAN_BUILD_TESTS=OFF -DCMAKE_BUILD_TYPE=${SYLVAN_BUILD_TYPE} -DCMAKE_POSITION_INDEPENDENT_CODE=ON -DSYLVAN_GMP=ON -DUSE_CARL=ON -Dcarl_DIR=${carl_DIR} -DBUILD_SHARED_LIBS=OFF
-        BINARY_DIR ${STORM_3RDPARTY_BINARY_DIR}/sylvan
-        BUILD_IN_SOURCE 0
-        INSTALL_COMMAND ""
-        INSTALL_DIR ${STORM_3RDPARTY_BINARY_DIR}/sylvan
-        LOG_CONFIGURE ON
-        LOG_BUILD ON
-        DEPENDS ${sylvan_dep}
-        BUILD_BYPRODUCTS ${STORM_3RDPARTY_BINARY_DIR}/sylvan/src/libsylvan${STATIC_EXT}
-        BUILD_ALWAYS 1
-)
-# BUILD ALWAYS ON due to: https://stackoverflow.com/questions/46708124/cmake-doesnt-rebuild-externalproject-on-changes
-
-ExternalProject_Get_Property(sylvan source_dir)
-ExternalProject_Get_Property(sylvan binary_dir)
-set(sylvan_INCLUDE_DIR "${source_dir}/src")
-set(sylvan_LIBRARY "${binary_dir}/src/libsylvan${STATIC_EXT}")
-message(STATUS "Storm - Using shipped version of sylvan.")
-message(STATUS "Storm - Linking with sylvan.")
-add_imported_library(sylvan STATIC ${sylvan_LIBRARY} ${sylvan_INCLUDE_DIR})
-add_dependencies(sylvan_STATIC sylvan)
-
-list(APPEND STORM_DEP_TARGETS sylvan_STATIC)
-
 #############################################################
 ##
 ##	Google Test gtest

diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h
@@ -1,41 +1,21 @@
 #pragma once
 
-#include "storm/api/storm.h"
+#include <type_traits>
 
 #include "storm-counterexamples/api/counterexamples.h"
 #include "storm-gamebased-ar/api/verification.h"
 #include "storm-parsers/api/storm-parsers.h"
 #include "storm-parsers/parser/ExpressionParser.h"
-
-#include "storm/io/file.h"
-#include "storm/utility/AutomaticSettings.h"
-#include "storm/utility/Engine.h"
-#include "storm/utility/NumberTraits.h"
-#include "storm/utility/SignalHandler.h"
-#include "storm/utility/macros.h"
-
-#include "storm/utility/Stopwatch.h"
-#include "storm/utility/initialize.h"
-
-#include <type_traits>
-
-#include "storm/storage/SymbolicModelDescription.h"
-#include "storm/storage/jani/Property.h"
-
+#include "storm/api/storm.h"
 #include "storm/builder/BuilderType.h"
-
-#include "storm/models/ModelBase.h"
-
 #include "storm/environment/Environment.h"
-
 #include "storm/exceptions/OptionParserException.h"
-
+#include "storm/io/file.h"
 #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
-
+#include "storm/models/ModelBase.h"
 #include "storm/models/sparse/StandardRewardModel.h"
 #include "storm/models/symbolic/MarkovAutomaton.h"
 #include "storm/models/symbolic/StandardRewardModel.h"
-
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/AbstractionSettings.h"
 #include "storm/settings/modules/BuildSettings.h"
@@ -48,10 +28,17 @@
 #include "storm/settings/modules/SylvanSettings.h"
 #include "storm/settings/modules/TransformationSettings.h"
 #include "storm/storage/Qvbs.h"
+#include "storm/storage/SymbolicModelDescription.h"
+#include "storm/storage/jani/Property.h"
 #include "storm/storage/jani/localeliminator/AutomaticAction.h"
 #include "storm/storage/jani/localeliminator/JaniLocalEliminator.h"
-
+#include "storm/utility/AutomaticSettings.h"
+#include "storm/utility/Engine.h"
+#include "storm/utility/NumberTraits.h"
+#include "storm/utility/SignalHandler.h"
 #include "storm/utility/Stopwatch.h"
+#include "storm/utility/initialize.h"
+#include "storm/utility/macros.h"
 
 namespace storm {
 namespace cli {
@@ -1430,26 +1417,41 @@ void processInputWithValueTypeAndDdlib(SymbolicInput const& input, ModelProcessi
 
 template<typename ValueType>
 void processInputWithValueType(SymbolicInput const& input, ModelProcessingInformation const& mpi) {
-    if (mpi.ddType == storm::dd::DdType::CUDD) {
-        STORM_LOG_ASSERT(mpi.verificationValueType == ModelProcessingInformation::ValueType::FinitePrecision &&
-                             mpi.buildValueType == ModelProcessingInformation::ValueType::FinitePrecision && (std::is_same<ValueType, double>::value),
-                         "Unexpected value type for Dd library cudd.");
-        processInputWithValueTypeAndDdlib<storm::dd::DdType::CUDD, double>(input, mpi);
-    } else {
-        STORM_LOG_ASSERT(mpi.ddType == storm::dd::DdType::Sylvan, "Unknown DD library.");
-        if (mpi.buildValueType == mpi.verificationValueType) {
-            processInputWithValueTypeAndDdlib<storm::dd::DdType::Sylvan, ValueType>(input, mpi);
-        } else {
-            // Right now, we only require (buildType == Exact and verificationType == FinitePrecision).
-            // We exclude all other combinations to safe a few template instantiations.
-            STORM_LOG_THROW((std::is_same<ValueType, double>::value) && mpi.buildValueType == ModelProcessingInformation::ValueType::Exact,
-                            storm::exceptions::InvalidArgumentException, "Unexpected combination of buildValueType and verificationValueType");
-#ifdef STORM_HAVE_CARL
-            processInputWithValueTypeAndDdlib<storm::dd::DdType::Sylvan, storm::RationalNumber, double>(input, mpi);
+    switch (mpi.ddType) {
+        case storm::dd::DdType::CUDD:
+#ifdef STORM_HAVE_CUDD
+            STORM_LOG_ASSERT(mpi.verificationValueType == ModelProcessingInformation::ValueType::FinitePrecision &&
+                                 mpi.buildValueType == ModelProcessingInformation::ValueType::FinitePrecision && (std::is_same<ValueType, double>::value),
+                             "Unexpected value type for Dd library CUDD.");
+            processInputWithValueTypeAndDdlib<storm::dd::DdType::CUDD, double>(input, mpi);
 #else
-            STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Unexpected buildValueType.");
+            STORM_LOG_THROW(
+                false, storm::exceptions::MissingLibraryException,
+                "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
+                "of Storm with CUDD support.");
 #endif
-        }
+            break;
+        case storm::dd::DdType::Sylvan:
+#ifdef STORM_HAVE_SYLVAN
+            if (mpi.buildValueType == mpi.verificationValueType) {
+                processInputWithValueTypeAndDdlib<storm::dd::DdType::Sylvan, ValueType>(input, mpi);
+            } else {
+                // Right now, we only require (buildType == Exact and verificationType == FinitePrecision).
+                // We exclude all other combinations to safe a few template instantiations.
+                STORM_LOG_THROW((std::is_same<ValueType, double>::value) && mpi.buildValueType == ModelProcessingInformation::ValueType::Exact,
+                                storm::exceptions::InvalidArgumentException, "Unexpected combination of buildValueType and verificationValueType");
+                processInputWithValueTypeAndDdlib<storm::dd::DdType::Sylvan, storm::RationalNumber, double>(input, mpi);
+            }
+#else
+            STORM_LOG_THROW(
+                false, storm::exceptions::MissingLibraryException,
+                "This version of Storm was compiled without support for Sylvan. Yet, a method was called that requires this support. Please choose a version "
+                "of Storm with Sylvan support.");
+#endif
+            break;
+        default:
+            STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected Dd Type.");
+            break;
     }
 }
 }  // namespace cli