diff --git a/CMakeLists.txt b/CMakeLists.txt index d6ff09d75..a811c1507 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -270,7 +270,7 @@ if(DOXYGEN_FOUND) set(CMAKE_DOXYGEN_OUTPUT_DIR "${CMAKE_CURRENT_BINARY_DIR}/doc") string(REGEX REPLACE ";" " " CMAKE_DOXYGEN_INPUT_LIST "${PROJECT_SOURCE_DIR}/src") - configure_file("${CMAKE_CURRENT_SOURCE_DIR}/doc/Doxyfile.in" "${CMAKE_CURRENT_BINARY_DIR}/Doxyfile" @ONLY) + configure_file("${CMAKE_CURRENT_SOURCE_DIR}/resources/doxygen/Doxyfile.in" "${CMAKE_CURRENT_BINARY_DIR}/Doxyfile" @ONLY) add_custom_target(doc ${DOXYGEN_EXECUTABLE} "${CMAKE_CURRENT_BINARY_DIR}/Doxyfile" DEPENDS "${CMAKE_CURRENT_BINARY_DIR}/Doxyfile" COMMENT "Generating API documentation with Doxygen" VERBATIM) endif(DOXYGEN_FOUND) @@ -333,6 +333,6 @@ add_custom_target(memcheck-functional-tests valgrind --leak-check=full --show-re add_custom_target(memcheck-performance-tests valgrind --leak-check=full --show-reachable=yes ${PROJECT_BINARY_DIR}/storm-performance-tests -v --fix-deadlocks DEPENDS storm-performance-tests) set(CPPLINT_ARGS --filter=-whitespace/tab,-whitespace/line_length,-legal/copyright,-readability/streams) -add_custom_target(style python cpplint.py ${CPPLINT_ARGS} `find ./src/ -iname "*.h" -or -iname "*.cpp" `) +add_custom_target(style python resources/3rdparty/cpplint/cpplint.py ${CPPLINT_ARGS} `find ./src/ -iname "*.h" -or -iname "*.cpp" `) include(StormCPackConfig.cmake) diff --git a/README.md b/README.md new file mode 100644 index 000000000..4a76de895 --- /dev/null +++ b/README.md @@ -0,0 +1 @@ +For more instructions, check out the documentation found in [Getting Started](doc/getting-started.md) diff --git a/doc/build.md b/doc/build.md new file mode 100644 index 000000000..23f2fc67e --- /dev/null +++ b/doc/build.md @@ -0,0 +1,23 @@ +CMake >= 2.8.11 + CMake is required as it is used to generate the Makefiles or Projects/Solutions required to build StoRM. + + Compiler: + A C++11 compliant compiler is required to build StoRM. It is tested and known to work with the following compilers: + - GCC 5.0 + - Clang 3.5.0 + + Other versions or compilers might work, but are not tested. + + The following Compilers are known NOT to work: Microsoft Visual Studio versions older than 2013, GCC versions 4.7 and older. + +Prerequisites: + Boost >= 1.60 + Build using the Boost Build system, for x64 use "bjam address-model=64" or "bjam.exe address-model=64 --build-type=complete" + + +It is recommended to make an out-of-source build, meaning that the folder in which CMake generates its Cache, Makefiles and output files should not be the Project Root nor its Source Directory. +A typical build layout is to create a folder "build" in the project root alongside the CMakeLists.txt file, change into this folder and execute "cmake .." as this will leave all source files untouched +and makes cleaning up the build tree very easy. +There are several options available for the CMake Script as to control behaviour and included components. +If no error occured during the last CMake Configure round, press Generate. +Now you can build StoRM using the generated project/makefiles in the Build folder you selected. \ No newline at end of file diff --git a/doc/dependencies.md b/doc/dependencies.md new file mode 100644 index 000000000..9b4b5c290 --- /dev/null +++ b/doc/dependencies.md @@ -0,0 +1,41 @@ + + + + Included Dependencies: + Carl 1.0 + + CUDD 3.0.0 + CUDD is included in the StoRM Sources under /resources/3rdparty/cudd-2.5.0 and builds automatically alongside StoRM. + Its Sourced where heavily modified as to incorporate newer Versions of Boost, changes in C++ (TR1 to C++11) and + to remove components only available under UNIX. + + Eigen 3.3 beta1 + Eigen is included in the StoRM Sources under /resources/3rdparty/eigen and builds automatically alongside StoRM. + + + GTest 1.7.0 + GTest is included in the StoRM Sources under /resources/3rdparty/gtest-1.7.0 and builds automatically alongside StoRM + GMM >= 4.2 + GMM is included in the StoRM Sources under /resources/3rdparty/gmm-4.2 and builds automatically alongside StoRM. + + +Optional: + Gurobi >= 5.6.2 + Specify the path to the gurobi root dir using -DGUROBI_ROOT=/your/path/to/gurobi + Z3 >= 4.3.2 + Specify the path to the z3 root dir using -DZ3_ROOT=/your/path/to/z3 +MathSAT >= 5.2.11 + Specify the path to the mathsat root dir using -DMSAT_ROOT=/your/path/to/mathsat +MPIR >= 2.7.0 + MSVC only and only if linked with MathSAT + Specify the path to the gmp-include directory -DGMP_INCLUDE_DIR=/your/path/to/mathsat + Specify the path to the mpir.lib directory -DGMP_MPIR_LIBRARY=/your/path/to/mpir.lib + Specify the path to the mpirxx.lib directory -DGMP_MPIRXX_LIBRARY=/your/path/to/mpirxx.lib +GMP + clang and gcc only +CUDA Toolkit >= 6.5 + Specify the path to the cuda toolkit root dir using -DCUDA_ROOT=/your/path/to/cuda +CUSP >= 0.4.0 + Only of built with CUDA Toolkit + CUSP is included in the StoRM Sources as a git-submodule unter /resources/3rdparty/cusplibrary + diff --git a/doc/getting-started.md b/doc/getting-started.md new file mode 100644 index 000000000..8b1378917 --- /dev/null +++ b/doc/getting-started.md @@ -0,0 +1 @@ + diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index a539f8b98..471a1f5c1 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -64,7 +64,7 @@ set(Boost_USE_STATIC_LIBS ${USE_BOOST_STATIC_LIBRARIES}) set(Boost_USE_MULTITHREADED ON) set(Boost_USE_STATIC_RUNTIME OFF) -find_package(Boost 1.56.0 QUIET REQUIRED) +find_package(Boost 1.57.0 QUIET REQUIRED) if ((NOT Boost_LIBRARY_DIRS) OR ("${Boost_LIBRARY_DIRS}" STREQUAL "")) set(Boost_LIBRARY_DIRS "${Boost_INCLUDE_DIRS}/stage/lib") @@ -194,7 +194,7 @@ if(USE_CARL) GIT_TAG master INSTALL_DIR ${STORM_3RDPARTY_BINARY_DIR}/carl SOURCE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/carl - CMAKE_ARGS -DCXX=${CMAKE_CXX_COMPILER} -DEXPORT_TO_CMAKE=0 -DUSE_CLN_NUMBERS=1 -DCMAKE_SKIP_INSTALL_ALL_DEPENDENCY=1 -DCMAKE_INSTALL_PREFIX:PATH=${STORM_3RDPARTY_BINARY_DIR}/carl + CMAKE_ARGS -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER} -DEXPORT_TO_CMAKE=0 -DUSE_CLN_NUMBERS=1 -DCMAKE_SKIP_INSTALL_ALL_DEPENDENCY=1 -DCMAKE_INSTALL_PREFIX:PATH=${STORM_3RDPARTY_BINARY_DIR}/carl BUILD_IN_SOURCE 0 BUILD_COMMAND make lib_carl INSTALL_COMMAND make install @@ -204,6 +204,7 @@ if(USE_CARL) LOG_INSTALL ON ) + add_dependencies(resources xercesc) include_directories(${STORM_3RDPARTY_BINARY_DIR}/carl/include) list(APPEND STORM_LINK_LIBRARIES ${STORM_3RDPARTY_BINARY_DIR}/carl/lib/libcarl${DYNAMIC_EXT}) set(STORM_HAVE_CARL ON) @@ -306,7 +307,7 @@ ExternalProject_Add( DOWNLOAD_COMMAND "" PREFIX "sylvan" SOURCE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/sylvan - CMAKE_ARGS -DSYLVAN_BUILD_TEST=Off -DSYLVAN_BUILD_EXAMPLES=Off -DCMAKE_BUILD_TYPE=Release + CMAKE_ARGS -DCMAKE_C_COMPILER=${CMAKE_C_COMPILER} -DSYLVAN_BUILD_TEST=Off -DSYLVAN_BUILD_EXAMPLES=Off -DCMAKE_BUILD_TYPE=Release BINARY_DIR "${PROJECT_BINARY_DIR}/sylvan" BUILD_IN_SOURCE 0 INSTALL_COMMAND "" @@ -351,7 +352,7 @@ ExternalProject_Add( SOURCE_DIR "${STORM_3RDPARTY_SOURCE_DIR}/gtest-1.7.0" # Force the same output paths for debug and release builds so that # we know in which place the binaries end up when using the Xcode generator - CMAKE_ARGS -Dgtest_force_shared_crt=ON -DCXX=${CMAKE_CXX_COMPILER} -DCMAKE_ARCHIVE_OUTPUT_DIRECTORY_DEBUG:PATH=${STORM_3RDPARTY_BINARY_DIR}/gtest-1.7.0 -DCMAKE_ARCHIVE_OUTPUT_DIRECTORY_RELEASE:PATH=${STORM_3RDPARTY_BINARY_DIR}/gtest-1.7.0 + CMAKE_ARGS -Dgtest_force_shared_crt=ON -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER} -DCMAKE_ARCHIVE_OUTPUT_DIRECTORY_DEBUG:PATH=${STORM_3RDPARTY_BINARY_DIR}/gtest-1.7.0 -DCMAKE_ARCHIVE_OUTPUT_DIRECTORY_RELEASE:PATH=${STORM_3RDPARTY_BINARY_DIR}/gtest-1.7.0 # Disable install step INSTALL_COMMAND "" BINARY_DIR "${STORM_3RDPARTY_BINARY_DIR}/gtest-1.7.0" @@ -551,4 +552,4 @@ if(ENABLE_CUDA) message (STATUS "StoRM - Linking with CUDA") list(APPEND STORM_LINK_LIBRARIES ${STORM_CUDA_LIB_NAME}) include_directories("${PROJECT_SOURCE_DIR}/cuda/kernels/") -endif() \ No newline at end of file +endif() diff --git a/cpplint.py b/resources/3rdparty/cpplint/cpplint.py similarity index 100% rename from cpplint.py rename to resources/3rdparty/cpplint/cpplint.py diff --git a/resources/3rdparty/include_xerces.cmake b/resources/3rdparty/include_xerces.cmake index 9258f66bc..73f559cec 100644 --- a/resources/3rdparty/include_xerces.cmake +++ b/resources/3rdparty/include_xerces.cmake @@ -31,6 +31,6 @@ if(USE_XERCES) FIND_LIBRARY(COREFOUNDATION_LIBRARY CoreFoundation ) FIND_LIBRARY(CORESERVICES_LIBRARY CoreServices ) endif() - find_package(curl) + find_package(CURL) list(APPEND STORM_LINK_LIBRARIES ${XERCESC_LIBRARIES} ${COREFOUNDATION_LIBRARY} ${CORESERVICES_LIBRARY} ${CURL_LIBRARIES}) -endif(USE_XERCES) \ No newline at end of file +endif(USE_XERCES) diff --git a/resources/BUILD.txt b/resources/BUILD.txt deleted file mode 100644 index 4057b110a..000000000 --- a/resources/BUILD.txt +++ /dev/null @@ -1,64 +0,0 @@ -CMake >= 2.8.11 - CMake is required as it is used to generate the Makefiles or Projects/Solutions required to build StoRM. - - Compiler: - A C++11 compliant compiler is required to build StoRM. It is tested and known to work with the following compilers: - - GCC 4.9.1 - - Clang 3.5.0 - - Microsoft Visual Studio 2013 - - Other versions or compilers might work, but are not tested. - - The following Compilers are known NOT to work: Microsoft Visual Studio versions older than 2013, GCC versions 4.7 and older. - -Prerequisites: - Boost >= 1.56 - Build using the Boost Build system, for x64 use "bjam address-model=64" or "bjam.exe address-model=64 --build-type=complete" - You may use --toolset to specify the compiler, for ex. msvc-10.0, intel11.1, etc - Doxygen - Set DOXYGEN_EXECUTABLE to your doxygen executable, e.g. "C:/Program Files/doxygen/bin/doxygen.exe" - GTest >= 1.7.0 - GTest is included in the StoRM Sources under /resources/3rdparty/gtest-1.7.0 and builds automatically alongside StoRM - CUDD >= 2.5.0 - CUDD is included in the StoRM Sources under /resources/3rdparty/cudd-2.5.0 and builds automatically alongside StoRM. - Its Sourced where heavily modified as to incorporate newer Versions of Boost, changes in C++ (TR1 to C++11) and - to remove components only available under UNIX. - Log4CPlus >= 1.1.2 - Log4CPlus is included in the StoRM Sources under /resources/3rdparty/log4cplus-1.1.3-rc1 and builds automatically alongside StoRM. - Its Sourced where slightly modified as to incorporate Unicode handling under Win32, Clang compatability and shared/static build options. - Eigen >= 3.2.1 - Eigen is included in the StoRM Sources under /resources/3rdparty/eigen and builds automatically alongside StoRM. - GMM >= 4.2 - GMM is included in the StoRM Sources under /resources/3rdparty/gmm-4.2 and builds automatically alongside StoRM. - LTL2DStar >= 0.5.1 - LTL2DStar is included in the StoRM Sources under /resources/3rdparty/ltl2dstar-0.5.1 and builds automatically alongside StoRM. - Its Sourced where heavily modified as to incorporate changes in C++ (TR1 to C++11) and - to remove components only available under UNIX. - -Optional: - Gurobi >= 5.6.2 - Specify the path to the gurobi root dir using -DGUROBI_ROOT=/your/path/to/gurobi - Z3 >= 4.3.2 - Specify the path to the z3 root dir using -DZ3_ROOT=/your/path/to/z3 -MathSAT >= 5.2.11 - Specify the path to the mathsat root dir using -DMSAT_ROOT=/your/path/to/mathsat -MPIR >= 2.7.0 - MSVC only and only if linked with MathSAT - Specify the path to the gmp-include directory -DGMP_INCLUDE_DIR=/your/path/to/mathsat - Specify the path to the mpir.lib directory -DGMP_MPIR_LIBRARY=/your/path/to/mpir.lib - Specify the path to the mpirxx.lib directory -DGMP_MPIRXX_LIBRARY=/your/path/to/mpirxx.lib -GMP - clang and gcc only and inly if linked with MathSAT -CUDA Toolkit >= 6.5 - Specify the path to the cuda toolkit root dir using -DCUDA_ROOT=/your/path/to/cuda -CUSP >= 0.4.0 - Only of built with CUDA Toolkit - CUSP is included in the StoRM Sources as a git-submodule unter /resources/3rdparty/cusplibrary - - -It is recommended to make an out-of-source build, meaning that the folder in which CMake generates its Cache, Makefiles and output files should not be the Project Root nor its Source Directory. -A typical build layout is to create a folder "build" in the project root alongside the CMakeLists.txt file, change into this folder and execute "cmake .." as this will leave all source files untouched -and makes cleaning up the build tree very easy. -There are several options available for the CMake Script as to control behaviour and included components. -If no error occured during the last CMake Configure round, press Generate. -Now you can build StoRM using the generated project/makefiles in the Build folder you selected. \ No newline at end of file diff --git a/doc/Doxyfile.in b/resources/doxygen/Doxyfile.in similarity index 100% rename from doc/Doxyfile.in rename to resources/doxygen/Doxyfile.in diff --git a/src/adapters/EigenAdapter.cpp b/src/adapters/EigenAdapter.cpp index 350ca8e20..94964964b 100644 --- a/src/adapters/EigenAdapter.cpp +++ b/src/adapters/EigenAdapter.cpp @@ -21,7 +21,10 @@ namespace storm { } template std::unique_ptr> EigenAdapter::toEigenSparseMatrix(storm::storage::SparseMatrix const& matrix); + +#ifdef STORM_HAVE_CARL template std::unique_ptr> EigenAdapter::toEigenSparseMatrix(storm::storage::SparseMatrix const& matrix); template std::unique_ptr> EigenAdapter::toEigenSparseMatrix(storm::storage::SparseMatrix const& matrix); +#endif } } diff --git a/src/builder/ExplicitGspnModelBuilder.cpp b/src/builder/ExplicitGspnModelBuilder.cpp index a58252373..8caabb5e3 100644 --- a/src/builder/ExplicitGspnModelBuilder.cpp +++ b/src/builder/ExplicitGspnModelBuilder.cpp @@ -185,7 +185,7 @@ namespace storm { std::vector>> weightedTransitions; for (auto& trans : enabledImmediateTransitions) { - if (trans->getWeight() == 0) { + if (trans->noWeightAttached()) { decltype(weightedTransitions) singleton; singleton.push_back(trans); result.push_back(singleton); diff --git a/src/builder/ExplicitGspnModelBuilder.h b/src/builder/ExplicitGspnModelBuilder.h index 16c0c8a72..38ba60f0b 100644 --- a/src/builder/ExplicitGspnModelBuilder.h +++ b/src/builder/ExplicitGspnModelBuilder.h @@ -1,12 +1,12 @@ #ifndef STORM_BUILDER_EXPLICITGSPNMODELBUILDER_H_ #define STORM_BUILDER_EXPLICITGSPNMODELBUILDER_H_ -#include +#include #include "src/models/sparse/MarkovAutomaton.h" #include "src/models/sparse/StandardRewardModel.h" -#include "src/storage/Bitvector.h" -#include "src/storage/BitvectorHashMap.h" +#include "src/storage/BitVector.h" +#include "src/storage/BitVectorHashMap.h" #include "src/storage/gspn/GSPN.h" #include "src/storage/gspn/ImmediateTransition.h" #include "src/storage/gspn/TimedTransition.h" diff --git a/src/builder/ExplicitModelBuilder.cpp b/src/builder/ExplicitModelBuilder.cpp index bb62757a4..5faf386e5 100644 --- a/src/builder/ExplicitModelBuilder.cpp +++ b/src/builder/ExplicitModelBuilder.cpp @@ -412,9 +412,11 @@ namespace storm { // Explicitly instantiate the class. template class ExplicitModelBuilder, uint32_t>; + +#ifdef STORM_HAVE_CARL template class ExplicitModelBuilder, uint32_t>; - - template class ExplicitModelBuilder, uint32_t>; template class ExplicitModelBuilder, uint32_t>; + template class ExplicitModelBuilder, uint32_t>; +#endif } } diff --git a/src/cli/cli.cpp b/src/cli/cli.cpp index 0c2e80f53..f71f71264 100644 --- a/src/cli/cli.cpp +++ b/src/cli/cli.cpp @@ -228,9 +228,17 @@ namespace storm { } if (storm::settings::getModule().isParametricSet()) { +#ifdef STORM_HAVE_CARL buildAndCheckSymbolicModel(preprocessedProgram, preprocessedFormulas, true); +#else + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No parameters are supported in this build."); +#endif } else if (storm::settings::getModule().isExactSet()) { +#ifdef STORM_HAVE_CARL buildAndCheckSymbolicModel(preprocessedProgram, preprocessedFormulas, true); +#else + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No exact numbers are supported in this build."); +#endif } else { buildAndCheckSymbolicModel(preprocessedProgram, preprocessedFormulas, true); } diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h index c2990b072..ccd48e42b 100644 --- a/src/cli/entrypoints.h +++ b/src/cli/entrypoints.h @@ -224,6 +224,7 @@ namespace storm { } } +#ifdef STORM_HAVE_CARL template<> void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas, bool onlyInitialStatesRelevant) { STORM_LOG_THROW(storm::settings::getModule().getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Cannot use this data type with an engine different than the sparse one."); @@ -235,6 +236,7 @@ namespace storm { STORM_LOG_THROW(storm::settings::getModule().getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Cannot use this data type with an engine different than the sparse one."); buildAndCheckSymbolicModelWithSparseEngine(program, formulas, onlyInitialStatesRelevant); } +#endif template void buildAndCheckExplicitModel(std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { diff --git a/src/generator/Choice.cpp b/src/generator/Choice.cpp index 7a209ccc4..7f91a4b4d 100644 --- a/src/generator/Choice.cpp +++ b/src/generator/Choice.cpp @@ -100,7 +100,10 @@ namespace storm { } template class Choice; + +#ifdef STORM_HAVE_CARL template class Choice; template class Choice; +#endif } -} \ No newline at end of file +} diff --git a/src/generator/CompressedState.cpp b/src/generator/CompressedState.cpp index 3a229112f..d7707d740 100644 --- a/src/generator/CompressedState.cpp +++ b/src/generator/CompressedState.cpp @@ -30,8 +30,11 @@ namespace storm { } template void unpackStateIntoEvaluator(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator& evaluator); + storm::expressions::SimpleValuation unpackStateIntoValuation(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionManager const& manager); + +#ifdef STORM_HAVE_CARL template void unpackStateIntoEvaluator(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator& evaluator); template void unpackStateIntoEvaluator(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator& evaluator); - storm::expressions::SimpleValuation unpackStateIntoValuation(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionManager const& manager); +#endif } -} \ No newline at end of file +} diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp index 9e0f10b7f..cfb08fb79 100644 --- a/src/generator/JaniNextStateGenerator.cpp +++ b/src/generator/JaniNextStateGenerator.cpp @@ -492,8 +492,10 @@ namespace storm { } template class JaniNextStateGenerator; + +#ifdef STORM_HAVE_CARL template class JaniNextStateGenerator; template class JaniNextStateGenerator; - +#endif } -} \ No newline at end of file +} diff --git a/src/generator/NextStateGenerator.cpp b/src/generator/NextStateGenerator.cpp index 54fb2f280..9c1eefbd5 100644 --- a/src/generator/NextStateGenerator.cpp +++ b/src/generator/NextStateGenerator.cpp @@ -28,7 +28,7 @@ namespace storm { } std::string const& LabelOrExpression::getLabel() const { - return boost::get(labelOrExpression); + return boost::get(labelOrExpression); } bool LabelOrExpression::isExpression() const { @@ -36,7 +36,7 @@ namespace storm { } storm::expressions::Expression const& LabelOrExpression::getExpression() const { - return boost::get(labelOrExpression); + return boost::get(labelOrExpression); } NextStateGeneratorOptions::NextStateGeneratorOptions(bool buildAllRewardModels, bool buildAllLabels) : buildAllRewardModels(buildAllRewardModels), buildAllLabels(buildAllLabels), buildChoiceLabels(false) { @@ -303,8 +303,10 @@ namespace storm { } template class NextStateGenerator; + +#ifdef STORM_HAVE_CARL template class NextStateGenerator; template class NextStateGenerator; - +#endif } } diff --git a/src/generator/NextStateGenerator.h b/src/generator/NextStateGenerator.h index 1a49b56c1..30a4157cd 100644 --- a/src/generator/NextStateGenerator.h +++ b/src/generator/NextStateGenerator.h @@ -4,11 +4,8 @@ #include #include - #include -#define BOOST_VARIANT_USE_RELAXED_GET_BY_DEFAULT - #include "src/storage/expressions/Expression.h" #include "src/storage/BitVectorHashMap.h" #include "src/storage/expressions/ExpressionEvaluator.h" diff --git a/src/generator/PrismNextStateGenerator.cpp b/src/generator/PrismNextStateGenerator.cpp index 552cd30a9..c0026a98d 100644 --- a/src/generator/PrismNextStateGenerator.cpp +++ b/src/generator/PrismNextStateGenerator.cpp @@ -77,7 +77,11 @@ namespace storm { template void PrismNextStateGenerator::checkValid(storm::prism::Program const& program) { // If the program still contains undefined constants and we are not in a parametric setting, assemble an appropriate error message. +#ifdef STORM_HAVE_CARL if (!std::is_same::value && program.hasUndefinedConstants()) { +#else + if (program.hasUndefinedConstants()) { +#endif std::vector> undefinedConstants = program.getUndefinedConstants(); std::stringstream stream; bool printComma = false; @@ -91,9 +95,13 @@ namespace storm { } stream << "."; STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " + stream.str()); - } else if (std::is_same::value && !program.hasUndefinedConstantsOnlyInUpdateProbabilitiesAndRewards()) { + } + +#ifdef STORM_HAVE_CARL + else if (std::is_same::value && !program.hasUndefinedConstantsOnlyInUpdateProbabilitiesAndRewards()) { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The program contains undefined constants that appear in some places other than update probabilities and reward value expressions, which is not admitted."); } +#endif } template @@ -561,7 +569,10 @@ namespace storm { } template class PrismNextStateGenerator; + +#ifdef STORM_HAVE_CARL template class PrismNextStateGenerator; template class PrismNextStateGenerator; +#endif } } diff --git a/src/generator/StateBehavior.cpp b/src/generator/StateBehavior.cpp index 28e256c18..4e71c537f 100644 --- a/src/generator/StateBehavior.cpp +++ b/src/generator/StateBehavior.cpp @@ -56,8 +56,10 @@ namespace storm { } template class StateBehavior; + +#ifdef STORM_HAVE_CARL template class StateBehavior; template class StateBehavior; - +#endif } -} \ No newline at end of file +} diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp index 4d2d8fbea..914b71cc1 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -140,8 +140,11 @@ namespace storm { // Explicitly instantiate the model checker. template class SparseCtmcCslModelChecker>; + +#ifdef STORM_HAVE_CARL template class SparseCtmcCslModelChecker>; template class SparseCtmcCslModelChecker>; - +#endif + } // namespace modelchecker } // namespace storm diff --git a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index dab1449de..c51563507 100644 --- a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -688,44 +688,61 @@ namespace storm { template std::vector SparseCtmcCslHelper::computeBoundedUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeBoundedUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeBoundedUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template std::vector SparseCtmcCslHelper::computeUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template std::vector SparseCtmcCslHelper::computeNextProbabilities(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeNextProbabilities(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeNextProbabilities(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template std::vector SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template std::vector SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template std::vector SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template storm::storage::SparseMatrix SparseCtmcCslHelper::computeUniformizedMatrix(storm::storage::SparseMatrix const& rateMatrix, storm::storage::BitVector const& maybeStates, double uniformizationRate, std::vector const& exitRates); + template std::vector SparseCtmcCslHelper::computeTransientProbabilities(storm::storage::SparseMatrix const& uniformizedMatrix, std::vector const* addVector, double timeBound, double uniformizationRate, std::vector values, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + +#ifdef STORM_HAVE_CARL + template std::vector SparseCtmcCslHelper::computeBoundedUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeBoundedUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + template std::vector SparseCtmcCslHelper::computeUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + template std::vector SparseCtmcCslHelper::computeNextProbabilities(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeNextProbabilities(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + template std::vector SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + template std::vector SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + template std::vector SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + template std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template storm::storage::SparseMatrix SparseCtmcCslHelper::computeProbabilityMatrix(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRates); template storm::storage::SparseMatrix SparseCtmcCslHelper::computeProbabilityMatrix(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRates); template storm::storage::SparseMatrix SparseCtmcCslHelper::computeProbabilityMatrix(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRates); - - template std::vector SparseCtmcCslHelper::computeTransientProbabilities(storm::storage::SparseMatrix const& uniformizedMatrix, std::vector const* addVector, double timeBound, double uniformizationRate, std::vector values, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + + + + + + +#endif } } } diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index bb3a1a701..1b36dd820 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -146,7 +146,10 @@ namespace storm { } template class SparseDtmcPrctlModelChecker>; + +#ifdef STORM_HAVE_CARL template class SparseDtmcPrctlModelChecker>; template class SparseDtmcPrctlModelChecker>; +#endif } -} \ No newline at end of file +} diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 629cf29eb..25804c37a 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -147,6 +147,9 @@ namespace storm { } template class SparseMdpPrctlModelChecker>; + +#ifdef STORM_HAVE_CARL template class SparseMdpPrctlModelChecker>; +#endif } -} \ No newline at end of file +} diff --git a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index 79a85fdfe..d6b721ade 100644 --- a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -401,8 +401,11 @@ namespace storm { } template class SparseDtmcPrctlHelper; + +#ifdef STORM_HAVE_CARL template class SparseDtmcPrctlHelper; template class SparseDtmcPrctlHelper; +#endif } } } diff --git a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 75fbfdfea..c9f7e83c4 100644 --- a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -650,11 +650,12 @@ namespace storm { template std::vector SparseMdpPrctlHelper::computeCumulativeRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, uint_fast64_t stepBound, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); template std::vector SparseMdpPrctlHelper::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); +#ifdef STORM_HAVE_CARL template class SparseMdpPrctlHelper; template std::vector SparseMdpPrctlHelper::computeInstantaneousRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, uint_fast64_t stepCount, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); template std::vector SparseMdpPrctlHelper::computeCumulativeRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, uint_fast64_t stepBound, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); template std::vector SparseMdpPrctlHelper::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - +#endif } } } diff --git a/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp b/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp index 5ffc50140..0725cc4a2 100644 --- a/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp +++ b/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp @@ -57,6 +57,7 @@ namespace storm { template class SparsePropositionalModelChecker>; template class SparsePropositionalModelChecker>; +#ifdef STORM_HAVE_CARL template class SparsePropositionalModelChecker>>; template class SparsePropositionalModelChecker>; @@ -70,5 +71,6 @@ namespace storm { template class SparsePropositionalModelChecker>; template class SparsePropositionalModelChecker>; template class SparsePropositionalModelChecker>; +#endif } -} \ No newline at end of file +} diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index e6f0bbb2d..fdf541d97 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -986,7 +986,10 @@ namespace storm { } template class SparseDtmcEliminationModelChecker>; + +#ifdef STORM_HAVE_CARL template class SparseDtmcEliminationModelChecker>; template class SparseDtmcEliminationModelChecker>; +#endif } // namespace modelchecker } // namespace storm diff --git a/src/modelchecker/results/CheckResult.cpp b/src/modelchecker/results/CheckResult.cpp index 324fdd089..7d8fcd1ac 100644 --- a/src/modelchecker/results/CheckResult.cpp +++ b/src/modelchecker/results/CheckResult.cpp @@ -145,10 +145,12 @@ namespace storm { template HybridQuantitativeCheckResult& CheckResult::asHybridQuantitativeCheckResult(); template HybridQuantitativeCheckResult const& CheckResult::asHybridQuantitativeCheckResult() const; +#ifdef STORM_HAVE_CARL template ExplicitQuantitativeCheckResult& CheckResult::asExplicitQuantitativeCheckResult(); template ExplicitQuantitativeCheckResult const& CheckResult::asExplicitQuantitativeCheckResult() const; template ExplicitQuantitativeCheckResult& CheckResult::asExplicitQuantitativeCheckResult(); template ExplicitQuantitativeCheckResult const& CheckResult::asExplicitQuantitativeCheckResult() const; +#endif } -} \ No newline at end of file +} diff --git a/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp b/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp index 652c094a5..dfe624f2a 100644 --- a/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp +++ b/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp @@ -250,7 +250,10 @@ namespace storm { } template class ExplicitQuantitativeCheckResult; + +#ifdef STORM_HAVE_CARL template class ExplicitQuantitativeCheckResult; template class ExplicitQuantitativeCheckResult; +#endif } } diff --git a/src/models/sparse/Ctmc.cpp b/src/models/sparse/Ctmc.cpp index e48f4590f..26b106c59 100644 --- a/src/models/sparse/Ctmc.cpp +++ b/src/models/sparse/Ctmc.cpp @@ -46,11 +46,13 @@ namespace storm { } template class Ctmc; + +#ifdef STORM_HAVE_CARL template class Ctmc; template class Ctmc>; template class Ctmc; - +#endif } // namespace sparse } // namespace models -} // namespace storm \ No newline at end of file +} // namespace storm diff --git a/src/models/sparse/DeterministicModel.cpp b/src/models/sparse/DeterministicModel.cpp index c2bd35b16..5962e6500 100644 --- a/src/models/sparse/DeterministicModel.cpp +++ b/src/models/sparse/DeterministicModel.cpp @@ -57,11 +57,13 @@ namespace storm { template class DeterministicModel; template class DeterministicModel; + +#ifdef STORM_HAVE_CARL template class DeterministicModel; template class DeterministicModel>; template class DeterministicModel; - +#endif } // namespace sparse } // namespace models -} // namespace storm \ No newline at end of file +} // namespace storm diff --git a/src/models/sparse/Dtmc.cpp b/src/models/sparse/Dtmc.cpp index 7997a1494..ce9f9e5aa 100644 --- a/src/models/sparse/Dtmc.cpp +++ b/src/models/sparse/Dtmc.cpp @@ -69,11 +69,13 @@ namespace storm { template class Dtmc; template class Dtmc; + +#ifdef STORM_HAVE_CARL template class Dtmc; template class Dtmc>; template class Dtmc; - +#endif } // namespace sparse } // namespace models } // namespace storm diff --git a/src/models/sparse/MarkovAutomaton.cpp b/src/models/sparse/MarkovAutomaton.cpp index b09da840e..887d3a13b 100644 --- a/src/models/sparse/MarkovAutomaton.cpp +++ b/src/models/sparse/MarkovAutomaton.cpp @@ -366,11 +366,12 @@ namespace storm { template class MarkovAutomaton; // template class MarkovAutomaton; +#ifdef STORM_HAVE_CARL template class MarkovAutomaton; template class MarkovAutomaton>; template class MarkovAutomaton; - +#endif } // namespace sparse } // namespace models } // namespace storm diff --git a/src/models/sparse/Mdp.cpp b/src/models/sparse/Mdp.cpp index cf436c7e1..8db2670f5 100644 --- a/src/models/sparse/Mdp.cpp +++ b/src/models/sparse/Mdp.cpp @@ -98,11 +98,13 @@ namespace storm { template class Mdp; template class Mdp; + +#ifdef STORM_HAVE_CARL template class Mdp; template class Mdp>; template class Mdp; - +#endif } // namespace sparse } // namespace models -} // namespace storm \ No newline at end of file +} // namespace storm diff --git a/src/models/sparse/Model.cpp b/src/models/sparse/Model.cpp index 8ea0710dc..d6eefe93a 100644 --- a/src/models/sparse/Model.cpp +++ b/src/models/sparse/Model.cpp @@ -312,7 +312,11 @@ namespace storm { template bool Model::supportsParameters() const { +#ifdef STORM_HAVE_CARL return std::is_same::value; +#else + return false; +#endif } template @@ -346,18 +350,21 @@ namespace storm { return this->rewardModels; } +#ifdef STORM_HAVE_CARL std::set getProbabilityParameters(Model const& model) { return storm::storage::getVariables(model.getTransitionMatrix()); } +#endif template class Model; template class Model; +#ifdef STORM_HAVE_CARL template class Model; template class Model>; template class Model; - +#endif } } } diff --git a/src/models/sparse/Model.h b/src/models/sparse/Model.h index a4422a8be..5936b0fe2 100644 --- a/src/models/sparse/Model.h +++ b/src/models/sparse/Model.h @@ -357,7 +357,9 @@ namespace storm { boost::optional> choiceLabeling; }; +#ifdef STORM_HAVE_CARL std::set getProbabilityParameters(Model const& model); +#endif } // namespace sparse } // namespace models } // namespace storm diff --git a/src/models/sparse/NondeterministicModel.cpp b/src/models/sparse/NondeterministicModel.cpp index 3a4af6664..f3c4d29d4 100644 --- a/src/models/sparse/NondeterministicModel.cpp +++ b/src/models/sparse/NondeterministicModel.cpp @@ -169,6 +169,8 @@ namespace storm { template class NondeterministicModel; template class NondeterministicModel; + +#ifdef STORM_HAVE_CARL template class NondeterministicModel; template class NondeterministicModel>; @@ -176,7 +178,7 @@ namespace storm { template void NondeterministicModel>::modifyStateRewards(std::string const& modelName, std::map const& modifications); template class NondeterministicModel; - +#endif } } -} \ No newline at end of file +} diff --git a/src/models/sparse/StandardRewardModel.cpp b/src/models/sparse/StandardRewardModel.cpp index 823d3a884..a539cfd15 100644 --- a/src/models/sparse/StandardRewardModel.cpp +++ b/src/models/sparse/StandardRewardModel.cpp @@ -318,6 +318,7 @@ namespace storm { template class StandardRewardModel; template std::ostream& operator<<(std::ostream& out, StandardRewardModel const& rewardModel); +#ifdef STORM_HAVE_CARL template std::vector StandardRewardModel::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& filter) const; template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix) const; template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights) const; @@ -346,6 +347,7 @@ namespace storm { template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards); template class StandardRewardModel; template std::ostream& operator<<(std::ostream& out, StandardRewardModel const& rewardModel); +#endif } } diff --git a/src/parser/DFTGalileoParser.cpp b/src/parser/DFTGalileoParser.cpp index 2cdda4929..5fc2e7c5a 100644 --- a/src/parser/DFTGalileoParser.cpp +++ b/src/parser/DFTGalileoParser.cpp @@ -71,12 +71,16 @@ namespace storm { toplevelId = stripQuotsFromName(line.substr(toplevelToken.size() + 1)); } else if (boost::starts_with(line, parametricToken)) { +#ifdef STORM_HAVE_CARL STORM_LOG_THROW((std::is_same::value), storm::exceptions::NotSupportedException, "Parameters only allowed when using rational functions."); std::string parameter = stripQuotsFromName(line.substr(parametricToken.size() + 1)); storm::expressions::Variable var = manager->declareRationalVariable(parameter); identifierMapping.emplace(var.getName(), var); parser.setIdentifierMapping(identifierMapping); STORM_LOG_TRACE("Added parameter: " << var.getName()); +#else + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameters are not supported in this build."); +#endif } else { std::vector tokens; boost::split(tokens, line, boost::is_any_of(" ")); diff --git a/src/solver/EigenLinearEquationSolver.cpp b/src/solver/EigenLinearEquationSolver.cpp index 25c16f1ae..47117b9a3 100644 --- a/src/solver/EigenLinearEquationSolver.cpp +++ b/src/solver/EigenLinearEquationSolver.cpp @@ -94,6 +94,7 @@ namespace storm { return restart; } +#ifdef STORM_HAVE_CARL EigenLinearEquationSolverSettings::EigenLinearEquationSolverSettings() { // Intentionally left empty. } @@ -101,6 +102,7 @@ namespace storm { EigenLinearEquationSolverSettings::EigenLinearEquationSolverSettings() { // Intentionally left empty. } +#endif template EigenLinearEquationSolver::EigenLinearEquationSolver(storm::storage::SparseMatrix const& A, EigenLinearEquationSolverSettings const& settings) : eigenA(storm::adapters::EigenAdapter::toEigenSparseMatrix(A)), settings(settings) { @@ -255,8 +257,8 @@ namespace storm { return eigenA->cols(); } - // Specialization form storm::RationalNumber - +#ifdef STORM_HAVE_CARL + // Specialization for storm::RationalNumber template<> void EigenLinearEquationSolver::solveEquations(std::vector& x, std::vector const& b) const { // Map the input vectors to Eigen's format. @@ -268,8 +270,7 @@ namespace storm { solver._solve_impl(eigenB, eigenX); } - // Specialization form storm::RationalFunction - + // Specialization for storm::RationalFunction template<> void EigenLinearEquationSolver::solveEquations(std::vector& x, std::vector const& b) const { // Map the input vectors to Eigen's format. @@ -280,7 +281,8 @@ namespace storm { solver.compute(*eigenA); solver._solve_impl(eigenB, eigenX); } - +#endif + template std::unique_ptr> EigenLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { return std::make_unique>(matrix, settings); @@ -307,16 +309,18 @@ namespace storm { } template class EigenLinearEquationSolverSettings; + template class EigenLinearEquationSolver; + template class EigenLinearEquationSolverFactory; + +#ifdef STORM_HAVE_CARL template class EigenLinearEquationSolverSettings; template class EigenLinearEquationSolverSettings; - template class EigenLinearEquationSolver; template class EigenLinearEquationSolver; template class EigenLinearEquationSolver; - template class EigenLinearEquationSolverFactory; template class EigenLinearEquationSolverFactory; template class EigenLinearEquationSolverFactory; - +#endif } -} \ No newline at end of file +} diff --git a/src/solver/EigenLinearEquationSolver.h b/src/solver/EigenLinearEquationSolver.h index 04c6c9718..688dcae64 100644 --- a/src/solver/EigenLinearEquationSolver.h +++ b/src/solver/EigenLinearEquationSolver.h @@ -40,6 +40,7 @@ namespace storm { uint_fast64_t restart; }; +#ifdef STORM_HAVE_CARL template<> class EigenLinearEquationSolverSettings { public: @@ -51,6 +52,7 @@ namespace storm { public: EigenLinearEquationSolverSettings(); }; +#endif /*! * A class that uses the Eigen library to implement the LinearEquationSolver interface. @@ -96,4 +98,4 @@ namespace storm { EigenLinearEquationSolverSettings settings; }; } -} \ No newline at end of file +} diff --git a/src/solver/EliminationLinearEquationSolver.cpp b/src/solver/EliminationLinearEquationSolver.cpp index 982d2a54b..8cf773c16 100644 --- a/src/solver/EliminationLinearEquationSolver.cpp +++ b/src/solver/EliminationLinearEquationSolver.cpp @@ -173,16 +173,19 @@ namespace storm { } template class EliminationLinearEquationSolverSettings; + template class EliminationLinearEquationSolver; + template class EliminationLinearEquationSolverFactory; + +#ifdef STORM_HAVE_CARL template class EliminationLinearEquationSolverSettings; template class EliminationLinearEquationSolverSettings; - template class EliminationLinearEquationSolver; template class EliminationLinearEquationSolver; template class EliminationLinearEquationSolver; - template class EliminationLinearEquationSolverFactory; template class EliminationLinearEquationSolverFactory; template class EliminationLinearEquationSolverFactory; +#endif } } diff --git a/src/solver/LinearEquationSolver.cpp b/src/solver/LinearEquationSolver.cpp index 81dc4124b..c4d46cd46 100644 --- a/src/solver/LinearEquationSolver.cpp +++ b/src/solver/LinearEquationSolver.cpp @@ -121,6 +121,7 @@ namespace storm { return std::make_unique>(*this); } +#ifdef STORM_HAVE_CARL std::unique_ptr> GeneralLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { return selectSolver(matrix); } @@ -162,18 +163,22 @@ namespace storm { std::unique_ptr> GeneralLinearEquationSolverFactory::clone() const { return std::make_unique>(*this); } +#endif template class LinearEquationSolver; + template class LinearEquationSolverFactory; + template class GeneralLinearEquationSolverFactory; + +#ifdef STORM_HAVE_CARL template class LinearEquationSolver; template class LinearEquationSolver; - template class LinearEquationSolverFactory; template class LinearEquationSolverFactory; template class LinearEquationSolverFactory; - template class GeneralLinearEquationSolverFactory; template class GeneralLinearEquationSolverFactory; template class GeneralLinearEquationSolverFactory; +#endif } -} \ No newline at end of file +} diff --git a/src/solver/LinearEquationSolver.h b/src/solver/LinearEquationSolver.h index aa243d593..5adac8ea1 100644 --- a/src/solver/LinearEquationSolver.h +++ b/src/solver/LinearEquationSolver.h @@ -154,6 +154,7 @@ namespace storm { std::unique_ptr> selectSolver(MatrixType&& matrix) const; }; +#ifdef STORM_HAVE_CARL template<> class GeneralLinearEquationSolverFactory : public LinearEquationSolverFactory { public: @@ -179,7 +180,7 @@ namespace storm { template std::unique_ptr> selectSolver(MatrixType&& matrix) const; }; - +#endif } // namespace solver } // namespace storm diff --git a/src/solver/MinMaxLinearEquationSolver.cpp b/src/solver/MinMaxLinearEquationSolver.cpp index a92f19dd9..c82514a37 100644 --- a/src/solver/MinMaxLinearEquationSolver.cpp +++ b/src/solver/MinMaxLinearEquationSolver.cpp @@ -144,6 +144,7 @@ namespace storm { return result; } +#ifdef STORM_HAVE_CARL template<> template std::unique_ptr> GeneralMinMaxLinearEquationSolverFactory::selectSolver(MatrixType&& matrix) const { @@ -152,15 +153,17 @@ namespace storm { STORM_LOG_THROW(method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration, storm::exceptions::InvalidSettingsException, "For this data type only value iteration and policy iteration are available."); return std::make_unique>(std::forward(matrix), std::make_unique>()); } - +#endif template class MinMaxLinearEquationSolver; template class MinMaxLinearEquationSolver; - template class MinMaxLinearEquationSolver; template class MinMaxLinearEquationSolverFactory; template class GeneralMinMaxLinearEquationSolverFactory; + +#ifdef STORM_HAVE_CARL + template class MinMaxLinearEquationSolver; template class MinMaxLinearEquationSolverFactory; template class GeneralMinMaxLinearEquationSolverFactory; - +#endif } } diff --git a/src/solver/SolveGoal.cpp b/src/solver/SolveGoal.cpp index 2f0cd365c..622a0c8de 100644 --- a/src/solver/SolveGoal.cpp +++ b/src/solver/SolveGoal.cpp @@ -51,8 +51,9 @@ namespace storm { template std::unique_ptr> configureLinearEquationSolver(BoundedGoal const& goal, storm::solver::LinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); template std::unique_ptr> configureLinearEquationSolver(SolveGoal const& goal, storm::solver::LinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); +#ifdef STORM_HAVE_CARL template std::unique_ptr> configureMinMaxLinearEquationSolver(BoundedGoal const& goal, storm::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); template std::unique_ptr> configureMinMaxLinearEquationSolver(SolveGoal const& goal, storm::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); - +#endif } } diff --git a/src/solver/StandardMinMaxLinearEquationSolver.cpp b/src/solver/StandardMinMaxLinearEquationSolver.cpp index 4e0609e80..1a1f1fcda 100644 --- a/src/solver/StandardMinMaxLinearEquationSolver.cpp +++ b/src/solver/StandardMinMaxLinearEquationSolver.cpp @@ -370,6 +370,7 @@ namespace storm { } } +#ifdef STORM_HAVE_CARL template<> StandardMinMaxLinearEquationSolverFactory::StandardMinMaxLinearEquationSolverFactory(EquationSolverType const& solverType, bool trackScheduler) : MinMaxLinearEquationSolverFactory(trackScheduler) { switch (solverType) { @@ -379,6 +380,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Cannot create the requested solver for this data type."); } } +#endif template std::unique_ptr> StandardMinMaxLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { @@ -441,11 +443,12 @@ namespace storm { template class NativeMinMaxLinearEquationSolverFactory; template class EliminationMinMaxLinearEquationSolverFactory; +#ifdef STORM_HAVE_CARL template class StandardMinMaxLinearEquationSolverSettings; template class StandardMinMaxLinearEquationSolver; template class StandardMinMaxLinearEquationSolverFactory; template class EigenMinMaxLinearEquationSolverFactory; template class EliminationMinMaxLinearEquationSolverFactory; - +#endif } -} \ No newline at end of file +} diff --git a/src/solver/TerminationCondition.cpp b/src/solver/TerminationCondition.cpp index 0503723bc..b0f155470 100644 --- a/src/solver/TerminationCondition.cpp +++ b/src/solver/TerminationCondition.cpp @@ -40,8 +40,9 @@ namespace storm { template class TerminateIfFilteredSumExceedsThreshold; template class TerminateIfFilteredExtremumExceedsThreshold; +#ifdef STORM_HAVE_CARL template class TerminateIfFilteredSumExceedsThreshold; template class TerminateIfFilteredExtremumExceedsThreshold; - +#endif } } diff --git a/src/solver/stateelimination/ConditionalStateEliminator.cpp b/src/solver/stateelimination/ConditionalStateEliminator.cpp index 0a86894bc..21ffec7ac 100644 --- a/src/solver/stateelimination/ConditionalStateEliminator.cpp +++ b/src/solver/stateelimination/ConditionalStateEliminator.cpp @@ -61,9 +61,11 @@ namespace storm { } template class ConditionalStateEliminator; + +#ifdef STORM_HAVE_CARL template class ConditionalStateEliminator; template class ConditionalStateEliminator; - +#endif } // namespace stateelimination } // namespace storage } // namespace storm diff --git a/src/solver/stateelimination/DynamicStatePriorityQueue.cpp b/src/solver/stateelimination/DynamicStatePriorityQueue.cpp index ec2c4fe3f..a0fede010 100644 --- a/src/solver/stateelimination/DynamicStatePriorityQueue.cpp +++ b/src/solver/stateelimination/DynamicStatePriorityQueue.cpp @@ -62,8 +62,11 @@ namespace storm { } template class DynamicStatePriorityQueue; + +#ifdef STORM_HAVE_CARL template class DynamicStatePriorityQueue; template class DynamicStatePriorityQueue; +#endif } } } diff --git a/src/solver/stateelimination/EliminatorBase.cpp b/src/solver/stateelimination/EliminatorBase.cpp index 25907ca8c..dac54a6f5 100644 --- a/src/solver/stateelimination/EliminatorBase.cpp +++ b/src/solver/stateelimination/EliminatorBase.cpp @@ -278,13 +278,15 @@ namespace storm { } template class EliminatorBase; + template class EliminatorBase; + +#ifdef STORM_HAVE_CARL template class EliminatorBase; template class EliminatorBase; - template class EliminatorBase; template class EliminatorBase; template class EliminatorBase; - +#endif } } -} \ No newline at end of file +} diff --git a/src/solver/stateelimination/EquationSystemEliminator.cpp b/src/solver/stateelimination/EquationSystemEliminator.cpp index 2ffe29705..f08f49107 100644 --- a/src/solver/stateelimination/EquationSystemEliminator.cpp +++ b/src/solver/stateelimination/EquationSystemEliminator.cpp @@ -10,8 +10,11 @@ namespace storm { } template class EquationSystemEliminator; + +#ifdef STORM_HAVE_CARL template class EquationSystemEliminator; template class EquationSystemEliminator; +#endif } } -} \ No newline at end of file +} diff --git a/src/solver/stateelimination/LongRunAverageEliminator.cpp b/src/solver/stateelimination/LongRunAverageEliminator.cpp index 88e5b5faa..5b4dde20f 100644 --- a/src/solver/stateelimination/LongRunAverageEliminator.cpp +++ b/src/solver/stateelimination/LongRunAverageEliminator.cpp @@ -26,9 +26,11 @@ namespace storm { } template class LongRunAverageEliminator; + +#ifdef STORM_HAVE_CARL template class LongRunAverageEliminator; template class LongRunAverageEliminator; - +#endif } // namespace stateelimination } // namespace storage } // namespace storm diff --git a/src/solver/stateelimination/PrioritizedStateEliminator.cpp b/src/solver/stateelimination/PrioritizedStateEliminator.cpp index 134cb3264..1b8cca6ff 100644 --- a/src/solver/stateelimination/PrioritizedStateEliminator.cpp +++ b/src/solver/stateelimination/PrioritizedStateEliminator.cpp @@ -29,9 +29,11 @@ namespace storm { } template class PrioritizedStateEliminator; + +#ifdef STORM_HAVE_CARL template class PrioritizedStateEliminator; template class PrioritizedStateEliminator; - +#endif } // namespace stateelimination } // namespace storage } // namespace storm diff --git a/src/solver/stateelimination/StateEliminator.cpp b/src/solver/stateelimination/StateEliminator.cpp index 98b1d64b3..c134d9ffa 100644 --- a/src/solver/stateelimination/StateEliminator.cpp +++ b/src/solver/stateelimination/StateEliminator.cpp @@ -28,9 +28,11 @@ namespace storm { } template class StateEliminator; + +#ifdef STORM_HAVE_CARL template class StateEliminator; template class StateEliminator; - +#endif } // namespace stateelimination } // namespace storage } // namespace storm diff --git a/src/storage/Distribution.cpp b/src/storage/Distribution.cpp index 7c3b5d99f..78e4a477d 100644 --- a/src/storage/Distribution.cpp +++ b/src/storage/Distribution.cpp @@ -152,10 +152,12 @@ namespace storm { template class Distribution; template std::ostream& operator<<(std::ostream& out, Distribution const& distribution); +#ifdef STORM_HAVE_CARL template class Distribution; template std::ostream& operator<<(std::ostream& out, Distribution const& distribution); template class Distribution; template std::ostream& operator<<(std::ostream& out, Distribution const& distribution); +#endif } } diff --git a/src/storage/FlexibleSparseMatrix.cpp b/src/storage/FlexibleSparseMatrix.cpp index 563f86633..102d20304 100644 --- a/src/storage/FlexibleSparseMatrix.cpp +++ b/src/storage/FlexibleSparseMatrix.cpp @@ -269,13 +269,14 @@ namespace storm { // Explicitly instantiate the matrix. template class FlexibleSparseMatrix; template std::ostream& operator<<(std::ostream& out, FlexibleSparseMatrix const& matrix); + +#ifdef STORM_HAVE_CARL template class FlexibleSparseMatrix; template std::ostream& operator<<(std::ostream& out, FlexibleSparseMatrix const& matrix); -#ifdef STORM_HAVE_CARL template class FlexibleSparseMatrix; template std::ostream& operator<<(std::ostream& out, FlexibleSparseMatrix const& matrix); #endif } // namespace storage -} // namespace storm \ No newline at end of file +} // namespace storm diff --git a/src/storage/MaximalEndComponentDecomposition.cpp b/src/storage/MaximalEndComponentDecomposition.cpp index d410b2546..0861513ce 100644 --- a/src/storage/MaximalEndComponentDecomposition.cpp +++ b/src/storage/MaximalEndComponentDecomposition.cpp @@ -193,8 +193,9 @@ namespace storm { template class MaximalEndComponentDecomposition; template MaximalEndComponentDecomposition::MaximalEndComponentDecomposition(storm::models::sparse::NondeterministicModel const& model); +#ifdef STORM_HAVE_CARL template class MaximalEndComponentDecomposition; template MaximalEndComponentDecomposition::MaximalEndComponentDecomposition(storm::models::sparse::NondeterministicModel const& model); - +#endif } } diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index 95f65ce99..add3debbb 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -1213,10 +1213,12 @@ namespace storm { } } +#ifdef STORM_HAVE_CARL template<> void SparseMatrix::performSuccessiveOverRelaxationStep(Interval omega, std::vector& x, std::vector const& b) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This operation is not supported."); } +#endif template void SparseMatrix::multiplyVectorWithMatrix(std::vector const& vector, std::vector& result) const { diff --git a/src/storage/StronglyConnectedComponentDecomposition.cpp b/src/storage/StronglyConnectedComponentDecomposition.cpp index e129c8b85..c32184681 100644 --- a/src/storage/StronglyConnectedComponentDecomposition.cpp +++ b/src/storage/StronglyConnectedComponentDecomposition.cpp @@ -227,16 +227,17 @@ namespace storm { } // Explicitly instantiate the SCC decomposition. - template class StronglyConnectedComponentDecomposition; + template class StronglyConnectedComponentDecomposition; template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, bool dropNaiveSccs, bool onlyBottomSccs); template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, StateBlock const& block, bool dropNaiveSccs, bool onlyBottomSccs); template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs); - template class StronglyConnectedComponentDecomposition; + template class StronglyConnectedComponentDecomposition; template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, bool dropNaiveSccs, bool onlyBottomSccs); template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, StateBlock const& block, bool dropNaiveSccs, bool onlyBottomSccs); template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs); +#ifdef STORM_HAVE_CARL template class StronglyConnectedComponentDecomposition; template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, bool dropNaiveSccs, bool onlyBottomSccs); template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, StateBlock const& block, bool dropNaiveSccs, bool onlyBottomSccs); @@ -246,5 +247,6 @@ namespace storm { template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, bool dropNaiveSccs, bool onlyBottomSccs); template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, StateBlock const& block, bool dropNaiveSccs, bool onlyBottomSccs); template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs); +#endif } // namespace storage -} // namespace storm \ No newline at end of file +} // namespace storm diff --git a/src/storage/bisimulation/BisimulationDecomposition.cpp b/src/storage/bisimulation/BisimulationDecomposition.cpp index 30fc5a2c9..dbad8c633 100644 --- a/src/storage/bisimulation/BisimulationDecomposition.cpp +++ b/src/storage/bisimulation/BisimulationDecomposition.cpp @@ -323,6 +323,7 @@ namespace storm { template class BisimulationDecomposition, bisimulation::DeterministicBlockData>; template class BisimulationDecomposition, bisimulation::DeterministicBlockData>; +#ifdef STORM_HAVE_CARL template class BisimulationDecomposition, bisimulation::DeterministicBlockData>; template class BisimulationDecomposition, bisimulation::DeterministicBlockData>; template class BisimulationDecomposition, bisimulation::DeterministicBlockData>; @@ -330,5 +331,6 @@ namespace storm { template class BisimulationDecomposition, bisimulation::DeterministicBlockData>; template class BisimulationDecomposition, bisimulation::DeterministicBlockData>; template class BisimulationDecomposition, bisimulation::DeterministicBlockData>; +#endif } } diff --git a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp index 89408e620..3f70fd379 100644 --- a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp @@ -652,10 +652,12 @@ namespace storm { template class DeterministicModelBisimulationDecomposition>; template class DeterministicModelBisimulationDecomposition>; +#ifdef STORM_HAVE_CARL template class DeterministicModelBisimulationDecomposition>; template class DeterministicModelBisimulationDecomposition>; template class DeterministicModelBisimulationDecomposition>; template class DeterministicModelBisimulationDecomposition>; +#endif } } diff --git a/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp b/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp index a1eea43dc..64a7efe45 100644 --- a/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp @@ -416,8 +416,10 @@ namespace storm { } template class NondeterministicModelBisimulationDecomposition>; + +#ifdef STORM_HAVE_CARL template class NondeterministicModelBisimulationDecomposition>; template class NondeterministicModelBisimulationDecomposition>; - +#endif } } diff --git a/src/storage/expressions/ExpressionEvaluator.cpp b/src/storage/expressions/ExpressionEvaluator.cpp index 6d44d680a..cf1493dac 100644 --- a/src/storage/expressions/ExpressionEvaluator.cpp +++ b/src/storage/expressions/ExpressionEvaluator.cpp @@ -30,6 +30,7 @@ namespace storm { this->variableToExpressionMap[variable] = this->getManager().rational(value); } +#ifdef STORM_HAVE_CARL ExpressionEvaluator::ExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : ExpressionEvaluatorWithVariableToExpressionMap(manager) { // Intentionally left empty. } @@ -50,5 +51,6 @@ namespace storm { template class ExpressionEvaluatorWithVariableToExpressionMap; template class ExpressionEvaluatorWithVariableToExpressionMap; +#endif } -} \ No newline at end of file +} diff --git a/src/storage/expressions/ExpressionEvaluator.h b/src/storage/expressions/ExpressionEvaluator.h index 2480af12d..e75d1cdf1 100644 --- a/src/storage/expressions/ExpressionEvaluator.h +++ b/src/storage/expressions/ExpressionEvaluator.h @@ -35,6 +35,7 @@ namespace storm { std::unordered_map variableToExpressionMap; }; +#ifdef STORM_HAVE_CARL template<> class ExpressionEvaluator : public ExpressionEvaluatorWithVariableToExpressionMap { public: @@ -58,7 +59,8 @@ namespace storm { // A visitor that can be used to translate expressions to rational functions. mutable ToRationalFunctionVisitor rationalFunctionVisitor; }; +#endif } } -#endif /* STORM_STORAGE_EXPRESSIONS_EXPRESSIONEVALUATOR_H_ */ \ No newline at end of file +#endif /* STORM_STORAGE_EXPRESSIONS_EXPRESSIONEVALUATOR_H_ */ diff --git a/src/storage/expressions/ExpressionEvaluatorBase.cpp b/src/storage/expressions/ExpressionEvaluatorBase.cpp index d98810886..aeca1b656 100644 --- a/src/storage/expressions/ExpressionEvaluatorBase.cpp +++ b/src/storage/expressions/ExpressionEvaluatorBase.cpp @@ -16,7 +16,10 @@ namespace storm { } template class ExpressionEvaluatorBase; + +#ifdef STORM_HAVE_CARL template class ExpressionEvaluatorBase; template class ExpressionEvaluatorBase; +#endif } -} \ No newline at end of file +} diff --git a/src/storage/expressions/ExprtkExpressionEvaluator.cpp b/src/storage/expressions/ExprtkExpressionEvaluator.cpp index 942c17172..d24bc742c 100755 --- a/src/storage/expressions/ExprtkExpressionEvaluator.cpp +++ b/src/storage/expressions/ExprtkExpressionEvaluator.cpp @@ -83,7 +83,10 @@ namespace storm { } template class ExprtkExpressionEvaluatorBase; + +#ifdef STORM_HAVE_CARL template class ExprtkExpressionEvaluatorBase; template class ExprtkExpressionEvaluatorBase; +#endif } -} \ No newline at end of file +} diff --git a/src/storage/expressions/ToRationalFunctionVisitor.cpp b/src/storage/expressions/ToRationalFunctionVisitor.cpp index 71e052bee..1a3dd0fc3 100644 --- a/src/storage/expressions/ToRationalFunctionVisitor.cpp +++ b/src/storage/expressions/ToRationalFunctionVisitor.cpp @@ -7,6 +7,8 @@ namespace storm { namespace expressions { + +#ifdef STORM_HAVE_CARL template ToRationalFunctionVisitor::ToRationalFunctionVisitor() : ExpressionVisitor(), cache(new carl::Cache>()) { // Intentionally left empty. @@ -95,6 +97,6 @@ namespace storm { } template class ToRationalFunctionVisitor; - +#endif } } diff --git a/src/storage/expressions/ToRationalFunctionVisitor.h b/src/storage/expressions/ToRationalFunctionVisitor.h index 6bd3a205b..12603f44e 100644 --- a/src/storage/expressions/ToRationalFunctionVisitor.h +++ b/src/storage/expressions/ToRationalFunctionVisitor.h @@ -10,6 +10,7 @@ namespace storm { namespace expressions { +#ifdef STORM_HAVE_CARL template class ToRationalFunctionVisitor : public ExpressionVisitor { public: @@ -45,7 +46,8 @@ namespace storm { // The cache that is used in case the underlying type needs a cache. std::shared_ptr>> cache; }; +#endif } } -#endif /* STORM_STORAGE_EXPRESSIONS_TORATIONALFUNCTIONVISITOR_H_ */ \ No newline at end of file +#endif /* STORM_STORAGE_EXPRESSIONS_TORATIONALFUNCTIONVISITOR_H_ */ diff --git a/src/storage/expressions/ToRationalNumberVisitor.cpp b/src/storage/expressions/ToRationalNumberVisitor.cpp index b17ec335a..785f36950 100644 --- a/src/storage/expressions/ToRationalNumberVisitor.cpp +++ b/src/storage/expressions/ToRationalNumberVisitor.cpp @@ -2,6 +2,7 @@ #include "src/utility/macros.h" #include "src/exceptions/InvalidArgumentException.h" +#include "src/exceptions/NotSupportedException.h" namespace storm { namespace expressions { @@ -52,7 +53,7 @@ namespace storm { template boost::any ToRationalNumberVisitor::visit(BinaryRelationExpression const& expression) { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function."); + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational number."); } template @@ -62,30 +63,39 @@ namespace storm { template boost::any ToRationalNumberVisitor::visit(UnaryBooleanFunctionExpression const& expression) { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function."); + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational number."); } template boost::any ToRationalNumberVisitor::visit(UnaryNumericalFunctionExpression const& expression) { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function."); + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational number."); } template boost::any ToRationalNumberVisitor::visit(BooleanLiteralExpression const& expression) { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function."); + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational number."); } template boost::any ToRationalNumberVisitor::visit(IntegerLiteralExpression const& expression) { +#ifdef STORM_HAVE_CARL return RationalNumberType(carl::rationalize(static_cast(expression.getValue()))); +#else + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Rational numbers are not supported in this build."); +#endif } template boost::any ToRationalNumberVisitor::visit(DoubleLiteralExpression const& expression) { +#ifdef STORM_HAVE_CARL return RationalNumberType(carl::rationalize(expression.getValue())); +#else + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Rational numbers are not supported in this build."); +#endif } +#ifdef STORM_HAVE_CARL template class ToRationalNumberVisitor; - +#endif } } diff --git a/src/storage/gspn/GSPN.h b/src/storage/gspn/GSPN.h index d81f93ad6..b8845cbff 100644 --- a/src/storage/gspn/GSPN.h +++ b/src/storage/gspn/GSPN.h @@ -3,6 +3,7 @@ #include #include +#include #include "src/storage/gspn/ImmediateTransition.h" #include "src/storage/gspn/Marking.h" diff --git a/src/storage/gspn/ImmediateTransition.h b/src/storage/gspn/ImmediateTransition.h index ea79d57bf..cf4839181 100644 --- a/src/storage/gspn/ImmediateTransition.h +++ b/src/storage/gspn/ImmediateTransition.h @@ -2,6 +2,7 @@ #define STORM_STORAGE_GSPN_IMMEDIATETRANSITION_H_ #include "src/storage/gspn/Transition.h" +#include "src/utility/constants.h" namespace storm { namespace gspn { @@ -25,8 +26,15 @@ namespace storm { WeightType getWeight() const { return this->weight; } + + /** + * True iff no weight is attached. + */ + bool noWeightAttached() { + return storm::utility::isZero(weight); + } private: - // the weight of the transition + // the weight of the transition. Must be positive, if zero, then no weight is attached. WeightType weight; }; } diff --git a/src/storage/gspn/Marking.h b/src/storage/gspn/Marking.h index 2e5095e50..04d6ac08e 100644 --- a/src/storage/gspn/Marking.h +++ b/src/storage/gspn/Marking.h @@ -3,6 +3,7 @@ #include #include +#include #include "src/storage/BitVector.h" namespace storm { diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp index 6b6f74d46..1bad1c994 100644 --- a/src/storm-dyftee.cpp +++ b/src/storm-dyftee.cpp @@ -139,7 +139,11 @@ int main(const int argc, const char** argv) { // From this point on we are ready to carry out the actual computations. if (parametric) { +#ifdef STORM_HAVE_CARL analyzeDFT(dftSettings.getDftFilename(), pctlFormula, dftSettings.useSymmetryReduction(), allowModular && dftSettings.useModularisation(), !dftSettings.isDisableDC() ); +#else + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameters are not supported in this build."); +#endif } else { analyzeDFT(dftSettings.getDftFilename(), pctlFormula, dftSettings.useSymmetryReduction(), allowModular && dftSettings.useModularisation(), !dftSettings.isDisableDC()); } diff --git a/src/utility/constants.cpp b/src/utility/constants.cpp index f3db552ed..436cfcce0 100644 --- a/src/utility/constants.cpp +++ b/src/utility/constants.cpp @@ -1,307 +1,316 @@ - #include "src/utility/constants.h" - - #include "src/storage/sparse/StateType.h" - #include "src/storage/SparseMatrix.h" - #include "src/settings/SettingsManager.h" - #include "src/settings/modules/GeneralSettings.h" - - #include "src/adapters/CarlAdapter.h" - - namespace storm { - namespace utility { - - template - ValueType one() { - return ValueType(1); - } - - template - ValueType zero() { - return ValueType(0); - } - - template - ValueType infinity() { - return std::numeric_limits::infinity(); - } - - template - bool isOne(ValueType const& a) { - return a == one(); - } - - template - bool isZero(ValueType const& a) { - return a == zero(); - } - - template - bool isConstant(ValueType const& a) { - return true; - } - - template<> - bool isOne(storm::RationalNumber const& a) { - return carl::isOne(a); - } - - template<> - bool isZero(storm::RationalNumber const& a) { - return carl::isZero(a); - } - - template<> - storm::RationalNumber infinity() { - // FIXME: this should be treated more properly. - return storm::RationalNumber(-1); - } - - template<> - bool isOne(storm::RationalFunction const& a) { - return a.isOne(); - } - - template<> - bool isZero(storm::RationalFunction const& a) { - return a.isZero(); - } - - template<> - bool isConstant(storm::RationalFunction const& a) { - return a.isConstant(); - } - - template<> - bool isOne(storm::Polynomial const& a) { - return a.isOne(); - } - - template<> - bool isZero(storm::Polynomial const& a) { - return a.isZero(); - } - - template<> - bool isConstant(storm::Polynomial const& a) { - return a.isConstant(); - } - - template<> - storm::RationalFunction infinity() { - //FIXME: this should be treated more properly. - return storm::RationalFunction(-1.0); - } - - template - ValueType pow(ValueType const& value, uint_fast64_t exponent) { - assert(false); - //return std::pow(value, exponent); - } - - template - ValueType simplify(ValueType value) { - // In the general case, we don't do anything here, but merely return the value. If something else is - // supposed to happen here, the templated function can be specialized for this particular type. - return value; - } - - template<> - double convertNumber(double const& number){ - return number; - } - - template - ValueType abs(ValueType const& number) { - return carl::abs(number); - } - - template<> - RationalFunction& simplify(RationalFunction& value); - - template<> - RationalFunction&& simplify(RationalFunction&& value); - - template<> - RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent) { - return carl::pow(value, exponent); - } - - template<> - RationalFunction simplify(RationalFunction value) { - value.simplify(); - return value; - } - - template<> - RationalFunction& simplify(RationalFunction& value) { - value.simplify(); - return value; - } - - template<> - RationalFunction&& simplify(RationalFunction&& value) { - value.simplify(); - return std::move(value); - } - - template<> - double convertNumber(RationalNumber const& number){ - return carl::toDouble(number); - } - - template<> - RationalNumber convertNumber(double const& number){ - return carl::rationalize(number); - } - - template<> - RationalFunction convertNumber(double const& number){ - return RationalFunction(carl::rationalize(number)); - } - - template<> - storm::RationalNumber abs(storm::RationalNumber const& number) { - return carl::abs(number); - } - - template - storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry) { - simplify(matrixEntry.getValue()); - return matrixEntry; - } - - template - storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry) { - simplify(matrixEntry.getValue()); - return matrixEntry; - } - - template - storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry) { - simplify(matrixEntry.getValue()); - return std::move(matrixEntry); - } - - // Explicit instantiations. - template bool isOne(double const& value); - template bool isZero(double const& value); - template bool isConstant(double const& value); - - template double one(); - template double zero(); - template double infinity(); - - template double pow(double const& value, uint_fast64_t exponent); - - template double simplify(double value); - - template storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry); - template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); - template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); - - template double abs(double const& number); - - template bool isOne(float const& value); - template bool isZero(float const& value); - template bool isConstant(float const& value); - - template float one(); - template float zero(); - template float infinity(); - - template float pow(float const& value, uint_fast64_t exponent); - - template float simplify(float value); - - template storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry); - template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); - template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); - - template bool isOne(int const& value); - template bool isZero(int const& value); - template bool isConstant(int const& value); - - template int one(); - template int zero(); - template int infinity(); - - template int pow(int const& value, uint_fast64_t exponent); - - template int simplify(int value); - - template storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry); - template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); - template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); - - template bool isOne(storm::storage::sparse::state_type const& value); - template bool isZero(storm::storage::sparse::state_type const& value); - template bool isConstant(storm::storage::sparse::state_type const& value); - - template uint32_t one(); - template uint32_t zero(); - template uint32_t infinity(); - - template storm::storage::sparse::state_type one(); - template storm::storage::sparse::state_type zero(); - template storm::storage::sparse::state_type infinity(); - - template storm::storage::sparse::state_type pow(storm::storage::sparse::state_type const& value, uint_fast64_t exponent); - - template storm::storage::sparse::state_type simplify(storm::storage::sparse::state_type value); - - template storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry); - template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); - template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); - - // Instantiations for rational number. - template bool isOne(storm::RationalNumber const& value); - template bool isZero(storm::RationalNumber const& value); - template bool isConstant(storm::RationalNumber const& value); - - template storm::RationalNumber one(); - template storm::RationalNumber zero(); - template storm::RationalNumber infinity(); - - template double convertNumber(storm::RationalNumber const& number); - template storm::RationalNumber convertNumber(double const& number); - - template storm::RationalNumber abs(storm::RationalNumber const& number); - - template storm::RationalNumber pow(storm::RationalNumber const& value, uint_fast64_t exponent); - - template storm::RationalNumber simplify(storm::RationalNumber value); - template storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry); - template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); - template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); - - #ifdef STORM_HAVE_CARL - template bool isOne(RationalFunction const& value); - template bool isZero(RationalFunction const& value); - template bool isConstant(RationalFunction const& value); - - template RationalFunction one(); - template RationalFunction zero(); - template storm::RationalFunction infinity(); - - template RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent); - template RationalFunction simplify(RationalFunction value); - template RationalFunction& simplify(RationalFunction& value); - template RationalFunction&& simplify(RationalFunction&& value); - - template Polynomial one(); - template Polynomial zero(); - - template bool isOne(Interval const& value); - template bool isZero(Interval const& value); - template bool isConstant(Interval const& value); - - template Interval one(); - template Interval zero(); - - template storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry); - template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); - template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); - #endif - - } - } +#include "src/utility/constants.h" + +#include "src/storage/sparse/StateType.h" +#include "src/storage/SparseMatrix.h" +#include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" + +#include "src/adapters/CarlAdapter.h" + +namespace storm { + namespace utility { + + template + ValueType one() { + return ValueType(1); + } + + template + ValueType zero() { + return ValueType(0); + } + + template + ValueType infinity() { + return std::numeric_limits::infinity(); + } + + template + bool isOne(ValueType const& a) { + return a == one(); + } + + template + bool isZero(ValueType const& a) { + return a == zero(); + } + + template + bool isConstant(ValueType const& a) { + return true; + } + +#ifdef STORM_HAVE_CARL + template<> + bool isOne(storm::RationalNumber const& a) { + return carl::isOne(a); + } + + template<> + bool isZero(storm::RationalNumber const& a) { + return carl::isZero(a); + } + + template<> + storm::RationalNumber infinity() { + // FIXME: this should be treated more properly. + return storm::RationalNumber(-1); + } + + template<> + bool isOne(storm::RationalFunction const& a) { + return a.isOne(); + } + + template<> + bool isZero(storm::RationalFunction const& a) { + return a.isZero(); + } + + template<> + bool isConstant(storm::RationalFunction const& a) { + return a.isConstant(); + } + + template<> + bool isOne(storm::Polynomial const& a) { + return a.isOne(); + } + + template<> + bool isZero(storm::Polynomial const& a) { + return a.isZero(); + } + + template<> + bool isConstant(storm::Polynomial const& a) { + return a.isConstant(); + } + + template<> + storm::RationalFunction infinity() { + // FIXME: this should be treated more properly. + return storm::RationalFunction(-1.0); + } +#endif + + template + ValueType pow(ValueType const& value, uint_fast64_t exponent) { + return std::pow(value, exponent); + } + + template + ValueType simplify(ValueType value) { + // In the general case, we don't do anything here, but merely return the value. If something else is + // supposed to happen here, the templated function can be specialized for this particular type. + return value; + } + + template<> + double convertNumber(double const& number){ + return number; + } + + template + ValueType abs(ValueType const& number) { + return std::fabs(number); + } + +#ifdef STORM_HAVE_CARL + template<> + RationalNumber pow(RationalNumber const& value, uint_fast64_t exponent) { + return carl::pow(value, exponent); + } + + template<> + RationalFunction& simplify(RationalFunction& value); + + template<> + RationalFunction&& simplify(RationalFunction&& value); + + template<> + RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent) { + return carl::pow(value, exponent); + } + + template<> + RationalFunction simplify(RationalFunction value) { + value.simplify(); + return value; + } + + template<> + RationalFunction& simplify(RationalFunction& value) { + value.simplify(); + return value; + } + + template<> + RationalFunction&& simplify(RationalFunction&& value) { + value.simplify(); + return std::move(value); + } + + template<> + double convertNumber(RationalNumber const& number){ + return carl::toDouble(number); + } + + template<> + RationalNumber convertNumber(double const& number){ + return carl::rationalize(number); + } + + template<> + RationalFunction convertNumber(double const& number){ + return RationalFunction(carl::rationalize(number)); + } + + template<> + storm::RationalNumber abs(storm::RationalNumber const& number) { + return carl::abs(number); + } +#endif + + template + storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry) { + simplify(matrixEntry.getValue()); + return matrixEntry; + } + + template + storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry) { + simplify(matrixEntry.getValue()); + return matrixEntry; + } + + template + storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry) { + simplify(matrixEntry.getValue()); + return std::move(matrixEntry); + } + + // Explicit instantiations. + template bool isOne(double const& value); + template bool isZero(double const& value); + template bool isConstant(double const& value); + + template double one(); + template double zero(); + template double infinity(); + + template double pow(double const& value, uint_fast64_t exponent); + + template double simplify(double value); + + template storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry); + template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); + template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); + + template double abs(double const& number); + + template bool isOne(float const& value); + template bool isZero(float const& value); + template bool isConstant(float const& value); + + template float one(); + template float zero(); + template float infinity(); + + template float pow(float const& value, uint_fast64_t exponent); + + template float simplify(float value); + + template storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry); + template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); + template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); + + template bool isOne(int const& value); + template bool isZero(int const& value); + template bool isConstant(int const& value); + + template int one(); + template int zero(); + template int infinity(); + + template int pow(int const& value, uint_fast64_t exponent); + + template int simplify(int value); + + template storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry); + template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); + template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); + + template bool isOne(storm::storage::sparse::state_type const& value); + template bool isZero(storm::storage::sparse::state_type const& value); + template bool isConstant(storm::storage::sparse::state_type const& value); + + template uint32_t one(); + template uint32_t zero(); + template uint32_t infinity(); + + template storm::storage::sparse::state_type one(); + template storm::storage::sparse::state_type zero(); + template storm::storage::sparse::state_type infinity(); + + template storm::storage::sparse::state_type pow(storm::storage::sparse::state_type const& value, uint_fast64_t exponent); + + template storm::storage::sparse::state_type simplify(storm::storage::sparse::state_type value); + + template storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry); + template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); + template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); + +#ifdef STORM_HAVE_CARL + // Instantiations for rational number. + template bool isOne(storm::RationalNumber const& value); + template bool isZero(storm::RationalNumber const& value); + template bool isConstant(storm::RationalNumber const& value); + + template storm::RationalNumber one(); + template storm::RationalNumber zero(); + template storm::RationalNumber infinity(); + + template double convertNumber(storm::RationalNumber const& number); + template storm::RationalNumber convertNumber(double const& number); + + template storm::RationalNumber abs(storm::RationalNumber const& number); + + template storm::RationalNumber pow(storm::RationalNumber const& value, uint_fast64_t exponent); + + template storm::RationalNumber simplify(storm::RationalNumber value); + template storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry); + template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); + template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); + + // Instantiations for rational function. + template bool isOne(RationalFunction const& value); + template bool isZero(RationalFunction const& value); + template bool isConstant(RationalFunction const& value); + + template RationalFunction one(); + template RationalFunction zero(); + template storm::RationalFunction infinity(); + + template RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent); + template RationalFunction simplify(RationalFunction value); + template RationalFunction& simplify(RationalFunction& value); + template RationalFunction&& simplify(RationalFunction&& value); + + template Polynomial one(); + template Polynomial zero(); + + template bool isOne(Interval const& value); + template bool isZero(Interval const& value); + template bool isConstant(Interval const& value); + + template Interval one(); + template Interval zero(); + + template storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry); + template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); + template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); +#endif + + } +} diff --git a/src/utility/graph.cpp b/src/utility/graph.cpp index 8a7e1e185..79b4a32a0 100644 --- a/src/utility/graph.cpp +++ b/src/utility/graph.cpp @@ -22,6 +22,8 @@ #include "src/utility/macros.h" #include "src/exceptions/InvalidArgumentException.h" +#include + namespace storm { namespace utility { namespace graph { @@ -1180,24 +1182,21 @@ namespace storm { template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix) ; // Instantiations for storm::RationalNumber. +#ifdef STORM_HAVE_CARL template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, bool useStepBound, uint_fast64_t maximalSteps); template storm::storage::BitVector getBsccCover(storm::storage::SparseMatrix const& transitionMatrix); template std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, boost::optional const& subsystem); - template storm::storage::BitVector performProbGreater0(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0); template storm::storage::BitVector performProb1(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& statesWithProbabilityGreater0); - template storm::storage::BitVector performProb1(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - template std::pair performProb01(storm::models::sparse::DeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - template std::pair performProb01(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template storm::storage::PartialScheduler computeSchedulerProbGreater0E(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional const& rowFilter); @@ -1214,33 +1213,27 @@ namespace storm { template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - template storm::storage::BitVector performProb1E(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template std::pair performProb01Max(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - template std::pair performProb01Max(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; template storm::storage::BitVector performProbGreater0A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0); - template storm::storage::BitVector performProb0E(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - template storm::storage::BitVector performProb0E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; + template storm::storage::BitVector performProb0E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; template storm::storage::BitVector performProb1A( storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template std::pair performProb01Min(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - template std::pair performProb01Min(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix); // End of instantiations for storm::RationalNumber. -#ifdef STORM_HAVE_CARL template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, bool useStepBound, uint_fast64_t maximalSteps); template storm::storage::BitVector getBsccCover(storm::storage::SparseMatrix const& transitionMatrix); diff --git a/src/utility/parametric.h b/src/utility/parametric.h index 244e1c141..0805ec34d 100644 --- a/src/utility/parametric.h +++ b/src/utility/parametric.h @@ -10,6 +10,7 @@ #include "src/adapters/CarlAdapter.h" +#include namespace storm { namespace utility { diff --git a/src/utility/prism.cpp b/src/utility/prism.cpp index 947d7e8a2..a34f5e531 100644 --- a/src/utility/prism.cpp +++ b/src/utility/prism.cpp @@ -9,6 +9,8 @@ #include "src/exceptions/InvalidArgumentException.h" +#include + namespace storm { namespace utility { namespace prism { @@ -82,4 +84,4 @@ namespace storm { } } -} \ No newline at end of file +} diff --git a/src/utility/stateelimination.cpp b/src/utility/stateelimination.cpp index 7076c3f15..e70bc6b02 100644 --- a/src/utility/stateelimination.cpp +++ b/src/utility/stateelimination.cpp @@ -202,6 +202,7 @@ namespace storm { template std::vector getDistanceBasedPriorities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector const& oneStepProbabilities, bool forward, bool reverse); template std::vector getStateDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector const& oneStepProbabilities, bool forward); +#ifdef STORM_HAVE_CARL template uint_fast64_t estimateComplexity(storm::RationalNumber const& value); template std::shared_ptr createStatePriorityQueue(boost::optional> const& distanceBasedStatePriorities, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities, storm::storage::BitVector const& states); template uint_fast64_t computeStatePenalty(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities); @@ -215,6 +216,7 @@ namespace storm { template uint_fast64_t computeStatePenaltyRegularExpression(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities); template std::vector getDistanceBasedPriorities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector const& oneStepProbabilities, bool forward, bool reverse); template std::vector getStateDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector const& oneStepProbabilities, bool forward); +#endif } } -} \ No newline at end of file +} diff --git a/src/utility/storm.h b/src/utility/storm.h index 6dd9dc526..b2f160008 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -220,6 +220,7 @@ namespace storm { } } +#ifdef STORM_HAVE_CARL template<> inline void generateCounterexample(storm::prism::Program const& program, std::shared_ptr> model, std::shared_ptr const& formula) { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for parametric model."); @@ -229,6 +230,7 @@ namespace storm { inline void generateCounterexample(storm::prism::Program const& program, std::shared_ptr> model, std::shared_ptr const& formula) { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for parametric model."); } +#endif template void generateCounterexamples(storm::prism::Program const& program, std::shared_ptr> model, std::vector> const& formulas) { @@ -332,6 +334,7 @@ namespace storm { } +#ifdef STORM_HAVE_CARL template<> inline std::unique_ptr verifySparseModel(std::shared_ptr> model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant) { storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); @@ -349,7 +352,6 @@ namespace storm { return result; } -#ifdef STORM_HAVE_CARL inline void exportParametricResultToFile(storm::RationalFunction const& result, storm::models::sparse::Dtmc::ConstraintCollector const& constraintCollector, std::string const& path) { std::ofstream filestream; filestream.open(path); diff --git a/test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp index 8caa788bb..b66c71f09 100644 --- a/test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp @@ -60,6 +60,7 @@ TEST(EigenDtmcPrctlModelCheckerTest, Die) { EXPECT_NEAR(11.0 / 3.0, quantitativeResult4[0], storm::settings::getModule().getPrecision()); } +#ifdef STORM_HAVE_CARL TEST(EigenDtmcPrctlModelCheckerTest, Die_RationalNumber) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); @@ -159,7 +160,7 @@ TEST(EigenDtmcPrctlModelCheckerTest, Die_RationalFunction) { EXPECT_EQ(storm::RationalNumber(11) / storm::RationalNumber(3), quantitativeResult4[0].evaluate(instantiation)); } - +#endif TEST(EigenDtmcPrctlModelCheckerTest, Crowds) { std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.lab", "", ""); diff --git a/test/functional/solver/EigenLinearEquationSolverTest.cpp b/test/functional/solver/EigenLinearEquationSolverTest.cpp index 33d073c62..2cd90dc36 100644 --- a/test/functional/solver/EigenLinearEquationSolverTest.cpp +++ b/test/functional/solver/EigenLinearEquationSolverTest.cpp @@ -64,6 +64,7 @@ TEST(EigenLinearEquationSolver, SparseLU) { ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule().getPrecision()); } +#ifdef STORM_HAVE_CARL TEST(EigenLinearEquationSolver, SparseLU_RationalNumber) { ASSERT_NO_THROW(storm::storage::SparseMatrixBuilder builder); storm::storage::SparseMatrixBuilder builder; @@ -115,6 +116,7 @@ TEST(EigenLinearEquationSolver, SparseLU_RationalFunction) { ASSERT_TRUE(x[1] == storm::RationalFunction(3)); ASSERT_TRUE(x[2] == storm::RationalFunction(-1)); } +#endif TEST(EigenLinearEquationSolver, DGMRES) { ASSERT_NO_THROW(storm::storage::SparseMatrixBuilder builder); @@ -412,4 +414,4 @@ TEST(EigenLinearEquationSolver, MatrixVectorMultiplication) { storm::solver::EigenLinearEquationSolver solver(A); ASSERT_NO_THROW(solver.repeatedMultiply(x, nullptr, 4)); ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule().getPrecision()); -} \ No newline at end of file +}