(export-iterations) introduce --exportiterations option, ExportIterations helper classes for C and Java

Generates HTML file with the individual steps of the iterative procedures. Relies on external JavaScript and CSS. Is already prepared for exporting interval iteration steps (possibility to export multiple vectors with type flag per iteration step) git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12073 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago · 30f7def86c
23 changed files with 402 additions and 1 deletions
--- a/prism/include/ExportIterations.h
+++ b/prism/include/ExportIterations.h
@ -0,0 +1,110 @@
+//==============================================================================
+//
+//	Copyright (c) 2016-
+//	Authors:
+//	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
+//
+//------------------------------------------------------------------------------
+//
+//	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
+//
+//==============================================================================
+
+
+#ifndef EXPORT_ITERATIONS_H
+#define EXPORT_ITERATIONS_H
+
+#include <cstdio>
+#include <string>
+#include <math.h>
+
+#include <cudd.h>
+#include <dd.h>
+#include "dv.h"
+#include "prism.h"
+#include <odd.h>
+
+class ExportIterations {
+private:
+	FILE *fp;
+
+public:
+	/**
+	 * Constructor, provide filename.
+	 */
+	ExportIterations(const char* title = "", const char* filename = get_export_iterations_filename()) {
+		fp = fopen(filename, "w");
+
+		fprintf(fp, "<!DOCTYPE html>\n");
+		fprintf(fp, "<html><head>\n");
+		fprintf(fp, "<meta charset=\"utf-8\">\n");
+		fprintf(fp, "<!-- HTML file automatically generated by the PRISM model checker -->\n");
+		fprintf(fp, "<!-- For visualising the individual steps of a value iteration computation -->\n");
+		fprintf(fp, "<!-- Loads supporting Javascript and CSS from www.prismmodelchecker.org -->\n");
+		fprintf(fp, "<title>%s</title>\n", title);
+		fprintf(fp, "<link rel='stylesheet' href='http://www.prismmodelchecker.org/js/res/iteration-vis-v1.css'>\n");
+		fprintf(fp, "<script src=\"http://www.prismmodelchecker.org/js/res/d3.js-v4/d3.min.js\"></script>\n");
+		fprintf(fp, "<body onload='init();'>\n");
+		fprintf(fp, "<h1>%s</h1>\n", title);
+		fprintf(fp, "<svg></svg>\n");
+		fprintf(fp, "<script src=\"http://www.prismmodelchecker.org/js/res/iteration-vis-v1.js\"></script>\n");
+	}
+
+	/**
+	 * Export the given vector, with size n and given type (0 = normal, VI from below, 1 = VI from above)
+	 */
+	void exportVector(double *soln, int n, int type) {
+		fprintf(fp, "<script>addVector([");
+		for (int i = 0; i < n; i++) {
+			if (i>0) fprintf(fp, ",");
+			double d = soln[i];
+			if (isinf(d)) {
+				if (d > 0)
+					fprintf(fp, "Infinity");
+				else
+					fprintf(fp, "-Infinity");
+			} else {
+				fprintf(fp, "%.17g", soln[i]);
+			}
+		}
+		fprintf(fp, "],%d)</script>\n", type);
+		fflush(fp);
+	}
+
+	/**
+	 * Export the given MTBDD vector, with num_rvars row variables,
+	 * odd for reachable state space and type (0= normal, VI from below, 1 = VI from above)
+	 */
+	void exportVector(DdNode *dd, DdNode **rvars, int num_rvars, ODDNode* odd, int type)
+	{
+		double* vec = mtbdd_to_double_vector(ddman, dd, rvars, num_rvars, odd);
+
+		// get number of states
+		int n = odd->eoff + odd->toff;
+
+		exportVector(vec, n, type);
+		delete[] vec;
+	}
+
+	/** Destructor, close file */
+	~ExportIterations() {
+		fprintf(fp, "</body></html>\n");
+		fclose(fp);
+	}
+};
+
+#endif
--- a/prism/include/PrismHybrid.h
+++ b/prism/include/PrismHybrid.h
@ -39,6 +39,14 @@ JNIEXPORT void JNICALL Java_hybrid_PrismHybrid_PH_1SetMainLog
 JNIEXPORT void JNICALL Java_hybrid_PrismHybrid_PH_1SetTechLog
  (JNIEnv *, jclass, jobject);

