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

Former-commit-id: f014b6d412

CMakeLists.txt

@@ -374,7 +374,7 @@ find_package(CLN QUIET)
 set(STORM_USE_CLN_NUMBERS OFF)
 if(CLN_FOUND)
     set(STORM_HAVE_CLN ON)
-	set(STORM_USE_CLN_NUMBERS OFF)
+	set(STORM_USE_CLN_NUMBERS ON)
     message(STATUS "StoRM - Linking with CLN ${CLN_VERSION_STRING}")
     include_directories("${CLN_INCLUDE_DIR}")
     list(APPEND STORM_LINK_LIBRARIES ${CLN_LIBRARIES})

src/solver/stateelimination/EliminatorBase.cpp

@@ -49,7 +49,8 @@ namespace storm {
                 } else if (Mode == ScalingMode::DivideOneMinus) {
                     if (hasEntryInColumn) {
                         STORM_LOG_ASSERT(columnValue != storm::utility::one<ValueType>(), "The scaling mode 'divide-one-minus' requires a non-one value in the given column.");
-                        columnValue = storm::utility::simplify(storm::utility::one<ValueType>() / (storm::utility::one<ValueType>() - columnValue));
+                        columnValue = storm::utility::one<ValueType>() / (storm::utility::one<ValueType>() - columnValue);
+                        columnValue = storm::utility::simplify(columnValue);
                     }
                 }
                 
