From 0b1b0d97e2841913370a63bad937e60c97565051 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Fri, 26 Jul 2019 08:42:39 +0200
Subject: [PATCH] utility/graph: fixed behavior of getReachableStates when an
 initial state is not in the constrained set.

---
 src/storm/utility/graph.cpp | 12 +++++++++---
 src/storm/utility/graph.h   |  1 +
 2 files changed, 10 insertions(+), 3 deletions(-)

diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp
index c1f1216ad..b774c65da 100644
--- a/src/storm/utility/graph.cpp
+++ b/src/storm/utility/graph.cpp
@@ -37,16 +37,22 @@ namespace storm {
                 uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount();
                 
                 // Initialize the stack used for the DFS with the states.
-                std::vector<uint_fast64_t> stack(initialStates.begin(), initialStates.end());
+                std::vector<uint_fast64_t> stack;
+                stack.reserve(initialStates.size());
+                for (auto const& state : initialStates) {
+                    if (constraintStates.get(state)) {
+                        stack.push_back(state);
+                    }
+                }
                 
                 // Initialize the stack for the step bound, if the number of steps is bounded.
                 std::vector<uint_fast64_t> stepStack;
                 std::vector<uint_fast64_t> remainingSteps;
                 if (useStepBound) {
                     stepStack.reserve(numberOfStates);
-                    stepStack.insert(stepStack.begin(), initialStates.getNumberOfSetBits(), maximalSteps);
+                    stepStack.insert(stepStack.begin(), stack.size(), maximalSteps);
                     remainingSteps.resize(numberOfStates);
-                    for (auto state : initialStates) {
+                    for (auto state : stack) {
                         remainingSteps[state] = maximalSteps;
                     }
                 }
diff --git a/src/storm/utility/graph.h b/src/storm/utility/graph.h
index 6f65bbcfa..d6f12cc94 100644
--- a/src/storm/utility/graph.h
+++ b/src/storm/utility/graph.h
@@ -60,6 +60,7 @@ namespace storm {
              * Performs a forward depth-first search through the underlying graph structure to identify the states that
              * are reachable from the given set only passing through a constrained set of states until some target
              * have been reached.
+             * If an initial state or a (constrained-reachable) target state is not in the constrained set, it will be added to the reachable states but not explored.
              *
              * @param transitionMatrix The transition relation of the graph structure to search.
              * @param initialStates The set of states from which to start the search.