Further steps towards implementation of MEC decomposition.

Former-commit-id: 8166b3b923

src/models/AbstractModel.h

@@ -148,7 +148,7 @@ 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(storm::storage::Decomposition const& decomposition) const {
+        storm::storage::SparseMatrix<bool> extractPartitionDependencyGraph(storm::storage::Decomposition<storm::storage::StateBlock> 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.
@@ -165,7 +165,7 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
             
             for (uint_fast64_t currentBlockIndex = 0; currentBlockIndex < decomposition.size(); ++currentBlockIndex) {
                 // Get the next block.
-                typename storm::storage::Decomposition::Block const& block = decomposition[currentBlockIndex];
+                typename storm::storage::StateBlock const& block = decomposition[currentBlockIndex];
                 
                 // Now, we determine the blocks which are reachable (in one step) from the current block.
                 storm::storage::VectorSet<uint_fast64_t> allTargetBlocks;

src/storage/BitVector.h

@@ -6,6 +6,8 @@
 #include <cmath>
 #include <cstdint>
 
+#include "src/storage/VectorSet.h"
+
 #include "src/exceptions/InvalidStateException.h"
 #include "src/exceptions/InvalidArgumentException.h"
 #include "src/exceptions/OutOfRangeException.h"
@@ -139,6 +141,19 @@ public:
 		}
 	}
     
+    /*!
+     * Creates a bit vector that has exactly those bits set that are defined by the given set.
+     *
+     * @param length The length of the bit vector to create.
+     * @param bitsToSet A set of indices whose bits to set in the bit vector.
+	 * @param initTrue The initial value of the first |length| bits.
+     */
+    BitVector(uint_fast64_t length, storm::storage::VectorSet<uint_fast64_t> const& bitsToSet, bool initTrue = false) : BitVector(length, initTrue) {
+        for (auto bit : bitsToSet) {
+            this->set(bit, true);
+        }
+    }
+
 	/*!
 	 * Copy Constructor. Performs a deep copy of the given bit vector.
 	 * @param bv A reference to the bit vector to be copied.

src/storage/Decomposition.cpp

@@ -1,57 +1,85 @@
 #include "src/storage/Decomposition.h"
+#include "src/storage/MaximalEndComponent.h"
 
 namespace storm {
     namespace storage {
         
-        Decomposition::Decomposition() : blocks() {
+        template <typename BlockType>
+        Decomposition<BlockType>::Decomposition() : blocks() {
             // Intentionally left empty.
         }
         
-        Decomposition::Decomposition(Decomposition const& other) : blocks(other.blocks) {
+        template <typename BlockType>
+        Decomposition<BlockType>::Decomposition(Decomposition const& other) : blocks(other.blocks) {
             // Intentionally left empty.
         }
         
-        Decomposition& Decomposition::operator=(Decomposition const& other) {
+        template <typename BlockType>
+        Decomposition<BlockType>& Decomposition<BlockType>::operator=(Decomposition const& other) {
             this->blocks = other.blocks;
             return *this;
         }
         
-        Decomposition::Decomposition(Decomposition&& other) : blocks(std::move(other.blocks)) {
+        template <typename BlockType>
+        Decomposition<BlockType>::Decomposition(Decomposition&& other) : blocks(std::move(other.blocks)) {
             // Intentionally left empty.
         }
         
-        Decomposition& Decomposition::operator=(Decomposition&& other) {
+        template <typename BlockType>
+        Decomposition<BlockType>& Decomposition<BlockType>::operator=(Decomposition&& other) {
             this->blocks = std::move(other.blocks);
             return *this;
         }
         
-        size_t Decomposition::size() const {
+        template <typename BlockType>
+        size_t Decomposition<BlockType>::size() const {
             return blocks.size();
         }
         
-        Decomposition::iterator Decomposition::begin() {
+        template <typename BlockType>
+        typename Decomposition<BlockType>::iterator Decomposition<BlockType>::begin() {
             return blocks.begin();
         }
         
-        Decomposition::iterator Decomposition::end() {
+        template <typename BlockType>
+        typename Decomposition<BlockType>::iterator Decomposition<BlockType>::end() {
             return blocks.end();
         }
         
-        Decomposition::const_iterator Decomposition::begin() const {
+        template <typename BlockType>
+        typename Decomposition<BlockType>::const_iterator Decomposition<BlockType>::begin() const {
             return blocks.begin();
         }
         
-        Decomposition::const_iterator Decomposition::end() const {
+        template <typename BlockType>
+        typename Decomposition<BlockType>::const_iterator Decomposition<BlockType>::end() const {
             return blocks.end();
         }
         
-        Decomposition::Block const& Decomposition::getBlock(uint_fast64_t index) const {
+        template <typename BlockType>
+        BlockType const& Decomposition<BlockType>::getBlock(uint_fast64_t index) const {
             return blocks.at(index);
         }
         
-        Decomposition::Block const& Decomposition::operator[](uint_fast64_t index) const {
+        template <typename BlockType>
+        BlockType const& Decomposition<BlockType>::operator[](uint_fast64_t index) const {
             return blocks[index];
         }
         
+        template <typename BlockType>
+        std::ostream& operator<<(std::ostream& out, Decomposition<BlockType> const& decomposition) {
+            out << "{";
+            if (decomposition.size() > 0) {
+                for (uint_fast64_t blockIndex = 0; blockIndex < decomposition.size() - 1; ++blockIndex) {
+                    out << decomposition.blocks[blockIndex] << ", ";
+                }
+                out << decomposition.blocks[decomposition.size() - 1];
+            }
+            out << "}";
+            return out;
+        }
+        
+        template class Decomposition<StateBlock>;
+        template class Decomposition<MaximalEndComponent>;
     } // namespace storage
 } // namespace storm

src/storage/Decomposition.h

@@ -7,15 +7,17 @@
 
 namespace storm {
     namespace storage {
+        typedef storm::storage::VectorSet<uint_fast64_t> StateBlock;
         
         /*!
-         * This class represents the decomposition of a model into state sets.
+         * This class represents the decomposition of a model into blocks which are of the template type.
          */
+        template <typename BlockType>
         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;
+            typedef BlockType Block;
+            typedef typename std::vector<Block>::iterator iterator;
+            typedef typename std::vector<Block>::const_iterator const_iterator;
             
             /*
              * Creates an empty SCC decomposition.
@@ -44,6 +46,8 @@ namespace storm {
             
             Block const& operator[](uint_fast64_t index) const;
             
+            friend std::ostream& operator<<(std::ostream& out, Decomposition const& decomposition);
+
         protected:
             // The blocks of the decomposition.
             std::vector<Block> blocks;

src/storage/MaximalEndComponent.cpp

@@ -0,0 +1,52 @@
+#include "src/storage/MaximalEndComponent.h"
+#include "src/exceptions/InvalidStateException.h"
+
+namespace storm {
+    namespace storage {
+        
+        MaximalEndComponent::MaximalEndComponent() : stateToChoicesMapping() {
+            // Intentionally left empty.
+        }
+        
+        MaximalEndComponent::MaximalEndComponent(MaximalEndComponent const& other) : stateToChoicesMapping(other.stateToChoicesMapping) {
+            // Intentionally left empty.
+        }
+        
+        MaximalEndComponent& MaximalEndComponent::operator=(MaximalEndComponent const& other) {
+            stateToChoicesMapping = other.stateToChoicesMapping;
+            return *this;
+        }
+        
+        MaximalEndComponent::MaximalEndComponent(MaximalEndComponent&& other) : stateToChoicesMapping(std::move(other.stateToChoicesMapping)) {
+            // Intentionally left empty.
+        }
+        
+        MaximalEndComponent& MaximalEndComponent::operator=(MaximalEndComponent&& other) {
+            stateToChoicesMapping = std::move(other.stateToChoicesMapping);
+            return *this;
+        }
+        
+        void MaximalEndComponent::addState(uint_fast64_t state, std::vector<uint_fast64_t> const& choices) {
+            stateToChoicesMapping[state] = choices;
+        }
+        
+        std::vector<uint_fast64_t> const& MaximalEndComponent::getChoicesForState(uint_fast64_t state) const {
+            auto stateChoicePair = stateToChoicesMapping.find(state);
+            
+            if (stateChoicePair == stateToChoicesMapping.end()) {
+                throw storm::exceptions::InvalidStateException() << "Cannot retrieve choices for state not contained in MEC.";
+            }
+            
+            return stateChoicePair->second;
+        }
+        
+        bool MaximalEndComponent::containsState(uint_fast64_t state) const {
+            auto stateChoicePair = stateToChoicesMapping.find(state);
+            
+            if (stateChoicePair == stateToChoicesMapping.end()) {
+                return false;
+            }
+            return true;
+        }
+    }
+}

src/storage/MaximalEndComponent.h

@@ -0,0 +1,59 @@
+#ifndef STORM_STORAGE_MAXIMALENDCOMPONENT_H_
+#define STORM_STORAGE_MAXIMALENDCOMPONENT_H_
+
+#include <unordered_map>
+#include <vector>
+
+namespace storm {
+    namespace storage {
+        /*!
+         * This class represents a maximal end-component of a nondeterministic model.
+         */
+        class MaximalEndComponent {
+        public:
+            /*!
+             * Creates an empty MEC.
+             */
+            MaximalEndComponent();
+            
+            MaximalEndComponent(MaximalEndComponent const& other);
+            
+            MaximalEndComponent& operator=(MaximalEndComponent const& other);
+            
+            MaximalEndComponent(MaximalEndComponent&& other);
+            
+            MaximalEndComponent& operator=(MaximalEndComponent&& other);
+            
+            /*!
+             * Adds the given state and the given choices to the MEC.
+             *
+             * @param state The state for which to add the choices.
+             * @param choices The choices to add for the state.
+             */
+            void addState(uint_fast64_t state, std::vector<uint_fast64_t> const& choices);
+            
+            /*!
+             * Retrieves the choices for the given state that are contained in this MEC under the
+             * assumption that the state is in the MEC.
+             *
+             * @param state The state for which to retrieve the choices.
+             * @return A list of choices of the state in the MEC.
+             */
+            std::vector<uint_fast64_t> const& getChoicesForState(uint_fast64_t state) const;
+            
+            /*!
+             * Retrieves whether the given state is contained in this MEC.
+             *
+             * @param state The state for which to query membership in the MEC.
+             * @return True if the given state is contained in the MEC.
+             */
+            bool containsState(uint_fast64_t state) const;
+            
+        private:
+            // This stores the mapping from states contained in the MEC to the choices in this MEC.
+            std::unordered_map<uint_fast64_t, std::vector<uint_fast64_t>> stateToChoicesMapping;
+        };
+    }
+}
+
+#endif /* STORM_STORAGE_MAXIMALENDCOMPONENT_H_ */

