Fixed adversary generation to avoid end component problems and disabled Prob1 automatically.

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

prism/src/prism/NondetModelChecker.java

@@ -54,7 +54,12 @@ public class NondetModelChecker extends NonProbModelChecker
 	// Options (in addition to those inherited from StateModelChecker):
 
 	// Use 0,1 precomputation algorithms?
+	// if 'precomp' is false, this disables all (non-essential) use of prob0/prob1
+	// if 'precomp' is true, the values of prob0/prob1 determine what is used
+	// (currently prob0/prob are not under user control)
 	protected boolean precomp;
+	protected boolean prob0;
+	protected boolean prob1;
 	// Use fairness?
 	protected boolean fairness;
 
@@ -71,15 +76,24 @@ public class NondetModelChecker extends NonProbModelChecker
 		nondetMask = model.getNondetMask();
 		allDDNondetVars = model.getAllDDNondetVars();
 		
-		// Display warning for some option combinations
-		if (prism.getExportAdv() != Prism.EXPORT_ADV_NONE && engine != Prism.SPARSE) {
-			mainLog.println("\nWarning: Adversary generation is only implemented for the sparse engine");
-		}
-		
-		// Inherit some options from parent Prism object.
-		// Store locally and/or pass onto engines/native code.
+		// Inherit some options from parent Prism object and store locally.
 		precomp = prism.getPrecomp();
+		prob0 = true;
+		prob1 = true;
 		fairness = prism.getFairness();
+		
+		// Display warning and/or make changes for some option combinations
+		if (prism.getExportAdv() != Prism.EXPORT_ADV_NONE) {
+			if (engine != Prism.SPARSE) {
+				mainLog.println("\nWarning: Adversary generation is only implemented for the sparse engine");
+			}
+			if (precomp && prob1) {
+				mainLog.println("\nWarning: Disabling Prob1 since this is needed for adversary generation");
+				prob1 = false;
+			}
+		}
+		
+		// Pass some options onto engines/native code.
 		PrismNative.setExportAdv(prism.getExportAdv());
 		PrismNative.setExportAdvFilename(prism.getExportAdvFilename());
 		switch (engine) {
@@ -185,7 +199,7 @@ public class NondetModelChecker extends NonProbModelChecker
 		}
 
 		// Compute probabilities
-		boolean qual = pb != null && ((p == 0) || (p == 1)) && precomp;
+		boolean qual = pb != null && ((p == 0) || (p == 1)) && precomp && prob0 && prob1;
 		probs = checkProbPathFormula(expr.getExpression(), qual, min);
 
 		// Print out probabilities
