bijection check for homomorphism

Former-commit-id: bf7f2f4066

src/storage/dft/DFT.cpp

@@ -180,20 +180,29 @@ namespace storm {
         std::vector<std::vector<size_t>> DFT<ValueType>::findSymmetries(DFTColouring<ValueType> const& colouring) const {
             std::vector<size_t> vec;
             vec.reserve(nrElements());
-            storm::utility::iota_n(std::back_inserter(vec), 14, 0);
+            storm::utility::iota_n(std::back_inserter(vec), nrElements(), 0);
             BijectionCandidates<ValueType> completeCategories = colouring.colourSubdft(vec);
             std::vector<std::vector<size_t>> res;
+            
             for(auto const& colourClass : completeCategories.gateCandidates) {
                 if(colourClass.second.size() > 1) {
+                    std::vector<size_t> handledWithinClass;
                     for(auto it1 = colourClass.second.cbegin(); it1 != colourClass.second.cend(); ++it1) {
+                        if(!getGate(*it1)->hasOnlyStaticParents()) {
+                            continue;
+                        }
                         std::vector<size_t> sortedParent1Ids = getGate(*it1)->parentIds();
                         std::sort(sortedParent1Ids.begin(), sortedParent1Ids.end());
                         auto it2 = it1;
                         for(++it2; it2 != colourClass.second.cend(); ++it2) {
+                            if(!getGate(*it2)->hasOnlyStaticParents()) {
+                                continue;
+                            }
                             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()) {
@@ -201,7 +210,11 @@ namespace storm {
                                     auto LHS = colouring.colourSubdft(isubdft1);
                                     auto RHS = colouring.colourSubdft(isubdft2);
                                     auto IsoCheck = DFTIsomorphismCheck<ValueType>(LHS, RHS, *this);
-                                    IsoCheck.findIsomorphism();
+                                    isSymmetry = IsoCheck.findIsomorphism();
+                                }
+                                if(isSymmetry) {
+                                    std::cout << "subdfts are symmetric" << std::endl;
+                                    
                                 }
                             }
                         }

src/storage/dft/DFTIsomorphism.h

@@ -261,11 +261,42 @@ namespace storage {
          */
         bool check() {
             // We can skip BEs, as they are identified by they're homomorphic if they are in the same class
-            for(auto const& index : bijection) {
-                // As they are in the same group, the types are fine already. We just have to check the children.
-
+            for(auto const& indexpair : bijection) {
+                // Check type first. Colouring takes care of a lot, but not necesarily everything (e.g. voting thresholds)
+                equalType(*dft.getElement(indexpair.first), *dft.getElement(indexpair.second));
+                if(dft.isGate(indexpair.first)) {
+                    assert(dft.isGate(indexpair.second));
+                    auto const& lGate = dft.getGate(indexpair.first);
+                    std::set<size_t> childrenLeftMapped;
+                    for(auto const& child : lGate->children() ) {
+                        childrenLeftMapped.insert(bijection.at(child->id()));
+                    }
+                    auto const& rGate = dft.getGate(indexpair.second);
+                    std::set<size_t> childrenRight;
+                    for(auto const& child : rGate->children() ) {
+                        childrenRight.insert(child->id());
+                    }
+                    if(childrenLeftMapped != childrenRight) {
+                        return false;
+                    }
+                } else if(dft.isDependency(indexpair.first)) {
+                    assert(dft.isDependency(indexpair.second));
+                    auto const& lDep = dft.getDependency(indexpair.first);
+                    auto const& rDep = dft.getDependency(indexpair.second);
+                    if(bijection.at(lDep->triggerEvent()->id()) != rDep->triggerEvent()->id()) {
+                        return false;
+                    } 
+                    if(bijection.at(lDep->dependentEvent()->id()) != rDep->dependentEvent()->id()) {
+                        return false;
+                    }
+                }
+                else {
+                    assert(dft.isBasicElement(indexpair.first));
+                    assert(dft.isBasicElement(indexpair.second));
+                    // No operations required.
+                }
             }
-            return false;
+            return true;
         }
 
     private:
@@ -341,9 +372,7 @@ namespace storage {
         }
 
 
-        //std::vector<std::pair<size_t, size_t>> computeNextCandidate(){
-
-        //}
+        
     };