From 13c3e00a9f829110944a292970f5031ca01f0a1b Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Fri, 16 Oct 2020 15:13:09 +0100
Subject: [PATCH] Tidy and comment explicit engine Dot export code.

---
 prism/src/explicit/DTMC.java            |  9 ++++---
 prism/src/explicit/MDP.java             | 35 ++++++++++++-------------
 prism/src/explicit/STPGAbstrSimple.java | 15 +++++------
 3 files changed, 29 insertions(+), 30 deletions(-)

diff --git a/prism/src/explicit/DTMC.java b/prism/src/explicit/DTMC.java
index c2d588e2..822ad473 100644
--- a/prism/src/explicit/DTMC.java
+++ b/prism/src/explicit/DTMC.java
@@ -87,20 +87,23 @@ public interface DTMC extends Model
 	@Override
 	default void exportTransitionsToDotFile(int i, PrismLog out, Iterable<explicit.graphviz.Decorator> decorators)
 	{
+		// Iterate through outgoing transitions for this state
 		Iterator<Map.Entry<Integer, Double>> iter = getTransitionsIterator(i);
 		while (iter.hasNext()) {
 			Map.Entry<Integer, Double> e = iter.next();
+			// Print a new dot file line for the arrow for this transition
 			out.print(i + " -> " + e.getKey());
-
+			// Annotate this arrow with the probability 
 			explicit.graphviz.Decoration d = new explicit.graphviz.Decoration();
 			d.setLabel(e.getValue().toString());
+			// Apply any other decorators requested
 			if (decorators != null) {
 				for (Decorator decorator : decorators) {
 					d = decorator.decorateProbability(i, e.getKey(), e.getValue(), d);
 				}
 			}
-
-			out.println(d.toString());
+			// Append to the dot file line for this transition
+			out.println(" " + d.toString() + ";");
 		}
 	}
 
diff --git a/prism/src/explicit/MDP.java b/prism/src/explicit/MDP.java
index c1c3612a..8c6e69a3 100644
--- a/prism/src/explicit/MDP.java
+++ b/prism/src/explicit/MDP.java
@@ -96,45 +96,44 @@ public interface MDP extends MDPGeneric<Double>
 	@Override
 	default void exportTransitionsToDotFile(int i, PrismLog out, Iterable<explicit.graphviz.Decorator> decorators)
 	{
-		int j, numChoices;
-		String nij;
-		Object action;
-		numChoices = getNumChoices(i);
-		for (j = 0; j < numChoices; j++) {
-			action = getAction(i, j);
-			nij = "n" + i + "_" + j;
+		// Iterate through outgoing 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 initial line fragment for this choice
+			String nij = "n" + i + "_" + j;
 			out.print(i + " -> " + nij + " ");
-
+			// Annotate this with the choice index/action 
 			explicit.graphviz.Decoration d = new explicit.graphviz.Decoration();
 			d.attributes().put("arrowhead", "none");
 			d.setLabel(j + (action != null ? ":" + action : ""));
-
+			// Apply any other decorators requested
 			if (decorators != null) {
 				for (Decorator decorator : decorators) {
 					d = decorator.decorateTransition(i, j, d);
 				}
 			}
-			out.print(d);
-			out.println(";");
-
+			// Append to the dot file line
+			out.println(" " + d.toString() + ";");
+			// Print a new dot file line for the point where this choice branches
 			out.print(nij + " [ shape=point,width=0.1,height=0.1,label=\"\" ];\n");
-
+			// Iterate through outgoing transitions for this choice
 			Iterator<Map.Entry<Integer, Double>> iter = getTransitionsIterator(i, j);
 			while (iter.hasNext()) {
 				Map.Entry<Integer, Double> e = iter.next();
+				// Print a new dot file line for the arrow for this transition
 				out.print(nij + " -> " + e.getKey() + " ");
-
+				// Annotate this arrow with the probability 
 				d = new explicit.graphviz.Decoration();
 				d.setLabel(e.getValue().toString());
-
+				// Apply any other decorators requested
 				if (decorators != null) {
 					for (Decorator decorator : decorators) {
 						d = decorator.decorateProbability(i, e.getKey(), j, e.getValue(), d);
 					}
 				}
-
-				out.print(d);
-				out.println(";");
+				// Append to the dot file line for this transition
+				out.println(" " + d.toString() + ";");
 			}
 		}
 	}
diff --git a/prism/src/explicit/STPGAbstrSimple.java b/prism/src/explicit/STPGAbstrSimple.java
index 937d058a..030405c0 100644
--- a/prism/src/explicit/STPGAbstrSimple.java
+++ b/prism/src/explicit/STPGAbstrSimple.java
@@ -359,21 +359,18 @@ public class STPGAbstrSimple extends ModelExplicit implements STPG, NondetModelS
 	@Override
 	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
-
+		// Custom dot format for game abstractions
+		// We ignore decorators for the moment
+		int j = -1;
 		for (DistributionSet distrs : trans.get(i)) {
 			j++;
-			nij = "n" + i + "_" + j;
+			String 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;
+			int k = -1;
 			for (Distribution distr : distrs) {
 				k++;
-				nijk = "n" + i + "_" + j + "_" + k;
+				String nijk = "n" + i + "_" + j + "_" + k;
 				out.print(nij + " -> " + nijk + " [ arrowhead=none,label=\"" + k + "\" ];\n");
 				out.print(nijk + " [ shape=point,label=\"\" ];\n");
 				for (Map.Entry<Integer, Double> e : distr) {