diff --git a/prism/include/ExportIterations.h b/prism/include/ExportIterations.h new file mode 100644 index 00000000..d1f73f7c --- /dev/null +++ b/prism/include/ExportIterations.h @@ -0,0 +1,110 @@ +//============================================================================== +// +// Copyright (c) 2016- +// Authors: +// * Joachim Klein (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 +#include +#include + +#include +#include +#include "dv.h" +#include "prism.h" +#include + +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, "\n"); + fprintf(fp, "\n"); + fprintf(fp, "\n"); + fprintf(fp, "\n"); + fprintf(fp, "\n"); + fprintf(fp, "\n"); + fprintf(fp, "%s\n", title); + fprintf(fp, "\n"); + fprintf(fp, "\n"); + fprintf(fp, "\n"); + fprintf(fp, "

%s

\n", title); + fprintf(fp, "\n"); + fprintf(fp, "\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, "\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, "\n"); + fclose(fp); + } +}; + +#endif diff --git a/prism/include/PrismHybrid.h b/prism/include/PrismHybrid.h index 06ce8c89..a652b60e 100644 --- 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 diff --git a/prism/include/PrismHybridGlob.h b/prism/include/PrismHybridGlob.h index a11615be..c27eeb02 100644 --- 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(); //------------------------------------------------------------------------------ diff --git a/prism/include/PrismMTBDD.h b/prism/include/PrismMTBDD.h index 5de04d58..259a4447 100644 --- 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 diff --git a/prism/include/PrismMTBDDGlob.h b/prism/include/PrismMTBDDGlob.h index 801eb253..1eeead0c 100644 --- 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(); //------------------------------------------------------------------------------ diff --git a/prism/include/PrismNative.h b/prism/include/PrismNative.h index d6c28117..ab4a4a24 100644 --- 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 diff --git a/prism/include/PrismNativeGlob.h b/prism/include/PrismNativeGlob.h index 54e820bc..a44acda9 100644 --- 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; //------------------------------------------------------------------------------ diff --git a/prism/include/PrismSparse.h b/prism/include/PrismSparse.h index 4a97de6b..222df9c7 100644 --- 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 diff --git a/prism/include/PrismSparseGlob.h b/prism/include/PrismSparseGlob.h index 04e9d4fc..4574e451 100644 --- 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(); //------------------------------------------------------------------------------ diff --git a/prism/include/prism.h b/prism/include/prism.h index 88791f32..735bece5 100644 --- 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) diff --git a/prism/src/explicit/ExportIterations.java b/prism/src/explicit/ExportIterations.java new file mode 100644 index 00000000..04e658ef --- /dev/null +++ b/prism/src/explicit/ExportIterations.java @@ -0,0 +1,153 @@ +//============================================================================== +// +// Copyright (c) 2016- +// Authors: +// * Joachim Klein (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(""); + log.println(""); + log.println(""); + log.println(""); + log.println(""); + log.println(""); + log.println("" + title + ""); + log.println(""); + log.println(""); + log.println(""); + log.println("

" + title + "

"); + log.println(""); + log.println(""); + } + + /** + * 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("\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("\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"); + } + + public static void setDefaultFilename(String newDefaultFilename) + { + defaultFilename = newDefaultFilename; + } + + public static String getDefaultFilename() + { + return defaultFilename; + } + + public static void resetDefaultFilename() + { + defaultFilename = "iterations.html"; + } +} diff --git a/prism/src/hybrid/PrismHybrid.cc b/prism/src/hybrid/PrismHybrid.cc index 649dfe96..ded3eb2b 100644 --- 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 //------------------------------------------------------------------------------ diff --git a/prism/src/hybrid/PrismHybrid.java b/prism/src/hybrid/PrismHybrid.java index 7abd0c36..f856146b 100644 --- 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 //------------------------------------------------------------------------------ diff --git a/prism/src/mtbdd/Makefile b/prism/src/mtbdd/Makefile index d08908b3..78bc14a6 100644 --- 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) diff --git a/prism/src/mtbdd/PrismMTBDD.cc b/prism/src/mtbdd/PrismMTBDD.cc index 7e9fb83e..8148239b 100644 --- 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 //------------------------------------------------------------------------------ diff --git a/prism/src/mtbdd/PrismMTBDD.java b/prism/src/mtbdd/PrismMTBDD.java index 937a1f3b..60a91dab 100644 --- 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 //------------------------------------------------------------------------------ diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index dbf993eb..d9402477 100644 --- 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)); } //------------------------------------------------------------------------------ diff --git a/prism/src/prism/PrismNative.cc b/prism/src/prism/PrismNative.cc index 634cb047..ba4cb28b 100644 --- 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); diff --git a/prism/src/prism/PrismNative.java b/prism/src/prism/PrismNative.java index 7847978f..28c58c74 100644 --- 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) { diff --git a/prism/src/prism/PrismSettings.java b/prism/src/prism/PrismSettings.java index 8e7c41b8..d2c30db3 100644 --- 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 ........... Export an adversary from MDP model checking (as an MDP)"); mainLog.println("-ltl2datool ............. Run executable to convert LTL formulas to deterministic automata"); mainLog.println("-ltl2dasyntax .............. 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:"); diff --git a/prism/src/prism/prism.cc b/prism/src/prism/prism.cc index 8ae72592..52d87ee8 100644 --- a/prism/src/prism/prism.cc +++ b/prism/src/prism/prism.cc @@ -32,6 +32,7 @@ #include #include #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; +} +//------------------------------------------------------------------------------ diff --git a/prism/src/sparse/PrismSparse.cc b/prism/src/sparse/PrismSparse.cc index 83ef00d6..bd0bc6e7 100644 --- 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; } -//------------------------------------------------------------------------------ \ No newline at end of file +//------------------------------------------------------------------------------ diff --git a/prism/src/sparse/PrismSparse.java b/prism/src/sparse/PrismSparse.java index 0ab390ac..c23b0f1f 100644 --- 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 //------------------------------------------------------------------------------