Added -exportadv option to enable adversary generation.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1728 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/include/PrismNative.h

@@ -7,6 +7,22 @@
 #ifdef __cplusplus
 extern "C" {
 #endif
+/*
+ * Class:     prism_PrismNative
+ * Method:    PN_SetExportAdv
+ * Signature: (I)V
+ */
+JNIEXPORT void JNICALL Java_prism_PrismNative_PN_1SetExportAdv
+  (JNIEnv *, jclass, jint);
+
+/*
+ * Class:     prism_PrismNative
+ * Method:    PN_SetExportAdvFilename
+ * Signature: (Ljava/lang/String;)V
+ */
+JNIEXPORT void JNICALL Java_prism_PrismNative_PN_1SetExportAdvFilename
+  (JNIEnv *, jclass, jstring);
+
 /*
  * Class:     prism_PrismNative
  * Method:    PN_GetStdout

prism/include/PrismNativeGlob.h

@@ -0,0 +1,46 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+#include <jni.h>
+
+//------------------------------------------------------------------------------
+
+// Constants - these need to match the definitions in prism/Prism.java
+
+const int EXPORT_ADV_NONE = 0;
+const int EXPORT_ADV_DTMC = 1;
+const int EXPORT_ADV_MDP = 2;
+
+//------------------------------------------------------------------------------
+
+// External refs to global variables
+
+// adversary export mode
+extern int export_adv;
+// adversary export filename
+extern const char *export_adv_filename;
+
+//------------------------------------------------------------------------------

prism/src/prism/NondetModelChecker.java

@@ -70,11 +70,18 @@ public class NondetModelChecker extends NonProbModelChecker
 		model = (NondetModel) m;
 		nondetMask = model.getNondetMask();
 		allDDNondetVars = model.getAllDDNondetVars();
-
+		
+		// Display warning for some option combinations
+		if (prism.getExportAdv() > 0 && engine != Prism.SPARSE) {
+			mainLog.println("Warning: Adversary generation is only implemented for the sparse engine");
+		}
+		
 		// Inherit some options from parent Prism object.
-		// Store locally and/or pass onto engines.
+		// Store locally and/or pass onto engines/native code.
 		precomp = prism.getPrecomp();
 		fairness = prism.getFairness();
+		PrismNative.setExportAdv(prism.getExportAdv());
+		PrismNative.setExportAdvFilename(prism.getExportAdvFilename());
 		switch (engine) {
 		case Prism.MTBDD:
 			PrismMTBDD.setTermCrit(prism.getTermCrit());

prism/src/prism/Prism.java

@@ -84,6 +84,11 @@ public class Prism implements PrismSettingsListener
 	public static final int EXPORT_ROWS = 5;
 	public static final int EXPORT_DOT_STATES = 6;
 	
+	// options for adversary export
+	public static final int EXPORT_ADV_NONE = 0;
+	public static final int EXPORT_ADV_DTMC = 1;
+	public static final int EXPORT_ADV_MDP = 2;
+	
 	// methods for SCC decomposition
 	public static final int XIEBEEREL = 1;
 	public static final int LOCKSTEP = 2;
@@ -328,6 +333,16 @@ public class Prism implements PrismSettingsListener
 		settings.set(PrismSettings.PRISM_SCC_METHOD, i-1); // note index offset correction
 	}
 	
+	public void setExportAdv(int i) throws PrismException
+	{
+		settings.set(PrismSettings.PRISM_EXPORT_ADV, i-1); // note index offset correction
+	}
+
+	public void setExportAdvFilename(String s) throws PrismException
+	{
+		settings.set(PrismSettings.PRISM_EXPORT_ADV_FILENAME, s);
+	}
+	
 	// set methods for miscellaneous options
 	
 	public void setExportTarget(boolean b) throws PrismException
@@ -442,6 +457,12 @@ public class Prism implements PrismSettingsListener
 	public int getSCCMethod()
 	{ return settings.getInteger(PrismSettings.PRISM_SCC_METHOD)+1; } //NOTE THE CORRECTION for the ChoiceSetting index
 	
+	public int getExportAdv()
+	{ return settings.getInteger(PrismSettings.PRISM_EXPORT_ADV)+1; } //NOTE THE CORRECTION for the ChoiceSetting index
+	
+	public String getExportAdvFilename()
+	{ return settings.getString(PrismSettings.PRISM_EXPORT_ADV_FILENAME); }
+	
 	// get methods for miscellaneous options
 	
 	public boolean getExportTarget()

prism/src/prism/PrismCL.java

@@ -999,6 +999,16 @@ public class PrismCL
 						errorAndExit("No file specified for -"+sw+" switch");
 					}
 				}
+				// export prism model to file
+				else if (sw.equals("exportadv")) {
+					if (i < args.length-1) {
+						prism.setExportAdv(Prism.EXPORT_ADV_DTMC);
+						prism.setExportAdvFilename(args[++i]);
+					}
+					else {
+						errorAndExit("No file specified for -"+sw+" switch");
+					}
+				}
 				// set scc computation algorithm
 				else if (sw.equals("sccmethod") || sw.equals("bsccmethod")) {
 					if (i < args.length-1) {

prism/src/prism/PrismNative.cc

@@ -30,6 +30,33 @@
 #include <limits.h>
 #include "jnipointer.h"
 
+// adversary export mode
+int export_adv;
+// adversary export filename
+const char *export_adv_filename;
+
+//------------------------------------------------------------------------------
+// Set methods for options in native code
+//------------------------------------------------------------------------------
+
+JNIEXPORT void JNICALL Java_prism_PrismNative_PN_1SetExportAdv(JNIEnv *env, jclass cls, jint i)
+{
+	export_adv = i;
+}
+
+//------------------------------------------------------------------------------
+
+JNIEXPORT void JNICALL Java_prism_PrismNative_PN_1SetExportAdvFilename(JNIEnv *env, jclass cls, jstring fn)
+{
+	if (fn) {
+		export_adv_filename = env->GetStringUTFChars(fn, 0);
+		// This never gets released. Oops.
+	} else {
+		export_adv_filename = NULL;
+	}
+}
+//------------------------------------------------------------------------------
+// Some miscellaneous native methods
 //------------------------------------------------------------------------------
 
 JNIEXPORT jlong __jlongpointer JNICALL Java_prism_PrismNative_PN_1GetStdout(JNIEnv *env, jclass cls)

prism/src/prism/PrismNative.java

@@ -27,7 +27,8 @@
 package prism;
 
 /**
- * A few utility methods, relying on native methods in the "prism" shared library
+ * Set methods to pass options to native code.
+ * And a few utility methods, relying on native methods in the "prism" shared library.
  */ 
 public class PrismNative
 {
@@ -43,6 +44,20 @@ public class PrismNative
 		}
 	}
 	
