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

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
master
Dave Parker 20 years ago
parent
ea856282e1
commit
a1b7a85a29
7 changed files with 38 additions and 1 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. 1
      prism/include/PrismSparseGlob.h
  3. 20
      prism/src/prism/Prism.java
  4. 5
      prism/src/prism/PrismCL.java
  5. 4
      prism/src/sparse/PS_ExportMDP.cc
  6. 4
      prism/src/sparse/PS_ExportMatrix.cc
  7. 4
      prism/src/sparse/PS_ExportSubMDP.cc

1
prism/include/PrismMTBDDGlob.h
View File

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

1
prism/include/PrismSparseGlob.h
View File

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

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

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

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

@ -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 <file> ........... 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 <file> ......... Export the transition matrix graph to a dot file");

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

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

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

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

4
prism/src/sparse/PS_ExportSubMDP.cc
View File

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

Write Preview
Loading…
Cancel
Save