From 2ea82a99a21094894286f8d29857c869e81b7848 Mon Sep 17 00:00:00 2001
From: Sascha Wunderlich <sascha.wunderlich@tu-dresden.de>
Date: Mon, 14 Nov 2016 14:14:36 +0100
Subject: [PATCH] automata.finite: toDot methods for DFA

---
 .../finite/DeterministicFiniteAutomaton.java  | 35 +++++++++++++++++++
 .../src/automata/finite/FiniteAutomaton.java  | 16 +++++++++
 .../NondeterministicFiniteAutomaton.java      |  5 ++-
 3 files changed, 55 insertions(+), 1 deletion(-)

diff --git a/prism/src/automata/finite/DeterministicFiniteAutomaton.java b/prism/src/automata/finite/DeterministicFiniteAutomaton.java
index 0ffc27ea..06de5312 100644
--- a/prism/src/automata/finite/DeterministicFiniteAutomaton.java
+++ b/prism/src/automata/finite/DeterministicFiniteAutomaton.java
@@ -172,4 +172,39 @@ 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/FiniteAutomaton.java b/prism/src/automata/finite/FiniteAutomaton.java
index 82f465a0..26ef1fc9 100644
--- a/prism/src/automata/finite/FiniteAutomaton.java
+++ b/prism/src/automata/finite/FiniteAutomaton.java
@@ -9,6 +9,10 @@ import java.util.Queue;
 import java.util.Set;
 import java.util.Stack;
 
+import prism.PrismException;
+import prism.PrismFileLog;
+import prism.PrismLog;
+
 public abstract class FiniteAutomaton<Symbol, E extends Edge<Symbol>> {
 	protected List<Symbol> apList;
 	
@@ -457,4 +461,16 @@ public abstract class FiniteAutomaton<Symbol, E extends Edge<Symbol>> {
 		
 		return result.toString();
 	}
+	
+	public void exportToDotFile(String filename) throws PrismException {
+		try (PrismFileLog log = PrismFileLog.create(filename)) {
+			exportToDotFile(log);
+		}
+	}
+	
+	public void exportToDotFile(PrismLog out) {
+		out.print(toDot());
+	}
+	
+	public abstract String toDot();
 }
diff --git a/prism/src/automata/finite/NondeterministicFiniteAutomaton.java b/prism/src/automata/finite/NondeterministicFiniteAutomaton.java
index 7405b416..743648fd 100644
--- a/prism/src/automata/finite/NondeterministicFiniteAutomaton.java
+++ b/prism/src/automata/finite/NondeterministicFiniteAutomaton.java
@@ -10,6 +10,9 @@ import java.util.Set;
 import parser.ast.Expression;
 import parser.ast.ExpressionLabel;
 import parser.ast.ExpressionRegular;
+import prism.PrismException;
+import prism.PrismFileLog;
+import prism.PrismLog;
 /**
  * Class to store a non-deterministic finite automaton.
  */
@@ -449,7 +452,7 @@ public class NondeterministicFiniteAutomaton<Symbol> extends FiniteAutomaton<Sym
 	 * 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");