diff --git a/prism/src/automata/DASimplifyAcceptance.java b/prism/src/automata/DASimplifyAcceptance.java index 8d0ecfe3..8f386ae7 100644 --- a/prism/src/automata/DASimplifyAcceptance.java +++ b/prism/src/automata/DASimplifyAcceptance.java @@ -2,6 +2,7 @@ package automata; import java.util.BitSet; +import prism.PrismComponent; import prism.PrismException; import explicit.SCCComputer; import acceptance.AcceptanceOmega; @@ -16,18 +17,19 @@ public class DASimplifyAcceptance /** * Tries to simplify the acceptance condition of the deterministic automaton. * Note that the passed parameter {@code da} may be destroyed by this function. + * @param parent the calling PrismComponent (for SCC computer) * @param da the DA to be simplified (may be destroyed) * @param allowedAcceptance the allowed acceptance types */ @SuppressWarnings("unchecked") - public static DA simplifyAcceptance(DA da, AcceptanceType... allowedAcceptance) + public static DA simplifyAcceptance(PrismComponent parent, DA da, AcceptanceType... allowedAcceptance) throws PrismException { // Simplifications for DRAs if (da.getAcceptance() instanceof AcceptanceRabin) { DA dra = (DA) da; // K_i states that do not occur in a (non-trivial) SCC of the DRA may as well be removed - SCCComputer sccComp = explicit.SCCComputer.createSCCComputer(null, new LTSFromDA(da)); + SCCComputer sccComp = explicit.SCCComputer.createSCCComputer(parent, new LTSFromDA(da)); sccComp.computeBSCCs(); BitSet trivial = sccComp.getNotInSCCs(); for (RabinPair pair : dra.getAcceptance()) { diff --git a/prism/src/automata/LTL2DA.java b/prism/src/automata/LTL2DA.java index 11648141..60ce8cbb 100644 --- a/prism/src/automata/LTL2DA.java +++ b/prism/src/automata/LTL2DA.java @@ -132,7 +132,7 @@ public class LTL2DA extends PrismComponent throw new PrismNotSupportedException("Could not convert LTL formula to deterministic automaton"); } - result = DASimplifyAcceptance.simplifyAcceptance(result, allowedAcceptance); + result = DASimplifyAcceptance.simplifyAcceptance(this, result, allowedAcceptance); return result; }