From ab11d3c2070a7a984ac4049681f9a91e914ca275 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 9 May 2013 23:38:38 +0200
Subject: [PATCH] Further refactoring of GraphAnalyzer class. Some comments are
 still missing and GraphAnalyzer should be made a namespace instead of a class
 with static methods only.

---
 ...ologicalValueIterationMdpPrctlModelChecker.h | 10 +++++-----
 src/utility/GraphAnalyzer.h                     | 17 +++++++++++------
 2 files changed, 16 insertions(+), 11 deletions(-)

diff --git a/src/modelchecker/TopologicalValueIterationMdpPrctlModelChecker.h b/src/modelchecker/TopologicalValueIterationMdpPrctlModelChecker.h
index 248749624..1466c02ec 100644
--- a/src/modelchecker/TopologicalValueIterationMdpPrctlModelChecker.h
+++ b/src/modelchecker/TopologicalValueIterationMdpPrctlModelChecker.h
@@ -67,11 +67,11 @@ private:
 		bool relative = s->get<bool>("relative");
 
 		// Now, we need to determine the SCCs of the MDP and a topological sort.
-		std::vector<std::vector<uint_fast64_t>> stronglyConnectedComponents;
-		storm::models::GraphTransitions<Type> stronglyConnectedComponentsDependencyGraph;
-		storm::utility::GraphAnalyzer::performSccDecomposition(matrix, nondeterministicChoiceIndices, stronglyConnectedComponents, stronglyConnectedComponentsDependencyGraph);
-		std::vector<uint_fast64_t> topologicalSort;
-		storm::utility::GraphAnalyzer::getTopologicalSort(stronglyConnectedComponentsDependencyGraph, topologicalSort);
+        std::pair<std::vector<std::vector<uint_fast64_t>>, storm::models::GraphTransitions<Type>> sccDecomposition = storm::utility::GraphAnalyzer::performSccDecomposition(this->getModel(), stronglyConnectedComponents, stronglyConnectedComponentsDependencyGraph);
+        std::vector<std::vector<uint_fast64_t>> stronglyConnectedComponents = std::move(sccDecomposition.first);
+        storm::models::GraphTransitions<Type> stronglyConnectedComponentsDependencyGraph = std::move(sccDecomposition.second);
+        
+		std::vector<uint_fast64_t> topologicalSort = storm::utility::GraphAnalyzer::getTopologicalSort(stronglyConnectedComponentsDependencyGraph);
 
 		// Set up the environment for the power method.
 		std::vector<Type> multiplyResult(matrix.getRowCount());
diff --git a/src/utility/GraphAnalyzer.h b/src/utility/GraphAnalyzer.h
index 17971a407..9f33a2f7f 100644
--- a/src/utility/GraphAnalyzer.h
+++ b/src/utility/GraphAnalyzer.h
@@ -430,10 +430,12 @@ public:
      * transitions of the SCCs.
      */
 	template <typename T>
-	static std::pair<std::vector<std::vector<uint_fast64_t>>, storm::models::GraphTransitions<T>> performSccDecomposition(storm::storage::SparseMatrix<T> const& matrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices) {
+	static std::pair<std::vector<std::vector<uint_fast64_t>>, storm::models::GraphTransitions<T>> performSccDecomposition(storm::models::AbstractNondeterministicModel<T> const& model) {
 		LOG4CPLUS_INFO(logger, "Computing SCC decomposition.");
-		// Get the forward transition relation from the model to ease the search.
-		storm::models::GraphTransitions<T> forwardTransitions(matrix, nondeterministicChoiceIndices, true);
+
+        // Get the forward transition relation from the model to ease the search.
+        std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices();
+		storm::models::GraphTransitions<T> forwardTransitions(model.getTransitionMatrix(), nondeterministicChoiceIndices, true);
 
 		// Perform the actual SCC decomposition based on the graph-transitions of the system.
 		std::pair<std::vector<std::vector<uint_fast64_t>>, storm::models::GraphTransitions<T>> result = performSccDecomposition(nondeterministicChoiceIndices.size() - 1, forwardTransitions);
@@ -514,7 +516,9 @@ public:
 
 private:
 	template <typename T>
-	static void performSccDecomposition(uint_fast64_t numberOfStates, storm::models::GraphTransitions<T> const& forwardTransitions, std::vector<std::vector<uint_fast64_t>>& stronglyConnectedComponents, storm::models::GraphTransitions<T>& stronglyConnectedComponentsDependencyGraph) {
+	static std::pair<std::vector<std::vector<uint_fast64_t>>, storm::models::GraphTransitions<T>> performSccDecomposition(uint_fast64_t numberOfStates, storm::models::GraphTransitions<T> const& forwardTransitions) {
+        std::pair<std::vector<std::vector<uint_fast64_t>>, storm::models::GraphTransitions<T>> sccDecomposition;
+
 		std::vector<uint_fast64_t> tarjanStack;
 		tarjanStack.reserve(numberOfStates);
 		storm::storage::BitVector tarjanStackStates(numberOfStates);
@@ -528,11 +532,12 @@ private:
 		uint_fast64_t currentIndex = 0;
 		for (uint_fast64_t state = 0; state < numberOfStates; ++state) {
 			if (!visitedStates.get(state)) {
-				performSccDecompositionHelper(state, currentIndex, stateIndices, lowlinks, tarjanStack, tarjanStackStates, visitedStates, forwardTransitions, stronglyConnectedComponents, stateToSccMap);
+				performSccDecompositionHelper(state, currentIndex, stateIndices, lowlinks, tarjanStack, tarjanStackStates, visitedStates, forwardTransitions, sccDecomposition.first, stateToSccMap);
 			}
 		}
 
-		stronglyConnectedComponentsDependencyGraph = storm::models::GraphTransitions<T>(forwardTransitions, stronglyConnectedComponents, stateToSccMap);
+		sccDecomposition.second = storm::models::GraphTransitions<T>(forwardTransitions, sccDecomposition.first, stateToSccMap);
+        return sccDecomposition;
 	}
 
 	template <typename T>