Add some adversary generation for multi-objective value iteration (just exports one adv for each separated weighted objective).

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

prism/src/prism/MultiObjModelChecker.java

@@ -754,6 +754,8 @@ public class MultiObjModelChecker extends PrismComponent
 		double tolerance = settings.getDouble(PrismSettings.PRISM_PARETO_EPSILON);
 		int maxIters = settings.getInteger(PrismSettings.PRISM_MULTI_MAX_POINTS);
 
+		int exportAdvSetting = settings.getChoice(PrismSettings.PRISM_EXPORT_ADV);
+		
 		NativeIntArray adversary = new NativeIntArray((int) modelProduct.getNumStates());
 		int dimProb = targets.length;
 		int dimReward = rewards.size();
@@ -781,6 +783,12 @@ public class MultiObjModelChecker extends PrismComponent
 		NDSparseMatrix trans_matrix = NDSparseMatrix.BuildNDSparseMatrix(a, modelProduct.getODD(), modelProduct.getAllDDRowVars(),
 				modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars());
 
+		// If adversary generation is enabled, we build/store action info
+		if (settings.getChoice(PrismSettings.PRISM_EXPORT_ADV) != Prism.EXPORT_ADV_NONE) {
+			NDSparseMatrix.AddActionsToNDSparseMatrix(a, modelProduct.getTransActions(), modelProduct.getODD(), modelProduct.getAllDDRowVars(),
+					modelProduct.getAllDDColVars(), modelProduct.getAllDDNondetVars(), trans_matrix);
+		}
+		
 		//create double vectors for probabilistic objectives
 		for (int i = 0; i < dimProb; i++) {
 			probDoubleVectors[i] = new DoubleVector(targets[i], modelProduct.getAllDDRowVars(), modelProduct.getODD());
@@ -795,6 +803,9 @@ public class MultiObjModelChecker extends PrismComponent
 
 		JDD.Deref(a);
 
+		// Disable adversary generation (if it was switched on) for these initial computations
+		PrismNative.setExportAdv(Prism.EXPORT_ADV_NONE);
+		
 		for (int i = 0; i < dimProb; i++) {
 			double[] result;
 
@@ -806,7 +817,7 @@ public class MultiObjModelChecker extends PrismComponent
 						rewardStepBounds);
 			} else {
 				result = PrismSparse.NondetMultiObj(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(),
-						modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights,
+						modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, modelProduct.getSynchs(), probDoubleVectors, probStepBounds, rewSparseMatrices, weights,
 						rewardStepBounds);
 			}
 
@@ -833,7 +844,7 @@ public class MultiObjModelChecker extends PrismComponent
 						rewardStepBounds);
 			} else {
 				result = PrismSparse.NondetMultiObj(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(),
-						modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights,
+						modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, modelProduct.getSynchs(), probDoubleVectors, probStepBounds, rewSparseMatrices, weights,
 						rewardStepBounds);
 			}
 
@@ -846,6 +857,9 @@ public class MultiObjModelChecker extends PrismComponent
 			}
 		}
 
+		// Reinstate temporarily-disabled adversary generation setting
+		PrismNative.setExportAdv(exportAdvSetting);
+		
 		if (verbose)
 			mainLog.println("Points for initial tile: " + pointsForInitialTile);
 
@@ -869,6 +883,12 @@ public class MultiObjModelChecker extends PrismComponent
 				weights[i] = direction.getCoord(i);
 			}
 
+			// If adversary generation is enabled, we amend the filename so that multiple adversaries can be exported
+			String advFileName = settings.getString(PrismSettings.PRISM_EXPORT_ADV_FILENAME);
+			if (settings.getChoice(PrismSettings.PRISM_EXPORT_ADV) != Prism.EXPORT_ADV_NONE) {
+				PrismNative.setExportAdvFilename(PrismUtils.addCounterSuffixToFilename(advFileName, iters));
+			}
+			
 			double[] result;
 			if (prism.getMDPSolnMethod() == Prism.MDP_MULTI_GAUSSSEIDEL) {
 				result = PrismSparse.NondetMultiObjGS(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(),
@@ -876,7 +896,7 @@ public class MultiObjModelChecker extends PrismComponent
 						rewardStepBounds);
 			} else {
 				result = PrismSparse.NondetMultiObj(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(),
-						modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights,
+						modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, modelProduct.getSynchs(), probDoubleVectors, probStepBounds, rewSparseMatrices, weights,
 						rewardStepBounds);
 			}
 
