diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index 5735af2a7..e231c7c8d 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -180,20 +180,29 @@ namespace storm { std::vector> DFT::findSymmetries(DFTColouring const& colouring) const { std::vector 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 completeCategories = colouring.colourSubdft(vec); std::vector> res; + for(auto const& colourClass : completeCategories.gateCandidates) { if(colourClass.second.size() > 1) { + std::vector handledWithinClass; for(auto it1 = colourClass.second.cbegin(); it1 != colourClass.second.cend(); ++it1) { + if(!getGate(*it1)->hasOnlyStaticParents()) { + continue; + } std::vector 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 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()) { @@ -201,7 +210,11 @@ namespace storm { auto LHS = colouring.colourSubdft(isubdft1); auto RHS = colouring.colourSubdft(isubdft2); auto IsoCheck = DFTIsomorphismCheck(LHS, RHS, *this); - IsoCheck.findIsomorphism(); + isSymmetry = IsoCheck.findIsomorphism(); + } + if(isSymmetry) { + std::cout << "subdfts are symmetric" << std::endl; + } } } diff --git a/src/storage/dft/DFTIsomorphism.h b/src/storage/dft/DFTIsomorphism.h index 6c4a44ad6..182a2b01c 100644 --- a/src/storage/dft/DFTIsomorphism.h +++ b/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 childrenLeftMapped; + for(auto const& child : lGate->children() ) { + childrenLeftMapped.insert(bijection.at(child->id())); + } + auto const& rGate = dft.getGate(indexpair.second); + std::set 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> computeNextCandidate(){ - - //} + };