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<explicit.graphviz.Decorator> 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

@@ -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
 	{

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<explicit.graphviz.Decorator> decorators)
 	{
 		Iterator<Map.Entry<Integer, Double>> iter = getTransitionsIterator(i);
 		while (iter.hasNext()) {
 			Map.Entry<Integer, Double> 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());
 		}
 	}
 

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<explicit.graphviz.Decorator> decorators)
 	{
 		for (Iterator<Integer> it = getSuccessorsIterator(s); it.hasNext(); ) {
 			Integer successor = it.next();
+
+			// we ignore decorators here
 			out.println(s + " -> " + successor + ";");
 		}
 	}

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<explicit.graphviz.Decorator> 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<Map.Entry<Integer, Double>> iter = getTransitionsIterator(i, j);
 			while (iter.hasNext()) {
 				Map.Entry<Integer, Double> 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(";");
 			}
 		}
 	}

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<explicit.graphviz.Decorator> 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<explicit.graphviz.Decorator>)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<explicit.graphviz.Decorator> decorators = new ArrayList<explicit.graphviz.Decorator>();
+		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<explicit.graphviz.Decorator> 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.
+	 * <br>
+	 * 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<explicit.graphviz.Decorator> decorators)
+	{
+		throw new UnsupportedOperationException();
+	}
 
 	/**
 	 * Export to a equivalent PRISM language model description.

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<State> 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;
 

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<explicit.graphviz.Decorator> 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;

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[])

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<explicit.graphviz.Decorator> 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
 	{