Fixed small but important bug in SCC decomposition that led to wrong results when using MSVC.

Former-commit-id: 07358dc2e8

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")

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