From 88544a9ec79bf7a4613eaf05fba64895701951d3 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Thu, 12 Oct 2017 18:19:36 +0200
Subject: [PATCH] Added assertion for turnRatesToProbabilities in MA

---
 src/storm/models/sparse/MarkovAutomaton.cpp | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/storm/models/sparse/MarkovAutomaton.cpp b/src/storm/models/sparse/MarkovAutomaton.cpp
index 8bc00fa99..ca79ccfac 100644
--- a/src/storm/models/sparse/MarkovAutomaton.cpp
+++ b/src/storm/models/sparse/MarkovAutomaton.cpp
@@ -152,7 +152,7 @@ namespace storm {
                     uint_fast64_t row = this->getTransitionMatrix().getRowGroupIndices()[state];
                     if (this->markovianStates.get(state)) {
                         if (assertRates) {
-                        STORM_LOG_THROW(this->exitRates[state] == this->getTransitionMatrix().getRowSum(row), storm::exceptions::InvalidArgumentException, "The specified exit rate is inconsistent with the rate matrix. Difference is " << (this->exitRates[state] - this->getTransitionMatrix().getRowSum(row)) << ".");
+                            STORM_LOG_THROW(this->exitRates[state] == this->getTransitionMatrix().getRowSum(row), storm::exceptions::InvalidArgumentException, "The specified exit rate is inconsistent with the rate matrix. Difference is " << (this->exitRates[state] - this->getTransitionMatrix().getRowSum(row)) << ".");
                         } else {
                             this->exitRates.push_back(this->getTransitionMatrix().getRowSum(row));
                         }
@@ -161,7 +161,11 @@ namespace storm {
                         }
                         ++row;
                     } else {
-                        this->exitRates.push_back(storm::utility::zero<ValueType>());
+                        if (assertRates) {
+                            STORM_LOG_THROW(storm::utility::isZero<ValueType>(this->exitRates[state]), storm::exceptions::InvalidArgumentException, "The specified exit rate for (non-Markovian) choice should be 0.");
+                        } else {
+                            this->exitRates.push_back(storm::utility::zero<ValueType>());
+                        }
                     }
                     for (; row < this->getTransitionMatrix().getRowGroupIndices()[state+1]; ++row) {
                         STORM_LOG_THROW(storm::utility::isOne(this->getTransitionMatrix().getRowSum(row)), storm::exceptions::InvalidArgumentException, "Entries of transition matrix do not sum up to one for (non-Markovian) choice " << row << " of state " << state << " (sum is " << this->getTransitionMatrix().getRowSum(row) << ").");