Added option to disable steady-state detection for CTMC transient analysis.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@63 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/include/PrismHybrid.h

@@ -119,6 +119,14 @@ JNIEXPORT void JNICALL Java_hybrid_PrismHybrid_PH_1SetNumSORLevels
 JNIEXPORT void JNICALL Java_hybrid_PrismHybrid_PH_1SetCompact
   (JNIEnv *, jclass, jboolean);
 
+/*
+ * Class:     hybrid_PrismHybrid
+ * Method:    PH_SetDoSSDetect
+ * Signature: (Z)V
+ */
+JNIEXPORT void JNICALL Java_hybrid_PrismHybrid_PH_1SetDoSSDetect
+  (JNIEnv *, jclass, jboolean);
+
 /*
  * Class:     hybrid_PrismHybrid
  * Method:    PH_GetErrorMessage

prism/include/PrismHybridGlob.h

@@ -69,6 +69,9 @@ extern int num_sor_levels;
 // use "compact modified" sparse matrix storage?
 extern bool compact;
 
+// use steady-state detection for transient computation?
+extern bool do_ss_detect;
+
 // details from numerical computation which may be queried
 extern double last_unif;
 

prism/include/PrismMTBDD.h

@@ -79,6 +79,14 @@ JNIEXPORT void JNICALL Java_mtbdd_PrismMTBDD_PM_1SetTermCritParam
 JNIEXPORT void JNICALL Java_mtbdd_PrismMTBDD_PM_1SetMaxIters
   (JNIEnv *, jclass, jint);
 
+/*
+ * Class:     mtbdd_PrismMTBDD
+ * Method:    PM_SetDoSSDetect
+ * Signature: (Z)V
+ */
+JNIEXPORT void JNICALL Java_mtbdd_PrismMTBDD_PM_1SetDoSSDetect
+  (JNIEnv *, jclass, jboolean);
+
 /*
  * Class:     mtbdd_PrismMTBDD
  * Method:    PM_GetErrorMessage

prism/include/PrismMTBDDGlob.h

@@ -61,6 +61,9 @@ extern int term_crit;
 extern double term_crit_param;
 extern int max_iters;
 
+// use steady-state detection for transient computation?
+extern bool do_ss_detect;
+
 // export stuff
 extern int export_type;
 extern FILE *export_file;

prism/include/PrismSparse.h

@@ -87,6 +87,14 @@ JNIEXPORT void JNICALL Java_sparse_PrismSparse_PS_1SetMaxIters
 JNIEXPORT void JNICALL Java_sparse_PrismSparse_PS_1SetCompact
   (JNIEnv *, jclass, jboolean);
 
+/*
+ * Class:     sparse_PrismSparse
+ * Method:    PS_SetDoSSDetect
+ * Signature: (Z)V
+ */
+JNIEXPORT void JNICALL Java_sparse_PrismSparse_PS_1SetDoSSDetect
+  (JNIEnv *, jclass, jboolean);
+
 /*
  * Class:     sparse_PrismSparse
  * Method:    PS_GetErrorMessage

prism/include/PrismSparseGlob.h

@@ -64,6 +64,9 @@ extern int max_iters;
 // use "compact modified" sparse matrix storage?
 extern bool compact;
 
+// use steady-state detection for transient computation?
+extern bool do_ss_detect;
+
 // export stuff
 extern int export_type;
 extern FILE *export_file;

prism/src/hybrid/PH_StochBoundedUntil.cc

@@ -235,7 +235,7 @@ jint mu			// probs for multiplying
 		mult_rec(hdd, 0, 0, 0);
 		
 		// check for steady state convergence
-		switch (term_crit) {
+		if (do_ss_detect) switch (term_crit) {
 		case TERM_CRIT_ABSOLUTE:
 			done = true;
 			for (i = 0; i < n; i++) {

prism/src/hybrid/PH_StochCumulReward.cc

@@ -263,7 +263,7 @@ jdouble time	// time bound
 		
 		// check for steady state convergence
 		// (note: doing outside loop means may not need to check all elements)
-		switch (term_crit) {
+		if (do_ss_detect) switch (term_crit) {
 		case TERM_CRIT_ABSOLUTE:
 			done = true;
 			for (i = 0; i < n; i++) {

prism/src/hybrid/PH_StochTransient.cc

@@ -214,7 +214,7 @@ jdouble time	// time bound
 		mult_rec(hdd, 0, 0, 0);
 		
 		// check for steady state convergence
-		switch (term_crit) {
+		if (do_ss_detect) switch (term_crit) {
 		case TERM_CRIT_ABSOLUTE:
 			done = true;
 			for (i = 0; i < n; i++) {

prism/src/hybrid/PrismHybrid.cc

@@ -69,6 +69,9 @@ int num_sor_levels;
 // use "compact modified" sparse matrix storage?
 bool compact;
 
+// use steady-state detection for transient computation?
+bool do_ss_detect;
+
 // error message
 char error_message[MAX_ERR_STRING_LEN];
 
@@ -234,6 +237,15 @@ JNIEXPORT void JNICALL Java_hybrid_PrismHybrid_PH_1SetCompact(JNIEnv *env, jclas
 	compact = b;
 }
 
+//------------------------------------------------------------------------------
+// use steady-state detection?
+//------------------------------------------------------------------------------
+
+JNIEXPORT void JNICALL Java_hybrid_PrismHybrid_PH_1SetDoSSDetect(JNIEnv *env, jclass cls, jboolean b)
+{
+	do_ss_detect = b;
+}
+
 //------------------------------------------------------------------------------
 // error message handling
 //------------------------------------------------------------------------------

prism/src/hybrid/PrismHybrid.java

@@ -184,6 +184,16 @@ public class PrismHybrid
 	{
 		PH_SetCompact(b);
 	}
+	
+	//------------------------------------------------------------------------------
+	// use steady-state detection?
+	//------------------------------------------------------------------------------
+	
+	private static native void PH_SetDoSSDetect(boolean b);
+	public static void setDoSSDetect(boolean b)
+	{
+		PH_SetDoSSDetect(b);
+	}
 
 	//------------------------------------------------------------------------------
 	// error message

prism/src/mtbdd/PM_StochBoundedUntil.cc

@@ -251,7 +251,7 @@ jint mu			// probs for multiplying
 //		PM_PrintToMainLog(env, "(%d %d %.0f)\n", DD_GetNumNodes(ddman, sum), DD_GetNumTerminals(ddman, sum), DD_GetNumMinterms(ddman, sum, num_rvars));
 		
 		// check for steady state convergence
-		switch (term_crit) {
+		if (do_ss_detect) switch (term_crit) {
 		case TERM_CRIT_ABSOLUTE:
 			if (DD_EqualSupNorm(ddman, tmp, sol, term_crit_param)) {
 				done = true;

prism/src/mtbdd/PM_StochCumulReward.cc

@@ -170,7 +170,7 @@ jdouble time	// time bound
 		tmp = DD_MatrixMultiply(ddman, q, tmp, cvars, num_cvars, MM_BOULDER);
 		
 		// check for steady state convergence
-		switch (term_crit) {
+		if (do_ss_detect) switch (term_crit) {
 		case TERM_CRIT_ABSOLUTE:
 			if (DD_EqualSupNorm(ddman, tmp, sol, term_crit_param)) {
 				done = true;

prism/src/mtbdd/PM_StochTransient.cc

@@ -227,7 +227,7 @@ jdouble time	// time bound
 //		PM_PrintToMainLog(env, "(%d %d %.0f)\n", DD_GetNumNodes(ddman, sum), DD_GetNumTerminals(ddman, sum), DD_GetNumMinterms(ddman, sum, num_rvars));
 		
 		// check for steady state convergence
-		switch (term_crit) {
+		if (do_ss_detect) switch (term_crit) {
 		case TERM_CRIT_ABSOLUTE:
 			if (DD_EqualSupNorm(ddman, tmp, sol, term_crit_param)) {
 				done = true;

prism/src/mtbdd/PrismMTBDD.cc

@@ -63,6 +63,9 @@ int export_type;
 FILE *export_file;
 JNIEnv *export_env;
 
+// use steady-state detection for transient computation?
+bool do_ss_detect;
+
 // error message
 char error_message[MAX_ERR_STRING_LEN];
 
@@ -229,6 +232,15 @@ void export_string(char *str, ...)
 	}
 }
 
+//------------------------------------------------------------------------------
+// use steady-state detection?
+//------------------------------------------------------------------------------
+
+JNIEXPORT void JNICALL Java_mtbdd_PrismMTBDD_PM_1SetDoSSDetect(JNIEnv *env, jclass cls, jboolean b)
+{
+	do_ss_detect = b;
+}
+
 //------------------------------------------------------------------------------
 // error message handling
 //------------------------------------------------------------------------------

prism/src/mtbdd/PrismMTBDD.java

@@ -144,6 +144,16 @@ public class PrismMTBDD
 		PM_SetMaxIters(i);
 	}
 
+	//------------------------------------------------------------------------------
+	// use steady-state detection?
+	//------------------------------------------------------------------------------
+	
+	private static native void PM_SetDoSSDetect(boolean b);
+	public static void setDoSSDetect(boolean b)
+	{
+		PM_SetDoSSDetect(b);
+	}
+
 	//------------------------------------------------------------------------------
 	// error message
 	//------------------------------------------------------------------------------

prism/src/prism/Prism.java

@@ -271,6 +271,11 @@ public class Prism
 		settings.set(PrismSettings.PRISM_SOR_MAX_MEM, i);
 	}
 	
+	public void setDoSSDetect(boolean b) throws PrismException
+	{
+		settings.set(PrismSettings.PRISM_DO_SS_DETECTION, b);
+	}
+	
 	public void setApmcStrategy(int i) throws PrismException
 	{
 		settings.set(PrismSettings.SIMULATOR_APMC_STRATEGY, i);
@@ -351,6 +356,9 @@ public class Prism
 	public int getSORMaxMem()
 	{ return settings.getInteger(PrismSettings.PRISM_SOR_MAX_MEM); }
 	
+	public boolean getDoSSDetect()
+	{ return settings.getBoolean(PrismSettings.PRISM_DO_SS_DETECTION); }
+	
 	public int getNumSORLevels()
 	{ return settings.getInteger(PrismSettings.PRISM_NUM_SOR_LEVELS); }
 	
@@ -1051,6 +1059,7 @@ public class Prism
 		if (model instanceof StochModel)
 		{
 			mc.setOption("bscccomp", getBSCCComp());
+			mc.setOption("dossdetect", getDoSSDetect());
 		}
 		if (model instanceof NondetModel)
 		{
@@ -1329,6 +1338,7 @@ public class Prism
 		mc.setOption("maxiters", getMaxIters()); // don't really need
 		mc.setOption("verbose", getVerbose());
 		mc.setOption("bscccomp", getBSCCComp()); // don't really need
+		mc.setOption("dossdetect", getDoSSDetect());
 		if (getEngine() == HYBRID || getEngine() == SPARSE)
 		{
 			mc.setOption("compact", getCompact());

prism/src/prism/PrismCL.java

@@ -1159,6 +1159,10 @@ public class PrismCL
 				else if (sw.equals("nobscc")) {
 					prism.setBSCCComp(false);
 				}
+				// no steady-state detection
+				else if (sw.equals("nossdetect")) {
+					prism.setDoSSDetect(false);
+				}
 				// sparse bits info
 				else if (sw.equals("sbmax")) {
 					if (i < args.length-1) {
@@ -1486,6 +1490,7 @@ public class PrismCL
 		mainLog.println("-fixdl ......................... Automatically put self-loops in deadlock states");
 		mainLog.println("-nocompact ..................... Switch off \"compact\" sparse storage schemes");
 		mainLog.println("-noprobchecks .................. Disable checks on model probabilities/rates");
+		mainLog.println("-nossdetect .................... Disable steady-state detection for CTMC transient computations");
 		mainLog.println();
 		mainLog.println("-sbmax <n> ..................... Set memory limit (KB) (for hybrid engine) [default 1024]");
 		mainLog.println("-sbl <n> ....................... Set number of levels (for hybrid engine) [default -1]");

prism/src/prism/PrismSettings.java

@@ -80,6 +80,7 @@ public class PrismSettings implements Observer
 	public static final	String PRISM_SB_MAX_MEM						= "prism.SBMaxMem";//"prism.hybridMaxMemory";
 	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";
 	
 	//GUI Model
 	public static final	String MODEL_AUTO_PARSE						= "model.autoParse";
@@ -179,6 +180,7 @@ public class PrismSettings implements Observer
 			{ INTEGER_TYPE,		PRISM_SB_MAX_MEM,						"hybrid max memory",					new Integer(1024),															"0,",																						"Maximum memory usage when adding sparse matrices to hybrid engine data structures" },
 			{ INTEGER_TYPE,		PRISM_NUM_SOR_LEVELS,					"hybrid num. levels (GS/SOR)",			new Integer(-1),															"-1,",																						"Number of MTBDD levels descended for hybrid engine data structures block division (GS/SOR)" },
 			{ INTEGER_TYPE,		PRISM_SOR_MAX_MEM,						"hybrid max memory (GS/SOR)",			new Integer(1024),															"0,",																						"Maximum memory usage for hybrid engine data structures block division (GS/SOR)" },
+			{ BOOLEAN_TYPE,		PRISM_DO_SS_DETECTION,					"use steady-state detection?",			new Boolean(true),															"0,",																						"Use steady-state detection for CTMC transient properties?" }
 		},
 		{
 			{ BOOLEAN_TYPE,		MODEL_AUTO_PARSE,						"auto parse?",							new Boolean(true),															"",																							"When set to true, prism models are parsed automatically as they are entered into the text editor." },

prism/src/prism/StochModelChecker.java

@@ -164,6 +164,11 @@ public class StochModelChecker implements ModelChecker
 		else if (option.equals("bscccomp")) {
 			bsccComp = b;
 		}
+		else if (option.equals("dossdetect")) {
+			PrismMTBDD.setDoSSDetect(b);
+			PrismSparse.setDoSSDetect(b);
+			PrismHybrid.setDoSSDetect(b);
+		}
 		else if (option.equals("compact")) {
 			PrismHybrid.setCompact(b);
 			PrismSparse.setCompact(b);

prism/src/sparse/PS_StochBoundedUntil.cc

@@ -262,7 +262,7 @@ jint mu			// probs for multiplying
 		
 		// check for steady state convergence
 		// (note: doing outside loop means may not need to check all elements)
-		switch (term_crit) {
+		if (do_ss_detect) switch (term_crit) {
 		case TERM_CRIT_ABSOLUTE:
 			done = true;
 			for (i = 0; i < n; i++) {

prism/src/sparse/PS_StochCumulReward.cc

@@ -289,7 +289,7 @@ jdouble time	// time bound
 		
 		// check for steady state convergence
 		// (note: doing outside loop means may not need to check all elements)
-		switch (term_crit) {
+		if (do_ss_detect) switch (term_crit) {
 		case TERM_CRIT_ABSOLUTE:
 			done = true;
 			for (i = 0; i < n; i++) {

prism/src/sparse/PS_StochTransient.cc

@@ -240,7 +240,7 @@ jdouble time	// time bound
 		
 		// check for steady state convergence
 		// (note: doing outside loop means may not need to check all elements)
-		switch (term_crit) {
+		if (do_ss_detect) switch (term_crit) {
 		case TERM_CRIT_ABSOLUTE:
 			done = true;
 			for (i = 0; i < n; i++) {

prism/src/sparse/PrismSparse.cc

@@ -60,6 +60,9 @@ int max_iters;
 // use "compact modified" sparse matrix storage?
 bool compact;
 
+// use steady-state detection for transient computation?
+bool do_ss_detect;
+
 // export stuff
 int export_type;
 FILE *export_file;
@@ -240,6 +243,15 @@ void export_string(char *str, ...)
 	}
 }
 
+//------------------------------------------------------------------------------
+// use steady-state detection?
+//------------------------------------------------------------------------------
+
+JNIEXPORT void JNICALL Java_sparse_PrismSparse_PS_1SetDoSSDetect(JNIEnv *env, jclass cls, jboolean b)
+{
+	do_ss_detect = b;
+}
+
 //------------------------------------------------------------------------------
 // error message handling
 //------------------------------------------------------------------------------

prism/src/sparse/PrismSparse.java

@@ -155,6 +155,16 @@ public class PrismSparse
 		PS_SetCompact(b);
 	}
 
+	//------------------------------------------------------------------------------
+	// use steady-state detection?
+	//------------------------------------------------------------------------------
+	
+	private static native void PS_SetDoSSDetect(boolean b);
+	public static void setDoSSDetect(boolean b)
+	{
+		PS_SetDoSSDetect(b);
+	}
+
 	//------------------------------------------------------------------------------
 	// error message
 	//------------------------------------------------------------------------------