From b3a02b6e8af3ffb1ae9d0741aa6dd39ef7feab7b Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Wed, 8 Mar 2017 11:25:54 +0100
Subject: [PATCH] fix in sparse ctmc model checker: bounded until returned
 empty result in case there are no non-prob0-states

---
 src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp       | 2 ++
 .../modelchecker/results/ExplicitQuantitativeCheckResult.cpp    | 1 +
 2 files changed, 3 insertions(+)

diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
index 10995f9b7..1dff5b454 100644
--- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
+++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
@@ -186,6 +186,8 @@ namespace storm {
                             }
                         }
                     }
+                } else {
+                    result = std::vector<ValueType>(numberOfStates, storm::utility::zero<ValueType>());
                 }
                 
                 return result;
diff --git a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp
index 5ea662a57..f9231a22c 100644
--- a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp
+++ b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp
@@ -61,6 +61,7 @@ namespace storm {
 
             if (this->isResultForAllStates()) {
                 map_type newMap;
+                
                 for (auto const& element : filterTruthValues) {
                     STORM_LOG_THROW(element < this->getValueVector().size(), storm::exceptions::InvalidAccessException, "Invalid index in results.");
                     newMap.emplace(element, this->getValueVector()[element]);