From b28b8273623e46e264a08ed0a380ddbaf9f80436 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sat, 11 May 2013 19:05:04 +0200 Subject: [PATCH] All methods of GraphAnalyzer: * commented, * return values instead of passing result variables by reference. --- src/utility/GraphAnalyzer.h | 43 ++++++++++++++++++++++++++++--------- 1 file changed, 33 insertions(+), 10 deletions(-) diff --git a/src/utility/GraphAnalyzer.h b/src/utility/GraphAnalyzer.h index 9f33a2f7f..2b61b877d 100644 --- a/src/utility/GraphAnalyzer.h +++ b/src/utility/GraphAnalyzer.h @@ -421,13 +421,11 @@ public: } /*! - * Performs a decomposition of the given matrix belonging to a nondeterministic model and vector indicating the - * nondeterministic choices into SCCs. + * Performs a decomposition of the given nondetermistic model into its SCCs. * - * @param matrix The matrix of the nondeterminstic model to decompose. - * @param nondeterministicChoiceIndices A vector indicating the non-deterministic choices of each state in the matrix. + * @param model The nondeterminstic model to decompose. * @return A pair whose first component represents the SCCs and whose second component represents the dependency - * transitions of the SCCs. + * graph of the SCCs. */ template static std::pair>, storm::models::GraphTransitions> performSccDecomposition(storm::models::AbstractNondeterministicModel const& model) { @@ -455,12 +453,13 @@ public: std::vector topologicalSort; topologicalSort.reserve(transitions.getNumberOfStates()); + // Prepare the stacks needed for recursion. std::vector recursionStack; recursionStack.reserve(transitions.getNumberOfStates()); - std::vector::stateSuccessorIterator> iteratorRecursionStack; iteratorRecursionStack.reserve(transitions.getNumberOfStates()); + // Perform a depth-first search over the given transitions and record states in the reverse order they were visited. storm::storage::BitVector visitedStates(transitions.getNumberOfStates()); for (uint_fast64_t state = 0; state < transitions.getNumberOfStates(); ++state) { if (!visitedStates.get(state)) { @@ -515,20 +514,28 @@ public: } private: + /*! + * Performs an SCC decomposition of the system given by its forward transitions. + * + * @param forwardTransitions The (forward) transition relation of the model to decompose. + * @return A pair whose first component represents the SCCs and whose second component represents the dependency + * graph of the SCCs. + */ template - static std::pair>, storm::models::GraphTransitions> performSccDecomposition(uint_fast64_t numberOfStates, storm::models::GraphTransitions const& forwardTransitions) { + static std::pair>, storm::models::GraphTransitions> performSccDecomposition(storm::models::GraphTransitions const& forwardTransitions) { std::pair>, storm::models::GraphTransitions> sccDecomposition; - + uint_fast64_t numberOfStates = forwardTransitions.getNumberOfStates(); + + // Set up the environment of Tarjan's algorithm. std::vector tarjanStack; tarjanStack.reserve(numberOfStates); storm::storage::BitVector tarjanStackStates(numberOfStates); - std::vector stateIndices(numberOfStates); std::vector lowlinks(numberOfStates); storm::storage::BitVector visitedStates(numberOfStates); - std::map stateToSccMap; + // Start the search for SCCs from every vertex in the graph structure, because there is. uint_fast64_t currentIndex = 0; for (uint_fast64_t state = 0; state < numberOfStates; ++state) { if (!visitedStates.get(state)) { @@ -536,10 +543,26 @@ private: } } + // Finally, determine the dependency graph over the SCCs and return result. sccDecomposition.second = storm::models::GraphTransitions(forwardTransitions, sccDecomposition.first, stateToSccMap); return sccDecomposition; } + /*! + * Performs an SCC decomposition using Tarjan's algorithm. + * + * @param startState The state at which the search is started. + * @param currentIndex The index that is to be used as the next free index. + * @param stateIndices The vector that stores the index for each state. + * @param lowlinks A vector that stores the lowlink of each state, i.e. the lowest index of a state reachable from + * a particular state. + * @param tarjanStack A stack used for Tarjan's algorithm. + * @param tarjanStackStates A bit vector that represents all states that are currently contained in tarjanStack. + * @param visitedStates A bit vector that stores all states that have already been visited. + * @param forwardTransitions The (forward) transition relation of the graph structure. + * @param stronglyConnectedComponents A vector of strongly connected components to which newly found SCCs are added. + * @param stateToSccMap A mapping from state indices to SCC indices that maps each state to its SCC. + */ template static void performSccDecompositionHelper(uint_fast64_t startState, uint_fast64_t& currentIndex, std::vector& stateIndices, std::vector& lowlinks, std::vector& tarjanStack, storm::storage::BitVector& tarjanStackStates, storm::storage::BitVector& visitedStates, storm::models::GraphTransitions const& forwardTransitions, std::vector>& stronglyConnectedComponents, std::map& stateToSccMap) { // Create the stacks needed for turning the recursive formulation of Tarjan's algorithm