+/*
+ * Class:     hybrid_PrismHybrid
+ * Method:    PH_SetExportIterations
+ * Signature: (Z)V
+ */
+JNIEXPORT void JNICALL Java_hybrid_PrismHybrid_PH_1SetExportIterations
+  (JNIEnv *, jclass, jboolean);
+
 /*
 * Class:     hybrid_PrismHybrid
 * Method:    PH_GetErrorMessage
--- a/prism/include/PrismHybridGlob.h
+++ b/prism/include/PrismHybridGlob.h
@ -51,5 +51,6 @@ void PH_PrintToTechLog(JNIEnv *env, const char *str, ...);
 void PH_PrintMemoryToMainLog(JNIEnv *env, const char *before, double mem, const char *after);
 void PH_SetErrorMessage(const char *str, ...);
 char *PH_GetErrorMessage();
+bool PH_GetFlagExportIterations();

 //------------------------------------------------------------------------------
--- a/prism/include/PrismMTBDD.h
+++ b/prism/include/PrismMTBDD.h
@ -39,6 +39,14 @@ JNIEXPORT void JNICALL Java_mtbdd_PrismMTBDD_PM_1SetMainLog
 JNIEXPORT void JNICALL Java_mtbdd_PrismMTBDD_PM_1SetTechLog
  (JNIEnv *, jclass, jobject);

+/*
+ * Class:     mtbdd_PrismMTBDD
+ * Method:    PM_SetExportIterations
+ * Signature: (Z)V
+ */
+JNIEXPORT void JNICALL Java_mtbdd_PrismMTBDD_PM_1SetExportIterations
+  (JNIEnv *, jclass, jboolean);
+
 /*
 * Class:     mtbdd_PrismMTBDD
 * Method:    PM_GetErrorMessage
--- a/prism/include/PrismMTBDDGlob.h
+++ b/prism/include/PrismMTBDDGlob.h
@ -51,5 +51,6 @@ void PM_SetErrorMessage(const char *str, ...);
 char *PM_GetErrorMessage();
 int store_export_info(int type, jstring fn, JNIEnv *env);
 void export_string(const char *str, ...);
+bool PM_GetFlagExportIterations();

 //------------------------------------------------------------------------------
--- a/prism/include/PrismNative.h
+++ b/prism/include/PrismNative.h
@ -127,6 +127,14 @@ JNIEXPORT void JNICALL Java_prism_PrismNative_PN_1SetExportAdv
 JNIEXPORT void JNICALL Java_prism_PrismNative_PN_1SetExportAdvFilename
  (JNIEnv *, jclass, jstring);

+/*
+ * Class:     prism_PrismNative
+ * Method:    PN_SetDefaultExportIterationsFilename
+ * Signature: (Ljava/lang/String;)V
+ */
+JNIEXPORT void JNICALL Java_prism_PrismNative_PN_1SetDefaultExportIterationsFilename
+  (JNIEnv *, jclass, jstring);
+
 /*
 * Class:     prism_PrismNative
 * Method:    PN_SetWorkingDirectory
--- a/prism/include/PrismNativeGlob.h
+++ b/prism/include/PrismNativeGlob.h
@ -99,6 +99,8 @@ EXPORT extern bool do_ss_detect;
 EXPORT extern int export_adv;
 // adversary export filename
 EXPORT extern const char *export_adv_filename;
+// export iterations filename
+EXPORT extern const char *export_iterations_filename;

 //------------------------------------------------------------------------------

--- a/prism/include/PrismSparse.h
+++ b/prism/include/PrismSparse.h
@ -39,6 +39,14 @@ JNIEXPORT void JNICALL Java_sparse_PrismSparse_PS_1SetMainLog
 JNIEXPORT void JNICALL Java_sparse_PrismSparse_PS_1SetTechLog
  (JNIEnv *, jclass, jobject);

+/*
+ * Class:     sparse_PrismSparse
+ * Method:    PS_SetExportIterations
+ * Signature: (Z)V
+ */
+JNIEXPORT void JNICALL Java_sparse_PrismSparse_PS_1SetExportIterations
+  (JNIEnv *, jclass, jboolean);
+
 /*
 * Class:     sparse_PrismSparse
 * Method:    PS_GetErrorMessage
--- a/prism/include/PrismSparseGlob.h
+++ b/prism/include/PrismSparseGlob.h
@ -53,5 +53,6 @@ void PS_SetErrorMessage(const char *str, ...);
 char *PS_GetErrorMessage();
 int store_export_info(int type, jstring fn, JNIEnv *env);
 void export_string(const char *str, ...);
+bool PS_GetFlagExportIterations();

 //------------------------------------------------------------------------------
--- a/prism/include/prism.h
+++ b/prism/include/prism.h
@ -51,6 +51,7 @@ EXPORT long get_real_time(JNIEnv *env);
 EXPORT void get_string_array_from_java(JNIEnv *env, jobject strings_list, jstring *&strings_jstrings, const char **&strings, int &size);
 EXPORT void release_string_array_from_java(JNIEnv *env, jstring *strings_jstrings, const char **strings, jint size);
 EXPORT FoxGlynnWeights fox_glynn(double q_tmax, double underflow, double overflow, double accuracy);
+EXPORT const char* get_export_iterations_filename();

 // Global constants
 // Delay between occasional updates for slow processes, e.g. numerical solution (milliseconds)
--- a/prism/src/explicit/ExportIterations.java
+++ b/prism/src/explicit/ExportIterations.java
@ -0,0 +1,153 @@
+//==============================================================================
+//	
+//	Copyright (c) 2016-
+//	Authors:
+//	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
+//	
+//------------------------------------------------------------------------------
+//	
+//	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
+//	
+//==============================================================================
+
+package explicit;
+
+import dv.DoubleVector;
+import prism.PrismException;
+import prism.PrismFileLog;
+import prism.PrismLog;
+
+/**
+ * Class for exporting / visualising the value vectors in
+ * a numerical iteration algorithm.
+ *
+ */
+public class ExportIterations {
+	private static String defaultFilename = "iterations.html";
+
+	private PrismLog log;
+
+	public ExportIterations(String title) throws PrismException
+	{
+		this(title, PrismFileLog.create(defaultFilename));
+	}
+
+	/**
+	 * Constructor.
+	 * @param log the log used for export
+	 */
+	public ExportIterations(String title, PrismLog log)
+	{
+		this.log = log;
+
+		log.println("<!DOCTYPE html>");
+		log.println("<html><head>");
+		log.println("<meta charset=\"utf-8\">");
+		log.println("<!-- HTML file automatically generated by the PRISM model checker -->");
+		log.println("<!-- For visualising the individual steps of a value iteration computation -->");
+		log.println("<!-- Loads supporting Javascript and CSS from www.prismmodelchecker.org -->");
+		log.println("<title>" + title + "</title>");
+		log.println("<link rel='stylesheet' href='http://www.prismmodelchecker.org/js/res/iteration-vis-v1.css'>");
+		log.println("<script src=\"http://www.prismmodelchecker.org/js/res/d3.js-v4/d3.min.js\"></script>");
+		log.println("<body onload='init();'>");
+		log.println("<h1>" + title + "</h1>");
+		log.println("<svg></svg>");
+		log.println("<script src=\"http://www.prismmodelchecker.org/js/res/iteration-vis-v1.js\"></script>");
+	}
+
+	/**
+	 * Export the given vector.
+	 * @param soln the value vector
+	 */
+	public void exportVector(double[] soln)
+	{
+		exportVector(soln, 0);
+	}
+
+	/**
+	 * Export the given vector.
+	 * @param soln the value vector
+	 * @param type the vector type (0 = normal, VI from below, 1 = VI from above)
+	 */
+	public void exportVector(double[] soln, int type)
+	{
+		log.print("<script>addVector([");
+		for (int i = 0; i < soln.length; i++) {
+			if (i>0) log.print(",");
+			double d = soln[i];
+			exportValue(d);
+		}
+		log.print("]," + type + ")</script>\n");
+	}
+
+	/**
+	 * Export the given vector.
+	 * @param soln the value vector
+	 */
+	public void exportVector(DoubleVector soln)
+	{
+		exportVector(soln, 0);
+	}
+
+	/**
+	 * Export the given vector.
+	 * @param soln the value vector
+	 * @param type the vector type (0 = normal, VI from below, 1 = VI from above)
+	 */
+	public void exportVector(DoubleVector soln, int type)
+	{
+		log.print("<script>addVector([");
+		for (int i = 0, n = soln.getSize(); i < n; i++) {
+			if (i>0) log.print(",");
+			double d = soln.getElement(i);
+			exportValue(d);
+		}
+		log.print("]," + type + ")</script>\n");
+	}
+
+	private void exportValue(double d)
+	{
+		if (d == Double.POSITIVE_INFINITY) {
+			log.print("Infinity");
+		} else if (d == Double.NEGATIVE_INFINITY) {
+			log.print("-Infinity");
+		} else {
+			log.print(d);
+		}
+	}
+
+	/** Print footer, export log */
+	public void close()
+	{
+		log.println("\n</body></html>");
+	}
+
+	public static void setDefaultFilename(String newDefaultFilename)
+	{
+		defaultFilename = newDefaultFilename;
+	}
+
+	public static String getDefaultFilename()
+	{
+		return defaultFilename;
+	}
+
+	public static void resetDefaultFilename()
+	{
+		defaultFilename = "iterations.html";
+	}
+}
--- a/prism/src/hybrid/PrismHybrid.cc
+++ b/prism/src/hybrid/PrismHybrid.cc
@ -57,6 +57,9 @@ static jmethodID main_log_mid = NULL;
 static jmethodID main_log_warn = NULL;
 static jmethodID tech_log_mid = NULL;

