diff --git a/prism/include/PrismHybrid.h b/prism/include/PrismHybrid.h index dafe6d3b..06ce8c89 100644 --- a/prism/include/PrismHybrid.h +++ b/prism/include/PrismHybrid.h @@ -39,94 +39,6 @@ JNIEXPORT void JNICALL Java_hybrid_PrismHybrid_PH_1SetMainLog JNIEXPORT void JNICALL Java_hybrid_PrismHybrid_PH_1SetTechLog (JNIEnv *, jclass, jobject); -/* - * Class: hybrid_PrismHybrid - * Method: PH_SetLinEqMethod - * Signature: (I)V - */ -JNIEXPORT void JNICALL Java_hybrid_PrismHybrid_PH_1SetLinEqMethod - (JNIEnv *, jclass, jint); - -/* - * Class: hybrid_PrismHybrid - * Method: PH_SetLinEqMethodParam - * Signature: (D)V - */ -JNIEXPORT void JNICALL Java_hybrid_PrismHybrid_PH_1SetLinEqMethodParam - (JNIEnv *, jclass, jdouble); - -/* - * Class: hybrid_PrismHybrid - * Method: PH_SetTermCrit - * Signature: (I)V - */ -JNIEXPORT void JNICALL Java_hybrid_PrismHybrid_PH_1SetTermCrit - (JNIEnv *, jclass, jint); - -/* - * Class: hybrid_PrismHybrid - * Method: PH_SetTermCritParam - * Signature: (D)V - */ -JNIEXPORT void JNICALL Java_hybrid_PrismHybrid_PH_1SetTermCritParam - (JNIEnv *, jclass, jdouble); - -/* - * Class: hybrid_PrismHybrid - * Method: PH_SetMaxIters - * Signature: (I)V - */ -JNIEXPORT void JNICALL Java_hybrid_PrismHybrid_PH_1SetMaxIters - (JNIEnv *, jclass, jint); - -/* - * Class: hybrid_PrismHybrid - * Method: PH_SetSBMaxMem - * Signature: (I)V - */ -JNIEXPORT void JNICALL Java_hybrid_PrismHybrid_PH_1SetSBMaxMem - (JNIEnv *, jclass, jint); - -/* - * Class: hybrid_PrismHybrid - * Method: PH_SetNumSBLevels - * Signature: (I)V - */ -JNIEXPORT void JNICALL Java_hybrid_PrismHybrid_PH_1SetNumSBLevels - (JNIEnv *, jclass, jint); - -/* - * Class: hybrid_PrismHybrid - * Method: PH_SetSORMaxMem - * Signature: (I)V - */ -JNIEXPORT void JNICALL Java_hybrid_PrismHybrid_PH_1SetSORMaxMem - (JNIEnv *, jclass, jint); - -/* - * Class: hybrid_PrismHybrid - * Method: PH_SetNumSORLevels - * Signature: (I)V - */ -JNIEXPORT void JNICALL Java_hybrid_PrismHybrid_PH_1SetNumSORLevels - (JNIEnv *, jclass, jint); - -/* - * Class: hybrid_PrismHybrid - * Method: PH_SetCompact - * Signature: (Z)V - */ -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 b4d27abb..a11615be 100644 --- a/prism/include/PrismHybridGlob.h +++ b/prism/include/PrismHybridGlob.h @@ -28,25 +28,7 @@ #include #include #include - -//------------------------------------------------------------------------------ - -// constants - these need to match the definitions in prism/Prism.java - -const int LIN_EQ_METHOD_POWER = 1; -const int LIN_EQ_METHOD_JACOBI = 2; -const int LIN_EQ_METHOD_GAUSSSEIDEL = 3; -const int LIN_EQ_METHOD_BGAUSSSEIDEL = 4; -const int LIN_EQ_METHOD_PGAUSSSEIDEL = 5; -const int LIN_EQ_METHOD_BPGAUSSSEIDEL = 6; -const int LIN_EQ_METHOD_JOR = 7; -const int LIN_EQ_METHOD_SOR = 8; -const int LIN_EQ_METHOD_BSOR = 9; -const int LIN_EQ_METHOD_PSOR = 10; -const int LIN_EQ_METHOD_BPSOR = 11; - -const int TERM_CRIT_ABSOLUTE = 1; -const int TERM_CRIT_RELATIVE = 2; +#include "PrismNativeGlob.h" //------------------------------------------------------------------------------ @@ -55,27 +37,6 @@ const int TERM_CRIT_RELATIVE = 2; // cudd manager extern DdManager *ddman; -// numerical method stuff -extern int lin_eq_method; -extern double lin_eq_method_param; -extern int term_crit; -extern double term_crit_param; -extern int max_iters; - -// sparse bits info -extern int sb_max_mem; -extern int num_sb_levels; - -// blocks info -extern int sor_max_mem; -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 3af33868..a0653b40 100644 --- a/prism/include/PrismMTBDD.h +++ b/prism/include/PrismMTBDD.h @@ -39,54 +39,6 @@ JNIEXPORT void JNICALL Java_mtbdd_PrismMTBDD_PM_1SetMainLog JNIEXPORT void JNICALL Java_mtbdd_PrismMTBDD_PM_1SetTechLog (JNIEnv *, jclass, jobject); -/* - * Class: mtbdd_PrismMTBDD - * Method: PM_SetLinEqMethod - * Signature: (I)V - */ -JNIEXPORT void JNICALL Java_mtbdd_PrismMTBDD_PM_1SetLinEqMethod - (JNIEnv *, jclass, jint); - -/* - * Class: mtbdd_PrismMTBDD - * Method: PM_SetLinEqMethodParam - * Signature: (D)V - */ -JNIEXPORT void JNICALL Java_mtbdd_PrismMTBDD_PM_1SetLinEqMethodParam - (JNIEnv *, jclass, jdouble); - -/* - * Class: mtbdd_PrismMTBDD - * Method: PM_SetTermCrit - * Signature: (I)V - */ -JNIEXPORT void JNICALL Java_mtbdd_PrismMTBDD_PM_1SetTermCrit - (JNIEnv *, jclass, jint); - -/* - * Class: mtbdd_PrismMTBDD - * Method: PM_SetTermCritParam - * Signature: (D)V - */ -JNIEXPORT void JNICALL Java_mtbdd_PrismMTBDD_PM_1SetTermCritParam - (JNIEnv *, jclass, jdouble); - -/* - * Class: mtbdd_PrismMTBDD - * Method: PM_SetMaxIters - * Signature: (I)V - */ -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 8b591d67..801eb253 100644 --- a/prism/include/PrismMTBDDGlob.h +++ b/prism/include/PrismMTBDDGlob.h @@ -26,32 +26,7 @@ #include #include - -//------------------------------------------------------------------------------ - -// constants - these need to match the definitions in prism/Prism.java - -const int EXPORT_PLAIN = 1; -const int EXPORT_MATLAB = 2; -const int EXPORT_DOT = 3; -const int EXPORT_MRMC = 4; -const int EXPORT_ROWS = 5; -const int EXPORT_DOT_STATES = 6; - -const int LIN_EQ_METHOD_POWER = 1; -const int LIN_EQ_METHOD_JACOBI = 2; -const int LIN_EQ_METHOD_GAUSSSEIDEL = 3; -const int LIN_EQ_METHOD_BGAUSSSEIDEL = 4; -const int LIN_EQ_METHOD_PGAUSSSEIDEL = 5; -const int LIN_EQ_METHOD_BPGAUSSSEIDEL = 6; -const int LIN_EQ_METHOD_JOR = 7; -const int LIN_EQ_METHOD_SOR = 8; -const int LIN_EQ_METHOD_BSOR = 9; -const int LIN_EQ_METHOD_PSOR = 10; -const int LIN_EQ_METHOD_BPSOR = 11; - -const int TERM_CRIT_ABSOLUTE = 1; -const int TERM_CRIT_RELATIVE = 2; +#include "PrismNativeGlob.h" //------------------------------------------------------------------------------ @@ -60,16 +35,6 @@ const int TERM_CRIT_RELATIVE = 2; // cudd manager extern DdManager *ddman; -// numerical method stuff -extern int lin_eq_method; -extern double lin_eq_method_param; -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/PrismNative.h b/prism/include/PrismNative.h index 058835c6..b75715c5 100644 --- a/prism/include/PrismNative.h +++ b/prism/include/PrismNative.h @@ -7,6 +7,94 @@ #ifdef __cplusplus extern "C" { #endif +/* + * Class: prism_PrismNative + * Method: PN_SetCompact + * Signature: (Z)V + */ +JNIEXPORT void JNICALL Java_prism_PrismNative_PN_1SetCompact + (JNIEnv *, jclass, jboolean); + +/* + * Class: prism_PrismNative + * Method: PN_SetLinEqMethod + * Signature: (I)V + */ +JNIEXPORT void JNICALL Java_prism_PrismNative_PN_1SetLinEqMethod + (JNIEnv *, jclass, jint); + +/* + * Class: prism_PrismNative + * Method: PN_SetLinEqMethodParam + * Signature: (D)V + */ +JNIEXPORT void JNICALL Java_prism_PrismNative_PN_1SetLinEqMethodParam + (JNIEnv *, jclass, jdouble); + +/* + * Class: prism_PrismNative + * Method: PN_SetTermCrit + * Signature: (I)V + */ +JNIEXPORT void JNICALL Java_prism_PrismNative_PN_1SetTermCrit + (JNIEnv *, jclass, jint); + +/* + * Class: prism_PrismNative + * Method: PN_SetTermCritParam + * Signature: (D)V + */ +JNIEXPORT void JNICALL Java_prism_PrismNative_PN_1SetTermCritParam + (JNIEnv *, jclass, jdouble); + +/* + * Class: prism_PrismNative + * Method: PN_SetMaxIters + * Signature: (I)V + */ +JNIEXPORT void JNICALL Java_prism_PrismNative_PN_1SetMaxIters + (JNIEnv *, jclass, jint); + +/* + * Class: prism_PrismNative + * Method: PN_SetSBMaxMem + * Signature: (I)V + */ +JNIEXPORT void JNICALL Java_prism_PrismNative_PN_1SetSBMaxMem + (JNIEnv *, jclass, jint); + +/* + * Class: prism_PrismNative + * Method: PN_SetNumSBLevels + * Signature: (I)V + */ +JNIEXPORT void JNICALL Java_prism_PrismNative_PN_1SetNumSBLevels + (JNIEnv *, jclass, jint); + +/* + * Class: prism_PrismNative + * Method: PN_SetSORMaxMem + * Signature: (I)V + */ +JNIEXPORT void JNICALL Java_prism_PrismNative_PN_1SetSORMaxMem + (JNIEnv *, jclass, jint); + +/* + * Class: prism_PrismNative + * Method: PN_SetNumSORLevels + * Signature: (I)V + */ +JNIEXPORT void JNICALL Java_prism_PrismNative_PN_1SetNumSORLevels + (JNIEnv *, jclass, jint); + +/* + * Class: prism_PrismNative + * Method: PN_SetDoSSDetect + * Signature: (Z)V + */ +JNIEXPORT void JNICALL Java_prism_PrismNative_PN_1SetDoSSDetect + (JNIEnv *, jclass, jboolean); + /* * Class: prism_PrismNative * Method: PN_SetExportAdv diff --git a/prism/include/PrismNativeGlob.h b/prism/include/PrismNativeGlob.h index 93ed862d..31c7d705 100644 --- a/prism/include/PrismNativeGlob.h +++ b/prism/include/PrismNativeGlob.h @@ -24,6 +24,10 @@ // //============================================================================== +#ifndef PRISMNATIVEGLOB_H +#define PRISMNATIVEGLOB_H + +//------------------------------------------------------------------------------ #include // Flags for building Windows DLLs @@ -37,17 +41,59 @@ // Constants - these need to match the definitions in prism/Prism.java +const int EXPORT_PLAIN = 1; +const int EXPORT_MATLAB = 2; +const int EXPORT_DOT = 3; +const int EXPORT_MRMC = 4; +const int EXPORT_ROWS = 5; +const int EXPORT_DOT_STATES = 6; + +const int LIN_EQ_METHOD_POWER = 1; +const int LIN_EQ_METHOD_JACOBI = 2; +const int LIN_EQ_METHOD_GAUSSSEIDEL = 3; +const int LIN_EQ_METHOD_BGAUSSSEIDEL = 4; +const int LIN_EQ_METHOD_PGAUSSSEIDEL = 5; +const int LIN_EQ_METHOD_BPGAUSSSEIDEL = 6; +const int LIN_EQ_METHOD_JOR = 7; +const int LIN_EQ_METHOD_SOR = 8; +const int LIN_EQ_METHOD_BSOR = 9; +const int LIN_EQ_METHOD_PSOR = 10; +const int LIN_EQ_METHOD_BPSOR = 11; + +const int TERM_CRIT_ABSOLUTE = 1; +const int TERM_CRIT_RELATIVE = 2; + const int EXPORT_ADV_NONE = 1; const int EXPORT_ADV_DTMC = 2; const int EXPORT_ADV_MDP = 3; //------------------------------------------------------------------------------ -// External refs to global variables +// External refs to global variables for options -// adversary export mode +// numerical method stuff +EXPORT extern int lin_eq_method; +EXPORT extern double lin_eq_method_param; +EXPORT extern int term_crit; +EXPORT extern double term_crit_param; +EXPORT extern int max_iters; +// use "compact modified" sparse matrix storage? +EXPORT extern bool compact; +// sparse bits info +EXPORT extern int sb_max_mem; +EXPORT extern int num_sb_levels; +// hybrid sor info +EXPORT extern int sor_max_mem; +EXPORT extern int num_sor_levels; +// use steady-state detection for transient computation? +EXPORT extern bool do_ss_detect; +// adversary EXPORT extern mode EXPORT extern int export_adv; // adversary export filename EXPORT extern const char *export_adv_filename; //------------------------------------------------------------------------------ + +#endif + +//------------------------------------------------------------------------------ diff --git a/prism/include/PrismSparse.h b/prism/include/PrismSparse.h index efeee3f0..ceffdc31 100644 --- a/prism/include/PrismSparse.h +++ b/prism/include/PrismSparse.h @@ -39,62 +39,6 @@ JNIEXPORT void JNICALL Java_sparse_PrismSparse_PS_1SetMainLog JNIEXPORT void JNICALL Java_sparse_PrismSparse_PS_1SetTechLog (JNIEnv *, jclass, jobject); -/* - * Class: sparse_PrismSparse - * Method: PS_SetLinEqMethod - * Signature: (I)V - */ -JNIEXPORT void JNICALL Java_sparse_PrismSparse_PS_1SetLinEqMethod - (JNIEnv *, jclass, jint); - -/* - * Class: sparse_PrismSparse - * Method: PS_SetLinEqMethodParam - * Signature: (D)V - */ -JNIEXPORT void JNICALL Java_sparse_PrismSparse_PS_1SetLinEqMethodParam - (JNIEnv *, jclass, jdouble); - -/* - * Class: sparse_PrismSparse - * Method: PS_SetTermCrit - * Signature: (I)V - */ -JNIEXPORT void JNICALL Java_sparse_PrismSparse_PS_1SetTermCrit - (JNIEnv *, jclass, jint); - -/* - * Class: sparse_PrismSparse - * Method: PS_SetTermCritParam - * Signature: (D)V - */ -JNIEXPORT void JNICALL Java_sparse_PrismSparse_PS_1SetTermCritParam - (JNIEnv *, jclass, jdouble); - -/* - * Class: sparse_PrismSparse - * Method: PS_SetMaxIters - * Signature: (I)V - */ -JNIEXPORT void JNICALL Java_sparse_PrismSparse_PS_1SetMaxIters - (JNIEnv *, jclass, jint); - -/* - * Class: sparse_PrismSparse - * Method: PS_SetCompact - * Signature: (Z)V - */ -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 f117ac56..04e9d4fc 100644 --- a/prism/include/PrismSparseGlob.h +++ b/prism/include/PrismSparseGlob.h @@ -26,32 +26,7 @@ #include #include - -//------------------------------------------------------------------------------ - -// constants - these need to match the definitions in prism/Prism.java - -const int EXPORT_PLAIN = 1; -const int EXPORT_MATLAB = 2; -const int EXPORT_DOT = 3; -const int EXPORT_MRMC = 4; -const int EXPORT_ROWS = 5; -const int EXPORT_DOT_STATES = 6; - -const int LIN_EQ_METHOD_POWER = 1; -const int LIN_EQ_METHOD_JACOBI = 2; -const int LIN_EQ_METHOD_GAUSSSEIDEL = 3; -const int LIN_EQ_METHOD_BGAUSSSEIDEL = 4; -const int LIN_EQ_METHOD_PGAUSSSEIDEL = 5; -const int LIN_EQ_METHOD_BPGAUSSSEIDEL = 6; -const int LIN_EQ_METHOD_JOR = 7; -const int LIN_EQ_METHOD_SOR = 8; -const int LIN_EQ_METHOD_BSOR = 9; -const int LIN_EQ_METHOD_PSOR = 10; -const int LIN_EQ_METHOD_BPSOR = 11; - -const int TERM_CRIT_ABSOLUTE = 1; -const int TERM_CRIT_RELATIVE = 2; +#include "PrismNativeGlob.h" //------------------------------------------------------------------------------ @@ -60,19 +35,6 @@ const int TERM_CRIT_RELATIVE = 2; // cudd manager extern DdManager *ddman; -// numerical method stuff -extern int lin_eq_method; -extern double lin_eq_method_param; -extern int term_crit; -extern double term_crit_param; -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/PrismHybrid.cc b/prism/src/hybrid/PrismHybrid.cc index b649f13d..fe340ff7 100644 --- a/prism/src/hybrid/PrismHybrid.cc +++ b/prism/src/hybrid/PrismHybrid.cc @@ -57,27 +57,6 @@ static jmethodID main_log_mid = NULL; static jmethodID main_log_warn = NULL; static jmethodID tech_log_mid = NULL; -// numerical method stuff -int lin_eq_method; -double lin_eq_method_param; -int term_crit; -double term_crit_param; -int max_iters; - -// sparse bits info -int sb_max_mem; -int num_sb_levels; - -// hybrid sor info -int sor_max_mem; -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]; @@ -210,93 +189,6 @@ void PH_PrintMemoryToMainLog(JNIEnv *env, const char *before, double mem, const } } -//------------------------------------------------------------------------------ -// numerical method stuff -//------------------------------------------------------------------------------ - -JNIEXPORT void JNICALL Java_hybrid_PrismHybrid_PH_1SetLinEqMethod(JNIEnv *env, jclass cls, jint i) -{ - lin_eq_method = i; -} - -//------------------------------------------------------------------------------ - -JNIEXPORT void JNICALL Java_hybrid_PrismHybrid_PH_1SetLinEqMethodParam(JNIEnv *env, jclass cls, jdouble d) -{ - lin_eq_method_param = d; -} - -//------------------------------------------------------------------------------ - -JNIEXPORT void JNICALL Java_hybrid_PrismHybrid_PH_1SetTermCrit(JNIEnv *env, jclass cls, jint i) -{ - term_crit = i; -} - -//------------------------------------------------------------------------------ - -JNIEXPORT void JNICALL Java_hybrid_PrismHybrid_PH_1SetTermCritParam(JNIEnv *env, jclass cls, jdouble d) -{ - term_crit_param = d; -} - -//------------------------------------------------------------------------------ - -JNIEXPORT void JNICALL Java_hybrid_PrismHybrid_PH_1SetMaxIters(JNIEnv *env, jclass cls, jint i) -{ - max_iters = i; -} - -//------------------------------------------------------------------------------ -// sparse bits info -//------------------------------------------------------------------------------ - -JNIEXPORT void JNICALL Java_hybrid_PrismHybrid_PH_1SetSBMaxMem(JNIEnv *env, jclass cls, jint sbmm) -{ - sb_max_mem = sbmm; -} - -//------------------------------------------------------------------------------ - -JNIEXPORT void JNICALL Java_hybrid_PrismHybrid_PH_1SetNumSBLevels(JNIEnv *env, jclass cls, jint nsbl) -{ - num_sb_levels = nsbl; -} - -//------------------------------------------------------------------------------ -// hybrid sor info -//------------------------------------------------------------------------------ - -JNIEXPORT void JNICALL Java_hybrid_PrismHybrid_PH_1SetSORMaxMem(JNIEnv *env, jclass cls, jint smm) -{ - sor_max_mem = smm; -} - -//------------------------------------------------------------------------------ - -JNIEXPORT void JNICALL Java_hybrid_PrismHybrid_PH_1SetNumSORLevels(JNIEnv *env, jclass cls, jint nsl) -{ - num_sor_levels = nsl; -} - -//------------------------------------------------------------------------------ -// use "compact modified" sparse matrix storage? -//------------------------------------------------------------------------------ - -JNIEXPORT void JNICALL Java_hybrid_PrismHybrid_PH_1SetCompact(JNIEnv *env, jclass cls, jboolean b) -{ - 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 b4edebe8..c35d912f 100644 --- a/prism/src/hybrid/PrismHybrid.java +++ b/prism/src/hybrid/PrismHybrid.java @@ -113,92 +113,6 @@ public class PrismHybrid PH_SetTechLog(log); } - //------------------------------------------------------------------------------ - // numerical method stuff - //------------------------------------------------------------------------------ - - private static native void PH_SetLinEqMethod(int i); - public static void setLinEqMethod(int i) - { - PH_SetLinEqMethod(i); - } - - private static native void PH_SetLinEqMethodParam(double d); - public static void setLinEqMethodParam(double d) - { - PH_SetLinEqMethodParam(d); - } - - private static native void PH_SetTermCrit(int i); - public static void setTermCrit(int i) - { - PH_SetTermCrit(i); - } - - private static native void PH_SetTermCritParam(double d); - public static void setTermCritParam(double d) - { - PH_SetTermCritParam(d); - } - - private static native void PH_SetMaxIters(int i); - public static void setMaxIters(int i) - { - PH_SetMaxIters(i); - } - - //------------------------------------------------------------------------------ - // sparse bits info - //------------------------------------------------------------------------------ - - private static native void PH_SetSBMaxMem(int i); - public static void setSBMaxMem(int i) - { - PH_SetSBMaxMem(i); - } - - private static native void PH_SetNumSBLevels(int i); - public static void setNumSBLevels(int i) - { - PH_SetNumSBLevels(i); - } - - //------------------------------------------------------------------------------ - // hybrid sor info - //------------------------------------------------------------------------------ - - private static native void PH_SetSORMaxMem(int i); - public static void setSORMaxMem(int i) - { - PH_SetSORMaxMem(i); - } - - private static native void PH_SetNumSORLevels(int i); - public static void setNumSORLevels(int i) - { - PH_SetNumSORLevels(i); - } - - //------------------------------------------------------------------------------ - // use "compact modified" sparse matrix storage? - //------------------------------------------------------------------------------ - - private static native void PH_SetCompact(boolean b); - public static void setCompact(boolean b) - { - 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/PrismMTBDD.cc b/prism/src/mtbdd/PrismMTBDD.cc index e92eb9ce..bded3276 100644 --- a/prism/src/mtbdd/PrismMTBDD.cc +++ b/prism/src/mtbdd/PrismMTBDD.cc @@ -57,21 +57,11 @@ static jmethodID main_log_mid = NULL; static jmethodID main_log_warn = NULL; static jmethodID tech_log_mid = NULL; -// numerical method stuff -int lin_eq_method; -double lin_eq_method_param; -int term_crit; -double term_crit_param; -int max_iters; - // export stuff 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]; @@ -178,43 +168,6 @@ void PM_PrintToTechLog(JNIEnv *env, const char *str, ...) printf("%s", full_string); } -//------------------------------------------------------------------------------ -// numerical method stuff -//------------------------------------------------------------------------------ - -JNIEXPORT void JNICALL Java_mtbdd_PrismMTBDD_PM_1SetLinEqMethod(JNIEnv *env, jclass cls, jint i) -{ - lin_eq_method = i; -} - -//------------------------------------------------------------------------------ - -JNIEXPORT void JNICALL Java_mtbdd_PrismMTBDD_PM_1SetLinEqMethodParam(JNIEnv *env, jclass cls, jdouble d) -{ - lin_eq_method_param = d; -} - -//------------------------------------------------------------------------------ - -JNIEXPORT void JNICALL Java_mtbdd_PrismMTBDD_PM_1SetTermCrit(JNIEnv *env, jclass cls, jint i) -{ - term_crit = i; -} - -//------------------------------------------------------------------------------ - -JNIEXPORT void JNICALL Java_mtbdd_PrismMTBDD_PM_1SetTermCritParam(JNIEnv *env, jclass cls, jdouble d) -{ - term_crit_param = d; -} - -//------------------------------------------------------------------------------ - -JNIEXPORT void JNICALL Java_mtbdd_PrismMTBDD_PM_1SetMaxIters(JNIEnv *env, jclass cls, jint i) -{ - max_iters = i; -} - //------------------------------------------------------------------------------ // export stuff //------------------------------------------------------------------------------ @@ -260,15 +213,6 @@ void export_string(const 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 73b0001d..fb688a6b 100644 --- a/prism/src/mtbdd/PrismMTBDD.java +++ b/prism/src/mtbdd/PrismMTBDD.java @@ -115,50 +115,6 @@ public class PrismMTBDD PM_SetTechLog(log); } - //------------------------------------------------------------------------------ - // numerical method stuff - //------------------------------------------------------------------------------ - - private static native void PM_SetLinEqMethod(int i); - public static void setLinEqMethod(int i) - { - PM_SetLinEqMethod(i); - } - - private static native void PM_SetLinEqMethodParam(double d); - public static void setLinEqMethodParam(double d) - { - PM_SetLinEqMethodParam(d); - } - - private static native void PM_SetTermCrit(int i); - public static void setTermCrit(int i) - { - PM_SetTermCrit(i); - } - - private static native void PM_SetTermCritParam(double d); - public static void setTermCritParam(double d) - { - PM_SetTermCritParam(d); - } - - private static native void PM_SetMaxIters(int i); - public static void setMaxIters(int i) - { - 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/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 76daef1d..b1880ca4 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -93,28 +93,15 @@ public class NondetModelChecker extends NonProbModelChecker } } - // Pass some options onto engines/native code. + // Pass some options onto native code. + PrismNative.setCompact(prism.getCompact()); + PrismNative.setTermCrit(prism.getTermCrit()); + PrismNative.setTermCritParam(prism.getTermCritParam()); + PrismNative.setMaxIters(prism.getMaxIters()); + PrismNative.setSBMaxMem(prism.getSBMaxMem()); + PrismNative.setNumSBLevels(prism.getNumSBLevels()); PrismNative.setExportAdv(prism.getExportAdv()); PrismNative.setExportAdvFilename(prism.getExportAdvFilename()); - switch (engine) { - case Prism.MTBDD: - PrismMTBDD.setTermCrit(prism.getTermCrit()); - PrismMTBDD.setTermCritParam(prism.getTermCritParam()); - PrismMTBDD.setMaxIters(prism.getMaxIters()); - break; - case Prism.SPARSE: - PrismSparse.setTermCrit(prism.getTermCrit()); - PrismSparse.setTermCritParam(prism.getTermCritParam()); - PrismSparse.setMaxIters(prism.getMaxIters()); - PrismSparse.setCompact(prism.getCompact()); - case Prism.HYBRID: - PrismHybrid.setTermCrit(prism.getTermCrit()); - PrismHybrid.setTermCritParam(prism.getTermCritParam()); - PrismHybrid.setMaxIters(prism.getMaxIters()); - PrismHybrid.setCompact(prism.getCompact()); - PrismHybrid.setSBMaxMem(prism.getSBMaxMem()); - PrismHybrid.setNumSBLevels(prism.getNumSBLevels()); - } } // ----------------------------------------------------------------------------------- diff --git a/prism/src/prism/PrismNative.cc b/prism/src/prism/PrismNative.cc index a551dbcf..b3c95a71 100644 --- a/prism/src/prism/PrismNative.cc +++ b/prism/src/prism/PrismNative.cc @@ -31,6 +31,24 @@ #include "PrismNativeGlob.h" #include "jnipointer.h" +// options + +// numerical method stuff +EXPORT int lin_eq_method; +EXPORT double lin_eq_method_param; +EXPORT int term_crit; +EXPORT double term_crit_param; +EXPORT int max_iters; +// use "compact modified" sparse matrix storage? +EXPORT bool compact; +// sparse bits info +EXPORT int sb_max_mem; +EXPORT int num_sb_levels; +// hybrid sor info +EXPORT int sor_max_mem; +EXPORT int num_sor_levels; +// use steady-state detection for transient computation? +EXPORT bool do_ss_detect; // adversary export mode EXPORT int export_adv; // adversary export filename @@ -40,6 +58,83 @@ EXPORT const char *export_adv_filename; // Set methods for options in native code //------------------------------------------------------------------------------ +JNIEXPORT void JNICALL Java_prism_PrismNative_PN_1SetCompact(JNIEnv *env, jclass cls, jboolean b) +{ + compact = b; +} + +//------------------------------------------------------------------------------ + +JNIEXPORT void JNICALL Java_prism_PrismNative_PN_1SetLinEqMethod(JNIEnv *env, jclass cls, jint i) +{ + lin_eq_method = i; +} + +//------------------------------------------------------------------------------ + +JNIEXPORT void JNICALL Java_prism_PrismNative_PN_1SetLinEqMethodParam(JNIEnv *env, jclass cls, jdouble d) +{ + lin_eq_method_param = d; +} + +//------------------------------------------------------------------------------ + +JNIEXPORT void JNICALL Java_prism_PrismNative_PN_1SetTermCrit(JNIEnv *env, jclass cls, jint i) +{ + term_crit = i; +} + +//------------------------------------------------------------------------------ + +JNIEXPORT void JNICALL Java_prism_PrismNative_PN_1SetTermCritParam(JNIEnv *env, jclass cls, jdouble d) +{ + term_crit_param = d; +} + +//------------------------------------------------------------------------------ + +JNIEXPORT void JNICALL Java_prism_PrismNative_PN_1SetMaxIters(JNIEnv *env, jclass cls, jint i) +{ + max_iters = i; +} + +//------------------------------------------------------------------------------ + +JNIEXPORT void JNICALL Java_prism_PrismNative_PN_1SetSBMaxMem(JNIEnv *env, jclass cls, jint sbmm) +{ + sb_max_mem = sbmm; +} + +//------------------------------------------------------------------------------ + +JNIEXPORT void JNICALL Java_prism_PrismNative_PN_1SetNumSBLevels(JNIEnv *env, jclass cls, jint nsbl) +{ + num_sb_levels = nsbl; +} + +//------------------------------------------------------------------------------ + +JNIEXPORT void JNICALL Java_prism_PrismNative_PN_1SetSORMaxMem(JNIEnv *env, jclass cls, jint smm) +{ + sor_max_mem = smm; +} + +//------------------------------------------------------------------------------ + +JNIEXPORT void JNICALL Java_prism_PrismNative_PN_1SetNumSORLevels(JNIEnv *env, jclass cls, jint nsl) +{ + num_sor_levels = nsl; +} + +//------------------------------------------------------------------------------ + +JNIEXPORT void JNICALL Java_prism_PrismNative_PN_1SetDoSSDetect(JNIEnv *env, jclass cls, jboolean b) +{ + do_ss_detect = b; +} + +//------------------------------------------------------------------------------ + JNIEXPORT void JNICALL Java_prism_PrismNative_PN_1SetExportAdv(JNIEnv *env, jclass cls, jint i) { export_adv = i; diff --git a/prism/src/prism/PrismNative.java b/prism/src/prism/PrismNative.java index 72c77aed..3a1676f6 100644 --- a/prism/src/prism/PrismNative.java +++ b/prism/src/prism/PrismNative.java @@ -44,7 +44,74 @@ public class PrismNative } } - // Mode/filename for export of adversaries + // Options passing + + private static native void PN_SetCompact(boolean b); + public static void setCompact(boolean b) + { + PN_SetCompact(b); + } + + private static native void PN_SetLinEqMethod(int i); + public static void setLinEqMethod(int i) + { + PN_SetLinEqMethod(i); + } + + private static native void PN_SetLinEqMethodParam(double d); + public static void setLinEqMethodParam(double d) + { + PN_SetLinEqMethodParam(d); + } + + private static native void PN_SetTermCrit(int i); + public static void setTermCrit(int i) + { + PN_SetTermCrit(i); + } + + private static native void PN_SetTermCritParam(double d); + public static void setTermCritParam(double d) + { + PN_SetTermCritParam(d); + } + + private static native void PN_SetMaxIters(int i); + public static void setMaxIters(int i) + { + PN_SetMaxIters(i); + } + + private static native void PN_SetSBMaxMem(int i); + public static void setSBMaxMem(int i) + { + PN_SetSBMaxMem(i); + } + + private static native void PN_SetNumSBLevels(int i); + public static void setNumSBLevels(int i) + { + PN_SetNumSBLevels(i); + } + + private static native void PN_SetSORMaxMem(int i); + public static void setSORMaxMem(int i) + { + PN_SetSORMaxMem(i); + } + + private static native void PN_SetNumSORLevels(int i); + public static void setNumSORLevels(int i) + { + PN_SetNumSORLevels(i); + } + + private static native void PN_SetDoSSDetect(boolean b); + public static void setDoSSDetect(boolean b) + { + PN_SetDoSSDetect(b); + } + private static native void PN_SetExportAdv(int i); public static void setExportAdv(int i) { diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index 118971de..002d895a 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/prism/src/prism/ProbModelChecker.java @@ -71,41 +71,24 @@ public class ProbModelChecker extends NonProbModelChecker model = (ProbModel) m; // Inherit some options from parent Prism object. - // Store locally and/or pass onto engines. + // Store locally and/or pass onto native code. precomp = prism.getPrecomp(); prob0 = prism.getProb0(); prob1 = prism.getProb1(); bsccComp = prism.getBSCCComp(); - switch (engine) { - case Prism.MTBDD: - PrismMTBDD.setLinEqMethod(prism.getLinEqMethod()); - PrismMTBDD.setLinEqMethodParam(prism.getLinEqMethodParam()); - PrismMTBDD.setTermCrit(prism.getTermCrit()); - PrismMTBDD.setTermCritParam(prism.getTermCritParam()); - PrismMTBDD.setMaxIters(prism.getMaxIters()); - PrismMTBDD.setDoSSDetect(prism.getDoSSDetect()); - break; - case Prism.SPARSE: - PrismSparse.setLinEqMethod(prism.getLinEqMethod()); - PrismSparse.setLinEqMethodParam(prism.getLinEqMethodParam()); - PrismSparse.setTermCrit(prism.getTermCrit()); - PrismSparse.setTermCritParam(prism.getTermCritParam()); - PrismSparse.setMaxIters(prism.getMaxIters()); - PrismSparse.setCompact(prism.getCompact()); - PrismSparse.setDoSSDetect(prism.getDoSSDetect()); - case Prism.HYBRID: - PrismHybrid.setLinEqMethod(prism.getLinEqMethod()); - PrismHybrid.setLinEqMethodParam(prism.getLinEqMethodParam()); - PrismHybrid.setTermCrit(prism.getTermCrit()); - PrismHybrid.setTermCritParam(prism.getTermCritParam()); - PrismHybrid.setMaxIters(prism.getMaxIters()); - PrismHybrid.setCompact(prism.getCompact()); - PrismHybrid.setSBMaxMem(prism.getSBMaxMem()); - PrismHybrid.setNumSBLevels(prism.getNumSBLevels()); - PrismHybrid.setSORMaxMem(prism.getSORMaxMem()); - PrismHybrid.setNumSORLevels(prism.getNumSORLevels()); - PrismHybrid.setDoSSDetect(prism.getDoSSDetect()); - } + PrismNative.setCompact(prism.getCompact()); + PrismNative.setLinEqMethod(prism.getLinEqMethod()); + PrismNative.setLinEqMethodParam(prism.getLinEqMethodParam()); + PrismNative.setTermCrit(prism.getTermCrit()); + PrismNative.setTermCritParam(prism.getTermCritParam()); + PrismNative.setMaxIters(prism.getMaxIters()); + PrismNative.setSBMaxMem(prism.getSBMaxMem()); + PrismNative.setNumSBLevels(prism.getNumSBLevels()); + PrismNative.setSORMaxMem(prism.getSORMaxMem()); + PrismNative.setNumSORLevels(prism.getNumSORLevels()); + PrismNative.setDoSSDetect(prism.getDoSSDetect()); + PrismNative.setExportAdv(prism.getExportAdv()); + PrismNative.setExportAdvFilename(prism.getExportAdvFilename()); } // Override-able "Constructor" diff --git a/prism/src/sparse/PrismSparse.cc b/prism/src/sparse/PrismSparse.cc index 27f78dff..7d47b6a2 100644 --- a/prism/src/sparse/PrismSparse.cc +++ b/prism/src/sparse/PrismSparse.cc @@ -56,19 +56,6 @@ static jmethodID main_log_mid = NULL; static jmethodID main_log_warn = NULL; static jmethodID tech_log_mid = NULL; -// numerical method stuff -int lin_eq_method; -double lin_eq_method_param; -int term_crit; -double term_crit_param; -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; @@ -203,52 +190,6 @@ void PS_PrintMemoryToMainLog(JNIEnv *env, const char *before, double mem, const } } -//------------------------------------------------------------------------------ -// numerical method stuff -//------------------------------------------------------------------------------ - -JNIEXPORT void JNICALL Java_sparse_PrismSparse_PS_1SetLinEqMethod(JNIEnv *env, jclass cls, jint i) -{ - lin_eq_method = i; -} - -//------------------------------------------------------------------------------ - -JNIEXPORT void JNICALL Java_sparse_PrismSparse_PS_1SetLinEqMethodParam(JNIEnv *env, jclass cls, jdouble d) -{ - lin_eq_method_param = d; -} - -//------------------------------------------------------------------------------ - -JNIEXPORT void JNICALL Java_sparse_PrismSparse_PS_1SetTermCrit(JNIEnv *env, jclass cls, jint i) -{ - term_crit = i; -} - -//------------------------------------------------------------------------------ - -JNIEXPORT void JNICALL Java_sparse_PrismSparse_PS_1SetTermCritParam(JNIEnv *env, jclass cls, jdouble d) -{ - term_crit_param = d; -} - -//------------------------------------------------------------------------------ - -JNIEXPORT void JNICALL Java_sparse_PrismSparse_PS_1SetMaxIters(JNIEnv *env, jclass cls, jint i) -{ - max_iters = i; -} - -//------------------------------------------------------------------------------ -// use "compact modified" sparse matrix storage? -//------------------------------------------------------------------------------ - -JNIEXPORT void JNICALL Java_sparse_PrismSparse_PS_1SetCompact(JNIEnv *env, jclass cls, jboolean b) -{ - compact = b; -} - //------------------------------------------------------------------------------ // export stuff //------------------------------------------------------------------------------ diff --git a/prism/src/sparse/PrismSparse.java b/prism/src/sparse/PrismSparse.java index 8bbc5dcc..fdf89d9c 100644 --- a/prism/src/sparse/PrismSparse.java +++ b/prism/src/sparse/PrismSparse.java @@ -116,60 +116,6 @@ public class PrismSparse PS_SetTechLog(log); } - //------------------------------------------------------------------------------ - // numerical method stuff - //---------------------------------------------------------------------------------------------- - - private static native void PS_SetLinEqMethod(int i); - public static void setLinEqMethod(int i) - { - PS_SetLinEqMethod(i); - } - - private static native void PS_SetLinEqMethodParam(double d); - public static void setLinEqMethodParam(double d) - { - PS_SetLinEqMethodParam(d); - } - - private static native void PS_SetTermCrit(int i); - public static void setTermCrit(int i) - { - PS_SetTermCrit(i); - } - - private static native void PS_SetTermCritParam(double d); - public static void setTermCritParam(double d) - { - PS_SetTermCritParam(d); - } - - private static native void PS_SetMaxIters(int i); - public static void setMaxIters(int i) - { - PS_SetMaxIters(i); - } - - //------------------------------------------------------------------------------ - // use "compact modified" sparse matrix storage? - //------------------------------------------------------------------------------ - - private static native void PS_SetCompact(boolean b); - public static void setCompact(boolean b) - { - 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 //------------------------------------------------------------------------------