diff --git a/prism/include/PrismNative.h b/prism/include/PrismNative.h index 36bc84e6..058835c6 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_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 diff --git a/prism/include/PrismNativeGlob.h b/prism/include/PrismNativeGlob.h new file mode 100644 index 00000000..a1629f28 --- /dev/null +++ b/prism/include/PrismNativeGlob.h @@ -0,0 +1,46 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (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 + +//------------------------------------------------------------------------------ + +// 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; + +//------------------------------------------------------------------------------ diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 2b96605e..f7b211a2 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/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()); diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 71f79211..985084e0 100644 --- a/prism/src/prism/Prism.java +++ b/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() diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 29080bf7..9a577f1f 100644 --- a/prism/src/prism/PrismCL.java +++ b/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) { diff --git a/prism/src/prism/PrismNative.cc b/prism/src/prism/PrismNative.cc index 519e7566..abf40a06 100644 --- a/prism/src/prism/PrismNative.cc +++ b/prism/src/prism/PrismNative.cc @@ -30,6 +30,33 @@ #include #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) diff --git a/prism/src/prism/PrismNative.java b/prism/src/prism/PrismNative.java index 27ad2a67..72c77aed 100644 --- a/prism/src/prism/PrismNative.java +++ b/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); diff --git a/prism/src/prism/PrismSettings.java b/prism/src/prism/PrismSettings.java index 730eaa8e..cf71c9df 100644 --- a/prism/src/prism/PrismSettings.java +++ b/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." }, diff --git a/prism/src/sparse/PS_NondetUntil.cc b/prism/src/sparse/PS_NondetUntil.cc index a5734aac..bce0d160 100644 --- a/prism/src/sparse/PS_NondetUntil.cc +++ b/prism/src/sparse/PS_NondetUntil.cc @@ -34,6 +34,7 @@ #include #include "sparse.h" #include "prism.h" +#include "PrismNativeGlob.h" #include "PrismSparseGlob.h" #include "jnipointer.h" #include @@ -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