Add acceptance.* package, with AcceptanceOmega and derived classes for BitSet-based acceptance and AcceptanceOmegaDD for JDD-based acceptance. [Joachim Klein]

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9576 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago · ad6c3b4800
7 changed files with 1125 additions and 0 deletions
--- a/prism/src/acceptance/AcceptanceOmega.java
+++ b/prism/src/acceptance/AcceptanceOmega.java
@ -0,0 +1,85 @@
+//==============================================================================
+//	
+//	Copyright (c) 2014-
+//	Authors:
+//	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package acceptance;
+
+import java.util.BitSet;
+
+import jdd.JDDVars;
+
+/**
+ * Generic interface for an omega-regular acceptance condition (BitSet-based).
+ */
+public interface AcceptanceOmega extends Cloneable
+{
+	/** Returns true if the bottom strongly connected component (BSSC)
+	 *  given by bscc_states is accepting for this acceptance condition.
+	 **/
+	public boolean isBSCCAccepting(BitSet bscc_states);
+
+	/** Get the acceptance signature for state i.
+	 **/
+	public String getSignatureForState(int i);
+
+	/**
+	 * Get a string describing the acceptance condition's size,
+	 * i.e. "x Rabin pairs", etc.
+	 */
+	public String getSizeStatistics();
+
+	/** Returns the AcceptanceType of this acceptance condition */
+	public AcceptanceType getType();
+
+	/** Returns the type of this acceptance condition as a String,
+	 * i.e., "R" for Rabin
+	 */
+	public String getTypeAbbreviated();
+
+	/** Returns a full name for this acceptance condition */
+	public String getTypeName();
+
+	/** Make a copy of the acceptance condition. */
+	public AcceptanceOmega clone();
+
+	/** Abstract functor for use with the lift function. */
+	public static abstract class LiftBitSet {
+		public abstract BitSet lift(BitSet states);
+	};
+
+	/**
+	 * Lift the state sets in the acceptance condition.
+	 * For each state set {@code states} in the condition,
+	 * {@code lifter.lift(states)} is called and the state set is
+	 * replaced by the result.
+	 **/
+	public void lift(LiftBitSet lifter);
+
+	/**
+	 * Convert this BitSet based acceptance condition to the corresponding BDD based acceptance condition.
+	 * @param ddRowVars JDDVars of the row variables corresponding to the bits in the bitset
+	 */
+	public AcceptanceOmegaDD toAcceptanceDD(JDDVars ddRowVars);
+}
--- a/prism/src/acceptance/AcceptanceOmegaDD.java
+++ b/prism/src/acceptance/AcceptanceOmegaDD.java
@ -0,0 +1,65 @@
+//==============================================================================
+//	
+//	Copyright (c) 2014-
+//	Authors:
+//	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package acceptance;
+
+import jdd.JDDNode;
+
+/**
+ * Generic interface for an omega-regular acceptance condition (BDD-based).
+ */
+public interface AcceptanceOmegaDD
+{
+	/** Returns true if the bottom strongly connected component (BSSC)
+	 *  given by bscc_states is accepting for this acceptance condition.
+	 * <br>[ REFS: <i>none</i>, DEREFS: <i>none</i> ]
+	 **/
+	public boolean isBSCCAccepting(JDDNode bscc_states);
+
+	/**
+	 * Get a string describing the acceptance condition's size,
+	 * i.e. "x Rabin pairs", etc.
+	 */
+	public String getSizeStatistics();
+
+	/** Returns the AcceptanceType of this acceptance condition */
+	public AcceptanceType getType();
+
+	/** Returns the type of this acceptance condition as a String,
+	 * i.e., "R" for Rabin
+	 */
+	public String getTypeAbbreviated();
+
+	/**
+	 * Clear the resources used by this acceptance condition.
+	 * Call to ensure that the JDD based state sets actually get
+	 * dereferenced.
+	 */
+	void clear();
+
+	/** Returns a full name for this acceptance condition */
+	public String getTypeName();
+}
--- a/prism/src/acceptance/AcceptanceRabin.java
+++ b/prism/src/acceptance/AcceptanceRabin.java
@ -0,0 +1,256 @@
+//==============================================================================
+//	
+//	Copyright (c) 2014-
+//	Authors:
+//	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package acceptance;
+
+import java.util.ArrayList;
+import java.util.BitSet;
+
+import jdd.JDDVars;
+
+/**
+ * A Rabin acceptance condition (based on BitSet state sets).
+ * This is a list of RabinPairs, which can be manipulated with the usual List interface.
+ * <br>
+ * Semantics: Each Rabin pair has a state set L and K and is accepting iff
+ * L is not visited infinitely often and K is visited infinitely often:
+ *   (F G !"L") & (G F "K").
+ *
+ * The Rabin condition is accepting if at least one of the pairs is accepting.
+ */
+@SuppressWarnings("serial")
+public class AcceptanceRabin
+       extends ArrayList<AcceptanceRabin.RabinPair>
+       implements AcceptanceOmega
+{
+
+	/**
+	 * A pair in a Rabin acceptance condition, i.e., with
+	 *  (F G !"L")  &  (G F "K")
+	 **/
+	public static class RabinPair {
+		/** State set L (should be visited only finitely often) */
+		private BitSet L;
+
+		/** State set K (should be visited infinitely often) */
+		private BitSet K;
+
+		/** Constructor with L and K state sets */
+		public RabinPair(BitSet L, BitSet K) {
+			this.L = L;
+			this.K = K;
+		}
+
+		/** Get the state set L */
+		public BitSet getL()
+		{
+			return L;
+		}
+
+		/** Get the state set K */
+		public BitSet getK()
+		{
+			return K;
+		}
+
+		/** Returns true if the bottom strongly connected component
+		 * given by bscc_states is accepting for this pair.
+		 */
+		public boolean isBSCCAccepting(BitSet bscc_states)
+		{
+			if (L.intersects(bscc_states)) {
+				// there is some state in bscc_states that is
+				// forbidden by L
+				return false;
+			}
+
+			if (K.intersects(bscc_states)) {
+				// there is some state in bscc_states that is
+				// contained in K -> infinitely often visits to K
+				return true;
+			}
+
+			return false;
+		}
+
+		/** Generate signature for this Rabin pair and the given state.
+		 *  If the state is a member of L, returns "-pairIndex".
+		 *  If the state is a member of K, returns "+pairIndex".
+		 *  @param stateIndex the state index
+		 *  @param pairIndex the index of this Rabin pair
+		 **/
+		public String getSignatureForState(int stateIndex, int pairIndex)
+		{
+			if (L.get(stateIndex)) {
+				return "-"+pairIndex;
+			} else if (K.get(stateIndex)) {
+				return "+"+pairIndex;
+			} else {
+				return "";
+			}
+		}
+
+		@Override
+		public RabinPair clone()
+		{
+			return new RabinPair((BitSet)L.clone(), (BitSet)K.clone());
+		}
+
+		/** Returns a textual representation of this Rabin pair. */
+		@Override
+		public String toString() {
+			return "(" + L + "," + K + ")";
+		}
+	}
+
+	/** Make a copy of the acceptance condition. */
+	public AcceptanceRabin clone()
+	{
+		AcceptanceRabin result = new AcceptanceRabin();
+		for (RabinPair pair : this) {
+			result.add(pair.clone());
+		}
+
+		return result;
+	}
+
+	/** Returns true if the bottom strongly connected component
+	 * given by bscc_states is accepting for this Rabin condition,
+	 * i.e., there is a pair that accepts for bscc_states.
+	 */
+	public boolean isBSCCAccepting(BitSet bscc_states)
+	{
+		for (RabinPair pair : this) {
+			if (pair.isBSCCAccepting(bscc_states)) {
+				return true;
+			}
+		}
+
+		return false;
+	}
+
+	@Override
+	public void lift(LiftBitSet lifter) {
+		for (RabinPair pair : this) {
+			pair.L = lifter.lift(pair.L);
+			pair.K = lifter.lift(pair.K);
+		}
+	}
+
+	/**
+	 * 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 AcceptanceStreett complement()
+	{
+		AcceptanceStreett accRabin = new AcceptanceStreett();
+
+		for (RabinPair accPairRabin : this) {
+			BitSet R = (BitSet) accPairRabin.getK().clone();
+			BitSet G = (BitSet) accPairRabin.getL().clone();
+			AcceptanceStreett.StreettPair accPairStreett = new AcceptanceStreett.StreettPair(R, G);
+			accRabin.add(accPairStreett);
+		}
+
+		return accRabin;
+	}
+
+	/**
+	 * 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 AcceptanceRabin or(AcceptanceRabin other)
+	{
+		AcceptanceRabin result = new AcceptanceRabin();
+		for (RabinPair pair : this) {
+			result.add((RabinPair) pair.clone());
+		}
+		for (RabinPair pair : other) {
+			result.add((RabinPair) pair.clone());
+		}
+		return result;
+	}
+
+	@Override
+	public AcceptanceRabinDD toAcceptanceDD(JDDVars ddRowVars)
+	{
+		return new AcceptanceRabinDD(this, ddRowVars);
+	}
+
+	/**
+	 * Get the acceptance signature for state stateIndex.
+	 **/
+	public String getSignatureForState(int stateIndex)
+	{
+		String result = "";
+
+		for (int pairIndex=0; pairIndex<size(); pairIndex++) {
+			RabinPair pair = get(pairIndex);
+			result += pair.getSignatureForState(stateIndex,  pairIndex);
+		}
+
+		return result;
+	}
+
+	/** Returns a textual representation of this acceptance condition. */
+	@Override
+	public String toString()
+	{
+		String result = "";
+		for (RabinPair pair : this) {
+			result += pair.toString();
+		}
+		return result;
+	}
+
+	@Override
+	public String getSizeStatistics()
+	{
+		return size() + " Rabin pairs";
+	}
+
+	@Override
+	public AcceptanceType getType()
+	{
+		return AcceptanceType.RABIN;
+	}
+
+	@Override
+	public String getTypeAbbreviated()
+	{
+		return "R";
+	}
+
+	@Override
+	public String getTypeName()
+	{
+		return "Rabin";
+	}
+}
--- a/prism/src/acceptance/AcceptanceRabinDD.java
+++ b/prism/src/acceptance/AcceptanceRabinDD.java
@ -0,0 +1,209 @@
+//==============================================================================
+//	
+//	Copyright (c) 2014-
+//	Authors:
+//	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package acceptance;
+
+import java.util.ArrayList;
+
+import common.IterableBitSet;
+
+import jdd.JDD;
+import jdd.JDDNode;
+import jdd.JDDVars;
+
+/**
+ * A Rabin acceptance condition (based on JDD state sets)
+ * This is a list of RabinPairs, which can be manipulated with the usual List interface.
+ * <br>
+ * Semantics: Each Rabin pair has a state set L and K and is accepting iff
+ * L is not visited infinitely often and K is visited infinitely often:
+ *   (F G !"L") & (G F "K").
+ *
+ * The Rabin condition is accepting if at least one of the pairs is accepting.
+ */
+@SuppressWarnings("serial")
+public class AcceptanceRabinDD
+       extends ArrayList<AcceptanceRabinDD.RabinPairDD>
+       implements AcceptanceOmegaDD
+{
+
+	/**
+	 * A pair in a Rabin acceptance condition, i.e., with
+	 *  (F G !"L")  &  (G F "K")
+	 **/
+	public static class RabinPairDD {
+		/** State set L (should be visited only finitely often) */
+		private JDDNode L;
+
+		/** State set K (should be visited infinitely often) */
+		private JDDNode K;
+
+		/**
+		 * Constructor with L and K state sets.
+		 * Becomes owner of the references of L and K.
+		 */
+		public RabinPairDD(JDDNode L, JDDNode K)
+		{
+			this.L = L;
+			this.K = K;
+		}
+
+		/** Clear resources of the state sets */
+		public void clear()
+		{
+			if (L!=null) JDD.Deref(L);
+			if (K!=null) JDD.Deref(K);
+		}
+
+		/** Get a referenced copy of the state set L.
+		 * <br>[ REFS: <i>result</i>, DEREFS: <i>none</i> ]
+		 */
+		public JDDNode getL()
+		{
+			JDD.Ref(L);
+			return L;
+		}
+
+		/** Get a referenced copy of the state set K.
+		 * <br>[ REFS: <i>result</i>, DEREFS: <i>none</i> ]
+		 */
+		public JDDNode getK()
+		{
+			JDD.Ref(K);
+			return K;
+		}
+
+		/** Returns true if the bottom strongly connected component
+		 * given by bscc_states is accepting for this pair.
+		 */
+		public boolean isBSCCAccepting(JDDNode bscc_states)
+		{
+			if (JDD.AreInterecting(L, bscc_states)) {
+				// there is some state in bscc_states that is
+				// forbidden by L
+				return false;
+			}
+
+			if (JDD.AreInterecting(K, bscc_states)) {
+				// there is some state in bscc_states that is
+				// contained in K -> infinitely often visits to K
+				return true;
+			}
+
+			return false;
+		}
+
+		/** Returns a textual representation of this Rabin pair. */
+		@Override
+		public String toString()
+		{
+			return "(" + L + "," + K + ")";
+		}
+	}
+
+	/**
+	 * Constructor, from a BitSet-based AcceptanceRabin.
+	 *
+	 * @param acceptance the BitSet-based acceptance condition
+	 * @param ddRowVars JDDVars of the row variables corresponding to the bits in the bit set
+	 */
+	public AcceptanceRabinDD(AcceptanceRabin acceptance, JDDVars ddRowVars)
+	{
+		for (AcceptanceRabin.RabinPair pair : acceptance) {
+			// get BDD based newL and newK from the bit sets
+			JDDNode newL = JDD.Constant(0);
+			for (int i : IterableBitSet.getSetBits(pair.getL())) {
+				newL = JDD.SetVectorElement(newL, ddRowVars, i, 1.0);
+			}
+
+			JDDNode newK = JDD.Constant(0);
+			for (int i : IterableBitSet.getSetBits(pair.getK())) {
+				newK = JDD.SetVectorElement(newK, ddRowVars, i, 1.0);
+			}
+
+			RabinPairDD newPair = new RabinPairDD(newL, newK);
+			this.add(newPair);
+		}
+	}
+
+	/** Returns true if the bottom strongly connected component
+	 * given by bscc_states is accepting for this Rabin condition,
+	 * i.e., there is a pair that accepts for bscc_states.
+	 */
+	public boolean isBSCCAccepting(JDDNode bscc_states)
+	{
+		for (RabinPairDD pair : this) {
+			if (pair.isBSCCAccepting(bscc_states)) {
+				return true;
+			}
+		}
+		return false;
+	}
+
+	@Override
+	public void clear()
+	{
+		for (RabinPairDD pair : this) {
+			pair.clear();
+		}
+		super.clear();
+	}
+
+	/** Returns a textual representation of this acceptance condition. */
+	@Override
+	public String toString()
+	{
+		String result = "";
+		for (RabinPairDD pair : this) {
+			result += pair.toString();
+		}
+		return result;
+	}
+
+	@Override
+	public String getSizeStatistics()
+	{
+		return size() + " Rabin pairs";
+	}
+
+	@Override
+	public AcceptanceType getType()
+	{
+		return AcceptanceType.RABIN;
+	}
+
+	@Override
+	public String getTypeAbbreviated()
+	{
+		return "R";
+	}
+
+	@Override
+	public String getTypeName()
+	{
+		return "Rabin";
+	}
+}
--- a/prism/src/acceptance/AcceptanceStreett.java
+++ b/prism/src/acceptance/AcceptanceStreett.java
@ -0,0 +1,257 @@
+//==============================================================================
+//	
+//	Copyright (c) 2014-
+//	Authors:
+//	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package acceptance;
+
+import java.util.ArrayList;
+import java.util.BitSet;
+
+import jdd.JDDVars;
+
+/**
+ * A Streett acceptance condition (based on BitSet state sets).
+ * This is a list of StreettPairs, which can be manipulated with the usual List interface.
+ * <br>
+ * Semantics: Each Streett pair has a state set R and G and is accepting iff
+ * visiting R infinitely often implies visiting G infinitely often:
+ *   (G F "R") -> (G F "G").
+ *
+ * The Streett condition is accepting if all pairs are accepting.
+ */
+@SuppressWarnings("serial")
+public class AcceptanceStreett
+       extends ArrayList<AcceptanceStreett.StreettPair>
+       implements AcceptanceOmega
+{
+
+	/**
+	 * A pair in a Streett acceptance condition, i.e., with
+	 *  (G F "R") -> (G F "G")
+	 **/
+	public static class StreettPair {
+		/** State set R */
+		private BitSet R;
+
+		/** State set G */
+		private BitSet G;
+
+		/** Constructor with R and G state sets */
+		public StreettPair(BitSet R, BitSet G)
+		{
+			this.R = R;
+			this.G = G;
+		}
+
+		/** Get the state set R */
+		public BitSet getR()
+		{
+			return R;
+		}
+
+		/** Get the state set G */
+		public BitSet getG()
+		{
+			return G;
+		}
+
+		/** Returns true if the bottom strongly connected component
+		 * given by bscc_states is accepting for this pair.
+		 */
+		public boolean isBSCCAccepting(BitSet bscc_states)
+		{
+			if (R.intersects(bscc_states)) {
+				// there is some state in bscc_states
+				// that is in R, requiring that G is visited
+				// as well:
+				if (!G.intersects(bscc_states)) {
+					return false;
+				} else {
+					// G is visited as well
+					return true;
+				}
+			} else {
+				// no R visited, no need to check for G
+				return true;
+			}
+		}
+
+		/** Generate signature for this Streett pair and the given state.
+		 *  If the state is a member of R, returns "-pairIndex".
+		 *  If the state is a member of G, returns "+pairIndex".
+		 *  @param stateIndex the state index
+		 *  @param pairIndex the index of this Streeet pair
+		 **/
+		public String getSignatureForState(int stateIndex, int pairIndex)
+		{
+			if (G.get(stateIndex)) {
+				return "+"+pairIndex;
+			} else if (R.get(stateIndex)) {
+				return "-"+pairIndex;
+			} else {
+				return "";
+			}
+		}
+
+		@Override
+		public StreettPair clone()
+		{
+			return new StreettPair((BitSet)R.clone(), (BitSet)G.clone());
+		}
+
+		/** Returns a textual representation of this Streett pair. */
+		@Override
+		public String toString() {
+			return "(" + R + "->" + G + ")";
+		}
+	}
+
+	/** Make a copy of the acceptance condition. */
+	public AcceptanceStreett clone()
+	{
+		AcceptanceStreett result = new AcceptanceStreett();
+		for (StreettPair pair : this) {
+			result.add(pair.clone());
+		}
+
+		return result;
+	}
+
+	/** Returns true if the bottom strongly connected component
+	 * given by bscc_states is accepting for this Streett condition,
+	 * i.e., all pairs accept for bscc_states.
+	 */
+	@Override
+	public boolean isBSCCAccepting(BitSet bscc_states)
+	{
+		for (StreettPair pair : this) {
+			if (!pair.isBSCCAccepting(bscc_states)) {
+				return false;
+			}
+		}
+		return true;
+	}
+
+
+	@Override
+	public void lift(LiftBitSet lifter) {
+		for (StreettPair pair : this) {
+			pair.R = lifter.lift(pair.R);
+			pair.G = lifter.lift(pair.G);
+		}
+	}
+
+	/**
+	 * 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 AcceptanceRabin complement()
+	{
+		AcceptanceRabin accRabin = new AcceptanceRabin();
+
+		for (StreettPair accPairStreett : this) {
+			BitSet L = (BitSet) accPairStreett.getG().clone();
+			BitSet K = (BitSet) accPairStreett.getR().clone();
+			AcceptanceRabin.RabinPair accPairRabin = new AcceptanceRabin.RabinPair(L, K);
+			accRabin.add(accPairRabin);
+		}
+		return accRabin;
+	}
+
+	/**
+	 * 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 AcceptanceStreett and(AcceptanceStreett other)
+	{
+		AcceptanceStreett result = new AcceptanceStreett();
+		for (StreettPair pair : this) {
+			result.add((StreettPair) pair.clone());
+		}
+		for (StreettPair pair : other) {
+			result.add((StreettPair) pair.clone());
+		}
+		return result;
+	}
+
+	@Override
+	public AcceptanceStreettDD toAcceptanceDD(JDDVars ddRowVars)
+	{
+		return new AcceptanceStreettDD(this, ddRowVars);
+	}
+
+	/**
+	 * Get the acceptance signature for state stateIndex.
+	 **/
+	public String getSignatureForState(int stateIndex)
+	{
+		String result = "";
+
+		for (int pairIndex=0; pairIndex<size(); pairIndex++) {
+			StreettPair pair = get(pairIndex);
+			result += pair.getSignatureForState(stateIndex,  pairIndex);
+		}
+
+		return result;
+	}
+
+	@Override
+	public String toString()
+	{
+		String result = "";
+		for (StreettPair pair : this) {
+			result += pair.toString();
+		}
+		return result;
+	}
+
+	@Override
+	public String getSizeStatistics()
+	{
+		return size() + " Streett pairs";
+	}
+
+	@Override
+	public AcceptanceType getType()
+	{
+		return AcceptanceType.STREETT;
+	}
+
+	@Override
+	public String getTypeAbbreviated()
+	{
+		return "S";
+	}
+
+	@Override
+	public String getTypeName()
+	{
+		return "Streett";
+	}
+}
--- a/prism/src/acceptance/AcceptanceStreettDD.java
+++ b/prism/src/acceptance/AcceptanceStreettDD.java
@ -0,0 +1,204 @@
+//==============================================================================
+//	
+//	Copyright (c) 2014-
+//	Authors:
+//	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package acceptance;
+
+import java.util.ArrayList;
+
+import common.IterableBitSet;
+
+import jdd.JDD;
+import jdd.JDDNode;
+import jdd.JDDVars;
+
+/**
+ * A Streett acceptance condition (based on JDD state sets).
+ * This is a list of StreettPairs, which can be manipulated with the usual List interface.
+ * <br>
+ * Semantics: Each Streett pair has a state set R and G and is accepting iff
+ * visiting R infinitely often implies visiting G infinitely often:
+ *   (G F "R") -> (G F "G").
+ *
+ * The Streett condition is accepting if all pairs are accepting.
+ */
+@SuppressWarnings("serial")
+public class AcceptanceStreettDD
+       extends ArrayList<AcceptanceStreettDD.StreettPair>
+       implements AcceptanceOmegaDD
+{
+
+	/**
+	 * A pair in a Streett acceptance condition, i.e., with
+	 *  (G F "R") -> (G F "G")
+	 **/
+	public static class StreettPair {
+		/** State set R */
+		private JDDNode R;
+		
+		/** State set G */
+		private JDDNode G;
+
+		/**
+		 * Constructor with R and G state sets.
+		 * Becomes owner of the references of R and G.
+		 */
+		public StreettPair(JDDNode R, JDDNode G)
+		{
+			this.R = R;
+			this.G = G;
+		}
+
+		/** Clear resources of the state sets */
+		public void clear()
+		{
+			if (R != null) JDD.Deref(R);
+			if (G != null) JDD.Deref(G);
+		}
+
+		/** Get a referenced copy of the state set R.
+		 * <br>[ REFS: <i>result</i>, DEREFS: <i>none</i> ]
+		 */
+		public JDDNode getR()
+		{
+			JDD.Ref(R);
+			return R;
+		}
+
+		/** Get a referenced copy of the state set G.
+		 * <br>[ REFS: <i>result</i>, DEREFS: <i>none</i> ]
+		 */
+		public JDDNode getG()
+		{
+			JDD.Ref(G);
+			return G;
+		}
+
+		/** Returns true if the bottom strongly connected component
+		 * given by bscc_states is accepting for this pair.
+		 */
+		public boolean isBSCCAccepting(JDDNode bscc_states)
+		{
+			if (JDD.AreInterecting(R, bscc_states)) {
+				// there is some state in bscc_states
+				// that is in R, requiring that G is visited
+				// as well:
+				if (!JDD.AreInterecting(G, bscc_states)) {
+					return false;
+				} else {
+					// G is visited as well
+					return true;
+				}
+			} else {
+				// no R visited, no need to check for G
+				return true;
+			}
+		}
+
+		@Override
+		public String toString()
+		{
+			return "(" + R + "->" + G + ")";
+		}
+	}
+
+	/**
+	 * Constructor, from a BitSet-based AcceptanceStreett.
+	 *
+	 * @param acceptance the BitSet-based acceptance condition
+	 * @param ddRowVars JDDVars of the row variables corresponding to the bits in the bit set
+	 */
+	public AcceptanceStreettDD(AcceptanceStreett acceptance, JDDVars ddRowVars)
+	{
+		for (AcceptanceStreett.StreettPair pair : acceptance) {
+			// get BDD based newR and newG from the bit sets
+			JDDNode newR = JDD.Constant(0);
+			for (int i : IterableBitSet.getSetBits(pair.getR())) {
+				newR = JDD.SetVectorElement(newR, ddRowVars, i, 1.0);
+			}
+	
+			JDDNode newG = JDD.Constant(0);
+			for (int i : IterableBitSet.getSetBits(pair.getG())) {
+				newG = JDD.SetVectorElement(newG, ddRowVars, i, 1.0);
+			}
+	
+			StreettPair newPair = new StreettPair(newR, newG);
+			this.add(newPair);
+		}
+	}
+
+	@Override
+	public boolean isBSCCAccepting(JDDNode bscc_states)
+	{
+		for (StreettPair pair : this) {
+			if (!pair.isBSCCAccepting(bscc_states)) {
+				return false;
+			}
+		}
+		return true;
+	}
+
+	@Override
+	public void clear()
+	{
+		for (StreettPair pair : this) {
+			pair.clear();
+		}
+		super.clear();
+	}
+
+	@Override
+	public String toString() {
+		String result = "";
+		for (StreettPair pair : this) {
+			result += pair.toString();
+		}
+		return result;
+	}
+
+	@Override
+	public String getSizeStatistics()
+	{
+		return size() + " Streett pairs";
+	}
+
+	@Override
+	public AcceptanceType getType()
+	{
+		return AcceptanceType.STREETT;
+	}
+
+	@Override
+	public String getTypeAbbreviated()
+	{
+		return "S";
+	}
+
+	@Override
+	public String getTypeName()
+	{
+		return "Streett";
+	}
+}
--- a/prism/src/acceptance/AcceptanceType.java
+++ b/prism/src/acceptance/AcceptanceType.java
@ -0,0 +1,49 @@
+//==============================================================================
+//	
+//	Copyright (c) 2014-
+//	Authors:
+//	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package acceptance;
+
+/**
+ * An omega-regular acceptance type.
+ */
+public enum AcceptanceType {
+	RABIN,
+ 	STREETT;
+
+	/**
+	 * Check whether an array of AcceptanceTypes contains a specific element.
+	 * @param types the array of AcceptanceTypes
+	 * @param type the AcceptanceType that is tested for
+	 */
+	public static boolean contains(AcceptanceType[] types, AcceptanceType type)
+	{
+		for (AcceptanceType t: types) {
+			if (t.equals(type))
+				return true;
+		}
+		return false;
+	}
+}