@@ -57,7 +58,8 @@ namespace storm {
                     for (auto entryIt = entriesInRow.begin(), entryIte = entriesInRow.end(); entryIt != entryIte; ++entryIt) {
                         // Only scale the entries in a different column.
                         if (entryIt->getColumn() != column) {
-                            entryIt->setValue(storm::utility::simplify(entryIt->getValue() * columnValue));
+                            auto tmpVal = entryIt->getValue() * columnValue;
+                            entryIt->setValue(storm::utility::simplify(tmpVal));
                         }
                     }
                     updateValue(column, columnValue);
@@ -145,7 +147,9 @@ namespace storm {
                             *result = *first1;
                             ++first1;
                         } else {
-                            auto probability = storm::utility::simplify(first1->getValue() + storm::utility::simplify(multiplyFactor * first2->getValue()));
+                            ValueType sprod = multiplyFactor * first2->getValue();
+                            ValueType sum = first1->getValue() + storm::utility::simplify(sprod);
+                            auto probability = storm::utility::simplify(sum);
                             *result = storm::storage::MatrixEntry<typename storm::storage::FlexibleSparseMatrix<ValueType>::index_type, typename storm::storage::FlexibleSparseMatrix<ValueType>::value_type>(first1->getColumn(), probability);
                             newBackwardEntries[successorOffsetInNewBackwardTransitions].emplace_back(predecessor, probability);
                             ++first1;

src/solver/stateelimination/LongRunAverageEliminator.cpp

@@ -12,13 +12,16 @@ namespace storm {
             
             template<typename ValueType>
             void LongRunAverageEliminator<ValueType>::updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) {
-                this->stateValues[state] = storm::utility::simplify(loopProbability * this->stateValues[state]);
-                averageTimeInStates[state] = storm::utility::simplify(loopProbability * averageTimeInStates[state]);
+                this->stateValues[state] = loopProbability * this->stateValues[state];
+                this->stateValues[state] = storm::utility::simplify(this->stateValues[state]);
+                averageTimeInStates[state] = loopProbability * averageTimeInStates[state];
+                averageTimeInStates[state] = storm::utility::simplify(averageTimeInStates[state]);
             }
        
             template<typename ValueType>
             void LongRunAverageEliminator<ValueType>::updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) {
-                this->stateValues[predecessor] = storm::utility::simplify(this->stateValues[predecessor] + storm::utility::simplify(probability * this->stateValues[state]));
+                this->stateValues[predecessor] = this->stateValues[predecessor] + storm::utility::simplify(probability * this->stateValues[state]);
+                this->stateValues[predecessor] = storm::utility::simplify(this->stateValues[predecessor]);
                 averageTimeInStates[predecessor] = storm::utility::simplify(averageTimeInStates[predecessor] + storm::utility::simplify(probability * averageTimeInStates[state]));
             }
             

src/utility/constants.cpp

@@ -1,306 +1,307 @@
-//#include "src/utility/constants.h"
-//
-//#include "src/storage/sparse/StateType.h"
-#include "src/storage/SparseMatrix.h"
-//#include "src/settings/SettingsManager.h"
-//#include "src/settings/modules/GeneralSettings.h"
-//
-//#include "src/adapters/CarlAdapter.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<typename ValueType>
-//        bool isOne(ValueType const& a) {
-//            return a == one<ValueType>();
-//        }
-//
-//        template<typename ValueType>
-//        bool isZero(ValueType const& a) {
-//            return a == zero<ValueType>();
-//        }
-//
-//        template<typename ValueType>
-//        bool isConstant(ValueType const& a) {
-//            return true;
-//        }
-//
-//        template<>
-//        bool isOne(storm::RationalNumber const& a) {
-//            return carl::isOne(a);
-//        }
-//
-//        template<>
-//        bool isZero(storm::RationalNumber const& a) {
-//            return carl::isZero(a);
-//        }
-//
-//        template<>
-//        storm::RationalNumber infinity() {
-//            // FIXME: this should be treated more properly.
-//            return storm::RationalNumber(-1);
-//        }
-//
-//        template<>
-//        bool isOne(storm::RationalFunction const& a) {
-//            return a.isOne();
-//        }
-//
-//        template<>
-//        bool isZero(storm::RationalFunction const& a) {
-//            return a.isZero();
-//        }
-//
-//        template<>
-//        bool isConstant(storm::RationalFunction const& a) {
-//            return a.isConstant();
-//        }
-//
-//        template<>
-//        bool isOne(storm::Polynomial const& a) {
-//            return a.isOne();
-//        }
-//
-//        template<>
-//        bool isZero(storm::Polynomial const& a) {
-//            return a.isZero();
-//        }
-//
-//        template<>
-//        bool isConstant(storm::Polynomial const& a) {
-//            return a.isConstant();
-//        }
-//
-//        template<>
-//        storm::RationalFunction infinity() {
-//            // FIXME: this should be treated more properly.
-//            return storm::RationalFunction(-1.0);
-//        }
-//
-//        template<typename ValueType>
-//        ValueType pow(ValueType const& value, uint_fast64_t exponent) {
-//            return std::pow(value, exponent);
-//        }
-//
-//		template<typename ValueType>
-//		ValueType simplify(ValueType value) {
-//            // In the general case, we don't do 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<>
-//        double convertNumber(double const& number){
-//            return number;
-//        }
-//
-//        template<typename ValueType>
-//        ValueType abs(ValueType const& number) {
-//            return carl::abs(number);
-//        }
-//
-//        template<>
-//        RationalFunction& simplify(RationalFunction& value);
-//
-//        template<>
-//        RationalFunction&& simplify(RationalFunction&& value);
-//
-//        template<>
-//        RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent) {
-//            return carl::pow(value, exponent);
-//        }
-//
-//        template<>
-//        RationalFunction simplify(RationalFunction value) {
-//            value.simplify();
-//            return value;
-//        }
-//
-//        template<>
-//        RationalFunction& simplify(RationalFunction& value) {
-//            value.simplify();
-//            return value;
-//        }
-//
-//        template<>
-//        RationalFunction&& simplify(RationalFunction&& value) {
-//            value.simplify();
-//            return std::move(value);
-//        }
-//
-//        template<>
-//        double convertNumber(RationalNumber const& number){
-//            return carl::toDouble(number);
-//        }
-//
-//        template<>
-//        RationalNumber convertNumber(double const& number){
-//            return carl::rationalize<RationalNumber>(number);
-//        }
-//
-//        template<>
-//        RationalFunction convertNumber(double const& number){
-//            return RationalFunction(carl::rationalize<RationalNumber>(number));
-//        }
-////
-////        template<>
-////        storm::RationalNumber abs(storm::RationalNumber const& number) {
-////            return carl::abs(number);
-////        }
-//
-        template<typename IndexType, typename ValueType>
-        storm::storage::MatrixEntry<IndexType, ValueType> simplify(storm::storage::MatrixEntry<IndexType, ValueType> matrixEntry) {
-            simplify(matrixEntry.getValue());
-            return matrixEntry;
-        }
-
-        template<typename IndexType, typename ValueType>
-        storm::storage::MatrixEntry<IndexType, ValueType>& simplify(storm::storage::MatrixEntry<IndexType, ValueType>& matrixEntry) {
-            simplify(matrixEntry.getValue());
-            return matrixEntry;
-        }
-
-        template<typename IndexType, typename ValueType>
-        storm::storage::MatrixEntry<IndexType, ValueType>&& simplify(storm::storage::MatrixEntry<IndexType, ValueType>&& matrixEntry) {
-            simplify(matrixEntry.getValue());
-            return std::move(matrixEntry);
-        }
-//
-//        // Explicit instantiations.
-//        template bool isOne(double const& value);
-//        template bool isZero(double const& value);
-//        template bool isConstant(double const& value);
-//
-//		template double one();
-//		template double zero();
-//		template double infinity();
-//
-//		template double pow(double const& value, uint_fast64_t exponent);
-//
-//		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);
-		template storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>& matrixEntry);
-		template storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>&& matrixEntry);
-//
-//        template double abs(double const& number);
-//
-//        template bool isOne(float const& value);
-//        template bool isZero(float const& value);
-//        template bool isConstant(float const& value);
-//
-//		template float one();
-//		template float zero();
-//		template float infinity();
-//
-//		template float pow(float const& value, uint_fast64_t exponent);
-//
-//		template float simplify(float value);
-
-		template storm::storage::MatrixEntry<storm::storage::sparse::state_type, float> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, float> matrixEntry);
-		template storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>& matrixEntry);
-		template storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>&& matrixEntry);
-
-//        template bool isOne(int const& value);
-//        template bool isZero(int const& value);
-//        template bool isConstant(int const& value);
-//
-//        template int one();
-//        template int zero();
-//        template int infinity();
-//
-//        template int pow(int const& value, uint_fast64_t exponent);
-//
-//        template int simplify(int value);
-
-        template storm::storage::MatrixEntry<storm::storage::sparse::state_type, int> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, int> matrixEntry);
-        template storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>& matrixEntry);
-        template storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>&& matrixEntry);
-
-//        template bool isOne(storm::storage::sparse::state_type const& value);
-//        template bool isZero(storm::storage::sparse::state_type const& value);
-//        template bool isConstant(storm::storage::sparse::state_type const& value);
-//
-//        template uint32_t one();
-//        template uint32_t zero();
-//        template uint32_t infinity();
-//
-//        template storm::storage::sparse::state_type one();
-//        template storm::storage::sparse::state_type zero();
-//        template storm::storage::sparse::state_type infinity();
-//
-//        template storm::storage::sparse::state_type pow(storm::storage::sparse::state_type const& value, uint_fast64_t exponent);
-//
-//        template storm::storage::sparse::state_type simplify(storm::storage::sparse::state_type value);
-//
-        template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type> matrixEntry);
-        template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>& matrixEntry);
-        template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>&& matrixEntry);
-//
-//        // Instantiations for rational number.
-//        template bool isOne(storm::RationalNumber const& value);
-//        template bool isZero(storm::RationalNumber const& value);
-//        template bool isConstant(storm::RationalNumber const& value);
-//
-//        template storm::RationalNumber one();
-//        template storm::RationalNumber zero();
-//        template storm::RationalNumber infinity();
-//
-//        template double convertNumber(storm::RationalNumber const& number);
-//        template storm::RationalNumber convertNumber(double const& number);
-//
-//        template storm::RationalNumber abs(storm::RationalNumber const& number);
-//
-////        template storm::RationalNumber pow(storm::RationalNumber const& value, uint_fast64_t exponent);
-//
-//        template storm::RationalNumber simplify(storm::RationalNumber value);
-        template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber> matrixEntry);
-        template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber>& matrixEntry);
-        template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber>&& matrixEntry);
-
-#ifdef STORM_HAVE_CARL
-//        template bool isOne(RationalFunction const& value);
-//        template bool isZero(RationalFunction const& value);
-//        template bool isConstant(RationalFunction const& value);
-//
-//        template RationalFunction one();
-//        template RationalFunction zero();
-//        template storm::RationalFunction infinity();
-//
-//        template RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent);
-//        template RationalFunction simplify(RationalFunction value);
-//        template RationalFunction& simplify(RationalFunction& value);
-//        template RationalFunction&& simplify(RationalFunction&& value);
-//
-//        template Polynomial one();
-//        template Polynomial zero();
-//
-//        template bool isOne(Interval const& value);
-//        template bool isZero(Interval const& value);
-//        template bool isConstant(Interval const& value);
-//
-//        template Interval one();
-//        template Interval zero();
-
-        template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction> matrixEntry);
-        template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>& matrixEntry);
-        template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>&& matrixEntry);
-#endif
-//
-    }
-}
+    #include "src/utility/constants.h"
+    
+    #include "src/storage/sparse/StateType.h"
+  #include "src/storage/SparseMatrix.h"
+    #include "src/settings/SettingsManager.h"
+    #include "src/settings/modules/GeneralSettings.h"
+    
+    #include "src/adapters/CarlAdapter.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<typename ValueType>
+            bool isOne(ValueType const& a) {
+                return a == one<ValueType>();
+            }
+    
+            template<typename ValueType>
+            bool isZero(ValueType const& a) {
+                return a == zero<ValueType>();
+            }
+    
+            template<typename ValueType>
+            bool isConstant(ValueType const& a) {
+                return true;
+            }
+    
+            template<>
+            bool isOne(storm::RationalNumber const& a) {
+                return carl::isOne(a);
+            }
+    
+            template<>
+            bool isZero(storm::RationalNumber const& a) {
+                return carl::isZero(a);
+            }
+    
+            template<>
+            storm::RationalNumber infinity() {
+                  // FIXME: this should be treated more properly.
+                return storm::RationalNumber(-1);
+            }
+    
+            template<>
+            bool isOne(storm::RationalFunction const& a) {
+                return a.isOne();
+            }
+    
+            template<>
+            bool isZero(storm::RationalFunction const& a) {
+                return a.isZero();
+            }
+    
+            template<>
+            bool isConstant(storm::RationalFunction const& a) {
+                return a.isConstant();
+            }
+    
+            template<>
+            bool isOne(storm::Polynomial const& a) {
+                return a.isOne();
+            }
+    
+            template<>
+            bool isZero(storm::Polynomial const& a) {
+                return a.isZero();
+            }
+    
+            template<>
+            bool isConstant(storm::Polynomial const& a) {
+                return a.isConstant();
+            }
+    
+            template<>
+            storm::RationalFunction infinity() {
+                   //FIXME: this should be treated more properly.
+                return storm::RationalFunction(-1.0);
+            }
+    
+            template<typename ValueType>
+            ValueType pow(ValueType const& value, uint_fast64_t exponent) {
+                assert(false);
+                //return std::pow(value, exponent);
+            }
+    
+    		template<typename ValueType>
+    		ValueType simplify(ValueType value) {
+                 //  In the general case, we don't do 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<>
+            double convertNumber(double const& number){
+                return number;
+            }
+    
+            template<typename ValueType>
+            ValueType abs(ValueType const& number) {
+                return carl::abs(number);
+            }
+    
+            template<>
+            RationalFunction& simplify(RationalFunction& value);
+    
+            template<>
+            RationalFunction&& simplify(RationalFunction&& value);
+    
+            template<>
+            RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent) {
+                return carl::pow(value, exponent);
+            }
+    
+            template<>
+            RationalFunction simplify(RationalFunction value) {
+                value.simplify();
+                return value;
+            }
+    
+            template<>
+            RationalFunction& simplify(RationalFunction& value) {
+                value.simplify();
+                return value;
+            }
+    
+            template<>
+            RationalFunction&& simplify(RationalFunction&& value) {
+                value.simplify();
+                return std::move(value);
+            }
+    
+            template<>
+            double convertNumber(RationalNumber const& number){
+                return carl::toDouble(number);
+            }
+    
+            template<>
+            RationalNumber convertNumber(double const& number){
+                return carl::rationalize<RationalNumber>(number);
+            }
+    
+            template<>
+            RationalFunction convertNumber(double const& number){
+                return RationalFunction(carl::rationalize<RationalNumber>(number));
+            }
+      
+              template<>
+              storm::RationalNumber abs(storm::RationalNumber const& number) {
+                  return carl::abs(number);
+              }
+    
+          template<typename IndexType, typename ValueType>
+          storm::storage::MatrixEntry<IndexType, ValueType> simplify(storm::storage::MatrixEntry<IndexType, ValueType> matrixEntry) {
+              simplify(matrixEntry.getValue());
+              return matrixEntry;
+          }
+  
+          template<typename IndexType, typename ValueType>
+          storm::storage::MatrixEntry<IndexType, ValueType>& simplify(storm::storage::MatrixEntry<IndexType, ValueType>& matrixEntry) {
+              simplify(matrixEntry.getValue());
+              return matrixEntry;
+          }
+  
+          template<typename IndexType, typename ValueType>
+          storm::storage::MatrixEntry<IndexType, ValueType>&& simplify(storm::storage::MatrixEntry<IndexType, ValueType>&& matrixEntry) {
+              simplify(matrixEntry.getValue());
+              return std::move(matrixEntry);
+          }
+    
+            //   Explicit instantiations.
+            template bool isOne(double const& value);
+            template bool isZero(double const& value);
+            template bool isConstant(double const& value);
+    
+    		template double one();
+    		template double zero();
+    		template double infinity();
+    
+    		template double pow(double const& value, uint_fast64_t exponent);
+    
+    		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);
+  		template storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>& matrixEntry);
+  		template storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>&& matrixEntry);
+    
+            template double abs(double const& number);
+    
+            template bool isOne(float const& value);
+            template bool isZero(float const& value);
+            template bool isConstant(float const& value);
+    
+    		template float one();
+    		template float zero();
+    		template float infinity();
+    
+    		template float pow(float const& value, uint_fast64_t exponent);
+    
+    		template float simplify(float value);
+  
+  		template storm::storage::MatrixEntry<storm::storage::sparse::state_type, float> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, float> matrixEntry);
+  		template storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>& matrixEntry);
+  		template storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>&& matrixEntry);
+  
+            template bool isOne(int const& value);
+            template bool isZero(int const& value);
+            template bool isConstant(int const& value);
+    
+            template int one();
+            template int zero();
+            template int infinity();
+    
+            template int pow(int const& value, uint_fast64_t exponent);
+    
+            template int simplify(int value);
+    
+            template storm::storage::MatrixEntry<storm::storage::sparse::state_type, int> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, int> matrixEntry);
+            template storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>& matrixEntry);
+            template storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>&& matrixEntry);
+    
+            template bool isOne(storm::storage::sparse::state_type const& value);
+            template bool isZero(storm::storage::sparse::state_type const& value);
+            template bool isConstant(storm::storage::sparse::state_type const& value);
+    
+            template uint32_t one();
+            template uint32_t zero();
+            template uint32_t infinity();
+    
+            template storm::storage::sparse::state_type one();
+            template storm::storage::sparse::state_type zero();
+            template storm::storage::sparse::state_type infinity();
+    
+            template storm::storage::sparse::state_type pow(storm::storage::sparse::state_type const& value, uint_fast64_t exponent);
+    
+            template storm::storage::sparse::state_type simplify(storm::storage::sparse::state_type value);
+    
+            template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type> matrixEntry);
+            template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>& matrixEntry);
+            template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>&& matrixEntry);
+    
+             // Instantiations for rational number.
+            template bool isOne(storm::RationalNumber const& value);
+            template bool isZero(storm::RationalNumber const& value);
+            template bool isConstant(storm::RationalNumber const& value);
+    
+            template storm::RationalNumber one();
+            template storm::RationalNumber zero();
+            template storm::RationalNumber infinity();
+    
+            template double convertNumber(storm::RationalNumber const& number);
+            template storm::RationalNumber convertNumber(double const& number);
+    
+            template storm::RationalNumber abs(storm::RationalNumber const& number);
+    
+              template storm::RationalNumber pow(storm::RationalNumber const& value, uint_fast64_t exponent);
+    
+            template storm::RationalNumber simplify(storm::RationalNumber value);
+            template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber> matrixEntry);
+            template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber>& matrixEntry);
+            template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber>&& matrixEntry);
+    
+    #ifdef STORM_HAVE_CARL
+            template bool isOne(RationalFunction const& value);
+            template bool isZero(RationalFunction const& value);
+            template bool isConstant(RationalFunction const& value);
+    
+            template RationalFunction one();
+            template RationalFunction zero();
+            template storm::RationalFunction infinity();
+    
+            template RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent);
+            template RationalFunction simplify(RationalFunction value);
+            template RationalFunction& simplify(RationalFunction& value);
+            template RationalFunction&& simplify(RationalFunction&& value);
+    
+            template Polynomial one();
+            template Polynomial zero();
+    
+            template bool isOne(Interval const& value);
+            template bool isZero(Interval const& value);
+            template bool isConstant(Interval const& value);
+    
+            template Interval one();
+            template Interval zero();
+    
+            template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction> matrixEntry);
+            template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>& matrixEntry);
+            template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>&& matrixEntry);
+    #endif
+    
+      }
+  }

