From d3fc2d8fbffe936d023993ad27964292f24c58a3 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 22 Oct 2014 09:50:48 +0200 Subject: [PATCH 1/2] 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); } } From 754e168aceb150d0a45a869beac05d35ac483708 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 22 Oct 2014 12:51:27 +0200 Subject: [PATCH 2/2] Bugfix for bisimulation. Former-commit-id: da93a5d4db51a3e06e05ca81428451ab1803685a --- ...icModelStrongBisimulationDecomposition.cpp | 29 +++++-------------- 1 file changed, 7 insertions(+), 22 deletions(-) diff --git a/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp b/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp index ea58b778c..1c11a8107 100644 --- a/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp +++ b/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp @@ -23,6 +23,7 @@ namespace storm { if (prev != nullptr) { prev->next = this; } + STORM_LOG_ASSERT(begin < end, "Unable to create block of illegal size."); } template @@ -48,11 +49,13 @@ namespace storm { void DeterministicModelStrongBisimulationDecomposition::Block::setBegin(storm::storage::sparse::state_type begin) { this->begin = begin; this->markedPosition = begin; + STORM_LOG_ASSERT(begin < end, "Unable to resize block to illegal size."); } template void DeterministicModelStrongBisimulationDecomposition::Block::setEnd(storm::storage::sparse::state_type end) { this->end = end; + STORM_LOG_ASSERT(begin < end, "Unable to resize block to illegal size."); } template @@ -401,35 +404,16 @@ namespace storm { return block; } - // We only split off the smaller of the two resulting blocks so we don't have to update large parts of the - // block mapping. - bool insertAfterCurrent = false; - if ((block.getBegin() + position) > ((block.getEnd() - block.getBegin()) / 2)) { - // If the splitting position is far in the back, we create the new block after the one we are splitting. - insertAfterCurrent = true; - } - // Actually create the new block and insert it at the correct position. - typename std::list::iterator selfIt; - if (insertAfterCurrent) { - selfIt = this->blocks.emplace(block.hasNextBlock() ? block.getNextIterator() : this->blocks.end(), position, block.getEnd(), &block, block.getNextBlockPointer(), block.getLabelPtr()); - } else { - selfIt = this->blocks.emplace(block.getIterator(), block.getBegin(), position, block.getPreviousBlockPointer(), &block, block.getLabelPtr()); - } + typename std::list::iterator selfIt = this->blocks.emplace(block.getIterator(), block.getBegin(), position, block.getPreviousBlockPointer(), &block, block.getLabelPtr()); selfIt->setIterator(selfIt); Block& newBlock = *selfIt; // Resize the current block appropriately. - if (insertAfterCurrent) { - block.setEnd(position); - } else { - block.setBegin(position); - } + block.setBegin(position); // Update the mapping of the states in the newly created block. - for (auto it = this->getBegin(newBlock), ite = this->getEnd(newBlock); it != ite; ++it) { - stateToBlockMapping[it->first] = &newBlock; - } + this->updateBlockMapping(newBlock, this->getBegin(newBlock), this->getEnd(newBlock)); return newBlock; } @@ -729,6 +713,7 @@ namespace storm { typename std::vector>::const_iterator end = partition.getEnd(block) - 1; storm::storage::sparse::state_type currentIndex = block.getBegin(); + // Now we can check whether the block needs to be split, which is the case iff the probabilities for the // first and the last state are different. while (!comparator.isEqual(begin->second, end->second)) {