towards using symred for counting abstr

Former-commit-id: 51bad8ba1e

src/storage/dft/DFT.cpp

@@ -186,8 +186,12 @@ namespace storm {
             
             for(auto const& colourClass : completeCategories.gateCandidates) {
                 if(colourClass.second.size() > 1) {
-                    std::vector<size_t> handledWithinClass;
+                    std::set<size_t> foundEqClassFor;
                     for(auto it1 = colourClass.second.cbegin(); it1 != colourClass.second.cend(); ++it1) {
+                        std::vector<std::vector<size_t>> symClass;
+                        if(foundEqClassFor.count(*it1) > 0) {
+                            continue;
+                        }
                         if(!getGate(*it1)->hasOnlyStaticParents()) {
                             continue;
                         }
@@ -200,20 +204,38 @@ namespace storm {
                             }
                             std::vector<size_t> sortedParent2Ids = getGate(*it2)->parentIds();
                             std::sort(sortedParent2Ids.begin(), sortedParent2Ids.end());
+                            
                             if(sortedParent1Ids == sortedParent2Ids) {
                                 std::cout << "Considering ids " << *it1 << ", " << *it2 << " for isomorphism." << std::endl;
                                 bool isSymmetry = false;
                                 std::vector<size_t> isubdft1 = getGate(*it1)->independentSubDft();
                                 std::vector<size_t> isubdft2 = getGate(*it2)->independentSubDft();
-                                if(!isubdft1.empty() && !isubdft2.empty() && isubdft1.size() == isubdft2.size()) {
-                                    std::cout << "Checking subdfts from " << *it1 << ", " << *it2 << " for isomorphism." << std::endl;
-                                    auto LHS = colouring.colourSubdft(isubdft1);
-                                    auto RHS = colouring.colourSubdft(isubdft2);
-                                    auto IsoCheck = DFTIsomorphismCheck<ValueType>(LHS, RHS, *this);
-                                    isSymmetry = IsoCheck.findIsomorphism();
+                                if(isubdft1.empty() || isubdft2.empty() || isubdft1.size() != isubdft2.size()) {
+                                    continue;
                                 }
+                                std::cout << "Checking subdfts from " << *it1 << ", " << *it2 << " for isomorphism." << std::endl;
+                                auto LHS = colouring.colourSubdft(isubdft1);
+                                auto RHS = colouring.colourSubdft(isubdft2);
+                                auto IsoCheck = DFTIsomorphismCheck<ValueType>(LHS, RHS, *this);
+                                isSymmetry = IsoCheck.findIsomorphism();
                                 if(isSymmetry) {
                                     std::cout << "subdfts are symmetric" << std::endl;
+                                    foundEqClassFor.insert(*it2);
+                                    if(symClass.empty()) {
+                                        for(auto const& i : isubdft1) {
+                                            symClass.push_back(std::vector<size_t>({i}));
+                                        }
+                                    }
+                                    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;
+                                        
+                                    }
                                     
                                 }
                             }

src/storage/dft/DFTElements.cpp

@@ -55,11 +55,6 @@ namespace storm {
         template<typename ValueType>
         void DFTElement<ValueType>::extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot) const {
             if(elemsInSubtree.count(this->id()) > 0) return;
-            std::cout << "ID " <<  this->id() <<  "PREL elems ";
-            for(auto const& i : elemsInSubtree) {
-                std::cout << i << " ";
-            }
-            std::cout << "in subtree." << std::endl;
             if(std::find(parentsOfSubRoot.begin(), parentsOfSubRoot.end(), mId) != parentsOfSubRoot.end()) {
                 // This is a parent of the suspected root, thus it is not a subdft.
                 elemsInSubtree.clear();

src/storage/dft/DFTElements.h

@@ -291,11 +291,6 @@ namespace storm {
                 std::vector<size_t> pids = this->parentIds();
                 for(auto const& child : mChildren) {
                     child->extendSubDft(unit, pids);
-                    std::cout << "int sub ";
-                    for(auto const& i : unit) {
-                        std::cout << i << " ";
-                    }
-                    std::cout << std::endl;
                     if(unit.empty()) {
                         // Parent in the subdft, ie it is *not* a subdft
                         break;

src/storage/dft/DFTIsomorphism.h

@@ -256,8 +256,8 @@ namespace storage {
          * Can only be called after the findIsomorphism procedure returned that an isomorphism has found.
          * @see findIsomorphism
          */
-        std::vector<std::pair<size_t, size_t>> getIsomorphism() const {
-
+        std::map<size_t, size_t> const& getIsomorphism() const {
+            return bijection;
         }
 
         /**