diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index 75d43eb47..570ba9fa5 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/src/storm-dft/storage/dft/DFT.cpp @@ -799,6 +799,11 @@ namespace storm { bool sharedSpareMode = false; std::map<size_t, size_t> bijection; + if (getElement(index1)->isRelevant() || getElement(index2)->isRelevant()) { + // Relevant events need to be uniquely identified and cannot be symmetric. + return {}; + } + if (isBasicElement(index1)) { if (!isBasicElement(index2)) { return {}; diff --git a/src/storm-dft/storage/dft/DFTIsomorphism.h b/src/storm-dft/storage/dft/DFTIsomorphism.h index a08fd6a07..8d35f2529 100644 --- a/src/storm-dft/storage/dft/DFTIsomorphism.h +++ b/src/storm-dft/storage/dft/DFTIsomorphism.h @@ -494,6 +494,9 @@ namespace storage { if (!equalType(*dft.getElement(indexpair.first), *dft.getElement(indexpair.second))) { return false; } + if (dft.getElement(indexpair.first)->isRelevant() || dft.getElement(indexpair.second)->isRelevant()) { + return false; + } if(dft.isGate(indexpair.first)) { STORM_LOG_ASSERT(dft.isGate(indexpair.second), "Element is no gate."); auto const& lGate = dft.getGate(indexpair.first);