diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp index d233e3f5f..493b70e4b 100644 --- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp +++ b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp @@ -201,7 +201,7 @@ namespace storm { storm::dd::Bdd targetStates = reachableStates && this->getStates(this->getTargetStateExpression()); // In the presence of target states, we keep only states that can reach the target states. - reachableStates = storm::utility::dd::computeBackwardsReachableStates(targetStates, reachableStates && !initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()) || initialStates; + reachableStates = storm::utility::dd::computeBackwardsReachableStates(targetStates, reachableStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()); // Include all successors of reachable states, because the backward search otherwise potentially // cuts probability 0 choices of these states. diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp index d25a51712..92b7e3bfb 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp @@ -193,7 +193,7 @@ namespace storm { storm::dd::Bdd targetStates = reachableStates && this->getStates(this->getTargetStateExpression()); // In the presence of target states, we keep only states that can reach the target states. - reachableStates = storm::utility::dd::computeBackwardsReachableStates(targetStates, reachableStates && !initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()) || initialStates; + reachableStates = storm::utility::dd::computeBackwardsReachableStates(targetStates, reachableStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()); // Include all successors of reachable states, because the backward search otherwise potentially // cuts probability 0 choices of these states.