symbolic LTL model checking: perform DA product constructions from the statesOfInterest

In general, this should provide a significant performance benefit, as
the reachable state space of the product model becomes smaller in the
usual cases (i.e., where we are only interested in the results from
the initial states or for some filter).


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

prism/src/prism/MultiObjModelChecker.java

@@ -103,7 +103,7 @@ public class MultiObjModelChecker extends PrismComponent
 		// Build product of MDP and automaton
 		mainLog.println("\nConstructing MDP-DRA product...");
 
-		NondetModel modelNew = mcLtl.constructProductMDP(dra[i], model, labelDDs, draDDRowVars, draDDColVars, false, i == 0 ? ddStateIndex : model.getStart());
+		NondetModel modelNew = mcLtl.constructProductMDP(dra[i], model, labelDDs, draDDRowVars, draDDColVars, (i == 0 ? ddStateIndex : model.getStart()).copy());
 
 		modelNew.printTransInfo(mainLog, prism.getExtraDDInfo());
 		// Deref label BDDs

prism/src/prism/NondetModelChecker.java

@@ -1200,9 +1200,6 @@ public class NondetModelChecker extends NonProbModelChecker
 		int i;
 		long l;
 
-		// currently, ignore statesOfInterest
-		JDD.Deref(statesOfInterest);
-
 		// For min probabilities, need to negate the formula
 		// (But check fairness setting since this may affect min/max)
 		// (add parentheses to allow re-parsing if required)
@@ -1225,14 +1222,19 @@ public class NondetModelChecker extends NonProbModelChecker
 				AcceptanceType.GENERALIZED_RABIN,
 				AcceptanceType.REACH
 		};
+		try {
 			da = mcLtl.constructDAForLTLFormula(this, model, expr, labelDDs, allowedAcceptance);
+		} catch (Exception e) {
+			JDD.Deref(statesOfInterest);
+			throw e;
+		}
 
 		// Build product of MDP and automaton
 		l = System.currentTimeMillis();
 		mainLog.println("\nConstructing MDP-"+da.getAutomataType()+" product...");
 		daDDRowVars = new JDDVars();
 		daDDColVars = new JDDVars();
-		modelProduct = mcLtl.constructProductMDP(da, model, labelDDs, daDDRowVars, daDDColVars);
+		modelProduct = mcLtl.constructProductMDP(da, model, labelDDs, daDDRowVars, daDDColVars, statesOfInterest);
 		l = System.currentTimeMillis() - l;
 		mainLog.println("Time for product construction: " + l / 1000.0 + " seconds.");
 		mainLog.println();
@@ -1458,9 +1460,6 @@ public class NondetModelChecker extends NonProbModelChecker
 		int i;
 		long l;
 
-		// currently, ignore statesOfInterest
-		JDD.Deref(statesOfInterest);
-
 		if (Expression.containsTemporalTimeBounds(expr)) {
 			if (model.getModelType().continuousTime()) {
 				throw new PrismException("DA construction for time-bounded operators not supported for " + model.getModelType()+".");
@@ -1518,7 +1517,7 @@ public class NondetModelChecker extends NonProbModelChecker
 		daDDRowVars = new JDDVars();
 		daDDColVars = new JDDVars();
 		l = System.currentTimeMillis();
-		modelProduct = mcLtl.constructProductMDP(da, model, labelDDs, daDDRowVars, daDDColVars);
+		modelProduct = mcLtl.constructProductMDP(da, model, labelDDs, daDDRowVars, daDDColVars, statesOfInterest);
 		l = System.currentTimeMillis() - l;
 		mainLog.println("Time for product construction: " + l / 1000.0 + " seconds.");
 		mainLog.println();

prism/src/prism/ProbModelChecker.java

@@ -552,9 +552,6 @@ public class ProbModelChecker extends NonProbModelChecker
 		JDDVars daDDRowVars, daDDColVars;
 		int i;
 
-		// TODO: take statesOfInterest into account for product construction
-		JDD.Deref(statesOfInterest);
-
 		AcceptanceType[] allowedAcceptance = {
 				AcceptanceType.REACH,
 				AcceptanceType.BUCHI,
@@ -571,7 +568,7 @@ public class ProbModelChecker extends NonProbModelChecker
 		mainLog.println("\nConstructing MC-"+da.getAutomataType()+" product...");
 		daDDRowVars = new JDDVars();
 		daDDColVars = new JDDVars();
-		modelProduct = mcLtl.constructProductMC(da, model, labelDDs, daDDRowVars, daDDColVars);
+		modelProduct = mcLtl.constructProductMC(da, model, labelDDs, daDDRowVars, daDDColVars, statesOfInterest);
 		mainLog.println();
 		modelProduct.printTransInfo(mainLog, prism.getExtraDDInfo());
 		// Output product, if required
@@ -968,9 +965,6 @@ public class ProbModelChecker extends NonProbModelChecker
 		int i;
 		long l;
 
-		// currently, ignore statesOfInterest
-		JDD.Deref(statesOfInterest);
-
 		if (Expression.containsTemporalTimeBounds(expr)) {
 			if (model.getModelType().continuousTime()) {
 				throw new PrismException("DA construction for time-bounded operators not supported for " + model.getModelType()+".");
@@ -1020,7 +1014,7 @@ public class ProbModelChecker extends NonProbModelChecker
 		daDDRowVars = new JDDVars();
 		daDDColVars = new JDDVars();
 		l = System.currentTimeMillis();
-		modelProduct = mcLtl.constructProductMC(da, model, labelDDs, daDDRowVars, daDDColVars);
+		modelProduct = mcLtl.constructProductMC(da, model, labelDDs, daDDRowVars, daDDColVars, statesOfInterest);
 		l = System.currentTimeMillis() - l;
 		mainLog.println("Time for product construction: " + l / 1000.0 + " seconds.");
 		mainLog.println();