Add improved Dot export for LTSs, including action labels.

prism/src/explicit/LTS.java

@@ -27,8 +27,8 @@
 package explicit;
 
 import java.util.BitSet;
-import java.util.Iterator;
 
+import explicit.graphviz.Decorator;
 import prism.ModelType;
 import prism.PrismException;
 import prism.PrismLog;
@@ -53,12 +53,25 @@ public interface LTS extends NondetModel
 	}
 
 	@Override
-	default void exportTransitionsToDotFile(int s, PrismLog out, Iterable<explicit.graphviz.Decorator> decorators)
+	default void exportTransitionsToDotFile(int i, 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 + ";");
+		// Iterate through outgoing transitions (i.e. choices) for this state
+		int numChoices = getNumChoices(i);
+		for (int j = 0; j < numChoices; j++) {
+			Object action = getAction(i, j);
+			// Print a new dot file line for the arrow for this transition
+			out.print(i + " -> " + getSuccessor(i, j));
+			// Annotate this with the choice index/action 
+			explicit.graphviz.Decoration d = new explicit.graphviz.Decoration();
+			d.setLabel(j + (action != null ? ":" + action : ""));
+			// Apply any other decorators requested
+			if (decorators != null) {
+				for (Decorator decorator : decorators) {
+					d = decorator.decorateTransition(i, j, d);
+				}
+			}
+			// Append to the dot file line
+			out.println(" " + d.toString() + ";");
 		}
 	}