LTL model checking optimisation - skip BSCC/EC detection if DRA is (syntactically) a DFA.

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

prism/src/explicit/DTMCModelChecker.java

@@ -105,13 +105,21 @@ public class DTMCModelChecker extends ProbModelChecker
 		int invMap[] = pair.second;
 		mainLog.print("\n" + modelProduct.infoStringTable());
 
-		// Find accepting BSCCs + compute reachability probabilities
-		mainLog.println("\nFinding accepting BSCCs...");
-		BitSet acceptingBSCCs = mcLtl.findAcceptingBSCCsForRabin(dra, modelProduct, invMap);
+		// Find accepting states + compute reachability probabilities
+		BitSet acc = null;
+		if (dra.isDFA()) {
+			// For a DFA, just collect the accept states
+			mainLog.println("\nSkipping BSCC detection since DRA is a DFA...");
+			acc = mcLtl.findTargetStatesForRabin(dra, modelProduct, invMap);
+		} else {
+			// Usually, we have to detect BSCCs in the product
+			mainLog.println("\nFinding accepting BSCCs...");
+			acc = mcLtl.findAcceptingBSCCsForRabin(dra, modelProduct, invMap);
+		}
 		mainLog.println("\nComputing reachability probabilities...");
 		mcProduct = new DTMCModelChecker(this);
 		mcProduct.inheritSettings(this);
-		probsProduct = StateValues.createFromDoubleArray(mcProduct.computeReachProbs((DTMC) modelProduct, acceptingBSCCs).soln, modelProduct);
+		probsProduct = StateValues.createFromDoubleArray(mcProduct.computeReachProbs((DTMC) modelProduct, acc).soln, modelProduct);
 
 		// Mapping probabilities in the original model
 		double[] probsProductDbl = probsProduct.getDoubleArray();

prism/src/explicit/LTLModelChecker.java

@@ -310,6 +310,33 @@ public class LTLModelChecker extends PrismComponent
 		return new Pair<NondetModel, int[]>(prodModel, invMap);
 	}
 
+	/**
+	 * Find the set of states in a model corresponding to the "target" part of a Rabin acceptance condition,
+	 * i.e. just the union of the K_i parts of the (L_i,K_i) pairs.  
+	 * @param dra The DRA
+	 * @param model The model
+	 * @param invMap The map returned by the constructProduct method(s)
+	 * @return
+	 */
+	public BitSet findTargetStatesForRabin(DRA<BitSet> dra, Model model, int invMap[])
+	{
+		// Get union of K_i sets
+		BitSet unionK = new BitSet();
+		int numAcceptancePairs = dra.getNumAcceptancePairs();
+		for (int acceptancePair = 0; acceptancePair < numAcceptancePairs; acceptancePair++) {
+			unionK.or(dra.getAcceptanceK(acceptancePair));
+		}
+		// Collate all model states with a K_i component
+		int draSize = dra.size();
+		int numStates = (int) model.getNumStates();
+		BitSet result = new BitSet();
+		for (int state = 0; state < numStates; state++) {
+			int draState = invMap[state] % draSize;
+			result.set(state, unionK.get(draState));
+		}
+		return result;
+	}
+	
 	/**
 	 * Find the set of states belong to accepting BSCCs in a model wrt a Rabin acceptance condition.
 	 * @param dra The DRA

prism/src/explicit/MDPModelChecker.java

@@ -112,13 +112,21 @@ public class MDPModelChecker extends ProbModelChecker
 		modelProduct = pair.first;
 		int invMap[] = pair.second;
 
-		// Find accepting MECs + compute reachability probabilities
-		mainLog.println("\nFinding accepting MECs...");
-		BitSet acceptingMECs = mcLtl.findAcceptingECStatesForRabin(dra, modelProduct, invMap);
+		// Find accepting states + compute reachability probabilities
+		BitSet acc = null;
+		if (dra.isDFA()) {
+			// For a DFA, just collect the accept states
+			mainLog.println("\nSkipping MEC detection since DRA is a DFA...");
+			acc = mcLtl.findTargetStatesForRabin(dra, modelProduct, invMap);
+		} else {
+			// Usually, we have to detect MECs in the product
+			mainLog.println("\nFinding accepting MECs...");
+			acc = mcLtl.findAcceptingECStatesForRabin(dra, modelProduct, invMap);
+		}
 		mainLog.println("\nComputing reachability probabilities...");
 		mcProduct = new MDPModelChecker(this);
 		mcProduct.inheritSettings(this);
-		probsProduct = StateValues.createFromDoubleArray(mcProduct.computeReachProbs((MDP) modelProduct, acceptingMECs, false).soln, modelProduct);
+		probsProduct = StateValues.createFromDoubleArray(mcProduct.computeReachProbs((MDP) modelProduct, acc, false).soln, modelProduct);
 
 		// Subtract from 1 if we're model checking a negated formula for regular Pmin
 		if (minMax.isMin()) {

prism/src/prism/DRA.java

@@ -198,7 +198,7 @@ public class DRA<Symbol>
 
 	/**
 	 * Is this Rabin automaton actually a Buchi automaton? This check is done syntactically:
-	 * it returns true if L_i is empty for any acceptance paairs (L_i,K_i).
+	 * it returns true if L_i is empty for any acceptance pairs (L_i,K_i).
 	 */
 	public boolean isDBA()
 	{
@@ -210,6 +210,32 @@ public class DRA<Symbol>
 		return true;
 	}
 	
