From 71183e47e7820c958cb4fb8d182122a3633c329b Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Thu, 25 Feb 2016 16:23:03 +0000
Subject: [PATCH] JDD: add Equiv BDD operation (dd1 <=> dd2)

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11219 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/jdd/JDD.java | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/prism/src/jdd/JDD.java b/prism/src/jdd/JDD.java
index 07bbd60e..c8d7797f 100644
--- a/prism/src/jdd/JDD.java
+++ b/prism/src/jdd/JDD.java
@@ -421,6 +421,15 @@ public class JDD
 		return ptrToNode(DD_Implies(dd1.ptr(), dd2.ptr()));
 	}
 	
+	/**
+	 * equivalence of dd1, dd2 (have to be 0/1-MTBDDs)
+	 * [ REFS: <i>result</i>, DEREFS: dd1, dd2 ]
+	 */
+	public static JDDNode Equiv(JDDNode dd1, JDDNode dd2)
+	{
+		return Not(Xor(dd1, dd2));
+	}
+	
 	/**
 	 * generic apply operation
 	 * <br>[ REFS: <i>result</i>, DEREFS: dd1, dd2 ]