From 1188cda2735121ebe6202e045c8d541011fbb6fd Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 26 Jul 2006 09:06:08 +0000 Subject: [PATCH] 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 | 8 ++++++++ prism/include/PrismHybridGlob.h | 3 +++ prism/include/PrismMTBDD.h | 8 ++++++++ prism/include/PrismMTBDDGlob.h | 3 +++ prism/include/PrismSparse.h | 8 ++++++++ prism/include/PrismSparseGlob.h | 3 +++ prism/src/hybrid/PH_StochBoundedUntil.cc | 2 +- prism/src/hybrid/PH_StochCumulReward.cc | 2 +- prism/src/hybrid/PH_StochTransient.cc | 2 +- prism/src/hybrid/PrismHybrid.cc | 12 ++++++++++++ prism/src/hybrid/PrismHybrid.java | 10 ++++++++++ prism/src/mtbdd/PM_StochBoundedUntil.cc | 2 +- prism/src/mtbdd/PM_StochCumulReward.cc | 2 +- prism/src/mtbdd/PM_StochTransient.cc | 2 +- prism/src/mtbdd/PrismMTBDD.cc | 12 ++++++++++++ prism/src/mtbdd/PrismMTBDD.java | 10 ++++++++++ prism/src/prism/Prism.java | 10 ++++++++++ prism/src/prism/PrismCL.java | 5 +++++ prism/src/prism/PrismSettings.java | 2 ++ prism/src/prism/StochModelChecker.java | 5 +++++ prism/src/sparse/PS_StochBoundedUntil.cc | 2 +- prism/src/sparse/PS_StochCumulReward.cc | 2 +- prism/src/sparse/PS_StochTransient.cc | 2 +- prism/src/sparse/PrismSparse.cc | 12 ++++++++++++ prism/src/sparse/PrismSparse.java | 10 ++++++++++ 25 files changed, 130 insertions(+), 9 deletions(-) diff --git a/prism/include/PrismHybrid.h b/prism/include/PrismHybrid.h index 590620b1..456a8bc9 100644 --- a/prism/include/PrismHybrid.h +++ b/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 diff --git a/prism/include/PrismHybridGlob.h b/prism/include/PrismHybridGlob.h index af92785e..56e82f60 100644 --- a/prism/include/PrismHybridGlob.h +++ b/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; diff --git a/prism/include/PrismMTBDD.h b/prism/include/PrismMTBDD.h index 8b2e6ab4..9151c699 100644 --- a/prism/include/PrismMTBDD.h +++ b/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 diff --git a/prism/include/PrismMTBDDGlob.h b/prism/include/PrismMTBDDGlob.h index 3cb4336e..306629a0 100644 --- a/prism/include/PrismMTBDDGlob.h +++ b/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; diff --git a/prism/include/PrismSparse.h b/prism/include/PrismSparse.h index 5d4bf17a..88b9fb29 100644 --- a/prism/include/PrismSparse.h +++ b/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 diff --git a/prism/include/PrismSparseGlob.h b/prism/include/PrismSparseGlob.h index 026df00b..14bebf12 100644 --- a/prism/include/PrismSparseGlob.h +++ b/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; diff --git a/prism/src/hybrid/PH_StochBoundedUntil.cc b/prism/src/hybrid/PH_StochBoundedUntil.cc index 396fbaa7..b09abeb7 100644 --- a/prism/src/hybrid/PH_StochBoundedUntil.cc +++ b/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++) { diff --git a/prism/src/hybrid/PH_StochCumulReward.cc b/prism/src/hybrid/PH_StochCumulReward.cc index c0389aab..1bce34ef 100644 --- a/prism/src/hybrid/PH_StochCumulReward.cc +++ b/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++) { diff --git a/prism/src/hybrid/PH_StochTransient.cc b/prism/src/hybrid/PH_StochTransient.cc index dd32b1ff..eede421a 100644 --- a/prism/src/hybrid/PH_StochTransient.cc +++ b/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++) { diff --git a/prism/src/hybrid/PrismHybrid.cc b/prism/src/hybrid/PrismHybrid.cc index 5dd3828f..081846cb 100644 --- a/prism/src/hybrid/PrismHybrid.cc +++ b/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 //------------------------------------------------------------------------------ diff --git a/prism/src/hybrid/PrismHybrid.java b/prism/src/hybrid/PrismHybrid.java index 82dd2117..314522d9 100644 --- a/prism/src/hybrid/PrismHybrid.java +++ b/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 diff --git a/prism/src/mtbdd/PM_StochBoundedUntil.cc b/prism/src/mtbdd/PM_StochBoundedUntil.cc index 4c83a9d7..1fe8bf3c 100644 --- a/prism/src/mtbdd/PM_StochBoundedUntil.cc +++ b/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; diff --git a/prism/src/mtbdd/PM_StochCumulReward.cc b/prism/src/mtbdd/PM_StochCumulReward.cc index 2948a135..df4a976f 100644 --- a/prism/src/mtbdd/PM_StochCumulReward.cc +++ b/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; diff --git a/prism/src/mtbdd/PM_StochTransient.cc b/prism/src/mtbdd/PM_StochTransient.cc index 869cf1ba..78fc582d 100644 --- a/prism/src/mtbdd/PM_StochTransient.cc +++ b/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; diff --git a/prism/src/mtbdd/PrismMTBDD.cc b/prism/src/mtbdd/PrismMTBDD.cc index 89ca8703..044231ec 100644 --- a/prism/src/mtbdd/PrismMTBDD.cc +++ b/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 //------------------------------------------------------------------------------ diff --git a/prism/src/mtbdd/PrismMTBDD.java b/prism/src/mtbdd/PrismMTBDD.java index c7150fe9..4d2d1e2a 100644 --- a/prism/src/mtbdd/PrismMTBDD.java +++ b/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 //------------------------------------------------------------------------------ diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 29820d80..d60c5488 100644 --- a/prism/src/prism/Prism.java +++ b/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()); diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index d5977b5f..e487920e 100644 --- a/prism/src/prism/PrismCL.java +++ b/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 ..................... Set memory limit (KB) (for hybrid engine) [default 1024]"); mainLog.println("-sbl ....................... Set number of levels (for hybrid engine) [default -1]"); diff --git a/prism/src/prism/PrismSettings.java b/prism/src/prism/PrismSettings.java index a15eb26c..d350c121 100644 --- a/prism/src/prism/PrismSettings.java +++ b/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." }, diff --git a/prism/src/prism/StochModelChecker.java b/prism/src/prism/StochModelChecker.java index dffd737a..edfdfd41 100644 --- a/prism/src/prism/StochModelChecker.java +++ b/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); diff --git a/prism/src/sparse/PS_StochBoundedUntil.cc b/prism/src/sparse/PS_StochBoundedUntil.cc index 4c88e88b..7d466fd8 100644 --- a/prism/src/sparse/PS_StochBoundedUntil.cc +++ 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++) { diff --git a/prism/src/sparse/PS_StochCumulReward.cc b/prism/src/sparse/PS_StochCumulReward.cc index 59a9e486..77e53648 100644 --- a/prism/src/sparse/PS_StochCumulReward.cc +++ b/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++) { diff --git a/prism/src/sparse/PS_StochTransient.cc b/prism/src/sparse/PS_StochTransient.cc index c516c919..ae81612d 100644 --- a/prism/src/sparse/PS_StochTransient.cc +++ b/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++) { diff --git a/prism/src/sparse/PrismSparse.cc b/prism/src/sparse/PrismSparse.cc index 54d41bb7..2200d58b 100644 --- a/prism/src/sparse/PrismSparse.cc +++ b/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 //------------------------------------------------------------------------------ diff --git a/prism/src/sparse/PrismSparse.java b/prism/src/sparse/PrismSparse.java index 1c06f084..41cbbda8 100644 --- a/prism/src/sparse/PrismSparse.java +++ b/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 //------------------------------------------------------------------------------