From 0d00e9097ed39c0feea0cf748f3a64c7db6c0d1b Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Wed, 12 Aug 2015 14:52:30 +0000
Subject: [PATCH] AcceptanceRabinDD, AcceptanceStreettDD: add complement and
 and(), or() methods

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10495 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/acceptance/AcceptanceRabinDD.java   | 47 +++++++++++++++++++
 prism/src/acceptance/AcceptanceStreettDD.java | 47 +++++++++++++++++++
 2 files changed, 94 insertions(+)

diff --git a/prism/src/acceptance/AcceptanceRabinDD.java b/prism/src/acceptance/AcceptanceRabinDD.java
index 13cc387e..d707a02c 100644
--- a/prism/src/acceptance/AcceptanceRabinDD.java
+++ b/prism/src/acceptance/AcceptanceRabinDD.java
@@ -96,6 +96,11 @@ public class AcceptanceRabinDD
 			return K;
 		}
 
+		public RabinPairDD clone()
+		{
+			return new RabinPairDD(getL(), getK());
+		}
+
 		/** Returns true if the bottom strongly connected component
 		 * given by bscc_states is accepting for this pair.
 		 * <br>[ REFS: <i>none</i>, DEREFS: <i>none</i> ]
@@ -125,6 +130,11 @@ public class AcceptanceRabinDD
 		}
 	}
 
+	/** Constructor, create empty condition */
+	public AcceptanceRabinDD()
+	{
+	}
+
 	/**
 	 * Constructor, from a BitSet-based AcceptanceRabin.
 	 *
@@ -161,6 +171,43 @@ public class AcceptanceRabinDD
 		return false;
 	}
 
+	/**
+	 * Get the Streett acceptance condition that is the dual of this Rabin acceptance condition, i.e.,
+	 * any word that is accepted by this condition is rejected by the returned Streett condition.
+	 * @return the complement Streett acceptance condition
+	 */
+	public AcceptanceStreettDD complement()
+	{
+		AcceptanceStreettDD accStreett = new AcceptanceStreettDD();
+
+		for (RabinPairDD accPairRabin : this) {
+			JDDNode R = accPairRabin.getK();
+			JDDNode G = accPairRabin.getL();
+			AcceptanceStreettDD.StreettPairDD accPairStreett = new AcceptanceStreettDD.StreettPairDD(R, G);
+			accStreett.add(accPairStreett);
+		}
+		return accStreett;
+	}
+
+	/**
+	 * Returns a new Rabin acceptance condition that corresponds to the disjunction
+	 * of this and the other Rabin acceptance condition. The RabinPairs are cloned, i.e.,
+	 * not shared with the argument acceptance condition.
+	 * @param other the other Rabin acceptance condition
+	 * @return new AcceptanceRabin, disjunction of this and other
+	 */
+	public AcceptanceRabinDD or(AcceptanceRabinDD other)
+	{
+		AcceptanceRabinDD result = new AcceptanceRabinDD();
+		for (RabinPairDD pair : this) {
+			result.add(pair.clone());
+		}
+		for (RabinPairDD pair : other) {
+			result.add(pair.clone());
+		}
+		return result;
+	}
+
 	@Override
 	public void clear()
 	{
diff --git a/prism/src/acceptance/AcceptanceStreettDD.java b/prism/src/acceptance/AcceptanceStreettDD.java
index 84b2cbc7..09ef942f 100644
--- a/prism/src/acceptance/AcceptanceStreettDD.java
+++ b/prism/src/acceptance/AcceptanceStreettDD.java
@@ -96,6 +96,11 @@ public class AcceptanceStreettDD
 			return G;
 		}
 
+		public StreettPairDD clone()
+		{
+			return new StreettPairDD(getR(), getG());
+		}
+
 		/** Returns true if the bottom strongly connected component
 		 * given by bscc_states is accepting for this pair.
 		 * <br>[ REFS: <i>none</i>, DEREFS: <i>none</i> ]
@@ -125,6 +130,11 @@ public class AcceptanceStreettDD
 		}
 	}
 
+	/** Constructor, create empty condition */
+	public AcceptanceStreettDD()
+	{
+	}
+
 	/**
 	 * Constructor, from a BitSet-based AcceptanceStreett.
 	 *
@@ -170,6 +180,43 @@ public class AcceptanceStreettDD
 		super.clear();
 	}
 
+	/**
+	 * Returns a new Streett acceptance condition that corresponds to the conjunction
+	 * of this and the other Streett acceptance condition. The StreettPairs are cloned, i.e.,
+	 * not shared with the argument acceptance condition.
+	 * @param other the other Streett acceptance condition
+	 * @return new AcceptanceStreett, conjunction of this and other
+	 */
+	public AcceptanceStreettDD and(AcceptanceStreettDD other)
+	{
+		AcceptanceStreettDD result = new AcceptanceStreettDD();
+		for (StreettPairDD pair : this) {
+			result.add(pair.clone());
+		}
+		for (StreettPairDD pair : other) {
+			result.add(pair.clone());
+		}
+		return result;
+	}
+
+	/**
+	 * Get the Rabin acceptance condition that is the dual of this Streett acceptance condition, i.e.,
+	 * any word that is accepted by this condition is rejected by the returned Rabin condition.
+	 * @return the complement Rabin acceptance condition
+	 */
+	public AcceptanceRabinDD complement()
+	{
+		AcceptanceRabinDD accRabin = new AcceptanceRabinDD();
+
+		for (StreettPairDD accPairStreett : this) {
+			JDDNode L = accPairStreett.getG();
+			JDDNode K = accPairStreett.getR();
+			AcceptanceRabinDD.RabinPairDD accPairRabin = new AcceptanceRabinDD.RabinPairDD(L, K);
+			accRabin.add(accPairRabin);
+		}
+		return accRabin;
+	}
+
 	@Override
 	public String toString() {
 		String result = "";