From e3b49ea35ffc97a7ff94a08d1a7480ca310c33c1 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Thu, 19 Nov 2015 16:36:19 +0000
Subject: [PATCH] SimpleLTL: add toDot() output of the syntax tree / DAG

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10896 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/jltl2ba/SimpleLTL.java | 63 ++++++++++++++++++++++++++++++++
 1 file changed, 63 insertions(+)

diff --git a/prism/src/jltl2ba/SimpleLTL.java b/prism/src/jltl2ba/SimpleLTL.java
index 3ce6165b..dbd2d147 100644
--- a/prism/src/jltl2ba/SimpleLTL.java
+++ b/prism/src/jltl2ba/SimpleLTL.java
@@ -27,11 +27,13 @@
 
 package jltl2ba;
 
+import java.io.PrintStream;
 import java.util.ArrayList;
 import java.util.HashMap;
 import java.util.List;
 import java.util.Map;
 
+import common.PlainObjectReference;
 import jltl2dstar.APMonom;
 import jltl2dstar.NBA;
 import prism.PrismException;
@@ -1299,4 +1301,65 @@ public class SimpleLTL {
 	{
 		return this.toNBA(new APSet());
 	}
+
+	/** Print a DOT representation of the syntax tree of this SimpleLTL formula */
+	public void toDot(PrintStream out) {
+		HashMap<PlainObjectReference<SimpleLTL>, String> map = new HashMap<PlainObjectReference<SimpleLTL>, String>();
+
+		out.println("digraph {");
+		toDot(out, map);
+		out.println("}");
+	}
+
+	/**
+	 * Print a DOT representation of the syntax tree of this SimpleLTL formula.
+	 *
+	 * @param out the output print stream
+	 * @param seen a map storing an identifier for each subformula that has already been seen / printed
+	 */
+	private String toDot(PrintStream out, HashMap<PlainObjectReference<SimpleLTL>, String> seen)
+	{
+		PlainObjectReference<SimpleLTL> ref = new PlainObjectReference<SimpleLTL>(this);
+		if (seen.containsKey(ref)) {
+			return seen.get(ref);
+		}
+
+		String id = Integer.toString(seen.size());
+		seen.put(ref, id);
+		out.println(id + " [label=\""+toStringLBT()+"\"]");
+
+		switch (kind) {
+		case AND:
+		case EQUIV:
+		case OR:
+		case UNTIL:
+		case RELEASE:
+		case IMPLIES: {
+			String leftID = left.toDot(out, seen);
+			String rightID = right.toDot(out, seen);
+			out.println(id + " -> " + leftID);
+			out.println(id + " -> " + rightID);
+			break;
+		}
+		case FINALLY:
+		case GLOBALLY:
+		case NEXT:
+		case NOT: {
+			String leftID = left.toDot(out, seen);
+			out.println(id + " -> " + leftID);
+			break;
+		}
+
+		case AP:
+		case TRUE:
+		case FALSE:
+			break;
+
+		default:
+			break;
+		}
+
+		return id;
+	}
+
 }