diff --git a/prism/src/automata/finite/DeterministicFiniteAutomaton.java b/prism/src/automata/finite/DeterministicFiniteAutomaton.java
index 06de5312..0ffc27ea 100644
--- a/prism/src/automata/finite/DeterministicFiniteAutomaton.java
+++ b/prism/src/automata/finite/DeterministicFiniteAutomaton.java
@@ -172,39 +172,4 @@ public class DeterministicFiniteAutomaton<Symbol> extends FiniteAutomaton<Symbol
 			}
 		}
 	}
-	
-	/**
-	 * Generate a representation in GraphViz's dot format.
-	 * States are black, red when accepting, blue when initial and violet when both.
-	 * @return
-	 */	
-	public String toDot() {
-		StringBuffer result = new StringBuffer();
-		result.append("digraph G {\n");
-		
-		for(State state : states) {
-    		String color = "black";
-    		
-    		if (isAcceptingState(state)) { color = "red"; }
-    		if (isInitialState(state)) { color = "blue"; }
-    		if (isAcceptingState(state) && isInitialState(state)) { color = "violet"; }
-    		
-    		result.append(state
-    				+ "[shape=box, color=" + color + ","
-    				+ " label=" + state + "]\n");
-		}
-		
-		for(SingleEdge<Symbol> edge : edges) {
-			String sourceLabel = edge.getSource().toString();
-			String symLabel = "\"" + edge.getLabel() + "\"";
-			State sink = edge.getSink();
-			String sinkLabel = "\"" + sink + "\"";
-			result.append(sourceLabel
-					+ " -> " + sinkLabel
-					+ "[label=" + symLabel + "];\n");
-		}
-		
-		result.append("}");
-		return result.toString();
-	}
 }
diff --git a/prism/src/automata/finite/Edge.java b/prism/src/automata/finite/Edge.java
index d6b44edb..fc93963c 100644
--- a/prism/src/automata/finite/Edge.java
+++ b/prism/src/automata/finite/Edge.java
@@ -1,5 +1,7 @@
 package automata.finite;
 
+import java.util.Set;
+
 public abstract class Edge<Symbol> {
 	protected State source; 
 	protected EdgeLabel<Symbol> label;
@@ -8,6 +10,8 @@ public abstract class Edge<Symbol> {
 		return source;
 	}
 	
+	public abstract Set<State> getSinks();
+	
 	public EdgeLabel<Symbol> getLabel() {
 		return label;
 	}
diff --git a/prism/src/automata/finite/FiniteAutomaton.java b/prism/src/automata/finite/FiniteAutomaton.java
index 7ef587d4..6fcbd5ed 100644
--- a/prism/src/automata/finite/FiniteAutomaton.java
+++ b/prism/src/automata/finite/FiniteAutomaton.java
@@ -459,4 +459,41 @@ public abstract class FiniteAutomaton<Symbol, E extends Edge<Symbol>> implements
 		
 		return result.toString();
 	}
+	
+	/**
+	 * Generate a representation in GraphViz's dot format.
+	 * States are black, red when accepting, blue when initial and violet when both.
+	 * @return
+	 */	
+	public String toDot() {
+		StringBuffer result = new StringBuffer();
+		result.append("digraph G {\n");
+		
+		for(State state : states) {
+    		String color = "black";
+    		String stateLabel = "\"" + state + "\"";
+    		
+    		if (isAcceptingState(state)) { color = "red"; }
+    		if (isInitialState(state)) { color = "blue"; }
+    		if (isAcceptingState(state) && isInitialState(state)) { color = "violet"; }
+    		
+    		result.append(stateLabel
+    				+ "[shape=box, color=" + color + ","
+    				+ " label=" + stateLabel + "]\n");
+		}
+		
+		for(Edge<Symbol> edge : edges) {
+			String sourceLabel = "\"" + edge.getSource() + "\"";
+			String symLabel = "\"" + edge.getLabel() + "\"";
+			for(State sink : edge.getSinks()) {
+				String sinkLabel = "\"" + sink + "\"";
+				result.append(sourceLabel
+						+ " -> " + sinkLabel
+						+ "[label=" + symLabel + "];\n");
+			}
+		}
+		
+		result.append("}");
+		return result.toString();
+	}
 }
diff --git a/prism/src/automata/finite/MultiEdge.java b/prism/src/automata/finite/MultiEdge.java
index 0e52d0b1..3b9469d4 100644
--- a/prism/src/automata/finite/MultiEdge.java
+++ b/prism/src/automata/finite/MultiEdge.java
@@ -12,6 +12,7 @@ public class MultiEdge<Symbol> extends Edge<Symbol> {
 		this.sinks = sinks;
 	}
 
+	@Override
 	public HashSet<State> getSinks() {
 		return sinks;
 	}
diff --git a/prism/src/automata/finite/NondeterministicFiniteAutomaton.java b/prism/src/automata/finite/NondeterministicFiniteAutomaton.java
index 15b5e89b..e3bdbd92 100644
--- a/prism/src/automata/finite/NondeterministicFiniteAutomaton.java
+++ b/prism/src/automata/finite/NondeterministicFiniteAutomaton.java
@@ -443,41 +443,4 @@ public class NondeterministicFiniteAutomaton<Symbol> extends FiniteAutomaton<Sym
 		
 		return dfa;
 	};
-	
-	
-	/**
-	 * Generate a representation in GraphViz's dot format.
-	 * States are black, red when accepting, blue when initial and violet when both.
-	 * @return
-	 */	
-	public String toDot() {
-		StringBuffer result = new StringBuffer();
-		result.append("digraph G {\n");
-		
-		for(State state : states) {
-    		String color = "black";
-    		
-    		if (isAcceptingState(state)) { color = "red"; }
-    		if (isInitialState(state)) { color = "blue"; }
-    		if (isAcceptingState(state) && isInitialState(state)) { color = "violet"; }
-    		
-    		result.append(state
-    				+ "[shape=box, color=" + color + ","
-    				+ " label=" + state + "]\n");
-		}
-		
-		for(MultiEdge<Symbol> edge : edges) {
-			String sourceLabel = edge.getSource().toString();
-			String symLabel = "\"" + edge.getLabel() + "\"";
-			for(State sink : edge.getSinks()) {
-				String sinkLabel = "\"" + sink + "\"";
-				result.append(sourceLabel
-						+ " -> " + sinkLabel
-						+ "[label=" + symLabel + "];\n");
-			}
-		}
-		
-		result.append("}");
-		return result.toString();
-	}
 }
diff --git a/prism/src/automata/finite/SingleEdge.java b/prism/src/automata/finite/SingleEdge.java
index b3da608a..7e3b9b62 100644
--- a/prism/src/automata/finite/SingleEdge.java
+++ b/prism/src/automata/finite/SingleEdge.java
@@ -1,5 +1,7 @@
 package automata.finite;
 
+import java.util.HashSet;
+
 public class SingleEdge<Symbol> extends Edge<Symbol> {
 	private State sink;
 	
@@ -14,6 +16,13 @@ public class SingleEdge<Symbol> extends Edge<Symbol> {
 		return sink;
 	}
 
+	@Override
+	public HashSet<State> getSinks() {
+		HashSet<State> ret = new HashSet<State>();
+		ret.add(getSink());
+		return ret;
+	}
+	
 	public void setSink(State sink) {
 		this.sink = sink;
 	}
@@ -61,4 +70,5 @@ public class SingleEdge<Symbol> extends Edge<Symbol> {
 			return false;
 		}
 	}
+
 }