From 584dc6caa7024a05a3a3fb4f1fbf3fac61862fa2 Mon Sep 17 00:00:00 2001
From: Alexander Bork <alexander.bork@rwth-aachen.de>
Date: Fri, 9 Aug 2019 13:33:13 +0200
Subject: [PATCH] Fixed error that matrix dimensions were to small if last
 columns have only 0 entries

---
 src/storm/transformer/NonMarkovianChainTransformer.cpp | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/storm/transformer/NonMarkovianChainTransformer.cpp b/src/storm/transformer/NonMarkovianChainTransformer.cpp
index 3170698c9..be5e57858 100644
--- a/src/storm/transformer/NonMarkovianChainTransformer.cpp
+++ b/src/storm/transformer/NonMarkovianChainTransformer.cpp
@@ -166,10 +166,11 @@ namespace storm {
                 }
             }
 
+            uint64_t newStateCount = ma->getNumberOfStates() - eliminationMapping.size();
             // Build the new MA
             storm::storage::SparseMatrix<ValueType> newTransitionMatrix;
             storm::models::sparse::StateLabeling newStateLabeling(
-                    ma->getNumberOfStates() - eliminationMapping.size());
+                    newStateCount);
             storm::storage::BitVector newMarkovianStates(ma->getNumberOfStates() - eliminationMapping.size(),
                                                          false);
             std::vector<ValueType> newExitRates;
@@ -230,7 +231,8 @@ namespace storm {
                     ++currentRow;
                 }
             }
-            newTransitionMatrix = matrixBuilder.build();
+            // explicitly force dimensions of the matrix in case a column is missing
+            newTransitionMatrix = matrixBuilder.build(newStateCount, newStateCount, newStateCount);
 
             storm::storage::sparse::ModelComponents<ValueType, RewardModelType> newComponents = storm::storage::sparse::ModelComponents<ValueType, RewardModelType>(
                     std::move(newTransitionMatrix), std::move(newStateLabeling));