+// export stuff
+static bool exportIterations = false;
+
 // error message
 static char error_message[MAX_ERR_STRING_LEN];

@ -212,6 +215,20 @@ JNIEXPORT jstring JNICALL Java_hybrid_PrismHybrid_PH_1GetErrorMessage(JNIEnv *en
 	return env->NewStringUTF(error_message);
 }

+//------------------------------------------------------------------------------
+// export flags
+//------------------------------------------------------------------------------
+
+JNIEXPORT void JNICALL Java_hybrid_PrismHybrid_PH_1SetExportIterations(JNIEnv *env, jclass cls, jboolean value)
+{
+	exportIterations = value;
+}
+
+bool PH_GetFlagExportIterations()
+{
+	return exportIterations;
+}
+
 //------------------------------------------------------------------------------
 // numerical computation detail queries
 //------------------------------------------------------------------------------
--- a/prism/src/hybrid/PrismHybrid.java
+++ b/prism/src/hybrid/PrismHybrid.java
@ -128,6 +128,12 @@ public class PrismHybrid
 		PH_SetTechLog(log);
 	}

+	private static native void PH_SetExportIterations(boolean value);
+	public static void SetExportIterations(boolean value)
+	{
+		PH_SetExportIterations(value);
+	}
+
 	//------------------------------------------------------------------------------
 	// error message
 	//------------------------------------------------------------------------------
