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 stack(initialStates.begin(), initialStates.end()); + std::vector 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 stepStack; std::vector 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.