src/storage/MaximalEndComponentDecomposition.cpp

@@ -0,0 +1,45 @@
+#include "src/storage/MaximalEndComponentDecomposition.h"
+
+namespace storm {
+    namespace storage {
+        
+        template<typename ValueType>
+        MaximalEndComponentDecomposition<ValueType>::MaximalEndComponentDecomposition() : Decomposition() {
+            // Intentionally left empty.
+        }
+        
+        template<typename ValueType>
+        MaximalEndComponentDecomposition<ValueType>::MaximalEndComponentDecomposition(storm::models::AbstractNondeterministicModel<ValueType> const& model) {
+            performMaximalEndComponentDecomposition(model);
+        }
+        
+        template<typename ValueType>
+        MaximalEndComponentDecomposition<ValueType>::MaximalEndComponentDecomposition(MaximalEndComponentDecomposition const& other) : Decomposition(other) {
+            // Intentionally left empty.
+        }
+        
+        template<typename ValueType>
+        MaximalEndComponentDecomposition<ValueType>& MaximalEndComponentDecomposition<ValueType>::operator=(MaximalEndComponentDecomposition const& other) {
+            Decomposition::operator=(other);
+            return *this;
+        }
+        
+        template<typename ValueType>
+        MaximalEndComponentDecomposition<ValueType>::MaximalEndComponentDecomposition(MaximalEndComponentDecomposition&& other) : Decomposition(std::move(other)) {
+            // Intentionally left empty.
+        }
+        
+        template<typename ValueType>
+        MaximalEndComponentDecomposition<ValueType>& MaximalEndComponentDecomposition<ValueType>::operator=(MaximalEndComponentDecomposition&& other) {
+            Decomposition::operator=(std::move(other));
+            return *this;
+        }
+        
+        template <typename ValueType>
+        void MaximalEndComponentDecomposition<ValueType>::performMaximalEndComponentDecomposition(storm::models::AbstractNondeterministicModel<ValueType> const& model) {
+            // TODO.
+        }
+        
+        template class MaximalEndComponentDecomposition<double>;
+    }
+}

