From 843a1d1fdfbb2089aa9d9bcdf0354c8c7fd19af5 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 14 Oct 2014 19:03:46 +0200
Subject: [PATCH] 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: 32244229768f94fa9e665bc8b2e82e8a593eaf5c
---
 src/models/Dtmc.h                 | 16 +++++++++++-----
 src/utility/ConstantsComparator.h | 16 ++++++++++------
 2 files changed, 21 insertions(+), 11 deletions(-)

diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h
index 98792982a..3ce4b1892 100644
--- a/src/models/Dtmc.h
+++ b/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;
 			}
diff --git a/src/utility/ConstantsComparator.h b/src/utility/ConstantsComparator.h
index fc46b251f..2da8fc084 100644
--- a/src/utility/ConstantsComparator.h
+++ b/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;