--- a/prism/src/mtbdd/Makefile
+++ b/prism/src/mtbdd/Makefile
@ -22,6 +22,7 @@ LIBRARIES = \
 -L$(PRISM_DIR_REL)/$(LIB_DIR) \
 -lodd \
 -ldd \
+-ldv \
 -lprism \
 $(LIBMATH)

--- a/prism/src/mtbdd/PrismMTBDD.cc
+++ b/prism/src/mtbdd/PrismMTBDD.cc
@ -61,6 +61,7 @@ static jmethodID tech_log_mid = NULL;
 int export_type;
 FILE *export_file;
 JNIEnv *export_env;
+static bool exportIterations = false;

 // error message
 static char error_message[MAX_ERR_STRING_LEN];
@ -213,6 +214,20 @@ void export_string(const char *str, ...)
 	}
 }

+//------------------------------------------------------------------------------
+// export flags
+//------------------------------------------------------------------------------
+
+JNIEXPORT void JNICALL Java_mtbdd_PrismMTBDD_PM_1SetExportIterations(JNIEnv *env, jclass cls, jboolean value)
+{
+	exportIterations = value;
+}
+
+bool PM_GetFlagExportIterations()
+{
+	return exportIterations;
+}
+
 //------------------------------------------------------------------------------
 // error message handling
 //------------------------------------------------------------------------------