+	/**
+	 * Is this Rabin automaton actually a finite automaton? This check is done syntactically:
+	 * it returns true if L_i is empty for any acceptance pairs (L_i,K_i)
+	 * and every transition from a K_i state goes to another K_i state.
+	 */
+	public boolean isDFA()
+	{
+		if (!isDBA())
+			return false;
+		// Compute union of all K_i sets
+		BitSet acc = new BitSet();
+		int n = getNumAcceptancePairs();
+		for (int i = 0; i < n; i++) {
+			acc.or(getAcceptanceK(i));
+		}
+		// Check if every transition from a K_i state goes to another K_i state.
+		for (int i = acc.nextSetBit(0); i >= 0; i = acc.nextSetBit(i + 1)) {
+			int m = getNumEdges(i);
+			for (int j = 0; j < m; j++) {
+				if (!acc.get(getEdgeDest(i, j)))
+						return false;
+			}
+		}
+		return true;
+	}
+	
 	/**
 	 * Print DRA in DOT format to an output stream.
 	 */

prism/src/prism/NondetModelChecker.java

@@ -1512,9 +1512,17 @@ public class NondetModelChecker extends NonProbModelChecker
 			out.close();
 		}
 
-		// Find accepting MECs + compute reachability probabilities
-		mainLog.println("\nFinding accepting end components...");
-		JDDNode acc = mcLtl.findAcceptingECStatesForRabin(dra, modelProduct, draDDRowVars, draDDColVars, fairness);
+		// Find accepting states + compute reachability probabilities
+		JDDNode acc = null;
+		if (dra.isDFA()) {
+			// For a DFA, just collect the accept states
+			mainLog.println("\nSkipping end component detection since DRA is a DFA...");
+			acc = mcLtl.findTargetStatesForRabin(dra, modelProduct, draDDRowVars, draDDColVars);
+		} else {
+			// Usually, we have to detect end components in the product
+			mainLog.println("\nFinding accepting end components...");
+			acc = mcLtl.findAcceptingECStatesForRabin(dra, modelProduct, draDDRowVars, draDDColVars, fairness);
+		}
 		mainLog.println("\nComputing reachability probabilities...");
 		mcProduct = new NondetModelChecker(prism, modelProduct, null);
 		probsProduct = mcProduct.checkProbUntil(modelProduct.getReach(), acc, qual, min && fairness);

prism/src/prism/ProbModelChecker.java

@@ -615,9 +615,17 @@ public class ProbModelChecker extends NonProbModelChecker
 			out.close();
 		}
 
-		// Find accepting BSCCs + compute reachability probabilities
-		mainLog.println("\nFinding accepting BSCCs...");
-		JDDNode acc = mcLtl.findAcceptingBSCCsForRabin(dra, modelProduct, draDDRowVars, draDDColVars);
+		// Find accepting states + compute reachability probabilities
+		JDDNode acc = null;
+		if (dra.isDFA()) {
+			// For a DFA, just collect the accept states
+			mainLog.println("\nSkipping BSCC detection since DRA is a DFA...");
+			acc = mcLtl.findTargetStatesForRabin(dra, modelProduct, draDDRowVars, draDDColVars);
+		} else {
+			// Usually, we have to detect BSCCs in the product
+			mainLog.println("\nFinding accepting BSCCs...");
+			acc = mcLtl.findAcceptingBSCCsForRabin(dra, modelProduct, draDDRowVars, draDDColVars);
+		}
 		mainLog.println("\nComputing reachability probabilities...");
 		mcProduct = createNewModelChecker(prism, modelProduct, null);
 		probsProduct = mcProduct.checkProbUntil(modelProduct.getReach(), acc, qual);