diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index 02082ee96..4da96acf6 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -737,7 +737,12 @@ namespace storm { std::pair result; result.first = performProb0A(backwardTransitions, phiStates, psiStates); - result.second = performProb1E(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates); + + // result.second = performProb1E(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates); + // Instead of calling performProb1E, we call the (more easier) performProb0E on the Prob0A states. + // This is valid because, when maximizing probabilities, states that have prob1 cannot reach a state with prob 0 (and will eventually reach a psiState). + // States that do not have prob1 will eventually reach a state with prob0. + result.second = performProb0E(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, ~psiStates, result.first); return result; } @@ -964,7 +969,10 @@ namespace storm { std::pair performProb01Min(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { std::pair result; result.first = performProb0E(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates); - result.second = performProb1A(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates); + // Instead of calling performProb1A, we call the (more easier) performProb0A on the Prob0E states. + // This is valid because, when minimizing probabilities, states that have prob1 cannot reach a state with prob 0 (and will eventually reach a psiState). + // States that do not have prob1 will eventually reach a state with prob0. + result.second = performProb0A(backwardTransitions, ~psiStates, result.first); return result; }