|
|
|
@ -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<BitSet, ? extends AcceptanceOmega> simplifyAcceptance(DA<BitSet, ? extends AcceptanceOmega> da, AcceptanceType... allowedAcceptance) |
|
|
|
public static DA<BitSet, ? extends AcceptanceOmega> simplifyAcceptance(PrismComponent parent, DA<BitSet, ? extends AcceptanceOmega> da, AcceptanceType... allowedAcceptance) |
|
|
|
throws PrismException |
|
|
|
{ |
|
|
|
// Simplifications for DRAs |
|
|
|
if (da.getAcceptance() instanceof AcceptanceRabin) { |
|
|
|
DA<BitSet, AcceptanceRabin> dra = (DA<BitSet, AcceptanceRabin>) 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()) { |
|
|
|
|