symbolic acceptance: make cloneable [with Steffen Maercker]

Similar to the explicit variants.


git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12038 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/acceptance/AcceptanceBuchiDD.java

@@ -92,6 +92,12 @@ public class AcceptanceBuchiDD implements AcceptanceOmegaDD
 		return JDD.AreIntersecting(acceptingStates, bscc_states);
 	}
 
+	@Override
+	public AcceptanceBuchiDD clone()
+	{
+		return new AcceptanceBuchiDD(acceptingStates.copy());
+	}
+
 	@Override
 	public String getSizeStatistics()
 	{

prism/src/acceptance/AcceptanceGenRabinDD.java

@@ -55,7 +55,7 @@ public class AcceptanceGenRabinDD
 	 * A pair in a Generalized Rabin acceptance condition, i.e., with
 	 *  (F G !"L") & (G F "K_1") & ... & (G F "K_n").
 	 **/
-	public static class GenRabinPairDD {
+	public static class GenRabinPairDD implements Cloneable {
 		/** State set L (should be visited only finitely often) */
 		private JDDNode L;
 
@@ -102,6 +102,16 @@ public class AcceptanceGenRabinDD
 			return K_list.get(j).copy();
 		}
 
+		@Override
+		public GenRabinPairDD clone()
+		{
+			ArrayList<JDDNode> newK_list = new ArrayList<JDDNode>();
+			for (JDDNode K_j : K_list) {
+				newK_list.add(K_j.copy());
+			}
+			return new GenRabinPairDD(getL(), newK_list);
+		}
+
 		/** 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> ]
@@ -183,6 +193,16 @@ public class AcceptanceGenRabinDD
 		return false;
 	}
 
+	@Override
+	public AcceptanceGenRabinDD clone()
+	{
+		AcceptanceGenRabinDD result = new AcceptanceGenRabinDD();
+		for (GenRabinPairDD pair : this) {
+			result.add(pair.clone());
+		}
+		return result;
+	}
+
 	@Override
 	public void clear()
 	{

prism/src/acceptance/AcceptanceGenericDD.java

@@ -175,6 +175,27 @@ public class AcceptanceGenericDD implements AcceptanceOmegaDD {
 		throw new UnsupportedOperationException("Unsupported operator in generic acceptance expression");
 	}
 
+	@Override
+	public AcceptanceGenericDD clone()
+	{
+		switch(kind) {
+		case TRUE:
+			return new AcceptanceGenericDD(true);
+		case FALSE:
+			return new AcceptanceGenericDD(false);
+		case AND:
+			return new AcceptanceGenericDD(ElementType.AND, left.clone(), right.clone());
+		case OR:
+			return new AcceptanceGenericDD(ElementType.OR, left.clone(), right.clone());
+		case INF:
+		case INF_NOT:
+		case FIN:
+		case FIN_NOT:
+			return new AcceptanceGenericDD(kind, states.copy());
+		}
+		throw new UnsupportedOperationException("Unsupported operatator in generic acceptance condition");
+	}
+
 	@Override
 	public String getSizeStatistics() {
 		return "generic acceptance with " + countAcceptanceSets() + " acceptance sets";

prism/src/acceptance/AcceptanceOmegaDD.java

@@ -31,7 +31,7 @@ import jdd.JDDNode;
 /**
  * Generic interface for an omega-regular acceptance condition (BDD-based).
  */
-public interface AcceptanceOmegaDD
+public interface AcceptanceOmegaDD extends Cloneable
 {
 	/** Returns true if the bottom strongly connected component (BSSC)
 	 *  given by bscc_states is accepting for this acceptance condition.
@@ -39,6 +39,12 @@ public interface AcceptanceOmegaDD
 	 **/
 	public boolean isBSCCAccepting(JDDNode bscc_states);
 
+	/**
+	 * Provides a copy of this acceptance condition.
+	 * <br>[ REFS: <i>result</i>, DEREFS: <i>none</i> ]
+	 */
+	public AcceptanceOmegaDD clone();
+
 	/**
 	 * Get a string describing the acceptance condition's size,
 	 * i.e. "x Rabin pairs", etc.

prism/src/acceptance/AcceptanceRabinDD.java

@@ -168,6 +168,16 @@ public class AcceptanceRabinDD
 		return false;
 	}
 
+	@Override
+	public AcceptanceRabinDD clone()
+	{
+		AcceptanceRabinDD result = new AcceptanceRabinDD();
+		for (RabinPairDD pair : this) {
+			result.add(pair.clone());
+		}
+		return result;
+	}
+
 	/**
 	 * 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.

prism/src/acceptance/AcceptanceReachDD.java

@@ -92,6 +92,12 @@ public class AcceptanceReachDD implements AcceptanceOmegaDD
 		return JDD.AreIntersecting(goalStates, bscc_states);
 	}
 
+	@Override
+	public AcceptanceReachDD clone()
+	{
+		return new AcceptanceReachDD(goalStates.copy());
+	}
+
 	@Override
 	public String getSizeStatistics()
 	{

prism/src/acceptance/AcceptanceStreettDD.java

@@ -169,6 +169,17 @@ public class AcceptanceStreettDD
 		return true;
 	}
 
+	@Override
+	public AcceptanceStreettDD clone()
+	{
+		AcceptanceStreettDD result = new AcceptanceStreettDD();
+		for (StreettPairDD pair : this) {
+			result.add(pair.clone());
+		}
+		return result;
+	}
+
+
 	@Override
 	public void clear()
 	{