From fbf28796b807c73b88ded7c7555b4e766ef35f40 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 14 Mar 2013 17:45:50 +0100
Subject: [PATCH] Fixed bug in gmm++ model checker: missing vector addition.

---
 src/modelchecker/GmmxxMdpPrctlModelChecker.h | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/modelchecker/GmmxxMdpPrctlModelChecker.h b/src/modelchecker/GmmxxMdpPrctlModelChecker.h
index d27b26b21..bacece187 100644
--- a/src/modelchecker/GmmxxMdpPrctlModelChecker.h
+++ b/src/modelchecker/GmmxxMdpPrctlModelChecker.h
@@ -59,6 +59,9 @@ private:
 		// Now perform matrix-vector multiplication as long as we meet the bound of the formula.
 		for (uint_fast64_t i = 0; i < repetitions; ++i) {
 			gmm::mult(*gmmxxMatrix, vector, multiplyResult);
+			if (summand != nullptr) {
+				gmm::add(*summand, multiplyResult);
+			}
 			if (this->minimumOperatorStack.top()) {
 				storm::utility::reduceVectorMin(multiplyResult, &vector, *nondeterministicChoiceIndices);
 			} else {