diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index e231c7c8d..1ce4618cf 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -186,8 +186,12 @@ namespace storm { for(auto const& colourClass : completeCategories.gateCandidates) { if(colourClass.second.size() > 1) { - std::vector handledWithinClass; + std::set foundEqClassFor; for(auto it1 = colourClass.second.cbegin(); it1 != colourClass.second.cend(); ++it1) { + std::vector> symClass; + if(foundEqClassFor.count(*it1) > 0) { + continue; + } if(!getGate(*it1)->hasOnlyStaticParents()) { continue; } @@ -200,20 +204,38 @@ namespace storm { } std::vector 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 isubdft1 = getGate(*it1)->independentSubDft(); std::vector 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(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(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({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; + + } } } diff --git a/src/storage/dft/DFTElements.cpp b/src/storage/dft/DFTElements.cpp index d59ec8f41..26f5f9cbe 100644 --- a/src/storage/dft/DFTElements.cpp +++ b/src/storage/dft/DFTElements.cpp @@ -55,11 +55,6 @@ namespace storm { template void DFTElement::extendSubDft(std::set& elemsInSubtree, std::vector 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(); diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h index 81b8ce303..c352bd38e 100644 --- a/src/storage/dft/DFTElements.h +++ b/src/storage/dft/DFTElements.h @@ -291,11 +291,6 @@ namespace storm { std::vector 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; diff --git a/src/storage/dft/DFTIsomorphism.h b/src/storage/dft/DFTIsomorphism.h index 5aec35714..0d5590d3d 100644 --- a/src/storage/dft/DFTIsomorphism.h +++ b/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> getIsomorphism() const { - + std::map const& getIsomorphism() const { + return bijection; } /**