--- a/prism/src/mtbdd/PrismMTBDD.java
+++ b/prism/src/mtbdd/PrismMTBDD.java
@ -115,6 +115,12 @@ public class PrismMTBDD
 		PM_SetTechLog(log);
 	}

+	private static native void PM_SetExportIterations(boolean value);
+	public static void SetExportIterations(boolean value)
+	{
+		PM_SetExportIterations(value);
+	}
+
 	//------------------------------------------------------------------------------
 	// error message
 	//------------------------------------------------------------------------------
--- a/prism/src/prism/Prism.java
+++ b/prism/src/prism/Prism.java
@ -1017,6 +1017,9 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 			}
 		}
 		jdd.SanityJDD.enabled = settings.getBoolean(PrismSettings.PRISM_JDD_SANITY_CHECKS);
+		PrismSparse.SetExportIterations(settings.getBoolean(PrismSettings.PRISM_EXPORT_ITERATIONS));
+		PrismHybrid.SetExportIterations(settings.getBoolean(PrismSettings.PRISM_EXPORT_ITERATIONS));
+		PrismMTBDD.SetExportIterations(settings.getBoolean(PrismSettings.PRISM_EXPORT_ITERATIONS));
 	}

 	//------------------------------------------------------------------------------
--- a/prism/src/prism/PrismNative.cc
+++ b/prism/src/prism/PrismNative.cc
@ -58,6 +58,8 @@ EXPORT bool do_ss_detect;
 EXPORT int export_adv;
 // adversary export filename
 EXPORT const char *export_adv_filename;
+// export iterations filename
+EXPORT const char *export_iterations_filename = "iterations.html";

 //------------------------------------------------------------------------------
 // Prism object
@ -183,6 +185,18 @@ JNIEXPORT void JNICALL Java_prism_PrismNative_PN_1SetExportAdvFilename(JNIEnv *e

 //------------------------------------------------------------------------------

+JNIEXPORT void JNICALL Java_prism_PrismNative_PN_1SetDefaultExportIterationsFilename(JNIEnv *env, jclass cls, jstring fn)
+{
+	if (fn) {
+		export_iterations_filename = env->GetStringUTFChars(fn, 0);
+		// This never gets released. Oops.
+	} else {
+		export_iterations_filename = NULL;
+	}
+}
+
+//------------------------------------------------------------------------------
+
 JNIEXPORT jint JNICALL Java_prism_PrismNative_PN_1SetWorkingDirectory(JNIEnv *env, jclass cls, jstring dn) {
 	int rv;
 	const char* dirname = env->GetStringUTFChars(dn, 0);
--- a/prism/src/prism/PrismNative.java
+++ b/prism/src/prism/PrismNative.java
@ -153,6 +153,12 @@ public class PrismNative
 		PN_SetExportAdvFilename(filename);
 	}

+	private static native void PN_SetDefaultExportIterationsFilename(String filename);
+	public static void setDefaultExportIterationsFilename(String filename)
+	{
+		PN_SetDefaultExportIterationsFilename(filename);
+	}
+
 	private static native int PN_SetWorkingDirectory(String dirname);
 	/** Changes the current working directory. Returns 0 on success. */
 	public static int setWorkingDirectory(String dirname) {
--- a/prism/src/prism/PrismSettings.java
+++ b/prism/src/prism/PrismSettings.java
@ -89,6 +89,7 @@ public class PrismSettings implements Observer
 	public static final	String PRISM_TERM_CRIT						= "prism.termCrit";//"prism.termination";
 	public static final	String PRISM_TERM_CRIT_PARAM				= "prism.termCritParam";//"prism.terminationEpsilon";
 	public static final	String PRISM_MAX_ITERS						= "prism.maxIters";//"prism.maxIterations";
+	public static final String PRISM_EXPORT_ITERATIONS				= "prism.exportIterations";
 	
 	public static final	String PRISM_CUDD_MAX_MEM					= "prism.cuddMaxMem";
 	public static final	String PRISM_CUDD_EPSILON					= "prism.cuddEpsilon";
@ -250,6 +251,8 @@ public class PrismSettings implements Observer
 																			"Epsilon value to use for checking termination of iterative numerical methods." },
 			{ INTEGER_TYPE,		PRISM_MAX_ITERS,						"Termination max. iterations",			"2.1",			new Integer(10000),															"0,",																						
 																			"Maximum number of iterations to perform if iterative methods do not converge." },
+			{ BOOLEAN_TYPE,		PRISM_EXPORT_ITERATIONS,				"Export iterations (debug/visualisation)",			"4.3.1",			false,														"",
+																			"Export solution vectors for iteration algorithms to iterations.html"},
 			// MODEL CHECKING OPTIONS:
 			{ BOOLEAN_TYPE,		PRISM_PRECOMPUTATION,					"Use precomputation",					"2.1",			new Boolean(true),															"",																							
 																			"Whether to use model checking precomputation algorithms (Prob0, Prob1, etc.), where optional." },
@ -1033,6 +1036,10 @@ public class PrismSettings implements Observer
 				throw new PrismException("No value specified for -" + sw + " switch");
 			}
 		}
