From c1e24408ae326fe00c21ab5885d2f0e158c698d2 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sun, 19 Feb 2012 18:27:04 +0000 Subject: [PATCH] New (hidden) options for different symbolic reachability methods (-frontier, -bfs). Also: new way to read options from C++ code: PrismNative stores reference to Prism object which is then queried. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4663 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/include/PrismMTBDD.h | 4 +-- prism/include/PrismNative.h | 16 ++++++++++ prism/include/PrismNativeGlob.h | 10 ++++++- prism/src/mtbdd/PM_Reachability.cc | 15 +++++----- prism/src/mtbdd/PrismMTBDD.java | 7 ++--- prism/src/prism/ExplicitFiles2MTBDD.java | 2 +- prism/src/prism/ExplicitModel2MTBDD.java | 2 +- prism/src/prism/LTLModelChecker.java | 4 +-- prism/src/prism/Model.java | 1 - prism/src/prism/Modules2MTBDD.java | 2 +- prism/src/prism/NondetModel.java | 4 +-- prism/src/prism/Prism.java | 22 ++++++++++++-- prism/src/prism/PrismCL.java | 7 +++++ prism/src/prism/PrismNative.cc | 38 +++++++++++++++++++++++- prism/src/prism/PrismNative.java | 29 ++++++++++++++++++ prism/src/prism/ProbModel.java | 7 +---- 16 files changed, 139 insertions(+), 31 deletions(-) diff --git a/prism/include/PrismMTBDD.h b/prism/include/PrismMTBDD.h index a0653b40..94e39ef9 100644 --- a/prism/include/PrismMTBDD.h +++ b/prism/include/PrismMTBDD.h @@ -50,10 +50,10 @@ JNIEXPORT jstring JNICALL Java_mtbdd_PrismMTBDD_PM_1GetErrorMessage /* * Class: mtbdd_PrismMTBDD * Method: PM_Reachability - * Signature: (JJIJIJI)J + * Signature: (JJIJIJLprism/Prism;)J */ JNIEXPORT jlong JNICALL Java_mtbdd_PrismMTBDD_PM_1Reachability - (JNIEnv *, jclass, jlong, jlong, jint, jlong, jint, jlong, jint); + (JNIEnv *, jclass, jlong, jlong, jint, jlong, jint, jlong, jobject); /* * Class: mtbdd_PrismMTBDD diff --git a/prism/include/PrismNative.h b/prism/include/PrismNative.h index b75715c5..e8ed62e7 100644 --- a/prism/include/PrismNative.h +++ b/prism/include/PrismNative.h @@ -7,6 +7,22 @@ #ifdef __cplusplus extern "C" { #endif +/* + * Class: prism_PrismNative + * Method: PN_FreeGlobalRefs + * Signature: ()V + */ +JNIEXPORT void JNICALL Java_prism_PrismNative_PN_1FreeGlobalRefs + (JNIEnv *, jclass); + +/* + * Class: prism_PrismNative + * Method: PN_SetPrism + * Signature: (Lprism/Prism;)V + */ +JNIEXPORT void JNICALL Java_prism_PrismNative_PN_1SetPrism + (JNIEnv *, jclass, jobject); + /* * Class: prism_PrismNative * Method: PN_SetCompact diff --git a/prism/include/PrismNativeGlob.h b/prism/include/PrismNativeGlob.h index 31c7d705..54e820bc 100644 --- a/prism/include/PrismNativeGlob.h +++ b/prism/include/PrismNativeGlob.h @@ -67,10 +67,18 @@ const int EXPORT_ADV_NONE = 1; const int EXPORT_ADV_DTMC = 2; const int EXPORT_ADV_MDP = 3; +const int REACH_BFS = 1; +const int REACH_FRONTIER = 2; + //------------------------------------------------------------------------------ -// External refs to global variables for options +// External refs to global variables + +// Prism object +EXPORT extern jclass prism_cls; +EXPORT extern jobject prism_obj; +// Options: // numerical method stuff EXPORT extern int lin_eq_method; EXPORT extern double lin_eq_method_param; diff --git a/prism/src/mtbdd/PM_Reachability.cc b/prism/src/mtbdd/PM_Reachability.cc index 35b530e7..6bc5e27d 100644 --- a/prism/src/mtbdd/PM_Reachability.cc +++ b/prism/src/mtbdd/PM_Reachability.cc @@ -47,8 +47,7 @@ jint num_rvars, jlong __jlongpointer cv, // col vars jint num_cvars, jlong __jlongpointer s, // start state -jint info // how much diagnostic info to display (0=none, 1=some) -) +jobject prism) { DdNode *trans01 = jlong_to_DdNode(t01); // 0-1 trans matrix DdNode *init = jlong_to_DdNode(s); // start state @@ -58,17 +57,19 @@ jint info // how much diagnostic info to display (0=none, 1=some) DdNode *reach, *frontier, *tmp; bool done; int iters; + + // get PRISM options + int reach_method = env->CallIntMethod(prism_obj, env->GetMethodID(prism_cls, "getReachMethod", "()I")); + int info = env->CallIntMethod(prism_obj, env->GetMethodID(prism_cls, "getExtraReachInfo", "()Z")); // timing stuff long start1, start2, start3, stop; double time_taken, time_for_setup, time_for_iters; - // start clocks + // start clocks start1 = util_cpu_time(); - int method = 1; - - if (method == 1) { + if (reach_method == REACH_BFS) { // initialise done = false; @@ -160,7 +161,7 @@ jint info // how much diagnostic info to display (0=none, 1=some) time_for_iters = time_taken; // print iterations/timing info - PM_PrintToMainLog(env, "\nReachability: %d iterations in %.2f seconds (average %.6f, setup %.2f)\n", iters, time_taken, time_for_iters/iters, time_for_setup); + PM_PrintToMainLog(env, "\nReachability (%s): %d iterations in %.2f seconds (average %.6f, setup %.2f)\n", reach_method==REACH_BFS?"BFS":"frontier", iters, time_taken, time_for_iters/iters, time_for_setup); return ptr_to_jlong(reach); } diff --git a/prism/src/mtbdd/PrismMTBDD.java b/prism/src/mtbdd/PrismMTBDD.java index fb688a6b..5f082be8 100644 --- a/prism/src/mtbdd/PrismMTBDD.java +++ b/prism/src/mtbdd/PrismMTBDD.java @@ -134,11 +134,10 @@ public class PrismMTBDD //------------------------------------------------------------------------------ // reachability - private static native long PM_Reachability(long trans01, long rv, int nrv, long cv, int ncv, long start, int info); - public static JDDNode Reachability(JDDNode trans01, JDDVars rows, JDDVars cols, JDDNode start) { return Reachability(trans01, rows, cols, start, 0); } - public static JDDNode Reachability(JDDNode trans01, JDDVars rows, JDDVars cols, JDDNode start, int info)// throws PrismException + private static native long PM_Reachability(long trans01, long rv, int nrv, long cv, int ncv, long start); + public static JDDNode Reachability(JDDNode trans01, JDDVars rows, JDDVars cols, JDDNode start) { - long ptr = PM_Reachability(trans01.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), start.ptr(), info); + long ptr = PM_Reachability(trans01.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), start.ptr()); //if (ptr == 0) throw new PrismException(getErrorMessage()); return new JDDNode(ptr); } diff --git a/prism/src/prism/ExplicitFiles2MTBDD.java b/prism/src/prism/ExplicitFiles2MTBDD.java index 41a0bcfe..4faad65d 100644 --- a/prism/src/prism/ExplicitFiles2MTBDD.java +++ b/prism/src/prism/ExplicitFiles2MTBDD.java @@ -451,7 +451,7 @@ public class ExplicitFiles2MTBDD // do reachability (or not) if (prism.getDoReach()) { mainLog.print("\nComputing reachable states...\n"); - model.doReachability(prism.getExtraReachInfo()); + model.doReachability(); model.filterReachableStates(); } else { diff --git a/prism/src/prism/ExplicitModel2MTBDD.java b/prism/src/prism/ExplicitModel2MTBDD.java index 4ebd3da0..0d9e30e2 100644 --- a/prism/src/prism/ExplicitModel2MTBDD.java +++ b/prism/src/prism/ExplicitModel2MTBDD.java @@ -212,7 +212,7 @@ public class ExplicitModel2MTBDD // Do reachability (if required) if (doReach) { mainLog.print("\nComputing reachable states...\n"); - model.doReachability(prism.getExtraReachInfo()); + model.doReachability(); model.filterReachableStates(); } else { // If not, assume any non-empty row/column is a reachable state diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java index 9252f4e3..444e5355 100644 --- a/prism/src/prism/LTLModelChecker.java +++ b/prism/src/prism/LTLModelChecker.java @@ -291,7 +291,7 @@ public class LTLModelChecker model.getConstantValues()); // Do reachability/etc. for the new model - modelProd.doReachability(prism.getExtraReachInfo()); + modelProd.doReachability(); modelProd.filterReachableStates(); modelProd.findDeadlocks(false); if (modelProd.getDeadlockStates().size() > 0) { @@ -507,7 +507,7 @@ public class LTLModelChecker modelProd.setSynchs(new Vector(model.getSynchs())); // Do reachability/etc. for the new model - modelProd.doReachability(prism.getExtraReachInfo()); + modelProd.doReachability(); modelProd.filterReachableStates(); modelProd.findDeadlocks(false); if (modelProd.getDeadlockStates().size() > 0) { diff --git a/prism/src/prism/Model.java b/prism/src/prism/Model.java index b839b322..d9f1ba90 100644 --- a/prism/src/prism/Model.java +++ b/prism/src/prism/Model.java @@ -113,7 +113,6 @@ public interface Model void resetTrans(JDDNode trans); void resetTransRewards(int i, JDDNode transRewards); void doReachability(); - void doReachability(boolean extraReachInfo); void skipReachability(); void setReach(JDDNode reach); void setTransActions(JDDNode transActions); // MDPs only diff --git a/prism/src/prism/Modules2MTBDD.java b/prism/src/prism/Modules2MTBDD.java index 4abe2ccf..536ef43a 100644 --- a/prism/src/prism/Modules2MTBDD.java +++ b/prism/src/prism/Modules2MTBDD.java @@ -287,7 +287,7 @@ public class Modules2MTBDD // do reachability (or not) if (prism.getDoReach()) { mainLog.print("\nComputing reachable states...\n"); - model.doReachability(prism.getExtraReachInfo()); + model.doReachability(); model.filterReachableStates(); } else { diff --git a/prism/src/prism/NondetModel.java b/prism/src/prism/NondetModel.java index 0a47db5c..484f8bb7 100644 --- a/prism/src/prism/NondetModel.java +++ b/prism/src/prism/NondetModel.java @@ -156,7 +156,7 @@ public class NondetModel extends ProbModel // do reachability - public void doReachability(boolean extraReachInfo) + public void doReachability() { JDDNode tmp; @@ -165,7 +165,7 @@ public class NondetModel extends ProbModel tmp = JDD.MaxAbstract(trans01, allDDNondetVars); // compute reachable states - reach = PrismMTBDD.Reachability(tmp, allDDRowVars, allDDColVars, start, extraReachInfo ? 1 : 0); + reach = PrismMTBDD.Reachability(tmp, allDDRowVars, allDDColVars, start); JDD.Deref(tmp); // work out number of reachable states diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index e0db21b0..2bfee359 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -150,6 +150,9 @@ public class Prism implements PrismSettingsListener // Round-off threshold for places where doubles are summed and compared to integers // (e.g. checking that probabilities sum to 1 in an update). private double sumRoundOff = 1e-5; + + // Method to use for (symbolic) state-space reachability + private int reachMethod = REACH_BFS; //------------------------------------------------------------------------------ // Logs @@ -489,6 +492,14 @@ public class Prism implements PrismSettingsListener sumRoundOff = d; } + public static int REACH_BFS = 1; + public static int REACH_FRONTIER = 2; + + public void setReachMethod(int reachMethod) + { + this.reachMethod = reachMethod; + } + // Get methods public static String getVersion() @@ -739,6 +750,11 @@ public class Prism implements PrismSettingsListener return sumRoundOff; } + public int getReachMethod() + { + return reachMethod; + } + public void addModelListener(PrismModelListener listener) { modelListeners.add(listener); @@ -1062,7 +1078,8 @@ public class Prism implements PrismSettingsListener cuddStarted = true; JDD.SetOutputStream(techLog.getFilePointer()); - // initialise all three engines + // initialise libraries/engines + PrismNative.initialise(this); PrismMTBDD.initialise(mainLog, techLog); PrismSparse.initialise(mainLog, techLog); PrismHybrid.initialise(mainLog, techLog); @@ -2732,7 +2749,8 @@ public class Prism implements PrismSettingsListener { // Clear any built model(s) clearBuiltModel(); - // Close down engines + // Close down libraries/engines + PrismNative.closeDown(); PrismMTBDD.closeDown(); PrismSparse.closeDown(); PrismHybrid.closeDown(); diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index b99db26b..4571bab9 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -1415,6 +1415,13 @@ public class PrismCL implements PrismModelListener else if (sw.equals("nobscc")) { prism.setBSCCComp(false); } + // reachability options (hidden options) + else if (sw.equals("frontier")) { + prism.setReachMethod(Prism.REACH_FRONTIER); + } + else if (sw.equals("bfs")) { + prism.setReachMethod(Prism.REACH_BFS); + } // Other switches - pass to PrismSettings diff --git a/prism/src/prism/PrismNative.cc b/prism/src/prism/PrismNative.cc index b3c95a71..962b595f 100644 --- a/prism/src/prism/PrismNative.cc +++ b/prism/src/prism/PrismNative.cc @@ -31,8 +31,11 @@ #include "PrismNativeGlob.h" #include "jnipointer.h" -// options +// Global ref to prism class/object +EXPORT jclass prism_cls = NULL; +EXPORT jobject prism_obj = NULL; +// Options: // numerical method stuff EXPORT int lin_eq_method; EXPORT double lin_eq_method_param; @@ -54,6 +57,26 @@ EXPORT int export_adv; // adversary export filename EXPORT const char *export_adv_filename; +//------------------------------------------------------------------------------ +// Prism object +//------------------------------------------------------------------------------ + +JNIEXPORT void JNICALL Java_prism_PrismNative_PN_1SetPrism(JNIEnv *env, jclass cls, jobject prism) +{ + // if prism has been set previously, we need to delete existing global refs first + if (prism_obj != NULL) { + env->DeleteGlobalRef(prism_cls); + prism_cls = NULL; + env->DeleteGlobalRef(prism_obj); + prism_obj = NULL; + } + + // make a global reference to the object + prism_obj = env->NewGlobalRef(prism); + // get the class and make a global reference to it + prism_cls = (jclass)env->NewGlobalRef(env->GetObjectClass(prism_obj)); +} + //------------------------------------------------------------------------------ // Set methods for options in native code //------------------------------------------------------------------------------ @@ -213,4 +236,17 @@ JNIEXPORT void JNICALL Java_prism_PrismNative_PN_1CloseFile(JNIEnv *env, jclass } //------------------------------------------------------------------------------ +// tidy up +//------------------------------------------------------------------------------ + +JNIEXPORT void JNICALL Java_prism_PrismNative_PN_1FreeGlobalRefs(JNIEnv *env, jclass cls) +{ + // delete all global references + env->DeleteGlobalRef(prism_cls); + prism_cls = NULL; + env->DeleteGlobalRef(prism_obj); + prism_obj = NULL; +} + +//------------------------------------------------------------------------------ diff --git a/prism/src/prism/PrismNative.java b/prism/src/prism/PrismNative.java index 3a1676f6..a9fd494c 100644 --- a/prism/src/prism/PrismNative.java +++ b/prism/src/prism/PrismNative.java @@ -44,6 +44,35 @@ public class PrismNative } } + // Initialise/close down methods + + public static void initialise(Prism prism) + { + setPrism(prism); + } + + public static void closeDown() + { + // Tidy up any JNI stuff + PN_FreeGlobalRefs(); + } + + // tidy up in jni (free global references) + private static native void PN_FreeGlobalRefs(); + + // Prism object + + // Place to store Prism object for Java code + private static Prism prism; + // JNI method to set Prism object for native code + private static native void PN_SetPrism(Prism prism); + // Method to set Prism object both in Java and C++ + public static void setPrism(Prism prism) + { + PrismNative.prism = prism; + PN_SetPrism(prism); + } + // Options passing private static native void PN_SetCompact(boolean b); diff --git a/prism/src/prism/ProbModel.java b/prism/src/prism/ProbModel.java index f2a88a54..7e32735a 100644 --- a/prism/src/prism/ProbModel.java +++ b/prism/src/prism/ProbModel.java @@ -466,14 +466,9 @@ public class ProbModel implements Model // do reachability public void doReachability() - { - doReachability(false); - } - - public void doReachability(boolean extraReachInfo) { // compute reachable states - setReach(PrismMTBDD.Reachability(trans01, allDDRowVars, allDDColVars, start, extraReachInfo ? 1 : 0)); + setReach(PrismMTBDD.Reachability(trans01, allDDRowVars, allDDColVars, start)); } // this method allows you to skip the reachability phase