From 59a81831f3c44425d20ed8ad18a9760137115737 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 31 Aug 2018 10:21:47 +0200 Subject: [PATCH] fixing bug in relevant states computation of menu-game-based abstraction --- src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp | 2 +- src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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.