function returns independent symmetries

Former-commit-id: 674f0bcff2

src/storage/dft/DFT.cpp

@@ -1,5 +1,6 @@
 #include <boost/container/flat_set.hpp>
 
+#include <map>
 #include "DFT.h"
 #include "src/exceptions/NotSupportedException.h"
 
@@ -177,12 +178,12 @@ namespace storm {
         }
 
         template<typename ValueType>
-        std::vector<std::vector<size_t>> DFT<ValueType>::findSymmetries(DFTColouring<ValueType> const& colouring) const {
+        DFTIndependentSymmetries DFT<ValueType>::findSymmetries(DFTColouring<ValueType> const& colouring) const {
             std::vector<size_t> vec;
             vec.reserve(nrElements());
             storm::utility::iota_n(std::back_inserter(vec), nrElements(), 0);
             BijectionCandidates<ValueType> completeCategories = colouring.colourSubdft(vec);
-            std::vector<std::vector<size_t>> res;
+            std::map<size_t, std::vector<std::vector<size_t>>> res;
             
             for(auto const& colourClass : completeCategories.gateCandidates) {
                 if(colourClass.second.size() > 1) {
@@ -229,10 +230,6 @@ namespace storm {
                                     auto symClassIt = symClass.begin();
                                     for(auto const& i : isubdft1) {
                                         symClassIt->emplace_back(IsoCheck.getIsomorphism().at(i));
-                                        for(auto const& v : *symClassIt) {
-                                            std::cout << v << " ";
-                                        }
-                                        std::cout << std::endl;
                                         ++symClassIt;
                                         
                                     }
@@ -240,10 +237,14 @@ namespace storm {
                                 }
                             }
                         }
+                        if(!symClass.empty()) {
+                            res.emplace(*it1, symClass);
+                        }
                     }
+                    
                 }
             }
-            return res;
+            return DFTIndependentSymmetries(res);
         }
 
 

src/storage/dft/DFT.h

@@ -11,7 +11,7 @@
 
 #include "DFTElements.h"
 #include "../BitVector.h"
-
+#include "SymmetricUnits.h"
 #include "../../utility/math.h"
 #include "src/utility/macros.h"
 
@@ -230,7 +230,7 @@ namespace storm {
 
             DFTColouring<ValueType> colourDFT() const;
 
-            std::vector<std::vector<size_t>> findSymmetries(DFTColouring<ValueType> const& colouring) const;
+            DFTIndependentSymmetries findSymmetries(DFTColouring<ValueType> const& colouring) const;
 
         private:
             bool elementIndicesCorrect() const {

src/storage/dft/SymmetricUnits.h

@@ -1,7 +1,28 @@
-#ifndef SYMMETRICUNITS_H
-#define	SYMMETRICUNITS_H
-
-
-
-#endif	/* SYMMETRICUNITS_H */
+#pragma once
 
+namespace storm {
+    namespace storage {
+        struct DFTIndependentSymmetries {
+            std::map<size_t, std::vector<std::vector<size_t>>> groups;
+            
+            DFTIndependentSymmetries(std::map<size_t, std::vector<std::vector<size_t>>> groups) : groups(groups) {
+                
+            }
+        };
+        
+        inline std::ostream& operator<<(std::ostream& os, DFTIndependentSymmetries const& s)  {
+            for(auto const& cl : s.groups) {
+                std::cout << "SYM GROUP FOR " << cl.first << std::endl;
+                for(auto const& eqClass : cl.second) {
+                    for(auto const& i : eqClass) {
+                        std::cout << i << " ";
+                    }
+                    std::cout << std::endl;
+                }
+            }
+            
+            
+            return os;
+        }
+    }
+}

src/storm-dyftee.cpp

@@ -23,7 +23,8 @@ void analyzeDFT(std::string filename, std::string property, bool symred = false)
     if(symred) {
         std::cout << dft.getElementsString() << std::endl;
         auto colouring = dft.colourDFT();
-        dft.findSymmetries(colouring);
+        auto res = dft.findSymmetries(colouring);
+        std::cout << res;
     }
         
     // Building Markov Automaton