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

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

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

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;

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);
 }

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);
 	}

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 {

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

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<String>(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) {

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

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 {

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

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();

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
 

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;
+}
+
+//------------------------------------------------------------------------------
 

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

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