@@ -786,7 +800,7 @@ public class NondetModelChecker extends NonProbModelChecker
 			// no
 			if (yes.equals(reach)) {
 				no = JDD.Constant(0);
-			} else if (precomp) {
+			} else if (precomp && prob0) {
 				if (min) {
 					// "min prob = 0" equates to "there exists a prob 0"
 					no = PrismMTBDD.Prob0E(tr01, reach, nondetMask, allDDRowVars, allDDColVars, allDDNondetVars, b1,
@@ -979,21 +993,39 @@ public class NondetModelChecker extends NonProbModelChecker
 			no = JDD.And(reach, JDD.Not(b2));
 			maybe = JDD.Constant(0);
 		} else {
+			// no
 			// if precomputation enabled
-			if (precomp) {
+			if (precomp && prob0) {
 				// min
 				if (min) {
 					// no: "min prob = 0" equates to "there exists an adversary prob equals 0"
-					no = PrismMTBDD
-							.Prob0E(tr01, reach, nondetMask, allDDRowVars, allDDColVars, allDDNondetVars, b1, b2);
+					no = PrismMTBDD.Prob0E(tr01, reach, nondetMask, allDDRowVars, allDDColVars, allDDNondetVars, b1, b2);
+				}
+				// max
+				else {
+					// no: "max prob = 0" equates to "for all adversaries prob equals 0"
+					no = PrismMTBDD.Prob0A(tr01, reach, allDDRowVars, allDDColVars, allDDNondetVars, b1, b2);
+				}
+			}
+			// if precomputation not enabled
+			else {
+				// no
+				JDD.Ref(reach);
+				JDD.Ref(b1);
+				JDD.Ref(b2);
+				no = JDD.And(reach, JDD.Not(JDD.Or(b1, b2)));
+			}
+			// yes
+			// if precomputation enabled (need both prob0/prob1 to be enabled to do prob1)
+			if (precomp && prob0 && prob1) {
+				// min
+				if (min) {
 					// yes: "min prob = 1" equates to "for all adversaries prob equals 1"
 					yes = PrismMTBDD.Prob1A(tr01, reach, nondetMask, allDDRowVars, allDDColVars, allDDNondetVars, no,
 							b2);
 				}
 				// max
 				else {
-					// no: "max prob = 0" equates to "for all adversaries prob equals 0"
-					no = PrismMTBDD.Prob0A(tr01, reach, allDDRowVars, allDDColVars, allDDNondetVars, b1, b2);
 					// yes: "max prob = 1" equates to "there exists an adversary prob equals 1"
 					yes = PrismMTBDD.Prob1E(tr01, reach, allDDRowVars, allDDColVars, allDDNondetVars, b1, b2, no);
 				}
@@ -1003,11 +1035,6 @@ public class NondetModelChecker extends NonProbModelChecker
 				// yes
 				JDD.Ref(b2);
 				yes = b2;
-				// no
-				JDD.Ref(reach);
-				JDD.Ref(b1);
-				JDD.Ref(b2);
-				no = JDD.And(reach, JDD.Not(JDD.Or(b1, b2)));
 			}
 			// maybe
 			JDD.Ref(reach);

prism/src/sparse/PS_NondetUntil.cc

@@ -87,6 +87,8 @@ jboolean min				// min or max probabilities (true = min, false = max)
 	bool adv_loop = false;
 	FILE *fp_adv = NULL;
 	int adv_j, adv_l2, adv_h2;
+	int *adv = NULL;
+	// action info
 	int *actions;
 	jstring *action_names_jstrings;
 	const char** action_names;
@@ -171,6 +173,19 @@ jboolean min				// min or max probabilities (true = min, false = max)
 	kbt += 2*kb;
 	PS_PrintMemoryToMainLog(env, "[2 x ", kb, "]\n");
 	
+	// if required, create storage for adversary and initialise
+	if (export_adv_enabled != EXPORT_ADV_NONE) {
+		PS_PrintToMainLog(env, "Allocating adversary vector... ");
+		adv = new int[n];
+		kb = n*sizeof(int)/1024.0;
+		kbt += kb;
+		PS_PrintMemoryToMainLog(env, "[", kb, "]\n");
+		// Initialise all entries to -1 ("don't know")
+		for (i = 0; i < n; i++) {
+			adv[i] = -1;
+		}
+	}
+	
 	// print total memory usage
 	PS_PrintMemoryToMainLog(env, "TOTAL: [", kbt, "]\n");
 	
@@ -201,22 +216,22 @@ jboolean min				// min or max probabilities (true = min, false = max)
 		}
 	}
 	
-	while ((!done && iters < max_iters) || adv_loop) {
+	// store local copies of stuff
+	double *non_zeros = ndsm->non_zeros;
+	unsigned char *row_counts = ndsm->row_counts;
+	int *row_starts = (int *)ndsm->row_counts;
+	unsigned char *choice_counts = ndsm->choice_counts;
+	int *choice_starts = (int *)ndsm->choice_counts;
+	bool use_counts = ndsm->use_counts;
+	unsigned int *cols = ndsm->cols;
+		
+	while (!done && iters < max_iters) {
 		
 		iters++;
 		
 //		PS_PrintToMainLog(env, "iter %d\n", iters);
 //		start3 = util_cpu_time();
 		
-		// store local copies of stuff
-		double *non_zeros = ndsm->non_zeros;
-		unsigned char *row_counts = ndsm->row_counts;
-		int *row_starts = (int *)ndsm->row_counts;
-		unsigned char *choice_counts = ndsm->choice_counts;
-		int *choice_starts = (int *)ndsm->choice_counts;
-		bool use_counts = ndsm->use_counts;
-		unsigned int *cols = ndsm->cols;
-		
 		// do matrix multiplication and min/max
 		h1 = h2 = 0;
 		for (i = 0; i < n; i++) {
@@ -233,20 +248,18 @@ jboolean min				// min or max probabilities (true = min, false = max)
 				}
 				if (first || (min&&(d2<d1)) || (!min&&(d2>d1))) {
 					d1 = d2;
-					if (adv_loop) { adv_j = j; adv_l2 = l2; adv_h2 = h2; }
+					// if adversary generation is enabled, remember new (strictly) better choices
+					if (export_adv_enabled != EXPORT_ADV_NONE) {
+						if (adv[i] == -1 || (min&&(d1<soln[i])) || (!min&&(d1>soln[i]))) {
+							adv[i] = j;
+						}
+					}
 				}
 				first = false;
 			}
 			// set vector element
 			// (if no choices, use value of yes)
 			soln2[i] = (h1 > l1) ? d1 : yes_vec[i];
-			// store adversary info (if required)
-			if (adv_loop) if (h1 > l1)
-				for (k = adv_l2; k < adv_h2; k++) {
-					fprintf(fp_adv, "%d %d %g", i, cols[k], non_zeros[k]);
-					if (actions != NULL) fprintf(fp_adv, " %s", actions[adv_j]>0?action_names[actions[adv_j]-1]:"");
-					fprintf(fp_adv, "\n");
-				}
 		}
 		
 		// check convergence
@@ -279,12 +292,31 @@ jboolean min				// min or max probabilities (true = min, false = max)
 		soln = soln2;
 		soln2 = tmpsoln;
 		
-		// if we're done, but adversary generation is required, go round once more
-		if (done && export_adv_enabled != EXPORT_ADV_NONE) adv_loop = !adv_loop;
-		
 //		PS_PrintToMainLog(env, "%.2f %.2f sec\n", ((double)(util_cpu_time() - start3)/1000), ((double)(util_cpu_time() - start2)/1000)/iters);
 	}
 	
+	// Traverse matrix to extract adversary
+	if (export_adv_enabled != EXPORT_ADV_NONE) {
+		h1 = h2 = 0;
+		for (i = 0; i < n; i++) {
+			if (!use_counts) { l1 = row_starts[i]; h1 = row_starts[i+1]; }
+			else { l1 = h1; h1 += row_counts[i]; }
+			// Have to loop through all choices (to compute offsets)
+			for (j = l1; j < h1; j++) {
+				if (!use_counts) { l2 = choice_starts[j]; h2 = choice_starts[j+1]; }
+				else { l2 = h2; h2 += choice_counts[j]; }
+				// But only output a choice if it is in the adversary
+				if (j == adv[i]) {
+					for (k = l2; k < h2; k++) {
+						fprintf(fp_adv, "%d %d %g", i, cols[k], non_zeros[k]);
+						if (actions != NULL) fprintf(fp_adv, " %s", actions[j]>0?action_names[actions[j]-1]:"");
+						fprintf(fp_adv, "\n");
+					}
+				}
+			}
+		}
+	}
+	
 	// stop clocks
 	stop = util_cpu_time();
 	time_for_iters = (double)(stop - start2)/1000;
@@ -314,6 +346,7 @@ jboolean min				// min or max probabilities (true = min, false = max)
 	if (ndsm) delete ndsm;
 	if (yes_vec) delete[] yes_vec;
 	if (soln2) delete[] soln2;
+	if (adv) delete[] adv;
 	if (actions != NULL) {
 		delete[] actions;
 		release_string_array_from_java(env, action_names_jstrings, action_names, num_actions);