diff --git a/prism/src/acceptance/AcceptanceBuchiDD.java b/prism/src/acceptance/AcceptanceBuchiDD.java
index cf9426db..d94be344 100644
--- a/prism/src/acceptance/AcceptanceBuchiDD.java
+++ b/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.
+ *
+ * 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()
diff --git a/prism/src/acceptance/AcceptanceGenRabinDD.java b/prism/src/acceptance/AcceptanceGenRabinDD.java
index 5c1191a3..194d241d 100644
--- a/prism/src/acceptance/AcceptanceGenRabinDD.java
+++ b/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() {
diff --git a/prism/src/acceptance/AcceptanceGenericDD.java b/prism/src/acceptance/AcceptanceGenericDD.java
index 1bcc6620..418208c5 100644
--- a/prism/src/acceptance/AcceptanceGenericDD.java
+++ b/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() {
diff --git a/prism/src/acceptance/AcceptanceOmegaDD.java b/prism/src/acceptance/AcceptanceOmegaDD.java
index fb07278d..0005a4e3 100644
--- a/prism/src/acceptance/AcceptanceOmegaDD.java
+++ b/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.
+ *
+ * [ REFS: result, DEREFS: none ]
+ * @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.
+ *
+ * Default implementation: toAcceptanceGeneric().complementToGeneric()
+ * [ REFS: result, DEREFS: none ]
+ */
+ public default AcceptanceGenericDD complementToGeneric()
+ {
+ AcceptanceGenericDD generic = this.toAcceptanceGeneric();
+ AcceptanceGenericDD complemented = generic.complementToGeneric();
+ generic.clear();
+ return complemented;
+ }
+
+ /**
+ * Convert this acceptance condition to an AcceptanceGeneric condition.
+ *
+ * [ REFS: result, DEREFS: none ]
+ */
+ public AcceptanceGenericDD toAcceptanceGeneric();
+
/** Returns the type of this acceptance condition as a String,
* i.e., "R" for Rabin
*/
diff --git a/prism/src/acceptance/AcceptanceRabinDD.java b/prism/src/acceptance/AcceptanceRabinDD.java
index 7db327d5..8fb51204 100644
--- a/prism/src/acceptance/AcceptanceRabinDD.java
+++ b/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.
+ *
+ * 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() {
diff --git a/prism/src/acceptance/AcceptanceReachDD.java b/prism/src/acceptance/AcceptanceReachDD.java
index 63e3dc60..e80b2333 100644
--- a/prism/src/acceptance/AcceptanceReachDD.java
+++ b/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.
+ *
+ * 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.
+ *
+ * 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() {
diff --git a/prism/src/acceptance/AcceptanceStreettDD.java b/prism/src/acceptance/AcceptanceStreettDD.java
index e0e8fa6b..8c2f9cc2 100644
--- a/prism/src/acceptance/AcceptanceStreettDD.java
+++ b/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.
+ *
+ * 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() {