From a1b7a85a2986c31f48fdcbb07da9d69cf483f80e Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 26 Apr 2007 11:23:07 +0000 Subject: [PATCH] Added new "rows" format for matrix export and -exportrows command-line switch. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@316 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/include/PrismMTBDDGlob.h | 1 + prism/include/PrismSparseGlob.h | 1 + prism/src/prism/Prism.java | 20 +++++++++++++++++++- prism/src/prism/PrismCL.java | 5 +++++ prism/src/sparse/PS_ExportMDP.cc | 4 ++++ prism/src/sparse/PS_ExportMatrix.cc | 4 ++++ prism/src/sparse/PS_ExportSubMDP.cc | 4 ++++ 7 files changed, 38 insertions(+), 1 deletion(-) diff --git a/prism/include/PrismMTBDDGlob.h b/prism/include/PrismMTBDDGlob.h index 062b7d99..0ad7d815 100644 --- a/prism/include/PrismMTBDDGlob.h +++ b/prism/include/PrismMTBDDGlob.h @@ -35,6 +35,7 @@ const int EXPORT_PLAIN = 1; const int EXPORT_MATLAB = 2; const int EXPORT_DOT = 3; const int EXPORT_MRMC = 4; +const int EXPORT_ROWS = 5; const int LIN_EQ_METHOD_POWER = 1; const int LIN_EQ_METHOD_JACOBI = 2; diff --git a/prism/include/PrismSparseGlob.h b/prism/include/PrismSparseGlob.h index c322d3b8..668f0f7c 100644 --- a/prism/include/PrismSparseGlob.h +++ b/prism/include/PrismSparseGlob.h @@ -35,6 +35,7 @@ const int EXPORT_PLAIN = 1; const int EXPORT_MATLAB = 2; const int EXPORT_DOT = 3; const int EXPORT_MRMC = 4; +const int EXPORT_ROWS = 5; const int LIN_EQ_METHOD_POWER = 1; const int LIN_EQ_METHOD_JACOBI = 2; diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index d095b461..c49ece6c 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -79,6 +79,7 @@ public class Prism implements PrismSettingsListener public static final int EXPORT_MATLAB = 2; public static final int EXPORT_DOT = 3; public static final int EXPORT_MRMC = 4; + public static final int EXPORT_ROWS = 5; //------------------------------------------------------------------------------ // Settings / flags / options @@ -916,6 +917,11 @@ public class Prism implements PrismSettingsListener if (!ordered) mainLog.println("\nWarning: Cannot export unordered transition matrix in MRMC format; using ordered."); ordered = true; } + // can only do ordered version of export for rows format + if (exportType == EXPORT_ROWS) { + if (!ordered) mainLog.println("\nWarning: Cannot export unordered transition matrix in rows format; using ordered."); + ordered = true; + } // print message mainLog.print("\nExporting transition matrix "); @@ -924,6 +930,7 @@ public class Prism implements PrismSettingsListener case EXPORT_MATLAB: mainLog.print("in Matlab format "); break; 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; } if (file != null) mainLog.println("to file \"" + file + "\"..."); else mainLog.println("below:"); @@ -937,6 +944,9 @@ public class Prism implements PrismSettingsListener { String s; + // rows format does not apply to vectors + if (exportType == EXPORT_ROWS) exportType = EXPORT_PLAIN; + // print message mainLog.print("\nExporting state rewards vector "); switch (exportType) { @@ -967,6 +977,11 @@ public class Prism implements PrismSettingsListener if (!ordered) mainLog.println("\nWarning: Cannot export unordered transition reward matrix in MRMC format; using ordered"); ordered = true; } + // can only do ordered version of export for rows format + if (exportType == EXPORT_ROWS) { + if (!ordered) mainLog.println("\nWarning: Cannot export unordered transition matrix in rows format; using ordered."); + ordered = true; + } // print message mainLog.print("\nExporting transition rewards matrix "); @@ -974,6 +989,7 @@ public class Prism implements PrismSettingsListener case EXPORT_PLAIN: mainLog.print("in plain text format "); break; case EXPORT_MATLAB: mainLog.print("in Matlab format "); break; case EXPORT_MRMC: mainLog.print("in MRMC format "); break; + case EXPORT_ROWS: mainLog.print("in rows format "); break; } if (file != null) mainLog.println("to file \"" + file + "\"..."); else mainLog.println("below:"); @@ -990,8 +1006,10 @@ public class Prism implements PrismSettingsListener int i; PrismLog tmpLog; - // no specific format for MRMC + // no specific states format for MRMC if (exportType == EXPORT_MRMC) exportType = EXPORT_PLAIN; + // rows format does not apply to states output + if (exportType == EXPORT_ROWS) exportType = EXPORT_PLAIN; // print message mainLog.print("\nExporting list of reachable states "); diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 78508f7b..e8d0ee64 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -877,6 +877,10 @@ public class PrismCL else if (sw.equals("exportmrmc")) { exportType = Prism.EXPORT_MRMC; } + // switch export mode to "rows" + else if (sw.equals("exportrows")) { + exportType = Prism.EXPORT_ROWS; + } // export model to plain text file (deprecated) else if (sw.equals("exportplain")) { if (i < args.length-1) { @@ -1462,6 +1466,7 @@ public class PrismCL mainLog.println("-exportlabels ........... Export the list of labels and satisfying states to a file"); mainLog.println("-exportmatlab .................. When exporting matrices/vectors/labels/etc., use Matlab format"); mainLog.println("-exportmrmc .................... When exporting matrices/vectors/labels, use MRMC format"); + mainLog.println("-exportrows .................... When exporting matrices, put a whole row on one line"); 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"); diff --git a/prism/src/sparse/PS_ExportMDP.cc b/prism/src/sparse/PS_ExportMDP.cc index 26af0287..79505a65 100644 --- a/prism/src/sparse/PS_ExportMDP.cc +++ b/prism/src/sparse/PS_ExportMDP.cc @@ -81,6 +81,7 @@ jstring fn // filename 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_ROWS: export_string("%d %d %d\n", n, nc, nnz); break; } // print main part of file @@ -100,13 +101,16 @@ jstring fn // filename for (j = l1; j < h1; j++) { 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); for (k = l2; k < h2; k++) { 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 [ label=\"%d: %.12g\" ];\n", i, cols[k], j-l1, non_zeros[k]); break; + case EXPORT_ROWS: export_string(" %.12g:%d", non_zeros[k], cols[k]); break; } } + if (export_type == EXPORT_ROWS) export_string("\n"); } } diff --git a/prism/src/sparse/PS_ExportMatrix.cc b/prism/src/sparse/PS_ExportMatrix.cc index db6321fb..402920c9 100644 --- a/prism/src/sparse/PS_ExportMatrix.cc +++ b/prism/src/sparse/PS_ExportMatrix.cc @@ -93,6 +93,7 @@ jstring fn // filename 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_MRMC: export_string("STATES %d\nTRANSITIONS %d\n", n, nnz); break; + case EXPORT_ROWS: export_string("%d %d\n", n, nnz); break; } // print main part of file @@ -125,6 +126,7 @@ jstring fn // filename for (i = 0; i < n; i++) { if (!use_counts) { l = row_starts[i]; h = row_starts[i+1]; } else { l = h; h += row_counts[i]; } + if (export_type == EXPORT_ROWS) export_string("%d", i); for (j = l; j < h; j++) { r = i; // "row major" version @@ -142,8 +144,10 @@ jstring fn // filename 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_MRMC: export_string("%d %d %.12g\n", r+1, c+1, d); break; + case EXPORT_ROWS: export_string(" %.12g:%d", d, c); break; } } + if (export_type == EXPORT_ROWS) export_string("\n"); } // print file footer diff --git a/prism/src/sparse/PS_ExportSubMDP.cc b/prism/src/sparse/PS_ExportSubMDP.cc index a8424700..b0515706 100644 --- a/prism/src/sparse/PS_ExportSubMDP.cc +++ b/prism/src/sparse/PS_ExportSubMDP.cc @@ -82,6 +82,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_ROWS: export_string("%d %d %d\n", n, nc, nnz); break; } // print main part of file @@ -101,12 +102,15 @@ jstring fn // filename for (j = l1; j < h1; j++) { 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); for (k = l2; k < h2; k++) { 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_ROWS: export_string(" %.12g:%d", non_zeros[k], cols[k]); break; } } + if (export_type == EXPORT_ROWS) export_string("\n"); } }