s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

New option to export model to dot file with embedded state info (-exporttransdotstates). 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1433 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 17 years ago
parent
5210408a81
commit
57547299d9
14 changed files with 129 additions and 17 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 1
      prism/include/PrismMTBDDGlob.h
  2. 8
      prism/include/PrismNative.h
  3. 1
      prism/include/PrismSparseGlob.h
  4. 5
      prism/src/mtbdd/PM_ExportMatrix.cc
  5. 22
      prism/src/prism/Prism.java
  6. 28
      prism/src/prism/PrismCL.java
  7. 12
      prism/src/prism/PrismFileLog.java
  8. 11
      prism/src/prism/PrismNative.cc
  9. 1
      prism/src/prism/PrismNative.java
  10. 1
      prism/src/prism/StateList.java
  11. 32
      prism/src/prism/StateListMTBDD.java
  12. 7
      prism/src/sparse/PS_ExportMDP.cc
  13. 5
      prism/src/sparse/PS_ExportMatrix.cc
  14. 12
      prism/src/userinterface/model/GUIMultiModel.java

1
prism/include/PrismMTBDDGlob.h
View File

@ -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;

8
prism/include/PrismNative.h
View File

@ -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

1
prism/include/PrismSparseGlob.h
View File

@ -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;

5
prism/src/mtbdd/PM_ExportMatrix.cc
View File

@ -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;
}

22
prism/src/prism/Prism.java
View File

@ -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, ...)

28
prism/src/prism/PrismCL.java
View File

@ -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 <file> ......... Export the transition matrix graph to a dot file");
mainLog.println("-exporttransdotstates <file> ... Export the transition matrix graph to a dot file, with state info");
mainLog.println("-exportdot <file> .............. Export the transition matrix MTBDD to a dot file");
mainLog.println("-exportbsccs <file> ............ Compute and export all BSCCs of the model");
mainLog.println("-exportprism <file> ............ Export final PRISM model to a file");

12
prism/src/prism/PrismFileLog.java
View File

@ -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;
}
}

11
prism/src/prism/PrismNative.cc
View File

@ -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);

1
prism/src/prism/PrismNative.java
View File

@ -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);

1
prism/src/prism/StateList.java
View File

@ -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);

32
prism/src/prism/StateListMTBDD.java
View File

@ -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++;

7
prism/src/sparse/PS_ExportMDP.cc
View File

@ -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;
}

5
prism/src/sparse/PS_ExportMatrix.cc
View File

@ -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;
}

12
prism/src/userinterface/model/GUIMultiModel.java
View File

@ -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");

Write Preview
Loading…
Cancel
Save