Revert recent DFA optimizations to allow for acceptance type refactoring. Functionality will be later readded using AcceptanceReach. [Joachim Klein]

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

prism/src/explicit/DTMCModelChecker.java

@@ -105,21 +105,13 @@ public class DTMCModelChecker extends ProbModelChecker
 		int invMap[] = pair.second;
 		mainLog.print("\n" + modelProduct.infoStringTable());
 
-		// 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
+		// Find accepting BSCCs + compute reachability probabilities
 		mainLog.println("\nFinding accepting BSCCs...");
-			acc = mcLtl.findAcceptingBSCCsForRabin(dra, modelProduct, invMap);
-		}
+		BitSet acceptingBSCCs = mcLtl.findAcceptingBSCCsForRabin(dra, modelProduct, invMap);
 		mainLog.println("\nComputing reachability probabilities...");
 		mcProduct = new DTMCModelChecker(this);
 		mcProduct.inheritSettings(this);
-		probsProduct = StateValues.createFromDoubleArray(mcProduct.computeReachProbs((DTMC) modelProduct, acc).soln, modelProduct);
+		probsProduct = StateValues.createFromDoubleArray(mcProduct.computeReachProbs((DTMC) modelProduct, acceptingBSCCs).soln, modelProduct);
 
 		// Mapping probabilities in the original model
 		double[] probsProductDbl = probsProduct.getDoubleArray();

prism/src/explicit/LTLModelChecker.java

@@ -314,33 +314,6 @@ 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,21 +112,13 @@ public class MDPModelChecker extends ProbModelChecker
 		modelProduct = pair.first;
 		int invMap[] = pair.second;
 
-		// 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
+		// Find accepting MECs + compute reachability probabilities
 		mainLog.println("\nFinding accepting MECs...");
-			acc = mcLtl.findAcceptingECStatesForRabin(dra, modelProduct, invMap);
-		}
+		BitSet acceptingMECs = mcLtl.findAcceptingECStatesForRabin(dra, modelProduct, invMap);
 		mainLog.println("\nComputing reachability probabilities...");
 		mcProduct = new MDPModelChecker(this);
 		mcProduct.inheritSettings(this);
-		probsProduct = StateValues.createFromDoubleArray(mcProduct.computeReachProbs((MDP) modelProduct, acc, false).soln, modelProduct);
+		probsProduct = StateValues.createFromDoubleArray(mcProduct.computeReachProbs((MDP) modelProduct, acceptingMECs, 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

@@ -196,49 +196,6 @@ public class DRA<Symbol>
 		return acceptanceK.get(i);
 	}
 
-	/**
-	 * Is this Rabin automaton actually a Buchi automaton? This check is done syntactically:
-	 * it returns true if L_i is empty for any acceptance pairs (L_i,K_i).
-	 */
-	public boolean isDBA()
-	{
-		int n = getNumAcceptancePairs();
-		for (int i = 0; i < n; i++) {
-			if (!getAcceptanceL(i).isEmpty())
-				return false;
-		}
-		return true;
-	}
-	
-	/**
-	 * Is this Rabin automaton actually a finite automaton? This check is done syntactically:
-	 * 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 boolean isDFA()
-	{
-		// 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));
-		}
-		// Make sure there are no L_i states in any K_j states
-		for (int i = 0; i < n; i++) {
-			if (acc.intersects(getAcceptanceL(i)))
-				return false;
-		}
-		// 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/LTLModelChecker.java

@@ -664,27 +664,6 @@ public class LTLModelChecker extends PrismComponent
 		return statesKi;
 	}
 
-	/**
-	 * 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 storing the Rabin acceptance condition
-	 * @param model The model
-	 * @param draDDRowVars BDD row variables for the DRA part of the model
-	 * @param draDDColVars BDD column variables for the DRA part of the model
-	 * @return
-	 */
-	public JDDNode findTargetStatesForRabin(DRA<BitSet> dra, Model model, JDDVars draDDRowVars, JDDVars draDDColVars)
-	{
-		JDDNode acceptingStates = JDD.Constant(0);
-		for (int i = 0; i < dra.getNumAcceptancePairs(); i++) {
-			JDDNode tmpK = buildKStatesForRabinPair(draDDRowVars, dra, i);
-			acceptingStates = JDD.Or(acceptingStates, tmpK);
-		}
-		JDD.Ref(model.getReach());
-		acceptingStates = JDD.And(model.getReach(), acceptingStates);
-		return acceptingStates;
-	}
-	
 	/**
 	 * Find the set of accepting BSCCs in a model wrt a Rabin acceptance condition.
 	 * @param dra The DRA storing the Rabin acceptance condition

prism/src/prism/NondetModelChecker.java

@@ -1013,17 +1013,9 @@ public class NondetModelChecker extends NonProbModelChecker
 			out.close();
 		}
 
-		// 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
+		// Find accepting MECs + compute reachability probabilities
 		mainLog.println("\nFinding accepting end components...");
-			acc = mcLtl.findAcceptingECStatesForRabin(dra, modelProduct, draDDRowVars, draDDColVars, fairness);
-		}
+		JDDNode 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

@@ -552,17 +552,9 @@ public class ProbModelChecker extends NonProbModelChecker
 			out.close();
 		}
 
-		// 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
+		// Find accepting BSCCs + compute reachability probabilities
 		mainLog.println("\nFinding accepting BSCCs...");
-			acc = mcLtl.findAcceptingBSCCsForRabin(dra, modelProduct, draDDRowVars, draDDColVars);
-		}
+		JDDNode acc = mcLtl.findAcceptingBSCCsForRabin(dra, modelProduct, draDDRowVars, draDDColVars);
 		mainLog.println("\nComputing reachability probabilities...");
 		mcProduct = createNewModelChecker(prism, modelProduct, null);
 		probsProduct = mcProduct.checkProbUntil(modelProduct.getReach(), acc, qual);