Commit to switch workplace.

Former-commit-id: da5fac08cf

src/models/AbstractModel.h

@@ -147,7 +147,8 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
          * @param decomposition A decomposition 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<T> extractPartitionDependencyGraph(storm::storage::Decomposition<storm::storage::StateBlock> const& decomposition) const {
+        template <typename BlockType>
+        storm::storage::SparseMatrix<T> extractPartitionDependencyGraph(storm::storage::Decomposition<BlockType> 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.
@@ -163,7 +164,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::StateBlock const& block = decomposition[currentBlockIndex];
+                typename storm::storage::Decomposition<BlockType>::block_type const& block = decomposition[currentBlockIndex];
                 
                 // Now, we determine the blocks which are reachable (in one step) from the current block.
                 boost::container::flat_set<uint_fast64_t> allTargetBlocks;

src/storage/Decomposition.cpp

@@ -1,4 +1,5 @@
 #include "src/storage/Decomposition.h"
+#include "src/storage/StronglyConnectedComponent.h"
 #include "src/storage/MaximalEndComponent.h"
 
 namespace storm {
@@ -89,8 +90,8 @@ namespace storm {
             return out;
         }
         
-        template class Decomposition<StateBlock>;
-        template std::ostream& operator<<(std::ostream& out, Decomposition<StateBlock> const& decomposition);
+        template class Decomposition<StronglyConnectedComponent>;
+        template std::ostream& operator<<(std::ostream& out, Decomposition<StronglyConnectedComponent> const& decomposition);
         
         template class Decomposition<MaximalEndComponent>;
         template std::ostream& operator<<(std::ostream& out, Decomposition<MaximalEndComponent> const& decomposition);

src/storage/Decomposition.h

@@ -119,8 +119,8 @@ namespace storm {
             block_type& operator[](uint_fast64_t index);
             
             // Declare the streaming operator as a friend function to enable output of decompositions.
-            template<typename BlockTimePrime>
-            friend std::ostream& operator<<(std::ostream& out, Decomposition<BlockTimePrime> const& decomposition);
+            template<typename BlockTypePrime>
+            friend std::ostream& operator<<(std::ostream& out, Decomposition<BlockTypePrime> const& decomposition);
             
         protected:
             // The blocks of the decomposition.

src/storage/MaximalEndComponent.h

@@ -4,6 +4,8 @@
 #include <unordered_map>
 #include <boost/container/flat_set.hpp>
 
+#include "src/storage/sparse/StateType.h"
+
 namespace storm {
     namespace storage {
         
@@ -12,7 +14,7 @@ namespace storm {
          */
         class MaximalEndComponent {
         public:
-            typedef boost::container::flat_set<uint_fast64_t> set_type;
+            typedef boost::container::flat_set<sparse::state_type> set_type;
             typedef std::unordered_map<uint_fast64_t, set_type> map_type;
             typedef map_type::iterator iterator;
             typedef map_type::const_iterator const_iterator;

src/storage/MaximalEndComponentDecomposition.cpp

@@ -1,5 +1,6 @@
 #include <list>
 #include <queue>
+#include <iostream>
 
 #include "src/storage/MaximalEndComponentDecomposition.h"
 #include "src/storage/StronglyConnectedComponentDecomposition.h"
@@ -56,7 +57,7 @@ namespace storm {
             endComponentStateSets.emplace_back(subsystem.begin(), subsystem.end());
             storm::storage::BitVector statesToCheck(model.getNumberOfStates());
             
-            
+            std::cout << " starting... " << std::endl;
             // The iterator used here should really be a const_iterator.
             // However, gcc 4.8 (and assorted libraries) does not provide an erase(const_iterator) method for std::list
             // but only an erase(iterator). This is in compliance with the c++11 draft N3337, which specifies the change
@@ -69,7 +70,9 @@ namespace storm {
                 bool mecChanged = false;
                 
                 // Get an SCC decomposition of the current MEC candidate.
+                std::cout << "boom" << std::endl;
                 StronglyConnectedComponentDecomposition<ValueType> sccs(model, mec, true);
+                std::cout << "boom1" << std::endl;
                 
                 // We need to do another iteration in case we have either more than once SCC or the SCC is smaller than
                 // the MEC canditate itself.
@@ -80,6 +83,7 @@ namespace storm {
                     statesToCheck.set(scc.begin(), scc.end());
                     
                     while (!statesToCheck.empty()) {
+                        std::cout << "not empty!" << std::endl;
                         storm::storage::BitVector statesToRemove(model.getNumberOfStates());
                         
                         for (auto state : statesToCheck) {
@@ -116,7 +120,7 @@ namespace storm {
                         statesToCheck.clear();
                         for (auto state : statesToRemove) {
                             for (auto const& entry : backwardTransitions.getRow(state)) {
-                                if (!scc.containsState(entry.getColumn())) {
+                                if (scc.containsState(entry.getColumn())) {
                                     statesToCheck.set(entry.getColumn());
                                 }
                             }
@@ -143,6 +147,8 @@ namespace storm {
                 
             } // End of loop over all MEC candidates.
             
+            std::cout << " got here... " << std::endl;
+            
             // Now that we computed the underlying state sets of the MECs, we need to properly identify the choices
             // contained in the MEC and store them as actual MECs.
             this->blocks.reserve(endComponentStateSets.size());
@@ -154,7 +160,7 @@ namespace storm {
                     for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) {
                         bool choiceContained = true;
                         for (auto const& entry : transitionMatrix.getRow(choice)) {
-                            if (mecStateSet.find(entry.getColumn()) == mecStateSet.end()) {
+                            if (!mecStateSet.containsState(entry.getColumn())) {
                                 choiceContained = false;
                                 break;
                             }

src/storage/StateBlock.cpp

@@ -2,46 +2,46 @@
 
 namespace storm {
     namespace storage {
-        template <typename ContainerType>
-        typename StateBlock<ContainerType>::iterator StateBlock<ContainerType>::begin() {
+        typename StateBlock::iterator StateBlock::begin() {
             return states.begin();
         }
         
-        template <typename ContainerType>
-        typename StateBlock<ContainerType>::const_iterator StateBlock<ContainerType>::begin() const {
+        typename StateBlock::const_iterator StateBlock::begin() const {
             return states.begin();
         }
         
-        template <typename ContainerType>
-        typename StateBlock<ContainerType>::iterator StateBlock<ContainerType>::end() {
+        typename StateBlock::iterator StateBlock::end() {
             return states.end();
         }
         
-        template <typename ContainerType>
-        typename StateBlock<ContainerType>::const_iterator StateBlock<ContainerType>::end() const {
+        typename StateBlock::const_iterator StateBlock::end() const {
             return states.end();
         }
         
-        template <typename ContainerType>
-        std::size_t StateBlock<ContainerType>::size() const {
+        std::size_t StateBlock::size() const {
             return states.size();
         }
         
-        template <typename ContainerType>
-        void StateBlock<ContainerType>::insert(value_type const& state) {
+        bool StateBlock::empty() const {
+            return states.empty();
+        }
+        
+        void StateBlock::insert(value_type const& state) {
             states.insert(state);
         }
 
-        template <typename ContainerType>
-        void StateBlock<ContainerType>::erase(value_type const& state) {
+        void StateBlock::erase(value_type const& state) {
             states.erase(state);
         }
 
-        template <typename ContainerType>
-        bool StateBlock<ContainerType>::containsState(value_type const& state) const {
+        bool StateBlock::containsState(value_type const& state) const {
             return this->states.find(state) != this->states.end();
         }
         
+        StateBlock::container_type const& StateBlock::getStates() const {
+            return this->states;
+        }
+        
         std::ostream& operator<<(std::ostream& out, FlatSetStateContainer const& block) {
             out << "{";
             for (auto const& element : block) {
@@ -51,7 +51,9 @@ namespace storm {
             return out;
         }
         
-        // Explicitly instantiate template.
-        template Block<FlatSetStateContainer>;
+        std::ostream& operator<<(std::ostream& out, StateBlock const& block) {
+            out << block.getStates();
+            return out;
+        }
     }
 }

src/storage/StateBlock.h

@@ -3,6 +3,7 @@
 
 #include <boost/container/flat_set.hpp>
 
+#include "src/utility/OsDetection.h"
 #include "src/storage/sparse/StateType.h"
 
 namespace storm {
@@ -11,24 +12,54 @@ namespace storm {
         // Typedef the most common state container
         typedef boost::container::flat_set<sparse::state_type> 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);
 
-        template <typename ContainerType = FlatSetStateContainer>
         class StateBlock {
         public:
-            typedef ContainerType container_type;
+            typedef FlatSetStateContainer container_type;
             typedef typename container_type::value_type value_type;
             static_assert(std::is_same<value_type, sparse::state_type>::value, "Illegal value type of container.");
             typedef typename container_type::iterator iterator;
             typedef typename container_type::const_iterator const_iterator;
             
+            // Default constructors.
+            StateBlock() = default;
+            StateBlock(StateBlock const& other) = default;
+            StateBlock(StateBlock&& other) = default;
+#ifndef WINDOWS
+            StateBlock& operator=(StateBlock const& other) = default;
+            StateBlock& operator=(StateBlock&& other) = default;
+#endif
+            /*!
+             * Creates a state block and inserts all elements in the given range.
+             *
+             * @param first The first element of the range to insert.
+             * @param last The last element of the range (that is itself not inserted).
+             */
+            template <typename InputIterator>
+            StateBlock(InputIterator first, InputIterator last) : states(first, last) {
+                // Intentionally left empty.
+            }
+            
+            /*!
+             * Constructs a state block from the given initializer list.
+             *
+             * @param list The list of states to add to this state block.
+             */
+            StateBlock(std::initializer_list<sparse::state_type> list) : states(list.begin(), list.end()) {
+                // Intentionally left empty.
+            }
+            
+            /*!
+             * Checks whether the two state blocks contain exactly the same states.
+             *
+             * @param other The state block with which to compare the current one.
+             * @return True iff the two state blocks contain exactly the same states.
+             */
+            bool operator==(StateBlock const& other) const {
+                return this->states == other.states;
+            }
+            
             /*!
              * Returns an iterator to the states in this SCC.
              *
@@ -92,10 +123,26 @@ namespace storm {
              */
             bool empty() const;
             
+            /*!
+             * Retrieves the set of states contained in the StateBlock.
+             *
+             * @return The set of states contained in the StateBlock.
+             */
+            container_type const& getStates() const;
+            
         private:
             // The container that holds the states.
-            ContainerType states;
+            container_type states;
         };
+        
+        /*!
+         * 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);
     }
 }
 

src/storage/StronglyConnectedComponent.h

@@ -3,6 +3,7 @@
 
 #include "src/storage/StateBlock.h"
 #include "src/storage/Decomposition.h"
+#include "src/utility/OsDetection.h"
 
 namespace storm {
     namespace storage {
@@ -11,11 +12,15 @@ namespace storm {
          * 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 StateBlock<FlatSetStateContainer> {
-            /*!
-             * Creates an empty strongly connected component.
-             */
-            StronglyConnectedComponent();
+        class StronglyConnectedComponent : public StateBlock {
+        public:
+            StronglyConnectedComponent() = default;
+            StronglyConnectedComponent(StronglyConnectedComponent const& other) = default;
+            StronglyConnectedComponent(StronglyConnectedComponent&& other) = default;
+#ifndef WINDOWS
+            StronglyConnectedComponent& operator=(StronglyConnectedComponent const& other) = default;
+            StronglyConnectedComponent& operator=(StronglyConnectedComponent&& other) = default;
+#endif
             
             /*!
              * Sets whether this SCC is trivial or not.

src/storage/StronglyConnectedComponentDecomposition.cpp

@@ -14,8 +14,7 @@ namespace storm {
         }
         
         template <typename ValueType>
-        template <typename ContainerType>
-        StronglyConnectedComponentDecomposition<ValueType>::StronglyConnectedComponentDecomposition(storm::models::AbstractModel<ValueType> const& model, StateBlock<ContainerType> const& block, bool dropNaiveSccs, bool onlyBottomSccs) {
+        StronglyConnectedComponentDecomposition<ValueType>::StronglyConnectedComponentDecomposition(storm::models::AbstractModel<ValueType> const& model, StateBlock const& block, bool dropNaiveSccs, bool onlyBottomSccs) {
             storm::storage::BitVector subsystem(model.getNumberOfStates(), block.begin(), block.end());
             performSccDecomposition(model.getTransitionMatrix(), subsystem, dropNaiveSccs, onlyBottomSccs);
         }
@@ -204,6 +203,5 @@ namespace storm {
         
         // Explicitly instantiate the SCC decomposition.
         template class StronglyConnectedComponentDecomposition<double>;
-        template StronglyConnectedComponentDecomposition<double>::StronglyConnectedComponentDecomposition(storm::models::AbstractModel<double> const& model, StateBlock<FlatSetStateContainer> const& block, bool dropNaiveSccs, bool onlyBottomSccs);
     } // namespace storage
 } // namespace storm

src/storage/StronglyConnectedComponentDecomposition.h

@@ -46,8 +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.
              */
-            template<typename ContainerType>
-            StronglyConnectedComponentDecomposition(storm::models::AbstractModel<ValueType> const& model, StateBlock<ContainerType> const& block, bool dropNaiveSccs = false, bool onlyBottomSccs = false);
+            StronglyConnectedComponentDecomposition(storm::models::AbstractModel<ValueType> const& model, StateBlock const& block, bool dropNaiveSccs = false, bool onlyBottomSccs = false);
             
             /*
              * Creates an SCC decomposition of the given subsystem in the given model.

test/functional/storage/StronglyConnectedComponentDecompositionTest.cpp

@@ -37,8 +37,8 @@ TEST(StronglyConnectedComponentDecomposition, FullSystem2) {
     storm::storage::StateBlock const& scc1 = sccDecomposition[0];
     storm::storage::StateBlock const& scc2 = sccDecomposition[1];
 
-    std::vector<uint_fast64_t> correctScc1 = {1, 3, 8, 9, 10};
-    std::vector<uint_fast64_t> correctScc2 = {4, 5, 6, 7};
+    storm::storage::StateBlock correctScc1 = {1, 3, 8, 9, 10};
+    storm::storage::StateBlock correctScc2 = {4, 5, 6, 7};
     ASSERT_TRUE(scc1 == storm::storage::StateBlock(correctScc1.begin(), correctScc1.end()) || scc1 == storm::storage::StateBlock(correctScc2.begin(), correctScc2.end()));
     ASSERT_TRUE(scc2 == storm::storage::StateBlock(correctScc1.begin(), correctScc1.end()) || scc2 == storm::storage::StateBlock(correctScc2.begin(), correctScc2.end()));