diff --git a/.github/workflows/Dockerfile.archlinux b/.github/workflows/Dockerfile.archlinux index 9e6312e2f4..a242407bb2 100644 --- 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 index a979cb16ac..a6ff95ce50 100644 --- 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 index 18f1178f09..a88827153b 100644 --- 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 index 06d4c92780..26734af4a1 100644 --- 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 index b08afb16c3..c13f946473 100644 --- 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 index fade2ede96..9c835043ff 100644 --- 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 index 3175d241c2..10d4768f43 100644 --- 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 #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 - -#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 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::value), - "Unexpected value type for Dd library cudd."); - processInputWithValueTypeAndDdlib(input, mpi); - } else { - STORM_LOG_ASSERT(mpi.ddType == storm::dd::DdType::Sylvan, "Unknown DD library."); - if (mpi.buildValueType == mpi.verificationValueType) { - processInputWithValueTypeAndDdlib(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::value) && mpi.buildValueType == ModelProcessingInformation::ValueType::Exact, - storm::exceptions::InvalidArgumentException, "Unexpected combination of buildValueType and verificationValueType"); -#ifdef STORM_HAVE_CARL - processInputWithValueTypeAndDdlib(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::value), + "Unexpected value type for Dd library CUDD."); + processInputWithValueTypeAndDdlib(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(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::value) && mpi.buildValueType == ModelProcessingInformation::ValueType::Exact, + storm::exceptions::InvalidArgumentException, "Unexpected combination of buildValueType and verificationValueType"); + processInputWithValueTypeAndDdlib(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 diff --git a/src/storm-config.h.in b/src/storm-config.h.in index 5245fd709d..17c129c635 100644 --- a/src/storm-config.h.in +++ b/src/storm-config.h.in @@ -48,6 +48,12 @@ // Whether SoPlex is available and to be used #cmakedefine STORM_HAVE_SOPLEX +// Whether CUDD is available and to be used +#cmakedefine STORM_HAVE_CUDD + +// Whether Sylvan is available and to be used +#cmakedefine STORM_HAVE_SYLVAN + // Whether benchmarks from QVBS can be used as input #cmakedefine STORM_HAVE_QVBS diff --git a/src/storm-dft/adapters/SFTBDDPropertyFormulaAdapter.h b/src/storm-dft/adapters/SFTBDDPropertyFormulaAdapter.h index d2c8b6e5ba..3f9db9ffa4 100644 --- a/src/storm-dft/adapters/SFTBDDPropertyFormulaAdapter.h +++ b/src/storm-dft/adapters/SFTBDDPropertyFormulaAdapter.h @@ -1,7 +1,6 @@ #pragma once #include - #include #include #include @@ -21,7 +20,9 @@ namespace adapters { class SFTBDDPropertyFormulaAdapter { using ValueType = double; +#ifdef STORM_HAVE_SYLVAN using Bdd = sylvan::Bdd; +#endif using FormulaCPointer = std::shared_ptr; using StateFormulaCPointer = std::shared_ptr; using UnaryStateFormulaCPointer = std::shared_ptr; @@ -30,6 +31,7 @@ class SFTBDDPropertyFormulaAdapter { using FormulaVector = std::vector; public: +#ifdef STORM_HAVE_SYLVAN SFTBDDPropertyFormulaAdapter( std::shared_ptr> dft, FormulaVector const &formulas, storm::dft::utility::RelevantEvents relevantEvents = {}, std::shared_ptr sylvanBddManager = std::make_shared()) @@ -40,39 +42,73 @@ class SFTBDDPropertyFormulaAdapter { auto const transformator{std::make_shared>(dft, sylvanBddManager, relevantEvents)}; checker = std::make_shared(transformator); } +#else + SFTBDDPropertyFormulaAdapter( + std::shared_ptr> dft, FormulaVector const &formulas, storm::dft::utility::RelevantEvents relevantEvents = {}, + std::shared_ptr sylvanBddManager = std::make_shared()) { + 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 /** * \return The internal DFT */ - std::shared_ptr> getDFT() const noexcept { + std::shared_ptr> getDFT() const { +#ifdef STORM_HAVE_SYLVAN return checker->getDFT(); +#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 } /** * \return The internal sylvanBddManager */ - std::shared_ptr getSylvanBddManager() const noexcept { + std::shared_ptr getSylvanBddManager() const { +#ifdef STORM_HAVE_SYLVAN return checker->getSylvanBddManager(); +#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 } /** * \return The internal SftToBddTransformator */ - std::shared_ptr> getTransformator() const noexcept { + std::shared_ptr> getTransformator() const { +#ifdef STORM_HAVE_SYLVAN return checker->getTransformator(); +#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 } /** * \return The internal SFTBDDChecker */ - std::shared_ptr getSFTBDDChecker() const noexcept { + std::shared_ptr getSFTBDDChecker() const { +#ifdef STORM_HAVE_SYLVAN return checker; +#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 } /** * Calculate the properties specified by the formulas */ std::vector check(size_t const chunksize = 0) { +#ifdef STORM_HAVE_SYLVAN auto const bdds{formulasToBdd()}; std::map BDDToBdd{}; @@ -109,8 +145,14 @@ class SFTBDDPropertyFormulaAdapter { } return rval; +#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 } +#ifdef STORM_HAVE_SYLVAN /** * \return * The bdds representing the StatesFormulas of the given formulas @@ -126,6 +168,7 @@ class SFTBDDPropertyFormulaAdapter { } return rval; } +#endif // TODO: Move formulahandling into its own module /** @@ -133,6 +176,7 @@ class SFTBDDPropertyFormulaAdapter { * where op is in {<=, <, =} and phi is a state formula */ static void checkForm(FormulaVector const &formulas) { +#ifdef STORM_HAVE_SYLVAN for (auto const &formula : formulas) { if (formula->isProbabilityOperatorFormula()) { auto const probabilityOperator{std::static_pointer_cast(formula)}; @@ -167,6 +211,11 @@ class SFTBDDPropertyFormulaAdapter { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Only ProbabilityOperatorFormulas are supported."); } } +#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 } /** @@ -174,6 +223,7 @@ class SFTBDDPropertyFormulaAdapter { * The upper timebound of the given formula */ static double getTimebound(FormulaCPointer const &formula) { +#ifdef STORM_HAVE_SYLVAN auto const probabilityOperator{std::static_pointer_cast(formula)}; auto const subFormula{probabilityOperator->getSubformula().asSharedPointer()}; @@ -181,9 +231,15 @@ class SFTBDDPropertyFormulaAdapter { auto const boundedUntil{std::static_pointer_cast(subFormula)}; return boundedUntil->getUpperBound().evaluateAsDouble(); +#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 } private: +#ifdef STORM_HAVE_SYLVAN std::shared_ptr checker; FormulaVector formulas; @@ -319,6 +375,7 @@ class SFTBDDPropertyFormulaAdapter { Bdd atomicLabelFormulaToBdd(AtomicLabelFormulaCPointer const &formula) const { return getTransformator()->transformRelevantEvents().at(getAtomicLabelString(formula)); } +#endif }; } // namespace adapters diff --git a/src/storm-dft/api/storm-dft.cpp b/src/storm-dft/api/storm-dft.cpp index 02286c88c3..283d20b9fa 100644 --- a/src/storm-dft/api/storm-dft.cpp +++ b/src/storm-dft/api/storm-dft.cpp @@ -1,15 +1,15 @@ #include "storm-dft/api/storm-dft.h" -#include "storm-conv/api/storm-conv.h" -#include "storm-conv/settings/modules/JaniExportSettings.h" -#include "storm-dft/settings/modules/DftGspnSettings.h" -#include "storm-dft/settings/modules/FaultTreeSettings.h" - #include #include + +#include "storm-conv/api/storm-conv.h" +#include "storm-conv/settings/modules/JaniExportSettings.h" #include "storm-dft/adapters/SFTBDDPropertyFormulaAdapter.h" #include "storm-dft/modelchecker/DftModularizationChecker.h" #include "storm-dft/modelchecker/SFTBDDChecker.h" +#include "storm-dft/settings/modules/DftGspnSettings.h" +#include "storm-dft/settings/modules/FaultTreeSettings.h" #include "storm-dft/storage/DFT.h" #include "storm-dft/storage/DftJsonExporter.h" #include "storm-dft/storage/SylvanBddManager.h" @@ -25,6 +25,7 @@ void analyzeDFTBdd(std::shared_ptr> const& dft, bool const calculateProbability, bool const useModularisation, std::string const importanceMeasureName, std::vector const& timepoints, std::vector> const& properties, std::vector const& additionalRelevantEventNames, size_t const chunksize) { +#ifdef STORM_HAVE_SYLVAN if (calculateMttf) { if (mttfAlgorithmName == "proceeding") { std::cout << "The numerically approximated MTTF is " << storm::dft::utility::MTTFHelperProceeding(dft, mttfStepsize, mttfPrecision) << '\n'; @@ -159,6 +160,11 @@ void analyzeDFTBdd(std::shared_ptr> const& dft, } } }); +#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 } template<> @@ -167,7 +173,7 @@ void analyzeDFTBdd(std::shared_ptr const& timepoints, std::vector> const& properties, std::vector const& additionalRelevantEventNames, size_t const chunksize) { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "BDD analysis is not supportet for this data type."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "BDD analysis is not supported for this data type."); } template diff --git a/src/storm-dft/api/storm-dft.h b/src/storm-dft/api/storm-dft.h index e951f3a4d0..757e73ffb3 100644 --- a/src/storm-dft/api/storm-dft.h +++ b/src/storm-dft/api/storm-dft.h @@ -14,7 +14,6 @@ #include "storm-dft/utility/FDEPConflictFinder.h" #include "storm-dft/utility/FailureBoundFinder.h" #include "storm-dft/utility/RelevantEvents.h" - #include "storm-gspn/api/storm-gspn.h" namespace storm::dft { diff --git a/src/storm-dft/modelchecker/SFTBDDChecker.cpp b/src/storm-dft/modelchecker/SFTBDDChecker.cpp index 9912319ca8..59427fdf59 100644 --- a/src/storm-dft/modelchecker/SFTBDDChecker.cpp +++ b/src/storm-dft/modelchecker/SFTBDDChecker.cpp @@ -1,9 +1,9 @@ -#include +#include "storm-dft/modelchecker/SFTBDDChecker.h" +#include #include #include -#include "storm-dft/modelchecker/SFTBDDChecker.h" #include "storm-dft/transformations/SftToBddTransformator.h" #include "storm/adapters/eigen.h" @@ -11,10 +11,12 @@ namespace storm::dft { namespace modelchecker { using ValueType = SFTBDDChecker::ValueType; +#ifdef STORM_HAVE_SYLVAN using Bdd = SFTBDDChecker::Bdd; +#endif +#ifdef STORM_HAVE_SYLVAN namespace { - /** * \returns * The probability that the bdd is true @@ -246,14 +248,14 @@ Bdd SFTBDDChecker::getTopLevelElementBdd() { return transformator->transformTopLevel(); } -std::shared_ptr> SFTBDDChecker::getDFT() const noexcept { +std::shared_ptr> SFTBDDChecker::getDFT() const { return transformator->getDFT(); } -std::shared_ptr SFTBDDChecker::getSylvanBddManager() const noexcept { +std::shared_ptr SFTBDDChecker::getSylvanBddManager() const { return transformator->getSylvanBddManager(); } -std::shared_ptr> SFTBDDChecker::getTransformator() const noexcept { +std::shared_ptr> SFTBDDChecker::getTransformator() const { return transformator; } @@ -632,6 +634,170 @@ void SFTBDDChecker::recursiveMCS(Bdd const bdd, std::vector &buffer, s recursiveMCS(bdd.Else(), buffer, minimalCutSets); } } +#else +SFTBDDChecker::SFTBDDChecker(std::shared_ptr> dft, + std::shared_ptr sylvanBddManager) { + 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."); +} + +SFTBDDChecker::SFTBDDChecker(std::shared_ptr> transformator) { + 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."); +} + +std::shared_ptr> SFTBDDChecker::getDFT() const { + 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."); +} +std::shared_ptr SFTBDDChecker::getSylvanBddManager() const { + 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."); +} + +std::shared_ptr> SFTBDDChecker::getTransformator() const { + 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."); +} + +std::vector> SFTBDDChecker::getMinimalCutSets() { + 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."); +} + +std::vector> SFTBDDChecker::getMinimalCutSetsAsIndices() { + 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."); +} + +ValueType SFTBDDChecker::getBirnbaumFactorAtTimebound(std::string const &beName, ValueType timebound) { + 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."); +} + +std::vector SFTBDDChecker::getAllBirnbaumFactorsAtTimebound(ValueType timebound) { + 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."); +} + +std::vector SFTBDDChecker::getBirnbaumFactorsAtTimepoints(std::string const &beName, std::vector const &timepoints, size_t chunksize) { + 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."); +} + +std::vector> SFTBDDChecker::getAllBirnbaumFactorsAtTimepoints(std::vector const &timepoints, size_t chunksize) { + 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."); +} + +ValueType SFTBDDChecker::getCIFAtTimebound(std::string const &beName, ValueType timebound) { + 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."); +} + +std::vector SFTBDDChecker::getAllCIFsAtTimebound(ValueType timebound) { + 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."); +} + +std::vector SFTBDDChecker::getCIFsAtTimepoints(std::string const &beName, std::vector const &timepoints, size_t chunksize) { + 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."); +} + +std::vector> SFTBDDChecker::getAllCIFsAtTimepoints(std::vector const &timepoints, size_t chunksize) { + 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."); +} + +ValueType SFTBDDChecker::getDIFAtTimebound(std::string const &beName, ValueType timebound) { + 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."); +} + +std::vector SFTBDDChecker::getAllDIFsAtTimebound(ValueType timebound) { + 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."); +} + +std::vector SFTBDDChecker::getDIFsAtTimepoints(std::string const &beName, std::vector const &timepoints, size_t chunksize) { + 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."); +} + +std::vector> SFTBDDChecker::getAllDIFsAtTimepoints(std::vector const &timepoints, size_t chunksize) { + 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."); +} + +ValueType SFTBDDChecker::getRAWAtTimebound(std::string const &beName, ValueType timebound) { + 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."); +} + +std::vector SFTBDDChecker::getAllRAWsAtTimebound(ValueType timebound) { + 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."); +} + +std::vector SFTBDDChecker::getRAWsAtTimepoints(std::string const &beName, std::vector const &timepoints, size_t chunksize) { + 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."); +} + +std::vector> SFTBDDChecker::getAllRAWsAtTimepoints(std::vector const &timepoints, size_t chunksize) { + 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."); +} + +ValueType SFTBDDChecker::getRRWAtTimebound(std::string const &beName, ValueType timebound) { + 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."); +} + +std::vector SFTBDDChecker::getAllRRWsAtTimebound(ValueType timebound) { + 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."); +} + +std::vector SFTBDDChecker::getRRWsAtTimepoints(std::string const &beName, std::vector const &timepoints, size_t chunksize) { + 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."); +} + +std::vector> SFTBDDChecker::getAllRRWsAtTimepoints(std::vector const &timepoints, size_t chunksize) { + 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 } // namespace modelchecker } // namespace storm::dft diff --git a/src/storm-dft/modelchecker/SFTBDDChecker.h b/src/storm-dft/modelchecker/SFTBDDChecker.h index 161d62535c..ab0ece4ae8 100644 --- a/src/storm-dft/modelchecker/SFTBDDChecker.h +++ b/src/storm-dft/modelchecker/SFTBDDChecker.h @@ -22,7 +22,9 @@ namespace modelchecker { class SFTBDDChecker { public: using ValueType = double; +#ifdef STORM_HAVE_SYLVAN using Bdd = sylvan::Bdd; +#endif SFTBDDChecker(std::shared_ptr> dft, std::shared_ptr sylvanBddManager = std::make_shared()); @@ -32,17 +34,17 @@ class SFTBDDChecker { /** * \return The internal DFT */ - std::shared_ptr> getDFT() const noexcept; + std::shared_ptr> getDFT() const; /** * \return The internal sylvanBddManager */ - std::shared_ptr getSylvanBddManager() const noexcept; + std::shared_ptr getSylvanBddManager() const; /** * \return The internal SftToBddTransformator */ - std::shared_ptr> getTransformator() const noexcept; + std::shared_ptr> getTransformator() const; /** * Exports the Bdd that represents the top level event to a file @@ -52,7 +54,13 @@ class SFTBDDChecker { * The name of the file the dot graph is written to */ void exportBddToDot(std::string const &filename) { +#ifdef STORM_HAVE_SYLVAN getSylvanBddManager()->exportBddToDot(getTopLevelElementBdd(), filename); +#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 } /** @@ -75,9 +83,16 @@ class SFTBDDChecker { * The Probability that the top level event fails. */ ValueType getProbabilityAtTimebound(ValueType timebound) { +#ifdef STORM_HAVE_SYLVAN return getProbabilityAtTimebound(getTopLevelElementBdd(), timebound); +#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 } +#ifdef STORM_HAVE_SYLVAN /** * \return * The Probabilities that the given Event fails at the given timebound. @@ -87,6 +102,7 @@ class SFTBDDChecker { * Must be from a call to some function of *this. */ ValueType getProbabilityAtTimebound(Bdd bdd, ValueType timebound) const; +#endif /** * \return @@ -100,9 +116,16 @@ class SFTBDDChecker { * A value of 0 represents to calculate the whole array at once. */ std::vector getProbabilitiesAtTimepoints(std::vector const &timepoints, size_t const chunksize = 0) { +#ifdef STORM_HAVE_SYLVAN return getProbabilitiesAtTimepoints(getTopLevelElementBdd(), timepoints, chunksize); +#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 } +#ifdef STORM_HAVE_SYLVAN /** * \return * The Probabilities that the given Event fails at the given timepoints. @@ -119,6 +142,7 @@ class SFTBDDChecker { * A value of 0 represents to calculate the whole array at once. */ std::vector getProbabilitiesAtTimepoints(Bdd bdd, std::vector const &timepoints, size_t chunksize = 0) const; +#endif /** * \return @@ -341,6 +365,7 @@ class SFTBDDChecker { std::vector> getAllRRWsAtTimepoints(std::vector const &timepoints, size_t chunksize = 0); private: +#ifdef STORM_HAVE_SYLVAN /** * Recursively traverses the given BDD and returns the minimalCutSets. * @@ -380,6 +405,7 @@ class SFTBDDChecker { Bdd getTopLevelElementBdd(); std::shared_ptr> transformator; +#endif }; } // namespace modelchecker diff --git a/src/storm-dft/storage/SylvanBddManager.h b/src/storm-dft/storage/SylvanBddManager.h index ae1231abaa..ef2ec66194 100644 --- a/src/storm-dft/storage/SylvanBddManager.h +++ b/src/storm-dft/storage/SylvanBddManager.h @@ -41,6 +41,7 @@ class SylvanBddManager { */ ~SylvanBddManager() = default; +#ifdef STORM_HAVE_SYLVAN /*! * All code that manipulates DDs shall be called through this function. * This is generally needed to set-up the correct context. @@ -164,13 +165,40 @@ class SylvanBddManager { storm::io::closeFile(filestream); } } +#else + void execute(std::function const &f) const { + 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."); + } + + uint32_t createVariable(std::string const name) { + 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."); + } + + uint32_t getIndex(std::string const name) const { + 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."); + } + + std::string getName(uint32_t const index) const { + 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 private: +#ifdef STORM_HAVE_SYLVAN storm::dd::InternalDdManager internalManager{}; uint32_t nextFreeVariableIndex{0}; std::map nameToIndex{}; std::map indexToName{}; +#endif }; } // namespace storage diff --git a/src/storm-dft/transformations/SftToBddTransformator.h b/src/storm-dft/transformations/SftToBddTransformator.h index 40fef853ff..b8b08a8efa 100644 --- a/src/storm-dft/transformations/SftToBddTransformator.h +++ b/src/storm-dft/transformations/SftToBddTransformator.h @@ -18,8 +18,11 @@ namespace transformations { template class SftToBddTransformator { public: +#ifdef STORM_HAVE_SYLVAN using Bdd = sylvan::Bdd; +#endif +#ifdef STORM_HAVE_SYLVAN SftToBddTransformator(std::shared_ptr> dft, std::shared_ptr sylvanBddManager = std::make_shared(), storm::dft::utility::RelevantEvents relevantEvents = {}) @@ -96,8 +99,36 @@ class SftToBddTransformator { std::shared_ptr getSylvanBddManager() const noexcept { return sylvanBddManager; } +#else + SftToBddTransformator(std::shared_ptr> dft, + std::shared_ptr sylvanBddManager = std::make_shared(), + storm::dft::utility::RelevantEvents relevantEvents = {}) { + 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."); + } + + std::vector const& getDdVariables() const noexcept { + 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."); + } + + std::shared_ptr> getDFT() const noexcept { + 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."); + } + + std::shared_ptr getSylvanBddManager() const noexcept { + 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 private: +#ifdef STORM_HAVE_SYLVAN std::map relevantEventBdds{}; std::vector variables{}; std::shared_ptr> dft; @@ -222,6 +253,7 @@ class SftToBddTransformator { Bdd translate(std::shared_ptr const> const basicElement) { return sylvanBddManager->getPositiveLiteral(basicElement->name()); } +#endif }; } // namespace transformations diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp index 7277670caf..0df330b502 100644 --- a/src/storm-pomdp-cli/storm-pomdp.cpp +++ b/src/storm-pomdp-cli/storm-pomdp.cpp @@ -1,18 +1,12 @@ -#include "storm/utility/initialize.h" +#include +#include "storm-cli-utilities/cli.h" +#include "storm-cli-utilities/model-handling.h" +#include "storm-pomdp-cli/settings/PomdpSettings.h" #include "storm-pomdp-cli/settings/modules/BeliefExplorationSettings.h" #include "storm-pomdp-cli/settings/modules/POMDPSettings.h" #include "storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.h" #include "storm-pomdp-cli/settings/modules/ToParametricSettings.h" -#include "storm/settings/modules/DebugSettings.h" -#include "storm/settings/modules/GeneralSettings.h" - -#include "storm-pomdp-cli/settings/PomdpSettings.h" -#include "storm/analysis/GraphConditions.h" - -#include "storm-cli-utilities/cli.h" -#include "storm-cli-utilities/model-handling.h" - #include "storm-pomdp/analysis/FormulaInformation.h" #include "storm-pomdp/analysis/IterativePolicySearch.h" #include "storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.h" @@ -27,16 +21,17 @@ #include "storm-pomdp/transformer/KnownProbabilityTransformer.h" #include "storm-pomdp/transformer/MakePOMDPCanonic.h" #include "storm-pomdp/transformer/PomdpMemoryUnfolder.h" +#include "storm/analysis/GraphConditions.h" #include "storm/api/storm.h" +#include "storm/exceptions/NotSupportedException.h" +#include "storm/exceptions/UnexpectedException.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "storm/settings/modules/DebugSettings.h" +#include "storm/settings/modules/GeneralSettings.h" #include "storm/utility/NumberTraits.h" #include "storm/utility/SignalHandler.h" #include "storm/utility/Stopwatch.h" - -#include "storm/exceptions/NotSupportedException.h" -#include "storm/exceptions/UnexpectedException.h" - -#include +#include "storm/utility/initialize.h" namespace storm { namespace pomdp { @@ -461,10 +456,24 @@ void processOptions() { std::tie(symbolicInput, mpi) = storm::cli::preprocessSymbolicInput(symbolicInput); switch (mpi.ddType) { case storm::dd::DdType::CUDD: +#ifdef STORM_HAVE_CUDD processOptionsWithDdLib(symbolicInput, mpi); +#else + 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 processOptionsWithDdLib(symbolicInput, 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."); diff --git a/src/storm-pomdp/analysis/QualitativeAnalysis.cpp b/src/storm-pomdp/analysis/QualitativeAnalysis.cpp deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/src/storm-pomdp/builder/BeliefMdpExplorer.cpp b/src/storm-pomdp/builder/BeliefMdpExplorer.cpp index 8c4b8cc4c7..b3347aed74 100644 --- a/src/storm-pomdp/builder/BeliefMdpExplorer.cpp +++ b/src/storm-pomdp/builder/BeliefMdpExplorer.cpp @@ -889,7 +889,6 @@ typename BeliefMdpExplorer::ValueType BeliefMdpExplo STORM_LOG_ASSERT(!pomdpValueBounds.lower.empty(), "Requested lower value bounds but none were available."); STORM_LOG_ASSERT(pomdpValueBounds.lower.size() > schedulerId, "Requested lower value bound for scheduler with ID " << schedulerId << " not available."); return beliefManager->getWeightedSum(beliefId, pomdpValueBounds.lower[schedulerId]); - ; } template diff --git a/src/storm-pomdp/modelchecker/BeliefExplorationPomdpModelChecker.cpp b/src/storm-pomdp/modelchecker/BeliefExplorationPomdpModelChecker.cpp index e6fe9d0de9..a5632df2d7 100644 --- a/src/storm-pomdp/modelchecker/BeliefExplorationPomdpModelChecker.cpp +++ b/src/storm-pomdp/modelchecker/BeliefExplorationPomdpModelChecker.cpp @@ -726,7 +726,9 @@ void BeliefExplorationPomdpModelChecker::UnfoldingControl::Pause && - !storm::utility::resources::isTerminate()); + !storm::utility::resources::isTerminate()) { + // Intentionally left empty + } } STORM_LOG_INFO("\tInteractive Unfolding terminated.\n"); } diff --git a/src/storm/adapters/AddExpressionAdapter.cpp b/src/storm/adapters/AddExpressionAdapter.cpp index 84e09e1d1b..58d14fe73f 100644 --- a/src/storm/adapters/AddExpressionAdapter.cpp +++ b/src/storm/adapters/AddExpressionAdapter.cpp @@ -1,17 +1,14 @@ #include "storm/adapters/AddExpressionAdapter.h" +#include "storm-config.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/exceptions/ExpressionEvaluationException.h" #include "storm/exceptions/InvalidArgumentException.h" -#include "storm/utility/macros.h" - #include "storm/storage/dd/Add.h" #include "storm/storage/dd/Bdd.h" #include "storm/storage/dd/DdManager.h" - -#include "storm-config.h" -#include "storm/adapters/RationalFunctionAdapter.h" - #include "storm/utility/constants.h" +#include "storm/utility/macros.h" namespace storm { namespace adapters { @@ -227,10 +224,7 @@ boost::any AddExpressionAdapter::visit(storm::expressions::Rati // Explicitly instantiate the symbolic expression adapter template class AddExpressionAdapter; template class AddExpressionAdapter; - -#ifdef STORM_HAVE_CARL template class AddExpressionAdapter; template class AddExpressionAdapter; -#endif } // namespace adapters } // namespace storm diff --git a/src/storm/adapters/sylvan.cpp b/src/storm/adapters/sylvan.cpp index d84b39ee46..5c2a58d3fc 100644 --- a/src/storm/adapters/sylvan.cpp +++ b/src/storm/adapters/sylvan.cpp @@ -1,5 +1,6 @@ #include "storm/adapters/sylvan.h" +#ifdef STORM_HAVE_SYLVAN namespace storm { namespace dd { @@ -13,3 +14,4 @@ bool sylvan_mtbdd_matches_variable_index(MTBDD node, uint64_t variableIndex, int } // namespace dd } // namespace storm +#endif diff --git a/src/storm/adapters/sylvan.h b/src/storm/adapters/sylvan.h index 83f6a9d5de..a34e880596 100644 --- a/src/storm/adapters/sylvan.h +++ b/src/storm/adapters/sylvan.h @@ -1,5 +1,8 @@ #pragma once +#include "storm-config.h" + +#ifdef STORM_HAVE_SYLVAN #pragma clang diagnostic push #pragma clang diagnostic ignored "-Wextra-semi" #pragma clang diagnostic ignored "-Wzero-length-array" @@ -47,3 +50,5 @@ bool sylvan_mtbdd_matches_variable_index(MTBDD node, uint64_t variableIndex, int #pragma GCC diagnostic pop #pragma clang diagnostic pop + +#endif \ No newline at end of file diff --git a/src/storm/api/transformation.h b/src/storm/api/transformation.h index 147e93fa0e..66be1aad2d 100644 --- a/src/storm/api/transformation.h +++ b/src/storm/api/transformation.h @@ -55,7 +55,6 @@ transformContinuousToDiscreteTimeSparseModel(std::shared_ptrgetType() << " to a discrete time model is not supported"); } return std::make_pair(nullptr, newFormulas); - ; } /*! @@ -87,7 +86,6 @@ transformContinuousToDiscreteTimeSparseModel(storm::models::sparse::Model diff --git a/src/storm/automata/LTL2DeterministicAutomaton.cpp b/src/storm/automata/LTL2DeterministicAutomaton.cpp index b21b2f6f1c..71bb1299ba 100644 --- a/src/storm/automata/LTL2DeterministicAutomaton.cpp +++ b/src/storm/automata/LTL2DeterministicAutomaton.cpp @@ -79,7 +79,9 @@ std::shared_ptr LTL2DeterministicAutomaton::ltl2daExtern int status; // wait for completion - while (wait(&status) != pid); + while (wait(&status) != pid) { + // Intentionally left emtpty + } int rv; if (WIFEXITED(status)) { diff --git a/src/storm/exceptions/MissingLibraryException.h b/src/storm/exceptions/MissingLibraryException.h new file mode 100644 index 0000000000..19b09105a8 --- /dev/null +++ b/src/storm/exceptions/MissingLibraryException.h @@ -0,0 +1,12 @@ +#pragma once + +#include "storm/exceptions/BaseException.h" +#include "storm/exceptions/ExceptionMacros.h" + +namespace storm { +namespace exceptions { + +STORM_NEW_EXCEPTION(MissingLibraryException) + +} // namespace exceptions +} // namespace storm diff --git a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp index e996985a72..86bdad20ed 100644 --- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -53,7 +53,6 @@ std::unique_ptr SparseCtmcCslModelChecker::com std::unique_ptr leftResultPointer = this->check(env, pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(env, pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); - ; ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); STORM_LOG_THROW(pathFormula.getTimeBoundReference().isTimeBound(), storm::exceptions::NotImplementedException, @@ -251,7 +250,6 @@ std::vector SparseCtmcCslModelChecker leftResultPointer = this->check(env, pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(env, pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); - ; ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); std::vector result = storm::modelchecker::helper::SparseCtmcCslHelper::computeAllTransientProbabilities( diff --git a/src/storm/modelchecker/csl/helper/SymbolicCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/SymbolicCtmcCslHelper.cpp deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/src/storm/modelchecker/csl/helper/SymbolicCtmcCslHelper.h b/src/storm/modelchecker/csl/helper/SymbolicCtmcCslHelper.h deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.cpp b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.cpp index 535f534b4a..0346b41e4f 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.cpp +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.cpp @@ -570,7 +570,6 @@ void DeterministicSchedsObjectiveHelper::computeLowerUpperBounds(Envi ValueType rewardValueForPosInfCase; if (getInfinityCase() == InfinityCase::HasPositiveInfinite) { rewardValueForPosInfCase = getThreshold(); - ; // We need to substract a lower bound for the value at the initial state std::vector rewards2Negative; rewards2Negative.reserve(rewards2.size()); diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/CostLimitClosure.cpp b/src/storm/modelchecker/prctl/helper/rewardbounded/CostLimitClosure.cpp index 0d2bc65df3..0a7d3e73ab 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/CostLimitClosure.cpp +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/CostLimitClosure.cpp @@ -178,7 +178,6 @@ bool CostLimitClosure::unionFull(CostLimitClosure const& first, CostLimitClosure } } return solver->check() == storm::solver::SmtSolver::CheckResult::Unsat; - ; } } // namespace rewardbounded } // namespace helper diff --git a/src/storm/modelchecker/results/SymbolicQualitativeCheckResult.cpp b/src/storm/modelchecker/results/SymbolicQualitativeCheckResult.cpp index f8ec271b7a..5a0dd7017e 100644 --- a/src/storm/modelchecker/results/SymbolicQualitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/SymbolicQualitativeCheckResult.cpp @@ -118,7 +118,6 @@ void SymbolicQualitativeCheckResult::filter(QualitativeCheckResult const& STORM_LOG_THROW(filter.isSymbolicQualitativeCheckResult(), storm::exceptions::InvalidOperationException, "Cannot filter symbolic check result with non-symbolic filter."); this->states &= filter.asSymbolicQualitativeCheckResult().getTruthValuesVector(); - ; this->truthValues &= filter.asSymbolicQualitativeCheckResult().getTruthValuesVector(); this->states &= filter.asSymbolicQualitativeCheckResult().getTruthValuesVector(); } diff --git a/src/storm/settings/modules/CoreSettings.cpp b/src/storm/settings/modules/CoreSettings.cpp index 163af134a7..073d215a8e 100644 --- a/src/storm/settings/modules/CoreSettings.cpp +++ b/src/storm/settings/modules/CoreSettings.cpp @@ -68,13 +68,26 @@ CoreSettings::CoreSettings() : ModuleSettings(moduleName), engine(storm::utility .build()) .build()); - std::vector ddLibraries = {"cudd", "sylvan"}; - this->addOption(storm::settings::OptionBuilder(moduleName, ddLibraryOptionName, false, "Sets which library is preferred for decision-diagram operations.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the library to prefer.") - .addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(ddLibraries)) - .setDefaultValueString("sylvan") - .build()) - .build()); + // Initialize options for DD libraries + std::vector ddLibraries; + std::string ddDefault = ""; +#ifdef STORM_HAVE_CUDD + ddLibraries.push_back("cudd"); + ddDefault = "cudd"; +#endif +#ifdef STORM_HAVE_SYLVAN + ddLibraries.push_back("sylvan"); + ddDefault = "sylvan"; // Overwrite previous default and give Sylvan priority +#endif + if (!ddLibraries.empty()) { + this->addOption( + storm::settings::OptionBuilder(moduleName, ddLibraryOptionName, false, "Sets which library is preferred for decision-diagram operations.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the library to prefer.") + .addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(ddLibraries)) + .setDefaultValueString(ddDefault) + .build()) + .build()); + } std::vector lpSolvers = {"gurobi", "glpk", "z3", "soplex"}; this->addOption(storm::settings::OptionBuilder(moduleName, lpSolverOptionName, false, "Sets which LP solver is preferred.") diff --git a/src/storm/storage/dd/Add.cpp b/src/storm/storage/dd/Add.cpp index 7b4f44580c..635dfcb4ea 100644 --- a/src/storm/storage/dd/Add.cpp +++ b/src/storm/storage/dd/Add.cpp @@ -1230,7 +1230,6 @@ template class Add; template std::ostream& operator<<(std::ostream& out, Add const& add); template class Add; -#ifdef STORM_HAVE_CARL template class Add; template std::ostream& operator<<(std::ostream& out, Add const& add); @@ -1247,6 +1246,5 @@ template Add Add Add::toValueType() const; template Add Add::toValueType() const; template Add Add::toValueType() const; -#endif } // namespace dd } // namespace storm diff --git a/src/storm/storage/dd/Add.h b/src/storm/storage/dd/Add.h index a1719d559f..a0e65bc8f6 100644 --- a/src/storm/storage/dd/Add.h +++ b/src/storm/storage/dd/Add.h @@ -1,21 +1,20 @@ -#ifndef STORM_STORAGE_DD_ADD_H_ -#define STORM_STORAGE_DD_ADD_H_ +#pragma once #include #include +#include "storm-config.h" +#include "storm/storage/SparseMatrix.h" #include "storm/storage/dd/Dd.h" #include "storm/storage/dd/DdType.h" +#include "storm/storage/dd/InternalAdd.h" +#include "storm/storage/dd/InternalDdManager.h" #include "storm/storage/dd/Odd.h" - +#include "storm/storage/dd/cudd/CuddAddIterator.h" #include "storm/storage/dd/cudd/InternalCuddAdd.h" #include "storm/storage/dd/sylvan/InternalSylvanAdd.h" - -#include "storm/storage/dd/cudd/CuddAddIterator.h" #include "storm/storage/dd/sylvan/SylvanAddIterator.h" -#include "storm-config.h" - namespace storm { namespace dd { template @@ -829,5 +828,3 @@ class Add : public Dd { }; } // namespace dd } // namespace storm - -#endif /* STORM_STORAGE_DD_ADD_H_ */ diff --git a/src/storm/storage/dd/Bdd.cpp b/src/storm/storage/dd/Bdd.cpp index f84a0f3ac5..5d94de7b1a 100644 --- a/src/storm/storage/dd/Bdd.cpp +++ b/src/storm/storage/dd/Bdd.cpp @@ -608,10 +608,8 @@ template std::vector Bdd::filterExplicitVector(Odd template Add Bdd::ite(Add const& thenAdd, Add const& elseAdd) const; template Add Bdd::ite(Add const& thenAdd, Add const& elseAdd) const; -#ifdef STORM_HAVE_CARL template Add Bdd::ite(Add const& thenAdd, Add const& elseAdd) const; -#endif template class Bdd; @@ -619,7 +617,6 @@ template Bdd Bdd::fromVector(DdManager const& metaVariables, storm::logic::ComparisonType comparisonType, double value); -#ifdef STORM_HAVE_CARL template Bdd Bdd::fromVector(DdManager const& ddManager, std::vector const& explicitValues, storm::dd::Odd const& odd, std::set const& metaVariables, @@ -628,34 +625,27 @@ template Bdd Bdd::fromVector(DdManager const& explicitValues, storm::dd::Odd const& odd, std::set const& metaVariables, storm::logic::ComparisonType comparisonType, storm::RationalFunction value); -#endif template Add Bdd::toAdd() const; template Add Bdd::toAdd() const; -#ifdef STORM_HAVE_CARL template Add Bdd::toAdd() const; template Add Bdd::toAdd() const; -#endif template std::vector Bdd::filterExplicitVector(Odd const& odd, std::vector const& values) const; template std::vector Bdd::filterExplicitVector(Odd const& odd, std::vector const& values) const; -#ifdef STORM_HAVE_CARL template std::vector Bdd::filterExplicitVector(Odd const& odd, std::vector const& values) const; template std::vector Bdd::filterExplicitVector(Odd const& odd, std::vector const& values) const; -#endif template Add Bdd::ite(Add const& thenAdd, Add const& elseAdd) const; template Add Bdd::ite(Add const& thenAdd, Add const& elseAdd) const; -#ifdef STORM_HAVE_CARL template Add Bdd::ite(Add const& thenAdd, Add const& elseAdd) const; template Add Bdd::ite(Add const& thenAdd, Add const& elseAdd) const; -#endif } // namespace dd } // namespace storm diff --git a/src/storm/storage/dd/Bdd.h b/src/storm/storage/dd/Bdd.h index a221e2bbe0..df2ebc45b9 100644 --- a/src/storm/storage/dd/Bdd.h +++ b/src/storm/storage/dd/Bdd.h @@ -1,14 +1,14 @@ -#ifndef STORM_STORAGE_DD_BDD_H_ -#define STORM_STORAGE_DD_BDD_H_ +#pragma once #include +#include "storm/storage/BitVector.h" +#include "storm/storage/PairHash.h" #include "storm/storage/dd/Dd.h" #include "storm/storage/dd/DdType.h" - -#include "storm/storage/PairHash.h" #include "storm/storage/dd/InternalBdd.h" #include "storm/storage/dd/cudd/InternalCuddBdd.h" +#include "storm/storage/dd/sylvan/InternalSylvanBdd.h" namespace storm { namespace logic { @@ -451,5 +451,3 @@ struct hash> { } }; } // namespace std - -#endif /* STORM_STORAGE_DD_BDD_H_ */ diff --git a/src/storm/storage/dd/DdManager.cpp b/src/storm/storage/dd/DdManager.cpp index 2ec39ad340..9020b29a3c 100644 --- a/src/storm/storage/dd/DdManager.cpp +++ b/src/storm/storage/dd/DdManager.cpp @@ -1,19 +1,16 @@ #include "storm/storage/dd/DdManager.h" -#include "storm/storage/expressions/ExpressionManager.h" +#include +#include +#include "storm-config.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/exceptions/InvalidArgumentException.h" -#include "storm/utility/constants.h" -#include "storm/utility/macros.h" - #include "storm/exceptions/InvalidOperationException.h" #include "storm/exceptions/NotSupportedException.h" - -#include "storm-config.h" -#include "storm/adapters/RationalFunctionAdapter.h" - -#include -#include +#include "storm/storage/expressions/ExpressionManager.h" +#include "storm/utility/constants.h" +#include "storm/utility/macros.h" namespace storm { namespace dd { @@ -523,27 +520,18 @@ template class DdManager; template Add DdManager::getAddZero() const; template Add DdManager::getAddZero() const; - -#ifdef STORM_HAVE_CARL template Add DdManager::getAddZero() const; -#endif template Add DdManager::getAddOne() const; template Add DdManager::getAddOne() const; - -#ifdef STORM_HAVE_CARL template Add DdManager::getAddOne() const; -#endif template Add DdManager::getInfinity() const; template Add DdManager::getInfinity() const; template Add DdManager::getConstant(double const& value) const; template Add DdManager::getConstant(uint_fast64_t const& value) const; - -#ifdef STORM_HAVE_CARL template Add DdManager::getConstant(storm::RationalNumber const& value) const; -#endif template Add DdManager::getIdentity(storm::expressions::Variable const& variable) const; template Add DdManager::getIdentity(storm::expressions::Variable const& variable) const; @@ -552,44 +540,32 @@ template class DdManager; template Add DdManager::getAddZero() const; template Add DdManager::getAddZero() const; -#ifdef STORM_HAVE_CARL template Add DdManager::getAddZero() const; template Add DdManager::getAddZero() const; -#endif template Add DdManager::getAddUndefined() const; template Add DdManager::getAddUndefined() const; -#ifdef STORM_HAVE_CARL template Add DdManager::getAddUndefined() const; template Add DdManager::getAddUndefined() const; -#endif template Add DdManager::getAddOne() const; template Add DdManager::getAddOne() const; -#ifdef STORM_HAVE_CARL template Add DdManager::getAddOne() const; template Add DdManager::getAddOne() const; -#endif template Add DdManager::getInfinity() const; template Add DdManager::getInfinity() const; -#ifdef STORM_HAVE_CARL template Add DdManager::getInfinity() const; template Add DdManager::getInfinity() const; -#endif template Add DdManager::getConstant(double const& value) const; template Add DdManager::getConstant(uint_fast64_t const& value) const; -#ifdef STORM_HAVE_CARL template Add DdManager::getConstant(storm::RationalNumber const& value) const; template Add DdManager::getConstant(storm::RationalFunction const& value) const; -#endif template Add DdManager::getIdentity(storm::expressions::Variable const& variable) const; template Add DdManager::getIdentity(storm::expressions::Variable const& variable) const; -#ifdef STORM_HAVE_CARL template Add DdManager::getIdentity(storm::expressions::Variable const& variable) const; template Add DdManager::getIdentity(storm::expressions::Variable const& variable) const; -#endif } // namespace dd } // namespace storm diff --git a/src/storm/storage/dd/DdManager.h b/src/storm/storage/dd/DdManager.h index 107233a41e..4201aede8c 100644 --- a/src/storm/storage/dd/DdManager.h +++ b/src/storm/storage/dd/DdManager.h @@ -1,22 +1,21 @@ -#ifndef STORM_STORAGE_DD_DDMANAGER_H_ -#define STORM_STORAGE_DD_DDMANAGER_H_ +#pragma once #include #include #include #include +#include "storm-config.h" #include "storm/storage/dd/Add.h" #include "storm/storage/dd/AddIterator.h" #include "storm/storage/dd/Bdd.h" #include "storm/storage/dd/DdMetaVariable.h" #include "storm/storage/dd/DdType.h" +#include "storm/storage/dd/InternalDdManager.h" #include "storm/storage/dd/MetaVariablePosition.h" - -#include "storm/storage/expressions/Variable.h" - #include "storm/storage/dd/cudd/InternalCuddDdManager.h" #include "storm/storage/dd/sylvan/InternalSylvanDdManager.h" +#include "storm/storage/expressions/Variable.h" namespace storm { namespace dd { @@ -413,5 +412,3 @@ class DdManager : public std::enable_shared_from_this> { }; } // namespace dd } // namespace storm - -#endif /* STORM_STORAGE_DD_DDMANAGER_H_ */ diff --git a/src/storm/storage/dd/DdType.h b/src/storm/storage/dd/DdType.h index 0b607d9a77..6bd8410871 100644 --- a/src/storm/storage/dd/DdType.h +++ b/src/storm/storage/dd/DdType.h @@ -1,10 +1,8 @@ -#ifndef STORM_STORAGE_DD_DDTYPE_H_ -#define STORM_STORAGE_DD_DDTYPE_H_ +#pragma once namespace storm { namespace dd { enum class DdType { CUDD, Sylvan }; -} -} // namespace storm -#endif /* STORM_STORAGE_DD_DDTYPE_H_ */ +} // namespace dd +} // namespace storm diff --git a/src/storm/storage/dd/InternalAdd.h b/src/storm/storage/dd/InternalAdd.h index 1a988621ff..021b2aa0d3 100644 --- a/src/storm/storage/dd/InternalAdd.h +++ b/src/storm/storage/dd/InternalAdd.h @@ -1,5 +1,4 @@ -#ifndef STORM_STORAGE_DD_INTERNALADD_H_ -#define STORM_STORAGE_DD_INTERNALADD_H_ +#pragma once #include "storm/storage/dd/DdType.h" @@ -9,5 +8,3 @@ template class InternalAdd; } } // namespace storm - -#endif /* STORM_STORAGE_DD_INTERNALADD_H_ */ diff --git a/src/storm/storage/dd/InternalDdManager.h b/src/storm/storage/dd/InternalDdManager.h index 217dedf3cf..4357838453 100644 --- a/src/storm/storage/dd/InternalDdManager.h +++ b/src/storm/storage/dd/InternalDdManager.h @@ -1,5 +1,4 @@ -#ifndef STORM_STORAGE_DD_INTERNALDDMANAGER_H_ -#define STORM_STORAGE_DD_INTERNALDDMANAGER_H_ +#pragma once #include "storm/storage/dd/DdType.h" @@ -9,5 +8,3 @@ template class InternalDdManager; } } // namespace storm - -#endif /* STORM_STORAGE_DD_INTERNALDDMANAGER_H_ */ diff --git a/src/storm/storage/dd/Odd.cpp b/src/storm/storage/dd/Odd.cpp index 4fef8e270a..b67de3f02a 100644 --- a/src/storm/storage/dd/Odd.cpp +++ b/src/storm/storage/dd/Odd.cpp @@ -148,7 +148,6 @@ void Odd::exportToDot(std::string const& filename) const { for (auto const& levelNodes : levelToOddNodesMap) { dotFile << "{ rank = same; \"" << levelNodes.first << "\"\n"; - ; for (auto const& node : levelNodes.second) { dotFile << "\"" << node << "\";\n"; } diff --git a/src/storm/storage/dd/bisimulation/InternalCuddSignatureRefiner.cpp b/src/storm/storage/dd/bisimulation/InternalCuddSignatureRefiner.cpp index ab9c346790..181f3ed8d8 100644 --- a/src/storm/storage/dd/bisimulation/InternalCuddSignatureRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/InternalCuddSignatureRefiner.cpp @@ -1,7 +1,7 @@ #include "storm/storage/dd/bisimulation/InternalCuddSignatureRefiner.h" +#include "storm/exceptions/MissingLibraryException.h" #include "storm/storage/dd/DdManager.h" - #include "storm/storage/dd/bisimulation/Partition.h" #include "storm/storage/dd/bisimulation/Signature.h" @@ -9,6 +9,7 @@ namespace storm { namespace dd { namespace bisimulation { +#ifdef STORM_HAVE_CUDD template InternalSignatureRefiner::InternalSignatureRefiner(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, @@ -40,7 +41,6 @@ Partition InternalSignatureRefiner const& oldPartition, Signature const& signature) { std::pair, boost::optional>> newPartitionDds = refine(oldPartition, signature.getSignatureAdd()); - ; ++numberOfRefinements; return oldPartition.replacePartition(newPartitionDds.first, nextFreeBlockIndex, nextFreeBlockIndex, newPartitionDds.second); } @@ -398,6 +398,27 @@ std::pair InternalSignatureRefiner +InternalSignatureRefiner::InternalSignatureRefiner(storm::dd::DdManager const& manager, + storm::expressions::Variable const& blockVariable, + std::set const& stateVariables, + storm::dd::Bdd const& nondeterminismVariables, + storm::dd::Bdd const& nonBlockVariables, + InternalSignatureRefinerOptions const& options) { + 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."); +} + +template +Partition InternalSignatureRefiner::refine( + Partition const& oldPartition, Signature const& signature) { + 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 template class InternalSignatureRefiner; diff --git a/src/storm/storage/dd/bisimulation/InternalCuddSignatureRefiner.h b/src/storm/storage/dd/bisimulation/InternalCuddSignatureRefiner.h index 06d488eb10..24f59054bc 100644 --- a/src/storm/storage/dd/bisimulation/InternalCuddSignatureRefiner.h +++ b/src/storm/storage/dd/bisimulation/InternalCuddSignatureRefiner.h @@ -1,17 +1,15 @@ #pragma once +#include "storm-config.h" + +#include #include #include -#include "storm/storage/dd/bisimulation/InternalSignatureRefiner.h" - #include "storm/storage/dd/Bdd.h" - -#include "storm/storage/expressions/Variable.h" - +#include "storm/storage/dd/bisimulation/InternalSignatureRefiner.h" #include "storm/storage/dd/cudd/utility.h" - -#include +#include "storm/storage/expressions/Variable.h" namespace storm { namespace dd { @@ -43,6 +41,7 @@ class InternalSignatureRefiner { Signature const& signature); private: +#ifdef STORM_HAVE_CUDD void clearCaches(); std::pair, boost::optional>> refine( @@ -83,8 +82,9 @@ class InternalSignatureRefiner { // The cache used to identify which old block numbers have already been reused. phmap::flat_hash_map reuseBlocksCache; +#endif }; } // namespace bisimulation } // namespace dd -} // namespace storm +} // namespace storm \ No newline at end of file diff --git a/src/storm/storage/dd/bisimulation/InternalSylvanSignatureRefiner.cpp b/src/storm/storage/dd/bisimulation/InternalSylvanSignatureRefiner.cpp index a54caa3869..86f2da1c6d 100644 --- a/src/storm/storage/dd/bisimulation/InternalSylvanSignatureRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/InternalSylvanSignatureRefiner.cpp @@ -1,20 +1,20 @@ #include "storm/storage/dd/bisimulation/InternalSylvanSignatureRefiner.h" -#include "storm/storage/dd/DdManager.h" - -#include "storm/storage/dd/sylvan/InternalSylvanBdd.h" - #include "storm/adapters/RationalFunctionAdapter.h" - +#include "storm/storage/dd/DdManager.h" #include "storm/storage/dd/bisimulation/Partition.h" #include "storm/storage/dd/bisimulation/Signature.h" +#include "storm/storage/dd/sylvan/InternalSylvanBdd.h" +#ifdef STORM_HAVE_SYLVAN #include "sylvan_cache.h" +#endif namespace storm { namespace dd { namespace bisimulation { +#ifdef STORM_HAVE_SYLVAN static const uint64_t NO_ELEMENT_MARKER = -1ull; InternalSylvanSignatureRefinerBase::InternalSylvanSignatureRefinerBase(storm::dd::DdManager const& manager, @@ -369,10 +369,42 @@ TASK_5(BDD, sylvan_refine_partition, BDD, dd, BDD, previous_partition, BDD, nond #pragma GCC diagnostic pop #pragma clang diagnostic pop +#else +InternalSylvanSignatureRefinerBase::InternalSylvanSignatureRefinerBase(storm::dd::DdManager const& manager, + storm::expressions::Variable const& blockVariable, + std::set const& stateVariables, + storm::dd::Bdd const& nondeterminismVariables, + storm::dd::Bdd const& nonBlockVariables, + InternalSignatureRefinerOptions const& options) { + 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."); +} + +template +InternalSignatureRefiner::InternalSignatureRefiner( + storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, + std::set const& stateVariables, storm::dd::Bdd const& nondeterminismVariables, + storm::dd::Bdd const& nonBlockVariables, InternalSignatureRefinerOptions const& options) + : storm::dd::bisimulation::InternalSylvanSignatureRefinerBase(manager, blockVariable, stateVariables, nondeterminismVariables, nonBlockVariables, options) { + 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."); +} + +template +Partition InternalSignatureRefiner::refine( + Partition const& oldPartition, Signature const& signature) { + 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 + template class InternalSignatureRefiner; template class InternalSignatureRefiner; template class InternalSignatureRefiner; } // namespace bisimulation } // namespace dd -} // namespace storm +} // namespace storm \ No newline at end of file diff --git a/src/storm/storage/dd/bisimulation/InternalSylvanSignatureRefiner.h b/src/storm/storage/dd/bisimulation/InternalSylvanSignatureRefiner.h index cf87039a7e..276aef880d 100644 --- a/src/storm/storage/dd/bisimulation/InternalSylvanSignatureRefiner.h +++ b/src/storm/storage/dd/bisimulation/InternalSylvanSignatureRefiner.h @@ -1,15 +1,13 @@ #pragma once -#include "storm/storage/dd/bisimulation/InternalSignatureRefiner.h" +#include +#include "storm-config.h" #include "storm/storage/dd/Bdd.h" - -#include "storm/storage/expressions/Variable.h" - +#include "storm/storage/dd/bisimulation/InternalSignatureRefiner.h" #include "storm/storage/dd/sylvan/InternalSylvanBdd.h" #include "storm/storage/dd/sylvan/utility.h" - -#include +#include "storm/storage/expressions/Variable.h" namespace storm { namespace dd { @@ -31,6 +29,7 @@ class InternalSylvanSignatureRefinerBase { storm::dd::Bdd const& nondeterminismVariables, storm::dd::Bdd const& nonBlockVariables, InternalSignatureRefinerOptions const& options); +#ifdef STORM_HAVE_SYLVAN storm::dd::DdManager const& manager; storm::expressions::Variable blockVariable; std::set stateVariables; @@ -57,6 +56,7 @@ class InternalSylvanSignatureRefinerBase { std::vector table; std::vector oldTable; uint64_t resizeFlag; +#endif }; template @@ -71,12 +71,14 @@ class InternalSignatureRefiner : public In Signature const& signature); private: +#ifdef STORM_HAVE_SYLVAN void clearCaches(); std::pair, boost::optional>> refine( Partition const& oldPartition, storm::dd::Add const& signatureAdd); +#endif }; } // namespace bisimulation } // namespace dd -} // namespace storm +} // namespace storm \ No newline at end of file diff --git a/src/storm/storage/dd/bisimulation/PartialQuotientExtractor.cpp b/src/storm/storage/dd/bisimulation/PartialQuotientExtractor.cpp index 3a6f2a18e1..c9c4035d79 100644 --- a/src/storm/storage/dd/bisimulation/PartialQuotientExtractor.cpp +++ b/src/storm/storage/dd/bisimulation/PartialQuotientExtractor.cpp @@ -164,11 +164,9 @@ std::shared_ptr> Partial template class PartialQuotientExtractor; template class PartialQuotientExtractor; -#ifdef STORM_HAVE_CARL template class PartialQuotientExtractor; template class PartialQuotientExtractor; template class PartialQuotientExtractor; -#endif } // namespace bisimulation } // namespace dd diff --git a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp index 7e60b79909..45b02e890b 100644 --- a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp +++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp @@ -1,38 +1,30 @@ #include "storm/storage/dd/bisimulation/QuotientExtractor.h" +#include #include -#include "storm/storage/dd/DdManager.h" - -#include "storm/models/symbolic/Ctmc.h" -#include "storm/models/symbolic/Dtmc.h" -#include "storm/models/symbolic/MarkovAutomaton.h" -#include "storm/models/symbolic/Mdp.h" -#include "storm/models/symbolic/StandardRewardModel.h" - +#include "storm/adapters/RationalFunctionAdapter.h" +#include "storm/exceptions/MissingLibraryException.h" +#include "storm/exceptions/NotSupportedException.h" #include "storm/models/sparse/Ctmc.h" #include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/StandardRewardModel.h" - -#include "storm/storage/dd/bisimulation/PreservationInformation.h" - -#include "storm/storage/dd/cudd/utility.h" -#include "storm/storage/dd/sylvan/utility.h" - +#include "storm/models/symbolic/Ctmc.h" +#include "storm/models/symbolic/Dtmc.h" +#include "storm/models/symbolic/MarkovAutomaton.h" +#include "storm/models/symbolic/Mdp.h" +#include "storm/models/symbolic/StandardRewardModel.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/BisimulationSettings.h" - -#include "storm/exceptions/NotSupportedException.h" -#include "storm/utility/macros.h" - #include "storm/storage/BitVector.h" #include "storm/storage/SparseMatrix.h" - -#include "storm/adapters/RationalFunctionAdapter.h" - -#include +#include "storm/storage/dd/DdManager.h" +#include "storm/storage/dd/bisimulation/PreservationInformation.h" +#include "storm/storage/dd/cudd/utility.h" +#include "storm/storage/dd/sylvan/utility.h" +#include "storm/utility/macros.h" namespace storm { namespace dd { @@ -72,10 +64,17 @@ class InternalRepresentativeComputer : public InternalR public: InternalRepresentativeComputer(storm::dd::Bdd const& partitionBdd, std::set const& rowVariables) : InternalRepresentativeComputerBase(partitionBdd, rowVariables) { +#ifdef STORM_HAVE_CUDD this->ddman = this->internalDdManager->getCuddManager().getManager(); +#else + 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 } storm::dd::Bdd getRepresentatives() { +#ifdef STORM_HAVE_CUDD return storm::dd::Bdd( *this->ddManager, storm::dd::InternalBdd( @@ -83,9 +82,15 @@ class InternalRepresentativeComputer : public InternalR cudd::BDD(this->internalDdManager->getCuddManager(), this->getRepresentativesRec(this->partitionBdd.getInternalBdd().getCuddDdNode(), this->rowVariablesCube.getInternalBdd().getCuddDdNode()))), this->rowVariables); +#else + 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 } private: +#ifdef STORM_HAVE_CUDD DdNodePtr getRepresentativesRec(DdNodePtr partitionNode, DdNodePtr stateVariablesCube) { if (partitionNode == Cudd_ReadLogicZero(ddman)) { return partitionNode; @@ -157,6 +162,7 @@ class InternalRepresentativeComputer : public InternalR ::DdManager* ddman; phmap::flat_hash_map visitedNodes; +#endif }; template<> @@ -164,19 +170,31 @@ class InternalRepresentativeComputer : public Interna public: InternalRepresentativeComputer(storm::dd::Bdd const& partitionBdd, std::set const& rowVariables) : InternalRepresentativeComputerBase(partitionBdd, rowVariables) { +#ifndef STORM_HAVE_SYLVAN + 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 // Intentionally left empty. } storm::dd::Bdd getRepresentatives() { +#ifdef STORM_HAVE_SYLVAN return storm::dd::Bdd( *this->ddManager, storm::dd::InternalBdd( this->internalDdManager, sylvan::Bdd(this->getRepresentativesRec(this->partitionBdd.getInternalBdd().getSylvanBdd().GetBDD(), this->rowVariablesCube.getInternalBdd().getSylvanBdd().GetBDD()))), this->rowVariables); +#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 } private: +#ifdef STORM_HAVE_SYLVAN BDD getRepresentativesRec(BDD partitionNode, BDD stateVariablesCube) { if (partitionNode == sylvan_false) { return sylvan_false; @@ -238,6 +256,7 @@ class InternalRepresentativeComputer : public Interna } phmap::flat_hash_map visitedNodes; +#endif }; template @@ -434,6 +453,7 @@ class InternalSparseQuotientExtractorBase { template class InternalSparseQuotientExtractor : public InternalSparseQuotientExtractorBase { public: +#ifdef STORM_HAVE_CUDD InternalSparseQuotientExtractor(storm::models::symbolic::Model const& model, storm::dd::Bdd const& partitionBdd, storm::expressions::Variable const& blockVariable, uint64_t numberOfBlocks, storm::dd::Bdd const& representatives) @@ -441,25 +461,48 @@ class InternalSparseQuotientExtractor : publ ddman(this->manager.getInternalDdManager().getCuddManager().getManager()) { this->createBlockToOffsetMapping(); } +#else + InternalSparseQuotientExtractor(storm::models::symbolic::Model const& model, + storm::dd::Bdd const& partitionBdd, storm::expressions::Variable const& blockVariable, + uint64_t numberOfBlocks, storm::dd::Bdd const& representatives) + : InternalSparseQuotientExtractorBase(model, partitionBdd, blockVariable, numberOfBlocks, representatives) { + 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 private: virtual storm::storage::SparseMatrix extractMatrixInternal(storm::dd::Add const& matrix) override { +#ifdef STORM_HAVE_CUDD + this->createMatrixEntryStorage(); extractTransitionMatrixRec(matrix.getInternalAdd().getCuddDdNode(), this->isNondeterministic ? this->nondeterminismOdd : this->odd, 0, this->partitionBdd.getInternalBdd().getCuddDdNode(), this->representatives.getInternalBdd().getCuddDdNode(), this->allSourceVariablesCube.getInternalBdd().getCuddDdNode(), this->nondeterminismVariablesCube.getInternalBdd().getCuddDdNode(), this->isNondeterministic ? &this->odd : nullptr, 0); return this->createMatrixFromEntries(); +#else + 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 } virtual std::vector extractVectorInternal(storm::dd::Add const& vector, storm::dd::Bdd const& variablesCube, storm::dd::Odd const& odd) override { +#ifdef STORM_HAVE_CUDD std::vector result(odd.getTotalOffset()); extractVectorRec(vector.getInternalAdd().getCuddDdNode(), this->representatives.getInternalBdd().getCuddDdNode(), variablesCube.getInternalBdd().getCuddDdNode(), odd, 0, result); return result; +#else + 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 } - +#ifdef STORM_HAVE_CUDD void createBlockToOffsetMapping() { this->createBlockToOffsetMappingRec(this->partitionBdd.getInternalBdd().getCuddDdNode(), this->representatives.getInternalBdd().getCuddDdNode(), this->rowVariablesCube.getInternalBdd().getCuddDdNode(), this->odd, 0); @@ -676,6 +719,7 @@ class InternalSparseQuotientExtractor : publ // A mapping from blocks (stored in terms of a DD node) to the offset of the corresponding block. phmap::flat_hash_map blockToOffset; +#endif }; template @@ -687,11 +731,18 @@ class InternalSparseQuotientExtractor const& representatives) : InternalSparseQuotientExtractorBase(model, partitionBdd, blockVariable, numberOfBlocks, representatives) { +#ifdef STORM_HAVE_SYLVAN this->createBlockToOffsetMapping(); +#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 } private: virtual storm::storage::SparseMatrix extractMatrixInternal(storm::dd::Add const& matrix) override { +#ifdef STORM_HAVE_SYLVAN this->createMatrixEntryStorage(); extractTransitionMatrixRec(matrix.getInternalAdd().getSylvanMtbdd().GetMTBDD(), this->isNondeterministic ? this->nondeterminismOdd : this->odd, 0, this->partitionBdd.getInternalBdd().getSylvanBdd().GetBDD(), this->representatives.getInternalBdd().getSylvanBdd().GetBDD(), @@ -699,17 +750,29 @@ class InternalSparseQuotientExtractornondeterminismVariablesCube.getInternalBdd().getSylvanBdd().GetBDD(), this->isNondeterministic ? &this->odd : nullptr, 0); return this->createMatrixFromEntries(); +#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 } virtual std::vector extractVectorInternal(storm::dd::Add const& vector, storm::dd::Bdd const& variablesCube, storm::dd::Odd const& odd) override { +#ifdef STORM_HAVE_SYLVAN std::vector result(odd.getTotalOffset()); extractVectorRec(vector.getInternalAdd().getSylvanMtbdd().GetMTBDD(), this->representatives.getInternalBdd().getSylvanBdd().GetBDD(), variablesCube.getInternalBdd().getSylvanBdd().GetBDD(), odd, 0, result); return result; +#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 } +#ifdef STORM_HAVE_SYLVAN void extractVectorRec(MTBDD vector, BDD representativesNode, BDD variables, storm::dd::Odd const& odd, uint64_t offset, std::vector& result) { if (representativesNode == sylvan_false || mtbdd_iszero(vector)) { @@ -899,6 +962,7 @@ class InternalSparseQuotientExtractor blockToOffset; +#endif }; template diff --git a/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp b/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp index 7b39559159..4e8dfaa3fd 100644 --- a/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp @@ -1,8 +1,8 @@ #include "storm/storage/dd/bisimulation/SignatureRefiner.h" #include "storm/storage/dd/DdManager.h" - #include "storm/storage/dd/bisimulation/InternalCuddSignatureRefiner.h" +#include "storm/storage/dd/bisimulation/InternalSignatureRefiner.h" #include "storm/storage/dd/bisimulation/InternalSylvanSignatureRefiner.h" namespace storm { diff --git a/src/storm/storage/dd/cudd/CuddAddIterator.cpp b/src/storm/storage/dd/cudd/CuddAddIterator.cpp index dcd0455a7c..5be0093a68 100644 --- a/src/storm/storage/dd/cudd/CuddAddIterator.cpp +++ b/src/storm/storage/dd/cudd/CuddAddIterator.cpp @@ -1,15 +1,18 @@ #include "storm/storage/dd/cudd/CuddAddIterator.h" + +#include + +#include "storm/exceptions/MissingLibraryException.h" #include "storm/storage/dd/DdManager.h" #include "storm/storage/dd/DdMetaVariable.h" #include "storm/storage/expressions/ExpressionManager.h" -#include "storm/utility/macros.h" - #include "storm/utility/constants.h" - -#include +#include "storm/utility/macros.h" namespace storm { namespace dd { + +#ifdef STORM_HAVE_CUDD template AddIterator::AddIterator() : ddManager(), @@ -216,11 +219,63 @@ std::pair AddIterator(valueAsDouble)); } +#else +template +AddIterator::AddIterator() { + 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."); +} + +template +AddIterator::AddIterator(AddIterator&& other) { + 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."); +} + +template +AddIterator& AddIterator::operator=(AddIterator&& other) { + 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."); +} + +template +AddIterator::~AddIterator() {} + +template +AddIterator& AddIterator::operator++() { + 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."); +} + +template +bool AddIterator::operator==(AddIterator const& other) const { + 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."); +} + +template +bool AddIterator::operator!=(AddIterator const& other) const { + 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."); +} + +template +std::pair AddIterator::operator*() const { + 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 + template class AddIterator; template class AddIterator; - -#ifdef STORM_HAVE_CARL template class AddIterator; -#endif + } // namespace dd -} // namespace storm +} // namespace storm \ No newline at end of file diff --git a/src/storm/storage/dd/cudd/CuddAddIterator.h b/src/storm/storage/dd/cudd/CuddAddIterator.h index d6c0677762..c636190cb4 100644 --- a/src/storm/storage/dd/cudd/CuddAddIterator.h +++ b/src/storm/storage/dd/cudd/CuddAddIterator.h @@ -1,5 +1,6 @@ -#ifndef STORM_STORAGE_DD_CUDDADDITERATOR_H_ -#define STORM_STORAGE_DD_CUDDADDITERATOR_H_ +#pragma once + +#include "storm-config.h" #include #include @@ -10,8 +11,10 @@ #include "storm/storage/dd/AddIterator.h" #include "storm/storage/expressions/SimpleValuation.h" +#ifdef STORM_HAVE_CUDD // Include the C++-interface of CUDD. #include "cuddObj.hh" +#endif namespace storm { namespace dd { @@ -75,6 +78,7 @@ class AddIterator { bool operator!=(AddIterator const& other) const; private: +#ifdef STORM_HAVE_CUDD /*! * Constructs a forward iterator using the given generator with the given set of relevant meta variables. * @@ -133,8 +137,7 @@ class AddIterator { // The current valuation of meta variables. storm::expressions::SimpleValuation currentValuation; +#endif }; } // namespace dd } // namespace storm - -#endif /* STORM_STORAGE_DD_CUDDADDITERATOR_H_ */ diff --git a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp index af8121e563..f6d9637fb6 100644 --- a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp +++ b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp @@ -1,20 +1,20 @@ #include "storm/storage/dd/cudd/InternalCuddAdd.h" +#include "storm/exceptions/MissingLibraryException.h" +#include "storm/exceptions/NotSupportedException.h" +#include "storm/storage/BitVector.h" +#include "storm/storage/SparseMatrix.h" #include "storm/storage/dd/Odd.h" #include "storm/storage/dd/cudd/CuddAddIterator.h" #include "storm/storage/dd/cudd/InternalCuddBdd.h" #include "storm/storage/dd/cudd/InternalCuddDdManager.h" - -#include "storm/storage/BitVector.h" -#include "storm/storage/SparseMatrix.h" - -#include "storm/exceptions/NotImplementedException.h" -#include "storm/exceptions/NotSupportedException.h" #include "storm/utility/constants.h" #include "storm/utility/macros.h" namespace storm { namespace dd { + +#ifdef STORM_HAVE_CUDD template InternalAdd::InternalAdd(InternalDdManager const* ddManager, cudd::ADD cuddAdd) : ddManager(ddManager), cuddAdd(cuddAdd) { @@ -874,16 +874,576 @@ DdNode* InternalAdd::fromVectorRec(::DdMana STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported"); } +#else +template +bool InternalAdd::operator==(InternalAdd const& other) const { + 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."); +} + +template +bool InternalAdd::operator!=(InternalAdd const& other) const { + 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."); +} + +template +InternalAdd InternalAdd::operator+(InternalAdd const& other) const { + 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."); +} + +template +InternalAdd& InternalAdd::operator+=(InternalAdd const& other) { + 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."); +} + +template +InternalAdd InternalAdd::operator*(InternalAdd const& other) const { + 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."); +} + +template +InternalAdd& InternalAdd::operator*=(InternalAdd const& other) { + 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."); +} + +template +InternalAdd InternalAdd::operator-(InternalAdd const& other) const { + 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."); +} + +template +InternalAdd& InternalAdd::operator-=(InternalAdd const& other) { + 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."); +} + +template +InternalAdd InternalAdd::operator/(InternalAdd const& other) const { + 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."); +} + +template +InternalAdd& InternalAdd::operator/=(InternalAdd const& other) { + 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."); +} + +template +InternalBdd InternalAdd::equals(InternalAdd const& other) const { + 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."); +} + +template +InternalBdd InternalAdd::notEquals(InternalAdd const& other) const { + 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."); +} + +template +InternalBdd InternalAdd::less(InternalAdd const& other) const { + 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."); +} + +template +InternalBdd InternalAdd::lessOrEqual(InternalAdd const& other) const { + 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."); +} + +template +InternalBdd InternalAdd::greater(InternalAdd const& other) const { + 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."); +} + +template +InternalBdd InternalAdd::greaterOrEqual(InternalAdd const& other) const { + 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."); +} + +template +InternalAdd InternalAdd::pow(InternalAdd const& other) const { + 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."); +} + +template +InternalAdd InternalAdd::mod(InternalAdd const& other) const { + 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."); +} + +template +InternalAdd InternalAdd::logxy(InternalAdd const& other) const { + 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."); +} + +template +InternalAdd InternalAdd::floor() const { + 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."); +} + +template +InternalAdd InternalAdd::ceil() const { + 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."); +} + +template +InternalAdd InternalAdd::sharpenKwekMehlhorn(size_t /*precision*/) const { + 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."); +} + +template +InternalAdd InternalAdd::minimum(InternalAdd const& other) const { + 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."); +} + +template +InternalAdd InternalAdd::maximum(InternalAdd const& other) const { + 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."); +} + +template +template +typename std::enable_if::value, InternalAdd>::type +InternalAdd::toValueType() const { + 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."); +} + +template +template +typename std::enable_if::value, InternalAdd>::type +InternalAdd::toValueType() const { + 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."); +} + +template +InternalAdd InternalAdd::sumAbstract(InternalBdd const& cube) const { + 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."); +} + +template +InternalAdd InternalAdd::minAbstract(InternalBdd const& cube) const { + 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."); +} + +template +InternalBdd InternalAdd::minAbstractRepresentative(InternalBdd const& cube) const { + 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."); +} + +template +InternalAdd InternalAdd::maxAbstract(InternalBdd const& cube) const { + 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."); +} + +template +InternalBdd InternalAdd::maxAbstractRepresentative(InternalBdd const& cube) const { + 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."); +} + +template +bool InternalAdd::equalModuloPrecision(InternalAdd const& other, ValueType const& precision, + bool relative) const { + 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."); +} + +template<> +bool InternalAdd::equalModuloPrecision(InternalAdd const& /*other*/, + storm::RationalNumber const& /*precision*/, bool /*relative*/) const { + 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."); +} + +template +InternalAdd InternalAdd::swapVariables(std::vector> const& from, + std::vector> const& to) const { + 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."); +} + +template +InternalAdd InternalAdd::permuteVariables(std::vector> const& from, + std::vector> const& to) const { + 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."); +} + +template +InternalAdd InternalAdd::multiplyMatrix( + InternalAdd const& otherMatrix, std::vector> const& summationDdVariables) const { + 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."); +} + +template +InternalAdd InternalAdd::multiplyMatrix( + InternalBdd const& otherMatrix, std::vector> const& summationDdVariables) const { + 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."); +} + +template +InternalBdd InternalAdd::greater(ValueType const& value) const { + 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."); +} + +template<> +InternalBdd InternalAdd::greater(storm::RationalNumber const& value) const { + 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."); +} + +template +InternalBdd InternalAdd::greaterOrEqual(ValueType const& value) const { + 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."); +} + +template<> +InternalBdd InternalAdd::greaterOrEqual(storm::RationalNumber const& value) const { + 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."); +} + +template +InternalBdd InternalAdd::less(ValueType const& value) const { + 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."); +} + +template<> +InternalBdd InternalAdd::less(storm::RationalNumber const& value) const { + 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."); +} + +template +InternalBdd InternalAdd::lessOrEqual(ValueType const& value) const { + 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."); +} + +template<> +InternalBdd InternalAdd::lessOrEqual(storm::RationalNumber const& value) const { + 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."); +} + +template +InternalBdd InternalAdd::notZero() const { + 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."); +} + +template +InternalAdd InternalAdd::constrain(InternalAdd const& constraint) const { + 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."); +} + +template +InternalAdd InternalAdd::restrict(InternalAdd const& constraint) const { + 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."); +} + +template +InternalBdd InternalAdd::getSupport() const { + 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."); +} + +template +uint_fast64_t InternalAdd::getNonZeroCount(uint_fast64_t numberOfDdVariables) const { + 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."); +} + +template +uint_fast64_t InternalAdd::getLeafCount() const { + 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."); +} + +template +uint_fast64_t InternalAdd::getNodeCount() const { + 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."); +} + +template +ValueType InternalAdd::getMin() const { + 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."); +} + +template +ValueType InternalAdd::getMax() const { + 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."); +} + +template +ValueType InternalAdd::getValue() const { + 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."); +} + +template +bool InternalAdd::isOne() const { + 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."); +} + +template +bool InternalAdd::isZero() const { + 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."); +} + +template +bool InternalAdd::isConstant() const { + 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."); +} + +template +uint_fast64_t InternalAdd::getIndex() const { + 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."); +} + +template +uint_fast64_t InternalAdd::getLevel() const { + 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."); +} + +template +void InternalAdd::exportToDot(std::string const& filename, std::vector const& ddVariableNamesAsStrings, + bool showVariablesIfPossible) const { + 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."); +} + +template +void InternalAdd::exportToText(std::string const&) const { + 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."); +} + +template +AddIterator InternalAdd::begin(DdManager const& fullDdManager, InternalBdd const&, + uint_fast64_t, std::set const& metaVariables, + bool enumerateDontCareMetaVariables) const { + 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."); +} + +template +AddIterator InternalAdd::end(DdManager const& fullDdManager) const { + 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."); +} + +template +std::string InternalAdd::getStringId() const { + 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."); +} + +template +Odd InternalAdd::createOdd(std::vector const& ddVariableIndices) const { + 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."); +} + +template +InternalDdManager const& InternalAdd::getInternalDdManager() const { + 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."); +} + +template +void InternalAdd::composeWithExplicitVector(storm::dd::Odd const& odd, std::vector const& ddVariableIndices, + std::vector& targetVector, + std::function const& function) const { + 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."); +} + +template +void InternalAdd::forEach(Odd const& odd, std::vector const& ddVariableIndices, + std::function const& function) const { + 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."); +} + +template +void InternalAdd::composeWithExplicitVector(storm::dd::Odd const& odd, std::vector const& ddVariableIndices, + std::vector const& offsets, std::vector& targetVector, + std::function const& function) const { + 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."); +} + +template +std::vector InternalAdd::decodeGroupLabels(std::vector const& ddGroupVariableIndices, + storm::storage::BitVector const& ddLabelVariableIndices) const { + 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."); +} + +template +std::vector> InternalAdd::splitIntoGroups( + std::vector const& ddGroupVariableIndices) const { + 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."); +} + +template +std::vector, InternalAdd>> InternalAdd::splitIntoGroups( + InternalAdd vector, std::vector const& ddGroupVariableIndices) const { + 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."); +} + +template +std::vector>> InternalAdd::splitIntoGroups( + std::vector> const& vectors, std::vector const& ddGroupVariableIndices) const { + 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."); +} + +template +void InternalAdd::toMatrixComponents(std::vector const& rowGroupIndices, std::vector& rowIndications, + std::vector>& columnsAndValues, + Odd const& rowOdd, Odd const& columnOdd, std::vector const& ddRowVariableIndices, + std::vector const& ddColumnVariableIndices, bool writeValues) const { + 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."); +} + +template +InternalAdd InternalAdd::fromVector(InternalDdManager const* ddManager, + std::vector const& values, storm::dd::Odd const& odd, + std::vector const& ddVariableIndices) { + 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 + template class InternalAdd; template InternalAdd InternalAdd::toValueType() const; template class InternalAdd; template InternalAdd InternalAdd::toValueType() const; -#ifdef STORM_HAVE_CARL template class InternalAdd; template InternalAdd InternalAdd::toValueType() const; template InternalAdd InternalAdd::toValueType() const; template InternalAdd InternalAdd::toValueType() const; -#endif } // namespace dd -} // namespace storm +} // namespace storm \ No newline at end of file diff --git a/src/storm/storage/dd/cudd/InternalCuddAdd.h b/src/storm/storage/dd/cudd/InternalCuddAdd.h index 38118c6932..536bedf7c6 100644 --- a/src/storm/storage/dd/cudd/InternalCuddAdd.h +++ b/src/storm/storage/dd/cudd/InternalCuddAdd.h @@ -1,5 +1,6 @@ -#ifndef STORM_STORAGE_DD_CUDD_INTERNALCUDDADD_H_ -#define STORM_STORAGE_DD_CUDD_INTERNALCUDDADD_H_ +#pragma once + +#include "storm-config.h" #include #include @@ -7,15 +8,15 @@ #include #include "storm/adapters/RationalNumberAdapter.h" - #include "storm/storage/dd/DdType.h" #include "storm/storage/dd/InternalAdd.h" #include "storm/storage/dd/Odd.h" - #include "storm/storage/expressions/Variable.h" +#ifdef STORM_HAVE_CUDD // Include the C++-interface of CUDD. #include "cuddObj.hh" +#endif namespace storm { namespace storage { @@ -53,6 +54,7 @@ class InternalAdd { friend class bisimulation::InternalSignatureRefiner; +#ifdef STORM_HAVE_CUDD /*! * Creates an ADD that encapsulates the given CUDD ADD. * @@ -60,6 +62,7 @@ class InternalAdd { * @param cuddAdd The CUDD ADD to store. */ InternalAdd(InternalDdManager const* ddManager, cudd::ADD cuddAdd); +#endif // Instantiate all copy/move constructors/assignments with the default implementation. InternalAdd() = default; @@ -670,6 +673,7 @@ class InternalAdd { InternalDdManager const& getInternalDdManager() const; +#ifdef STORM_HAVE_CUDD /*! * Retrieves the CUDD ADD object associated with this ADD. * @@ -683,6 +687,7 @@ class InternalAdd { * @return The DD node of CUDD associated with this ADD. */ DdNode* getCuddDdNode() const; +#endif /*! * Retrieves a string representation of an ID for thid ADD. @@ -690,6 +695,7 @@ class InternalAdd { std::string getStringId() const; private: +#ifdef STORM_HAVE_CUDD /*! * Performs a recursive step for forEach. * @@ -827,8 +833,7 @@ class InternalAdd { InternalDdManager const* ddManager; cudd::ADD cuddAdd; +#endif }; } // namespace dd } // namespace storm - -#endif /* STORM_STORAGE_DD_CUDD_INTERNALCUDDADD_H_ */ diff --git a/src/storm/storage/dd/cudd/InternalCuddBdd.cpp b/src/storm/storage/dd/cudd/InternalCuddBdd.cpp index b1f8e1fb3a..5cd2dceb0c 100644 --- a/src/storm/storage/dd/cudd/InternalCuddBdd.cpp +++ b/src/storm/storage/dd/cudd/InternalCuddBdd.cpp @@ -2,17 +2,18 @@ #include -#include "storm/storage/dd/Odd.h" -#include "storm/storage/dd/cudd/InternalCuddDdManager.h" - +#include "storm/exceptions/MissingLibraryException.h" +#include "storm/exceptions/NotSupportedException.h" #include "storm/storage/BitVector.h" #include "storm/storage/PairHash.h" - -#include "storm/exceptions/NotSupportedException.h" +#include "storm/storage/dd/Odd.h" +#include "storm/storage/dd/cudd/InternalCuddDdManager.h" #include "storm/utility/macros.h" namespace storm { namespace dd { + +#ifdef STORM_HAVE_CUDD InternalBdd::InternalBdd(InternalDdManager const* ddManager, cudd::BDD cuddBdd) : ddManager(ddManager), cuddBdd(cuddBdd) { // Intentionally left empty. } @@ -610,13 +611,277 @@ storm::expressions::Variable InternalBdd::toExpressionRec( // Return the variable for this node. return newNodeVariable; } +#else +InternalBdd InternalBdd::fromVector(InternalDdManager const* ddManager, Odd const& odd, + std::vector const& sortedDdVariableIndices, + std::function const& filter) { + 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."); +} + +bool InternalBdd::operator==(InternalBdd const& other) const { + 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."); +} + +bool InternalBdd::operator!=(InternalBdd const& other) const { + 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."); +} + +InternalBdd InternalBdd::relationalProduct(InternalBdd const& relation, + std::vector> const& rowVariables, + std::vector> const& columnVariables) const { + 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."); +} + +InternalBdd InternalBdd::inverseRelationalProduct(InternalBdd const& relation, + std::vector> const& rowVariables, + std::vector> const& columnVariables) const { + 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."); +} + +InternalBdd InternalBdd::inverseRelationalProductWithExtendedRelation( + InternalBdd const& relation, std::vector> const& rowVariables, + std::vector> const& columnVariables) const { + 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."); +} + +InternalBdd InternalBdd::ite(InternalBdd const& thenDd, InternalBdd const& elseDd) const { + 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."); +} + +template +InternalAdd InternalBdd::ite(InternalAdd const& thenAdd, + InternalAdd const& elseAdd) const { + 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."); +} + +InternalBdd InternalBdd::operator||(InternalBdd const& other) const { + 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."); +} + +InternalBdd& InternalBdd::operator|=(InternalBdd const& other) { + 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."); +} + +InternalBdd InternalBdd::operator&&(InternalBdd const& other) const { + 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."); +} + +InternalBdd& InternalBdd::operator&=(InternalBdd const& other) { + 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."); +} + +InternalBdd InternalBdd::iff(InternalBdd const& other) const { + 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."); +} + +InternalBdd InternalBdd::exclusiveOr(InternalBdd const& other) const { + 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."); +} + +InternalBdd InternalBdd::implies(InternalBdd const& other) const { + 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."); +} + +InternalBdd InternalBdd::operator!() const { + 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."); +} + +InternalBdd& InternalBdd::complement() { + 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."); +} + +InternalBdd InternalBdd::existsAbstract(InternalBdd const& cube) const { + 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."); +} + +InternalBdd InternalBdd::existsAbstractRepresentative(InternalBdd const& cube) const { + 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."); +} + +InternalBdd InternalBdd::universalAbstract(InternalBdd const& cube) const { + 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."); +} + +InternalBdd InternalBdd::andExists(InternalBdd const& other, InternalBdd const& cube) const { + 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."); +} + +InternalBdd InternalBdd::constrain(InternalBdd const& constraint) const { + 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."); +} + +InternalBdd InternalBdd::restrict(InternalBdd const& constraint) const { + 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."); +} + +InternalBdd InternalBdd::swapVariables(std::vector> const& from, + std::vector> const& to) const { + 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."); +} + +InternalBdd InternalBdd::getSupport() const { + 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."); +} + +uint_fast64_t InternalBdd::getNonZeroCount(uint_fast64_t numberOfDdVariables) const { + 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."); +} + +uint_fast64_t InternalBdd::getLeafCount() const { + 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."); +} + +uint_fast64_t InternalBdd::getNodeCount() const { + 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."); +} + +bool InternalBdd::isOne() const { + 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."); +} + +bool InternalBdd::isZero() const { + 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."); +} + +uint_fast64_t InternalBdd::getIndex() const { + 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."); +} + +uint_fast64_t InternalBdd::getLevel() const { + 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."); +} + +void InternalBdd::exportToDot(std::string const& filename, std::vector const& ddVariableNamesAsStrings, + bool showVariablesIfPossible) const { + 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."); +} + +void InternalBdd::exportToText(std::string const&) const { + 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."); +} + +template +InternalAdd InternalBdd::toAdd() const { + 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."); +} + +storm::storage::BitVector InternalBdd::toVector(storm::dd::Odd const& rowOdd, std::vector const& ddVariableIndices) const { + 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."); +} + +Odd InternalBdd::createOdd(std::vector const& ddVariableIndices) const { + 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."); +} + +template +void InternalBdd::filterExplicitVector(Odd const& odd, std::vector const& ddVariableIndices, + std::vector const& sourceValues, std::vector& targetValues) const { + 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."); +} + +std::vector> InternalBdd::splitIntoGroups(std::vector const& ddGroupVariableIndices) const { + 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."); +} + +void InternalBdd::filterExplicitVector(Odd const& odd, std::vector const& ddVariableIndices, + storm::storage::BitVector const& sourceValues, storm::storage::BitVector& targetValues) const { + 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."); +} + +std::pair, std::unordered_map> InternalBdd::toExpression( + storm::expressions::ExpressionManager& manager) const { + 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 template InternalAdd InternalBdd::toAdd() const; template InternalAdd InternalBdd::toAdd() const; -#ifdef STORM_HAVE_CARL template InternalAdd InternalBdd::toAdd() const; -#endif +#ifdef STORM_HAVE_CUDD template void InternalBdd::filterExplicitVectorRec(DdNode const* dd, cudd::Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, uint_fast64_t currentOffset, @@ -628,6 +893,7 @@ template void InternalBdd::filterExplicitVectorRec( uint_fast64_t currentOffset, storm::dd::Odd const& odd, std::vector& result, uint_fast64_t& currentIndex, std::vector const& values); +#endif template void InternalBdd::filterExplicitVector(Odd const& odd, std::vector const& ddVariableIndices, std::vector const& sourceValues, std::vector& targetValues) const; @@ -641,4 +907,4 @@ template InternalAdd InternalBdd::ite template InternalAdd InternalBdd::ite(InternalAdd const& thenAdd, InternalAdd const& elseAdd) const; } // namespace dd -} // namespace storm +} // namespace storm \ No newline at end of file diff --git a/src/storm/storage/dd/cudd/InternalCuddBdd.h b/src/storm/storage/dd/cudd/InternalCuddBdd.h index 60061e9037..f3bcf551e8 100644 --- a/src/storm/storage/dd/cudd/InternalCuddBdd.h +++ b/src/storm/storage/dd/cudd/InternalCuddBdd.h @@ -1,20 +1,23 @@ -#ifndef STORM_STORAGE_DD_CUDD_INTERNALCUDDBDD_H_ -#define STORM_STORAGE_DD_CUDD_INTERNALCUDDBDD_H_ +#pragma once + +#include "storm-config.h" #include #include #include #include -#include "storm/storage/expressions/Expression.h" -#include "storm/storage/expressions/ExpressionManager.h" - +#include "storm/exceptions/MissingLibraryException.h" #include "storm/storage/dd/DdType.h" #include "storm/storage/dd/InternalAdd.h" #include "storm/storage/dd/InternalBdd.h" +#include "storm/storage/expressions/Expression.h" +#include "storm/storage/expressions/ExpressionManager.h" +#ifdef STORM_HAVE_CUDD // Include the C++-interface of CUDD. #include "cuddObj.hh" +#endif namespace storm { namespace storage { @@ -36,6 +39,7 @@ class InternalBdd { template friend class InternalAdd; +#ifdef STORM_HAVE_CUDD /*! * Creates a DD that encapsulates the given CUDD ADD. * @@ -44,6 +48,7 @@ class InternalBdd { * @param containedMetaVariables The meta variables that appear in the DD. */ InternalBdd(InternalDdManager const* ddManager, cudd::BDD cuddBdd); +#endif // Instantiate all copy/move constructors/assignments with the default implementation. InternalBdd() = default; @@ -411,6 +416,7 @@ class InternalBdd { friend struct std::hash>; +#ifdef STORM_HAVE_CUDD /*! * Retrieves the CUDD BDD object associated with this DD. * @@ -424,8 +430,10 @@ class InternalBdd { * @return The DD node of CUDD associated with this BDD. */ DdNode* getCuddDdNode() const; +#endif private: +#ifdef STORM_HAVE_CUDD /*! * Builds a BDD representing the values that make the given filter function evaluate to true. * @@ -547,6 +555,7 @@ class InternalBdd { InternalDdManager const* ddManager; cudd::BDD cuddBdd; +#endif }; } // namespace dd } // namespace storm @@ -554,10 +563,16 @@ class InternalBdd { namespace std { template<> struct hash> { +#ifdef STORM_HAVE_CUDD std::size_t operator()(storm::dd::InternalBdd const& key) const { return reinterpret_cast(key.cuddBdd.getNode()); } +#else + std::size_t operator()(storm::dd::InternalBdd const&) const { + 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 }; } // namespace std - -#endif /* STORM_STORAGE_DD_CUDD_INTERNALCUDDBDD_H_ */ diff --git a/src/storm/storage/dd/cudd/InternalCuddDdManager.cpp b/src/storm/storage/dd/cudd/InternalCuddDdManager.cpp index fbbc40c114..f16e5524c9 100644 --- a/src/storm/storage/dd/cudd/InternalCuddDdManager.cpp +++ b/src/storm/storage/dd/cudd/InternalCuddDdManager.cpp @@ -1,13 +1,15 @@ #include "storm/storage/dd/cudd/InternalCuddDdManager.h" +#include "storm/exceptions/MissingLibraryException.h" +#include "storm/exceptions/NotSupportedException.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/CuddSettings.h" - -#include "storm/exceptions/NotSupportedException.h" +#include "storm/utility/macros.h" namespace storm { namespace dd { +#ifdef STORM_HAVE_CUDD InternalDdManager::InternalDdManager() : cuddManager(), reorderingTechnique(CUDD_REORDER_NONE), numberOfDdVariables(0) { this->cuddManager.SetMaxMemory( static_cast(storm::settings::getModule().getMaximalMemory() * 1024ul * 1024ul)); @@ -217,6 +219,122 @@ uint_fast64_t InternalDdManager::getNumberOfDdVariables() const { return numberOfDdVariables; } +#else + +InternalDdManager::InternalDdManager() { + 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."); +} + +InternalDdManager::~InternalDdManager() { + // Intentionally left empty. +} + +InternalBdd InternalDdManager::getBddOne() const { + 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."); +} + +template +InternalAdd InternalDdManager::getAddOne() const { + 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."); +} + +InternalBdd InternalDdManager::getBddZero() const { + 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."); +} + +InternalBdd InternalDdManager::getBddEncodingLessOrEqualThan(uint64_t bound, InternalBdd const& cube, + uint64_t numberOfDdVariables) const { + 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."); +} + +template +InternalAdd InternalDdManager::getAddZero() const { + 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."); +} + +template +InternalAdd InternalDdManager::getAddUndefined() const { + 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."); +} + +template +InternalAdd InternalDdManager::getConstant(ValueType const& value) const { + 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."); +} + +template<> +InternalAdd InternalDdManager::getConstant(storm::RationalNumber const& value) const { + 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."); +} + +std::vector> InternalDdManager::createDdVariables(uint64_t numberOfLayers, + boost::optional const& position) { + 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."); +} + +bool InternalDdManager::supportsOrderedInsertion() const { + 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."); +} + +void InternalDdManager::allowDynamicReordering(bool value) { + 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."); +} + +bool InternalDdManager::isDynamicReorderingAllowed() const { + 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."); +} + +void InternalDdManager::triggerReordering() { + 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."); +} + +void InternalDdManager::debugCheck() const { + 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."); +} + +void InternalDdManager::execute(std::function const& f) const { + 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."); +} + +uint_fast64_t InternalDdManager::getNumberOfDdVariables() const { + 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 + template InternalAdd InternalDdManager::getAddOne() const; template InternalAdd InternalDdManager::getAddOne() const; template InternalAdd InternalDdManager::getAddOne() const; diff --git a/src/storm/storage/dd/cudd/InternalCuddDdManager.h b/src/storm/storage/dd/cudd/InternalCuddDdManager.h index 6b1aed667d..212c93f692 100644 --- a/src/storm/storage/dd/cudd/InternalCuddDdManager.h +++ b/src/storm/storage/dd/cudd/InternalCuddDdManager.h @@ -1,16 +1,18 @@ -#ifndef STORM_STORAGE_DD_INTERNALCUDDDDMANAGER_H_ -#define STORM_STORAGE_DD_INTERNALCUDDDDMANAGER_H_ +#pragma once + +#include "storm-config.h" #include #include #include "storm/storage/dd/DdType.h" #include "storm/storage/dd/InternalDdManager.h" - #include "storm/storage/dd/cudd/InternalCuddAdd.h" #include "storm/storage/dd/cudd/InternalCuddBdd.h" +#ifdef STORM_HAVE_CUDD #include "cuddObj.hh" +#endif namespace storm { namespace dd { @@ -148,6 +150,7 @@ class InternalDdManager { */ uint_fast64_t getNumberOfDdVariables() const; +#ifdef STORM_HAVE_CUDD /*! * Retrieves the underlying CUDD manager. * @@ -161,8 +164,10 @@ class InternalDdManager { * @return The underlying CUDD manager. */ cudd::Cudd const& getCuddManager() const; +#endif private: +#ifdef STORM_HAVE_CUDD // Helper function to create the BDD whose encodings are below a given bound. DdNodePtr getBddEncodingLessOrEqualThanRec(uint64_t minimalValue, uint64_t maximalValue, uint64_t bound, DdNodePtr cube, uint64_t remainingDdVariables) const; @@ -175,8 +180,7 @@ class InternalDdManager { // Keeps track of the number of registered DD variables. uint_fast64_t numberOfDdVariables; +#endif }; } // namespace dd } // namespace storm - -#endif /* STORM_STORAGE_DD_INTERNALCUDDDDMANAGER_H_ */ diff --git a/src/storm/storage/dd/cudd/utility.h b/src/storm/storage/dd/cudd/utility.h index 8b6f0326d3..09f3aa42ea 100644 --- a/src/storm/storage/dd/cudd/utility.h +++ b/src/storm/storage/dd/cudd/utility.h @@ -1,5 +1,9 @@ #pragma once +#include "storm-config.h" + +#ifdef STORM_HAVE_CUDD + #include // Include the C++-interface of CUDD. @@ -19,3 +23,4 @@ struct CuddPointerPairHash { } // namespace dd } // namespace storm +#endif \ No newline at end of file diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp index 3c25667020..6f2b5d8da5 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -1,24 +1,21 @@ #include "storm/storage/dd/sylvan/InternalSylvanAdd.h" #include "storm/adapters/RationalFunctionAdapter.h" - -#include "storm/storage/dd/DdManager.h" -#include "storm/storage/dd/sylvan/InternalSylvanDdManager.h" -#include "storm/storage/dd/sylvan/SylvanAddIterator.h" - -#include "storm/storage/BitVector.h" -#include "storm/storage/SparseMatrix.h" - #include "storm/exceptions/InvalidOperationException.h" #include "storm/exceptions/NotImplementedException.h" #include "storm/exceptions/NotSupportedException.h" +#include "storm/storage/BitVector.h" +#include "storm/storage/SparseMatrix.h" +#include "storm/storage/dd/DdManager.h" +#include "storm/storage/dd/sylvan/InternalSylvanDdManager.h" +#include "storm/storage/dd/sylvan/SylvanAddIterator.h" #include "storm/utility/constants.h" #include "storm/utility/macros.h" -#include "storm-config.h" - namespace storm { namespace dd { + +#ifdef STORM_HAVE_SYLVAN template InternalAdd::InternalAdd() : ddManager(nullptr), sylvanMtbdd() { // Intentionally left empty. @@ -43,13 +40,9 @@ ValueType InternalAdd::getValue(MTBDD const& node) { } else if (std::is_same::value) { STORM_LOG_ASSERT(mtbdd_gettype(node) == 0, "Expected an unsigned value."); return negated ? -mtbdd_getint64(node) : mtbdd_getint64(node); - } -#ifdef STORM_HAVE_CARL - else if (std::is_same::value) { + } else if (std::is_same::value) { STORM_LOG_ASSERT(false, "Non-specialized version of getValue() called for storm::RationalFunction value."); - } -#endif - else { + } else { STORM_LOG_ASSERT(false, "Illegal or unknown type in MTBDD."); } } @@ -67,7 +60,6 @@ storm::RationalNumber InternalAdd::getVal return negated ? -(*rationalNumber) : (*rationalNumber); } -#ifdef STORM_HAVE_CARL template<> storm::RationalFunction InternalAdd::getValue(MTBDD const& node) { STORM_LOG_ASSERT(mtbdd_isleaf(node), "Expected leaf, but got variable " << mtbdd_getvar(node) << "."); @@ -82,7 +74,6 @@ storm::RationalFunction InternalAdd::ge return negated ? -(*rationalFunction) : (*rationalFunction); } -#endif template bool InternalAdd::operator==(InternalAdd const& other) const { @@ -105,13 +96,11 @@ InternalAdd InternalAdd(ddManager, this->sylvanMtbdd.PlusRN(other.sylvanMtbdd)); } -#ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::operator+( InternalAdd const& other) const { return InternalAdd(ddManager, this->sylvanMtbdd.PlusRF(other.sylvanMtbdd)); } -#endif template InternalAdd& InternalAdd::operator+=(InternalAdd const& other) { @@ -126,14 +115,12 @@ InternalAdd& InternalAdd InternalAdd& InternalAdd::operator+=( InternalAdd const& other) { this->sylvanMtbdd = this->sylvanMtbdd.PlusRF(other.sylvanMtbdd); return *this; } -#endif template InternalAdd InternalAdd::operator*(InternalAdd const& other) const { @@ -146,13 +133,11 @@ InternalAdd InternalAdd(ddManager, this->sylvanMtbdd.TimesRN(other.sylvanMtbdd)); } -#ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::operator*( InternalAdd const& other) const { return InternalAdd(ddManager, this->sylvanMtbdd.TimesRF(other.sylvanMtbdd)); } -#endif template InternalAdd& InternalAdd::operator*=(InternalAdd const& other) { @@ -167,14 +152,12 @@ InternalAdd& InternalAdd InternalAdd& InternalAdd::operator*=( InternalAdd const& other) { this->sylvanMtbdd = this->sylvanMtbdd.TimesRF(other.sylvanMtbdd); return *this; } -#endif template InternalAdd InternalAdd::operator-(InternalAdd const& other) const { @@ -187,13 +170,11 @@ InternalAdd InternalAdd(ddManager, this->sylvanMtbdd.MinusRN(other.sylvanMtbdd)); } -#ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::operator-( InternalAdd const& other) const { return InternalAdd(ddManager, this->sylvanMtbdd.MinusRF(other.sylvanMtbdd)); } -#endif template InternalAdd& InternalAdd::operator-=(InternalAdd const& other) { @@ -208,14 +189,12 @@ InternalAdd& InternalAdd InternalAdd& InternalAdd::operator-=( InternalAdd const& other) { this->sylvanMtbdd = this->sylvanMtbdd.MinusRF(other.sylvanMtbdd); return *this; } -#endif template InternalAdd InternalAdd::operator/(InternalAdd const& other) const { @@ -228,13 +207,11 @@ InternalAdd InternalAdd(ddManager, this->sylvanMtbdd.DivideRN(other.sylvanMtbdd)); } -#ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::operator/( InternalAdd const& other) const { return InternalAdd(ddManager, this->sylvanMtbdd.DivideRF(other.sylvanMtbdd)); } -#endif template InternalAdd& InternalAdd::operator/=(InternalAdd const& other) { @@ -249,14 +226,12 @@ InternalAdd& InternalAdd InternalAdd& InternalAdd::operator/=( InternalAdd const& other) { this->sylvanMtbdd = this->sylvanMtbdd.DivideRF(other.sylvanMtbdd); return *this; } -#endif template InternalBdd InternalAdd::equals(InternalAdd const& other) const { @@ -268,13 +243,11 @@ InternalBdd InternalAdd:: return InternalBdd(ddManager, this->sylvanMtbdd.EqualsRN(other.sylvanMtbdd)); } -#ifdef STORM_HAVE_CARL template<> InternalBdd InternalAdd::equals( InternalAdd const& other) const { return InternalBdd(ddManager, this->sylvanMtbdd.EqualsRF(other.sylvanMtbdd)); } -#endif template InternalBdd InternalAdd::notEquals(InternalAdd const& other) const { @@ -291,13 +264,11 @@ InternalBdd InternalAdd:: return InternalBdd(ddManager, this->sylvanMtbdd.LessRN(other.sylvanMtbdd)); } -#ifdef STORM_HAVE_CARL template<> InternalBdd InternalAdd::less( InternalAdd const& other) const { return InternalBdd(ddManager, this->sylvanMtbdd.LessRF(other.sylvanMtbdd)); } -#endif template InternalBdd InternalAdd::lessOrEqual(InternalAdd const& other) const { @@ -310,13 +281,11 @@ InternalBdd InternalAdd:: return InternalBdd(ddManager, this->sylvanMtbdd.LessOrEqualRN(other.sylvanMtbdd)); } -#ifdef STORM_HAVE_CARL template<> InternalBdd InternalAdd::lessOrEqual( InternalAdd const& other) const { return InternalBdd(ddManager, this->sylvanMtbdd.LessOrEqualRF(other.sylvanMtbdd)); } -#endif template InternalBdd InternalAdd::greater(InternalAdd const& other) const { @@ -339,13 +308,11 @@ InternalAdd InternalAdd(ddManager, this->sylvanMtbdd.PowRN(other.sylvanMtbdd)); } -#ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::pow( InternalAdd const& other) const { return InternalAdd(ddManager, this->sylvanMtbdd.PowRF(other.sylvanMtbdd)); } -#endif template InternalAdd InternalAdd::mod(InternalAdd const& other) const { @@ -358,13 +325,11 @@ InternalAdd InternalAdd(ddManager, this->sylvanMtbdd.ModRN(other.sylvanMtbdd)); } -#ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::mod( InternalAdd const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Operation (mod) not supported by rational functions."); } -#endif template InternalAdd InternalAdd::logxy(InternalAdd const& other) const { @@ -377,13 +342,11 @@ InternalAdd InternalAdd InternalAdd InternalAdd::logxy( InternalAdd const&) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Operation (logxy) not supported by rational functions."); } -#endif template InternalAdd InternalAdd::floor() const { @@ -395,12 +358,10 @@ InternalAdd InternalAdd(ddManager, this->sylvanMtbdd.FloorRN()); } -#ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::floor() const { return InternalAdd(ddManager, this->sylvanMtbdd.FloorRF()); } -#endif template InternalAdd InternalAdd::ceil() const { @@ -412,24 +373,20 @@ InternalAdd InternalAdd(ddManager, this->sylvanMtbdd.CeilRN()); } -#ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::ceil() const { return InternalAdd(ddManager, this->sylvanMtbdd.CeilRF()); } -#endif template InternalAdd InternalAdd::sharpenKwekMehlhorn(size_t precision) const { return InternalAdd(ddManager, this->sylvanMtbdd.SharpenKwekMehlhorn(precision)); } -#ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::sharpenKwekMehlhorn(size_t /*precision*/) const { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported."); } -#endif template InternalAdd InternalAdd::minimum(InternalAdd const& other) const { @@ -442,13 +399,11 @@ InternalAdd InternalAdd(ddManager, this->sylvanMtbdd.MinRN(other.sylvanMtbdd)); } -#ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::minimum( InternalAdd const& other) const { return InternalAdd(ddManager, this->sylvanMtbdd.MinRF(other.sylvanMtbdd)); } -#endif template InternalAdd InternalAdd::maximum(InternalAdd const& other) const { @@ -461,13 +416,11 @@ InternalAdd InternalAdd(ddManager, this->sylvanMtbdd.MaxRN(other.sylvanMtbdd)); } -#ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::maximum( InternalAdd const& other) const { return InternalAdd(ddManager, this->sylvanMtbdd.MaxRF(other.sylvanMtbdd)); } -#endif template template @@ -490,13 +443,11 @@ InternalAdd InternalAdd(ddManager, this->sylvanMtbdd.ToRationalNumber()); } -#ifdef STORM_HAVE_CARL template<> template<> InternalAdd InternalAdd::toValueType() const { return InternalAdd(ddManager, this->sylvanMtbdd.ToDoubleRF()); } -#endif template InternalAdd InternalAdd::sumAbstract(InternalBdd const& cube) const { @@ -509,13 +460,11 @@ InternalAdd InternalAdd(ddManager, this->sylvanMtbdd.AbstractPlusRN(cube.sylvanBdd)); } -#ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::sumAbstract( InternalBdd const& cube) const { return InternalAdd(ddManager, this->sylvanMtbdd.AbstractPlusRF(cube.sylvanBdd)); } -#endif template InternalAdd InternalAdd::minAbstract(InternalBdd const& cube) const { @@ -538,13 +487,11 @@ InternalAdd InternalAdd(ddManager, this->sylvanMtbdd.AbstractMinRN(cube.sylvanBdd)); } -#ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::minAbstract( InternalBdd const& cube) const { return InternalAdd(ddManager, this->sylvanMtbdd.AbstractMinRF(cube.sylvanBdd)); } -#endif template InternalAdd InternalAdd::maxAbstract(InternalBdd const& cube) const { @@ -567,13 +514,11 @@ InternalAdd InternalAdd(ddManager, this->sylvanMtbdd.AbstractMaxRN(cube.sylvanBdd)); } -#ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::maxAbstract( InternalBdd const& cube) const { return InternalAdd(ddManager, this->sylvanMtbdd.AbstractMaxRF(cube.sylvanBdd)); } -#endif template bool InternalAdd::equalModuloPrecision(InternalAdd const& other, ValueType const& precision, @@ -585,7 +530,6 @@ bool InternalAdd::equalModuloPrecision(InternalAdd
bool InternalAdd::equalModuloPrecision(InternalAdd const& other, storm::RationalNumber const& precision, bool relative) const { @@ -605,7 +549,6 @@ bool InternalAdd::equalModuloPrecision( return this->sylvanMtbdd.EqualNormRF(other.sylvanMtbdd, precision); } } -#endif template InternalAdd InternalAdd::swapVariables(std::vector> const& from, @@ -644,7 +587,6 @@ InternalAdd InternalAdd::m return InternalAdd(ddManager, this->sylvanMtbdd.AndExists(otherMatrix.sylvanMtbdd, summationVariables.getSylvanBdd())); } -#ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::multiplyMatrix( InternalAdd const& otherMatrix, std::vector> const& summationDdVariables) const { @@ -656,7 +598,6 @@ InternalAdd InternalAdd(ddManager, this->sylvanMtbdd.AndExistsRF(otherMatrix.sylvanMtbdd, summationVariables.getSylvanBdd())); } -#endif template<> InternalAdd InternalAdd::multiplyMatrix( @@ -682,7 +623,6 @@ InternalAdd InternalAdd::m ddManager, this->sylvanMtbdd.AndExists(sylvan::Bdd(otherMatrix.getSylvanBdd().GetBDD()), summationVariables.getSylvanBdd())); } -#ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::multiplyMatrix( InternalBdd const& otherMatrix, std::vector> const& summationDdVariables) const { @@ -694,7 +634,6 @@ InternalAdd InternalAdd( ddManager, this->sylvanMtbdd.AndExistsRF(sylvan::Bdd(otherMatrix.getSylvanBdd().GetBDD()), summationVariables.getSylvanBdd())); } -#endif template<> InternalAdd InternalAdd::multiplyMatrix( @@ -718,12 +657,10 @@ InternalBdd InternalAdd:: return InternalBdd(ddManager, this->sylvanMtbdd.BddStrictThresholdRN(value)); } -#ifdef STORM_HAVE_CARL template<> InternalBdd InternalAdd::greater(storm::RationalFunction const& value) const { return InternalBdd(ddManager, this->sylvanMtbdd.BddStrictThresholdRF(value)); } -#endif template InternalBdd InternalAdd::greaterOrEqual(ValueType const& value) const { @@ -735,12 +672,10 @@ InternalBdd InternalAdd:: return InternalBdd(ddManager, this->sylvanMtbdd.BddThresholdRN(value)); } -#ifdef STORM_HAVE_CARL template<> InternalBdd InternalAdd::greaterOrEqual(storm::RationalFunction const& value) const { return InternalBdd(ddManager, this->sylvanMtbdd.BddThresholdRF(value)); } -#endif template InternalBdd InternalAdd::less(ValueType const& value) const { @@ -800,12 +735,10 @@ storm::RationalNumber InternalAdd::getMin return getValue(this->sylvanMtbdd.MinimumRN().GetMTBDD()); } -#ifdef STORM_HAVE_CARL template<> storm::RationalFunction InternalAdd::getMin() const { return getValue(this->sylvanMtbdd.MinimumRF().GetMTBDD()); } -#endif template ValueType InternalAdd::getMax() const { @@ -817,12 +750,10 @@ storm::RationalNumber InternalAdd::getMax return getValue(this->sylvanMtbdd.MaximumRN().GetMTBDD()); } -#ifdef STORM_HAVE_CARL template<> storm::RationalFunction InternalAdd::getMax() const { return getValue(this->sylvanMtbdd.MaximumRF().GetMTBDD()); } -#endif template ValueType InternalAdd::getValue() const { @@ -1398,13 +1329,551 @@ std::string InternalAdd::getStringId() const { return ss.str(); } +#else +template +InternalAdd::InternalAdd() { + 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."); +} + +template +bool InternalAdd::operator==(InternalAdd const& other) const { + 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."); +} + +template +bool InternalAdd::operator!=(InternalAdd const& other) const { + 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."); +} + +template +InternalAdd InternalAdd::operator+(InternalAdd const& other) const { + 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."); +} + +template +InternalAdd& InternalAdd::operator+=(InternalAdd const& other) { + 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."); +} + +template +InternalAdd InternalAdd::operator*(InternalAdd const& other) const { + 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."); +} + +template +InternalAdd& InternalAdd::operator*=(InternalAdd const& other) { + 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."); +} + +template +InternalAdd InternalAdd::operator-(InternalAdd const& other) const { + 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."); +} + +template +InternalAdd& InternalAdd::operator-=(InternalAdd const& other) { + 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."); +} + +template +InternalAdd InternalAdd::operator/(InternalAdd const& other) const { + 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."); +} + +template +InternalAdd& InternalAdd::operator/=(InternalAdd const& other) { + 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."); +} + +template +InternalBdd InternalAdd::equals(InternalAdd const& other) const { + 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."); +} + +template +InternalBdd InternalAdd::notEquals(InternalAdd const& other) const { + 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."); +} + +template +InternalBdd InternalAdd::less(InternalAdd const& other) const { + 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."); +} + +template +InternalBdd InternalAdd::lessOrEqual(InternalAdd const& other) const { + 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."); +} + +template +InternalBdd InternalAdd::greater(InternalAdd const& other) const { + 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."); +} + +template +InternalBdd InternalAdd::greaterOrEqual(InternalAdd const& other) const { + 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."); +} + +template +InternalAdd InternalAdd::pow(InternalAdd const& other) const { + 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."); +} + +template +InternalAdd InternalAdd::mod(InternalAdd const& other) const { + 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."); +} + +template +InternalAdd InternalAdd::logxy(InternalAdd const& other) const { + 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."); +} + +template +InternalAdd InternalAdd::floor() const { + 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."); +} + +template +InternalAdd InternalAdd::ceil() const { + 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."); +} + +template +InternalAdd InternalAdd::sharpenKwekMehlhorn(size_t precision) const { + 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."); +} + +template +InternalAdd InternalAdd::minimum(InternalAdd const& other) const { + 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."); +} + +template +InternalAdd InternalAdd::maximum(InternalAdd const& other) const { + 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."); +} + +template +template +InternalAdd InternalAdd::toValueType() const { + 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."); +} + +template<> +template<> +InternalAdd InternalAdd::toValueType() const { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot convert this ADD to the target type."); +} + +template<> +template<> +InternalAdd InternalAdd::toValueType() const { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot convert this ADD to the target type."); +} + +template<> +template<> +InternalAdd InternalAdd::toValueType() const { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot convert this ADD to the target type."); +} + +template +InternalAdd InternalAdd::sumAbstract(InternalBdd const& cube) const { + 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."); +} + +template +InternalAdd InternalAdd::minAbstract(InternalBdd const& cube) const { + 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."); +} + +template +InternalBdd InternalAdd::minAbstractRepresentative(InternalBdd const& cube) const { + 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."); +} + +template +InternalAdd InternalAdd::maxAbstract(InternalBdd const& cube) const { + 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."); +} + +template +InternalBdd InternalAdd::maxAbstractRepresentative(InternalBdd const& cube) const { + 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."); +} + +template +bool InternalAdd::equalModuloPrecision(InternalAdd const& other, ValueType const& precision, + bool relative) const { + 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."); +} + +template +InternalAdd InternalAdd::swapVariables(std::vector> const& from, + std::vector> const& to) const { + 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."); +} + +template +InternalAdd InternalAdd::permuteVariables(std::vector> const& from, + std::vector> const& to) const { + 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."); +} + +template +InternalAdd InternalAdd::multiplyMatrix( + InternalAdd const& otherMatrix, std::vector> const& summationDdVariables) const { + 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."); +} + +template +InternalAdd InternalAdd::multiplyMatrix( + InternalBdd const& otherMatrix, std::vector> const& summationDdVariables) const { + 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."); +} + +template +InternalBdd InternalAdd::greater(ValueType const& value) const { + 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."); +} + +template +InternalBdd InternalAdd::greaterOrEqual(ValueType const& value) const { + 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."); +} + +template +InternalBdd InternalAdd::less(ValueType const& value) const { + 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."); +} + +template +InternalBdd InternalAdd::lessOrEqual(ValueType const& value) const { + 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."); +} + +template +InternalBdd InternalAdd::notZero() const { + 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."); +} + +template +InternalAdd InternalAdd::constrain(InternalAdd const&) const { + 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."); +} + +template +InternalAdd InternalAdd::restrict(InternalAdd const&) const { + 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."); +} + +template +InternalBdd InternalAdd::getSupport() const { + 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."); +} + +template +uint_fast64_t InternalAdd::getNonZeroCount(uint_fast64_t numberOfDdVariables) const { + 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."); +} + +template +uint_fast64_t InternalAdd::getLeafCount() const { + 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."); +} + +template +uint_fast64_t InternalAdd::getNodeCount() const { + 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."); +} + +template +ValueType InternalAdd::getMin() const { + 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."); +} + +template +ValueType InternalAdd::getMax() const { + 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."); +} + +template +ValueType InternalAdd::getValue() const { + 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."); +} + +template +bool InternalAdd::isOne() const { + 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."); +} + +template +bool InternalAdd::isZero() const { + 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."); +} + +template +bool InternalAdd::isConstant() const { + 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."); +} + +template +uint_fast64_t InternalAdd::getIndex() const { + 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."); +} + +template +uint_fast64_t InternalAdd::getLevel() const { + 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."); +} + +template +void InternalAdd::exportToDot(std::string const& filename, std::vector const&, bool) const { + 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."); +} + +template +void InternalAdd::exportToText(std::string const& filename) const { + 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."); +} + +template +AddIterator InternalAdd::begin(DdManager const& fullDdManager, + InternalBdd const& variableCube, + uint_fast64_t numberOfDdVariables, + std::set const& metaVariables, + bool enumerateDontCareMetaVariables) const { + 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."); +} + +template +AddIterator InternalAdd::end(DdManager const& fullDdManager) const { + 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."); +} + +template +Odd InternalAdd::createOdd(std::vector const& ddVariableIndices) const { + 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."); +} + +template +InternalDdManager const& InternalAdd::getInternalDdManager() const { + 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."); +} + +template +void InternalAdd::composeWithExplicitVector(storm::dd::Odd const& odd, std::vector const& ddVariableIndices, + std::vector& targetVector, + std::function const& function) const { + 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."); +} + +template +void InternalAdd::composeWithExplicitVector(storm::dd::Odd const& odd, std::vector const& ddVariableIndices, + std::vector const& offsets, std::vector& targetVector, + std::function const& function) const { + 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."); +} + +template +void InternalAdd::forEach(Odd const& odd, std::vector const& ddVariableIndices, + std::function const& function) const { + 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."); +} + +template +std::vector InternalAdd::decodeGroupLabels(std::vector const& ddGroupVariableIndices, + storm::storage::BitVector const& ddLabelVariableIndices) const { + 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."); +} + +template +std::vector> InternalAdd::splitIntoGroups( + std::vector const& ddGroupVariableIndices) const { + 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."); +} + +template +std::vector, InternalAdd>> InternalAdd::splitIntoGroups( + InternalAdd vector, std::vector const& ddGroupVariableIndices) const { + 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."); +} + +template +std::vector>> InternalAdd::splitIntoGroups( + std::vector> const& vectors, std::vector const& ddGroupVariableIndices) const { + 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."); +} + +template +void InternalAdd::toMatrixComponents(std::vector const& rowGroupIndices, std::vector& rowIndications, + std::vector>& columnsAndValues, + Odd const& rowOdd, Odd const& columnOdd, std::vector const& ddRowVariableIndices, + std::vector const& ddColumnVariableIndices, bool writeValues) const { + 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."); +} + +template +InternalAdd InternalAdd::fromVector(InternalDdManager const* ddManager, + std::vector const& values, storm::dd::Odd const& odd, + std::vector const& ddVariableIndices) { + 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."); +} + +template +std::string InternalAdd::getStringId() const { + 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 + template class InternalAdd; template class InternalAdd; - template class InternalAdd; - -#ifdef STORM_HAVE_CARL template class InternalAdd; -#endif + } // namespace dd } // namespace storm diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h index 5786533df5..8c66ba28e6 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h @@ -1,21 +1,17 @@ -#ifndef STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANADD_H_ -#define STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANADD_H_ +#pragma once #include #include +#include "storm-config.h" +#include "storm/adapters/RationalFunctionForward.h" #include "storm/storage/dd/DdType.h" #include "storm/storage/dd/InternalAdd.h" #include "storm/storage/dd/Odd.h" - #include "storm/storage/dd/sylvan/InternalSylvanBdd.h" #include "storm/storage/dd/sylvan/SylvanAddIterator.h" - #include "storm/storage/expressions/Variable.h" -#include "storm-config.h" -#include "storm/adapters/RationalFunctionForward.h" - namespace storm { namespace storage { template @@ -46,6 +42,7 @@ class InternalAdd { friend class AddIterator; friend class InternalBdd; +#ifdef STORM_HAVE_SYLVAN /*! * Creates an ADD that encapsulates the given Sylvan MTBDD. * @@ -53,6 +50,7 @@ class InternalAdd { * @param sylvanMtbdd The sylvan MTBDD to store. */ InternalAdd(InternalDdManager const* ddManager, sylvan::Mtbdd const& sylvanMtbdd); +#endif // Instantiate all copy/move constructors/assignments with the default implementation. InternalAdd(); @@ -662,6 +660,7 @@ class InternalAdd { InternalDdManager const& getInternalDdManager() const; +#ifdef STORM_HAVE_SYLVAN /*! * Retrieves the underlying sylvan MTBDD. * @@ -675,10 +674,12 @@ class InternalAdd { * @return The value of the leaf. */ static ValueType getValue(MTBDD const& node); +#endif std::string getStringId() const; private: +#ifdef STORM_HAVE_SYLVAN /*! * Recursively builds the ODD from an ADD. * @@ -834,22 +835,19 @@ class InternalAdd { */ static MTBDD getLeaf(storm::RationalNumber const& value); -#ifdef STORM_HAVE_CARL /*! * Retrieves the sylvan representation of the given storm::Rat�onalFunction. * * @return The sylvan node for the given value. */ static MTBDD getLeaf(storm::RationalFunction const& value); -#endif // The manager responsible for this MTBDD. InternalDdManager const* ddManager; // The underlying sylvan MTBDD. sylvan::Mtbdd sylvanMtbdd; +#endif }; } // namespace dd } // namespace storm - -#endif /* STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANADD_H_ */ diff --git a/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp b/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp index 7571eb672b..e2f4d06f29 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp @@ -2,22 +2,20 @@ #include +#include "storm/adapters/RationalFunctionAdapter.h" +#include "storm/exceptions/InvalidOperationException.h" +#include "storm/exceptions/NotSupportedException.h" +#include "storm/storage/BitVector.h" +#include "storm/storage/PairHash.h" #include "storm/storage/dd/sylvan/InternalSylvanAdd.h" #include "storm/storage/dd/sylvan/InternalSylvanDdManager.h" #include "storm/storage/dd/sylvan/SylvanAddIterator.h" - -#include "storm/storage/BitVector.h" -#include "storm/storage/PairHash.h" - -#include "storm/exceptions/InvalidOperationException.h" -#include "storm/exceptions/NotSupportedException.h" #include "storm/utility/macros.h" -#include "storm-config.h" -#include "storm/adapters/RationalFunctionAdapter.h" - namespace storm { namespace dd { + +#ifdef STORM_HAVE_SYLVAN InternalBdd::InternalBdd() : ddManager(nullptr), sylvanBdd() { // Intentionally left empty. } @@ -279,15 +277,11 @@ InternalAdd InternalBdd::toAdd() cons return InternalAdd(ddManager, this->sylvanBdd.toDoubleMtbdd()); } else if (std::is_same::value) { return InternalAdd(ddManager, this->sylvanBdd.toInt64Mtbdd()); - } -#ifdef STORM_HAVE_CARL - else if (std::is_same::value) { + } else if (std::is_same::value) { return InternalAdd(ddManager, this->sylvanBdd.toStormRationalNumberMtbdd()); } else if (std::is_same::value) { return InternalAdd(ddManager, this->sylvanBdd.toStormRationalFunctionMtbdd()); - } -#endif - else { + } else { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Illegal ADD type."); } } @@ -620,6 +614,275 @@ storm::expressions::Variable InternalBdd::toExpressionRec( // Return the variable for this node. return newNodeVariable; } +#else +InternalBdd::InternalBdd() { + 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."); +} + +InternalBdd InternalBdd::fromVector(InternalDdManager const* ddManager, Odd const& odd, + std::vector const& sortedDdVariableIndices, + std::function const& filter) { + 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."); +} + +bool InternalBdd::operator==(InternalBdd const& other) const { + 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."); +} + +bool InternalBdd::operator!=(InternalBdd const& other) const { + 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."); +} + +InternalBdd InternalBdd::relationalProduct(InternalBdd const& relation, + std::vector> const&, + std::vector> const&) const { + 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."); +} + +InternalBdd InternalBdd::inverseRelationalProduct(InternalBdd const& relation, + std::vector> const&, + std::vector> const&) const { + 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."); +} + +InternalBdd InternalBdd::inverseRelationalProductWithExtendedRelation( + InternalBdd const& relation, std::vector> const& rowVariables, + std::vector> const& columnVariables) const { + 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."); +} + +InternalBdd InternalBdd::ite(InternalBdd const& thenDd, InternalBdd const& elseDd) const { + 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."); +} + +template +InternalAdd InternalBdd::ite(InternalAdd const& thenAdd, + InternalAdd const& elseAdd) const { + 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."); +} + +InternalBdd InternalBdd::operator||(InternalBdd const& other) const { + 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."); +} + +InternalBdd& InternalBdd::operator|=(InternalBdd const& other) { + 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."); +} + +InternalBdd InternalBdd::operator&&(InternalBdd const& other) const { + 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."); +} + +InternalBdd& InternalBdd::operator&=(InternalBdd const& other) { + 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."); +} + +InternalBdd InternalBdd::iff(InternalBdd const& other) const { + 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."); +} + +InternalBdd InternalBdd::exclusiveOr(InternalBdd const& other) const { + 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."); +} + +InternalBdd InternalBdd::implies(InternalBdd const& other) const { + 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."); +} + +InternalBdd InternalBdd::operator!() const { + 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."); +} + +InternalBdd& InternalBdd::complement() { + 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."); +} + +InternalBdd InternalBdd::existsAbstract(InternalBdd const& cube) const { + 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."); +} + +InternalBdd InternalBdd::existsAbstractRepresentative(InternalBdd const& cube) const { + 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."); +} + +InternalBdd InternalBdd::universalAbstract(InternalBdd const& cube) const { + 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."); +} + +InternalBdd InternalBdd::andExists(InternalBdd const& other, InternalBdd const& cube) const { + 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."); +} + +InternalBdd InternalBdd::constrain(InternalBdd const& constraint) const { + 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."); +} + +InternalBdd InternalBdd::restrict(InternalBdd const& constraint) const { + 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."); +} + +InternalBdd InternalBdd::swapVariables(std::vector> const& from, + std::vector> const& to) const { + 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."); +} + +InternalBdd InternalBdd::getSupport() const { + 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."); +} + +uint_fast64_t InternalBdd::getNonZeroCount(uint_fast64_t numberOfDdVariables) const { + 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."); +} + +uint_fast64_t InternalBdd::getLeafCount() const { + 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."); +} + +uint_fast64_t InternalBdd::getNodeCount() const { + 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."); +} + +bool InternalBdd::isOne() const { + 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."); +} + +bool InternalBdd::isZero() const { + 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."); +} + +uint_fast64_t InternalBdd::getIndex() const { + 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."); +} + +uint_fast64_t InternalBdd::getLevel() const { + 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."); +} + +void InternalBdd::exportToDot(std::string const& filename, std::vector const&, bool) const { + 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."); +} + +void InternalBdd::exportToText(std::string const& filename) const { + 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."); +} + +template +InternalAdd InternalBdd::toAdd() const { + 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."); +} + +storm::storage::BitVector InternalBdd::toVector(storm::dd::Odd const& rowOdd, std::vector const& ddVariableIndices) const { + 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."); +} + +Odd InternalBdd::createOdd(std::vector const& ddVariableIndices) const { + 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."); +} + +template +void InternalBdd::filterExplicitVector(Odd const& odd, std::vector const& ddVariableIndices, + std::vector const& sourceValues, std::vector& targetValues) const { + 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."); +} + +void InternalBdd::filterExplicitVector(Odd const& odd, std::vector const& ddVariableIndices, + storm::storage::BitVector const& sourceValues, storm::storage::BitVector& targetValues) const { + 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."); +} + +std::vector> InternalBdd::splitIntoGroups(std::vector const& ddGroupVariableIndices) const { + 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."); +} + +std::pair, std::unordered_map> +InternalBdd::toExpression(storm::expressions::ExpressionManager& manager) const { + 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 template InternalAdd InternalBdd::toAdd() const; template InternalAdd InternalBdd::toAdd() const; @@ -646,4 +909,4 @@ template InternalAdd InternalBdd InternalBdd::ite( InternalAdd const& thenAdd, InternalAdd const& elseAdd) const; } // namespace dd -} // namespace storm +} // namespace storm \ No newline at end of file diff --git a/src/storm/storage/dd/sylvan/InternalSylvanBdd.h b/src/storm/storage/dd/sylvan/InternalSylvanBdd.h index 27733e2b4e..42f1d8b3d1 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanBdd.h +++ b/src/storm/storage/dd/sylvan/InternalSylvanBdd.h @@ -1,19 +1,18 @@ -#ifndef STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANBDD_H_ -#define STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANBDD_H_ +#pragma once #include #include #include #include -#include "storm/storage/expressions/Expression.h" -#include "storm/storage/expressions/ExpressionManager.h" - +#include "storm-config.h" +#include "storm/adapters/sylvan.h" +#include "storm/exceptions/MissingLibraryException.h" #include "storm/storage/dd/DdType.h" #include "storm/storage/dd/InternalAdd.h" #include "storm/storage/dd/InternalBdd.h" - -#include "storm/adapters/sylvan.h" +#include "storm/storage/expressions/Expression.h" +#include "storm/storage/expressions/ExpressionManager.h" namespace storm { namespace storage { @@ -32,7 +31,9 @@ class InternalBdd { template friend class InternalAdd; +#ifdef STORM_HAVE_SYLVAN InternalBdd(InternalDdManager const* ddManager, sylvan::Bdd const& sylvanBdd); +#endif // Instantiate all copy/move constructors/assignments with the default implementation. InternalBdd(); @@ -402,6 +403,7 @@ class InternalBdd { friend struct std::hash>; +#ifdef STORM_HAVE_SYLVAN /*! * Retrieves the sylvan BDD. * @@ -415,8 +417,10 @@ class InternalBdd { * @return The sylvan BDD. */ sylvan::Bdd const& getSylvanBdd() const; +#endif private: +#ifdef STORM_HAVE_SYLVAN /*! * Builds a BDD representing the values that make the given filter function evaluate to true. * @@ -534,6 +538,7 @@ class InternalBdd { // The sylvan BDD. sylvan::Bdd sylvanBdd; +#endif }; } // namespace dd } // namespace storm @@ -541,10 +546,16 @@ class InternalBdd { namespace std { template<> struct hash> { +#ifdef STORM_HAVE_SYLVAN std::size_t operator()(storm::dd::InternalBdd const& key) const { return static_cast(key.sylvanBdd.GetBDD()); } +#else + std::size_t operator()(storm::dd::InternalBdd const&) const { + 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 }; } // namespace std - -#endif /* STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANBDD_H_ */ diff --git a/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp b/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp index dcd24495b8..ba63c72f4c 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp @@ -3,22 +3,19 @@ #include #include -#include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/SylvanSettings.h" - +#include "storm/adapters/RationalFunctionAdapter.h" +#include "storm/adapters/sylvan.h" #include "storm/exceptions/InvalidSettingsException.h" #include "storm/exceptions/NotSupportedException.h" +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/SylvanSettings.h" #include "storm/utility/constants.h" #include "storm/utility/macros.h" -#include "storm/adapters/RationalFunctionAdapter.h" -#include "storm/adapters/sylvan.h" - -#include "storm-config.h" - namespace storm { namespace dd { +#ifdef STORM_HAVE_SYLVAN #if defined(__clang__) #pragma clang diagnostic push #pragma clang diagnostic ignored "-Wzero-length-array" @@ -122,13 +119,11 @@ InternalAdd InternalDdManager(this, sylvan::Mtbdd::stormRationalNumberTerminal(storm::utility::one())); } -#ifdef STORM_HAVE_CARL template<> InternalAdd InternalDdManager::getAddOne() const { return InternalAdd(this, sylvan::Mtbdd::stormRationalFunctionTerminal(storm::utility::one())); } -#endif InternalBdd InternalDdManager::getBddZero() const { return InternalBdd(this, sylvan::Bdd::bddZero()); @@ -176,13 +171,11 @@ InternalAdd InternalDdManager(this, sylvan::Mtbdd::stormRationalNumberTerminal(storm::utility::zero())); } -#ifdef STORM_HAVE_CARL template<> InternalAdd InternalDdManager::getAddZero() const { return InternalAdd(this, sylvan::Mtbdd::stormRationalFunctionTerminal(storm::utility::zero())); } -#endif template InternalAdd InternalDdManager::getAddUndefined() const { @@ -204,12 +197,10 @@ InternalAdd InternalDdManager(this, sylvan::Mtbdd::stormRationalNumberTerminal(value)); } -#ifdef STORM_HAVE_CARL template<> InternalAdd InternalDdManager::getConstant(storm::RationalFunction const& value) const { return InternalAdd(this, sylvan::Mtbdd::stormRationalFunctionTerminal(value)); } -#endif std::vector> InternalDdManager::createDdVariables(uint64_t numberOfLayers, boost::optional const& position) { @@ -266,14 +257,131 @@ void InternalDdManager::execute(std::function const& f) uint_fast64_t InternalDdManager::getNumberOfDdVariables() const { return nextFreeVariableIndex; } +#else +InternalDdManager::InternalDdManager() { + 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."); +} + +InternalDdManager::~InternalDdManager() {} + +InternalBdd InternalDdManager::getBddOne() const { + 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."); +} + +template +InternalAdd InternalDdManager::getAddOne() const { + 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."); +} + +InternalBdd InternalDdManager::getBddZero() const { + 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."); +} + +InternalBdd InternalDdManager::getBddEncodingLessOrEqualThan(uint64_t bound, InternalBdd const& cube, + uint64_t numberOfDdVariables) const { + 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."); +} +template +InternalAdd InternalDdManager::getAddZero() const { + 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."); +} + +template +InternalAdd InternalDdManager::getAddUndefined() const { + 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."); +} + +template +InternalAdd InternalDdManager::getConstant(ValueType const& value) const { + 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."); +} + +std::vector> InternalDdManager::createDdVariables(uint64_t numberOfLayers, + boost::optional const& position) { + 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."); +} + +bool InternalDdManager::supportsOrderedInsertion() const { + 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."); +} + +void InternalDdManager::allowDynamicReordering(bool) { + 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."); +} + +bool InternalDdManager::isDynamicReorderingAllowed() const { + 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."); +} + +void InternalDdManager::triggerReordering() { + 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."); +} + +void InternalDdManager::debugCheck() const { + 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."); +} + +void InternalDdManager::execute(std::function const& f) const { + 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."); +} + +uint_fast64_t InternalDdManager::getNumberOfDdVariables() const { + 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 + +#ifndef STORM_HAVE_SYLVAN +// There is already an explicit template instantiations if Sylvan is available +template InternalAdd InternalDdManager::getAddOne() const; +template InternalAdd InternalDdManager::getAddOne() const; +template InternalAdd InternalDdManager::getAddOne() const; +template InternalAdd InternalDdManager::getAddOne() const; +template InternalAdd InternalDdManager::getAddZero() const; +template InternalAdd InternalDdManager::getAddZero() const; +template InternalAdd InternalDdManager::getAddZero() const; +template InternalAdd InternalDdManager::getAddZero() const; +template InternalAdd InternalDdManager::getConstant(double const& value) const; +template InternalAdd InternalDdManager::getConstant(uint_fast64_t const& value) const; +template InternalAdd InternalDdManager::getConstant(storm::RationalNumber const& value) const; +template InternalAdd InternalDdManager::getConstant(storm::RationalFunction const& value) const; +#endif template InternalAdd InternalDdManager::getAddUndefined() const; template InternalAdd InternalDdManager::getAddUndefined() const; - template InternalAdd InternalDdManager::getAddUndefined() const; - -#ifdef STORM_HAVE_CARL template InternalAdd InternalDdManager::getAddUndefined() const; -#endif + } // namespace dd } // namespace storm diff --git a/src/storm/storage/dd/sylvan/InternalSylvanDdManager.h b/src/storm/storage/dd/sylvan/InternalSylvanDdManager.h index b2d0fed472..9c87306196 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanDdManager.h +++ b/src/storm/storage/dd/sylvan/InternalSylvanDdManager.h @@ -1,17 +1,14 @@ -#ifndef STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANDDMANAGER_H_ -#define STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANDDMANAGER_H_ +#pragma once #include +#include "storm-config.h" +#include "storm/adapters/RationalFunctionForward.h" #include "storm/storage/dd/DdType.h" #include "storm/storage/dd/InternalDdManager.h" - #include "storm/storage/dd/sylvan/InternalSylvanAdd.h" #include "storm/storage/dd/sylvan/InternalSylvanBdd.h" -#include "storm-config.h" -#include "storm/adapters/RationalFunctionForward.h" - namespace storm { namespace dd { template @@ -150,6 +147,8 @@ class InternalDdManager { uint_fast64_t getNumberOfDdVariables() const; private: +#ifdef STORM_HAVE_SYLVAN + // Helper function to create the BDD whose encodings are below a given bound. BDD getBddEncodingLessOrEqualThanRec(uint64_t minimalValue, uint64_t maximalValue, uint64_t bound, BDD cube, uint64_t remainingDdVariables) const; @@ -165,41 +164,8 @@ class InternalDdManager { // The index of the next free variable index. This needs to be shared across all instances since the sylvan // manager is implicitly 'global'. static uint_fast64_t nextFreeVariableIndex; -}; - -template<> -InternalAdd InternalDdManager::getAddOne() const; - -template<> -InternalAdd InternalDdManager::getAddOne() const; - -#ifdef STORM_HAVE_CARL -template<> -InternalAdd InternalDdManager::getAddOne() const; #endif +}; -template<> -InternalAdd InternalDdManager::getAddZero() const; - -template<> -InternalAdd InternalDdManager::getAddZero() const; - -#ifdef STORM_HAVE_CARL -template<> -InternalAdd InternalDdManager::getAddZero() const; -#endif - -template<> -InternalAdd InternalDdManager::getConstant(double const& value) const; - -template<> -InternalAdd InternalDdManager::getConstant(uint_fast64_t const& value) const; - -#ifdef STORM_HAVE_CARL -template<> -InternalAdd InternalDdManager::getConstant(storm::RationalFunction const& value) const; -#endif } // namespace dd } // namespace storm - -#endif /* STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANDDMANAGER_H_ */ diff --git a/src/storm/storage/dd/sylvan/SylvanAddIterator.cpp b/src/storm/storage/dd/sylvan/SylvanAddIterator.cpp index 2350ab658a..78d3ee0cd2 100644 --- a/src/storm/storage/dd/sylvan/SylvanAddIterator.cpp +++ b/src/storm/storage/dd/sylvan/SylvanAddIterator.cpp @@ -1,19 +1,18 @@ #include "storm/storage/dd/sylvan/SylvanAddIterator.h" -#include "storm/storage/dd/sylvan/InternalSylvanAdd.h" +#include +#include "storm/adapters/RationalFunctionAdapter.h" +#include "storm/exceptions/NotImplementedException.h" #include "storm/storage/dd/DdManager.h" +#include "storm/storage/dd/sylvan/InternalSylvanAdd.h" #include "storm/storage/expressions/ExpressionManager.h" - -#include "storm/exceptions/NotImplementedException.h" #include "storm/utility/macros.h" -#include - -#include "storm/adapters/RationalFunctionAdapter.h" - namespace storm { namespace dd { + +#ifdef STORM_HAVE_SYLVAN template AddIterator::AddIterator() { // Intentionally left empty. @@ -207,14 +206,46 @@ void AddIterator::treatNextInCube() { } } } +#else +template +AddIterator::AddIterator() { + 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."); +} + +template +AddIterator& AddIterator::operator++() { + 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."); +} + +template +bool AddIterator::operator==(AddIterator const& other) const { + 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."); +} + +template +bool AddIterator::operator!=(AddIterator const& other) const { + 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."); +} + +template +std::pair AddIterator::operator*() const { + 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 template class AddIterator; template class AddIterator; - template class AddIterator; - -#ifdef STORM_HAVE_CARL template class AddIterator; -#endif } // namespace dd } // namespace storm diff --git a/src/storm/storage/dd/sylvan/SylvanAddIterator.h b/src/storm/storage/dd/sylvan/SylvanAddIterator.h index 66a0f9b981..0aafd59b8b 100644 --- a/src/storm/storage/dd/sylvan/SylvanAddIterator.h +++ b/src/storm/storage/dd/sylvan/SylvanAddIterator.h @@ -1,13 +1,12 @@ -#ifndef STORM_STORAGE_DD_SYLVAN_SYLVANADDITERATOR_H_ -#define STORM_STORAGE_DD_SYLVAN_SYLVANADDITERATOR_H_ +#pragma once #include +#include "storm-config.h" +#include "storm/adapters/sylvan.h" #include "storm/storage/dd/AddIterator.h" #include "storm/storage/expressions/SimpleValuation.h" -#include "storm/adapters/sylvan.h" - namespace storm { namespace dd { // Forward-declare the DdManager class. @@ -65,6 +64,7 @@ class AddIterator { bool operator!=(AddIterator const& other) const; private: +#ifdef STORM_HAVE_SYLVAN /*! * Constructs a forward iterator using the given generator with the given set of relevant meta variables. * @@ -156,8 +156,7 @@ class AddIterator { // The current valuation of meta variables. storm::expressions::SimpleValuation currentValuation; +#endif }; } // namespace dd } // namespace storm - -#endif /* STORM_STORAGE_DD_SYLVAN_SYLVANADDITERATOR_H_ */ diff --git a/src/storm/storage/dd/sylvan/utility.h b/src/storm/storage/dd/sylvan/utility.h index 858a32de25..d24204cec6 100644 --- a/src/storm/storage/dd/sylvan/utility.h +++ b/src/storm/storage/dd/sylvan/utility.h @@ -1,9 +1,12 @@ #pragma once -#include "storm/adapters/sylvan.h" +#include "storm-config.h" +#ifdef STORM_HAVE_SYLVAN #include +#include "storm/adapters/sylvan.h" + namespace storm { namespace dd { @@ -29,3 +32,4 @@ struct SylvanMTBDDPairLess { } // namespace dd } // namespace storm +#endif \ No newline at end of file diff --git a/src/storm/storage/jani/LValue.cpp b/src/storm/storage/jani/LValue.cpp index 1a0cd0c31e..183f8dc543 100644 --- a/src/storm/storage/jani/LValue.cpp +++ b/src/storm/storage/jani/LValue.cpp @@ -86,7 +86,6 @@ LValue LValue::changeAssignmentVariables(std::map { protected: void SetUp() override { +#ifdef STORM_HAVE_SYLVAN auto const ¶m{TestWithParam::GetParam()}; auto dft{storm::dft::api::loadDFTGalileoFile(param.filepath)}; checker = std::make_shared(dft); +#else + GTEST_SKIP() << "Library Sylvan not available."; +#endif } std::shared_ptr checker; }; TEST_P(SftBddTest, bddHash) { +#ifdef STORM_HAVE_SYLVAN auto const ¶m{TestWithParam::GetParam()}; EXPECT_EQ(checker->getTransformator()->transformTopLevel().GetShaHash(), param.bddHash); +#else + GTEST_SKIP() << "Library Sylvan not available."; +#endif } TEST_P(SftBddTest, ProbabilityAtTimeOne) { @@ -178,6 +186,7 @@ static std::vector sftTestData{ INSTANTIATE_TEST_SUITE_P(SFTs, SftBddTest, testing::ValuesIn(sftTestData), [](auto const &info) { return info.param.testname; }); TEST(TestBdd, AndOrRelevantEvents) { +#ifdef STORM_HAVE_SYLVAN auto dft = storm::dft::api::loadDFTGalileoFile(STORM_TEST_RESOURCES_DIR "/dft/bdd/AndOrTest.dft"); auto manager = std::make_shared(); storm::dft::utility::RelevantEvents relevantEvents{"F", "F1", "F2", "x1"}; @@ -191,9 +200,13 @@ TEST(TestBdd, AndOrRelevantEvents) { EXPECT_EQ(result.at("F1").GetShaHash(), "c5cf2304417926961c3e1ce1d876fc2886ece1365fd946bfd3e1abd71401696d"); EXPECT_EQ(result.at("F2").GetShaHash(), "a4f129fa27c6cd32625b088811d4b12f8059ae0547ee035c083deed9ef9d2c59"); EXPECT_EQ(result.at("x1").GetShaHash(), "b0d991484e405a391b6d3d241fed9c00d4a2e5bf6f57300512394d819253893d"); +#else + GTEST_SKIP() << "Library Sylvan not available."; +#endif } TEST(TestBdd, AndOrRelevantEventsChecked) { +#ifdef STORM_HAVE_SYLVAN auto dft = storm::dft::api::loadDFTGalileoFile(STORM_TEST_RESOURCES_DIR "/dft/bdd/AndOrTest.dft"); auto manager{std::make_shared()}; storm::dft::utility::RelevantEvents relevantEvents{"F", "F1", "F2", "x1"}; @@ -209,17 +222,25 @@ TEST(TestBdd, AndOrRelevantEventsChecked) { EXPECT_NEAR(checker.getProbabilityAtTimebound(relevantEventsBdds["F2"], 1), 0.75, 1e-6); EXPECT_NEAR(checker.getProbabilityAtTimebound(relevantEventsBdds["x1"], 1), 0.5, 1e-6); +#else + GTEST_SKIP() << "Library Sylvan not available."; +#endif } TEST(TestBdd, AndOrFormulaFail) { +#ifdef STORM_HAVE_SYLVAN auto dft = storm::dft::api::loadDFTGalileoFile(STORM_TEST_RESOURCES_DIR "/dft/bdd/AndOrTest.dft"); auto const props{storm::api::extractFormulasFromProperties(storm::api::parseProperties("P=? [F < 1 !\"F2_failed\"];"))}; storm::dft::adapters::SFTBDDPropertyFormulaAdapter checker{dft, props}; STORM_SILENT_EXPECT_THROW(checker.check(), storm::exceptions::NotSupportedException); +#else + GTEST_SKIP() << "Library Sylvan not available."; +#endif } TEST(TestBdd, AndOrFormula) { +#ifdef STORM_HAVE_SYLVAN auto dft = storm::dft::api::loadDFTGalileoFile(STORM_TEST_RESOURCES_DIR "/dft/bdd/AndOrTest.dft"); auto const props{ storm::api::extractFormulasFromProperties(storm::api::parseProperties("P=? [F <= 1 \"failed\"];" @@ -276,6 +297,9 @@ TEST(TestBdd, AndOrFormula) { EXPECT_EQ(result[5].GetShaHash(), "a4f129fa27c6cd32625b088811d4b12f8059ae0547ee035c083deed9ef9d2c59"); EXPECT_EQ(result[6].GetShaHash(), "c5cf2304417926961c3e1ce1d876fc2886ece1365fd946bfd3e1abd71401696d"); EXPECT_EQ(result[7].GetShaHash(), "a4f129fa27c6cd32625b088811d4b12f8059ae0547ee035c083deed9ef9d2c59"); +#else + GTEST_SKIP() << "Library Sylvan not available."; +#endif } } // namespace diff --git a/src/test/storm-dft/bdd/TestBddModularizer.cpp b/src/test/storm-dft/bdd/TestBddModularizer.cpp index 79a3c250e3..1b81a73559 100644 --- a/src/test/storm-dft/bdd/TestBddModularizer.cpp +++ b/src/test/storm-dft/bdd/TestBddModularizer.cpp @@ -15,9 +15,13 @@ struct ModularizerTestData { class BddModularizerTest : public testing::TestWithParam { protected: void SetUp() override { +#ifdef STORM_HAVE_SYLVAN auto const ¶m{TestWithParam::GetParam()}; auto dft{storm::dft::api::loadDFTGalileoFile(param.filepath)}; checker = std::make_shared>(dft); +#else + GTEST_SKIP() << "Library Sylvan not available."; +#endif } std::shared_ptr> checker; diff --git a/src/test/storm-dft/bdd/TestBddVarOrdering.cpp b/src/test/storm-dft/bdd/TestBddVarOrdering.cpp index 96a158cab5..aa7720430a 100644 --- a/src/test/storm-dft/bdd/TestBddVarOrdering.cpp +++ b/src/test/storm-dft/bdd/TestBddVarOrdering.cpp @@ -8,6 +8,7 @@ namespace { TEST(TestBddVarOrdering, VariableOrdering) { +#ifdef STORM_HAVE_SYLVAN auto dft = storm::dft::api::loadDFTGalileoFile(STORM_TEST_RESOURCES_DIR "/dft/bdd/AndOrTest.dft"); auto manager{std::make_shared()}; auto transformator{std::make_shared>(dft, manager)}; @@ -36,9 +37,13 @@ TEST(TestBddVarOrdering, VariableOrdering) { EXPECT_EQ("x1", manager->getName(2)); EXPECT_EQ("x3", manager->getName(3)); EXPECT_EQ(7ul, bdd.NodeCount()); +#else + GTEST_SKIP() << "Library Sylvan not available."; +#endif } TEST(TestBddVarOrdering, OrderParser) { +#ifdef STORM_HAVE_SYLVAN auto dft = storm::dft::api::loadDFTGalileoFile(STORM_TEST_RESOURCES_DIR "/dft/bdd/AndOrTest.dft"); // Load variable ordering @@ -59,6 +64,9 @@ TEST(TestBddVarOrdering, OrderParser) { EXPECT_EQ("x1", manager->getName(2)); EXPECT_EQ("x3", manager->getName(3)); EXPECT_EQ(7ul, bdd.NodeCount()); +#else + GTEST_SKIP() << "Library Sylvan not available."; +#endif } } // namespace diff --git a/src/test/storm-dft/storage/BEDistributionTest.cpp b/src/test/storm-dft/storage/BEDistributionTest.cpp index 8760bb6b19..0c41191902 100644 --- a/src/test/storm-dft/storage/BEDistributionTest.cpp +++ b/src/test/storm-dft/storage/BEDistributionTest.cpp @@ -10,10 +10,12 @@ TEST(BEDistributionTest, ConstantFail) { auto dft = storm::dft::api::loadDFTGalileoFile(STORM_TEST_RESOURCES_DIR "/dft/be_fail.dft"); double timebound = 0.8; +#ifdef STORM_HAVE_SYLVAN // Perform BDD-based analysis on FT auto checker = std::make_shared(dft); double resultBDD = checker->getProbabilityAtTimebound(timebound); EXPECT_NEAR(resultBDD, 0.3296799540, 1e-10); +#endif // Perform Markovian analysis on FT auto dft2 = storm::dft::api::prepareForMarkovAnalysis(*dft); @@ -21,17 +23,19 @@ TEST(BEDistributionTest, ConstantFail) { std::string property = "Pmax=? [F<=" + std::to_string(timebound) + " \"failed\"]"; std::vector> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property)); double resultMC = boost::get(storm::dft::api::analyzeDFT(*dft2, properties)[0]); - EXPECT_NEAR(resultBDD, resultMC, 1e-10); + EXPECT_NEAR(resultMC, 0.3296799540, 1e-10); } TEST(BEDistributionTest, ConstantNonFail) { auto dft = storm::dft::api::loadDFTGalileoFile(STORM_TEST_RESOURCES_DIR "/dft/be_constant.dft"); double timebound = 0.8; +#ifdef STORM_HAVE_SYLVAN // Perform BDD-based analysis on FT auto checker = std::make_shared(dft); double resultBDD = checker->getProbabilityAtTimebound(timebound); EXPECT_NEAR(resultBDD, 0.9592377960, 1e-10); +#endif // Perform Markovian analysis on FT auto dft2 = storm::dft::api::prepareForMarkovAnalysis(*dft); @@ -39,17 +43,19 @@ TEST(BEDistributionTest, ConstantNonFail) { std::string property = "P=? [F<=" + std::to_string(timebound) + " \"failed\"]"; std::vector> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property)); double resultMC = boost::get(storm::dft::api::analyzeDFT(*dft2, properties)[0]); - EXPECT_NEAR(resultBDD, resultMC, 1e-10); + EXPECT_NEAR(resultMC, 0.9592377960, 1e-10); } TEST(BEDistributionTest, ConstantNonFail2) { auto dft = storm::dft::api::loadDFTGalileoFile(STORM_TEST_RESOURCES_DIR "/dft/be_nonfail2.dft"); double timebound = 0.8; +#ifdef STORM_HAVE_SYLVAN // Perform BDD-based analysis on FT auto checker = std::make_shared(dft); double resultBDD = checker->getProbabilityAtTimebound(timebound); EXPECT_EQ(resultBDD, 0); +#endif // Perform Markovian analysis on FT auto dft2 = storm::dft::api::prepareForMarkovAnalysis(*dft); @@ -57,17 +63,19 @@ TEST(BEDistributionTest, ConstantNonFail2) { std::string property = "P=? [F<=" + std::to_string(timebound) + " \"failed\"]"; std::vector> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property)); double resultMC = boost::get(storm::dft::api::analyzeDFT(*dft2, properties)[0]); - EXPECT_EQ(resultBDD, resultMC); + EXPECT_EQ(resultMC, 0); } TEST(BEDistributionTest, Probability) { auto dft = storm::dft::api::loadDFTGalileoFile(STORM_TEST_RESOURCES_DIR "/dft/be_probabilistic.dft"); double timebound = 0.8; +#ifdef STORM_HAVE_SYLVAN // Perform BDD-based analysis on FT auto checker = std::make_shared(dft); double resultBDD = checker->getProbabilityAtTimebound(timebound); EXPECT_NEAR(resultBDD, 0.1095403852, 1e-10); +#endif // Perform Markovian analysis on FT auto dft2 = storm::dft::api::prepareForMarkovAnalysis(*dft); @@ -75,17 +83,19 @@ TEST(BEDistributionTest, Probability) { std::string property = "Pmax=? [F<=" + std::to_string(timebound) + " \"failed\"]"; std::vector> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property)); double resultMC = boost::get(storm::dft::api::analyzeDFT(*dft2, properties)[0]); - EXPECT_NEAR(resultBDD, resultMC, 1e-10); + EXPECT_NEAR(resultMC, 0.1095403852, 1e-10); } TEST(BEDistributionTest, Exponential) { auto dft = storm::dft::api::loadDFTGalileoFile(STORM_TEST_RESOURCES_DIR "/dft/and.dft"); double timebound = 0.8; +#ifdef STORM_HAVE_SYLVAN // Perform BDD-based analysis on FT auto checker = std::make_shared(dft); double resultBDD = checker->getProbabilityAtTimebound(timebound); EXPECT_NEAR(resultBDD, 0.108688872, 1e-10); +#endif // Perform Markovian analysis on FT auto dft2 = storm::dft::api::prepareForMarkovAnalysis(*dft); @@ -93,17 +103,19 @@ TEST(BEDistributionTest, Exponential) { std::string property = "P=? [F<=" + std::to_string(timebound) + " \"failed\"]"; std::vector> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property)); double resultMC = boost::get(storm::dft::api::analyzeDFT(*dft2, properties)[0]); - EXPECT_NEAR(resultBDD, resultMC, 1e-10); + EXPECT_NEAR(resultMC, 0.108688872, 1e-10); } TEST(BEDistributionTest, Erlang) { auto dft = storm::dft::api::loadDFTGalileoFile(STORM_TEST_RESOURCES_DIR "/dft/be_erlang.dft"); double timebound = 0.8; +#ifdef STORM_HAVE_SYLVAN // Perform BDD-based analysis on FT auto checker = std::make_shared(dft); double resultBDD = checker->getProbabilityAtTimebound(timebound); EXPECT_NEAR(resultBDD, 0.4949009834, 1e-10); +#endif // Perform Markovian analysis on FT auto dft2 = storm::dft::api::prepareForMarkovAnalysis(*dft); @@ -111,10 +123,11 @@ TEST(BEDistributionTest, Erlang) { std::string property = "P=? [F<=" + std::to_string(timebound) + " \"failed\"]"; std::vector> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property)); double resultMC = boost::get(storm::dft::api::analyzeDFT(*dft2, properties)[0]); - EXPECT_NEAR(resultBDD, resultMC, 1e-10); + EXPECT_NEAR(resultMC, 0.4949009834, 1e-10); } TEST(BEDistributionTest, Weibull) { +#ifdef STORM_HAVE_SYLVAN auto dft = storm::dft::api::loadDFTGalileoFile(STORM_TEST_RESOURCES_DIR "/dft/be_weibull.dft"); double timebound = 2; @@ -122,9 +135,13 @@ TEST(BEDistributionTest, Weibull) { auto checker = std::make_shared(dft); double resultBDD = checker->getProbabilityAtTimebound(timebound); EXPECT_NEAR(resultBDD, 0.0382982486, 1e-10); +#else + GTEST_SKIP() << "Library Sylvan not available."; +#endif } TEST(BEDistributionTest, LogNormal) { +#ifdef STORM_HAVE_SYLVAN auto dft = storm::dft::api::loadDFTGalileoFile(STORM_TEST_RESOURCES_DIR "/dft/be_lognormal.dft"); double timebound = 0.8; @@ -132,6 +149,9 @@ TEST(BEDistributionTest, LogNormal) { auto checker = std::make_shared(dft); double resultBDD = checker->getProbabilityAtTimebound(timebound); EXPECT_NEAR(resultBDD, 0.2336675428, 1e-10); +#else + GTEST_SKIP() << "Library Sylvan not available."; +#endif } } // namespace diff --git a/src/test/storm-gamebased-ar/abstraction/GraphTest.cpp b/src/test/storm-gamebased-ar/abstraction/GraphTest.cpp index 3b29126e8b..99d5196115 100644 --- a/src/test/storm-gamebased-ar/abstraction/GraphTest.cpp +++ b/src/test/storm-gamebased-ar/abstraction/GraphTest.cpp @@ -22,11 +22,23 @@ class Cudd { public: + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_CUDD + GTEST_SKIP() << "Library CUDD not available."; +#endif + } + static const storm::dd::DdType DdType = storm::dd::DdType::CUDD; }; class Sylvan { public: + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_SYLVAN + GTEST_SKIP() << "Library Sylvan not available."; +#endif + } + static const storm::dd::DdType DdType = storm::dd::DdType::Sylvan; }; @@ -40,6 +52,7 @@ class GraphTestAR : public ::testing::Test { #ifndef STORM_HAVE_MSAT GTEST_SKIP() << "MathSAT not available."; #endif + TestType::checkLibraryAvailable(); } }; @@ -429,7 +442,6 @@ TYPED_TEST(GraphTestAR, SymbolicProb01StochasticGameWlan) { storm::dd::Add stateDistributionsUnderStrategies = (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd() * result.player2Strategy.get().template toAdd()) .sumAbstract(game.getColumnVariables()); - ; EXPECT_EQ(2831ull, stateDistributionsUnderStrategies.getNonZeroCount()); // Check that the number of distributions per state is one (or zero in the case where there are no prob0 states). diff --git a/src/test/storm-gamebased-ar/abstraction/PrismMenuGameTest.cpp b/src/test/storm-gamebased-ar/abstraction/PrismMenuGameTest.cpp index 4330f09e9e..06593ded63 100644 --- a/src/test/storm-gamebased-ar/abstraction/PrismMenuGameTest.cpp +++ b/src/test/storm-gamebased-ar/abstraction/PrismMenuGameTest.cpp @@ -15,11 +15,23 @@ class Cudd { public: + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_CUDD + GTEST_SKIP() << "Library CUDD not available."; +#endif + } + static const storm::dd::DdType DdType = storm::dd::DdType::CUDD; }; class Sylvan { public: + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_SYLVAN + GTEST_SKIP() << "Library Sylvan not available."; +#endif + } + static const storm::dd::DdType DdType = storm::dd::DdType::Sylvan; }; @@ -33,6 +45,7 @@ class PrismMenuGame : public ::testing::Test { #ifndef STORM_HAVE_MSAT GTEST_SKIP() << "MathSAT not available."; #endif + TestType::checkLibraryAvailable(); } }; diff --git a/src/test/storm-gamebased-ar/modelchecker/abstraction/GameBasedDtmcModelCheckerTest.cpp b/src/test/storm-gamebased-ar/modelchecker/abstraction/GameBasedDtmcModelCheckerTest.cpp index 358f2794f0..e0401c2ac5 100644 --- a/src/test/storm-gamebased-ar/modelchecker/abstraction/GameBasedDtmcModelCheckerTest.cpp +++ b/src/test/storm-gamebased-ar/modelchecker/abstraction/GameBasedDtmcModelCheckerTest.cpp @@ -17,11 +17,23 @@ class Cudd { public: + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_CUDD + GTEST_SKIP() << "Library CUDD not available."; +#endif + } + static const storm::dd::DdType DdType = storm::dd::DdType::CUDD; }; class Sylvan { public: + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_SYLVAN + GTEST_SKIP() << "Library Sylvan not available."; +#endif + } + static const storm::dd::DdType DdType = storm::dd::DdType::Sylvan; }; @@ -35,6 +47,7 @@ class GameBasedDtmcModelCheckerTest : public ::testing::Test { #ifndef STORM_HAVE_MSAT GTEST_SKIP() << "MathSAT not available."; #endif + TestType::checkLibraryAvailable(); } }; diff --git a/src/test/storm-gamebased-ar/modelchecker/abstraction/GameBasedMdpModelCheckerTest.cpp b/src/test/storm-gamebased-ar/modelchecker/abstraction/GameBasedMdpModelCheckerTest.cpp index fa17d4cb8a..00019208fe 100644 --- a/src/test/storm-gamebased-ar/modelchecker/abstraction/GameBasedMdpModelCheckerTest.cpp +++ b/src/test/storm-gamebased-ar/modelchecker/abstraction/GameBasedMdpModelCheckerTest.cpp @@ -15,11 +15,23 @@ class Cudd { public: + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_CUDD + GTEST_SKIP() << "Library CUDD not available."; +#endif + } + static const storm::dd::DdType DdType = storm::dd::DdType::CUDD; }; class Sylvan { public: + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_SYLVAN + GTEST_SKIP() << "Library Sylvan not available."; +#endif + } + static const storm::dd::DdType DdType = storm::dd::DdType::Sylvan; }; @@ -33,6 +45,7 @@ class GameBasedMdpModelCheckerTest : public ::testing::Test { #ifndef STORM_HAVE_MSAT GTEST_SKIP() << "MathSAT not available."; #endif + TestType::checkLibraryAvailable(); } }; typedef ::testing::Types TestingTypes; diff --git a/src/test/storm-pars/modelchecker/SymbolicParametricDtmcPrctlModelCheckerTest.cpp b/src/test/storm-pars/modelchecker/SymbolicParametricDtmcPrctlModelCheckerTest.cpp index 33a8973ab0..67db0a0d10 100644 --- a/src/test/storm-pars/modelchecker/SymbolicParametricDtmcPrctlModelCheckerTest.cpp +++ b/src/test/storm-pars/modelchecker/SymbolicParametricDtmcPrctlModelCheckerTest.cpp @@ -18,6 +18,7 @@ #include "storm/environment/solver/SolverEnvironment.h" TEST(SymbolicDtmcPrctlModelCheckerTest, Die_RationalFunction_Sylvan) { +#ifdef STORM_HAVE_SYLVAN storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/pdtmc/parametric_die.pm"); storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); @@ -83,4 +84,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die_RationalFunction_Sylvan) { EXPECT_EQ(storm::utility::convertNumber(quantitativeResult4.sum().evaluate(instantiation)), storm::utility::convertNumber(std::string("11/3"))); +#else + GTEST_SKIP() << "Library Sylvan not available."; +#endif } diff --git a/src/test/storm-pomdp/analysis/QualitativeAnalysisTest.cpp b/src/test/storm-pomdp/analysis/QualitativeAnalysisTest.cpp index ce21047485..a9f0124834 100644 --- a/src/test/storm-pomdp/analysis/QualitativeAnalysisTest.cpp +++ b/src/test/storm-pomdp/analysis/QualitativeAnalysisTest.cpp @@ -155,14 +155,19 @@ TEST_F(QualitativeAnalysis, Iterative_Maze) { } TEST_F(QualitativeAnalysis, SymbolicBelSup_Simple) { +#ifdef STORM_HAVE_SYLVAN symbolicbelsup_test(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "slippery=0.4", "Pmax=? [F \"goal\" ]", false); symbolicbelsup_test(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "slippery=0.0", "Pmax=? [F \"goal\" ]", false); symbolicbelsup_test(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "slippery=0.4", "Pmax=? [F \"goal\" ]", true); symbolicbelsup_test(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "slippery=0.0", "Pmax=? [F \"goal\" ]", true); +#else + GTEST_SKIP() << "Library Sylvan not available."; +#endif } TEST_F(QualitativeAnalysis, SymbolicBelSup_Maze) { +#ifdef STORM_HAVE_SYLVAN symbolicbelsup_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.4", "Pmax=? [F \"goal\" ]", false); symbolicbelsup_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.0", "Pmax=? [F \"goal\" ]", false); symbolicbelsup_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.4", "Pmax=? [!\"bad\" U \"goal\" ]", false); @@ -172,4 +177,7 @@ TEST_F(QualitativeAnalysis, SymbolicBelSup_Maze) { symbolicbelsup_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.0", "Pmax=? [F \"goal\" ]", true); symbolicbelsup_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.4", "Pmax=? [!\"bad\" U \"goal\" ]", true); symbolicbelsup_test(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "sl=0.0", "Pmax=? [!\"bad\" U \"goal\"]", true); +#else + GTEST_SKIP() << "Library Sylvan not available."; +#endif } diff --git a/src/test/storm/builder/DdJaniModelBuilderTest.cpp b/src/test/storm/builder/DdJaniModelBuilderTest.cpp index 80259ef428..d089a1e13e 100644 --- a/src/test/storm/builder/DdJaniModelBuilderTest.cpp +++ b/src/test/storm/builder/DdJaniModelBuilderTest.cpp @@ -19,18 +19,32 @@ namespace { class Cudd { public: + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_CUDD + GTEST_SKIP() << "Library CUDD not available."; +#endif + } + static const storm::dd::DdType DdType = storm::dd::DdType::CUDD; }; class Sylvan { public: + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_SYLVAN + GTEST_SKIP() << "Library Sylvan not available."; +#endif + } + static const storm::dd::DdType DdType = storm::dd::DdType::Sylvan; }; template class DdJaniModelBuilderTest : public ::testing::Test { public: - static const storm::dd::DdType DdType = TestType::DdType; + void SetUp() override { + TestType::checkLibraryAvailable(); + } storm::jani::Model getJaniModelFromPrism(std::string const& pathInTestResourcesDir, bool prismCompatability = false) { storm::storage::SymbolicModelDescription modelDescription = @@ -40,6 +54,8 @@ class DdJaniModelBuilderTest : public ::testing::Test { EXPECT_TRUE(unsupportedFeatures.empty()) << "Model '" << pathInTestResourcesDir << "' uses unsupported feature(s) " << unsupportedFeatures.toString(); return m; } + + static const storm::dd::DdType DdType = TestType::DdType; }; typedef ::testing::Types TestingTypes; diff --git a/src/test/storm/builder/DdPrismModelBuilderTest.cpp b/src/test/storm/builder/DdPrismModelBuilderTest.cpp index b201e5ad9e..6565c79b9b 100644 --- a/src/test/storm/builder/DdPrismModelBuilderTest.cpp +++ b/src/test/storm/builder/DdPrismModelBuilderTest.cpp @@ -15,17 +15,33 @@ class Cudd { public: + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_CUDD + GTEST_SKIP() << "Library CUDD not available."; +#endif + } + static const storm::dd::DdType DdType = storm::dd::DdType::CUDD; }; class Sylvan { public: + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_SYLVAN + GTEST_SKIP() << "Library Sylvan not available."; +#endif + } + static const storm::dd::DdType DdType = storm::dd::DdType::Sylvan; }; template class DdPrismModelBuilderTest : public ::testing::Test { public: + void SetUp() override { + TestType::checkLibraryAvailable(); + } + static const storm::dd::DdType DdType = TestType::DdType; }; diff --git a/src/test/storm/modelchecker/csl/CtmcCslModelCheckerTest.cpp b/src/test/storm/modelchecker/csl/CtmcCslModelCheckerTest.cpp index f152f11667..cc2133e25e 100644 --- a/src/test/storm/modelchecker/csl/CtmcCslModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/csl/CtmcCslModelCheckerTest.cpp @@ -121,6 +121,13 @@ class HybridCuddGmmxxGmresEnvironment { static const bool isExact = false; typedef double ValueType; typedef storm::models::symbolic::Ctmc ModelType; + + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_CUDD + GTEST_SKIP() << "Library CUDD not available."; +#endif + } + static storm::Environment createEnvironment() { storm::Environment env; env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx); @@ -137,6 +144,13 @@ class JaniHybridCuddGmmxxGmresEnvironment { static const bool isExact = false; typedef double ValueType; typedef storm::models::symbolic::Ctmc ModelType; + + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_CUDD + GTEST_SKIP() << "Library CUDD not available."; +#endif + } + static storm::Environment createEnvironment() { storm::Environment env; env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx); @@ -153,6 +167,13 @@ class HybridSylvanGmmxxGmresEnvironment { static const bool isExact = false; typedef double ValueType; typedef storm::models::symbolic::Ctmc ModelType; + + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_SYLVAN + GTEST_SKIP() << "Library Sylvan not available."; +#endif + } + static storm::Environment createEnvironment() { storm::Environment env; env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx); @@ -175,6 +196,9 @@ class CtmcCslModelCheckerTest : public ::testing::Test { #ifndef STORM_HAVE_Z3 GTEST_SKIP() << "Z3 not available."; #endif + if constexpr (TestType::engine == CtmcEngine::PrismHybrid || TestType::engine == CtmcEngine::JaniHybrid) { + TestType::checkLibraryAvailable(); + } } storm::Environment const& env() const { diff --git a/src/test/storm/modelchecker/csl/LraCtmcCslModelCheckerTest.cpp b/src/test/storm/modelchecker/csl/LraCtmcCslModelCheckerTest.cpp index f92558681a..329141ab6a 100644 --- a/src/test/storm/modelchecker/csl/LraCtmcCslModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/csl/LraCtmcCslModelCheckerTest.cpp @@ -80,6 +80,13 @@ class GBJaniHybridCuddGmmxxGmresEnvironment { static const bool isExact = false; typedef double ValueType; typedef storm::models::symbolic::Ctmc ModelType; + + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_CUDD + GTEST_SKIP() << "Library CUDD not available."; +#endif + } + static storm::Environment createEnvironment() { storm::Environment env; env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx); @@ -101,6 +108,13 @@ class GBJaniHybridSylvanGmmxxGmresEnvironment { static const bool isExact = false; typedef double ValueType; typedef storm::models::symbolic::Ctmc ModelType; + + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_SYLVAN + GTEST_SKIP() << "Library Sylvan not available."; +#endif + } + static storm::Environment createEnvironment() { storm::Environment env; env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx); @@ -246,6 +260,9 @@ class LraCtmcCslModelCheckerTest : public ::testing::Test { #ifndef STORM_HAVE_Z3 GTEST_SKIP() << "Z3 not available."; #endif + if constexpr (TestType::engine == CtmcEngine::JaniHybrid) { + TestType::checkLibraryAvailable(); + } } storm::Environment const& env() const { diff --git a/src/test/storm/modelchecker/csl/MarkovAutomatonCslModelCheckerTest.cpp b/src/test/storm/modelchecker/csl/MarkovAutomatonCslModelCheckerTest.cpp index 4220981ab1..4010abee25 100644 --- a/src/test/storm/modelchecker/csl/MarkovAutomatonCslModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/csl/MarkovAutomatonCslModelCheckerTest.cpp @@ -63,6 +63,13 @@ class JaniHybridDoubleValueIterationEnvironment { static const bool isExact = false; typedef double ValueType; typedef storm::models::symbolic::MarkovAutomaton ModelType; + + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_SYLVAN + GTEST_SKIP() << "Library Sylvan not available."; +#endif + } + static storm::Environment createEnvironment() { storm::Environment env; env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration, true); @@ -126,6 +133,9 @@ class MarkovAutomatonCslModelCheckerTest : public ::testing::Test { #ifndef STORM_HAVE_Z3 GTEST_SKIP() << "Z3 not available."; #endif + if constexpr (TestType::engine == MaEngine::JaniHybrid) { + TestType::checkLibraryAvailable(); + } } storm::Environment const& env() const { diff --git a/src/test/storm/modelchecker/multiobjective/SparseDtmcMultiDimensionalRewardUnfoldingTest.cpp b/src/test/storm/modelchecker/multiobjective/SparseDtmcMultiDimensionalRewardUnfoldingTest.cpp index c1f6f6483b..f8f21c98f9 100644 --- a/src/test/storm/modelchecker/multiobjective/SparseDtmcMultiDimensionalRewardUnfoldingTest.cpp +++ b/src/test/storm/modelchecker/multiobjective/SparseDtmcMultiDimensionalRewardUnfoldingTest.cpp @@ -35,7 +35,6 @@ TEST_F(SparseDtmcMultiDimensionalRewardUnfoldingTest, cost_bounded_die) { std::shared_ptr> dtmc = storm::api::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *dtmc->getInitialStates().begin(); - ; std::unique_ptr result; result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask(formulas[0], true)); @@ -70,7 +69,6 @@ TEST_F(SparseDtmcMultiDimensionalRewardUnfoldingTest, cost_bounded_leader) { std::shared_ptr> dtmc = storm::api::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *dtmc->getInitialStates().begin(); - ; std::unique_ptr result; result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask(formulas[0], true)); @@ -109,7 +107,6 @@ TEST_F(SparseDtmcMultiDimensionalRewardUnfoldingTest, cost_bounded_crowds) { std::shared_ptr> dtmc = storm::api::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *dtmc->getInitialStates().begin(); - ; std::unique_ptr result; result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask(formulas[0], true)); diff --git a/src/test/storm/modelchecker/multiobjective/SparseMdpCbMultiObjectiveModelCheckerTest.cpp b/src/test/storm/modelchecker/multiobjective/SparseMdpCbMultiObjectiveModelCheckerTest.cpp index 306364575c..5d43abb977 100644 --- a/src/test/storm/modelchecker/multiobjective/SparseMdpCbMultiObjectiveModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/multiobjective/SparseMdpCbMultiObjectiveModelCheckerTest.cpp @@ -39,7 +39,6 @@ TEST_F(SparseMdpCbMultiObjectiveModelCheckerTest, consensus) { std::shared_ptr> mdp = storm::api::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); - ; std::unique_ptr result; diff --git a/src/test/storm/modelchecker/multiobjective/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp b/src/test/storm/modelchecker/multiobjective/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp index 9f30f75837..c4fa8887ca 100644 --- a/src/test/storm/modelchecker/multiobjective/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp +++ b/src/test/storm/modelchecker/multiobjective/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp @@ -44,7 +44,6 @@ TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_one_dim_walk_sma std::shared_ptr> mdp = storm::api::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); - ; std::unique_ptr result; result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask(formulas[0], true)); @@ -92,7 +91,6 @@ TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_one_dim_walk_lar std::shared_ptr> mdp = storm::api::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); - ; std::unique_ptr result; @@ -130,7 +128,6 @@ TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_tiny_ec) { std::shared_ptr> mdp = storm::api::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); - ; std::unique_ptr result; @@ -187,7 +184,6 @@ TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_zeroconf_dl) { storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> mdp = storm::api::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); - ; std::unique_ptr result; @@ -219,7 +215,6 @@ TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_csma) { std::shared_ptr> mdp = storm::api::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); - ; std::unique_ptr result; @@ -252,7 +247,6 @@ TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_lower_bounds) { std::shared_ptr> mdp = storm::api::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); - ; std::unique_ptr result; @@ -316,7 +310,6 @@ TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, one_dim_walk_small) { std::shared_ptr> mdp = storm::api::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); - ; std::unique_ptr result; @@ -394,7 +387,6 @@ TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, one_dim_walk_large) { std::shared_ptr> mdp = storm::api::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); - ; std::unique_ptr result; @@ -437,7 +429,6 @@ TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, tiny_ec) { std::shared_ptr> mdp = storm::api::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); - ; std::unique_ptr result; @@ -504,7 +495,6 @@ TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, zeroconf_dl) { storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> mdp = storm::api::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); - ; std::unique_ptr result; @@ -535,7 +525,6 @@ TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, csma) { std::shared_ptr> mdp = storm::api::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); - ; std::unique_ptr result; @@ -572,7 +561,6 @@ TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, lower_bounds) { std::shared_ptr> mdp = storm::api::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); - ; std::unique_ptr result; diff --git a/src/test/storm/modelchecker/multiobjective/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp b/src/test/storm/modelchecker/multiobjective/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp index 5ebbbb751b..46a9a54c0a 100644 --- a/src/test/storm/modelchecker/multiobjective/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/multiobjective/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp @@ -38,7 +38,6 @@ TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, consensus) { storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> mdp = storm::api::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); - ; std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[0]->asMultiObjectiveFormula()); diff --git a/src/test/storm/modelchecker/prctl/dtmc/DtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/dtmc/DtmcPrctlModelCheckerTest.cpp index 1a2ed94839..ebaa32b922 100644 --- a/src/test/storm/modelchecker/prctl/dtmc/DtmcPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/prctl/dtmc/DtmcPrctlModelCheckerTest.cpp @@ -317,6 +317,13 @@ class HybridSylvanGmmxxGmresEnvironment { static const bool isExact = false; typedef double ValueType; typedef storm::models::symbolic::Dtmc ModelType; + + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_SYLVAN + GTEST_SKIP() << "Library Sylvan not available."; +#endif + } + static storm::Environment createEnvironment() { storm::Environment env; env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx); @@ -333,6 +340,13 @@ class HybridCuddNativeJacobiEnvironment { static const bool isExact = false; typedef double ValueType; typedef storm::models::symbolic::Dtmc ModelType; + + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_CUDD + GTEST_SKIP() << "Library CUDD not available."; +#endif + } + static storm::Environment createEnvironment() { storm::Environment env; env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native); @@ -349,6 +363,13 @@ class HybridCuddNativeSoundValueIterationEnvironment { static const bool isExact = false; typedef double ValueType; typedef storm::models::symbolic::Dtmc ModelType; + + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_CUDD + GTEST_SKIP() << "Library CUDD not available."; +#endif + } + static storm::Environment createEnvironment() { storm::Environment env; env.solver().setForceSoundness(true); @@ -366,6 +387,13 @@ class HybridSylvanNativeRationalSearchEnvironment { static const bool isExact = true; typedef storm::RationalNumber ValueType; typedef storm::models::symbolic::Dtmc ModelType; + + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_SYLVAN + GTEST_SKIP() << "Library Sylvan not available."; +#endif + } + static storm::Environment createEnvironment() { storm::Environment env; env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native); @@ -381,6 +409,13 @@ class DdSylvanNativePowerEnvironment { static const bool isExact = false; typedef double ValueType; typedef storm::models::symbolic::Dtmc ModelType; + + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_SYLVAN + GTEST_SKIP() << "Library Sylvan not available."; +#endif + } + static storm::Environment createEnvironment() { storm::Environment env; env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native); @@ -397,6 +432,13 @@ class JaniDdSylvanNativePowerEnvironment { static const bool isExact = false; typedef double ValueType; typedef storm::models::symbolic::Dtmc ModelType; + + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_SYLVAN + GTEST_SKIP() << "Library Sylvan not available."; +#endif + } + static storm::Environment createEnvironment() { storm::Environment env; env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native); @@ -413,6 +455,13 @@ class DdCuddNativeJacobiEnvironment { static const bool isExact = false; typedef double ValueType; typedef storm::models::symbolic::Dtmc ModelType; + + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_CUDD + GTEST_SKIP() << "Library CUDD not available."; +#endif + } + static storm::Environment createEnvironment() { storm::Environment env; env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native); @@ -429,6 +478,13 @@ class DdSylvanRationalSearchEnvironment { static const bool isExact = true; typedef storm::RationalNumber ValueType; typedef storm::models::symbolic::Dtmc ModelType; + + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_SYLVAN + GTEST_SKIP() << "Library Sylvan not available."; +#endif + } + static storm::Environment createEnvironment() { storm::Environment env; env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native); @@ -450,6 +506,9 @@ class DtmcPrctlModelCheckerTest : public ::testing::Test { #ifndef STORM_HAVE_Z3 GTEST_SKIP() << "Z3 not available."; #endif + if constexpr (TestType::engine == DtmcEngine::Hybrid || TestType::engine == DtmcEngine::PrismDd || TestType::engine == DtmcEngine::JaniDd) { + TestType::checkLibraryAvailable(); + } } storm::Environment const& env() const { diff --git a/src/test/storm/modelchecker/prctl/mdp/MdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/mdp/MdpPrctlModelCheckerTest.cpp index bb0fc28c74..4d276e4299 100644 --- a/src/test/storm/modelchecker/prctl/mdp/MdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/prctl/mdp/MdpPrctlModelCheckerTest.cpp @@ -277,6 +277,13 @@ class HybridCuddDoubleValueIterationEnvironment { static const bool isExact = false; typedef double ValueType; typedef storm::models::symbolic::Mdp ModelType; + + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_CUDD + GTEST_SKIP() << "Library CUDD not available."; +#endif + } + static storm::Environment createEnvironment() { storm::Environment env; env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); @@ -291,6 +298,13 @@ class HybridSylvanDoubleValueIterationEnvironment { static const bool isExact = false; typedef double ValueType; typedef storm::models::symbolic::Mdp ModelType; + + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_SYLVAN + GTEST_SKIP() << "Library Sylvan not available."; +#endif + } + static storm::Environment createEnvironment() { storm::Environment env; env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); @@ -305,6 +319,13 @@ class HybridCuddDoubleSoundValueIterationEnvironment { static const bool isExact = false; typedef double ValueType; typedef storm::models::symbolic::Mdp ModelType; + + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_CUDD + GTEST_SKIP() << "Library CUDD not available."; +#endif + } + static storm::Environment createEnvironment() { storm::Environment env; env.solver().setForceSoundness(true); @@ -321,6 +342,13 @@ class HybridCuddDoubleOptimisticValueIterationEnvironment { static const bool isExact = false; typedef double ValueType; typedef storm::models::symbolic::Mdp ModelType; + + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_CUDD + GTEST_SKIP() << "Library CUDD not available."; +#endif + } + static storm::Environment createEnvironment() { storm::Environment env; env.solver().setForceSoundness(true); @@ -337,6 +365,13 @@ class HybridSylvanRationalPolicyIterationEnvironment { static const bool isExact = true; typedef storm::RationalNumber ValueType; typedef storm::models::symbolic::Mdp ModelType; + + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_SYLVAN + GTEST_SKIP() << "Library Sylvan not available."; +#endif + } + static storm::Environment createEnvironment() { storm::Environment env; env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration); @@ -350,6 +385,13 @@ class DdCuddDoubleValueIterationEnvironment { static const bool isExact = false; typedef double ValueType; typedef storm::models::symbolic::Mdp ModelType; + + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_CUDD + GTEST_SKIP() << "Library CUDD not available."; +#endif + } + static storm::Environment createEnvironment() { storm::Environment env; env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); @@ -364,6 +406,13 @@ class JaniDdCuddDoubleValueIterationEnvironment { static const bool isExact = false; typedef double ValueType; typedef storm::models::symbolic::Mdp ModelType; + + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_CUDD + GTEST_SKIP() << "Library CUDD not available."; +#endif + } + static storm::Environment createEnvironment() { storm::Environment env; env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); @@ -378,6 +427,13 @@ class DdSylvanDoubleValueIterationEnvironment { static const bool isExact = false; typedef double ValueType; typedef storm::models::symbolic::Mdp ModelType; + + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_SYLVAN + GTEST_SKIP() << "Library Sylvan not available."; +#endif + } + static storm::Environment createEnvironment() { storm::Environment env; env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); @@ -392,6 +448,13 @@ class DdCuddDoublePolicyIterationEnvironment { static const bool isExact = false; typedef double ValueType; typedef storm::models::symbolic::Mdp ModelType; + + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_CUDD + GTEST_SKIP() << "Library CUDD not available."; +#endif + } + static storm::Environment createEnvironment() { storm::Environment env; env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration); @@ -406,6 +469,13 @@ class DdSylvanRationalRationalSearchEnvironment { static const bool isExact = true; typedef storm::RationalNumber ValueType; typedef storm::models::symbolic::Mdp ModelType; + + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_SYLVAN + GTEST_SKIP() << "Library Sylvan not available."; +#endif + } + static storm::Environment createEnvironment() { storm::Environment env; env.solver().minMax().setMethod(storm::solver::MinMaxMethod::RationalSearch); @@ -426,6 +496,9 @@ class MdpPrctlModelCheckerTest : public ::testing::Test { #ifndef STORM_HAVE_Z3 GTEST_SKIP() << "Z3 not available."; #endif + if constexpr (TestType::engine == MdpEngine::Hybrid || TestType::engine == MdpEngine::PrismDd || TestType::engine == MdpEngine::JaniDd) { + TestType::checkLibraryAvailable(); + } } storm::Environment const& env() const { diff --git a/src/test/storm/solver/FullySymbolicGameSolverTest.cpp b/src/test/storm/solver/FullySymbolicGameSolverTest.cpp index 5fd2c5bcbb..444e5b6264 100644 --- a/src/test/storm/solver/FullySymbolicGameSolverTest.cpp +++ b/src/test/storm/solver/FullySymbolicGameSolverTest.cpp @@ -10,17 +10,33 @@ class Cudd { public: + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_CUDD + GTEST_SKIP() << "Library CUDD not available."; +#endif + } + static const storm::dd::DdType DdType = storm::dd::DdType::CUDD; }; class Sylvan { public: + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_SYLVAN + GTEST_SKIP() << "Library Sylvan not available."; +#endif + } + static const storm::dd::DdType DdType = storm::dd::DdType::Sylvan; }; template class FullySymbolicGameSolverTest : public ::testing::Test { public: + void SetUp() override { + TestType::checkLibraryAvailable(); + } + static const storm::dd::DdType DdType = TestType::DdType; }; diff --git a/src/test/storm/storage/DdTest.cpp b/src/test/storm/storage/DdTest.cpp index 31fc58770f..6ed02434b0 100644 --- a/src/test/storm/storage/DdTest.cpp +++ b/src/test/storm/storage/DdTest.cpp @@ -7,23 +7,40 @@ #include "storm/storage/dd/Add.h" #include "storm/storage/dd/DdManager.h" #include "storm/storage/dd/DdMetaVariable.h" +#include "storm/storage/dd/DdType.h" #include "storm/storage/dd/Odd.h" #include "storm/storage/expressions/Expression.h" #include "storm/storage/expressions/ExpressionManager.h" class Cudd { public: + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_CUDD + GTEST_SKIP() << "Library CUDD not available."; +#endif + } + static const storm::dd::DdType DdType = storm::dd::DdType::CUDD; }; class Sylvan { public: + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_SYLVAN + GTEST_SKIP() << "Library Sylvan not available."; +#endif + } + static const storm::dd::DdType DdType = storm::dd::DdType::Sylvan; }; template class Dd : public ::testing::Test { public: + void SetUp() override { + TestType::checkLibraryAvailable(); + } + static const storm::dd::DdType DdType = TestType::DdType; }; diff --git a/src/test/storm/storage/SylvanDdTest.cpp b/src/test/storm/storage/SylvanDdTest.cpp index f276a28e1b..cbdfca122b 100644 --- a/src/test/storm/storage/SylvanDdTest.cpp +++ b/src/test/storm/storage/SylvanDdTest.cpp @@ -15,12 +15,22 @@ class Sylvan { public: + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_SYLVAN + GTEST_SKIP() << "Library Sylvan not available."; +#endif + } + static const storm::dd::DdType DdType = storm::dd::DdType::Sylvan; }; template class SylvanDd : public ::testing::Test { public: + void SetUp() override { + TestType::checkLibraryAvailable(); + } + static const storm::dd::DdType DdType = TestType::DdType; }; diff --git a/src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp b/src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp index 7c20ddc69f..1844491704 100644 --- a/src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp +++ b/src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp @@ -22,17 +22,33 @@ class Cudd { public: + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_CUDD + GTEST_SKIP() << "Library CUDD not available."; +#endif + } + static const storm::dd::DdType DdType = storm::dd::DdType::CUDD; }; class Sylvan { public: + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_SYLVAN + GTEST_SKIP() << "Library Sylvan not available."; +#endif + } + static const storm::dd::DdType DdType = storm::dd::DdType::Sylvan; }; template class SymbolicModelBisimulationDecomposition : public ::testing::Test { public: + void SetUp() override { + TestType::checkLibraryAvailable(); + } + static const storm::dd::DdType DdType = TestType::DdType; }; diff --git a/src/test/storm/utility/GraphTest.cpp b/src/test/storm/utility/GraphTest.cpp index a3cab89082..e046e296dc 100644 --- a/src/test/storm/utility/GraphTest.cpp +++ b/src/test/storm/utility/GraphTest.cpp @@ -18,11 +18,23 @@ class Cudd { public: + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_CUDD + GTEST_SKIP() << "Library CUDD not available."; +#endif + } + static const storm::dd::DdType DdType = storm::dd::DdType::CUDD; }; class Sylvan { public: + static void checkLibraryAvailable() { +#ifndef STORM_HAVE_SYLVAN + GTEST_SKIP() << "Library Sylvan not available."; +#endif + } + static const storm::dd::DdType DdType = storm::dd::DdType::Sylvan; }; @@ -34,8 +46,9 @@ class GraphTestSymbolic : public ::testing::Test { protected: void SetUp() override { #ifndef STORM_HAVE_Z3 - GTEST_SKIP() << "Z3 not available."; + GTEST_SKIP() << "Library Z3 not available."; #endif + TestType::checkLibraryAvailable(); } }; @@ -43,7 +56,7 @@ class GraphTestExplicit : public ::testing::Test { protected: void SetUp() override { #ifndef STORM_HAVE_Z3 - GTEST_SKIP() << "Z3 not available."; + GTEST_SKIP() << "Library Z3 not available."; #endif } };