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

Slight changes to exporttransdot format (to match explicit): boxes bot circles for states (works better when there are state labels) and larger dots for mdp transitions. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3283 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 15 years ago
parent
7737034db7
commit
f61753b14e
3 changed files with 4 additions and 4 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      prism/src/mtbdd/PM_ExportMatrix.cc
  2. 4
      prism/src/sparse/PS_ExportMDP.cc
  3. 2
      prism/src/sparse/PS_ExportMatrix.cc

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

@ -71,7 +71,7 @@ jstring fn // filename
switch (export_type) { 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_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_MATLAB: export_string("%s = sparse(%d,%d);\n", export_name, odd->eoff+odd->toff, odd->eoff+odd->toff); break;
case EXPORT_DOT: case EXPORT_DOT_STATES: export_string("digraph %s {\nsize=\"8,5\"\nnode [shape = circle];\n", export_name); break;
case EXPORT_DOT: case EXPORT_DOT_STATES: export_string("digraph %s {\nsize=\"8,5\"\nnode [shape = box];\n", export_name); break;
} }
// print main part of file // print main part of file

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

@ -100,7 +100,7 @@ jstring fn // filename
switch (export_type) { switch (export_type) {
case EXPORT_PLAIN: export_string("%d %d %d\n", n, nc, nnz); break; 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_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: case EXPORT_DOT_STATES: export_string("digraph %s {\nsize=\"8,5\"\nnode [shape = circle];\n", export_name); break;
case EXPORT_DOT: case EXPORT_DOT_STATES: export_string("digraph %s {\nsize=\"8,5\"\nnode [shape=box];\n", export_name); break;
case EXPORT_ROWS: export_string("%d %d %d\n", n, nc, nnz); break; case EXPORT_ROWS: export_string("%d %d %d\n", n, nc, nnz); break;
} }
@ -126,7 +126,7 @@ jstring fn // filename
export_string("%d -> n%d_%d [ arrowhead=none,label=\"%d", i, i, j-l1, j-l1); export_string("%d -> n%d_%d [ arrowhead=none,label=\"%d", i, i, j-l1, j-l1);
if (actions != NULL) export_string(":%s", (actions[j]>0?action_names[actions[j]-1]:"")); if (actions != NULL) export_string(":%s", (actions[j]>0?action_names[actions[j]-1]:""));
export_string("\" ];\n"); export_string("\" ];\n");
export_string("n%d_%d [ shape=point,label=\"\" ];\n", i, j-l1);
export_string("n%d_%d [ shape=point,width=0.1,height=0.1,label=\"\" ];\n", i, j-l1);
} }
for (k = l2; k < h2; k++) { for (k = l2; k < h2; k++) {
switch (export_type) { switch (export_type) {

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

@ -95,7 +95,7 @@ jstring fn // filename
switch (export_type) { switch (export_type) {
case EXPORT_PLAIN: export_string("%d %d\n", n, nnz); break; 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_MATLAB: export_string("%s = sparse(%d,%d);\n", export_name, n, n); break;
case EXPORT_DOT: case EXPORT_DOT_STATES: export_string("digraph %s {\nsize=\"8,5\"\nnode [shape = circle];\n", export_name); break;
case EXPORT_DOT: case EXPORT_DOT_STATES: export_string("digraph %s {\nsize=\"8,5\"\nnode [shape=box];\n", export_name); break;
case EXPORT_MRMC: export_string("STATES %d\nTRANSITIONS %d\n", n, nnz); 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; case EXPORT_ROWS: export_string("%d %d\n", n, nnz); break;
} }

Write Preview
Loading…
Cancel
Save