symbolic acceptance: provide toAcceptanceGeneric() conversion, methods for complementing [with Steffen Maercker]

Similar to the explicit variants.

Deprecates old complement() methods in AcceptanceRabinDD, AcceptanceStreettDD.


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

prism/src/acceptance/AcceptanceBuchiDD.java

@@ -31,6 +31,7 @@ import common.IterableBitSet;
 import jdd.JDD;
 import jdd.JDDNode;
 import jdd.JDDVars;
+import prism.PrismNotSupportedException;
 
 /**
  * A Büchi acceptance condition (based on JDD state sets).
@@ -110,6 +111,64 @@ public class AcceptanceBuchiDD implements AcceptanceOmegaDD
 		return AcceptanceType.BUCHI;
 	}
 
+	/**
+	 * Get the Streett acceptance condition that is the equivalent of this Buchi condition.
+	 */
+	public AcceptanceStreettDD toStreett()
+	{
+		AcceptanceStreettDD streett = new AcceptanceStreettDD();
+		streett.add(new AcceptanceStreettDD.StreettPairDD(JDD.Constant(1), acceptingStates.copy()));
+		return streett;
+	}
+
+	@Override
+	public AcceptanceOmegaDD complement(AcceptanceType... allowedAcceptance) throws PrismNotSupportedException
+	{
+		if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.RABIN)) {
+			return complementToRabin();
+		} else if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.STREETT)) {
+			return complementToStreett();
+		} else if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.GENERIC)) {
+			return complementToGeneric();
+		}
+		throw new PrismNotSupportedException("Can not complement " + getType() + " acceptance to a supported acceptance type");
+	}
+
+	/**
+	 * Get a Rabin acceptance condition that is the complement of this 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 complementToRabin()
+	{
+		AcceptanceRabinDD rabin = new AcceptanceRabinDD();
+		rabin.add(new AcceptanceRabinDD.RabinPairDD(acceptingStates.copy(), JDD.Constant(1)));
+		return rabin;
+	}
+
+	/**
+	 * Get a Streett acceptance condition that is the complement of this condition, i.e.,
+	 * any word that is accepted by this condition is rejected by the returned Streett condition.
+	 * <br>
+	 * Relies on the fact that once the goal states have been reached, all subsequent states
+	 * are goal states.
+	 *
+	 * @return the complement Streett acceptance condition
+	 */
+	public AcceptanceStreettDD complementToStreett()
+	{
+		AcceptanceStreettDD streett = new AcceptanceStreettDD();
+		streett.add(new AcceptanceStreettDD.StreettPairDD(acceptingStates.copy(), JDD.Constant(0)));
+		return streett;
+	}
+
+	@Override
+	public AcceptanceGenericDD toAcceptanceGeneric()
+	{
+		return new AcceptanceGenericDD(AcceptanceGeneric.ElementType.INF, acceptingStates.copy());
+	}
+
 	@Override
 	@Deprecated
 	public String getTypeAbbreviated()

prism/src/acceptance/AcceptanceGenRabinDD.java

@@ -30,10 +30,10 @@ package acceptance;
 import java.util.ArrayList;
 
 import common.IterableBitSet;
-
 import jdd.JDD;
 import jdd.JDDNode;
 import jdd.JDDVars;
+import prism.PrismNotSupportedException;
 
 /**
  * A Generalized Rabin acceptance condition (based on JDD state sets)
@@ -135,6 +135,24 @@ public class AcceptanceGenRabinDD
 			return true;
 		}
 
+		public AcceptanceGenericDD toAcceptanceGeneric()
+ 		{
+			AcceptanceGenericDD genericL = new AcceptanceGenericDD(AcceptanceGeneric.ElementType.FIN, L.copy());
+			if (getNumK() == 0) {
+				return genericL;
+			}
+			AcceptanceGenericDD genericKs = null;
+			for (JDDNode K : K_list) {
+				AcceptanceGenericDD genericK = new AcceptanceGenericDD(AcceptanceGeneric.ElementType.INF, K.copy());
+				if (genericKs == null) {
+					genericKs = genericK;
+				} else {
+					genericKs = new AcceptanceGenericDD(AcceptanceGeneric.ElementType.AND, genericKs, genericK);
+				}
+			}
+			return new AcceptanceGenericDD(AcceptanceGeneric.ElementType.AND, genericL, genericKs);
+ 		}
+
 		/** Returns a textual representation of this Rabin pair. */
 		@Override
 		public String toString()
@@ -235,6 +253,33 @@ public class AcceptanceGenRabinDD
 		return AcceptanceType.GENERALIZED_RABIN;
 	}
 
