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

@@ -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);

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();

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")) {

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." },