diff --git a/src/modelchecker/reachability/SparseSccModelChecker.cpp b/src/modelchecker/reachability/SparseSccModelChecker.cpp index aa3f9d950..f6e65cdb5 100644 --- a/src/modelchecker/reachability/SparseSccModelChecker.cpp +++ b/src/modelchecker/reachability/SparseSccModelChecker.cpp @@ -150,7 +150,21 @@ namespace storm { } // Now, we return the value for the only initial state. - return oneStepProbabilities[initialStateIndex]; + return simplify(oneStepProbabilities[initialStateIndex]); + } + + template + bool hasSelfLoop(storm::storage::sparse::state_type state, FlexibleSparseMatrix const& matrix) { + for (auto const& entry : matrix.getRow(state)) { + if (entry.getColumn() < state) { + continue; + } else if (entry.getColumn() > state) { + return false; + } else if (entry.getColumn() == state) { + return true; + } + } + return false; } template @@ -179,9 +193,10 @@ namespace storm { remainingSccs.set(sccIndex, false); } } + STORM_LOG_DEBUG("Eliminated all trivial SCCs."); // And then recursively treat the remaining sub-SCCs. - STORM_LOG_DEBUG("Eliminating remaining SCCs on level " << level << "."); + STORM_LOG_DEBUG("Eliminating " << remainingSccs.getNumberOfSetBits() << " remaining SCCs on level " << level << "."); for (auto sccIndex : remainingSccs) { storm::storage::StronglyConnectedComponent const& newScc = decomposition.getBlock(sccIndex); @@ -205,12 +220,26 @@ namespace storm { } else { // In this case, we perform simple state elimination in the current SCC. + STORM_LOG_DEBUG("SCC of size " << scc.getNumberOfSetBits() << " is small enough to be eliminated directly."); storm::storage::BitVector remainingStates = scc & ~entryStates; + // Eliminate the remaining states that do not have a self-loop (in the current, i.e. modified) + // transition probability matrix. + for (auto const& state : remainingStates) { + if (!hasSelfLoop(state, matrix)) { + eliminateState(matrix, oneStepProbabilities, state, backwardTransitions); + remainingStates.set(state, false); + } + } + + STORM_LOG_DEBUG("Eliminated all states without self-loop."); + // Eliminate the remaining states. for (auto const& state : remainingStates) { eliminateState(matrix, oneStepProbabilities, state, backwardTransitions); } + + STORM_LOG_DEBUG("Eliminated all states with self-loop."); } // Finally, eliminate the entry states (if we are required to do so). @@ -224,6 +253,7 @@ namespace storm { entryStateQueue.push_back(state); } } + STORM_LOG_DEBUG("Eliminated/added entry states."); return maximalDepth; } @@ -235,7 +265,7 @@ namespace storm { void SparseSccModelChecker::eliminateState(FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix& backwardTransitions) { ++counter; - STORM_LOG_DEBUG("Eliminating state " << counter << "."); + STORM_LOG_DEBUG("Eliminating state " << state << "."); if (counter > matrix.getNumberOfRows() / 10) { ++chunkCounter; STORM_PRINT_AND_LOG("Eliminated " << (chunkCounter * 10) << "% of the states." << std::endl); @@ -491,6 +521,12 @@ namespace storm { return this->data[index]; } + template + typename FlexibleSparseMatrix::row_type const& FlexibleSparseMatrix::getRow(index_type index) const { + return this->data[index]; + } + + template typename FlexibleSparseMatrix::index_type FlexibleSparseMatrix::getNumberOfRows() const { return this->data.size(); diff --git a/src/modelchecker/reachability/SparseSccModelChecker.h b/src/modelchecker/reachability/SparseSccModelChecker.h index d624b7e15..ba25b5f68 100644 --- a/src/modelchecker/reachability/SparseSccModelChecker.h +++ b/src/modelchecker/reachability/SparseSccModelChecker.h @@ -24,6 +24,7 @@ namespace storm { void reserveInRow(index_type row, index_type numberOfElements); row_type& getRow(index_type); + row_type const& getRow(index_type) const; index_type getNumberOfRows() const;