+	@Override
+	public AcceptanceOmegaDD complement(AcceptanceType... allowedAcceptance) throws PrismNotSupportedException
+	{
+		if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.GENERIC)) {
+			return complementToGeneric();
+		}
+		throw new PrismNotSupportedException("Can not complement " + getType() + " acceptance to a supported acceptance type");
+	}
+
+	@Override
+	public AcceptanceGenericDD toAcceptanceGeneric()
+	{
+		if (size() == 0) {
+			return new AcceptanceGenericDD(false);
+		}
+		AcceptanceGenericDD genericPairs = null;
+		for (GenRabinPairDD pair : this) {
+			AcceptanceGenericDD genericPair = pair.toAcceptanceGeneric();
+			if (genericPairs == null) {
+				genericPairs = genericPair;
+			} else {
+				genericPairs = new AcceptanceGenericDD(AcceptanceGeneric.ElementType.OR, genericPairs, genericPair);
+			}
+		}
+		return genericPairs;
+	}
+
 	@Override
 	@Deprecated
 	public String getTypeAbbreviated() {

prism/src/acceptance/AcceptanceGenericDD.java

@@ -32,6 +32,7 @@ import acceptance.AcceptanceGeneric.ElementType;
 import jdd.JDD;
 import jdd.JDDNode;
 import jdd.JDDVars;
+import prism.PrismNotSupportedException;
 
 /**
  * A generic acceptance condition (based on JDD state sets).
@@ -206,6 +207,54 @@ public class AcceptanceGenericDD implements AcceptanceOmegaDD {
 		return AcceptanceType.GENERIC;
 	}
 
+	@Override
+	public AcceptanceOmegaDD complement(AcceptanceType... allowedAcceptance) throws PrismNotSupportedException
+	{
+		if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.GENERIC)) {
+			return this.complementToGeneric();
+		}
+		throw new PrismNotSupportedException("Can not complement " + getType() + " acceptance to required acceptance type");
+	}
+
+	/** Complement this acceptance condition, return as AcceptanceGeneric. */
+	@Override
+	public AcceptanceGenericDD complementToGeneric()
+	{
+		// overrides the default implementation in AcceptanceOmegaDD, as it's the base case
+		// that is used there
+
+		switch (kind) {
+		case TRUE:
+			return new AcceptanceGenericDD(false);
+		case FALSE:
+			return new AcceptanceGenericDD(true);
+		case AND:
+			return new AcceptanceGenericDD(ElementType.OR,
+			                               getLeft().complementToGeneric(),
+			                               getRight().complementToGeneric());
+		case OR:
+			return new AcceptanceGenericDD(ElementType.AND,
+			                               getLeft().complementToGeneric(),
+			                               getRight().complementToGeneric());
+		case FIN:
+			return new AcceptanceGenericDD(ElementType.INF, states.copy());
+		case FIN_NOT:
+			return new AcceptanceGenericDD(ElementType.INF_NOT, states.copy());
+		case INF:
+			return new AcceptanceGenericDD(ElementType.FIN, states.copy());
+		case INF_NOT:
+			return new AcceptanceGenericDD(ElementType.FIN_NOT, states.copy());
+		default:
+			throw new UnsupportedOperationException();
+		}
+	}
+
+	@Override
+	public AcceptanceGenericDD toAcceptanceGeneric()
+	{
+		return this.clone();
+	}
+
 	@Override
 	@Deprecated
 	public String getTypeAbbreviated() {

prism/src/acceptance/AcceptanceOmegaDD.java

@@ -27,6 +27,8 @@
 package acceptance;
 
 import jdd.JDDNode;
+import prism.PrismException;
+import prism.PrismNotSupportedException;
 
 /**
  * Generic interface for an omega-regular acceptance condition (BDD-based).
@@ -54,6 +56,36 @@ public interface AcceptanceOmegaDD extends Cloneable
 	/** Returns the AcceptanceType of this acceptance condition */
 	public AcceptanceType getType();
 
+	/**
+	 * Complement the acceptance condition if possible.
+	 * <br>
+	 * [ REFS: <i>result</i>, DEREFS: <i>none</i> ]
+	 * @param allowedAcceptance the allowed acceptance types that may be used for complementing
+	 * @throws PrismNotSupportedException if none of the allowed acceptance types can be used as target for complementing
+	 */
+	public AcceptanceOmegaDD complement(AcceptanceType... allowedAcceptance) throws PrismNotSupportedException;
+
+	/**
+	 * Complement this acceptance condition to an AcceptanceGeneric condition.
+	 * <br>
+	 * Default implementation: toAcceptanceGeneric().complementToGeneric()
+	 * [ REFS: <i>result</i>, DEREFS: <i>none</i> ]
+	 */
+	public default AcceptanceGenericDD complementToGeneric()
+	{
+		AcceptanceGenericDD generic = this.toAcceptanceGeneric();
+		AcceptanceGenericDD complemented = generic.complementToGeneric();
+		generic.clear();
+		return complemented;
+	}
+
+	/**
+	 * Convert this acceptance condition to an AcceptanceGeneric condition.
+	 * <br>
+	 * [ REFS: <i>result</i>, DEREFS: <i>none</i> ]
+	 */
+	public AcceptanceGenericDD toAcceptanceGeneric();
+
 	/** Returns the type of this acceptance condition as a String,
 	 * i.e., "R" for Rabin
 	 */

prism/src/acceptance/AcceptanceRabinDD.java

@@ -32,6 +32,7 @@ import common.IterableBitSet;
 import jdd.JDD;
 import jdd.JDDNode;
 import jdd.JDDVars;
+import prism.PrismNotSupportedException;
 
 /**
  * A Rabin acceptance condition (based on JDD state sets)
@@ -119,6 +120,16 @@ public class AcceptanceRabinDD
 			return false;
 		}
 
+		public AcceptanceGenericDD toAcceptanceGeneric()
+ 		{
+			AcceptanceGenericDD genericL = new AcceptanceGenericDD(AcceptanceGeneric.ElementType.FIN, getL());
+			AcceptanceGenericDD genericK = new AcceptanceGenericDD(AcceptanceGeneric.ElementType.INF, getK());
+
+			//      F G ! "L" & G F "K"
+			// <=>  Fin(L) & Inf(K)
+			return new AcceptanceGenericDD(AcceptanceGeneric.ElementType.AND, genericL, genericK);
+ 		}
+
 		/** Returns a textual representation of this Rabin pair. */
 		@Override
 		public String toString()
@@ -181,19 +192,14 @@ public class AcceptanceRabinDD
 	/**
 	 * 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.
+	 * <br>
+	 * Deprecated, use complementToStreett() or complement(...)
 	 * @return the complement Streett acceptance condition
 	 */
+	@Deprecated
 	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;
+		return complementToStreett();
 	}
 
 	/**
@@ -247,6 +253,55 @@ public class AcceptanceRabinDD
 		return AcceptanceType.RABIN;
 	}
 
+	@Override
+	public AcceptanceOmegaDD complement(AcceptanceType... allowedAcceptance) throws PrismNotSupportedException
+	{
+		if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.STREETT)) {
+			return complementToStreett();
+		}
+		if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.GENERIC)) {
+			return complementToGeneric();
+		}
+		throw new PrismNotSupportedException("Can not complement " + getType() + " acceptance to a supported acceptance type");
+	}
+
+	/**
+	 * 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 complementToStreett()
+	{
+		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;
+	}
+
+	@Override
+	public AcceptanceGenericDD toAcceptanceGeneric()
+	{
+		if (size() == 0) {
+			return new AcceptanceGenericDD(false);
+		}
+		AcceptanceGenericDD genericPairs = null;
+		for (RabinPairDD pair : this) {
+			AcceptanceGenericDD genericPair = pair.toAcceptanceGeneric();
+			if (genericPairs == null) {
+				genericPairs = genericPair;
+			} else {
+				genericPairs = new AcceptanceGenericDD(AcceptanceGeneric.ElementType.OR, genericPairs, genericPair);
+			}
+		}
+		return genericPairs;
+	}
+
 	@Override
 	@Deprecated
 	public String getTypeAbbreviated() {

prism/src/acceptance/AcceptanceReachDD.java

@@ -31,6 +31,7 @@ import common.IterableBitSet;
 import jdd.JDD;
 import jdd.JDDNode;
 import jdd.JDDVars;
+import prism.PrismNotSupportedException;
 
 /**
  * A reachability acceptance condition (based on JDD state sets).
@@ -110,6 +111,57 @@ public class AcceptanceReachDD implements AcceptanceOmegaDD
 		return AcceptanceType.REACH;
 	}
 
+	@Override
+	public AcceptanceOmegaDD complement(AcceptanceType... allowedAcceptance) throws PrismNotSupportedException
+	{
+		if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.RABIN)) {
+			return complementToRabin();
+		} else if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.STREETT)) {
+			return complementToStreett();
+		} else if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.GENERIC)) {
+			return complementToGeneric();
+		}
+		throw new PrismNotSupportedException("Can not complement " + getType() + " acceptance to a supported acceptance type");
+	}
+
+	/**
+	 * Get a Rabin acceptance condition that is the complement of this condition, i.e.,
+	 * any word that is accepted by this condition is rejected by the returned Rabin condition.
+	 * <br>
+	 * Relies on the fact that once the goal states have been reached, all subsequent states
+	 * are goal states.
+	 *
+	 * @return the complement Rabin acceptance condition
+	 */
+	public AcceptanceRabinDD complementToRabin()
+	{
+		AcceptanceRabinDD rabin = new AcceptanceRabinDD();
+		rabin.add(new AcceptanceRabinDD.RabinPairDD(goalStates.copy(), JDD.Constant(1)));
+		return rabin;
+	}
+
+	/**
+	 * Get a Streett acceptance condition that is the complement of this condition, i.e.,
+	 * any word that is accepted by this condition is rejected by the returned Streett condition.
+	 * <br>
+	 * Relies on the fact that once the goal states have been reached, all subsequent states
+	 * are goal states.
+	 *
+	 * @return the complement Streett acceptance condition
+	 */
+	public AcceptanceStreettDD complementToStreett()
+	{
+		AcceptanceStreettDD streett = new AcceptanceStreettDD();
+		streett.add(new AcceptanceStreettDD.StreettPairDD(goalStates.copy(), JDD.Constant(0)));
+		return streett;
+	}
+
+	@Override
+	public AcceptanceGenericDD toAcceptanceGeneric()
+	{
+		return new AcceptanceGenericDD(AcceptanceGeneric.ElementType.INF, goalStates.copy());
+	}
+
 	@Override
 	@Deprecated
 	public String getTypeAbbreviated() {

prism/src/acceptance/AcceptanceStreettDD.java

@@ -29,10 +29,10 @@ package acceptance;
 import java.util.ArrayList;
 
 import common.IterableBitSet;
-
 import jdd.JDD;
 import jdd.JDDNode;
 import jdd.JDDVars;
+import prism.PrismNotSupportedException;
 
 /**
  * A Streett acceptance condition (based on JDD state sets).
@@ -121,6 +121,17 @@ public class AcceptanceStreettDD
 			}
 		}
 
+		public AcceptanceGenericDD toAcceptanceGeneric()
+		{
+		    AcceptanceGenericDD genericR = new AcceptanceGenericDD(AcceptanceGeneric.ElementType.FIN, getR());
+		    AcceptanceGenericDD genericG = new AcceptanceGenericDD(AcceptanceGeneric.ElementType.INF, getG());
+		    //      G F "R" -> G F "G"
+		    // <=>  ! G F "R"  | G F "G"
+		    // <=>  F G ! "R"  | G F "G"
+		    // <=>  Fin(R) | Inf(G)
+		    return new AcceptanceGenericDD(AcceptanceGeneric.ElementType.OR, genericR, genericG);
+                }
+
 		@Override
 		public String toString()
 		{
@@ -211,19 +222,14 @@ public class AcceptanceStreettDD
 	/**
 	 * 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.
+	 * <br>
+	 * Deprecated, use complementToRabin or complement(...).
 	 * @return the complement Rabin acceptance condition
 	 */
+	@Deprecated
 	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;
+		return complementToRabin();
 	}
 
 	@Override
@@ -247,6 +253,49 @@ public class AcceptanceStreettDD
 		return AcceptanceType.STREETT;
 	}
 
+	@Override
+	public AcceptanceOmegaDD complement(AcceptanceType... allowedAcceptance) throws PrismNotSupportedException
+	{
+		if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.RABIN)) {
+			return complementToRabin();
+		}
+		if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.GENERIC)) {
+			return complementToGeneric();
+		}
+		throw new PrismNotSupportedException("Can not complement " + getType() + " acceptance to a supported acceptance type");
+	}
+
+	public AcceptanceRabinDD complementToRabin()
+	{
+		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 AcceptanceGenericDD toAcceptanceGeneric()
+	{
+		if (size() == 0) {
+			return new AcceptanceGenericDD(true);
+		}
+		AcceptanceGenericDD genericPairs = null;
+		for (StreettPairDD pair : this) {
+			AcceptanceGenericDD genericPair = pair.toAcceptanceGeneric();
+			if (genericPairs == null) {
+				genericPairs = genericPair;
+			} else {
+				genericPairs = new AcceptanceGenericDD(AcceptanceGeneric.ElementType.AND, genericPairs, genericPair);
+			}
+		}
+		return genericPairs;
+	}
+
 	@Override
 	@Deprecated
 	public String getTypeAbbreviated() {