+	// Mode/filename for export of adversaries
+	private static native void PN_SetExportAdv(int i);
+	public static void setExportAdv(int i)
+	{
+		PN_SetExportAdv(i);
+	}
+	
+	private static native void PN_SetExportAdvFilename(String filename);
+	public static void setExportAdvFilename(String filename)
+	{
+		PN_SetExportAdvFilename(filename);
+	}
+	
+	// Some miscellaneous native methods
 	public static native long PN_GetStdout();
 	public static native long PN_OpenFile(String filename);
 	public static native long PN_OpenFileAppend(String filename);

prism/src/prism/PrismSettings.java

@@ -92,6 +92,8 @@ public class PrismSettings implements Observer
 	public static final String PRISM_SYMM_RED_PARAMS					= "prism.symmRedParams";
 	public static final String PRISM_PTA_METHOD					= "prism.ptaMethod";
 	public static final String PRISM_AR_OPTIONS					= "prism.arOptions";
+	public static final String PRISM_EXPORT_ADV					= "prism.exportAdv";
+	public static final String PRISM_EXPORT_ADV_FILENAME			= "prism.exportAdvFilename";
 	
 	//GUI Model
 	public static final	String MODEL_AUTO_PARSE						= "model.autoParse";
@@ -195,12 +197,14 @@ public class PrismSettings implements Observer
 			{ INTEGER_TYPE,		PRISM_NUM_SOR_LEVELS,					"Hybrid GS levels",						"2.1",			new Integer(-1),															"-1,",																						"Number of MTBDD levels descended for hybrid engine data structures block division with GS/SOR." },
 			{ INTEGER_TYPE,		PRISM_SOR_MAX_MEM,						"Hybrid GS memory (KB)",				"2.1",			new Integer(1024),															"0,",																						"Maximum memory usage for hybrid engine data structures block division with GS/SOR (KB)." },
 			{ BOOLEAN_TYPE,		PRISM_DO_SS_DETECTION,					"Use steady-state detection",			"2.1",			new Boolean(true),															"0,",																						"Use steady-state detection during CTMC transient probability computation." },
