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

@@ -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()
 	{

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 = "";