From bec72228418db48a6f3fce18a81be0c19099e84d Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 9 Nov 2007 09:17:34 +0000 Subject: [PATCH] Promoted "extraddinfo" flag to full PRISM option and added some extra output during model construction. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@520 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/Modules2MTBDD.java | 15 +++++++++++++++ prism/src/prism/Prism.java | 9 +++++++++ prism/src/prism/PrismCL.java | 7 +++---- prism/src/prism/PrismSettings.java | 4 +++- 4 files changed, 30 insertions(+), 5 deletions(-) diff --git a/prism/src/prism/Modules2MTBDD.java b/prism/src/prism/Modules2MTBDD.java index a3d50f09..07b76fa0 100644 --- a/prism/src/prism/Modules2MTBDD.java +++ b/prism/src/prism/Modules2MTBDD.java @@ -49,6 +49,7 @@ public class Modules2MTBDD // 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) @@ -169,6 +170,9 @@ public class Modules2MTBDD 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."); } @@ -279,6 +283,13 @@ public class Modules2MTBDD // mainLog.println(); // JDD.Deref(tmp); + // Print some info (if extraddinfo flag on) + if (extraDDInfo) { + 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) { doReachability(); @@ -2028,6 +2039,10 @@ public class Modules2MTBDD reach = PrismMTBDD.Reachability(tmp, allDDRowVars, allDDColVars, start); JDD.Deref(tmp); + // Print some info (if extraddinfo flag on) + if (extraDDInfo) { + mainLog.print("Reach: " + JDD.GetNumNodes(reach) + " nodes\n"); + } // remove non-reachable states from transition matrix JDD.Ref(reach); trans = JDD.Apply(JDD.TIMES, reach, trans); diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 73804da4..8576a362 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -288,6 +288,11 @@ public class Prism implements PrismSettingsListener settings.set(PrismSettings.PRISM_DO_SS_DETECTION, b); } + public void setExtraDDInfo(boolean b) throws PrismException + { + settings.set(PrismSettings.PRISM_EXTRA_DD_INFO, b); + } + // set methods for miscellaneous options public void setDoReach(boolean b) throws PrismException @@ -366,6 +371,9 @@ public class Prism implements PrismSettingsListener public boolean getDoSSDetect() { return settings.getBoolean(PrismSettings.PRISM_DO_SS_DETECTION); } + public boolean getExtraDDInfo() + { return settings.getBoolean(PrismSettings.PRISM_EXTRA_DD_INFO); } + public int getNumSORLevels() { return settings.getInteger(PrismSettings.PRISM_NUM_SOR_LEVELS); } @@ -824,6 +832,7 @@ public class Prism implements PrismSettingsListener mod2mtbdd.setOption("construction", getConstruction()); mod2mtbdd.setOption("doreach", getDoReach()); mod2mtbdd.setOption("doprobchecks", getDoProbChecks()); + mod2mtbdd.setOption("extraddinfo", getExtraDDInfo()); // build model l = System.currentTimeMillis(); diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 61127268..cde31054 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -60,7 +60,6 @@ public class PrismCL private boolean exportordered = true; private boolean simulate = false; private boolean simpath = false; - private boolean extraDDInfo = false; private int typeOverride = 0; // property info @@ -562,7 +561,7 @@ public class PrismCL // otherwise print error and bail out else { mainLog.println(); - model.printTransInfo(mainLog, extraDDInfo); + model.printTransInfo(mainLog, prism.getExtraDDInfo()); mainLog.print("\nError: Model contains " + states.size() + " deadlock states"); if (!verbose && states.size() > 10) { mainLog.print(".\nThe first 10 deadlock states are displayed below. To view them all use the -v switch.\n"); @@ -580,7 +579,7 @@ public class PrismCL // print more model info mainLog.println(); - model.printTransInfo(mainLog, extraDDInfo); + model.printTransInfo(mainLog, prism.getExtraDDInfo()); } // do any exporting requested @@ -1167,7 +1166,7 @@ public class PrismCL } // extra dd info on else if (sw.equals("extraddinfo")) { - extraDDInfo = true; + prism.setExtraDDInfo(true); } // precomputation algs off else if (sw.equals("nopre")) { diff --git a/prism/src/prism/PrismSettings.java b/prism/src/prism/PrismSettings.java index 50df96d2..e9d995d0 100644 --- a/prism/src/prism/PrismSettings.java +++ b/prism/src/prism/PrismSettings.java @@ -87,6 +87,7 @@ public class PrismSettings implements Observer public static final String PRISM_NUM_SOR_LEVELS = "prism.numSORLevels";//"prism.hybridSORLevels"; 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"; //GUI Model public static final String MODEL_AUTO_PARSE = "model.autoParse"; @@ -178,7 +179,8 @@ public class PrismSettings implements Observer { INTEGER_TYPE, PRISM_SB_MAX_MEM, "Hybrid sparse memory (KB)", "3.0", new Integer(1024), "0,", "Maximum memory usage when adding sparse matrices to hybrid engine data structures (KB)." }, { 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_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, MODEL_AUTO_PARSE, "Auto parse", "3.0", new Boolean(true), "", "Parse PRISM models automatically as they are loaded/edited in the text editor." },