Throw exception for difference operation

ultimate-pa · Nov 25, 2024 · 5e731c8 · 5e731c8
1 parent ae94f3b
commit 5e731c8
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/...mata/src/de/uni_freiburg/informatik/ultimate/automata/petrinet/operations/Difference.java b/...mata/src/de/uni_freiburg/informatik/ultimate/automata/petrinet/operations/Difference.java
@@ -53,6 +53,7 @@
 import de.uni_freiburg.informatik.ultimate.automata.petrinet.netdatastructures.Transition;
 import de.uni_freiburg.informatik.ultimate.automata.statefactory.IBlackWhiteStateFactory;
 import de.uni_freiburg.informatik.ultimate.automata.statefactory.IPetriNet2FiniteAutomatonStateFactory;
+import de.uni_freiburg.informatik.ultimate.util.datastructures.DataStructureUtils;
 import de.uni_freiburg.informatik.ultimate.util.datastructures.ImmutableSet;
 import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.HashRelation;
 
@@ -165,6 +166,10 @@ public Difference(final AutomataLibraryServices services, final IBlackWhiteState
 			final LoopSyncMethod loopSyncMethod, final DifferencePairwiseOnDemand<LETTER, PLACE, ?> inputDpod,
 			final boolean removeRedundantFlow) throws AutomataOperationCanceledException, PetriNetNot1SafeException {
 		super(services);
+		if (DataStructureUtils.haveNonEmptyIntersection(originalMinuend.getPlaces(), subtrahendDfa.getStates())) {
+			throw new UnsupportedOperationException(
+					"Difference is only supported for operands with distinct places / states.");
+		}
 		mSubtrahend = subtrahendDfa;
 		mContentFactory = factory;
 		mLoopSyncMethod = loopSyncMethod;