Refactored SCC-Decomposition design as a preparation step for computing maximal end components of Markov automata.

Former-commit-id: 4596ba71ec

src/models/AbstractModel.h

@@ -10,6 +10,7 @@
 #include "src/storage/BitVector.h"
 #include "src/storage/SparseMatrix.h"
 #include "src/storage/VectorSet.h"
+#include "src/storage/StronglyConnectedComponentDecomposition.h"
 #include "src/utility/Hash.h"
 
 namespace storm {
@@ -146,15 +147,14 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
          * @param partition A vector containing the blocks of the partition of the system.
          * @return A sparse matrix with bool entries that represents the dependency graph of the blocks of the partition.
          */
-        storm::storage::SparseMatrix<bool> extractPartitionDependencyGraph(std::vector<std::vector<uint_fast64_t>> const& partition) const {
-            uint_fast64_t numberOfStates = partition.size();
+        storm::storage::SparseMatrix<bool> extractPartitionDependencyGraph(storm::storage::Decomposition const& decomposition) const {
+            uint_fast64_t numberOfStates = decomposition.size();
             
-            // First, we need to create a mapping of states to their SCC index, to ease the computation
-            // of dependency transitions later.
+            // First, we need to create a mapping of states to their SCC index, to ease the computation of dependency transitions later.
             std::vector<uint_fast64_t> stateToBlockMap(this->getNumberOfStates());
-            for (uint_fast64_t i = 0; i < numberOfStates; ++i) {
-                for (uint_fast64_t j = 0; j < partition[i].size(); ++j) {
-                    stateToBlockMap[partition[i][j]] = i;
+            for (uint_fast64_t i = 0; i < decomposition.size(); ++i) {
+                for (auto state : decomposition[i]) {
+                    stateToBlockMap[state] = i;
                 }
             }
             
@@ -162,12 +162,12 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
             storm::storage::SparseMatrix<bool> dependencyGraph(numberOfStates);
             dependencyGraph.initialize();
             
-            for (uint_fast64_t currentBlockIndex = 0; currentBlockIndex < partition.size(); ++currentBlockIndex) {
+            for (uint_fast64_t currentBlockIndex = 0; currentBlockIndex < decomposition.size(); ++currentBlockIndex) {
                 // Get the next block.
-                std::vector<uint_fast64_t> const& block = partition[currentBlockIndex];
+                typename storm::storage::Decomposition::Block const& block = decomposition[currentBlockIndex];
                 
                 // Now, we determine the blocks which are reachable (in one step) from the current block.
-                std::set<uint_fast64_t> allTargetBlocks;
+                storm::storage::VectorSet<uint_fast64_t> allTargetBlocks;
                 for (auto state : block) {
                     typename storm::storage::SparseMatrix<T>::Rows rows = this->getRows(state);
                     for (auto& transition : rows) {

src/storage/Decomposition.cpp

@@ -0,0 +1,57 @@
+#include "src/storage/Decomposition.h"
+
+namespace storm {
+    namespace storage {
+        
+        Decomposition::Decomposition() : blocks() {
+            // Intentionally left empty.
+        }
+        
+        Decomposition::Decomposition(Decomposition const& other) : blocks(other.blocks) {
+            // Intentionally left empty.
+        }
+        
+        Decomposition& Decomposition::operator=(Decomposition const& other) {
+            this->blocks = other.blocks;
+            return *this;
+        }
+        
+        Decomposition::Decomposition(Decomposition&& other) : blocks(std::move(other.blocks)) {
+            // Intentionally left empty.
+        }
+        
+        Decomposition& Decomposition::operator=(Decomposition&& other) {
+            this->blocks = std::move(other.blocks);
+            return *this;
+        }
+        
+        size_t Decomposition::size() const {
+            return blocks.size();
+        }
+        
+        Decomposition::iterator Decomposition::begin() {
+            return blocks.begin();
+        }
+        
+        Decomposition::iterator Decomposition::end() {
+            return blocks.end();
+        }
+        
+        Decomposition::const_iterator Decomposition::begin() const {
+            return blocks.begin();
+        }
+        
+        Decomposition::const_iterator Decomposition::end() const {
+            return blocks.end();
+        }
+        
+        Decomposition::Block const& Decomposition::getBlock(uint_fast64_t index) const {
+            return blocks.at(index);
+        }
+        
+        Decomposition::Block const& Decomposition::operator[](uint_fast64_t index) const {
+            return blocks[index];
+        }
+        
+    } // namespace storage
+} // namespace storm

src/storage/Decomposition.h

@@ -0,0 +1,54 @@
+#ifndef STORM_STORAGE_DECOMPOSITION_H_
+#define STORM_STORAGE_DECOMPOSITION_H_
+
+#include <vector>
+
+#include "src/storage/VectorSet.h"
+
+namespace storm {
+    namespace storage {
+        
+        /*!
+         * This class represents the decomposition of a model into state sets.
+         */
+        class Decomposition {
+        public:
+            typedef storm::storage::VectorSet<uint_fast64_t> Block;
+            typedef std::vector<Block>::iterator iterator;
+            typedef std::vector<Block>::const_iterator const_iterator;
+            
+            /*
+             * Creates an empty SCC decomposition.
+             */
+            Decomposition();
+            
+            Decomposition(Decomposition const& other);
+            
+            Decomposition& operator=(Decomposition const& other);
+            
+            Decomposition(Decomposition&& other);
+            
+            Decomposition& operator=(Decomposition&& other);
+            
+            size_t size() const;
+            
+            iterator begin();
+            
+            iterator end();
+            
+            const_iterator begin() const;
+            
+            const_iterator end() const;
+            
+            Block const& getBlock(uint_fast64_t index) const;
+            
+            Block const& operator[](uint_fast64_t index) const;
+            
+        protected:
+            // The blocks of the decomposition.
+            std::vector<Block> blocks;
+        };
+    }
+}
+
+#endif /* STORM_STORAGE_DECOMPOSITION_H_ */

src/storage/StronglyConnectedComponentDecomposition.cpp

@@ -0,0 +1,156 @@
+#include "src/storage/StronglyConnectedComponentDecomposition.h"
+#include "src/models/AbstractModel.h"
+
+namespace storm {
+    namespace storage {
+        template<typename T>
+        StronglyConnectedComponentDecomposition<T>::StronglyConnectedComponentDecomposition() : Decomposition() {
+            // Intentionally left empty.
+        }
+
+        template <typename T>
+        StronglyConnectedComponentDecomposition<T>::StronglyConnectedComponentDecomposition(storm::models::AbstractModel<T> const& model) : Decomposition() {
+            performSccDecomposition(model);
+        }
+        
+        template <typename T>
+        StronglyConnectedComponentDecomposition<T>::StronglyConnectedComponentDecomposition(StronglyConnectedComponentDecomposition const& other) : Decomposition(other) {
+            // Intentionally left empty.
+        }
+        
+        template <typename T>
+        StronglyConnectedComponentDecomposition<T>& StronglyConnectedComponentDecomposition<T>::operator=(StronglyConnectedComponentDecomposition const& other) {
+            this->blocks = other.blocks;
+            return *this;
+        }
+        
+        template <typename T>
+        StronglyConnectedComponentDecomposition<T>::StronglyConnectedComponentDecomposition(StronglyConnectedComponentDecomposition&& other) : Decomposition(std::move(other)) {
+            // Intentionally left empty.
+        }
+        
+        template <typename T>
+        StronglyConnectedComponentDecomposition<T>& StronglyConnectedComponentDecomposition<T>::operator=(StronglyConnectedComponentDecomposition&& other) {
+            this->blocks = std::move(other.blocks);
+            return *this;
+        }
+        
+        template <typename T>
+        void StronglyConnectedComponentDecomposition<T>::performSccDecomposition(storm::models::AbstractModel<T> const& model) {
+            LOG4CPLUS_INFO(logger, "Computing SCC decomposition.");
+            
+            uint_fast64_t numberOfStates = model.getNumberOfStates();
+            
+            // Set up the environment of Tarjan's algorithm.
+            std::vector<uint_fast64_t> tarjanStack;
+            tarjanStack.reserve(numberOfStates);
+            storm::storage::BitVector tarjanStackStates(numberOfStates);
+            std::vector<uint_fast64_t> stateIndices(numberOfStates);
+            std::vector<uint_fast64_t> lowlinks(numberOfStates);
+            storm::storage::BitVector visitedStates(numberOfStates);
+            
+            // 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)) {
+                    performSccDecompositionHelper(model, state, currentIndex, stateIndices, lowlinks, tarjanStack, tarjanStackStates, visitedStates);
+                }
+            }
+            
+            LOG4CPLUS_INFO(logger, "Done computing SCC decomposition.");
+        }
+        
+        template <typename T>
+        void StronglyConnectedComponentDecomposition<T>::performSccDecompositionHelper(storm::models::AbstractModel<T> const& model, uint_fast64_t startState, uint_fast64_t& currentIndex, std::vector<uint_fast64_t>& stateIndices, std::vector<uint_fast64_t>& lowlinks, std::vector<uint_fast64_t>& tarjanStack, storm::storage::BitVector& tarjanStackStates, storm::storage::BitVector& visitedStates) {
+            // Create the stacks needed for turning the recursive formulation of Tarjan's algorithm
+            // into an iterative version. In particular, we keep one stack for states and one stack
+            // for the iterators. The last one is not strictly needed, but reduces iteration work when
+            // all successors of a particular state are considered.
+            std::vector<uint_fast64_t> recursionStateStack;
+            recursionStateStack.reserve(lowlinks.size());
+            std::vector<typename storm::storage::SparseMatrix<T>::ConstIterator> recursionIteratorStack;
+            recursionIteratorStack.reserve(lowlinks.size());
+            std::vector<bool> statesInStack(lowlinks.size());
+            
+            // Initialize the recursion stacks with the given initial state (and its successor iterator).
+            recursionStateStack.push_back(startState);
+            recursionIteratorStack.push_back(model.getRows(startState).begin());
+            
+        recursionStepForward:
+            while (!recursionStateStack.empty()) {
+                uint_fast64_t currentState = recursionStateStack.back();
+                typename storm::storage::SparseMatrix<T>::ConstIterator successorIt = recursionIteratorStack.back();
+                
+                // Perform the treatment of newly discovered state as defined by Tarjan's algorithm
+                visitedStates.set(currentState, true);
+                stateIndices[currentState] = currentIndex;
+                lowlinks[currentState] = currentIndex;
+                ++currentIndex;
+                tarjanStack.push_back(currentState);
+                tarjanStackStates.set(currentState, true);
+                
+                // Now, traverse all successors of the current state.
+                for(; successorIt != model.getRows(currentState).end(); ++successorIt) {
+                    // If we have not visited the successor already, we need to perform the procedure
+                    // recursively on the newly found state.
+                    if (!visitedStates.get(successorIt.column())) {
+                        // Save current iterator position so we can continue where we left off later.
+                        recursionIteratorStack.pop_back();
+                        recursionIteratorStack.push_back(successorIt);
+                        
+                        // Put unvisited successor on top of our recursion stack and remember that.
+                        recursionStateStack.push_back(successorIt.column());
+                        statesInStack[successorIt.column()] = true;
+                        
+                        // Also, put initial value for iterator on corresponding recursion stack.
+                        recursionIteratorStack.push_back(model.getRows(successorIt.column()).begin());
+                        
+                        // Perform the actual recursion step in an iterative way.
+                        goto recursionStepForward;
+                        
+                    recursionStepBackward:
+                        lowlinks[currentState] = std::min(lowlinks[currentState], lowlinks[successorIt.column()]);
+                    } else if (tarjanStackStates.get(successorIt.column())) {
+                        // Update the lowlink of the current state.
+                        lowlinks[currentState] = std::min(lowlinks[currentState], stateIndices[successorIt.column()]);
+                    }
+                }
+                
+                // If the current state is the root of a SCC, we need to pop all states of the SCC from
+                // the algorithm's stack.
+                if (lowlinks[currentState] == stateIndices[currentState]) {
+                    Block scc;
+                    
+                    uint_fast64_t lastState = 0;
+                    do {
+                        // Pop topmost state from the algorithm's stack.
+                        lastState = tarjanStack.back();
+                        tarjanStack.pop_back();
+                        tarjanStackStates.set(lastState, false);
+                        
+                        // Add the state to the current SCC.
+                        scc.insert(lastState);
+                    } while (lastState != currentState);
+                    this->blocks.emplace_back(std::move(scc));
+                }
+                
+                // If we reach this point, we have completed the recursive descent for the current state.
+                // That is, we need to pop it from the recursion stacks.
+                recursionStateStack.pop_back();
+                recursionIteratorStack.pop_back();
+                
+                // If there is at least one state under the current one in our recursion stack, we need
+                // to restore the topmost state as the current state and jump to the part after the
+                // original recursive call.
+                if (recursionStateStack.size() > 0) {
+                    currentState = recursionStateStack.back();
+                    successorIt = recursionIteratorStack.back();
+                    
+                    goto recursionStepBackward;
+                }
+            }
+        }
+        
+        template class StronglyConnectedComponentDecomposition<double>;
+    } // namespace storage
+} // namespace storm

src/storage/StronglyConnectedComponentDecomposition.h

@@ -0,0 +1,49 @@
+#ifndef STORM_STORAGE_STRONGLYCONNECTEDCOMPONENTDECOMPOSITION_H_
+#define STORM_STORAGE_STRONGLYCONNECTEDCOMPONENTDECOMPOSITION_H_
+
+#include "src/storage/Decomposition.h"
+#include "src/storage/VectorSet.h"
+#include "src/storage/BitVector.h"
+#include "src/storage/SparseMatrix.h"
+
+namespace storm {
+    namespace models {
+        // Forward declare the abstract model class.
+        template <typename T> class AbstractModel;
+    }
+    
+    namespace storage {
+        
+        /*!
+         * This class represents the decomposition of a graph-like structure into its strongly connected components.
+         */
+        template <typename T>
+        class StronglyConnectedComponentDecomposition : public Decomposition {
+        public:
+            /*
+             * Creates an empty SCC decomposition.
+             */
+            StronglyConnectedComponentDecomposition();
+            
+            /*
+             * Creates an SCC decomposition of the given model.
+             */
+            StronglyConnectedComponentDecomposition(storm::models::AbstractModel<T> const& model);
+            
+            StronglyConnectedComponentDecomposition(StronglyConnectedComponentDecomposition const& other);
+            
+            StronglyConnectedComponentDecomposition& operator=(StronglyConnectedComponentDecomposition const& other);
+            
+            StronglyConnectedComponentDecomposition(StronglyConnectedComponentDecomposition&& other);
+            
+            StronglyConnectedComponentDecomposition& operator=(StronglyConnectedComponentDecomposition&& other);
+            
+        private:
+            void performSccDecomposition(storm::models::AbstractModel<T> const& model);
+            
+            void performSccDecompositionHelper(storm::models::AbstractModel<T> const& model, uint_fast64_t startState, uint_fast64_t& currentIndex, std::vector<uint_fast64_t>& stateIndices, std::vector<uint_fast64_t>& lowlinks, std::vector<uint_fast64_t>& tarjanStack, storm::storage::BitVector& tarjanStackStates, storm::storage::BitVector& visitedStates);
+        };
+    }
+}
+
+#endif /* STORM_STORAGE_STRONGLYCONNECTEDCOMPONENTDECOMPOSITION_H_ */

src/storage/VectorSet.h

@@ -10,6 +10,8 @@
 
 #include <algorithm>
 #include <iostream>
+#include <vector>
+#include <set>
 
 namespace storm  {
     namespace storage {

src/utility/graph.h

@@ -550,143 +550,6 @@ namespace storm {
                 return result;
             }
             
-            /*!
-             * 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 matrix The transition matrix representing the graph structure.
-             * @param stronglyConnectedComponents A vector of strongly connected components to which newly found SCCs are added.
-             */
-            template <typename T>
-            void performSccDecompositionHelper(uint_fast64_t startState, uint_fast64_t& currentIndex, std::vector<uint_fast64_t>& stateIndices, std::vector<uint_fast64_t>& lowlinks, std::vector<uint_fast64_t>& tarjanStack, storm::storage::BitVector& tarjanStackStates, storm::storage::BitVector& visitedStates, storm::storage::SparseMatrix<T> const& matrix, std::vector<std::vector<uint_fast64_t>>& stronglyConnectedComponents) {
-                // Create the stacks needed for turning the recursive formulation of Tarjan's algorithm
-                // into an iterative version. In particular, we keep one stack for states and one stack
-                // for the iterators. The last one is not strictly needed, but reduces iteration work when
-                // all successors of a particular state are considered.
-                std::vector<uint_fast64_t> recursionStateStack;
-                recursionStateStack.reserve(lowlinks.size());
-                std::vector<typename storm::storage::SparseMatrix<T>::ConstIndexIterator> recursionIteratorStack;
-                recursionIteratorStack.reserve(lowlinks.size());
-                std::vector<bool> statesInStack(lowlinks.size());
-                
-                // Initialize the recursion stacks with the given initial state (and its successor iterator).
-                recursionStateStack.push_back(startState);
-                recursionIteratorStack.push_back(matrix.constColumnIteratorBegin(startState));
-                
-            recursionStepForward:
-                while (!recursionStateStack.empty()) {
-                    uint_fast64_t currentState = recursionStateStack.back();
-                    typename storm::storage::SparseMatrix<T>::ConstIndexIterator successorIt = recursionIteratorStack.back();
-                    
-                    // Perform the treatment of newly discovered state as defined by Tarjan's algorithm
-                    visitedStates.set(currentState, true);
-                    stateIndices[currentState] = currentIndex;
-                    lowlinks[currentState] = currentIndex;
-                    ++currentIndex;
-                    tarjanStack.push_back(currentState);
-                    tarjanStackStates.set(currentState, true);
-                    
-                    // Now, traverse all successors of the current state.
-                    for(; successorIt != matrix.constColumnIteratorEnd(currentState); ++successorIt) {
-                        // If we have not visited the successor already, we need to perform the procedure
-                        // recursively on the newly found state.
-                        if (!visitedStates.get(*successorIt)) {
-                            // Save current iterator position so we can continue where we left off later.
-                            recursionIteratorStack.pop_back();
-                            recursionIteratorStack.push_back(successorIt);
-                            
-                            // Put unvisited successor on top of our recursion stack and remember that.
-                            recursionStateStack.push_back(*successorIt);
-                            statesInStack[*successorIt] = true;
-                            
-                            // Also, put initial value for iterator on corresponding recursion stack.
-                            recursionIteratorStack.push_back(matrix.constColumnIteratorBegin(*successorIt));
-                            
-                            // Perform the actual recursion step in an iterative way.
-                            goto recursionStepForward;
-                            
-                        recursionStepBackward:
-                            lowlinks[currentState] = std::min(lowlinks[currentState], lowlinks[*successorIt]);
-                        } else if (tarjanStackStates.get(*successorIt)) {
-                            // Update the lowlink of the current state.
-                            lowlinks[currentState] = std::min(lowlinks[currentState], stateIndices[*successorIt]);
-                        }
-                    }
-                    
-                    // If the current state is the root of a SCC, we need to pop all states of the SCC from
-                    // the algorithm's stack.
-                    if (lowlinks[currentState] == stateIndices[currentState]) {
-                        stronglyConnectedComponents.emplace_back();
-                        
-                        uint_fast64_t lastState = 0;
-                        do {
-                            // Pop topmost state from the algorithm's stack.
-                            lastState = tarjanStack.back();
-                            tarjanStack.pop_back();
-                            tarjanStackStates.set(lastState, false);
-                            
-                            // Add the state to the current SCC.
-                            stronglyConnectedComponents.back().push_back(lastState);
-                        } while (lastState != currentState);
-                    }
-                    
-                    // If we reach this point, we have completed the recursive descent for the current state.
-                    // That is, we need to pop it from the recursion stacks.
-                    recursionStateStack.pop_back();
-                    recursionIteratorStack.pop_back();
-                    
-                    // If there is at least one state under the current one in our recursion stack, we need
-                    // to restore the topmost state as the current state and jump to the part after the
-                    // original recursive call.
-                    if (recursionStateStack.size() > 0) {
-                        currentState = recursionStateStack.back();
-                        successorIt = recursionIteratorStack.back();
-                        
-                        goto recursionStepBackward;
-                    }
-                }
-            }
-            
-            /*!
-             * Performs a decomposition of the given model into its SCCs.
-             *
-             * @param model The nondeterminstic model to decompose.
-             * @return A vector of SCCs of the model.
-             */
-            template <typename T>
-            std::vector<std::vector<uint_fast64_t>> performSccDecomposition(storm::models::AbstractModel<T> const& model) {
-                LOG4CPLUS_INFO(logger, "Computing SCC decomposition.");
-                
-                std::vector<std::vector<uint_fast64_t>> scc;
-                uint_fast64_t numberOfStates = model.getNumberOfStates();
-                
-                // Set up the environment of Tarjan's algorithm.
-                std::vector<uint_fast64_t> tarjanStack;
-                tarjanStack.reserve(numberOfStates);
-                storm::storage::BitVector tarjanStackStates(numberOfStates);
-                std::vector<uint_fast64_t> stateIndices(numberOfStates);
-                std::vector<uint_fast64_t> lowlinks(numberOfStates);
-                storm::storage::BitVector visitedStates(numberOfStates);
-                
-                // 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)) {
-                        performSccDecompositionHelper(state, currentIndex, stateIndices, lowlinks, tarjanStack, tarjanStackStates, visitedStates, model.getTransitionMatrix(), scc);
-                    }
-                }
-                
-                LOG4CPLUS_INFO(logger, "Done computing SCC decomposition.");
-                return scc;
-            }
-            
             /*!
              * Performs a topological sort of the states of the system according to the given transitions.
              *

test/performance/graph/GraphTest.cpp

@@ -3,6 +3,7 @@
 #include "src/settings/Settings.h"
 #include "src/parser/AutoParser.h"
 #include "src/utility/graph.h"
+#include "src/storage/StronglyConnectedComponentDecomposition.h"
 
 TEST(GraphTest, PerformProb01) {
 	storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", "");
@@ -91,7 +92,7 @@ TEST(GraphTest, PerformSCCDecompositionAndGetDependencyGraph) {
 	std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
     
     LOG4CPLUS_WARN(logger, "Computing SCC decomposition of crowds/crowds20_5...");
-    std::vector<std::vector<uint_fast64_t>> sccDecomposition(std::move(storm::utility::graph::performSccDecomposition(*dtmc)));
+    storm::storage::StronglyConnectedComponentDecomposition<double> sccDecomposition(*dtmc);
     LOG4CPLUS_WARN(logger, "Done.");
     
     ASSERT_EQ(sccDecomposition.size(), 1290297ull);
@@ -108,7 +109,7 @@ TEST(GraphTest, PerformSCCDecompositionAndGetDependencyGraph) {
     std::shared_ptr<storm::models::Dtmc<double>> dtmc2 = parser2.getModel<storm::models::Dtmc<double>>();
 
     LOG4CPLUS_WARN(logger, "Computing SCC decomposition of synchronous_leader/leader6_8...");
-    sccDecomposition = std::move(storm::utility::graph::performSccDecomposition(*dtmc2));
+    sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*dtmc2);
     LOG4CPLUS_WARN(logger, "Done.");
 
     ASSERT_EQ(sccDecomposition.size(), 1279673ull);
@@ -125,16 +126,16 @@ TEST(GraphTest, PerformSCCDecompositionAndGetDependencyGraph) {
 	std::shared_ptr<storm::models::Mdp<double>> mdp = parser3.getModel<storm::models::Mdp<double>>();
     
     LOG4CPLUS_WARN(logger, "Computing SCC decomposition of asynchronous_leader/leader6...");
-    sccDecomposition = std::move(storm::utility::graph::performSccDecomposition(*mdp));
+    sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*mdp);
     LOG4CPLUS_WARN(logger, "Done.");
 
-    ASSERT_EQ(sccDecomposition.size(), 214675ull);
+    ASSERT_EQ(sccDecomposition.size(), 146844ull);
     
     LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of asynchronous_leader/leader6...");
     sccDependencyGraph = std::move(mdp->extractPartitionDependencyGraph(sccDecomposition));
     LOG4CPLUS_WARN(logger, "Done.");
     
-    ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 684093ull);
+    ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 489918ull);
     
     mdp = nullptr;
     
@@ -142,16 +143,16 @@ TEST(GraphTest, PerformSCCDecompositionAndGetDependencyGraph) {
 	std::shared_ptr<storm::models::Mdp<double>> mdp2 = parser4.getModel<storm::models::Mdp<double>>();
 
     LOG4CPLUS_WARN(logger, "Computing SCC decomposition of consensus/coin4_6...");
-    sccDecomposition = std::move(storm::utility::graph::performSccDecomposition(*mdp2));
+    sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*mdp2);
     LOG4CPLUS_WARN(logger, "Done.");
 
-    ASSERT_EQ(sccDecomposition.size(), 63611ull);
+    ASSERT_EQ(sccDecomposition.size(), 2611ull);
     
     LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of consensus/coin4_6...");
     sccDependencyGraph = std::move(mdp2->extractPartitionDependencyGraph(sccDecomposition));
     LOG4CPLUS_WARN(logger, "Done.");
     
-    ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 213400ull);
+    ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 7888ull);
 
     mdp2 = nullptr;
 }