From c88e540a1a60c81a51d28e5c86418a2e4677d5cb Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 16 Jun 2016 16:54:56 +0200
Subject: [PATCH] fixed bug in graph preprocessing algorithms that support a
 maximal number of steps

Former-commit-id: aed124e5f88dad4e14687d38379e31ea5b55f440
---
 src/utility/graph.cpp | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/utility/graph.cpp b/src/utility/graph.cpp
index bd10cfd03..b188872cf 100644
--- a/src/utility/graph.cpp
+++ b/src/utility/graph.cpp
@@ -151,7 +151,9 @@ namespace storm {
                     }
                     
                     for (typename storm::storage::SparseMatrix<T>::const_iterator entryIt = backwardTransitions.begin(currentState), entryIte = backwardTransitions.end(currentState); entryIt != entryIte; ++entryIt) {
-                        if (phiStates[entryIt->getColumn()] && (!statesWithProbabilityGreater0.get(entryIt->getColumn()) && (!useStepBound || remainingSteps[entryIt->getColumn()] < currentStepBound - 1))) {
+                        if (phiStates[entryIt->getColumn()] && (!statesWithProbabilityGreater0.get(entryIt->getColumn()) && (!useStepBound || remainingSteps[entryIt->getColumn()] < currentStepBound))) {
+                            statesWithProbabilityGreater0.set(entryIt->getColumn(), true);
+
                             // If we don't have a bound on the number of steps to take, just add the state to the stack.
                             if (useStepBound) {
                                 // If there is at least one more step to go, we need to push the state and the new number of steps.
@@ -161,7 +163,6 @@ namespace storm {
                                     continue;
                                 }
                             }
-                            statesWithProbabilityGreater0.set(entryIt->getColumn(), true);
                             stack.push_back(entryIt->getColumn());
                         }
                     }
@@ -440,7 +441,7 @@ namespace storm {
                     }
                     
                     for (typename storm::storage::SparseMatrix<T>::const_iterator entryIt = backwardTransitions.begin(currentState), entryIte = backwardTransitions.end(currentState); entryIt != entryIte; ++entryIt) {
-                        if (phiStates.get(entryIt->getColumn()) && (!statesWithProbabilityGreater0.get(entryIt->getColumn()) && (!useStepBound || remainingSteps[entryIt->getColumn()] < currentStepBound - 1))) {
+                        if (phiStates.get(entryIt->getColumn()) && (!statesWithProbabilityGreater0.get(entryIt->getColumn()) && (!useStepBound || remainingSteps[entryIt->getColumn()] < currentStepBound))) {
                             // If we don't have a bound on the number of steps to take, just add the state to the stack.
                             if (useStepBound) {
                                 // If there is at least one more step to go, we need to push the state and the new number of steps.
@@ -589,7 +590,7 @@ namespace storm {
                     }
                     
                     for(typename storm::storage::SparseMatrix<T>::const_iterator predecessorEntryIt = backwardTransitions.begin(currentState), predecessorEntryIte = backwardTransitions.end(currentState); predecessorEntryIt != predecessorEntryIte; ++predecessorEntryIt) {
-                        if (phiStates.get(predecessorEntryIt->getColumn()) && (!statesWithProbabilityGreater0.get(predecessorEntryIt->getColumn()) && (!useStepBound || remainingSteps[predecessorEntryIt->getColumn()] < currentStepBound - 1))) {
+                        if (phiStates.get(predecessorEntryIt->getColumn()) && (!statesWithProbabilityGreater0.get(predecessorEntryIt->getColumn()) && (!useStepBound || remainingSteps[predecessorEntryIt->getColumn()] < currentStepBound))) {
                             // Check whether the predecessor has at least one successor in the current state set for every
                             // nondeterministic choice.
                             bool addToStatesWithProbabilityGreater0 = true;