From f9b84efc89738cf32804b10f61e4183ea3b111f0 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Mon, 4 Jan 2016 17:03:06 +0000
Subject: [PATCH] NBA: DOT output (roughly similar to the ltl2dstar DOT output)

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11105 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/jltl2dstar/NBA.java | 29 ++++++++++++++++++++++++++++-
 1 file changed, 28 insertions(+), 1 deletion(-)

diff --git a/prism/src/jltl2dstar/NBA.java b/prism/src/jltl2dstar/NBA.java
index ba382ade..4442134c 100644
--- a/prism/src/jltl2dstar/NBA.java
+++ b/prism/src/jltl2dstar/NBA.java
@@ -307,7 +307,34 @@ public class NBA implements Iterable<NBA_State> {
 		out.println("--END--");
 	}
 
-	// public void print_dot(std::ostream& out);
+	/** Print the NBA as a Graphviz (DOT) graph to out */
+	public void print_dot(PrintStream out) {
+		out.println("digraph nba {");
+		out.println(" node [fontname=Helvetica]");
+		out.println(" edge [constraints=false, fontname=Helvetica]");
+
+		for (NBA_State state : _index) {
+			out.print(" " + state.getName());  // id
+			out.print(" [shape=");
+			out.print((state.isFinal() ? "box" : "circle"));
+			if (state == getStartState()) {
+				out.print(", style=filled, color=black, fillcolor=grey");
+			}
+			out.println("]");
+
+			for (Map.Entry<APElement, MyBitSet> edge : state) {
+				APElement label = edge.getKey();
+				//String labelString = "["+label.toStringHOA(_apset.size())+"]";
+				String labelString = label.toString(getAPSet(),true);
+				MyBitSet to_states = edge.getValue();
+				for (Integer to : to_states) {
+					out.print("  " + state.getName() + " -> " + to);
+					out.println(" [label=\"" + labelString + "\"]");
+				}
+			}
+		}
+		out.println("}");
+	}
 
 	/** Return number of states. */
 	public int getStateCount()