From 7b79848f3280054cf9282e54b4c1d5955f6b29fa Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 4 May 2010 16:48:07 +0000 Subject: [PATCH] Updated (sparse engine) adversary generation for reachability rewards to use new switches, actions, etc. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1877 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/include/PrismSparse.h | 4 +- prism/src/prism/NondetModelChecker.java | 6 +- prism/src/sparse/PS_NondetReachReward.cc | 158 +++++++++++++++++------ prism/src/sparse/PrismSparse.java | 6 +- 4 files changed, 125 insertions(+), 49 deletions(-) diff --git a/prism/include/PrismSparse.h b/prism/include/PrismSparse.h index 1083df4f..efeee3f0 100644 --- a/prism/include/PrismSparse.h +++ b/prism/include/PrismSparse.h @@ -178,10 +178,10 @@ JNIEXPORT jlong JNICALL Java_sparse_PrismSparse_PS_1NondetInstReward /* * Class: sparse_PrismSparse * Method: PS_NondetReachReward - * Signature: (JJJJJIJIJIJJJZ)J + * Signature: (JJLjava/util/List;JJJJIJIJIJJJZ)J */ JNIEXPORT jlong JNICALL Java_sparse_PrismSparse_PS_1NondetReachReward - (JNIEnv *, jclass, jlong, jlong, jlong, jlong, jlong, jint, jlong, jint, jlong, jint, jlong, jlong, jlong, jboolean); + (JNIEnv *, jclass, jlong, jlong, jobject, jlong, jlong, jlong, jlong, jint, jlong, jint, jlong, jint, jlong, jlong, jlong, jboolean); /* * Class: sparse_PrismSparse diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index f4ef85c1..fadf82f6 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -727,7 +727,7 @@ public class NondetModelChecker extends NonProbModelChecker // compute rewards try { - rewards = computeReachRewards(trans, trans01, stateRewards, transRewards, b, min); + rewards = computeReachRewards(trans, transActions, trans01, stateRewards, transRewards, b, min); } catch (PrismException e) { JDD.Deref(b); throw e; @@ -1138,7 +1138,7 @@ public class NondetModelChecker extends NonProbModelChecker // compute rewards for reach reward - protected StateValues computeReachRewards(JDDNode tr, JDDNode tr01, JDDNode sr, JDDNode trr, JDDNode b, boolean min) + protected StateValues computeReachRewards(JDDNode tr, JDDNode tra, JDDNode tr01, JDDNode sr, JDDNode trr, JDDNode b, boolean min) throws PrismException { JDDNode inf, maybe, prob1, no; @@ -1240,7 +1240,7 @@ public class NondetModelChecker extends NonProbModelChecker rewards = new StateValuesMTBDD(rewardsMTBDD, model); break; case Prism.SPARSE: - rewardsDV = PrismSparse.NondetReachReward(tr, sr, trr, odd, allDDRowVars, allDDColVars, + rewardsDV = PrismSparse.NondetReachReward(tr, tra, model.getSynchs(), sr, trr, odd, allDDRowVars, allDDColVars, allDDNondetVars, b, inf, maybe, min); rewards = new StateValuesDV(rewardsDV, model); break; diff --git a/prism/src/sparse/PS_NondetReachReward.cc b/prism/src/sparse/PS_NondetReachReward.cc index 0d3df77a..9314f291 100644 --- a/prism/src/sparse/PS_NondetReachReward.cc +++ b/prism/src/sparse/PS_NondetReachReward.cc @@ -33,6 +33,8 @@ #include #include #include "sparse.h" +#include "prism.h" +#include "PrismNativeGlob.h" #include "PrismSparseGlob.h" #include "jnipointer.h" #include @@ -43,7 +45,9 @@ JNIEXPORT jlong __jlongpointer JNICALL Java_sparse_PrismSparse_PS_1NondetReachRe ( JNIEnv *env, jclass cls, -jlong __jlongpointer t, // trans matrix +jlong __jlongpointer t, // trans matrix +jlong __jlongpointer ta, // trans action labels +jobject synchs, jlong __jlongpointer sr, // state rewards jlong __jlongpointer trr, // transition rewards jlong __jlongpointer od, // odd @@ -53,26 +57,27 @@ jlong __jlongpointer cv, // col vars jint num_cvars, jlong __jlongpointer ndv, // nondet vars jint num_ndvars, -jlong __jlongpointer g, // 'goal' states +jlong __jlongpointer g, // 'goal' states jlong __jlongpointer in, // 'inf' states -jlong __jlongpointer m, // 'maybe' states -jboolean min // min or max probabilities (true = min, false = max) +jlong __jlongpointer m, // 'maybe' states +jboolean min // min or max probabilities (true = min, false = max) ) { // cast function parameters - DdNode *trans = jlong_to_DdNode(t); // trans matrix + DdNode *trans = jlong_to_DdNode(t); // trans matrix + DdNode *trans_actions = jlong_to_DdNode(ta); // trans action labels DdNode *state_rewards = jlong_to_DdNode(sr); // state rewards DdNode *trans_rewards = jlong_to_DdNode(trr); // transition rewards - ODDNode *odd = jlong_to_ODDNode(od); // reachable states + 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 - DdNode *goal = jlong_to_DdNode(g); // 'goal' states - DdNode *inf = jlong_to_DdNode(in); // 'inf' states - DdNode *maybe = jlong_to_DdNode(m); // 'maybe' states + DdNode *goal = jlong_to_DdNode(g); // 'goal' states + DdNode *inf = jlong_to_DdNode(in); // 'inf' states + DdNode *maybe = jlong_to_DdNode(m); // 'maybe' states // mtbdds - DdNode *a; + DdNode *a, *tmp = NULL; // model stats int n, nc, nc_r; long nnz, nnz_r; @@ -84,9 +89,16 @@ jboolean min // min or max probabilities (true = min, false = max) long start1, start2, start3, stop; double time_taken, time_for_setup, time_for_iters; // adversary stuff - bool adv = false, adv_loop = false; + int export_adv_enabled = export_adv; + bool adv_loop = false; FILE *fp_adv = NULL; - int adv_l, adv_h; + int adv_j, adv_l2, adv_h2; + int *adv = NULL; + // action info + int *actions; + jstring *action_names_jstrings; + const char** action_names; + int num_actions; // misc int i, j, k, k_r, l1, h1, l2, h2, l2_r, h2_r, iters; double d1, d2, kb, kbt; @@ -128,6 +140,28 @@ jboolean min // min or max probabilities (true = min, false = max) PS_PrintToMainLog(env, "[n=%d, nc=%d, nnz=%d, k=%d] ", n, nc, nnz, ndsm->k); PS_PrintMemoryToMainLog(env, "[", kb, "]\n"); + // if needed, and if info is available, build a vector of action indices for the MDP + actions = NULL; + if (export_adv_enabled != EXPORT_ADV_NONE) { + if (trans_actions != NULL) { + PS_PrintToMainLog(env, "Building action information... "); + // first need to filter out unwanted rows + Cudd_Ref(trans_actions); + Cudd_Ref(maybe); + tmp = DD_Apply(ddman, APPLY_TIMES, trans_actions, maybe); + // then convert to a vector of integer indices + actions = build_nd_action_vector(ddman, a, tmp, ndsm, rvars, cvars, num_rvars, ndvars, num_ndvars, odd); + Cudd_RecursiveDeref(ddman, tmp); + kb = n*4.0/1024.0; + kbt += kb; + PS_PrintMemoryToMainLog(env, "[", kb, "]\n"); + // also extract list of action names from 'synchs' + get_string_array_from_java(env, synchs, action_names_jstrings, action_names, num_actions); + } else { + PS_PrintToMainLog(env, "Warning: Action labels are not available for adversary generation.\n", export_adv_filename); + } + } + // build sparse matrix (rewards) PS_PrintToMainLog(env, "Building sparse matrix (transition rewards)... "); ndsm_r = build_sub_nd_sparse_matrix(ddman, a, trans_rewards, rvars, cvars, num_rvars, ndvars, num_ndvars, odd); @@ -162,6 +196,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"); @@ -181,41 +228,41 @@ jboolean min // min or max probabilities (true = min, false = max) PS_PrintToMainLog(env, "\nStarting iterations...\n"); // open file to store adversary (if required) - if (adv) { - fp_adv = fopen("adv.tra", "w"); + if (export_adv_enabled != EXPORT_ADV_NONE) { + fp_adv = fopen(export_adv_filename, "w"); if (fp_adv) { fprintf(fp_adv, "%d ?\n", n); } else { - PS_PrintToMainLog(env, "\nWarning: Adversary generation cancelled (could not open file \"%s\").\n", "adv.tra"); - adv = false; + PS_PrintToMainLog(env, "\nWarning: Adversary generation cancelled (could not open file \"%s\").\n", export_adv_filename); + export_adv_enabled = EXPORT_ADV_NONE; } } - while ((!done && iters < max_iters) || adv_loop) { + // store local copies of stuff + // firstly for transition matrix + 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; + // and then for transition rewards matrix + // (note: we don't need row_counts/row_starts for + // this since choice structure mirrors transition matrix) + double *non_zeros_r = ndsm_r->non_zeros; + unsigned char *choice_counts_r = ndsm_r->choice_counts; + int *choice_starts_r = (int *)ndsm_r->choice_counts; + bool use_counts_r = ndsm_r->use_counts; + unsigned int *cols_r = ndsm_r->cols; + + while (!done && iters < max_iters) { iters++; // PS_PrintToMainLog(env, "iter %d\n", iters); // start3 = util_cpu_time(); - // store local copies of stuff - // firstly for transition matrix - 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; - // and then for transition rewards matrix - // (note: we don't need row_counts/row_starts for - // this since choice structure mirrors transition matrix) - double *non_zeros_r = ndsm_r->non_zeros; - unsigned char *choice_counts_r = ndsm_r->choice_counts; - int *choice_starts_r = (int *)ndsm_r->choice_counts; - bool use_counts_r = ndsm_r->use_counts; - unsigned int *cols_r = ndsm_r->cols; - // do matrix multiplication and min/max h1 = h2 = h2_r = 0; // loop through states @@ -248,16 +295,18 @@ jboolean min // min or max probabilities (true = min, false = max) // see if this value is the min/max so far if (first || (min&&(d2d1))) { d1 = d2; - if (adv_loop) { adv_l = l2; adv_h = h2; } + // if adversary generation is enabled, remember new (strictly) better choices + if (export_adv_enabled != EXPORT_ADV_NONE) { + if (adv[i] == -1 || (min&&(d1soln[i]))) { + adv[i] = j; + } + } } first = false; } // set vector element // (if there were no choices from this state, reward is zero/infinity) soln2[i] = (h1 > l1) ? d1 : inf_vec[i] > 0 ? HUGE_VAL : 0; - // store adversary info (if required) - if (adv_loop) if (h1 > l1) - for (k = adv_l; k < adv_h; k++) fprintf(fp_adv, "%d %d %g\n", i, cols[k], non_zeros[k]); } // check convergence @@ -296,6 +345,28 @@ jboolean min // min or max probabilities (true = min, false = max) // 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; @@ -308,9 +379,9 @@ jboolean min // min or max probabilities (true = min, false = max) if (!done) { delete soln; soln = NULL; PS_SetErrorMessage("Iterative method did not converge within %d iterations.\nConsider using a different numerical method or increasing the maximum number of iterations", iters); } // close file to store adversary (if required) - if (adv) { + if (export_adv_enabled != EXPORT_ADV_NONE) { fclose(fp_adv); - PS_PrintToMainLog(env, "\nAdversary written to file \"%s\".\n", "adv.tra"); + PS_PrintToMainLog(env, "\nAdversary written to file \"%s\".\n", export_adv_filename); } // catch exceptions: register error, free memory @@ -329,6 +400,11 @@ jboolean min // min or max probabilities (true = min, false = max) if (inf_vec) delete[] inf_vec; if (sr_vec) delete[] sr_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); + } return ptr_to_jlong(soln); } diff --git a/prism/src/sparse/PrismSparse.java b/prism/src/sparse/PrismSparse.java index ce2ba6d1..8bbc5dcc 100644 --- a/prism/src/sparse/PrismSparse.java +++ b/prism/src/sparse/PrismSparse.java @@ -274,10 +274,10 @@ public class PrismSparse } // pctl reach reward (nondeterministic/mdp) - private static native long PS_NondetReachReward(long trans, long sr, long trr, long odd, long rv, int nrv, long cv, int ncv, long ndv, int nndv, long goal, long inf, long maybe, boolean minmax); - public static DoubleVector NondetReachReward(JDDNode trans, JDDNode sr, JDDNode trr, ODDNode odd, JDDVars rows, JDDVars cols, JDDVars nondet, JDDNode goal, JDDNode inf, JDDNode maybe, boolean minmax) throws PrismException + private static native long PS_NondetReachReward(long trans, long trans_actions, List synchs, long sr, long trr, long odd, long rv, int nrv, long cv, int ncv, long ndv, int nndv, long goal, long inf, long maybe, boolean minmax); + public static DoubleVector NondetReachReward(JDDNode trans, JDDNode transActions, List synchs, JDDNode sr, JDDNode trr, ODDNode odd, JDDVars rows, JDDVars cols, JDDVars nondet, JDDNode goal, JDDNode inf, JDDNode maybe, boolean minmax) throws PrismException { - long ptr = PS_NondetReachReward(trans.ptr(), sr.ptr(), trr.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(), goal.ptr(), inf.ptr(), maybe.ptr(), minmax); + long ptr = PS_NondetReachReward(trans.ptr(), (transActions == null) ? 0 : transActions.ptr(), synchs, sr.ptr(), trr.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(), goal.ptr(), inf.ptr(), maybe.ptr(), minmax); if (ptr == 0) throw new PrismException(getErrorMessage()); return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff())); }