Browse Source

utility/graph: fixed behavior of getReachableStates when an initial state is not in the constrained set.

tempestpy_adaptions
Tim Quatmann 5 years ago
parent
commit
0b1b0d97e2
  1. 12
      src/storm/utility/graph.cpp
  2. 1
      src/storm/utility/graph.h

12
src/storm/utility/graph.cpp

@ -37,16 +37,22 @@ namespace storm {
uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount(); uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount();
// Initialize the stack used for the DFS with the states. // 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. // 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> stepStack;
std::vector<uint_fast64_t> remainingSteps; std::vector<uint_fast64_t> remainingSteps;
if (useStepBound) { if (useStepBound) {
stepStack.reserve(numberOfStates); stepStack.reserve(numberOfStates);
stepStack.insert(stepStack.begin(), initialStates.getNumberOfSetBits(), maximalSteps);
stepStack.insert(stepStack.begin(), stack.size(), maximalSteps);
remainingSteps.resize(numberOfStates); remainingSteps.resize(numberOfStates);
for (auto state : initialStates) {
for (auto state : stack) {
remainingSteps[state] = maximalSteps; remainingSteps[state] = maximalSteps;
} }
} }

1
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 * 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 * are reachable from the given set only passing through a constrained set of states until some target
* have been reached. * 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 transitionMatrix The transition relation of the graph structure to search.
* @param initialStates The set of states from which to start the search. * @param initialStates The set of states from which to start the search.

Loading…
Cancel
Save