From be0eee21dba3dd0f6cd6b4d84d296faa7012b0eb Mon Sep 17 00:00:00 2001 From: sjunges Date: Wed, 2 Sep 2015 12:44:10 +0200 Subject: [PATCH 1/6] Dont build so many models with float/rational functions Former-commit-id: 692ab47afa67579455a0920710573787a1be76fd --- src/models/sparse/Ctmc.cpp | 6 +++--- src/models/sparse/MarkovAutomaton.cpp | 8 ++++---- src/models/sparse/StochasticTwoPlayerGame.cpp | 8 ++++---- 3 files changed, 11 insertions(+), 11 deletions(-) diff --git a/src/models/sparse/Ctmc.cpp b/src/models/sparse/Ctmc.cpp index 371d48270..9f4ddfcd6 100644 --- a/src/models/sparse/Ctmc.cpp +++ b/src/models/sparse/Ctmc.cpp @@ -40,9 +40,9 @@ namespace storm { template class Ctmc; -#ifdef STORM_HAVE_CARL - template class Ctmc; -#endif +//#ifdef STORM_HAVE_CARL +// template class Ctmc; +//#endif } // namespace sparse } // namespace models diff --git a/src/models/sparse/MarkovAutomaton.cpp b/src/models/sparse/MarkovAutomaton.cpp index 03b9341f2..b04c294f7 100644 --- a/src/models/sparse/MarkovAutomaton.cpp +++ b/src/models/sparse/MarkovAutomaton.cpp @@ -218,11 +218,11 @@ namespace storm { } template class MarkovAutomaton; - template class MarkovAutomaton; +// template class MarkovAutomaton; -#ifdef STORM_HAVE_CARL - template class MarkovAutomaton; -#endif +//#ifdef STORM_HAVE_CARL +// template class MarkovAutomaton; +//#endif } // namespace sparse } // namespace models diff --git a/src/models/sparse/StochasticTwoPlayerGame.cpp b/src/models/sparse/StochasticTwoPlayerGame.cpp index 132410720..ecbb204c5 100644 --- a/src/models/sparse/StochasticTwoPlayerGame.cpp +++ b/src/models/sparse/StochasticTwoPlayerGame.cpp @@ -32,11 +32,11 @@ namespace storm { } template class StochasticTwoPlayerGame; - template class StochasticTwoPlayerGame; +// template class StochasticTwoPlayerGame; -#ifdef STORM_HAVE_CARL - template class StochasticTwoPlayerGame; -#endif +//#ifdef STORM_HAVE_CARL +// template class StochasticTwoPlayerGame; +//#endif } // namespace sparse } // namespace models From 6503d929de9a8e6bab36e195ff77934c4b521555 Mon Sep 17 00:00:00 2001 From: sjunges Date: Wed, 2 Sep 2015 19:16:32 +0200 Subject: [PATCH 2/6] includes the headers for the number types supported by the carl-configuration used on the system Former-commit-id: 18f80e9157a93a73b45ab2147f0c000e10a3c4f7 --- src/adapters/CarlAdapter.h | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/adapters/CarlAdapter.h b/src/adapters/CarlAdapter.h index c0191701a..99e01e575 100644 --- a/src/adapters/CarlAdapter.h +++ b/src/adapters/CarlAdapter.h @@ -6,8 +6,7 @@ #ifdef STORM_HAVE_CARL -#include -#include +#include #include #include #include From ebab145180c4c6253713e9d6732b99ac9c5dbbec Mon Sep 17 00:00:00 2001 From: sjunges Date: Wed, 2 Sep 2015 19:43:45 +0200 Subject: [PATCH 3/6] use default bitvector move, which is fine Former-commit-id: e646a13fb5cef099228987b8cc520989d6ae64d5 --- src/storage/BitVector.cpp | 4 ++-- src/storage/BitVector.h | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/storage/BitVector.cpp b/src/storage/BitVector.cpp index 3e1e9bb5b..ab08e8991 100644 --- a/src/storage/BitVector.cpp +++ b/src/storage/BitVector.cpp @@ -91,9 +91,9 @@ namespace storm { // Intentionally left empty. } - BitVector::BitVector(BitVector&& other) : bitCount(other.bitCount), bucketVector(std::move(other.bucketVector)) { + //BitVector::BitVector(BitVector&& other) : bitCount(other.bitCount), bucketVector(std::move(other.bucketVector)) { // Intentionally left empty. - } + //} BitVector& BitVector::operator=(BitVector const& other) { // Only perform the assignment if the source and target are not identical. diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h index 4c5e64352..d52f07427 100644 --- a/src/storage/BitVector.h +++ b/src/storage/BitVector.h @@ -135,7 +135,7 @@ namespace storm { * * @param other The bit vector from which to move-construct. */ - BitVector(BitVector&& other); + BitVector(BitVector&& other) = default; /*! * Compares the given bit vector with the current one. From 46d8accf6e9f38d06729bb14c9c576c8d531c4ea Mon Sep 17 00:00:00 2001 From: sjunges Date: Wed, 2 Sep 2015 19:44:10 +0200 Subject: [PATCH 4/6] logic::comparisontype operations Former-commit-id: fdcb275bc87656aa32d492120d5a5ed43461c0e2 --- src/logic/ComparisonType.h | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/logic/ComparisonType.h b/src/logic/ComparisonType.h index 61dbe53bb..ccfff25b6 100644 --- a/src/logic/ComparisonType.h +++ b/src/logic/ComparisonType.h @@ -6,7 +6,14 @@ namespace storm { namespace logic { enum class ComparisonType { Less, LessEqual, Greater, GreaterEqual }; - + + inline bool isStrict(ComparisonType t) { + return (t == ComparisonType::Less || t == ComparisonType::Greater); + } + + inline bool isLowerBound(ComparisonType t) { + return (t == ComparisonType::Greater || t == ComparisonType::GreaterEqual); + } std::ostream& operator<<(std::ostream& out, ComparisonType const& comparisonType); } } From bdb105ce85101622dcea76ad53ba424c173a13c3 Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 3 Sep 2015 14:17:47 +0200 Subject: [PATCH 5/6] cmake: marked several variables as advanced Former-commit-id: 8f6c0634725e819c22375db073371b03354a6c74 --- resources/3rdparty/glpk-4.53/CMakeLists.txt | 2 ++ resources/3rdparty/gtest-1.7.0/CMakeLists.txt | 2 ++ resources/3rdparty/log4cplus-1.1.3-rc1/CMakeLists.txt | 2 ++ resources/3rdparty/log4cplus-1.1.3-rc1/ConfigureChecks.cmake | 2 ++ resources/cmake/FindGMP.cmake | 4 +++- 5 files changed, 11 insertions(+), 1 deletion(-) diff --git a/resources/3rdparty/glpk-4.53/CMakeLists.txt b/resources/3rdparty/glpk-4.53/CMakeLists.txt index d206b7615..8302fa365 100644 --- a/resources/3rdparty/glpk-4.53/CMakeLists.txt +++ b/resources/3rdparty/glpk-4.53/CMakeLists.txt @@ -33,6 +33,8 @@ option(DEBUG "Sets whether the DEBUG mode is used" OFF) set(ADDITIONAL_INCLUDE_DIRS "" CACHE STRING "Additional directories added to the include directories.") set(ADDITIONAL_LINK_DIRS "" CACHE STRING "Additional directories added to the link directories.") +MARK_AS_ADVANCED(WITH_GLPK_EXAMPLES WITH_GMP ENABLE_DL ENABLE_ODBC ENABLE_MYSQL) + # If the DEBUG option was turned on, we will target a debug version and a release version otherwise if (DEBUG) set (CMAKE_BUILD_TYPE "DEBUG") diff --git a/resources/3rdparty/gtest-1.7.0/CMakeLists.txt b/resources/3rdparty/gtest-1.7.0/CMakeLists.txt index 05094977b..648d4cd73 100644 --- a/resources/3rdparty/gtest-1.7.0/CMakeLists.txt +++ b/resources/3rdparty/gtest-1.7.0/CMakeLists.txt @@ -22,6 +22,8 @@ option(gtest_build_samples "Build gtest's sample programs." OFF) option(gtest_disable_pthreads "Disable uses of pthreads in gtest." OFF) +MARK_AS_ADVANCED(gtest_build_tests gtest_build_samples gtest_disable_pthreads gtest_force_shared_crt) + # Defines pre_project_set_up_hermetic_build() and set_up_hermetic_build(). include(cmake/hermetic_build.cmake OPTIONAL) diff --git a/resources/3rdparty/log4cplus-1.1.3-rc1/CMakeLists.txt b/resources/3rdparty/log4cplus-1.1.3-rc1/CMakeLists.txt index caf2426c3..269960827 100644 --- a/resources/3rdparty/log4cplus-1.1.3-rc1/CMakeLists.txt +++ b/resources/3rdparty/log4cplus-1.1.3-rc1/CMakeLists.txt @@ -139,3 +139,5 @@ endif (LOG4CPLUS_QT4) if (LOG4CPLUS_DEFINE_INSTALL_TARGET) include(Log4CPlusCPack.cmake) endif() + +MARK_AS_ADVANCED(ENABLE_SYMBOLS_VISIBILITY _WIN32_WINNT WITH_ICONV LOG4CPLUS_WORKING_C_LOCALE LOG4CPLUS_WORKING_LOCALE LOG4CPLUS_BUILD_LOGGINGSERVER LOG4CPLUS_BUILD_TESTING LOG4CPLUS_DEFINE_INSTALL_TARGET LOG4CPLUS_QT4) diff --git a/resources/3rdparty/log4cplus-1.1.3-rc1/ConfigureChecks.cmake b/resources/3rdparty/log4cplus-1.1.3-rc1/ConfigureChecks.cmake index 2090bd6bf..9f1c941ce 100644 --- a/resources/3rdparty/log4cplus-1.1.3-rc1/ConfigureChecks.cmake +++ b/resources/3rdparty/log4cplus-1.1.3-rc1/ConfigureChecks.cmake @@ -380,3 +380,5 @@ set(HAVE_PRETTY_FUNCTION_MACRO ${LOG4CPLUS_HAVE_PRETTY_FUNCTION_MACRO} ) set(HAVE___SYNC_ADD_AND_FETCH ${LOG4CPLUS_HAVE___SYNC_ADD_AND_FETCH} ) set(HAVE___SYNC_SUB_AND_FETCH ${LOG4CPLUS_HAVE___SYNC_SUB_AND_FETCH} ) + +MARK_AS_ADVANCED(LIBADVAPI32 LIBCPOSIX LIBICONV LIBKERNEL32 LIBNSL LIBPOSIX4 LIBRT LIBSOCKET LIBWS2_32) \ No newline at end of file diff --git a/resources/cmake/FindGMP.cmake b/resources/cmake/FindGMP.cmake index 77aaf5034..7f3bc1bfa 100644 --- a/resources/cmake/FindGMP.cmake +++ b/resources/cmake/FindGMP.cmake @@ -51,4 +51,6 @@ elseif(GMP_FOUND) if(GMP_FIND_REQUIRED) message(FATAL_ERROR "Could not find GMP") endif() -endif() \ No newline at end of file +endif() + +MARK_AS_ADVANCED(GMP_MPIRXX_LIBRARY GMP_MPIR_LIBRARY GMP_INCLUDE_DIR GMP_LIBRARY) \ No newline at end of file From dbe997a43307f707774994521fb50a17219f4e03 Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 3 Sep 2015 14:30:51 +0200 Subject: [PATCH 6/6] resolved linker error - sorry Former-commit-id: 6fcb8fa24567cb5dba4510a0d96dd67494a1aae9 --- src/models/sparse/Ctmc.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/models/sparse/Ctmc.cpp b/src/models/sparse/Ctmc.cpp index 9f4ddfcd6..371d48270 100644 --- a/src/models/sparse/Ctmc.cpp +++ b/src/models/sparse/Ctmc.cpp @@ -40,9 +40,9 @@ namespace storm { template class Ctmc; -//#ifdef STORM_HAVE_CARL -// template class Ctmc; -//#endif +#ifdef STORM_HAVE_CARL + template class Ctmc; +#endif } // namespace sparse } // namespace models