@@ -1047,7 +1067,7 @@ public class MultiObjModelChecker extends PrismComponent
 			} else {
 				//System.out.println("Not doing GS");
 				result = PrismSparse.NondetMultiObj(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(),
-						modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, null, null, new NDSparseMatrix[] { rewSparseMatrices[0] },
+						modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, modelProduct.getSynchs(), null, null, new NDSparseMatrix[] { rewSparseMatrices[0] },
 						new double[] { 1.0 }, new int[] { rewardStepBounds[0] });
 			}
 			numberOfPoints++;
@@ -1085,7 +1105,7 @@ public class MultiObjModelChecker extends PrismComponent
 						rewardStepBounds);
 			} else {
 				result = PrismSparse.NondetMultiObj(modelProduct.getODD(), modelProduct.getAllDDRowVars(), modelProduct.getAllDDColVars(),
-						modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, probDoubleVectors, probStepBounds, rewSparseMatrices, weights,
+						modelProduct.getAllDDNondetVars(), false, st, adversary, trans_matrix, modelProduct.getSynchs(), probDoubleVectors, probStepBounds, rewSparseMatrices, weights,
 						rewardStepBounds);
 			}
 			numberOfPoints++;

prism/src/sparse/NDSparseMatrix.java

@@ -44,6 +44,8 @@ public class NDSparseMatrix
 
 	private static native long PS_BuildSubNDSparseMatrix(long trans, long odd, long rv, int nrv, long cv, int ncv, long ndv, int nndv, long rewards);
 
+	private static native void PS_AddActionsToNDSparseMatrix(long trans, long trans_actions, long odd, long rv, int nrv, long cv, int ncv, long ndv, int nndv, long ndsm);
+	
 	private static native void PS_DeleteNDSparseMatrix(long ptr_matrix);
 
 	static {
@@ -108,4 +110,9 @@ public class NDSparseMatrix
 			throw new PrismException(PrismSparse.getErrorMessage());
 		return new NDSparseMatrix(ptr);
 	}
+
+	public static void AddActionsToNDSparseMatrix(JDDNode trans, JDDNode transActions, ODDNode odd, JDDVars rows, JDDVars cols, JDDVars nondet, NDSparseMatrix ndsm) throws PrismException
+	{
+		PS_AddActionsToNDSparseMatrix(trans.ptr(), transActions.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(), ndsm.getPtr());
+	}
 }

prism/src/sparse/PS_NondetMultiObj.cc

@@ -62,6 +62,7 @@ JNIEXPORT jdoubleArray __jlongpointer JNICALL Java_sparse_PrismSparse_PS_1Nondet
  jlong __jlongpointer _start, // initial state(s)
  jlong _adversary,
  jlong __jlongpointer _ndsm, //pointer to trans sparse matrix
+ jobject synchs,
  jlongArray _yes_vec, //pointer to yes vector array
  jintArray _prob_step_bounds, //step bounds for probabilistic operators
  jlongArray  _ndsm_r, //pointer to reward sparse matrix array
@@ -98,8 +99,8 @@ JNIEXPORT jdoubleArray __jlongpointer JNICALL Java_sparse_PrismSparse_PS_1Nondet
 	int adv_j;
 	int *adv = NULL;
 	// action info
-	int *actions;
 	jstring *action_names_jstrings;
+	const char** action_names = NULL;
 	int num_actions;
 	// misc
 	int i, j, k, l1, h1, l2, h2, iters;
@@ -107,7 +108,6 @@ JNIEXPORT jdoubleArray __jlongpointer JNICALL Java_sparse_PrismSparse_PS_1Nondet
 	double d1, d2, kb, kbt;
 	double *pd1 = NULL, *pd2 = NULL;
 	bool done, weightedDone, first;
-	const char** action_names = NULL;
 	int num_yes = 0;
 	int start_index;
 	unsigned int *row_starts1, *predecessors;
