From 0143cef09e1c7d5a5dadbd6fa9f55f22a25b78fb Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 5 Dec 2007 10:42:44 +0000 Subject: [PATCH] Addition of -extrareachinfo option (and rearrangement of options in Modules2MTBDD). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@545 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/include/PrismMTBDD.h | 4 +- prism/src/mtbdd/PM_Reachability.cc | 22 ++++++-- prism/src/mtbdd/PrismMTBDD.java | 7 ++- prism/src/prism/Modules2MTBDD.java | 91 +++++------------------------- prism/src/prism/Prism.java | 22 +++++--- prism/src/prism/PrismCL.java | 7 ++- prism/src/prism/PrismSettings.java | 4 +- 7 files changed, 57 insertions(+), 100 deletions(-) diff --git a/prism/include/PrismMTBDD.h b/prism/include/PrismMTBDD.h index c976bdbd..3e87a1db 100644 --- a/prism/include/PrismMTBDD.h +++ b/prism/include/PrismMTBDD.h @@ -98,10 +98,10 @@ JNIEXPORT jstring JNICALL Java_mtbdd_PrismMTBDD_PM_1GetErrorMessage /* * Class: mtbdd_PrismMTBDD * Method: PM_Reachability - * Signature: (JJIJIJ)J + * Signature: (JJIJIJI)J */ JNIEXPORT jlong JNICALL Java_mtbdd_PrismMTBDD_PM_1Reachability - (JNIEnv *, jclass, jlong, jlong, jint, jlong, jint, jlong); + (JNIEnv *, jclass, jlong, jlong, jint, jlong, jint, jlong, jint); /* * Class: mtbdd_PrismMTBDD diff --git a/prism/src/mtbdd/PM_Reachability.cc b/prism/src/mtbdd/PM_Reachability.cc index e4db980d..5e5dcada 100644 --- a/prism/src/mtbdd/PM_Reachability.cc +++ b/prism/src/mtbdd/PM_Reachability.cc @@ -46,7 +46,8 @@ jlong __pointer rv, // row vars jint num_rvars, jlong __pointer cv, // col vars jint num_cvars, -jlong __pointer s // start state +jlong __pointer s, // start state +jint info // how much diagnostic info to display (0=none, 1=some) ) { DdNode *trans01 = jlong_to_DdNode(t01); // 0-1 trans matrix @@ -76,9 +77,14 @@ jlong __pointer s // start state // PM_PrintToMainLog(env, "Reachability:\n"); while (!done) { iters++; -// PM_PrintToMainLog(env, "Iteration %d: ", iters); -// PM_PrintToMainLog(env, "%0.f (%d) ", DD_GetNumMinterms(ddman, reach, num_rvars), DD_GetNumNodes(ddman, reach)); -// start2 = util_cpu_time(); + + // output info on progress + if (info > 0) { + PM_PrintToMainLog(env, "Iteration %d:", iters); + PM_PrintToMainLog(env, " %0.f states", DD_GetNumMinterms(ddman, reach, num_rvars)); + PM_PrintToMainLog(env, " (%d nodes)", DD_GetNumNodes(ddman, reach)); + start2 = util_cpu_time(); + } // PM_PrintToMainLog(env, "[permute(%d)", DD_GetNumNodes(ddman, reach)); // start3 = util_cpu_time(); @@ -112,8 +118,12 @@ jlong __pointer s // start state } Cudd_RecursiveDeref(ddman, reach); reach = tmp; -// stop = util_cpu_time(); -// PM_PrintToMainLog(env, " = %f\n", (double)(stop - start2)/1000); + + // output info on progress + if (info > 0) { + stop = util_cpu_time(); + PM_PrintToMainLog(env, " (%.2f seconds)\n", (double)(stop - start2)/1000); + } } reach = DD_PermuteVariables(ddman, reach, cvars, rvars, num_cvars); // ...to here diff --git a/prism/src/mtbdd/PrismMTBDD.java b/prism/src/mtbdd/PrismMTBDD.java index 9d90b225..5aff9022 100644 --- a/prism/src/mtbdd/PrismMTBDD.java +++ b/prism/src/mtbdd/PrismMTBDD.java @@ -178,10 +178,11 @@ public class PrismMTBDD //------------------------------------------------------------------------------ // reachability - private static native long PM_Reachability(long trans01, long rv, int nrv, long cv, int ncv, long start); - public static JDDNode Reachability(JDDNode trans01, JDDVars rows, JDDVars cols, JDDNode start)// throws PrismException + private static native long PM_Reachability(long trans01, long rv, int nrv, long cv, int ncv, long start, int info); + public static JDDNode Reachability(JDDNode trans01, JDDVars rows, JDDVars cols, JDDNode start) { return Reachability(trans01, rows, cols, start, 0); } + public static JDDNode Reachability(JDDNode trans01, JDDVars rows, JDDVars cols, JDDNode start, int info)// throws PrismException { - long ptr = PM_Reachability(trans01.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), start.ptr()); + long ptr = PM_Reachability(trans01.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), start.ptr(), info); //if (ptr == 0) throw new PrismException(getErrorMessage()); return new JDDNode(ptr); } diff --git a/prism/src/prism/Modules2MTBDD.java b/prism/src/prism/Modules2MTBDD.java index 1cef0a9a..db63f3e8 100644 --- a/prism/src/prism/Modules2MTBDD.java +++ b/prism/src/prism/Modules2MTBDD.java @@ -42,19 +42,13 @@ public class Modules2MTBDD // constants private static final double ACCEPTABLE_ROUND_OFF = 10e-6; // when checking for sums to 1 + // Prism object + private Prism prism; + // logs private PrismLog mainLog; // main log private PrismLog techLog; // tech log - // flags/settings - private boolean doReach = true; // by default, do reachability (sometimes might want to skip it though) - private boolean doProbChecks; // perform checks on probs/rates? (sum to one, etc.) - private boolean extraDDInfo; // display extra info about DDs - // the following two settings are now surplus to requirements - // because of the way nondeterminism is handled in the mtbdd construction - private int ordering = 1; // mtbdd variable ordering (1=top, 2=middle) (default: 1) - private int construction = 3; // mtbdd construction method (1=dup, 3=0) (default: 3) - // ModulesFile object to store syntax tree from parser private ModulesFile modulesFile; @@ -153,73 +147,14 @@ public class Modules2MTBDD // constructor - public Modules2MTBDD(PrismLog log1, PrismLog log2, ModulesFile mf) + public Modules2MTBDD(Prism p, ModulesFile mf) { - mainLog = log1; - techLog = log2; + prism = p; + mainLog = p.getMainLog(); + techLog = p.getTechLog(); modulesFile = mf; } - // set options (generic) - - public void setOption(String option, boolean b) - { - if (option.equals("doreach")) { - doReach = b; - } - else if (option.equals("doprobchecks")) { - doProbChecks = b; - } - else if (option.equals("extraddinfo")) { - extraDDInfo = b; - } - else { - mainLog.println("\nWarning: option \""+option+"\" not supported by Modules2MTBDD translator."); - } - } - - public void setOption(String option, int i) - { - if (option.equals("ordering")) { - setOrdering(i); - } - else if (option.equals("construction")) { - setConstruction(i); - } - else { - mainLog.println("\nWarning: option \""+option+"\" not supported by Modules2MTBDD translator."); - } - } - - public void setOption(String option, String s) - { - mainLog.println("\nWarning: option \""+option+"\" not supported by Modules2MTBDD translator."); - } - - // set flags/settings - - private void setOrdering(int i) - { - if (i > 0) { - ordering = i; - } - else { - // default to 1 - ordering = 1; - } - } - - private void setConstruction(int i) - { - if (i > 0) { - construction = i; - } - else { - // default to 3 - construction = 3; - } - } - // main method - translate public Model translate() throws PrismException @@ -284,14 +219,14 @@ public class Modules2MTBDD // JDD.Deref(tmp); // Print some info (if extraddinfo flag on) - if (extraDDInfo) { + if (prism.getExtraDDInfo()) { mainLog.print("Transition matrix (pre-reachability): "); mainLog.print(JDD.GetNumNodes(trans) + " nodes ("); mainLog.print(JDD.GetNumTerminals(trans) + " terminal)\n"); } // do reachability (or not!) - if (doReach) { + if (prism.getDoReach()) { doReachability(); } else { @@ -363,7 +298,7 @@ public class Modules2MTBDD int ddVarsUsed = 0; ddVarNames = new Vector(); - switch (ordering) { + switch (prism.getOrdering()) { case 1: // ordering: (a ... a) (s ... s) (l ... l) (r c ... r c) @@ -1413,7 +1348,7 @@ public class Modules2MTBDD throw new PrismException(s); } // only do remaining checks if 'doprobchecks' flag is set - if (doProbChecks) { + if (prism.getDoProbChecks()) { // sum probs/rates in updates JDD.Ref(upDDs[l]); tmp = JDD.SumAbstract(upDDs[l], moduleDDColVars[m]); @@ -2036,11 +1971,11 @@ public class Modules2MTBDD // compute reachable states mainLog.print("\nComputing reachable states...\n"); - reach = PrismMTBDD.Reachability(tmp, allDDRowVars, allDDColVars, start); + reach = PrismMTBDD.Reachability(tmp, allDDRowVars, allDDColVars, start, prism.getExtraReachInfo()?1:0); JDD.Deref(tmp); // Print some info (if extraddinfo flag on) - if (extraDDInfo) { + if (prism.getExtraDDInfo()) { mainLog.print("Reach: " + JDD.GetNumNodes(reach) + " nodes\n"); } // remove non-reachable states from transition matrix diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index bd7ab28c..e5af81c2 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -89,17 +89,18 @@ public class Prism implements PrismSettingsListener private PrismSettings settings; // A few miscellaneous options (i.e. defunct/hidden/undocumented/etc.) + // See constructor below for default values private boolean doReach; // do reachability? (sometimes might want to skip it) private boolean bsccComp; // do bscc computation before steady-state? - // mtbdd construction method + // MTBDD construction method (NOW DEFUNCT) // 1 - use with ordering 1: nondet vars form a tree at the top // 3 - use with ordering 2: zero for nonexistant bits // nb: option 2 removed because it was stupid private int construction; - // mtbdd variable ordering + // MTBDD variable ordering // 1 - (s ... s) (l ... l) (r c ... r c) // 2 - (s l ... l r c ... r c) (s l ... l r c ... r c) ... private int ordering; @@ -168,7 +169,7 @@ public class Prism implements PrismSettingsListener // default values for miscellaneous options doReach = true; bsccComp = true; - construction = 0; + construction = 3; ordering = 1; } @@ -293,6 +294,11 @@ public class Prism implements PrismSettingsListener settings.set(PrismSettings.PRISM_EXTRA_DD_INFO, b); } + public void setExtraReachInfo(boolean b) throws PrismException + { + settings.set(PrismSettings.PRISM_EXTRA_REACH_INFO, b); + } + // set methods for miscellaneous options public void setDoReach(boolean b) throws PrismException @@ -374,6 +380,9 @@ public class Prism implements PrismSettingsListener public boolean getExtraDDInfo() { return settings.getBoolean(PrismSettings.PRISM_EXTRA_DD_INFO); } + public boolean getExtraReachInfo() + { return settings.getBoolean(PrismSettings.PRISM_EXTRA_REACH_INFO); } + public int getNumSORLevels() { return settings.getInteger(PrismSettings.PRISM_NUM_SOR_LEVELS); } @@ -827,12 +836,7 @@ public class Prism implements PrismSettingsListener mainLog.print("...\n"); // create translator - mod2mtbdd = new Modules2MTBDD(mainLog, techLog, modulesFile); - mod2mtbdd.setOption("ordering", getOrdering()); - mod2mtbdd.setOption("construction", getConstruction()); - mod2mtbdd.setOption("doreach", getDoReach()); - mod2mtbdd.setOption("doprobchecks", getDoProbChecks()); - mod2mtbdd.setOption("extraddinfo", getExtraDDInfo()); + mod2mtbdd = new Modules2MTBDD(this, modulesFile); // build model l = System.currentTimeMillis(); diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index d60ec123..af32fd0f 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -1168,6 +1168,10 @@ public class PrismCL else if (sw.equals("extraddinfo")) { prism.setExtraDDInfo(true); } + // extra reach info on + else if (sw.equals("extrareachinfo")) { + prism.setExtraReachInfo(true); + } // precomputation algs off else if (sw.equals("nopre")) { prism.setPrecomp(false); @@ -1464,7 +1468,7 @@ public class PrismCL mainLog.println("-exportresults .......... Export the results of model checking to a file"); mainLog.println("-exporttrans ............ Export the transition matrix to a file"); mainLog.println("-exportstaterewards ..... Export the state rewards vector to a file"); - mainLog.println("-exporttransrewards ...... Export the transition rewards matrix to a file"); + mainLog.println("-exporttransrewards ..... Export the transition rewards matrix to a file"); mainLog.println("-exportstates ........... Export the list of reachable states to a file"); mainLog.println("-exportlabels ........... Export the list of labels and satisfying states to a file"); mainLog.println("-exportmatlab .................. When exporting matrices/vectors/labels/etc., use Matlab format"); @@ -1499,6 +1503,7 @@ public class PrismCL mainLog.println(); mainLog.println("-verbose (or -v) ............... Verbose mode: print out state lists and probability vectors"); mainLog.println("-extraddinfo ................... Display extra info about some (MT)BDDs"); + mainLog.println("-extrareachinfo ................ Display extra info about progress of reachability"); mainLog.println("-nopre ......................... Skip precomputation algorithms"); mainLog.println("-fair .......................... Use fairness (when model checking PCTL on MDPs)"); mainLog.println("-nofair ........................ Don't use fairness (when model checking PCTL on MDPs) [default]"); diff --git a/prism/src/prism/PrismSettings.java b/prism/src/prism/PrismSettings.java index e9d995d0..ad06d623 100644 --- a/prism/src/prism/PrismSettings.java +++ b/prism/src/prism/PrismSettings.java @@ -88,6 +88,7 @@ public class PrismSettings implements Observer public static final String PRISM_SOR_MAX_MEM = "prism.SORMaxMem";//"prism.hybridSORMaxMemory"; public static final String PRISM_DO_SS_DETECTION = "prism.doSSDetect"; public static final String PRISM_EXTRA_DD_INFO = "prism.extraDDInfo"; + public static final String PRISM_EXTRA_REACH_INFO = "prism.extraReachInfo"; //GUI Model public static final String MODEL_AUTO_PARSE = "model.autoParse"; @@ -180,7 +181,8 @@ public class PrismSettings implements Observer { INTEGER_TYPE, PRISM_NUM_SOR_LEVELS, "Hybrid GS levels", "3.0", new Integer(-1), "-1,", "Number of MTBDD levels descended for hybrid engine data structures block division with GS/SOR." }, { INTEGER_TYPE, PRISM_SOR_MAX_MEM, "Hybrid GS memory (KB)", "3.0", new Integer(1024), "0,", "Maximum memory usage for hybrid engine data structures block division with GS/SOR (KB)." }, { BOOLEAN_TYPE, PRISM_DO_SS_DETECTION, "Use steady-state detection", "3.0", new Boolean(true), "0,", "Use steady-state detection during CTMC transient probability computation." }, - { BOOLEAN_TYPE, PRISM_EXTRA_DD_INFO, "Extra MTBDD information", "3.0", new Boolean(false), "0,", "Display extra information about (MT)BDDs used during and after model construction." } + { BOOLEAN_TYPE, PRISM_EXTRA_DD_INFO, "Extra MTBDD information", "3.2", new Boolean(false), "0,", "Display extra information about (MT)BDDs used during and after model construction." }, + { BOOLEAN_TYPE, PRISM_EXTRA_REACH_INFO, "Extra reachability information", "3.2", new Boolean(false), "0,", "Display extra information about progress of reachability during model construction." } }, { { BOOLEAN_TYPE, MODEL_AUTO_PARSE, "Auto parse", "3.0", new Boolean(true), "", "Parse PRISM models automatically as they are loaded/edited in the text editor." },