diff --git a/prism/include/PrismMTBDDGlob.h b/prism/include/PrismMTBDDGlob.h index 8b4abcd2..789da200 100644 --- a/prism/include/PrismMTBDDGlob.h +++ b/prism/include/PrismMTBDDGlob.h @@ -36,6 +36,7 @@ const int EXPORT_MATLAB = 2; const int EXPORT_DOT = 3; const int EXPORT_MRMC = 4; const int EXPORT_ROWS = 5; +const int EXPORT_DOT_STATES = 6; const int LIN_EQ_METHOD_POWER = 1; const int LIN_EQ_METHOD_JACOBI = 2; diff --git a/prism/include/PrismNative.h b/prism/include/PrismNative.h index 013d22e5..36bc84e6 100644 --- a/prism/include/PrismNative.h +++ b/prism/include/PrismNative.h @@ -23,6 +23,14 @@ JNIEXPORT jlong JNICALL Java_prism_PrismNative_PN_1GetStdout JNIEXPORT jlong JNICALL Java_prism_PrismNative_PN_1OpenFile (JNIEnv *, jclass, jstring); +/* + * Class: prism_PrismNative + * Method: PN_OpenFileAppend + * Signature: (Ljava/lang/String;)J + */ +JNIEXPORT jlong JNICALL Java_prism_PrismNative_PN_1OpenFileAppend + (JNIEnv *, jclass, jstring); + /* * Class: prism_PrismNative * Method: PN_PrintToFile diff --git a/prism/include/PrismSparseGlob.h b/prism/include/PrismSparseGlob.h index acbfb6f5..641101bc 100644 --- a/prism/include/PrismSparseGlob.h +++ b/prism/include/PrismSparseGlob.h @@ -36,6 +36,7 @@ const int EXPORT_MATLAB = 2; const int EXPORT_DOT = 3; const int EXPORT_MRMC = 4; const int EXPORT_ROWS = 5; +const int EXPORT_DOT_STATES = 6; const int LIN_EQ_METHOD_POWER = 1; const int LIN_EQ_METHOD_JACOBI = 2; diff --git a/prism/src/mtbdd/PM_ExportMatrix.cc b/prism/src/mtbdd/PM_ExportMatrix.cc index a1aa4359..4a57385e 100644 --- a/prism/src/mtbdd/PM_ExportMatrix.cc +++ b/prism/src/mtbdd/PM_ExportMatrix.cc @@ -71,7 +71,7 @@ jstring fn // filename switch (export_type) { case EXPORT_PLAIN: export_string("%d %.0f\n", odd->eoff+odd->toff, DD_GetNumMinterms(ddman, matrix, num_rvars+num_cvars)); break; case EXPORT_MATLAB: export_string("%s = sparse(%d,%d);\n", export_name, odd->eoff+odd->toff, odd->eoff+odd->toff); break; - case EXPORT_DOT: export_string("digraph %s {\nsize=\"8,5\"\norientation=land;\nnode [shape = circle];\n", export_name); break; + case EXPORT_DOT: case EXPORT_DOT_STATES: export_string("digraph %s {\nsize=\"8,5\"\nnode [shape = circle];\n", export_name); break; } // print main part of file @@ -79,6 +79,7 @@ jstring fn // filename // print file footer switch (export_type) { + // Note: no footer for EXPORT_DOT_STATES case EXPORT_DOT: export_string("}\n"); break; } @@ -103,7 +104,7 @@ static void export_rec(DdNode *dd, DdNode **rvars, DdNode **cvars, int num_vars, switch (export_type) { case EXPORT_PLAIN: export_string("%d %d %.12g\n", r, c, Cudd_V(dd)); break; case EXPORT_MATLAB: export_string("%s(%d,%d)=%.12g;\n", export_name, r+1, c+1, Cudd_V(dd)); break; - case EXPORT_DOT: export_string("%d -> %d [ label=\"%.12g\" ];\n", r, c, Cudd_V(dd)); break; + case EXPORT_DOT: case EXPORT_DOT_STATES: export_string("%d -> %d [ label=\"%.12g\" ];\n", r, c, Cudd_V(dd)); break; } return; } diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index d0f55686..83dd0547 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -82,6 +82,7 @@ public class Prism implements PrismSettingsListener public static final int EXPORT_DOT = 3; public static final int EXPORT_MRMC = 4; public static final int EXPORT_ROWS = 5; + public static final int EXPORT_DOT_STATES = 6; // methods for SCC decomposition public static final int XIEBEEREL = 1; @@ -1022,11 +1023,32 @@ public class Prism implements PrismSettingsListener case EXPORT_DOT: mainLog.print("in Dot format "); break; case EXPORT_MRMC: mainLog.print("in MRMC format "); break; case EXPORT_ROWS: mainLog.print("in rows format "); break; + case EXPORT_DOT_STATES: mainLog.print("in Dot format (with states) "); break; } if (file != null) mainLog.println("to file \"" + file + "\"..."); else mainLog.println("below:"); // do export model.exportToFile(exportType, ordered, file); + + // for export to dotm with states, need to do a bit more + if (exportType == EXPORT_DOT_STATES) { + // open (appending to) existing new file log or use main log + PrismLog tmpLog; + if (file != null) { + tmpLog = new PrismFileLog(file.getPath(), true); + if (!tmpLog.ready()) { + throw new FileNotFoundException(); + } + } else { + tmpLog = mainLog; + } + // insert states info into dot file + model.getReachableStates().printDot(tmpLog); + // print footer + tmpLog.println("}"); + // tidy up + if (file != null) tmpLog.close(); + } } // export state rewards to a file (plain, matlab, ...) diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 63020007..5996daac 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -53,6 +53,7 @@ public class PrismCL private boolean exportspy = false; private boolean exportdot = false; private boolean exporttransdot = false; + private boolean exporttransdotstates = false; private boolean exportbsccs = false; private boolean exportresults = false; private boolean exportprism = false; @@ -88,6 +89,7 @@ public class PrismCL private String exportSpyFilename = null; private String exportDotFilename = null; private String exportTransDotFilename = null; + private String exportTransDotStatesFilename = null; private String exportBSCCsFilename = null; private String exportResultsFilename = null; private String exportPrismFilename = null; @@ -724,6 +726,21 @@ public class PrismCL } } + // export transition matrix graph to dot file (with states) + if (exporttransdotstates) { + try { + File f = (exportTransDotStatesFilename.equals("stdout")) ? null : new File(exportTransDotStatesFilename); + prism.exportTransToFile(model, exportordered, Prism.EXPORT_DOT_STATES, f); + } + // in case of error, report it and proceed + catch (FileNotFoundException e) { + error("Couldn't open file \"" + exportTransDotStatesFilename + "\" for output"); + } + catch (PrismException e) { + error(e.getMessage()); + } + } + // export BSCCs to a file if (exportbsccs) { try { @@ -942,6 +959,16 @@ public class PrismCL errorAndExit("No file specified for -"+sw+" switch"); } } + // export transition matrix graph to dot file (with states) + else if (sw.equals("exporttransdotstates")) { + if (i < args.length-1) { + exporttransdotstates = true; + exportTransDotStatesFilename = args[++i]; + } + else { + errorAndExit("No file specified for -"+sw+" switch"); + } + } // export bsccs to file else if (sw.equals("exportbsccs")) { if (i < args.length-1) { @@ -1654,6 +1681,7 @@ public class PrismCL mainLog.println("-exportordered ................. When exporting matrices, order entries (by row) [default]"); mainLog.println("-exportunordered ............... When exporting matrices, don't order entries"); mainLog.println("-exporttransdot ......... Export the transition matrix graph to a dot file"); + mainLog.println("-exporttransdotstates ... Export the transition matrix graph to a dot file, with state info"); mainLog.println("-exportdot .............. Export the transition matrix MTBDD to a dot file"); mainLog.println("-exportbsccs ............ Compute and export all BSCCs of the model"); mainLog.println("-exportprism ............ Export final PRISM model to a file"); diff --git a/prism/src/prism/PrismFileLog.java b/prism/src/prism/PrismFileLog.java index f29ce328..c1cd3c58 100644 --- a/prism/src/prism/PrismFileLog.java +++ b/prism/src/prism/PrismFileLog.java @@ -43,7 +43,17 @@ public class PrismFileLog implements PrismLog open(s); } + public PrismFileLog(String s, boolean append) + { + open(s, append); + } + public void open(String s) + { + open (s, false); + } + + public void open(String s, boolean append) { filename = s; if (s.equals("stdout")) { @@ -51,7 +61,7 @@ public class PrismFileLog implements PrismLog stdout = true; } else { - fp = PrismNative.PN_OpenFile(s); + fp = append ? PrismNative.PN_OpenFileAppend(s) : PrismNative.PN_OpenFile(s); stdout = false; } } diff --git a/prism/src/prism/PrismNative.cc b/prism/src/prism/PrismNative.cc index d6e741e4..519e7566 100644 --- a/prism/src/prism/PrismNative.cc +++ b/prism/src/prism/PrismNative.cc @@ -51,6 +51,17 @@ JNIEXPORT jlong __jlongpointer JNICALL Java_prism_PrismNative_PN_1OpenFile(JNIEn //------------------------------------------------------------------------------ +JNIEXPORT jlong __jlongpointer JNICALL Java_prism_PrismNative_PN_1OpenFileAppend(JNIEnv *env, jclass cls, jstring filename) +{ + const char *str = env->GetStringUTFChars(filename, 0); + FILE *fp = fopen(str, "a"); + env->ReleaseStringUTFChars(filename, str); + return ptr_to_jlong(fp); +} + +//------------------------------------------------------------------------------ + + JNIEXPORT void JNICALL Java_prism_PrismNative_PN_1PrintToFile(JNIEnv *env, jclass cls, jlong __jlongpointer fp, jstring s) { const char *str = env->GetStringUTFChars(s, 0); diff --git a/prism/src/prism/PrismNative.java b/prism/src/prism/PrismNative.java index 4dc1f565..27ad2a67 100644 --- a/prism/src/prism/PrismNative.java +++ b/prism/src/prism/PrismNative.java @@ -45,6 +45,7 @@ public class PrismNative public static native long PN_GetStdout(); public static native long PN_OpenFile(String filename); + public static native long PN_OpenFileAppend(String filename); public static native void PN_PrintToFile(long fp, String s); public static native void PN_FlushFile(long fp); public static native void PN_CloseFile(long fp); diff --git a/prism/src/prism/StateList.java b/prism/src/prism/StateList.java index 42538db0..b8be03cf 100644 --- a/prism/src/prism/StateList.java +++ b/prism/src/prism/StateList.java @@ -37,6 +37,7 @@ public interface StateList String sizeString(); void print(PrismLog log); void printMatlab(PrismLog log); + void printDot(PrismLog log); void print(PrismLog log, int n); void printMatlab(PrismLog log, int n); boolean includes(JDDNode state); diff --git a/prism/src/prism/StateListMTBDD.java b/prism/src/prism/StateListMTBDD.java index a8cc21a4..98ecb007 100644 --- a/prism/src/prism/StateListMTBDD.java +++ b/prism/src/prism/StateListMTBDD.java @@ -61,8 +61,9 @@ public class StateListMTBDD implements StateList // log for output from print method PrismLog outputLog; - // output in Matlab format? - boolean matlab = false; + // output format + enum OutputFormat { NORMAL, MATLAB, DOT }; + OutputFormat outputFormat = OutputFormat.NORMAL; // constructor @@ -112,9 +113,15 @@ public class StateListMTBDD implements StateList } public void printMatlab(PrismLog log) { - matlab = true; + outputFormat = OutputFormat.MATLAB; print(log); - matlab = false; + outputFormat = OutputFormat.NORMAL; + } + public void printDot(PrismLog log) + { + outputFormat = OutputFormat.DOT; + print(log); + outputFormat = OutputFormat.NORMAL; } // print first n states of list @@ -128,9 +135,9 @@ public class StateListMTBDD implements StateList } public void printMatlab(PrismLog log, int n) { - matlab = true; + outputFormat = OutputFormat.MATLAB; print(log, n); - matlab = false; + outputFormat = OutputFormat.NORMAL; } // printing method @@ -171,7 +178,12 @@ public class StateListMTBDD implements StateList // base case - at bottom (nonzero terminal) if (level == numVars) { - if (!matlab) outputLog.print(n + ":("); + switch (outputFormat) { + case NORMAL: outputLog.print(n + ":("); break; + case MATLAB: break; + case DOT: outputLog.print(n + " [label=\"" + n + "\\n("); break; + } + if (outputFormat == OutputFormat.NORMAL) outputLog.print(n + ":("); j = varList.getNumVars(); for (i = 0; i < j; i++) { // integer variable @@ -184,7 +196,11 @@ public class StateListMTBDD implements StateList } if (i < j-1) outputLog.print(","); } - if (!matlab) outputLog.print(")"); + switch (outputFormat) { + case NORMAL: outputLog.print(")"); break; + case MATLAB: break; + case DOT: outputLog.print(")\"];"); break; + } outputLog.println(); count++; diff --git a/prism/src/sparse/PS_ExportMDP.cc b/prism/src/sparse/PS_ExportMDP.cc index 9a34aaab..34450c71 100644 --- a/prism/src/sparse/PS_ExportMDP.cc +++ b/prism/src/sparse/PS_ExportMDP.cc @@ -84,7 +84,7 @@ jstring fn // filename switch (export_type) { case EXPORT_PLAIN: export_string("%d %d %d\n", n, nc, nnz); break; case EXPORT_MATLAB: for (i = 0; i < ndsm->k; i++) export_string("%s%d = sparse(%d,%d);\n", export_name, i+1, n, n); break; - case EXPORT_DOT: export_string("digraph %s {\nsize=\"8,5\"\norientation=land;\nnode [shape = circle];\n", export_name); break; + case EXPORT_DOT: case EXPORT_DOT_STATES: export_string("digraph %s {\nsize=\"8,5\"\nnode [shape = circle];\n", export_name); break; case EXPORT_ROWS: export_string("%d %d %d\n", n, nc, nnz); break; } @@ -106,7 +106,7 @@ jstring fn // filename if (!use_counts) { l2 = choice_starts[j]; h2 = choice_starts[j+1]; } else { l2 = h2; h2 += choice_counts[j]; } if (export_type == EXPORT_ROWS) export_string("%d", i); - else if (export_type == EXPORT_DOT) { + else if (export_type == EXPORT_DOT || export_type == EXPORT_DOT_STATES) { export_string("%d -> %d.%d [ arrowhead=none,label=\"%d\" ];\n", i, i, j-l1, j-l1); export_string("%d.%d [ shape=circle,width=0.1,height=0.1,label=\"\" ];\n", i, j-l1); } @@ -114,7 +114,7 @@ jstring fn // filename switch (export_type) { case EXPORT_PLAIN: export_string("%d %d %d %.12g\n", i, j-l1, cols[k], non_zeros[k]); break; case EXPORT_MATLAB: export_string("%s%d(%d,%d)=%.12g;\n", export_name, j-l1+1, i+1, cols[k]+1, non_zeros[k]); break; - case EXPORT_DOT: export_string("%d.%d -> %d [ label=\"%.12g\" ];\n", i, j-l1, cols[k], non_zeros[k]); break; + case EXPORT_DOT: case EXPORT_DOT_STATES: export_string("%d.%d -> %d [ label=\"%.12g\" ];\n", i, j-l1, cols[k], non_zeros[k]); break; case EXPORT_ROWS: export_string(" %.12g:%d", non_zeros[k], cols[k]); break; } } @@ -124,6 +124,7 @@ jstring fn // filename // print file footer switch (export_type) { + // Note: no footer for EXPORT_DOT_STATES case EXPORT_DOT: export_string("}\n"); break; } diff --git a/prism/src/sparse/PS_ExportMatrix.cc b/prism/src/sparse/PS_ExportMatrix.cc index 322f48fa..202c5c19 100644 --- a/prism/src/sparse/PS_ExportMatrix.cc +++ b/prism/src/sparse/PS_ExportMatrix.cc @@ -95,7 +95,7 @@ jstring fn // filename switch (export_type) { case EXPORT_PLAIN: export_string("%d %d\n", n, nnz); break; case EXPORT_MATLAB: export_string("%s = sparse(%d,%d);\n", export_name, n, n); break; - case EXPORT_DOT: export_string("digraph %s {\nsize=\"8,5\"\norientation=land;\nnode [shape = circle];\n", export_name); break; + case EXPORT_DOT: case EXPORT_DOT_STATES: export_string("digraph %s {\nsize=\"8,5\"\nnode [shape = circle];\n", export_name); break; case EXPORT_MRMC: export_string("STATES %d\nTRANSITIONS %d\n", n, nnz); break; case EXPORT_ROWS: export_string("%d %d\n", n, nnz); break; } @@ -146,7 +146,7 @@ jstring fn // filename switch (export_type) { case EXPORT_PLAIN: export_string("%d %d %.12g\n", r, c, d); break; case EXPORT_MATLAB: export_string("%s(%d,%d)=%.12g;\n", export_name, r+1, c+1, d); break; - case EXPORT_DOT: export_string("%d -> %d [ label=\"%.12g\" ];\n", r, c, d); break; + case EXPORT_DOT: case EXPORT_DOT_STATES: export_string("%d -> %d [ label=\"%.12g\" ];\n", r, c, d); break; case EXPORT_MRMC: export_string("%d %d %.12g\n", r+1, c+1, d); break; case EXPORT_ROWS: export_string(" %.12g:%d", d, c); break; } @@ -156,6 +156,7 @@ jstring fn // filename // print file footer switch (export_type) { + // Note: no footer for EXPORT_DOT_STATES case EXPORT_DOT: export_string("}\n"); break; } diff --git a/prism/src/userinterface/model/GUIMultiModel.java b/prism/src/userinterface/model/GUIMultiModel.java index 4a56a8d1..4b446224 100644 --- a/prism/src/userinterface/model/GUIMultiModel.java +++ b/prism/src/userinterface/model/GUIMultiModel.java @@ -61,7 +61,7 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener private AbstractAction viewStates, viewTrans, viewStateRewards, viewTransRewards, viewPrismCode, computeSS, computeTr, newPRISMModel, newGraphicModel, newPEPAModel, loadModel, reloadModel, saveModel, saveAsModel, parseModel, buildModel, - exportStatesPlain, exportStatesMatlab, exportTransPlain, exportTransMatlab, exportTransDot, exportTransMRMC, + exportStatesPlain, exportStatesMatlab, exportTransPlain, exportTransMatlab, exportTransDot, exportTransDotStates, exportTransMRMC, exportStateRewardsPlain, exportStateRewardsMatlab, exportStateRewardsMRMC, exportTransRewardsPlain, exportTransRewardsMatlab, exportTransRewardsMRMC; private JPopupMenu popup; @@ -145,6 +145,7 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener exportTransPlain.setEnabled(!computing); exportTransMatlab.setEnabled(!computing); exportTransDot.setEnabled(!computing); + exportTransDotStates.setEnabled(!computing); exportTransMRMC.setEnabled(!computing); exportStateRewardsPlain.setEnabled(!computing); exportStateRewardsMatlab.setEnabled(!computing); @@ -315,6 +316,7 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener // pop up dialog to select file switch (exportType) { case Prism.EXPORT_DOT: res = showSaveFileDialog(dotFilter, dotFilter[0]); break; + case Prism.EXPORT_DOT_STATES: res = showSaveFileDialog(dotFilter, dotFilter[0]); break; case Prism.EXPORT_MATLAB: res = showSaveFileDialog(matlabFilter, matlabFilter[0]); break; default: res = showSaveFileDialog(textFilter, textFilter[0]); break; } @@ -565,6 +567,13 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener exportTransDot.putValue(Action.NAME, "Dot file"); exportTransDot.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallFileDot.png")); + exportTransDotStates = new AbstractAction() { public void actionPerformed(ActionEvent e) { + a_exportBuildAs(GUIMultiModelHandler.TRANS_EXPORT, Prism.EXPORT_DOT_STATES); } }; + exportTransDotStates.putValue(Action.LONG_DESCRIPTION, "Exports the transition matrix graph to a Dot file (with states)"); + exportTransDotStates.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_S)); + exportTransDotStates.putValue(Action.NAME, "Dot file (with states)"); + exportTransDotStates.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallFileDot.png")); + exportTransMRMC = new AbstractAction() { public void actionPerformed(ActionEvent e) { a_exportBuildAs(GUIMultiModelHandler.TRANS_EXPORT, Prism.EXPORT_MRMC); } }; exportTransMRMC.putValue(Action.LONG_DESCRIPTION, "Exports the transition matrix to a MRMC file"); @@ -809,6 +818,7 @@ public class GUIMultiModel extends GUIPlugin implements PrismSettingsListener exportTransMenu.add(exportTransPlain); exportTransMenu.add(exportTransMatlab); exportTransMenu.add(exportTransDot); + exportTransMenu.add(exportTransDotStates); exportTransMenu.add(exportTransMRMC); exportMenu.add(exportTransMenu); exportStateRewardsMenu = new JMenu("State rewards");