More preparations for counting abstraction

Former-commit-id: b283b28fdd

src/storage/dft/DFT.cpp

@@ -85,17 +85,23 @@ namespace storm {
                 visitQueue.push(mTopLevelIndex);
                 stateIndex = performStateGenerationInfoDFS(generationInfo, visitQueue, visited, stateIndex);
             } else {
-                // Perform DFS for first subtree of each symmetry
                 for (auto const& symmetryGroup : symmetries.groups) {
+                    assert(!symmetryGroup.second.empty());
+
+                    // Perform DFS for first subtree of each symmetry
                     visitQueue.push(symmetryGroup.first);
-                    size_t stateIndexBefore = stateIndex;
+                    size_t groupIndex = stateIndex;
                     stateIndex = performStateGenerationInfoDFS(generationInfo, visitQueue, visited, stateIndex);
-                    size_t offset = stateIndex - stateIndexBefore;
+                    size_t offset = stateIndex - groupIndex;
                     
                     // Mirror symmetries
-                    assert(!symmetryGroup.second.empty());
+                    size_t noSymmetricElements = symmetryGroup.second.front().size();
+                    assert(noSymmetricElements > 1);
+
                     for (std::vector<size_t> symmetricElements : symmetryGroup.second) {
-                        assert(symmetricElements.size() > 1);
+                        assert(symmetricElements.size() == noSymmetricElements);
+
+                        // Initialize for original element
                         size_t originalElement = symmetricElements[0];
                         size_t index = generationInfo.getStateIndex(originalElement);
                         size_t activationIndex = isRepresentative(originalElement) ? generationInfo.getSpareActivationIndex(originalElement) : 0;
@@ -122,6 +128,13 @@ namespace storm {
                             }
                         }
                     }
+
+                    // Store starting indices of symmetry groups
+                    std::vector<size_t> symmetryIndices;
+                    for (size_t i = 0; i < noSymmetricElements; ++i) {
+                        symmetryIndices.push_back(groupIndex + i * offset);
+                    }
+                    generationInfo.addSymmetry(offset, symmetryIndices);
                 }
             }
 
@@ -146,9 +159,32 @@ namespace storm {
             STORM_LOG_TRACE(generationInfo);
             assert(stateIndex == mStateVectorSize);
             assert(visited.full());
+            
             return generationInfo;
         }
         
+        template<typename ValueType>
+        size_t DFT<ValueType>::generateStateInfo(DFTStateGenerationInfo& generationInfo, size_t id, storm::storage::BitVector& visited, size_t stateIndex) const {
+            assert(!visited[id]);
+            visited.set(id);
+            
+            // Reserve bits for element
+            generationInfo.addStateIndex(id, stateIndex);
+            stateIndex += 2;
+            
+            if (isRepresentative(id)) {
+                generationInfo.addSpareActivationIndex(id, stateIndex);
+                ++stateIndex;
+            }
+            
+            if (mElements[id]->isSpareGate()) {
+                generationInfo.addSpareUsageIndex(id, stateIndex);
+                stateIndex += generationInfo.usageInfoBits();
+            }
+            
+            return stateIndex;
+        }
+        
         template<typename ValueType>
         size_t DFT<ValueType>::performStateGenerationInfoDFS(DFTStateGenerationInfo& generationInfo, std::queue<size_t>& visitQueue, storm::storage::BitVector& visited, size_t stateIndex) const {
             while (!visitQueue.empty()) {
@@ -158,30 +194,14 @@ namespace storm {
                     // Already visited
                     continue;
                 }
-                visited.set(id);
-                DFTElementPointer element = mElements[id];
+                stateIndex = generateStateInfo(generationInfo, id, visited, stateIndex);
                 
                 // Insert children
-                if (element->isGate()) {
-                    for (auto const& child : std::static_pointer_cast<DFTGate<ValueType>>(element)->children()) {
+                if (mElements[id]->isGate()) {
+                    for (auto const& child : std::static_pointer_cast<DFTGate<ValueType>>(mElements[id])->children()) {
                         visitQueue.push(child->id());
                     }
                 }
-                
-                // Reserve bits for element
-                generationInfo.addStateIndex(id, stateIndex);
-                stateIndex += 2;
-                
-                if (isRepresentative(id)) {
-                    generationInfo.addSpareActivationIndex(id, stateIndex);
-                    ++stateIndex;
-                }
-                
-                if (element->isSpareGate()) {
-                    generationInfo.addSpareUsageIndex(id, stateIndex);
-                    stateIndex += generationInfo.usageInfoBits();
-                }
-                
             }
             return stateIndex;
         }

src/storage/dft/DFT.h

@@ -41,6 +41,7 @@ namespace storm {
             std::map<size_t, size_t> mSpareUsageIndex; // id spare -> index first bit in state
             std::map<size_t, size_t> mSpareActivationIndex; // id spare representative -> index in state
             std::vector<size_t> mIdToStateIndex; // id -> index first bit in state
+            std::vector<std::pair<size_t, std::vector<size_t>>> mSymmetries; // pair (lenght of symmetry group, vector indicating the starting points of the symmetry groups)
             
         public:
             
@@ -79,6 +80,24 @@ namespace storm {
                 return mSpareActivationIndex.at(id);
             }
             
+            size_t addSymmetry(size_t lenght, std::vector<size_t>& startingIndices) {
+                mSymmetries.push_back(std::make_pair(lenght, startingIndices));
+            }
+            
+            size_t getSymmetrySize() {
+                return mSymmetries.size();
+            }
+            
+            size_t getSymmetryLength(size_t pos) {
+                assert(pos < mSymmetries.size());
+                return mSymmetries[pos].first;
+            }
+            
+            std::vector<size_t> const& getSymmetryIndices(size_t pos) {
+                assert(pos < mSymmetries.size());
+                return mSymmetries[pos].second;
+            }
+            
             friend std::ostream& operator<<(std::ostream& os, DFTStateGenerationInfo const& info) {
                 os << "Id to state index:" << std::endl;
                 for (size_t id = 0; id < info.mIdToStateIndex.size(); ++id) {
@@ -92,6 +111,14 @@ namespace storm {
                 for (auto pair : info.mSpareActivationIndex) {
                     os << pair.first << " -> " << pair.second << std::endl;
                 }
+                os << "Symmetries:" << std::endl;
+                for (auto pair : info.mSymmetries) {
+                    os << "Length: " << pair.first << ", starting indices: ";
+                    for (size_t index : pair.second) {
+                        os << index << ", ";
+                    }
+                    os << std::endl;
+                }
                 return os;
             }
             
@@ -128,6 +155,8 @@ namespace storm {
             
             DFTStateGenerationInfo buildStateGenerationInfo(storm::storage::DFTIndependentSymmetries const& symmetries) const;
             
+            size_t generateStateInfo(DFTStateGenerationInfo& generationInfo, size_t id, storm::storage::BitVector& visited, size_t stateIndex) const;
+
             size_t performStateGenerationInfoDFS(DFTStateGenerationInfo& generationInfo, std::queue<size_t>& visitQueue, storm::storage::BitVector& visited, size_t stateIndex) const;
             
             size_t stateVectorSize() const {