src/storage/MaximalEndComponentDecomposition.h

@@ -0,0 +1,47 @@
+#ifndef STORM_STORAGE_MAXIMALENDCOMPONENTDECOMPOSITION_H_
+#define STORM_STORAGE_MAXIMALENDCOMPONENTDECOMPOSITION_H_
+
+#include "src/storage/Decomposition.h"
+#include "src/storage/StronglyConnectedComponentDecomposition.h"
+#include "src/storage/MaximalEndComponent.h"
+#include "src/models/AbstractNondeterministicModel.h"
+
+namespace storm  {
+    namespace storage {
+        
+        template <typename ValueType>
+        class MaximalEndComponentDecomposition : public Decomposition<MaximalEndComponent> {
+        public:
+            /*
+             * Creates an empty MEC decomposition.
+             */
+            MaximalEndComponentDecomposition();
+            
+            /*
+             * Creates an MEC decomposition of the given model.
+             *
+             * @param model The model to decompose into MECs.
+             */
+            MaximalEndComponentDecomposition(storm::models::AbstractNondeterministicModel<ValueType> const& model);
+            
+            MaximalEndComponentDecomposition(MaximalEndComponentDecomposition const& other);
+            
+            MaximalEndComponentDecomposition& operator=(MaximalEndComponentDecomposition const& other);
+            
+            MaximalEndComponentDecomposition(MaximalEndComponentDecomposition&& other);
+            
+            MaximalEndComponentDecomposition& operator=(MaximalEndComponentDecomposition&& other);
+            
+        private:
+            /*!
+             * Performs the actual decomposition of the given model into MECs. Stores the MECs found in the current decomposition
+             * as a side-effect.
+             *
+             * @param model The model to decompose.
+             */
+            void performMaximalEndComponentDecomposition(storm::models::AbstractNondeterministicModel<ValueType> const& model);
+        };
+    }
+}
+
+#endif /* STORM_STORAGE_MAXIMALENDCOMPONENTDECOMPOSITION_H_ */

