Tried to pave the way for generic blocks for decompositions, but I don't know whether this is the way to go.

Former-commit-id: 4a7b51f33c

src/modelchecker/reachability/SparseSccModelChecker.cpp

@@ -73,7 +73,7 @@ namespace storm {
             
             template<typename ValueType>
             void SparseSccModelChecker<ValueType>::treatScc(storm::models::Dtmc<ValueType> const& dtmc, FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix<ValueType> const& forwardTransitions, FlexibleSparseMatrix<ValueType>& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level) {
-                // If the SCCs are still quite large, we try to split them further.
+                // If the SCCs are large enough, we try to split them further.
                 if (scc.getNumberOfSetBits() > SparseSccModelChecker<ValueType>::maximalSccSize) {
                     // Here, we further decompose the SCC into sub-SCCs.
                     storm::storage::StronglyConnectedComponentDecomposition<ValueType> decomposition(forwardTransitions, scc & ~entryStates, true, false);

src/storage/Block.cpp

@@ -0,0 +1,49 @@
+#include "src/storage/Block.h"
+
+namespace storm {
+    namespace storage {
+        Block::iterator Block::begin() {
+            return states.begin();
+        }
+        
+        Block::const_iterator Block::begin() const {
+            return states.begin();
+        }
+        
+        StronglyConnectedComponent::iterator Block::end() {
+            return states.end();
+        }
+        
+        StronglyConnectedComponent::const_iterator Block::end() const {
+            return states.end();
+        }
+        
+        std::size_t Block::size() const {
+            return states.size();
+        }
+        
+        void Block::insert(value_type const& state) {
+            states.insert(state);
+        }
+        
+        void Block::erase(value_type const& state) {
+            states.erase(state);
+        }
+        
+        bool Block::containsState(value_type const& state) const {
+            return this->states.find(state) != this->states.end();
+        }
+        
+        std::ostream& operator<<(std::ostream& out, StateBlock const& block) {
+            out << "{";
+            for (auto const& element : block) {
+                out << element << ", ";
+            }
+            out << "}";
+            return out;
+        }
+        
+        // Explicitly instantiate template.
+        template Block<>;
+    }
+}

src/storage/Block.h

@@ -0,0 +1,93 @@
+#ifndef STORM_STORAGE_BLOCK_H_
+#define STORM_STORAGE_BLOCK_H_
+
+#include <boost/container/flat_set.hpp>
+
+namespace storm {
+    namespace storage {
+        
+        typedef boost::container::flat_set<uint_fast64_t> FlatSetStateContainer;
+        
+        /*!
+         * Writes a string representation of the state block to the given output stream.
+         *
+         * @param out The output stream to write to.
+         * @param block The block to print to the stream.
+         * @return The given output stream.
+         */
+        std::ostream& operator<<(std::ostream& out, FlatSetStateContainer const& block);
+        
+        class Block {
+        public:
+            typedef ContainerType container_type;
+            typedef typename container_type::value_type value_type;
+            typedef typename container_type::iterator iterator;
+            typedef typename container_type::const_iterator const_iterator;
+            
+            /*!
+             * Returns an iterator to the states in this SCC.
+             *
+             * @return An iterator to the states in this SCC.
+             */
+            iterator begin();
+            
+            /*!
+             * Returns a const iterator to the states in this SCC.
+             *
+             * @return A const iterator to the states in this SCC.
+             */
+            const_iterator begin() const;
+            
+            /*!
+             * Returns an iterator that points one past the end of the states in this SCC.
+             *
+             * @return An iterator that points one past the end of the states in this SCC.
+             */
+            iterator end();
+            
+            /*!
+             * Returns a const iterator that points one past the end of the states in this SCC.
+             *
+             * @return A const iterator that points one past the end of the states in this SCC.
+             */
+            const_iterator end() const;
+            
+            /*!
+             * Retrieves whether the given state is in the SCC.
+             *
+             * @param state The state for which to query membership.
+             */
+            bool containsState(value_type const& state) const;
+            
+            /*!
+             * Inserts the given element into this SCC.
+             *
+             * @param state The state to add to this SCC.
+             */
+            void insert(value_type const& state);
+            
+            /*!
+             * Removes the given element from this SCC.
+             *
+             * @param state The element to remove.
+             */
+            void erase(value_type const& state);
+            
+            /*!
+             * Retrieves the number of states in this SCC.
+             *
+             * @return The number of states in this SCC.
+             */
+            std::size_t size() const;
+            
+            /*!
+             * Retrieves whether this SCC is empty.
+             *
+             * @return True iff the SCC is empty.
+             */
+            bool empty() const;
+        };
+    }
+}
+
+#endif /* STORM_STORAGE_BLOCK_H_ */

src/storage/Decomposition.cpp

@@ -76,15 +76,6 @@ namespace storm {
             return blocks[index];
         }
         
-        std::ostream& operator<<(std::ostream& out, StateBlock const& block) {
-            out << "{";
-            for (auto const& element : block) {
-                out << element << ", ";
-            }
-            out << "}";
-            return out;
-        }
-        
         template <typename BlockType>
         std::ostream& operator<<(std::ostream& out, Decomposition<BlockType> const& decomposition) {
             out << "[";

src/storage/Decomposition.h

@@ -2,21 +2,9 @@
 #define STORM_STORAGE_DECOMPOSITION_H_
 
 #include <vector>
-#include <boost/container/flat_set.hpp>
 
 namespace storm {
     namespace storage {
-        // A typedef that specifies the type of a block consisting of states only.
-        typedef boost::container::flat_set<uint_fast64_t> StateBlock;
-        
-        /*!
-         * Writes a string representation of the state block to the given output stream.
-         *
-         * @param out The output stream to write to.
-         * @param block The block to print to the stream.
-         * @return The given output stream.
-         */
-        std::ostream& operator<<(std::ostream& out, StateBlock const& block);
         
         /*!
          * This class represents the decomposition of a model into blocks which are of the template type.
@@ -24,9 +12,9 @@ namespace storm {
         template <typename BlockType>
         class Decomposition {
         public:
-            typedef BlockType Block;
-            typedef typename std::vector<Block>::iterator iterator;
-            typedef typename std::vector<Block>::const_iterator const_iterator;
+            typedef BlockType block_type;
+            typedef typename std::vector<block_type>::iterator iterator;
+            typedef typename std::vector<block_type>::const_iterator const_iterator;
             
             /*!
              * Creates an empty decomposition.
@@ -104,7 +92,7 @@ namespace storm {
              * @param index The index of the block to retrieve.
              * @return The block with the given index.
              */
-            Block const& getBlock(uint_fast64_t index) const;
+            block_type const& getBlock(uint_fast64_t index) const;
             
             /*!
              * Retrieves the block with the given index. If the index is out-of-bounds, an exception is thrown.
@@ -112,7 +100,7 @@ namespace storm {
              * @param index The index of the block to retrieve.
              * @return The block with the given index.
              */
-            Block& getBlock(uint_fast64_t index);
+            block_type& getBlock(uint_fast64_t index);
             
             /*!
              * Retrieves the block with the given index. If the index is out-of-bounds, an behaviour is undefined.
@@ -120,7 +108,7 @@ namespace storm {
              * @param index The index of the block to retrieve.
              * @return The block with the given index.
              */
-            Block const& operator[](uint_fast64_t index) const;
+            block_type const& operator[](uint_fast64_t index) const;
             
             /*!
              * Retrieves the block with the given index. If the index is out-of-bounds, an behaviour is undefined.
@@ -128,7 +116,7 @@ namespace storm {
              * @param index The index of the block to retrieve.
              * @return The block with the given index.
              */
-            Block& operator[](uint_fast64_t index);
+            block_type& operator[](uint_fast64_t index);
             
             // Declare the streaming operator as a friend function to enable output of decompositions.
             template<typename BlockTimePrime>
@@ -136,7 +124,7 @@ namespace storm {
             
         protected:
             // The blocks of the decomposition.
-            std::vector<Block> blocks;
+            std::vector<block_type> blocks;
         };
     }
 }

src/storage/MaximalEndComponentDecomposition.cpp

@@ -88,7 +88,7 @@ namespace storm {
                             for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) {
                                 bool choiceContainedInMEC = true;
                                 for (auto const& entry : transitionMatrix.getRow(choice)) {
-                                    if (scc.find(entry.getColumn()) == scc.end()) {
+                                    if (!scc.containsState(entry.getColumn())) {
                                         choiceContainedInMEC = false;
                                         break;
                                     }
@@ -116,7 +116,7 @@ namespace storm {
                         statesToCheck.clear();
                         for (auto state : statesToRemove) {
                             for (auto const& entry : backwardTransitions.getRow(state)) {
-                                if (scc.find(entry.getColumn()) != scc.end()) {
+                                if (!scc.containsState(entry.getColumn())) {
                                     statesToCheck.set(entry.getColumn());
                                 }
                             }
@@ -127,7 +127,7 @@ namespace storm {
                 // If the MEC changed, we delete it from the list of MECs and append the possible new MEC candidates to
                 // the list instead.
                 if (mecChanged) {
-                    for (StateBlock& scc : sccs) {
+                    for (StronglyConnectedComponent& scc : sccs) {
                         if (!scc.empty()) {
                             endComponentStateSets.push_back(std::move(scc));
                         }

src/storage/StronglyConnectedComponent.cpp

@@ -0,0 +1,13 @@
+#include "src/storage/StronglyConnectedComponent.h"
+
+namespace storm {
+    namespace storage {
+        void StronglyConnectedComponent::setIsTrivial(bool trivial) {
+            this->isTrivialScc = trivial;
+        }
+        
+        bool StronglyConnectedComponent::isTrivial() const {
+            return isTrivialScc;
+        }
+    }
+}

src/storage/StronglyConnectedComponent.h

@@ -0,0 +1,53 @@
+#ifndef STORM_STORAGE_STRONGLYCONNECTEDCOMPONENT_H_
+#define STORM_STORAGE_STRONGLYCONNECTEDCOMPONENT_H_
+
+#include "src/storage/Block.h"
+#include "src/storage/Decomposition.h"
+
+namespace storm {
+    namespace storage {
+        
+        typedef FlatSetStateContainer SccBlock;
+        
+        /*!
+         * This class represents a strongly connected component, i.e., a set of states such that every state can reach
+         * every other state.
+         */
+        class StronglyConnectedComponent : public Block<SccBlock> {
+        public:
+            typedef SccBlock block_type;
+            typedef block_type::value_type value_type;
+            typedef block_type::iterator iterator;
+            typedef block_type::const_iterator const_iterator;
+            
+            /*!
+             * Creates an empty strongly connected component.
+             */
+            StronglyConnectedComponent();
+            
+            /*!
+             * Sets whether this SCC is trivial or not.
+             *
+             * @param trivial A flag indicating whether this SCC is trivial or not.
+             */
+            void setIsTrivial(bool trivial);
+            
+            /*!
+             * Retrieves whether this SCC is trivial.
+             *
+             * @return True iff this SCC is trivial.
+             */
+            bool isTrivial() const;
+            
+        private:
+            // Stores whether this SCC is trivial.
+            bool isTrivialScc;
+            
+            // The states in this SCC.
+            block_type states;
+        };
+        
+    }
+}
+
+#endif /* STORM_STORAGE_STRONGLYCONNECTEDCOMPONENT_H_ */

src/storage/StronglyConnectedComponentDecomposition.cpp

@@ -119,7 +119,7 @@ namespace storm {
                 }
                 
                 // Create the new set of blocks by moving all the blocks we need to keep into it.
-                std::vector<Block> newBlocks((~blocksToDrop).getNumberOfSetBits());
+                std::vector<block_type> newBlocks((~blocksToDrop).getNumberOfSetBits());
                 uint_fast64_t currentBlock = 0;
                 for (uint_fast64_t blockIndex = 0; blockIndex < this->blocks.size(); ++blockIndex) {
                     if (!blocksToDrop.get(blockIndex)) {

src/storage/StronglyConnectedComponentDecomposition.h

@@ -3,6 +3,7 @@
 
 #include "src/storage/SparseMatrix.h"
 #include "src/storage/Decomposition.h"
+#include "src/storage/StronglyConnectedComponent.h"
 #include "src/storage/BitVector.h"
 
 namespace storm {
@@ -17,8 +18,8 @@ namespace storm {
          * This class represents the decomposition of a graph-like structure into its strongly connected components.
          */
         template <typename ValueType>
-        class StronglyConnectedComponentDecomposition : public Decomposition<StateBlock> {
-        public:
+        class StronglyConnectedComponentDecomposition : public Decomposition<StronglyConnectedComponent> {
+        public:            
             /*
              * Creates an empty SCC decomposition.
              */
@@ -45,7 +46,7 @@ namespace storm {
              * @param onlyBottomSccs If set to true, only bottom SCCs, i.e. SCCs in which all states have no way of
              * leaving the SCC), are kept.
              */
-            StronglyConnectedComponentDecomposition(storm::models::AbstractModel<ValueType> const& model, StateBlock const& block, bool dropNaiveSccs = false, bool onlyBottomSccs = false);
+            StronglyConnectedComponentDecomposition(storm::models::AbstractModel<ValueType> const& model, Block const& block, bool dropNaiveSccs = false, bool onlyBottomSccs = false);
             
             /*
              * Creates an SCC decomposition of the given subsystem in the given model.