From 59f44c56ee5b8e976b4c049ebfcdb3bdd21462ac Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Thu, 19 Nov 2015 16:37:35 +0000
Subject: [PATCH] SimpleLTL: isTree() check to ensure that graph structure is
 tree, not DAG

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

diff --git a/prism/src/jltl2ba/SimpleLTL.java b/prism/src/jltl2ba/SimpleLTL.java
index dbd2d147..40019835 100644
--- a/prism/src/jltl2ba/SimpleLTL.java
+++ b/prism/src/jltl2ba/SimpleLTL.java
@@ -30,6 +30,7 @@ package jltl2ba;
 import java.io.PrintStream;
 import java.util.ArrayList;
 import java.util.HashMap;
+import java.util.HashSet;
 import java.util.List;
 import java.util.Map;
 
@@ -890,6 +891,42 @@ public class SimpleLTL {
 		return false;
 	}
 
+	/**
+	 * Returns true if this SimpleLTL structure is a tree, i.e., not a
+	 * directed acyclical graph (DAG) where sharing of subtrees is allowed.
+	 */
+	public boolean isTree()
+	{
+		HashSet<PlainObjectReference<SimpleLTL>> seen = new HashSet<PlainObjectReference<SimpleLTL>>();
+		return isTree(seen);
+	}
+
+	/**
+	 * Recursive function for checking if this SimpleLTL structure is a tree, i.e., not a
+	 * directed acyclical graph (DAG) where sharing of subtrees is allowed.
+	 *
+	 * The already seen SimpleLTL subtrees are tracked in {@code seen}.
+	 */
+	private boolean isTree(HashSet<PlainObjectReference<SimpleLTL>> seen)
+	{
+		PlainObjectReference<SimpleLTL> ref = new PlainObjectReference<SimpleLTL>(this);
+		if (seen.contains(ref)) {
+			return false;
+		}
+		seen.add(ref);
+
+		if (left != null && !left.isTree(seen)) {
+			// left child exists and is not a tree
+			return false;
+		}
+		if (right != null && !right.isTree(seen)) {
+			// right child exists and is not a tree
+			return false;
+		}
+
+		return true;
+	}
+
 	public SimpleLTL toDNF() throws PrismException
 	{
 		switch (kind) {