From cd8dafa6eac8c4530f978b7fe578a90fa108753c Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Mon, 31 Jul 2017 16:37:40 +0200
Subject: [PATCH] Check for absence of negative probabilities in matrix

---
 src/storm/storage/SparseMatrix.cpp | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp
index 1a005d2d0..905fbffa9 100644
--- a/src/storm/storage/SparseMatrix.cpp
+++ b/src/storm/storage/SparseMatrix.cpp
@@ -1571,7 +1571,7 @@ namespace storm {
         typename SparseMatrix<ValueType>::index_type SparseMatrix<ValueType>::getNonconstantRowGroupCount() const {
             index_type nonConstRowGroups = 0;
             for (index_type rowGroup=0; rowGroup < this->getRowGroupCount(); ++rowGroup) {
-                for( auto const& entry : this->getRowGroup(rowGroup)){
+                for (auto const& entry : this->getRowGroup(rowGroup)){
                     if(!storm::utility::isConstant(entry.getValue())){
                         ++nonConstRowGroups;
                         break;
@@ -1584,11 +1584,18 @@ namespace storm {
         template<typename ValueType>
         bool SparseMatrix<ValueType>::isProbabilistic() const {
             storm::utility::ConstantsComparator<ValueType> comparator;
-            for(index_type row = 0; row < this->rowCount; ++row) {
+            for (index_type row = 0; row < this->rowCount; ++row) {
                 if(!comparator.isOne(getRowSum(row))) {
                     return false;
                 }
             }
+            for (auto const& entry : *this) {
+                if (comparator.isConstant(entry.getValue())) {
+                    if (comparator.isLess(entry.getValue(), storm::utility::zero<ValueType>())) {
+                        return false;
+                    }
+                }
+            }
             return true;
         }