From d3a267a2dc4e332919e992881e6bc4c4d7ec3052 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 3 Jun 2014 09:28:10 +0000 Subject: [PATCH] Refactor exportToDot methods for explicit model classes - subclasses just need to export their transitions, so it is easier to add more functionality regarding state info. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8389 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/DTMCExplicit.java | 19 ++++--------- prism/src/explicit/MDPExplicit.java | 36 ++++++++++------------- prism/src/explicit/ModelExplicit.java | 23 ++++++++++++++- prism/src/explicit/STPGAbstrSimple.java | 38 +++++++++++-------------- prism/src/param/ParamModel.java | 6 ++++ 5 files changed, 65 insertions(+), 57 deletions(-) diff --git a/prism/src/explicit/DTMCExplicit.java b/prism/src/explicit/DTMCExplicit.java index 5ecce327..b11e70c4 100644 --- a/prism/src/explicit/DTMCExplicit.java +++ b/prism/src/explicit/DTMCExplicit.java @@ -96,21 +96,14 @@ public abstract class DTMCExplicit extends ModelExplicit implements DTMC } @Override - public void exportToDotFile(PrismLog out, BitSet mark) + public void exportTransitionsToDotFile(int i, PrismLog out) { - int i; - out.print("digraph " + getModelType() + " {\nsize=\"8,5\"\nnode [shape=box];\n"); - for (i = 0; i < numStates; i++) { - if (mark != null && mark.get(i)) - out.print(i + " [style=filled fillcolor=\"#cccccc\"]\n"); - Iterator> iter = getTransitionsIterator(i); - while (iter.hasNext()) { - Map.Entry e = iter.next(); - out.print(i + " -> " + e.getKey() + " [ label=\""); - out.print(e.getValue() + "\" ];\n"); - } + Iterator> iter = getTransitionsIterator(i); + while (iter.hasNext()) { + Map.Entry e = iter.next(); + out.print(i + " -> " + e.getKey() + " [ label=\""); + out.print(e.getValue() + "\" ];\n"); } - out.print("}\n"); } @Override diff --git a/prism/src/explicit/MDPExplicit.java b/prism/src/explicit/MDPExplicit.java index d0ab45eb..27ea93f2 100644 --- a/prism/src/explicit/MDPExplicit.java +++ b/prism/src/explicit/MDPExplicit.java @@ -108,32 +108,26 @@ public abstract class MDPExplicit extends ModelExplicit implements MDP } @Override - public void exportToDotFile(PrismLog out, BitSet mark) + public void exportTransitionsToDotFile(int i, PrismLog out) { - int i, j, numChoices; + int j, numChoices; String nij; Object action; - out.print("digraph " + getModelType() + " {\nsize=\"8,5\"\nnode [shape=box];\n"); - for (i = 0; i < numStates; i++) { - if (mark != null && mark.get(i)) - out.print(i + " [style=filled fillcolor=\"#cccccc\"]\n"); - numChoices = getNumChoices(i); - for (j = 0; j < numChoices; j++) { - action = getAction(i, j); - nij = "n" + i + "_" + j; - out.print(i + " -> " + nij + " [ arrowhead=none,label=\"" + j); - if (action != null) - out.print(":" + action); - out.print("\" ];\n"); - out.print(nij + " [ shape=point,width=0.1,height=0.1,label=\"\" ];\n"); - Iterator> iter = getTransitionsIterator(i, j); - while (iter.hasNext()) { - Map.Entry e = iter.next(); - out.print(nij + " -> " + e.getKey() + " [ label=\"" + e.getValue() + "\" ];\n"); - } + numChoices = getNumChoices(i); + for (j = 0; j < numChoices; j++) { + action = getAction(i, j); + nij = "n" + i + "_" + j; + out.print(i + " -> " + nij + " [ arrowhead=none,label=\"" + j); + if (action != null) + out.print(":" + action); + out.print("\" ];\n"); + out.print(nij + " [ shape=point,width=0.1,height=0.1,label=\"\" ];\n"); + Iterator> iter = getTransitionsIterator(i, j); + while (iter.hasNext()) { + Map.Entry e = iter.next(); + out.print(nij + " -> " + e.getKey() + " [ label=\"" + e.getValue() + "\" ];\n"); } } - out.print("}\n"); } @Override diff --git a/prism/src/explicit/ModelExplicit.java b/prism/src/explicit/ModelExplicit.java index 3aaac05d..e942d8f5 100644 --- a/prism/src/explicit/ModelExplicit.java +++ b/prism/src/explicit/ModelExplicit.java @@ -319,8 +319,29 @@ public abstract class ModelExplicit implements Model } @Override - public abstract void exportToDotFile(PrismLog out, BitSet mark); + public void exportToDotFile(PrismLog out, BitSet mark) + { + int i; + // Header + out.print("digraph " + getModelType() + " {\nsize=\"8,5\"\nnode [shape=box];\n"); + for (i = 0; i < numStates; i++) { + // Style for each state + if (mark != null && mark.get(i)) + out.print(i + " [style=filled fillcolor=\"#cccccc\"]\n"); + // Transitions for state i + exportTransitionsToDotFile(i, out); + } + // Footer + out.print("}\n"); + } + /** + * Export the transitions from state {@code i} in Dot format to {@code out}. + * @param i State index + * @param out PrismLog for output + */ + protected abstract void exportTransitionsToDotFile(int i, PrismLog out); + @Override public abstract void exportToPrismLanguage(String filename) throws PrismException; diff --git a/prism/src/explicit/STPGAbstrSimple.java b/prism/src/explicit/STPGAbstrSimple.java index 5752ab8d..6e1e6c6c 100644 --- a/prism/src/explicit/STPGAbstrSimple.java +++ b/prism/src/explicit/STPGAbstrSimple.java @@ -394,33 +394,27 @@ public class STPGAbstrSimple extends ModelExplicit implements STPG, NondetModelS } @Override - public void exportToDotFile(PrismLog out, BitSet mark) + protected void exportTransitionsToDotFile(int i, PrismLog out) { - int i, j, k; + int j, k; String nij, nijk; - out.print("digraph " + getModelType() + " {\nsize=\"8,5\"\nnode [shape=box];\n"); - for (i = 0; i < numStates; i++) { - if (mark != null && mark.get(i)) - out.print(i + " [style=filled fillcolor=\"#cccccc\"]\n"); - j = -1; - for (DistributionSet distrs : trans.get(i)) { - j++; - nij = "n" + i + "_" + j; - out.print(i + " -> " + nij + " [ arrowhead=none,label=\"" + j + "\" ];\n"); - out.print(nij + " [ shape=circle,width=0.1,height=0.1,label=\"\" ];\n"); - k = -1; - for (Distribution distr : distrs) { - k++; - nijk = "n" + i + "_" + j + "_" + k; - out.print(nij + " -> " + nijk + " [ arrowhead=none,label=\"" + k + "\" ];\n"); - out.print(nijk + " [ shape=point,label=\"\" ];\n"); - for (Map.Entry e : distr) { - out.print(nijk + " -> " + e.getKey() + " [ label=\"" + e.getValue() + "\" ];\n"); - } + j = -1; + for (DistributionSet distrs : trans.get(i)) { + j++; + nij = "n" + i + "_" + j; + out.print(i + " -> " + nij + " [ arrowhead=none,label=\"" + j + "\" ];\n"); + out.print(nij + " [ shape=circle,width=0.1,height=0.1,label=\"\" ];\n"); + k = -1; + for (Distribution distr : distrs) { + k++; + nijk = "n" + i + "_" + j + "_" + k; + out.print(nij + " -> " + nijk + " [ arrowhead=none,label=\"" + k + "\" ];\n"); + out.print(nijk + " [ shape=point,label=\"\" ];\n"); + for (Map.Entry e : distr) { + out.print(nijk + " -> " + e.getKey() + " [ label=\"" + e.getValue() + "\" ];\n"); } } } - out.print("}\n"); } @Override diff --git a/prism/src/param/ParamModel.java b/prism/src/param/ParamModel.java index 5a9c7617..2e9363ce 100644 --- a/prism/src/param/ParamModel.java +++ b/prism/src/param/ParamModel.java @@ -207,6 +207,12 @@ final class ParamModel extends ModelExplicit throw new UnsupportedOperationException(); } + @Override + protected void exportTransitionsToDotFile(int i, PrismLog out) + { + throw new UnsupportedOperationException(); + } + @Override public void exportToPrismLanguage(String filename) throws PrismException {