Added comparator use for checking validity of probability matrices such that only if the value is actually constant it is required to be one.

Former-commit-id: 3224422976

src/models/Dtmc.h

@@ -20,6 +20,7 @@
 #include "src/settings/SettingsManager.h"
 #include "src/utility/vector.h"
 #include "src/utility/matrix.h"
+#include "src/utility/ConstantsComparator.h"
 
 namespace storm {
 
@@ -299,21 +300,26 @@ private:
 	 *	Checks probability matrix if all rows sum up to one.
 	 */
 	bool checkValidityOfProbabilityMatrix() {
-        double precision = storm::settings::generalSettings().getPrecision();
-
 		if (this->getTransitionMatrix().getRowCount() != this->getTransitionMatrix().getColumnCount()) {
 			// not square
 			LOG4CPLUS_ERROR(logger, "Probability matrix is not square.");
 			return false;
 		}
 
+        storm::utility::ConstantsComparator<T> comparator;
 		for (uint_fast64_t row = 0; row < this->getTransitionMatrix().getRowCount(); ++row) {
 			T sum = this->getTransitionMatrix().getRowSum(row);
-                        
-			if (sum == 0) {
+            
+            // If the sum is not a constant, for example for parametric models, we cannot check whether the sum is one
+            // or not.
+            if (!comparator.isConstant(sum)) {
+                continue;
+            }
+            
+			if (comparator.isZero(sum)) {
 				return false;
 			}
-			if (std::abs(sum - 1) > precision) {
+			if (!comparator.isOne(sum)) {
 				LOG4CPLUS_ERROR(logger, "Row " << row << " has sum " << sum << ".");
 				return false;
 			}

src/utility/ConstantsComparator.h

@@ -36,15 +36,15 @@ namespace storm {
         template<typename ValueType>
         class ConstantsComparator {
         public:
-            bool isOne(ValueType const& value) {
+            bool isOne(ValueType const& value) const {
                 return value == one<ValueType>();
             }
             
-            bool isZero(ValueType const& value) {
+            bool isZero(ValueType const& value) const {
                 return value == zero<ValueType>();
             }
             
-            bool isEqual(ValueType const& value1, ValueType const& value2) {
+            bool isEqual(ValueType const& value1, ValueType const& value2) const {
                 return value1 == value2;
             }
         };
@@ -61,18 +61,22 @@ namespace storm {
                 // Intentionally left empty.
             }
             
-            bool isOne(double const& value) {
+            bool isOne(double const& value) const {
                 return std::abs(value - one<double>()) <= precision;
             }
             
-            bool isZero(double const& value) {
+            bool isZero(double const& value) const {
                 return std::abs(value) <= precision;
             }
             
-            bool isEqual(double const& value1, double const& value2) {
+            bool isEqual(double const& value1, double const& value2) const {
                 return std::abs(value1 - value2) <= precision;
             }
             
+            bool isConstant(double const& value) const {
+                return true;
+            }
+            
         private:
             // The precision used for comparisons.
             double precision;