From d3fc2d8fbffe936d023993ad27964292f24c58a3 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 22 Oct 2014 09:50:48 +0200 Subject: [PATCH] Fixed small but important bug in SCC decomposition that led to wrong results when using MSVC. Former-commit-id: 07358dc2e830ff3c2e1e3f224bf2c4117f8af4fa --- CMakeLists.txt | 17 ++--- src/storage/StronglyConnectedComponent.cpp | 4 + src/storage/StronglyConnectedComponent.h | 2 +- src/utility/ConstantsComparator.cpp | 85 ++++++++++++++++++++++ src/utility/ConstantsComparator.h | 54 +++++--------- 5 files changed, 116 insertions(+), 46 deletions(-) create mode 100644 src/utility/ConstantsComparator.cpp diff --git a/CMakeLists.txt b/CMakeLists.txt index 2864e3882..61516b10c 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -96,11 +96,9 @@ if(CMAKE_COMPILER_IS_GNUCC) set(STORM_COMPILED_BY "GCC") # Set standard flags for GCC set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops") - set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++11 -Wall -pedantic -DBOOST_RESULT_OF_USE_DECLTYPE") - # -Werror is atm removed as this gave some problems with existing code - # May be re-set later - # (Thomas Heinemann, 2012-12-21) - + add_definitions(-DBOOST_RESULT_OF_USE_DECLTYPE) + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++11 -Wall -pedantic") + # Turn on popcnt instruction if desired (yes by default) if (STORM_USE_POPCNT) set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -mpopcnt") @@ -118,6 +116,8 @@ elseif(MSVC) add_definitions(/D_VARIADIC_MAX=10) # Windows.h breaks GMM in gmm_except.h because of its macro definition for min and max add_definitions(/DNOMINMAX) + # required for using boost's transform iterator + add_definitions(/DBOOST_RESULT_OF_USE_DECLTYPE) # since nobody cares at the moment add_definitions(/wd4250) @@ -146,10 +146,9 @@ else(CLANG) set(CMAKE_XCODE_ATTRIBUTE_CLANG_CXX_LIBRARY "libc++") endif() - set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++11 -stdlib=${CLANG_STDLIB} -Wall -pedantic -Wno-unused-variable -DBOOST_RESULT_OF_USE_DECLTYPE -ftemplate-depth=1024") - - set (CMAKE_CXX_FLAGS_DEBUG "${CMAKE_CXX_FLAGS_DEBUG} -g") - + add_definitions(-DBOOST_RESULT_OF_USE_DECLTYPE) + set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++11 -stdlib=${CLANG_STDLIB} -Wall -pedantic -Wno-unused-variable -ftemplate-depth=1024") + # Turn on popcnt instruction if desired (yes by default) if (STORM_USE_POPCNT) set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -mpopcnt") diff --git a/src/storage/StronglyConnectedComponent.cpp b/src/storage/StronglyConnectedComponent.cpp index 6540a8acf..8661ebd0e 100644 --- a/src/storage/StronglyConnectedComponent.cpp +++ b/src/storage/StronglyConnectedComponent.cpp @@ -2,6 +2,10 @@ namespace storm { namespace storage { + StronglyConnectedComponent::StronglyConnectedComponent() : isTrivialScc(false) { + // Intentionally left empty. + } + void StronglyConnectedComponent::setIsTrivial(bool trivial) { this->isTrivialScc = trivial; } diff --git a/src/storage/StronglyConnectedComponent.h b/src/storage/StronglyConnectedComponent.h index 1a81742c9..dfbede4a9 100644 --- a/src/storage/StronglyConnectedComponent.h +++ b/src/storage/StronglyConnectedComponent.h @@ -14,7 +14,7 @@ namespace storm { */ class StronglyConnectedComponent : public StateBlock { public: - StronglyConnectedComponent() = default; + StronglyConnectedComponent(); StronglyConnectedComponent(StronglyConnectedComponent const& other) = default; #ifndef WINDOWS StronglyConnectedComponent(StronglyConnectedComponent&& other) = default; diff --git a/src/utility/ConstantsComparator.cpp b/src/utility/ConstantsComparator.cpp new file mode 100644 index 000000000..77d76ab22 --- /dev/null +++ b/src/utility/ConstantsComparator.cpp @@ -0,0 +1,85 @@ +#include "src/utility/ConstantsComparator.h" + +#include "src/storage/sparse/StateType.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<> + double simplify(double value) { + // In the general case, we don't to 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 + bool ConstantsComparator::isOne(ValueType const& value) const { + return value == one(); + } + + template + bool ConstantsComparator::isZero(ValueType const& value) const { + return value == zero(); + } + + template + bool ConstantsComparator::isEqual(ValueType const& value1, ValueType const& value2) const { + return value1 == value2; + } + + ConstantsComparator::ConstantsComparator() : precision(storm::settings::generalSettings().getPrecision()) { + // Intentionally left empty. + } + + ConstantsComparator::ConstantsComparator(double precision) : precision(precision) { + // Intentionally left empty. + } + + bool ConstantsComparator::isOne(double const& value) const { + return std::abs(value - one()) <= precision; + } + + bool ConstantsComparator::isZero(double const& value) const { + return std::abs(value) <= precision; + } + + bool ConstantsComparator::isEqual(double const& value1, double const& value2) const { + return std::abs(value1 - value2) <= precision; + } + + bool ConstantsComparator::isConstant(double const& value) const { + return true; + } + + template + storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry) { + simplify(matrixEntry.getValue()); + return matrixEntry; + } + + template class ConstantsComparator; + + template double one(); + template double zero(); + template double infinity(); + + template double simplify(double value); + + template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); + } +} \ No newline at end of file diff --git a/src/utility/ConstantsComparator.h b/src/utility/ConstantsComparator.h index 2da8fc084..a25e0ac91 100644 --- a/src/utility/ConstantsComparator.h +++ b/src/utility/ConstantsComparator.h @@ -13,75 +13,57 @@ #include #include "src/settings/SettingsManager.h" +#include "src/storage/SparseMatrix.h" namespace storm { namespace utility { template - ValueType one() { - return ValueType(1); - } + ValueType one(); template - ValueType zero() { - return ValueType(0); - } + ValueType zero(); template - ValueType infinity() { - return std::numeric_limits::infinity(); - } + ValueType infinity(); + template + ValueType simplify(ValueType value); + // A class that can be used for comparing constants. template class ConstantsComparator { public: - bool isOne(ValueType const& value) const { - return value == one(); - } + bool isOne(ValueType const& value) const; - bool isZero(ValueType const& value) const { - return value == zero(); - } + bool isZero(ValueType const& value) const; - bool isEqual(ValueType const& value1, ValueType const& value2) const { - return value1 == value2; - } + bool isEqual(ValueType const& value1, ValueType const& value2) const; }; // For doubles we specialize this class and consider the comparison modulo some predefined precision. template<> class ConstantsComparator { public: - ConstantsComparator() : precision(storm::settings::generalSettings().getPrecision()) { - // Intentionally left empty. - } + ConstantsComparator(); - ConstantsComparator(double precision) : precision(precision) { - // Intentionally left empty. - } + ConstantsComparator(double precision); - bool isOne(double const& value) const { - return std::abs(value - one()) <= precision; - } + bool isOne(double const& value) const; - bool isZero(double const& value) const { - return std::abs(value) <= precision; - } + bool isZero(double const& value) const; - bool isEqual(double const& value1, double const& value2) const { - return std::abs(value1 - value2) <= precision; - } + bool isEqual(double const& value1, double const& value2) const; - bool isConstant(double const& value) const { - return true; - } + bool isConstant(double const& value) const; private: // The precision used for comparisons. double precision; }; + template + storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); } }