src/utility/constants.h

@@ -11,196 +11,51 @@
 
 #include <limits>
 #include <cstdint>
-#include "src/storage/sparse/StateType.h"
-#include "src/settings/SettingsManager.h"
-#include "src/settings/modules/GeneralSettings.h"
-
-#include "src/adapters/CarlAdapter.h"
 
 namespace storm {
-    
+
     // Forward-declare MatrixEntry class.
     namespace storage {
         template<typename IndexType, typename ValueType> class MatrixEntry;
     }
-    
-    namespace utility {
 
-        template<typename ValueType>
-        ValueType one() {
-            return ValueType(1);
-        }
+    namespace utility {
 
         template<typename ValueType>
-        ValueType zero() {
-            return ValueType(0);
-        }
+        ValueType one();
 
         template<typename ValueType>
-        ValueType infinity() {
-            return std::numeric_limits<ValueType>::infinity();
-        }
+        ValueType zero();
 
         template<typename ValueType>
-        bool isOne(ValueType const& a) {
-            return a == one<ValueType>();
-        }
+        ValueType infinity();
 
         template<typename ValueType>
-        bool isZero(ValueType const& a) {
-            return a == zero<ValueType>();
-        }
+        bool isOne(ValueType const& a);
 
         template<typename ValueType>
-        bool isConstant(ValueType const& a) {
-            return true;
-        }
-
-        template<>
-        bool isOne(storm::RationalNumber const& a) {
-            return carl::isOne(a);
-        }
-
-        template<>
-        bool isZero(storm::RationalNumber const& a) {
-            return carl::isZero(a);
-        }
-
-        template<>
-        storm::RationalNumber infinity() {
-            // FIXME: this should be treated more properly.
-            return storm::RationalNumber(-1);
-        }
-
-        template<>
-        bool isOne(storm::RationalFunction const& a) {
-            return a.isOne();
-        }
-
-        template<>
-        bool isZero(storm::RationalFunction const& a) {
-            return a.isZero();
-        }
-
-        template<>
-        bool isConstant(storm::RationalFunction const& a) {
-            return a.isConstant();
-        }
-
-        template<>
-        bool isOne(storm::Polynomial const& a) {
-            return a.isOne();
-        }
-
-        template<>
-        bool isZero(storm::Polynomial const& a) {
-            return a.isZero();
-        }
-
-        template<>
-        bool isConstant(storm::Polynomial const& a) {
-            return a.isConstant();
-        }
-
-        template<>
-        storm::RationalFunction infinity() {
-            // FIXME: this should be treated more properly.
-            return storm::RationalFunction(-1.0);
-        }
+        bool isZero(ValueType const& a);
 
         template<typename ValueType>
-        ValueType pow(ValueType const& value, uint_fast64_t exponent) {
-            return std::pow(value, exponent);
-        }
+        bool isConstant(ValueType const& a);
 
         template<typename ValueType>
-        ValueType simplify(ValueType value) {
-            // In the general case, we don't do 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 SourceType, typename TargetType>
-        TargetType convertNumber(SourceType const& number);
-
-        template<>
-        double convertNumber(double const& number){
-            return number;
-        }
+        ValueType pow(ValueType const& value, uint_fast64_t exponent);
 
         template<typename ValueType>
-        ValueType abs(ValueType const& number) {
-            return carl::abs(number);
-        }
-
-        template<>
-        RationalFunction& simplify(RationalFunction& value);
-
-        template<>
-        RationalFunction&& simplify(RationalFunction&& value);
-
-        template<>
-        RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent) {
-            return carl::pow(value, exponent);
-        }
-
-        template<>
-        RationalFunction simplify(RationalFunction value) {
-            value.simplify();
-            return value;
-        }
-
-        template<>
-        RationalFunction& simplify(RationalFunction& value) {
-            value.simplify();
-            return value;
-        }
-
-        template<>
-        RationalFunction&& simplify(RationalFunction&& value) {
-            value.simplify();
-            return std::move(value);
-        }
-
-        template<>
-        double convertNumber(RationalNumber const& number){
-            return carl::toDouble(number);
-        }
-
-        template<>
-        RationalNumber convertNumber(double const& number){
-            return carl::rationalize<RationalNumber>(number);
-        }
-
-        template<>
-        RationalFunction convertNumber(double const& number){
-            return RationalFunction(carl::rationalize<RationalNumber>(number));
-        }
-//
-//        template<>
-//        storm::RationalNumber abs(storm::RationalNumber const& number) {
-//            return carl::abs(number);
-//        }
-
-        template<typename IndexType, typename ValueType>
-        storm::storage::MatrixEntry<IndexType, ValueType> simplify(storm::storage::MatrixEntry<IndexType, ValueType> matrixEntry) {
-            simplify(matrixEntry.getValue());
-            return matrixEntry;
-        }
+        ValueType simplify(ValueType value);
 
         template<typename IndexType, typename ValueType>
-        storm::storage::MatrixEntry<IndexType, ValueType>& simplify(storm::storage::MatrixEntry<IndexType, ValueType>& matrixEntry) {
-            simplify(matrixEntry.getValue());
-            return matrixEntry;
-        }
+        storm::storage::MatrixEntry<IndexType, ValueType>& simplify(storm::storage::MatrixEntry<IndexType, ValueType>& matrixEntry);
 
         template<typename IndexType, typename ValueType>
-        storm::storage::MatrixEntry<IndexType, ValueType>&& simplify(storm::storage::MatrixEntry<IndexType, ValueType>&& matrixEntry) {
-            simplify(matrixEntry.getValue());
-            return std::move(matrixEntry);
-        }
+        storm::storage::MatrixEntry<IndexType, ValueType>&& simplify(storm::storage::MatrixEntry<IndexType, ValueType>&& matrixEntry);
 
+        template<typename TargetType, typename SourceType>
+        TargetType convertNumber(SourceType const& number);
 
+        template<typename ValueType>
+        ValueType abs(ValueType const& number);
     }
 }
 

src/utility/vector.h

@@ -592,11 +592,13 @@ namespace storm {
 					if (val2 == 0) {
                         return (storm::utility::abs(val1) <= precision);
 					}
-                    if (storm::utility::abs((val1 - val2)/val2) > precision) {
+                    T relDiff = (val1 - val2)/val2;
+                    if (storm::utility::abs(relDiff) > precision) {
                         return false;
                     }
                 } else {
-                    if (storm::utility::abs(val1 - val2) > precision) return false;
+                    T diff = val1 - val2;
+                    if (storm::utility::abs(diff) > precision) return false;
                 }
                 return true;
             }