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 {