diff --git a/src/modelchecker/reachability/SparseSccModelChecker.cpp b/src/modelchecker/reachability/SparseSccModelChecker.cpp index a74c801f9..fe8cb821b 100644 --- a/src/modelchecker/reachability/SparseSccModelChecker.cpp +++ b/src/modelchecker/reachability/SparseSccModelChecker.cpp @@ -42,7 +42,7 @@ namespace storm { storm::storage::BitVector statesWithProbability0 = statesWithProbability01.first; storm::storage::BitVector statesWithProbability1 = statesWithProbability01.second; storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1); - + // If the initial state is known to have either probability 0 or 1, we can directly return the result. if (!maybeStates.get(initialStateIndex)) { return statesWithProbability0.get(initialStateIndex) ? 0 : 1; @@ -77,12 +77,27 @@ namespace storm { if (scc.getNumberOfSetBits() > SparseSccModelChecker::maximalSccSize) { // Here, we further decompose the SCC into sub-SCCs. storm::storage::StronglyConnectedComponentDecomposition decomposition(forwardTransitions, scc & ~entryStates, true, false); - + // To eliminate the remaining one-state SCCs, we need to keep track of them. storm::storage::BitVector remainingStates(scc); - // And then recursively treat all sub-SCCs. - for (auto const& newScc : decomposition) { + // Store a bit vector of remaining SCCs so we can be flexible when it comes to the order in which + // we eliminate the SCCs. + storm::storage::BitVector remainingSccs(decomposition.size(), true); + + // First, get rid of the trivial SCCs. + for (uint_fast64_t sccIndex = 0; sccIndex < decomposition.size(); ++sccIndex) { + storm::storage::StronglyConnectedComponent const& scc = decomposition.getBlock(sccIndex); + if (scc.isTrivial()) { + storm::storage::sparse::state_type onlyState = *scc.begin(); + eliminateState(matrix, oneStepProbabilities, onlyState, backwardTransitions); + remainingSccs.set(sccIndex, false); + } + } + + // And then recursively treat the remaining sub-SCCs. + for (auto sccIndex : remainingSccs) { + storm::storage::StronglyConnectedComponent const& newScc = decomposition.getBlock(sccIndex); // If the SCC consists of just one state, we do not explore it recursively, but rather eliminate // it directly. if (newScc.size() == 1) { @@ -106,7 +121,7 @@ namespace storm { // Recursively descend in SCC-hierarchy. treatScc(dtmc, matrix, oneStepProbabilities, entryStates, newSccAsBitVector, forwardTransitions, backwardTransitions, true, level + 1); } - + // If we are not supposed to eliminate the entry states, we need to take them out of the set of // remaining states. if (!eliminateEntryStates) { @@ -121,7 +136,7 @@ namespace storm { } else { // In this case, we perform simple state elimination in the current SCC. storm::storage::BitVector remainingStates(scc); - + // If we are not supposed to eliminate the entry states, we need to take them out of the set of // remaining states. if (!eliminateEntryStates) { @@ -252,7 +267,7 @@ namespace storm { typename FlexibleSparseMatrix::row_type newPredecessors; newPredecessors.reserve((last1 - first1) + (last2 - first2)); std::insert_iterator::row_type> result(newPredecessors, newPredecessors.end()); - + for (; first1 != last1; ++result) { if (first2 == last2) { @@ -279,7 +294,7 @@ namespace storm { // Now move the new predecessors in place. successorBackwardTransitions = std::move(newPredecessors); } - + // Clear the eliminated row to reduce memory consumption. currentStateSuccessors.clear(); diff --git a/src/storage/StronglyConnectedComponentDecomposition.cpp b/src/storage/StronglyConnectedComponentDecomposition.cpp index d8e80a36f..c6c8f9913 100644 --- a/src/storage/StronglyConnectedComponentDecomposition.cpp +++ b/src/storage/StronglyConnectedComponentDecomposition.cpp @@ -86,6 +86,17 @@ namespace storm { this->blocks[stateToSccMapping[state]].insert(state); } + // Now flag all trivial SCCs as such. + for (uint_fast64_t sccIndex = 0; sccIndex < sccCount; ++sccIndex) { + if (this->blocks[sccIndex].size() == 1) { + uint_fast64_t onlyState = *this->blocks[sccIndex].begin(); + + if (!statesWithSelfLoop.get(onlyState)) { + this->blocks[sccIndex].setIsTrivial(true); + } + } + } + // If requested, we need to drop some SCCs. if (onlyBottomSccs || dropNaiveSccs) { storm::storage::BitVector blocksToDrop(sccCount); @@ -93,12 +104,8 @@ namespace storm { // If requested, we need to delete all naive SCCs. if (dropNaiveSccs) { for (uint_fast64_t sccIndex = 0; sccIndex < sccCount; ++sccIndex) { - if (this->blocks[sccIndex].size() == 1) { - uint_fast64_t onlyState = *this->blocks[sccIndex].begin(); - - if (!statesWithSelfLoop.get(onlyState)) { - blocksToDrop.set(sccIndex); - } + if (this->blocks[sccIndex].isTrivial()) { + blocksToDrop.set(sccIndex); } } }