Merge branch 'master' of https://sselab.de/lab9/private/git/storm

Conflicts:
	CMakeLists.txt

Former-commit-id: b88be0c91f

CMakeLists.txt

@@ -96,10 +96,8 @@ 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)
@@ -118,7 +116,7 @@ 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)
-	# Boost Defs
+	# Boost Defs, required for using boost's transform iterator
 	add_definitions(/DBOOST_RESULT_OF_USE_DECLTYPE)
 	
 	# since nobody cares at the moment
@@ -148,9 +146,8 @@ 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)

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<typename ValueType>
@@ -48,11 +49,13 @@ namespace storm {
         void DeterministicModelStrongBisimulationDecomposition<ValueType>::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<typename ValueType>
         void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::setEnd(storm::storage::sparse::state_type end) {
             this->end = end;
+            STORM_LOG_ASSERT(begin < end, "Unable to resize block to illegal size.");
         }
         
         template<typename ValueType>
@@ -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<Block>::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<Block>::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<std::pair<storm::storage::sparse::state_type, ValueType>>::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)) {

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;
         }

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;

src/utility/ConstantsComparator.cpp

@@ -0,0 +1,85 @@
+#include "src/utility/ConstantsComparator.h"
+
+#include "src/storage/sparse/StateType.h"
+
+namespace storm {
+    namespace utility {
+        
+        template<typename ValueType>
+        ValueType one() {
+            return ValueType(1);
+        }
+        
+        template<typename ValueType>
+        ValueType zero() {
+            return ValueType(0);
+        }
+        
+        template<typename ValueType>
+        ValueType infinity() {
+            return std::numeric_limits<ValueType>::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<typename ValueType>
+        bool ConstantsComparator<ValueType>::isOne(ValueType const& value) const {
+            return value == one<ValueType>();
+        }
+        
+        template<typename ValueType>
+        bool ConstantsComparator<ValueType>::isZero(ValueType const& value) const {
+            return value == zero<ValueType>();
+        }
+        
+        template<typename ValueType>
+        bool ConstantsComparator<ValueType>::isEqual(ValueType const& value1, ValueType const& value2) const {
+            return value1 == value2;
+        }
+        
+        ConstantsComparator<double>::ConstantsComparator() : precision(storm::settings::generalSettings().getPrecision()) {
+            // Intentionally left empty.
+        }
+        
+        ConstantsComparator<double>::ConstantsComparator(double precision) : precision(precision) {
+            // Intentionally left empty.
+        }
+        
+        bool ConstantsComparator<double>::isOne(double const& value) const {
+            return std::abs(value - one<double>()) <= precision;
+        }
+        
+        bool ConstantsComparator<double>::isZero(double const& value) const {
+            return std::abs(value) <= precision;
+        }
+        
+        bool ConstantsComparator<double>::isEqual(double const& value1, double const& value2) const {
+            return std::abs(value1 - value2) <= precision;
+        }
+        
+        bool ConstantsComparator<double>::isConstant(double const& value) const {
+            return true;
+        }
+        
+        template<typename IndexType, typename ValueType>
+        storm::storage::MatrixEntry<IndexType, ValueType>& simplify(storm::storage::MatrixEntry<IndexType, ValueType>& matrixEntry) {
+            simplify(matrixEntry.getValue());
+            return matrixEntry;
+        }
+        
+        template class ConstantsComparator<double>;
+        
+        template double one();
+        template double zero();
+        template double infinity();
+
+        template double simplify(double value);
+        
+        template storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>& matrixEntry);
+    }
+}

src/utility/ConstantsComparator.h

@@ -13,75 +13,57 @@
 #include <cstdint>
 
 #include "src/settings/SettingsManager.h"
+#include "src/storage/SparseMatrix.h"
 
 namespace storm {
     namespace utility {
         
         template<typename ValueType>
-        ValueType one() {
-            return ValueType(1);
-        }
+        ValueType one();
         
         template<typename ValueType>
-        ValueType zero() {
-            return ValueType(0);
-        }
+        ValueType zero();
         
         template<typename ValueType>
-        ValueType infinity() {
-            return std::numeric_limits<ValueType>::infinity();
-        }
+        ValueType infinity();
+        
+        template<typename ValueType>
+        ValueType simplify(ValueType value);
 
         // A class that can be used for comparing constants.
         template<typename ValueType>
         class ConstantsComparator {
         public:
-            bool isOne(ValueType const& value) const {
-                return value == one<ValueType>();
-            }
+            bool isOne(ValueType const& value) const;
             
-            bool isZero(ValueType const& value) const {
-                return value == zero<ValueType>();
-            }
+            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<double> {
         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<double>()) <= 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<typename IndexType, typename ValueType>
+        storm::storage::MatrixEntry<IndexType, ValueType>& simplify(storm::storage::MatrixEntry<IndexType, ValueType>& matrixEntry);
     }
 }