From 78d3755e4e339f9e2c6c0d0d24e15c45b3fb9320 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Tue, 19 Aug 2014 08:34:05 +0000
Subject: [PATCH] A jltl2ba bug fix from Joachim Klein - fixes various
 previously reported LTL->DRA crashes.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9109 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/jltl2ba/Alternating.java | 31 +++++++++++++++---------------
 prism/src/jltl2ba/Generalized.java |  6 +++---
 2 files changed, 19 insertions(+), 18 deletions(-)

diff --git a/prism/src/jltl2ba/Alternating.java b/prism/src/jltl2ba/Alternating.java
index 3605bc44..45a47d45 100644
--- a/prism/src/jltl2ba/Alternating.java
+++ b/prism/src/jltl2ba/Alternating.java
@@ -66,21 +66,22 @@ public class Alternating {
 			rv.nxt = nxt;
 			return rv;
 		}
+	}
+	
+	public static ATrans do_merge_atrans(ATrans first, ATrans second) {
+		if (first == null || second == null)
+			return null;
 
-		public ATrans merge(ATrans other) {
-			if (other == null)
-				return null;
-
-			ATrans rv = this.clone();
+		ATrans rv = first.clone();
+		rv.nxt = null;
 
-			rv.to.or(other.to);
-			rv.pos.or(other.pos);
-			rv.neg.or(other.neg);
+		rv.to.or(second.to);
+		rv.pos.or(second.pos);
+		rv.neg.or(second.neg);
 
-			if (rv.pos.intersects(rv.neg))
-				rv = null;
-			return rv;
-		}
+		if (rv.pos.intersects(rv.neg))
+			rv = null;
+		return rv;
 	}
 
 	public static class AProd {
@@ -133,7 +134,7 @@ public class Alternating {
 			rgt = _boolean(p.right);
 			for (t1 = lft; t1 != null; t1 = t1.nxt) {
 				for (t2 = rgt; t2 != null; t2 = t2.nxt) {
-					ATrans tmp = t1.merge(t2);
+					ATrans tmp = do_merge_atrans(t1, t2);
 					if (tmp != null) {
 						tmp.nxt = result;
 						result = tmp;
@@ -217,7 +218,7 @@ public class Alternating {
 				ATrans tmp;
 
 				for (t2 = buildAlternating(p.left); t2 != null; t2 = t2.nxt) {
-					tmp = t1.merge(t2); /* p && q */
+					tmp = do_merge_atrans(t1, t2); /* p && q */
 					if (tmp != null) {
 						tmp.nxt = t;
 						t = tmp;
@@ -234,7 +235,7 @@ public class Alternating {
 		case AND:
 			for (t1 = buildAlternating(p.left); t1 != null; t1 = t1.nxt) {
 				for (t2 = buildAlternating(p.right); t2 != null; t2 = t2.nxt) {
-					ATrans tmp = t1.merge(t2);
+					ATrans tmp = do_merge_atrans(t1, t2);
 					if (tmp != null) {
 						tmp.nxt = t;
 						t = tmp;
diff --git a/prism/src/jltl2ba/Generalized.java b/prism/src/jltl2ba/Generalized.java
index 1aada420..43be508f 100644
--- a/prism/src/jltl2ba/Generalized.java
+++ b/prism/src/jltl2ba/Generalized.java
@@ -336,7 +336,7 @@ public class Generalized {
 			p.trans = a.transition.get(list.get(i));
 			if (p.trans == null)
 				trans_exist = 0;
-			p.prod = prod.nxt.prod.merge(p.trans);
+			p.prod = Alternating.do_merge_atrans(prod.nxt.prod, p.trans);
 			p.nxt = prod.nxt;
 			p.prv = prod;
 			p.nxt.prv = p;
@@ -393,11 +393,11 @@ public class Generalized {
 			if (p == prod)
 				break;
 			p.trans = p.trans.nxt;
-			p.prod = p.nxt.prod.merge(p.trans);
+			p.prod = Alternating.do_merge_atrans(p.nxt.prod, p.trans);
 			p = p.prv;
 			while (p != prod) {
 				p.trans = a.transition.get(p.astate);
-				p.prod = p.nxt.prod.merge(p.trans);
+				p.prod = Alternating.do_merge_atrans(p.nxt.prod, p.trans);
 				p = p.prv;
 			}
 		}