From db56e3bc0f8d1f8fb0db42180a9a877454dbfa6e Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 18 Mar 2010 13:52:47 +0000 Subject: [PATCH] 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 | 65 ++++++++++++++------- prism/src/sparse/PS_NondetUntil.cc | 75 ++++++++++++++++++------- 2 files changed, 100 insertions(+), 40 deletions(-) diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index add7a924..f4ef85c1 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/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); diff --git a/prism/src/sparse/PS_NondetUntil.cc b/prism/src/sparse/PS_NondetUntil.cc index f84e9b23..c6459c31 100644 --- a/prism/src/sparse/PS_NondetUntil.cc +++ b/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&&(d2d1))) { 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&&(d1soln[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);