From 5e731c8a254bd0678ce855c02dc3cfa31b0fd03d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Thu, 19 Sep 2024 13:02:17 +0200 Subject: [PATCH] Throw exception for difference operation --- .../ultimate/automata/petrinet/operations/Difference.java | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/petrinet/operations/Difference.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/petrinet/operations/Difference.java index 5a91050c466..94a93e18f19 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/petrinet/operations/Difference.java +++ b/trunk/source/Library-Automata/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 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;