s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Move most native code options from engine shared libraries to prism library. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4277 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 14 years ago
parent
2451c25702
commit
3e4c617a81
18 changed files with 323 additions and 768 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 88
      prism/include/PrismHybrid.h
  2. 41
      prism/include/PrismHybridGlob.h
  3. 48
      prism/include/PrismMTBDD.h
  4. 37
      prism/include/PrismMTBDDGlob.h
  5. 88
      prism/include/PrismNative.h
  6. 50
      prism/include/PrismNativeGlob.h
  7. 56
      prism/include/PrismSparse.h
  8. 40
      prism/include/PrismSparseGlob.h
  9. 108
      prism/src/hybrid/PrismHybrid.cc
  10. 86
      prism/src/hybrid/PrismHybrid.java
  11. 56
      prism/src/mtbdd/PrismMTBDD.cc
  12. 44
      prism/src/mtbdd/PrismMTBDD.java
  13. 27
      prism/src/prism/NondetModelChecker.java
  14. 95
      prism/src/prism/PrismNative.cc
  15. 69
      prism/src/prism/PrismNative.java
  16. 45
      prism/src/prism/ProbModelChecker.java
  17. 59
      prism/src/sparse/PrismSparse.cc
  18. 54
      prism/src/sparse/PrismSparse.java

88
prism/include/PrismHybrid.h
View File

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

41
prism/include/PrismHybridGlob.h
View File

@ -28,25 +28,7 @@
#include <jni.h>
#include <cudd.h>
#include <dd.h>
//------------------------------------------------------------------------------
// 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;

48
prism/include/PrismMTBDD.h
View File

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

37
prism/include/PrismMTBDDGlob.h
View File

@ -26,32 +26,7 @@
#include <stdarg.h>
#include <jni.h>
//------------------------------------------------------------------------------
// 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;

88
prism/include/PrismNative.h
View File

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

50
prism/include/PrismNativeGlob.h
View File

@ -24,6 +24,10 @@
//
//==============================================================================
#ifndef PRISMNATIVEGLOB_H
#define PRISMNATIVEGLOB_H
//------------------------------------------------------------------------------
#include <jni.h>
// 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
//------------------------------------------------------------------------------

56
prism/include/PrismSparse.h
View File

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

40
prism/include/PrismSparseGlob.h
View File

@ -26,32 +26,7 @@
#include <stdarg.h>
#include <jni.h>
//------------------------------------------------------------------------------
// 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;

108
prism/src/hybrid/PrismHybrid.cc
View File

@ -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
//------------------------------------------------------------------------------

86
prism/src/hybrid/PrismHybrid.java
View File

@ -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
//------------------------------------------------------------------------------

56
prism/src/mtbdd/PrismMTBDD.cc
View File

@ -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
//------------------------------------------------------------------------------

44
prism/src/mtbdd/PrismMTBDD.java
View File

@ -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
//------------------------------------------------------------------------------

27
prism/src/prism/NondetModelChecker.java
View File

@ -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());
}
}
// -----------------------------------------------------------------------------------

95
prism/src/prism/PrismNative.cc
View File

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

69
prism/src/prism/PrismNative.java
View File

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

45
prism/src/prism/ProbModelChecker.java
View File

@ -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"

59
prism/src/sparse/PrismSparse.cc
View File

@ -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
//------------------------------------------------------------------------------

54
prism/src/sparse/PrismSparse.java
View File

@ -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
//------------------------------------------------------------------------------

Write Preview
Loading…
Cancel
Save