src/storage/StronglyConnectedComponentDecomposition.cpp

@@ -3,40 +3,46 @@
 
 namespace storm {
     namespace storage {
-        template<typename T>
-        StronglyConnectedComponentDecomposition<T>::StronglyConnectedComponentDecomposition() : Decomposition() {
+        template<typename ValueType>
+        StronglyConnectedComponentDecomposition<ValueType>::StronglyConnectedComponentDecomposition() : Decomposition() {
             // Intentionally left empty.
         }
 
-        template <typename T>
-        StronglyConnectedComponentDecomposition<T>::StronglyConnectedComponentDecomposition(storm::models::AbstractModel<T> const& model) : Decomposition() {
-            performSccDecomposition(model);
+        template <typename ValueType>
+        StronglyConnectedComponentDecomposition<ValueType>::StronglyConnectedComponentDecomposition(storm::models::AbstractModel<ValueType> const& model, bool dropNaiveSccs) : Decomposition() {
+            performSccDecomposition(model, dropNaiveSccs);
         }
         
-        template <typename T>
-        StronglyConnectedComponentDecomposition<T>::StronglyConnectedComponentDecomposition(StronglyConnectedComponentDecomposition const& other) : Decomposition(other) {
+        template <typename ValueType>
+        StronglyConnectedComponentDecomposition<ValueType>::StronglyConnectedComponentDecomposition(storm::models::AbstractModel<ValueType> const& model, StateBlock const& block, bool dropNaiveSccs) {
+            storm::storage::BitVector subsystem(model.getNumberOfStates(), block);
+            performSccDecomposition(model, subsystem, dropNaiveSccs);
+        }
+        
+        template <typename ValueType>
+        StronglyConnectedComponentDecomposition<ValueType>::StronglyConnectedComponentDecomposition(StronglyConnectedComponentDecomposition const& other) : Decomposition(other) {
             // Intentionally left empty.
         }
         
-        template <typename T>
-        StronglyConnectedComponentDecomposition<T>& StronglyConnectedComponentDecomposition<T>::operator=(StronglyConnectedComponentDecomposition const& other) {
+        template <typename ValueType>
+        StronglyConnectedComponentDecomposition<ValueType>& StronglyConnectedComponentDecomposition<ValueType>::operator=(StronglyConnectedComponentDecomposition const& other) {
             this->blocks = other.blocks;
             return *this;
         }
         
-        template <typename T>
-        StronglyConnectedComponentDecomposition<T>::StronglyConnectedComponentDecomposition(StronglyConnectedComponentDecomposition&& other) : Decomposition(std::move(other)) {
+        template <typename ValueType>
+        StronglyConnectedComponentDecomposition<ValueType>::StronglyConnectedComponentDecomposition(StronglyConnectedComponentDecomposition&& other) : Decomposition(std::move(other)) {
             // Intentionally left empty.
         }
         
-        template <typename T>
-        StronglyConnectedComponentDecomposition<T>& StronglyConnectedComponentDecomposition<T>::operator=(StronglyConnectedComponentDecomposition&& other) {
+        template <typename ValueType>
+        StronglyConnectedComponentDecomposition<ValueType>& StronglyConnectedComponentDecomposition<ValueType>::operator=(StronglyConnectedComponentDecomposition&& other) {
             this->blocks = std::move(other.blocks);
             return *this;
         }
         
-        template <typename T>
-        void StronglyConnectedComponentDecomposition<T>::performSccDecomposition(storm::models::AbstractModel<T> const& model) {
+        template <typename ValueType>
+        void StronglyConnectedComponentDecomposition<ValueType>::performSccDecomposition(storm::models::AbstractModel<ValueType> const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs) {
             LOG4CPLUS_INFO(logger, "Computing SCC decomposition.");
             
             uint_fast64_t numberOfStates = model.getNumberOfStates();
@@ -49,26 +55,38 @@ namespace storm {
             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.
+            // Start the search for SCCs from every vertex in the block.
             uint_fast64_t currentIndex = 0;
-            for (uint_fast64_t state = 0; state < numberOfStates; ++state) {
+            for (auto state : subsystem) {
                 if (!visitedStates.get(state)) {
-                    performSccDecompositionHelper(model, state, currentIndex, stateIndices, lowlinks, tarjanStack, tarjanStackStates, visitedStates);
+                    performSccDecompositionHelper(model, state, subsystem, currentIndex, stateIndices, lowlinks, tarjanStack, tarjanStackStates, visitedStates, dropNaiveSccs);
                 }
             }
             
             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) {
+        
+        template <typename ValueType>
+        void StronglyConnectedComponentDecomposition<ValueType>::performSccDecomposition(storm::models::AbstractModel<ValueType> const& model, bool dropNaiveSccs) {
+            uint_fast64_t numberOfStates = model.getNumberOfStates();
+
+            // Prepare a block that contains all states for a call to the other overload of this function.
+            storm::storage::BitVector fullSystem(numberOfStates, true);
+            
+            // Call the overloaded function.
+            performSccDecomposition(model, fullSystem, dropNaiveSccs);
+        }
+        
+        template <typename ValueType>
+        void StronglyConnectedComponentDecomposition<ValueType>::performSccDecompositionHelper(storm::models::AbstractModel<ValueType> const& model, uint_fast64_t startState, storm::storage::BitVector const& subsystem, 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, bool dropNaiveSccs) {
             // 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;
+            std::vector<typename storm::storage::SparseMatrix<ValueType>::ConstIterator> recursionIteratorStack;
             recursionIteratorStack.reserve(lowlinks.size());
             std::vector<bool> statesInStack(lowlinks.size());
             
@@ -79,9 +97,9 @@ namespace storm {
         recursionStepForward:
             while (!recursionStateStack.empty()) {
                 uint_fast64_t currentState = recursionStateStack.back();
-                typename storm::storage::SparseMatrix<T>::ConstIterator successorIt = recursionIteratorStack.back();
+                typename storm::storage::SparseMatrix<ValueType>::ConstIterator successorIt = recursionIteratorStack.back();
                 
-                // Perform the treatment of newly discovered state as defined by Tarjan's algorithm
+                // Perform the treatment of newly discovered state as defined by Tarjan's algorithm.
                 visitedStates.set(currentState, true);
                 stateIndices[currentState] = currentIndex;
                 lowlinks[currentState] = currentIndex;
@@ -93,7 +111,7 @@ namespace storm {
                 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())) {
+                    if (!visitedStates.get(successorIt.column()) && subsystem.get(successorIt.column())) {
                         // Save current iterator position so we can continue where we left off later.
                         recursionIteratorStack.pop_back();
                         recursionIteratorStack.push_back(successorIt);
@@ -131,8 +149,12 @@ namespace storm {
                         // Add the state to the current SCC.
                         scc.insert(lastState);
                     } while (lastState != currentState);
+                    
+                    // Only add the SCC if it is non-trivial if the corresponding flag was set.
+                    if (scc.size() > 1 || !dropNaiveSccs) {
                         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.

src/storage/StronglyConnectedComponentDecomposition.h

@@ -9,7 +9,7 @@
 namespace storm {
     namespace models {
         // Forward declare the abstract model class.
-        template <typename T> class AbstractModel;
+        template <typename ValueType> class AbstractModel;
     }
     
     namespace storage {
@@ -17,8 +17,8 @@ namespace storm {
         /*!
          * This class represents the decomposition of a graph-like structure into its strongly connected components.
          */
-        template <typename T>
-        class StronglyConnectedComponentDecomposition : public Decomposition {
+        template <typename ValueType>
+        class StronglyConnectedComponentDecomposition : public Decomposition<StateBlock> {
         public:
             /*
              * Creates an empty SCC decomposition.
@@ -27,8 +27,22 @@ namespace storm {
             
             /*
              * Creates an SCC decomposition of the given model.
+             *
+             * @param model The model to decompose into SCCs.
+             * @param dropNaiveSccs A flag that indicates whether trivial SCCs (i.e. SCCs consisting of just one state
+             * are to be kept in the decomposition.
              */
-            StronglyConnectedComponentDecomposition(storm::models::AbstractModel<T> const& model);
+            StronglyConnectedComponentDecomposition(storm::models::AbstractModel<ValueType> const& model, bool dropNaiveSccs = false);
+
+            /*
+             * Creates an SCC decomposition of given block in the given model.
+             *
+             * @param model The model that contains the block.
+             * @param block The block to decompose into SCCs.
+             * @param dropNaiveSccs A flag that indicates whether trivial SCCs (i.e. SCCs consisting of just one state
+             * are to be kept in the decomposition.
+             */
+            StronglyConnectedComponentDecomposition(storm::models::AbstractModel<ValueType> const& model, StateBlock const& block, bool dropNaiveSccs = false);
             
             StronglyConnectedComponentDecomposition(StronglyConnectedComponentDecomposition const& other);
             
@@ -39,9 +53,11 @@ namespace storm {
             StronglyConnectedComponentDecomposition& operator=(StronglyConnectedComponentDecomposition&& other);
             
         private:
-            void performSccDecomposition(storm::models::AbstractModel<T> const& model);
+            void performSccDecomposition(storm::models::AbstractModel<ValueType> const& model, bool dropNaiveSccs);
+            
+            void performSccDecomposition(storm::models::AbstractModel<ValueType> const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs);
             
-            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);
+            void performSccDecompositionHelper(storm::models::AbstractModel<ValueType> const& model, uint_fast64_t startState, storm::storage::BitVector const& subsystem, 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, bool dropNaiveSccs);
         };
     }
 }

src/storage/VectorSet.h

@@ -14,6 +14,8 @@
 #include <vector>
 #include <set>
 
+#include "src/exceptions/InvalidStateException.h"
+
 namespace storm  {
     namespace storage {
         
@@ -149,6 +151,24 @@ namespace storm  {
                 return data.end();
             }
             
+            T const& min() const {
+                if (this->size() == 0) {
+                    throw storm::exceptions::InvalidStateException() << "Cannot retrieve minimum of empty set.";
+                }
+                
+                ensureSet();
+                return data.first;
+            }
+            
+            T const& max() const {
+                if (this->size() == 0) {
+                    throw storm::exceptions::InvalidStateException() << "Cannot retrieve minimum of empty set.";
+                }
+                
+                ensureSet();
+                return data.back;
+            }
+            
             void insert(T const& element) {
                 data.push_back(element);
                 dirty = true;

src/storm.cpp

@@ -24,6 +24,7 @@
 #include "src/models/Dtmc.h"
 #include "src/models/MarkovAutomaton.h"
 #include "src/storage/SparseMatrix.h"
+#include "src/storage/MaximalEndComponentDecomposition.h"
 #include "src/models/AtomicPropositionsLabeling.h"
 #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
 #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"