@@ -158,6 +158,13 @@ JNIEXPORT jdoubleArray __jlongpointer JNICALL Java_sparse_PrismSparse_PS_1Nondet
 		// build sparse matrix
 		ndsm = (NDSparseMatrix *) jlong_to_NDSparseMatrix(_ndsm);
 		
+		// if needed, and if info is available, get action names
+		if (export_adv_enabled != EXPORT_ADV_NONE) {
+			if (synchs != NULL) {
+				get_string_array_from_java(env, synchs, action_names_jstrings, action_names, num_actions);
+			}
+		}
+	
 		// get number of transitions/choices
 		nnz = ndsm->nnz;
 		nc = ndsm->nc;
@@ -192,9 +199,6 @@ JNIEXPORT jdoubleArray __jlongpointer JNICALL Java_sparse_PrismSparse_PS_1Nondet
 			}
 		}
 		
-		// if needed, and if info is available, build a vector of action indices for the MDP
-		actions = NULL;
-		
 		// get vector for yes
 		yes_vec = new double *[lenProb];
 		for (int probi = 0; probi < lenProb; probi++) {
@@ -231,11 +235,7 @@ JNIEXPORT jdoubleArray __jlongpointer JNICALL Java_sparse_PrismSparse_PS_1Nondet
 		
 		// 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;
@@ -596,6 +596,47 @@ JNIEXPORT jdoubleArray __jlongpointer JNICALL Java_sparse_PrismSparse_PS_1Nondet
 			}
 		}
 		
+		// Traverse matrix to extract adversary
+		if (export_adv_enabled != EXPORT_ADV_NONE) {
+			// Do two passes: first to compute the number of transitions,
+			// the second to actually do the export
+			int num_trans = 0;
+			for (int pass = 1; pass <= 2; pass++) {
+				if (pass == 2) {
+					fprintf(fp_adv, "%d %d\n", n, num_trans);
+				}
+				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]) {
+							switch (pass) {
+							case 1:
+								num_trans += (h2-l2);
+								break;
+							case 2:
+								for (k = l2; k < h2; k++) {
+									switch (export_adv_enabled) {
+									case EXPORT_ADV_DTMC:
+										fprintf(fp_adv, "%d %d %g", i, cols[k], non_zeros[k]); break;
+									case EXPORT_ADV_MDP:
+										fprintf(fp_adv, "%d 0 %d %g", i, cols[k], non_zeros[k]); break;
+									}
+									if (ndsm->actions != NULL) fprintf(fp_adv, " %s", ndsm->actions[j]>0?action_names[ndsm->actions[j]-1]:"");
+									fprintf(fp_adv, "\n");
+								}
+							}
+						}
+					}
+				}
+			}
+		}
+	
 		// stop clocks
 		stop = util_cpu_time();
 		time_for_iters = (double)(stop - start2)/1000;
@@ -661,15 +702,12 @@ JNIEXPORT jdoubleArray __jlongpointer JNICALL Java_sparse_PrismSparse_PS_1Nondet
 			if (psoln[it]) delete[] psoln[it];
 		}
 	}
-	
 	if (psoln2) delete[] psoln2;
 	if (psoln) delete[] psoln;
-	    
-	if (actions != NULL) {
-		delete[] actions;
+	if (adv) delete[] adv;
+	if (action_names != NULL) {
 		release_string_array_from_java(env, action_names_jstrings, action_names, num_actions);
 	}
-	if (adv) delete[] adv;
 
 	return ret;
 }

prism/src/sparse/PrismSparse.cc

@@ -366,6 +366,39 @@ JNIEXPORT jlong __jlongpointer JNICALL Java_sparse_NDSparseMatrix_PS_1BuildSubND
 
 //------------------------------------------------------------------------------
 
