diff --git a/prism/src/prism/MultiObjModelChecker.java b/prism/src/prism/MultiObjModelChecker.java index 34ce1296..f1efe7a7 100644 --- a/prism/src/prism/MultiObjModelChecker.java +++ b/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++; diff --git a/prism/src/sparse/NDSparseMatrix.java b/prism/src/sparse/NDSparseMatrix.java index 62b8d14e..7924c639 100644 --- a/prism/src/sparse/NDSparseMatrix.java +++ b/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()); + } } diff --git a/prism/src/sparse/PS_NondetMultiObj.cc b/prism/src/sparse/PS_NondetMultiObj.cc index c0ff3d87..efeeac79 100644 --- a/prism/src/sparse/PS_NondetMultiObj.cc +++ b/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; } diff --git a/prism/src/sparse/PrismSparse.cc b/prism/src/sparse/PrismSparse.cc index 15bbc6a8..83ef00d6 100644 --- a/prism/src/sparse/PrismSparse.cc +++ b/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) diff --git a/prism/src/sparse/PrismSparse.java b/prism/src/sparse/PrismSparse.java index 7d8f9c02..3a57b3fa 100644 --- a/prism/src/sparse/PrismSparse.java +++ b/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 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 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