diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index b774c65da..02082ee96 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -882,36 +882,46 @@ namespace storm { size_t numberOfStates = phiStates.size(); // Initialize the environment for the iterative algorithm. - storm::storage::BitVector currentStates(numberOfStates, true); + storm::storage::BitVector bv1, bv2; + storm::storage::BitVector* currentStates = &bv1; + *currentStates = phiStates; + storm::storage::BitVector* nextStates = &bv2; + *nextStates = psiStates; std::vector stack; stack.reserve(numberOfStates); + // Simplify comparison between next and current states by keeping track of the number of set bits + uint64_t currentStatesSetBits = numberOfStates; + uint64_t numPsiStates = psiStates.getNumberOfSetBits(); + uint64_t nextStatesSetBits = numPsiStates; + // Perform the loop as long as the set of states gets smaller. bool done = false; uint_fast64_t currentState; while (!done) { stack.clear(); - storm::storage::BitVector nextStates(psiStates); stack.insert(stack.end(), psiStates.begin(), psiStates.end()); while (!stack.empty()) { currentState = stack.back(); stack.pop_back(); - for(typename storm::storage::SparseMatrix::const_iterator predecessorEntryIt = backwardTransitions.begin(currentState), predecessorEntryIte = backwardTransitions.end(currentState); predecessorEntryIt != predecessorEntryIte; ++predecessorEntryIt) { - if (phiStates.get(predecessorEntryIt->getColumn()) && !nextStates.get(predecessorEntryIt->getColumn())) { + for(auto const& predecessor : backwardTransitions.getRow(currentState)) { + auto predecessorState = predecessor.getColumn(); + if (phiStates.get(predecessorState) && !nextStates->get(predecessorState)) { // Check whether the predecessor has only successors in the current state set for all of the // nondeterminstic choices and that for each choice there exists a successor that is already // in the next states. bool addToStatesWithProbability1 = true; - for (uint_fast64_t row = nondeterministicChoiceIndices[predecessorEntryIt->getColumn()]; row < nondeterministicChoiceIndices[predecessorEntryIt->getColumn() + 1]; ++row) { + for (uint_fast64_t row = nondeterministicChoiceIndices[predecessorState]; row < nondeterministicChoiceIndices[predecessorState + 1]; ++row) { bool hasAtLeastOneSuccessorWithProbability1 = false; - for (typename storm::storage::SparseMatrix::const_iterator successorEntryIt = transitionMatrix.begin(row), successorEntryIte = transitionMatrix.end(row); successorEntryIt != successorEntryIte; ++successorEntryIt) { - if (!currentStates.get(successorEntryIt->getColumn())) { + for (auto const& successor : transitionMatrix.getRow(row)) { + auto successorState = successor.getColumn(); + if (!currentStates->get(successorState)) { addToStatesWithProbability1 = false; goto afterCheckLoop; } - if (nextStates.get(successorEntryIt->getColumn())) { + if (!hasAtLeastOneSuccessorWithProbability1 && nextStates->get(successorState)) { hasAtLeastOneSuccessorWithProbability1 = true; } } @@ -927,21 +937,27 @@ namespace storm { // add it to the set of states for the next iteration and perform a backward search from // that state. if (addToStatesWithProbability1) { - nextStates.set(predecessorEntryIt->getColumn(), true); - stack.push_back(predecessorEntryIt->getColumn()); + ++nextStatesSetBits; + nextStates->set(predecessorState, true); + stack.push_back(predecessorState); } } } } - // Check whether we need to perform an additional iteration. - if (currentStates == nextStates) { + if (currentStatesSetBits == nextStatesSetBits && *currentStates == *nextStates) { done = true; } else { - currentStates = std::move(nextStates); + // Prepare next iteration. + // The nextStates become the new currentStates. + std::swap(currentStates, nextStates); + currentStatesSetBits = nextStatesSetBits; + *nextStates = psiStates; + nextStatesSetBits = numPsiStates; + } } - return currentStates; + return *currentStates; } template