Revelant DFT events are not part of symmetries

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 {};

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);