From 881a5718703a863d1ac49031253c09230dc9b863 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 21 Jul 2017 14:00:29 +0000 Subject: [PATCH] explicit DOT export: support decorators This commit refactors the exportToDotFile infrastructure of the explicit engine to allow the flexible decoration of the nodes and edges in the DOT file, e.g., for annotating rewards, marking certain states, etc. We provide default implementations in explicit.Model for most methods, only exportTransitionsToDotFile needs to be provided in derived classes to allow DOT export. Note that the abstract method in ModelExplicit abstract void exportTransitionsToDotFile(int i, PrismLog out); has been removed, which will lead to errors in derived classes where implementations of this method have been marked with the @Override annotation. To fix this, simply replace the signature of your implementation of void exportTransitionsToDotFile(int i, PrismLog out); by void exportTransitionsToDotFile(int i, PrismLog out, Iterable decorators) (as defined in explicit.Model). You can simply ignore the decorators parameter at first. Later on, if you want to support decoration, have a look at the implementations of this method in DTMCExplicit and MDPExplicit for the proper handling. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12115 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/automata/LTSFromDA.java | 6 -- prism/src/explicit/DTMCExplicit.java | 16 +++- prism/src/explicit/LTSExplicit.java | 5 +- prism/src/explicit/MDPExplicit.java | 36 ++++++-- prism/src/explicit/Model.java | 104 ++++++++++++++++++++++-- prism/src/explicit/ModelExplicit.java | 59 -------------- prism/src/explicit/STPGAbstrSimple.java | 5 +- prism/src/explicit/SubNondetModel.java | 29 ------- prism/src/param/ParamModel.java | 44 ++++++++-- 9 files changed, 185 insertions(+), 119 deletions(-) diff --git a/prism/src/automata/LTSFromDA.java b/prism/src/automata/LTSFromDA.java index 58cca064..0a62288b 100644 --- a/prism/src/automata/LTSFromDA.java +++ b/prism/src/automata/LTSFromDA.java @@ -134,12 +134,6 @@ public class LTSFromDA extends ModelExplicit implements LTS throw new RuntimeException("Not implemented yet"); } - @Override - protected void exportTransitionsToDotFile(int i, PrismLog out) - { - throw new RuntimeException("Not implemented yet"); - } - @Override public void exportToPrismLanguage(String filename) throws PrismException { diff --git a/prism/src/explicit/DTMCExplicit.java b/prism/src/explicit/DTMCExplicit.java index d5d46d15..79c8fed2 100644 --- a/prism/src/explicit/DTMCExplicit.java +++ b/prism/src/explicit/DTMCExplicit.java @@ -34,6 +34,7 @@ import java.util.Map; import java.util.TreeMap; import java.util.Map.Entry; +import explicit.graphviz.Decorator; import prism.ModelType; import prism.Pair; import prism.PrismException; @@ -82,13 +83,22 @@ public abstract class DTMCExplicit extends ModelExplicit implements DTMC } @Override - public void exportTransitionsToDotFile(int i, PrismLog out) + public void exportTransitionsToDotFile(int i, PrismLog out, Iterable decorators) { 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(i + " -> " + e.getKey()); + + explicit.graphviz.Decoration d = new explicit.graphviz.Decoration(); + d.setLabel(e.getValue().toString()); + if (decorators != null) { + for (Decorator decorator : decorators) { + d = decorator.decorateProbability(i, e.getKey(), e.getValue(), d); + } + } + + out.println(d.toString()); } } diff --git a/prism/src/explicit/LTSExplicit.java b/prism/src/explicit/LTSExplicit.java index 7e006a43..8e997dea 100644 --- a/prism/src/explicit/LTSExplicit.java +++ b/prism/src/explicit/LTSExplicit.java @@ -33,6 +33,7 @@ import java.util.Collections; import java.util.Iterator; import java.util.LinkedHashSet; +import explicit.graphviz.Decorator; import prism.ModelType; import prism.PrismException; import prism.PrismLog; @@ -192,10 +193,12 @@ public class LTSExplicit extends ModelExplicit implements LTS } @Override - protected void exportTransitionsToDotFile(int s, PrismLog out) + public void exportTransitionsToDotFile(int s, PrismLog out, Iterable decorators) { for (Iterator it = getSuccessorsIterator(s); it.hasNext(); ) { Integer successor = it.next(); + + // we ignore decorators here out.println(s + " -> " + successor + ";"); } } diff --git a/prism/src/explicit/MDPExplicit.java b/prism/src/explicit/MDPExplicit.java index ce493746..e1ec641b 100644 --- a/prism/src/explicit/MDPExplicit.java +++ b/prism/src/explicit/MDPExplicit.java @@ -42,6 +42,7 @@ import prism.PrismException; import prism.PrismLog; import prism.PrismUtils; import strat.MDStrategy; +import explicit.graphviz.Decorator; import explicit.rewards.MDPRewards; /** @@ -110,7 +111,7 @@ public abstract class MDPExplicit extends ModelExplicit implements MDP } @Override - public void exportTransitionsToDotFile(int i, PrismLog out) + public void exportTransitionsToDotFile(int i, PrismLog out, Iterable decorators) { int j, numChoices; String nij; @@ -119,15 +120,38 @@ public abstract class MDPExplicit extends ModelExplicit implements MDP 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(i + " -> " + nij + " "); + + explicit.graphviz.Decoration d = new explicit.graphviz.Decoration(); + d.attributes().put("arrowhead", "none"); + d.setLabel(j + (action != null ? ":" + action : "")); + + if (decorators != null) { + for (Decorator decorator : decorators) { + d = decorator.decorateTransition(i, j, d); + } + } + out.print(d); + out.println(";"); + 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(nij + " -> " + e.getKey() + " "); + + d = new explicit.graphviz.Decoration(); + d.setLabel(e.getValue().toString()); + + if (decorators != null) { + for (Decorator decorator : decorators) { + d = decorator.decorateProbability(i, e.getKey(), j, e.getValue(), d); + } + } + + out.print(d); + out.println(";"); } } } diff --git a/prism/src/explicit/Model.java b/prism/src/explicit/Model.java index 3450d59c..e00a1cf1 100644 --- a/prism/src/explicit/Model.java +++ b/prism/src/explicit/Model.java @@ -27,17 +27,21 @@ package explicit; import java.io.File; +import java.util.ArrayList; import java.util.BitSet; +import java.util.Collections; import java.util.Iterator; import java.util.List; import java.util.Set; import java.util.function.IntPredicate; +import explicit.graphviz.Decorator; import parser.State; import parser.Values; import parser.VarList; import prism.ModelType; import prism.PrismException; +import prism.PrismFileLog; import prism.PrismLog; /** @@ -287,27 +291,56 @@ public interface Model * Export to a dot file. * @param filename Name of file to export to */ - public void exportToDotFile(String filename) throws PrismException; + default void exportToDotFile(String filename) throws PrismException + { + try (PrismFileLog log = PrismFileLog.create(filename)) { + exportToDotFile(log); + } + } /** * Export to a dot file, highlighting states in 'mark'. * @param filename Name of file to export to * @param mark States to highlight (ignored if null) */ - public void exportToDotFile(String filename, BitSet mark) throws PrismException; + default void exportToDotFile(String filename, BitSet mark) throws PrismException + { + try (PrismFileLog log = PrismFileLog.create(filename)) { + exportToDotFile(log, mark); + } + } + + /** + * Export to a dot file, decorating states and transitions with the provided decorators + * @param filename Name of the file to export to + */ + default void exportToDotFile(String filename, Iterable decorators) throws PrismException + { + try (PrismFileLog log = PrismFileLog.create(filename)) { + exportToDotFile(log, decorators); + } + } /** * Export to a dot file. * @param out PrismLog to export to */ - public void exportToDotFile(PrismLog out); + default void exportToDotFile(PrismLog out) + { + exportToDotFile(out, (Iterable)null); + } /** * Export to a dot file, highlighting states in 'mark'. * @param out PrismLog to export to * @param mark States to highlight (ignored if null) */ - public void exportToDotFile(PrismLog out, BitSet mark); + default void exportToDotFile(PrismLog out, BitSet mark) { + if (mark == null) { + exportToDotFile(out); + } + exportToDotFile(out, Collections.singleton(new explicit.graphviz.MarkStateSetDecorator(mark))); + } /** * Export to a dot file, highlighting states in 'mark'. @@ -315,7 +348,68 @@ public interface Model * @param mark States to highlight (ignored if null) * @param showStates Show state info on nodes? */ - public void exportToDotFile(PrismLog out, BitSet mark, boolean showStates); + default void exportToDotFile(PrismLog out, BitSet mark, boolean showStates) + { + ArrayList decorators = new ArrayList(); + if (showStates) { + decorators.add(new explicit.graphviz.ShowStatesDecorator(getStatesList())); + } + if (mark != null) { + decorators.add(new explicit.graphviz.MarkStateSetDecorator(mark)); + } + exportToDotFile(out, decorators); + } + + /** + * Export to a dot file, decorating states and transitions with the provided decorators + * @param out PrismLog to export to + */ + default void exportToDotFile(PrismLog out, Iterable decorators) + { + explicit.graphviz.Decoration defaults = new explicit.graphviz.Decoration(); + defaults.attributes().put("shape", "box"); + + // Header + out.print("digraph " + getModelType() + " {\nsize=\"8,5\"\nnode " + defaults.toString() + ";\n"); + int i, numStates; + for (i = 0, numStates = getNumStates(); i < numStates; i++) { + // initialize + explicit.graphviz.Decoration d = new explicit.graphviz.Decoration(defaults); + d.setLabel(Integer.toString(i)); + + // run any decorators + if (decorators != null) { + for (Decorator decorator : decorators) { + d = decorator.decorateState(i, d); + } + } + + String decoration = d.toString(); + out.println(i + " " + decoration + ";"); + + // Transitions for state i + exportTransitionsToDotFile(i, out, decorators); + } + + // Footer + out.print("}\n"); + } + + /** + * Export the transitions from state {@code i} in Dot format to {@code out}, + * decorating using the given decorators. + *
+ * The default implementation throws an UnsupportedOperationException, + * so this method should be overloaded. + * + * @param i State index + * @param out PrismLog for output + * @param decorators the decorators (may be {@code null}) + */ + default void exportTransitionsToDotFile(int i, PrismLog out, Iterable decorators) + { + throw new UnsupportedOperationException(); + } /** * Export to a equivalent PRISM language model description. diff --git a/prism/src/explicit/ModelExplicit.java b/prism/src/explicit/ModelExplicit.java index 5f354aa6..c042635d 100644 --- a/prism/src/explicit/ModelExplicit.java +++ b/prism/src/explicit/ModelExplicit.java @@ -389,65 +389,6 @@ public abstract class ModelExplicit implements Model @Override public abstract void exportToPrismExplicitTra(PrismLog out); - @Override - public void exportToDotFile(String filename) throws PrismException - { - exportToDotFile(filename, null); - } - - @Override - public void exportToDotFile(String filename, BitSet mark) throws PrismException - { - try (PrismFileLog log = PrismFileLog.create(filename)) { - exportToDotFile(log, mark); - } - } - - @Override - public void exportToDotFile(PrismLog out) - { - exportToDotFile(out, null, false); - } - - @Override - public void exportToDotFile(PrismLog out, BitSet mark) - { - exportToDotFile(out, mark, false); - } - - @Override - public void exportToDotFile(PrismLog out, BitSet mark, boolean showStates) - { - 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); - } - // Append state info (if required) - if (showStates) { - List states = getStatesList(); - if (states != null) { - for (i = 0; i < numStates; i++) { - out.print(i + " [label=\"" + i + "\\n" + states.get(i) + "\"]\n"); - } - } - } - // 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 b8d9c0eb..02a23c96 100644 --- a/prism/src/explicit/STPGAbstrSimple.java +++ b/prism/src/explicit/STPGAbstrSimple.java @@ -395,11 +395,14 @@ public class STPGAbstrSimple extends ModelExplicit implements STPG, NondetModelS } @Override - protected void exportTransitionsToDotFile(int i, PrismLog out) + public void exportTransitionsToDotFile(int i, PrismLog out, Iterable decorators) { int j, k; String nij, nijk; j = -1; + + // we ignore decorators for the moment + for (DistributionSet distrs : trans.get(i)) { j++; nij = "n" + i + "_" + j; diff --git a/prism/src/explicit/SubNondetModel.java b/prism/src/explicit/SubNondetModel.java index 929248b4..1e2c1bc1 100644 --- a/prism/src/explicit/SubNondetModel.java +++ b/prism/src/explicit/SubNondetModel.java @@ -253,35 +253,6 @@ public class SubNondetModel implements NondetModel throw new UnsupportedOperationException(); } - @Override - public void exportToDotFile(String filename) throws PrismException - { - throw new UnsupportedOperationException(); - } - - @Override - public void exportToDotFile(String filename, BitSet mark) throws PrismException - { - throw new UnsupportedOperationException(); - } - - @Override - public void exportToDotFile(PrismLog out) - { - throw new UnsupportedOperationException(); - } - - @Override - public void exportToDotFile(PrismLog out, BitSet mark) - { - throw new UnsupportedOperationException(); - } - - @Override - public void exportToDotFile(PrismLog out, BitSet mark, boolean showStates) - { - throw new UnsupportedOperationException(); - } @Override public void exportToDotFileWithStrat(PrismLog out, BitSet mark, int strat[]) diff --git a/prism/src/param/ParamModel.java b/prism/src/param/ParamModel.java index 56df56ac..e3f10709 100644 --- a/prism/src/param/ParamModel.java +++ b/prism/src/param/ParamModel.java @@ -30,6 +30,7 @@ import java.io.File; import java.util.BitSet; import java.util.Iterator; import java.util.LinkedList; +import java.util.Map; import java.util.Map.Entry; import java.util.TreeSet; @@ -39,6 +40,7 @@ import prism.PrismException; import prism.PrismLog; import explicit.ModelExplicit; import explicit.SuccessorsIterator; +import explicit.graphviz.Decorator; /** * Represents a parametric Markov model. @@ -227,7 +229,7 @@ public final class ParamModel extends ModelExplicit @Override - protected void exportTransitionsToDotFile(int i, PrismLog out) + public void exportTransitionsToDotFile(int i, PrismLog out, Iterable decorators) { int numChoices = getNumChoices(i); for (int j = 0; j < numChoices; j++) { @@ -235,8 +237,19 @@ public final class ParamModel extends ModelExplicit String nij = null; if (modelType.nondeterministic()) { nij = "n" + i + "_" + j; - out.print(i + " -> " + nij + " [ arrowhead=none,label=\"" + j); - out.print("\" ];\n"); + out.print(i + " -> " + nij + " "); + explicit.graphviz.Decoration d = new explicit.graphviz.Decoration(); + d.attributes().put("arrowhead", "none"); + d.setLabel(Integer.toString(j)); + + if (decorators != null) { + for (Decorator decorator : decorators) { + d = decorator.decorateTransition(i, j, d); + } + } + out.print(d); + out.println(";"); + out.print(nij + " [ shape=point,width=0.1,height=0.1,label=\"\" ];\n"); } @@ -252,19 +265,32 @@ public final class ParamModel extends ModelExplicit out.print(nij + " -> " + e.getKey() + " "); } - String value; + Object value; if (e.getValue().isConstant()) { - value = e.getValue().asBigRational().toString(); + value = e.getValue().asBigRational(); } else { - value = e.getValue().toString(); + value = e.getValue(); } - - out.print("[ label=\"" + value + "\" ];\n"); + explicit.graphviz.Decoration d = new explicit.graphviz.Decoration(); + d.setLabel(value.toString()); + + if (decorators != null) { + for (Decorator decorator : decorators) { + if (!modelType.nondeterministic()) { + d = decorator.decorateProbability(i, e.getKey(), value, d); + } else { + d = decorator.decorateProbability(i, e.getKey(), j, value, d); + } + } + } + + out.print(d); + out.println(";"); } } } - + @Override public void exportToPrismLanguage(String filename) throws PrismException {