diff --git a/src/utility/GraphAnalyzer.h b/src/utility/GraphAnalyzer.h index f9b6b783a..75437040a 100644 --- a/src/utility/GraphAnalyzer.h +++ b/src/utility/GraphAnalyzer.h @@ -415,6 +415,59 @@ public: *statesWithProbability1 = *currentStates; delete currentStates; } + + template + static uint_fast64_t performSccDecomposition(storm::models::AbstractNondeterministicModel& model) { + // Get some temporaries for convenience. + std::shared_ptr> transitionMatrix = model.getTransitionMatrix(); + std::shared_ptr> nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices(); + uint_fast64_t numberOfStates = model.getNumberOfStates(); + + // Get the forward transition relation from the model to ease the search. + storm::models::GraphTransitions forwardTransitions(transitionMatrix, nondeterministicChoiceIndices, true); + + std::vector tarjanStack; + tarjanStack.reserve(numberOfStates); + storm::storage::BitVector tarjanStackStates(numberOfStates); + + std::vector stateIndices(numberOfStates); + std::vector lowlinks(numberOfStates); + storm::storage::BitVector visitedStates(numberOfStates); + + uint_fast64_t currentIndex = 0; + + for (uint_fast64_t i = 0; i < numberOfStates; ++i) { + if (!visitedStates.get(i)) { + performSccDecompositionHelper(i, currentIndex, stateIndices, lowlinks, tarjanStack, visitedStates, forwardTransitions); + } + } + + + return 0; + } + +private: + template + static void performSccDecompositionHelper(uint_fast64_t currentState, uint_fast64_t& currentIndex, std::vector& stateIndices, std::vector& lowlinks, std::vector& tarjanStack, storm::storage::BitVector& tarjanStackStates, storm::storage::BitVector& visitedStates, storm::models::GraphTransitions& forwardTransitions) { + std::vector recursionStack; + recursionStack.reserve(lowlinks.size()); + + stateIndices[currentState] = currentIndex; + lowlinks[currentState] = currentIndex; + ++currentIndex; + + tarjanStack.push_back(currentState); + tarjanStackStates.set(currentState, true); + + for(auto it = forwardTransitions.beginStateSuccessorsIterator(currentState); it != forwardTransitions.endStateSuccessorsIterator(currentState); ++it) { + if (!visitedStates.get(*it)) { + + } else if (tarjanStackStates.get(*it)) { + lowlinks[currentState] = std::min(lowlinks[currentState], stateIndices[*it]); + } + } + + } }; } // namespace utility