+JNIEXPORT void JNICALL Java_sparse_NDSparseMatrix_PS_1AddActionsToNDSparseMatrix
+(JNIEnv *env, jclass cls,
+ jlong __jlongpointer t,    // trans
+ jlong __jlongpointer ta,    // trans action labels
+ jlong __jlongpointer od, // odd
+ jlong __jlongpointer rv, // row vars
+ jint num_rvars,
+ jlong __jlongpointer cv, // col vars
+ jint num_cvars,
+ jlong __jlongpointer ndv,  // nondet vars
+ jint num_ndvars,
+ jlong __jlongpointer nd    // sparse matrix
+ )
+{
+    DdNode *trans = jlong_to_DdNode(t); 			//trans/reward matrix
+	DdNode *trans_actions = jlong_to_DdNode(ta);	// trans action labels
+    ODDNode *odd = jlong_to_ODDNode(od);      // reachable states
+    DdNode **rvars = jlong_to_DdNode_array(rv);   // row vars
+    DdNode **cvars = jlong_to_DdNode_array(cv);   // col vars
+    DdNode **ndvars = jlong_to_DdNode_array(ndv); // nondet vars
+	NDSparseMatrix *ndsm = (NDSparseMatrix *) jlong_to_NDSparseMatrix(nd); // sparse matrix
+    
+	jstring *action_names_jstrings;
+	const char** action_names = NULL;
+	int num_actions;
+	
+	if (trans_actions != NULL) {
+		build_nd_action_vector(ddman, trans, trans_actions, ndsm, rvars, cvars, num_rvars, ndvars, num_ndvars, odd);
+	}
+}
+
+//------------------------------------------------------------------------------
+
 JNIEXPORT void __jlongpointer JNICALL Java_sparse_NDSparseMatrix_PS_1DeleteNDSparseMatrix
 (JNIEnv *env, jclass cls,
  jlong __jlongpointer _ndsm)

prism/src/sparse/PrismSparse.java

@@ -238,8 +238,8 @@ public class PrismSparse
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 	
-	private static native double[] PS_NondetMultiObj(long odd, long rv, int nrv, long cv, int ncv, long ndv, int nndv, boolean minmax, long start, long ptr_adversary, long ptr_TransSparseMatrix, long[] ptr_yes_vec, int[] probStepBounds, long[] ptr_RewSparseMatrix, double[] rewardWeights, int[] rewardStepBounds);
-	public static double[] NondetMultiObj(ODDNode odd, JDDVars rows, JDDVars cols, JDDVars nondet, boolean minmax, JDDNode start, NativeIntArray adversary, NDSparseMatrix transSparseMatrix, DoubleVector[] yes_vec, int[] probStepBounds, NDSparseMatrix[] rewSparseMatrix, double[] rewardWeights, int[] rewardStepBounds) throws PrismException
+	private static native double[] PS_NondetMultiObj(long odd, long rv, int nrv, long cv, int ncv, long ndv, int nndv, boolean minmax, long start, long ptr_adversary, long ptr_TransSparseMatrix, List<String> synchs, long[] ptr_yes_vec, int[] probStepBounds, long[] ptr_RewSparseMatrix, double[] rewardWeights, int[] rewardStepBounds);
+	public static double[] NondetMultiObj(ODDNode odd, JDDVars rows, JDDVars cols, JDDVars nondet, boolean minmax, JDDNode start, NativeIntArray adversary, NDSparseMatrix transSparseMatrix, List<String> synchs, DoubleVector[] yes_vec, int[] probStepBounds, NDSparseMatrix[] rewSparseMatrix, double[] rewardWeights, int[] rewardStepBounds) throws PrismException
 	{
 		long[] ptr_ndsp_r = null;
 		if (rewSparseMatrix != null) {
@@ -255,7 +255,7 @@ public class PrismSparse
 				ptr_yes_vec[i] = (yes_vec[i]!=null) ? yes_vec[i].getPtr() : 0;
 		}
 		
-		double[] ret = PS_NondetMultiObj(odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(), minmax, start.ptr(), adversary.getPtr(), transSparseMatrix.getPtr(), ptr_yes_vec, probStepBounds, ptr_ndsp_r, rewardWeights, rewardStepBounds);
+		double[] ret = PS_NondetMultiObj(odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(), minmax, start.ptr(), adversary.getPtr(), transSparseMatrix.getPtr(), synchs, ptr_yes_vec, probStepBounds, ptr_ndsp_r, rewardWeights, rewardStepBounds);
 		if (ret == null)
 			throw new PrismException(getErrorMessage());
 		else