-			{ BOOLEAN_TYPE,		PRISM_EXTRA_DD_INFO,					"Extra MTBDD information",				"3.1.1",			new Boolean(false),															"0,",																						"Display extra information about (MT)BDDs used during and after model construction." },
-			{ BOOLEAN_TYPE,		PRISM_EXTRA_REACH_INFO,					"Extra reachability information",		"3.1.1",			new Boolean(false),															"0,",																						"Display extra information about progress of reachability during model construction." },
+			{ BOOLEAN_TYPE,		PRISM_EXTRA_DD_INFO,					"Extra MTBDD information",				"3.1.1",		new Boolean(false),															"0,",																						"Display extra information about (MT)BDDs used during and after model construction." },
+			{ BOOLEAN_TYPE,		PRISM_EXTRA_REACH_INFO,					"Extra reachability information",		"3.1.1",		new Boolean(false),															"0,",																						"Display extra information about progress of reachability during model construction." },
 			{ CHOICE_TYPE,		PRISM_SCC_METHOD,						"SCC decomposition method",				"3.2",			"Lockstep",																	"Xie-Beerel,Lockstep,SCC-Find",																"Which algorithm to use for decomposing a graph into strongly connected components (SCCs)." },
-			{ STRING_TYPE,		PRISM_SYMM_RED_PARAMS,						"Symmetry reduction parameters",				"3.2",			"",																	"",																"Parameters for symmetry reduction (format: \"i j\" where i and j are the number of modules before and after the symmetric ones; empty string means symmetry reduction disabled)." },
-			{ CHOICE_TYPE,		PRISM_PTA_METHOD,						"PTA model checking method",				"3.3",			"Stochastic games",																	"Digital clocks,Stochastic games,Bisimulation minimisation",																"Which method to use for model checking of PTAs." },
-			{ STRING_TYPE,		PRISM_AR_OPTIONS,						"Abstraction refinement options",				"3.3",			"",																	"",																"Various options passed to the asbtraction-refinement engine (e.g. for PTA model checking)." },
+			{ STRING_TYPE,		PRISM_SYMM_RED_PARAMS,					"Symmetry reduction parameters",		"3.2",			"",																	"",																"Parameters for symmetry reduction (format: \"i j\" where i and j are the number of modules before and after the symmetric ones; empty string means symmetry reduction disabled)." },
+			{ CHOICE_TYPE,		PRISM_PTA_METHOD,						"PTA model checking method",			"3.3",			"Stochastic games",																	"Digital clocks,Stochastic games,Bisimulation minimisation",																"Which method to use for model checking of PTAs." },
+			{ STRING_TYPE,		PRISM_AR_OPTIONS,						"Abstraction refinement options",		"3.3",			"",																	"",																"Various options passed to the asbtraction-refinement engine (e.g. for PTA model checking)." },
+			{ CHOICE_TYPE,		PRISM_EXPORT_ADV,						"Adversary export",						"3.3",			"None",																	"None,DTMC,MDP",																"Type of adversary to generate and export during MDP model checking" },
+			{ STRING_TYPE,		PRISM_EXPORT_ADV_FILENAME,				"Adversary export filename",			"3.3",			"adv.tra",																	"",																"Name of file for MDP adversary export (if enabled)" },
 		},
 		{
 			{ BOOLEAN_TYPE,		MODEL_AUTO_PARSE,						"Auto parse",							"2.1",			new Boolean(true),															"",																							"Parse PRISM models automatically as they are loaded/edited in the text editor." },

prism/src/sparse/PS_NondetUntil.cc

@@ -34,6 +34,7 @@
 #include <dv.h>
 #include "sparse.h"
 #include "prism.h"
+#include "PrismNativeGlob.h"
 #include "PrismSparseGlob.h"
 #include "jnipointer.h"
 #include <new>
@@ -82,7 +83,8 @@ jboolean min				// min or max probabilities (true = min, false = max)
 	long start1, start2, start3, stop;
 	double time_taken, time_for_setup, time_for_iters;
 	// adversary stuff
-	bool adv = true, adv_loop = false;
+	int export_adv_enabled = export_adv;
+	bool adv_loop = false;
 	FILE *fp_adv = NULL;
 	int adv_j, adv_l2, adv_h2;
 	int *actions;
@@ -121,7 +123,7 @@ jboolean min				// min or max probabilities (true = min, false = max)
 	PS_PrintMemoryToMainLog(env, "[", kb, "]\n");
 	
 	// if needed, and if info is available, build a vector of action indices for the mdp
-	if (adv && trans_actions != NULL) {
+	if (export_adv_enabled > 0 && trans_actions != NULL) {
 		PS_PrintToMainLog(env, "Building action information... ");
 		// first need to filter out unwanted rows
 		Cudd_Ref(trans_actions);
@@ -174,13 +176,13 @@ jboolean min				// min or max probabilities (true = min, false = max)
 	PS_PrintToMainLog(env, "\nStarting iterations...\n");
 	
 	// open file to store adversary (if required)
-	if (adv) {
-		fp_adv = fopen("adv.tra", "w");
+	if (export_adv_enabled > 0) {
+		fp_adv = fopen(export_adv_filename, "w");
 		if (fp_adv) {
 			fprintf(fp_adv, "%d ?\n", n);
 		} else {
-			PS_PrintToMainLog(env, "\nWarning: Adversary generation cancelled (could not open file \"%s\").\n", "adv.tra");
-			adv = false;
+			PS_PrintToMainLog(env, "\nWarning: Adversary generation cancelled (could not open file \"%s\").\n", export_adv_filename);
+			export_adv_enabled = false;
 		}
 	}
 	
@@ -263,7 +265,7 @@ jboolean min				// min or max probabilities (true = min, false = max)
 		soln2 = tmpsoln;
 		
 		// if we're done, but adversary generation is required, go round once more
-		if (done && adv) adv_loop = !adv_loop;
+		if (done && export_adv_enabled > 0) adv_loop = !adv_loop;
 		
 //		PS_PrintToMainLog(env, "%.2f %.2f sec\n", ((double)(util_cpu_time() - start3)/1000), ((double)(util_cpu_time() - start2)/1000)/iters);
 	}
@@ -280,9 +282,9 @@ jboolean min				// min or max probabilities (true = min, false = max)
 	if (!done) { delete soln; soln = NULL; PS_SetErrorMessage("Iterative method did not converge within %d iterations.\nConsider using a different numerical method or increasing the maximum number of iterations", iters); }
 	
 	// close file to store adversary (if required)
-	if (adv) {
+	if (export_adv_enabled) {
 		fclose(fp_adv);
-		PS_PrintToMainLog(env, "\nAdversary written to file \"%s\".\n", "adv.tra");
+		PS_PrintToMainLog(env, "\nAdversary written to file \"%s\".\n", export_adv_filename);
 	}
 	
 	// catch exceptions: register error, free memory