diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index 0a90f1513..d56166f60 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -196,8 +196,8 @@ namespace storm { if(!getGate(*it1)->hasOnlyStaticParents()) { continue; } - std::vector sortedParent1Ids = getGate(*it1)->parentIds(); - std::sort(sortedParent1Ids.begin(), sortedParent1Ids.end()); + + std::pair, std::vector> influencedElem1Ids = getSortedParentAndOutDepIds(*it1); auto it2 = it1; for(++it2; it2 != colourClass.second.cend(); ++it2) { if(!getGate(*it2)->hasOnlyStaticParents()) { @@ -206,7 +206,7 @@ namespace storm { std::vector sortedParent2Ids = getGate(*it2)->parentIds(); std::sort(sortedParent2Ids.begin(), sortedParent2Ids.end()); - if(sortedParent1Ids == sortedParent2Ids) { + if(influencedElem1Ids == getSortedParentAndOutDepIds(*it2)) { std::cout << "Considering ids " << *it1 << ", " << *it2 << " for isomorphism." << std::endl; bool isSymmetry = false; std::vector isubdft1 = getGate(*it1)->independentSubDft(); @@ -247,6 +247,18 @@ namespace storm { return DFTIndependentSymmetries(res); } + template + std::pair, std::vector> DFT::getSortedParentAndOutDepIds(size_t index) const { + std::pair, std::vector> res; + res.first = getElement(index)->parentIds(); + std::sort(res.first.begin(), res.first.end()); + for(auto const& dep : getElement(index)->outgoingDependencies()) { + res.second.push_back(dep->id()); + } + std::sort(res.second.begin(), res.second.end()); + return res; + } + // Explicitly instantiate the class. template class DFT; diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h index 57bfee16d..1583cc8d5 100644 --- a/src/storage/dft/DFT.h +++ b/src/storage/dft/DFT.h @@ -233,6 +233,8 @@ namespace storm { DFTIndependentSymmetries findSymmetries(DFTColouring const& colouring) const; private: + std::pair, std::vector> getSortedParentAndOutDepIds(size_t index) const; + bool elementIndicesCorrect() const { for(size_t i = 0; i < mElements.size(); ++i) { if(mElements[i]->id() != i) return false;