+		// export iterations
+		else if (sw.equals("exportiterations")) {
+			set(PRISM_EXPORT_ITERATIONS, true);
+		}
 		
 		// MODEL CHECKING OPTIONS:
 		
@ -1670,6 +1677,7 @@ public class PrismSettings implements Observer
 		mainLog.println("-exportadvmdp <file> ........... Export an adversary from MDP model checking (as an MDP)");
 		mainLog.println("-ltl2datool <exec> ............. Run executable <exec> to convert LTL formulas to deterministic automata");
 		mainLog.println("-ltl2dasyntax <x> .............. Specify output format for -ltl2datool switch (lbt, spin, spot, rabinizer)");
+		mainLog.println("-exportiterations .............. Export vectors for iteration algorithms to file");
 		
 		mainLog.println();
 		mainLog.println("MULTI-OBJECTIVE MODEL CHECKING:");
--- a/prism/src/prism/prism.cc
+++ b/prism/src/prism/prism.cc
@ -32,6 +32,7 @@
 #include <new>
 #include <vector>
 #include "jnipointer.h"
+#include "PrismNativeGlob.h"

 //------------------------------------------------------------------------------

@ -251,3 +252,8 @@ EXPORT FoxGlynnWeights fox_glynn(double q_tmax, double underflow, double overflo
 }

 //------------------------------------------------------------------------------
+
+const char* get_export_iterations_filename() {
+	return export_iterations_filename;
+}
+//------------------------------------------------------------------------------
--- a/prism/src/sparse/PrismSparse.cc
+++ b/prism/src/sparse/PrismSparse.cc
@ -62,6 +62,7 @@ static jmethodID tech_log_mid = NULL;
 int export_type;
 FILE *export_file;
 JNIEnv *export_env;
+static bool exportIterations = false;

 // error message
 static char error_message[MAX_ERR_STRING_LEN];
@ -269,6 +270,17 @@ JNIEXPORT jstring JNICALL Java_sparse_PrismSparse_PS_1GetErrorMessage(JNIEnv *en
 	return env->NewStringUTF(error_message);
 }

+
+JNIEXPORT void JNICALL Java_sparse_PrismSparse_PS_1SetExportIterations(JNIEnv *env, jclass cls, jboolean value)
+{
+	exportIterations = value;
+}
+
+bool PS_GetFlagExportIterations()
+{
+	return exportIterations;
+}
+
 //------------------------------------------------------------------------------
 // tidy up
 //------------------------------------------------------------------------------
@ -407,4 +419,4 @@ JNIEXPORT void __jlongpointer JNICALL Java_sparse_NDSparseMatrix_PS_1DeleteNDSpa
    if (ndsm) delete ndsm;
 }

-//------------------------------------------------------------------------------
+//------------------------------------------------------------------------------
--- a/prism/src/sparse/PrismSparse.java
+++ b/prism/src/sparse/PrismSparse.java
@ -138,6 +138,12 @@ public class PrismSparse
 		PS_SetTechLog(log);
 	}

+	private static native void PS_SetExportIterations(boolean value);
+	public static void SetExportIterations(boolean value)
+	{
+		PS_SetExportIterations(value);
+	}
+
 	//------------------------------------------------------------------------------
 	// error message
 	//------------------------------------------------------------------------------