From 341efe4d21d468665362aba8c8b8a3b66f015f58 Mon Sep 17 00:00:00 2001 From: Chris Novakovic Date: Wed, 26 Sep 2018 17:15:14 +0100 Subject: [PATCH] Don't hardcode maximum dimensions for DOT graphs When DOT graphs of a model are exported, their maximum permitted size is hardcoded to 8 inches wide by 5 inches high, which is too small for the rendered drawing to be useful (e.g. during debugging) for all but the simplest of models. Remove the maximum size restriction, allowing tools to render the drawing with its natural dimensions. --- prism-tests/functionality/export/dot/cluster.sm.dot | 1 - prism-tests/functionality/export/dot/cluster.sm.sta.dot | 1 - prism-tests/functionality/export/dot/dice.pm.dot | 1 - prism-tests/functionality/export/dot/dice.pm.sta.dot | 1 - prism-tests/functionality/export/dot/robot.prism.dot | 1 - prism-tests/functionality/export/dot/robot.prism.sta.dot | 1 - prism/src/explicit/MDPExplicit.java | 2 +- prism/src/explicit/Model.java | 2 +- prism/src/explicit/QuantAbstractRefine.java | 2 +- prism/src/explicit/modelviews/MDPView.java | 4 ++-- prism/src/mtbdd/PM_ExportMatrix.cc | 2 +- prism/src/sparse/PS_ExportMDP.cc | 2 +- prism/src/sparse/PS_ExportMatrix.cc | 2 +- 13 files changed, 8 insertions(+), 14 deletions(-) diff --git a/prism-tests/functionality/export/dot/cluster.sm.dot b/prism-tests/functionality/export/dot/cluster.sm.dot index 7941de13..be8b3a35 100644 --- a/prism-tests/functionality/export/dot/cluster.sm.dot +++ b/prism-tests/functionality/export/dot/cluster.sm.dot @@ -1,5 +1,4 @@ digraph R { -size="8,5" node [shape=box]; 0 -> 8 [ label="10" ]; 0 -> 10 [ label="10" ]; diff --git a/prism-tests/functionality/export/dot/cluster.sm.sta.dot b/prism-tests/functionality/export/dot/cluster.sm.sta.dot index fef7ea40..1a5ec1eb 100644 --- a/prism-tests/functionality/export/dot/cluster.sm.sta.dot +++ b/prism-tests/functionality/export/dot/cluster.sm.sta.dot @@ -1,5 +1,4 @@ digraph R { -size="8,5" node [shape=box]; 0 -> 8 [ label="10" ]; 0 -> 10 [ label="10" ]; diff --git a/prism-tests/functionality/export/dot/dice.pm.dot b/prism-tests/functionality/export/dot/dice.pm.dot index 3dd88ca0..82a99439 100644 --- a/prism-tests/functionality/export/dot/dice.pm.dot +++ b/prism-tests/functionality/export/dot/dice.pm.dot @@ -1,5 +1,4 @@ digraph P { -size="8,5" node [shape=box]; 0 -> 1 [ label="0.5" ]; 0 -> 2 [ label="0.5" ]; diff --git a/prism-tests/functionality/export/dot/dice.pm.sta.dot b/prism-tests/functionality/export/dot/dice.pm.sta.dot index ff05bdb0..b4316e94 100644 --- a/prism-tests/functionality/export/dot/dice.pm.sta.dot +++ b/prism-tests/functionality/export/dot/dice.pm.sta.dot @@ -1,5 +1,4 @@ digraph P { -size="8,5" node [shape=box]; 0 -> 1 [ label="0.5" ]; 0 -> 2 [ label="0.5" ]; diff --git a/prism-tests/functionality/export/dot/robot.prism.dot b/prism-tests/functionality/export/dot/robot.prism.dot index 68a4802d..a666344a 100644 --- a/prism-tests/functionality/export/dot/robot.prism.dot +++ b/prism-tests/functionality/export/dot/robot.prism.dot @@ -1,5 +1,4 @@ digraph S { -size="8,5" node [shape=box]; 0 -> n0_0 [ arrowhead=none,label="0:south" ]; n0_0 [ shape=point,width=0.1,height=0.1,label="" ]; diff --git a/prism-tests/functionality/export/dot/robot.prism.sta.dot b/prism-tests/functionality/export/dot/robot.prism.sta.dot index 50650fd4..b75060d5 100644 --- a/prism-tests/functionality/export/dot/robot.prism.sta.dot +++ b/prism-tests/functionality/export/dot/robot.prism.sta.dot @@ -1,5 +1,4 @@ digraph S { -size="8,5" node [shape=box]; 0 -> n0_0 [ arrowhead=none,label="0:south" ]; n0_0 [ shape=point,width=0.1,height=0.1,label="" ]; diff --git a/prism/src/explicit/MDPExplicit.java b/prism/src/explicit/MDPExplicit.java index faf32d01..8ec497da 100644 --- a/prism/src/explicit/MDPExplicit.java +++ b/prism/src/explicit/MDPExplicit.java @@ -160,7 +160,7 @@ public abstract class MDPExplicit extends ModelExplicit implements MDP String nij; Object action; String style; - out.print("digraph " + getModelType() + " {\nsize=\"8,5\"\nnode [shape=box];\n"); + out.print("digraph " + getModelType() + " {\nnode [shape=box];\n"); for (i = 0; i < numStates; i++) { if (mark != null && mark.get(i)) out.print(i + " [style=filled fillcolor=\"#cccccc\"]\n"); diff --git a/prism/src/explicit/Model.java b/prism/src/explicit/Model.java index e00a1cf1..48514ae2 100644 --- a/prism/src/explicit/Model.java +++ b/prism/src/explicit/Model.java @@ -370,7 +370,7 @@ public interface Model defaults.attributes().put("shape", "box"); // Header - out.print("digraph " + getModelType() + " {\nsize=\"8,5\"\nnode " + defaults.toString() + ";\n"); + out.print("digraph " + getModelType() + " {\nnode " + defaults.toString() + ";\n"); int i, numStates; for (i = 0, numStates = getNumStates(); i < numStates; i++) { // initialize diff --git a/prism/src/explicit/QuantAbstractRefine.java b/prism/src/explicit/QuantAbstractRefine.java index 509e0054..69ea1158 100644 --- a/prism/src/explicit/QuantAbstractRefine.java +++ b/prism/src/explicit/QuantAbstractRefine.java @@ -1267,7 +1267,7 @@ public abstract class QuantAbstractRefine extends PrismComponent try { FileWriter out = new FileWriter(filename); - out.write("digraph " + "STPG" + " {\nsize=\"8,5\"\nnode [shape=box];\n"); + out.write("digraph " + "STPG" + " {\nnode [shape=box];\n"); for (i = 0; i < stpg.getNumStates(); i++) { if (known.get(i)) out.write(i + " [label=\"" + i + " {" + lbSoln[i] + "}" + "\" style=filled fillcolor=\"#cccccc\""); diff --git a/prism/src/explicit/modelviews/MDPView.java b/prism/src/explicit/modelviews/MDPView.java index f88eaf9b..563006d2 100644 --- a/prism/src/explicit/modelviews/MDPView.java +++ b/prism/src/explicit/modelviews/MDPView.java @@ -275,7 +275,7 @@ public abstract class MDPView extends ModelView implements MDP, Cloneable @Override public void exportToDotFileWithStrat(final PrismLog out, final BitSet mark, final int[] strat) { - out.print("digraph " + getModelType() + " {\nsize=\"8,5\"\nnode [shape=box];\n"); + out.print("digraph " + getModelType() + " {\nnode [shape=box];\n"); for (int state = 0, numStates = getNumStates(); state < numStates; state++) { if (mark != null && mark.get(state)) out.print(state + " [style=filled fillcolor=\"#cccccc\"]\n"); @@ -348,4 +348,4 @@ public abstract class MDPView extends ModelView implements MDP, Cloneable } } } -} \ No newline at end of file +} diff --git a/prism/src/mtbdd/PM_ExportMatrix.cc b/prism/src/mtbdd/PM_ExportMatrix.cc index eb5b22b6..a39bc785 100644 --- a/prism/src/mtbdd/PM_ExportMatrix.cc +++ b/prism/src/mtbdd/PM_ExportMatrix.cc @@ -72,7 +72,7 @@ jstring fn // filename switch (export_type) { case EXPORT_PLAIN: export_string("%" PRId64 " %.0f\n", odd->eoff+odd->toff, DD_GetNumMinterms(ddman, matrix, num_rvars+num_cvars)); break; case EXPORT_MATLAB: export_string("%s = sparse(%" PRId64 ",%" PRId64 ");\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 = box];\n", export_name); break; + case EXPORT_DOT: case EXPORT_DOT_STATES: export_string("digraph %s {\nnode [shape = box];\n", export_name); break; } // print main part of file diff --git a/prism/src/sparse/PS_ExportMDP.cc b/prism/src/sparse/PS_ExportMDP.cc index 5f6852aa..99f370be 100644 --- a/prism/src/sparse/PS_ExportMDP.cc +++ b/prism/src/sparse/PS_ExportMDP.cc @@ -99,7 +99,7 @@ jstring fn // filename switch (export_type) { case EXPORT_PLAIN: export_string("%d %d %ld\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: case EXPORT_DOT_STATES: export_string("digraph %s {\nsize=\"8,5\"\nnode [shape=box];\n", export_name); break; + case EXPORT_DOT: case EXPORT_DOT_STATES: export_string("digraph %s {\nnode [shape=box];\n", export_name); break; case EXPORT_ROWS: export_string("%d %d %ld\n", n, nc, nnz); break; } diff --git a/prism/src/sparse/PS_ExportMatrix.cc b/prism/src/sparse/PS_ExportMatrix.cc index 07e3ee14..b392350f 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: case EXPORT_DOT_STATES: export_string("digraph %s {\nsize=\"8,5\"\nnode [shape=box];\n", export_name); break; + case EXPORT_DOT: case EXPORT_DOT_STATES: export_string("digraph %s {\nnode [shape=box];\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; }