Fixed wrong check for submatrix property of reward matrices.

src/models/Dtmc.h

@@ -50,11 +50,10 @@ public:
 			throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid.";
 		}
 		if (this->getTransitionRewardMatrix() != nullptr) {
-			// FIXME: This is temporarily commented out, because the checking routine does not work properly.
-			//if (!this->getTransitionRewardMatrix()->isSubmatrixOf(*(this->getTransitionMatrix()))) {
-			//	LOG4CPLUS_ERROR(logger, "Transition reward matrix is not a submatrix of the transition matrix, i.e. there are rewards for transitions that do not exist.");
-			//	throw storm::exceptions::InvalidArgumentException() << "There are transition rewards for nonexistent transitions.";
-			//}
+			if (!this->getTransitionRewardMatrix()->isSubmatrixOf(*(this->getTransitionMatrix()))) {
+				LOG4CPLUS_ERROR(logger, "Transition reward matrix is not a submatrix of the transition matrix, i.e. there are rewards for transitions that do not exist.");
+				throw storm::exceptions::InvalidArgumentException() << "There are transition rewards for nonexistent transitions.";
+			}
 		}
 	}
 

src/storage/SparseMatrix.h

@@ -865,16 +865,28 @@ public:
 	 *	@param matrix Matrix to check against.
 	 *	@return True iff this is a submatrix of matrix.
 	 */
-	bool isSubmatrixOf(SparseMatrix<T> const & matrix) const {
-		// FIXME: THIS DOES NOT IMPLEMENT WHAT IS PROMISED.
+	bool isSubmatrixOf(SparseMatrix<T> const& matrix) const {
 		if (this->getRowCount() != matrix.getRowCount()) return false;
 		if (this->getColumnCount() != matrix.getColumnCount()) return false;
 
+		/*
 		for (uint_fast64_t row = 0; row < this->getRowCount(); ++row) {
 			for (uint_fast64_t elem = rowIndications[row], elem2 = matrix.rowIndications[row]; elem < rowIndications[row + 1] && elem < matrix.rowIndications[row + 1]; ++elem, ++elem2) {
 				if (columnIndications[elem] < matrix.columnIndications[elem2]) return false;
 			}
 		}
+		*/
+
+		for (uint_fast64_t row = 0; row < this->getRowCount(); ++row) {
+			for (uint_fast64_t elem = rowIndications[row], elem2 = matrix.rowIndications[row]; elem < rowIndications[row + 1] && elem < matrix.rowIndications[row + 1]; ++elem) {
+				// Skip over all entries of the other matrix that are before the current entry in
+				// the current matrix.
+				while (elem2 < matrix.rowIndications[row + 1] && matrix.columnIndications[elem2] < columnIndications[elem]) {
+					++elem2;
+				}
+				if (!(elem2 < matrix.rowIndications[row + 1]) || columnIndications[elem] != matrix.columnIndications[elem2]) return false;
+			}
+		}
 		return true;
 	}