Add another simplification of DRAs - remove any state in a K_i set that does not occur in a non-trivial SCC of the DRA. This also allows more DRAs to be simplified to DFAs.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10013 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/prism/DASimplifyAcceptance.java

@@ -2,26 +2,40 @@ package prism;
 
 import java.util.BitSet;
 
+import explicit.SCCComputer;
 import acceptance.AcceptanceOmega;
 import acceptance.AcceptanceRabin;
 import acceptance.AcceptanceReach;
 import acceptance.AcceptanceType;
+import acceptance.AcceptanceRabin.RabinPair;
 
 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 da the DA to be simplified (may be destroyed)
 	 * @param allowedAcceptance the allowed acceptance types
-	 * @return
 	 */
-	public static DA<BitSet, ? extends AcceptanceOmega> simplifyAcceptance(DA<BitSet, ? extends AcceptanceOmega> da, AcceptanceType... allowedAcceptance) {
+	@SuppressWarnings("unchecked")
+	public static DA<BitSet, ? extends AcceptanceOmega> simplifyAcceptance(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;
-			if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.REACH) &&
-			    isDFA(dra)) {
+			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));
+			sccComp.computeBSCCs();
+			BitSet trivial = sccComp.getNotInSCCs();
+			for (RabinPair pair : dra.getAcceptance()) {
+				if (pair.getK().intersects(trivial)) {
+					pair.getK().andNot(trivial);
+				}
+			}
+			// See if the DRA is actually a DFA
+			if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.REACH) && isDFA(dra)) {
 				// we can switch to AcceptanceReach
 				AcceptanceReach reachAcceptance = new AcceptanceReach(getDFAGoalStatesForRabin(dra.getAcceptance()));
 				DA.switchAcceptance(dra, reachAcceptance);
@@ -36,12 +50,12 @@ public class DASimplifyAcceptance
 	 * it returns true if every transition from a K_i state goes to another K_i state.
 	 * We also require that there are no L_i states overlapping with any K_j states.
 	 */
-	public static boolean isDFA(DA<BitSet,AcceptanceRabin> dra)
+	public static boolean isDFA(DA<BitSet, AcceptanceRabin> dra)
 	{
 		AcceptanceRabin acceptance = dra.getAcceptance();
 		// Compute potential set of goal states as the union of all K_i sets
 		BitSet goalStates = getDFAGoalStatesForRabin(acceptance);
-		
+
 		// Make sure there are no L_i states in the goal states for any i
 		for (int i = 0; i < acceptance.size(); i++) {
 			if (goalStates.intersects(acceptance.get(i).getL()))