Acceptance: add complement functionality, some more comments

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

prism/src/acceptance/AcceptanceGenRabin.java

@@ -30,6 +30,8 @@ package acceptance;
 import java.util.ArrayList;
 import java.util.BitSet;
 
+import prism.PrismException;
+import prism.PrismNotSupportedException;
 import jdd.JDDVars;
 
 /**
@@ -188,6 +190,22 @@ public class AcceptanceGenRabin
 		return false;
 	}
 
+	/** Complement this acceptance condition, return as AcceptanceGeneric. */
+	public AcceptanceGeneric complementToGeneric()
+	{
+		AcceptanceGeneric generic = toAcceptanceGeneric();
+		return generic.complementToGeneric();
+	}
+
+	@Override
+	public AcceptanceOmega complement(int numStates, AcceptanceType... allowedAcceptance) throws PrismException
+	{
+		if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.GENERIC)) {
+			return complementToGeneric();
+		}
+		throw new PrismNotSupportedException("Can not complement " + getTypeName() + " acceptance to a supported acceptance type");
+	}
+
 	@Override
 	public void lift(LiftBitSet lifter) {
 		for (GenRabinPair pair : this) {

prism/src/acceptance/AcceptanceGeneric.java

@@ -29,6 +29,8 @@ package acceptance;
 
 import java.util.BitSet;
 
+import prism.PrismException;
+import prism.PrismNotSupportedException;
 import jdd.JDDVars;
 
 /**
@@ -198,6 +200,43 @@ public class AcceptanceGeneric implements AcceptanceOmega {
 		throw new UnsupportedOperationException("Unsupported operator in generic acceptance condition");
 	}
 
+	/** Complement this acceptance condition, return as AcceptanceGeneric. */
+	public AcceptanceGeneric complementToGeneric()
+	{
+		switch (kind) {
+		case TRUE: return new AcceptanceGeneric(false);
+		case FALSE:  return new AcceptanceGeneric(true);
+
+		case AND:
+			return new AcceptanceGeneric(ElementType.OR,
+			                             getLeft().complementToGeneric(),
+			                             getRight().complementToGeneric());
+		case OR:
+			return new AcceptanceGeneric(ElementType.AND,
+                        	             getLeft().complementToGeneric(),
+                        	             getRight().complementToGeneric());
+		case FIN:
+			return new AcceptanceGeneric(ElementType.INF, (BitSet) states.clone());
+		case FIN_NOT:
+			return new AcceptanceGeneric(ElementType.INF_NOT, (BitSet) states.clone());
+		case INF:
+			return new AcceptanceGeneric(ElementType.FIN, (BitSet) states.clone());
+		case INF_NOT:
+			return new AcceptanceGeneric(ElementType.FIN_NOT, (BitSet) states.clone());
+		default:
+			throw new UnsupportedOperationException();
+		}
+	}
+
+	@Override
+	public AcceptanceOmega complement(int numStates, AcceptanceType... allowedAcceptance) throws PrismException
+	{
+		if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.GENERIC)) {
+			return this.complementToGeneric();
+		}
+		throw new PrismNotSupportedException("Can not complement " + getTypeName() + " acceptance to required acceptance type");
+	}
+
 	@Override
 	public void lift(LiftBitSet lifter) {
 		switch(kind) {
@@ -272,4 +311,5 @@ public class AcceptanceGeneric implements AcceptanceOmega {
 		}
 	}
 
+
 }

prism/src/acceptance/AcceptanceOmega.java

@@ -28,6 +28,7 @@ package acceptance;
 
 import java.util.BitSet;
 
+import prism.PrismException;
 import jdd.JDDVars;
 
 /**
@@ -64,6 +65,13 @@ public interface AcceptanceOmega extends Cloneable
 	/** Make a copy of the acceptance condition. */
 	public AcceptanceOmega clone();
 
+	/**
+	 * Complement the acceptance condition if possible.
+	 * @param numStates the number of states in the underlying model / automaton (needed for complementing BitSets)
+	 * @param allowedAcceptance the allowed acceptance types that may be used for complementing
+	 */
+	public AcceptanceOmega complement(int numStates, AcceptanceType... allowedAcceptance) throws PrismException;
+
 	/** Abstract functor for use with the lift function. */
 	public static abstract class LiftBitSet {
 		public abstract BitSet lift(BitSet states);

prism/src/acceptance/AcceptanceRabin.java

@@ -29,6 +29,8 @@ package acceptance;
 import java.util.ArrayList;
 import java.util.BitSet;
 
+import prism.PrismException;
+import prism.PrismNotSupportedException;
 import jdd.JDDVars;
 
 /**
@@ -58,7 +60,10 @@ public class AcceptanceRabin
 		/** State set K (should be visited infinitely often) */
 		private BitSet K;
 
-		/** Constructor with L and K state sets */
+		/**
+		 * Constructor with L and K state sets.
+		 *  (F G !"L")  &  (G F "K")
+		 */
 		public RabinPair(BitSet L, BitSet K) {
 			this.L = L;
 			this.K = K;
@@ -175,7 +180,7 @@ public class AcceptanceRabin
 	 * any word that is accepted by this condition is rejected by the returned Streett condition.
 	 * @return the complement Streett acceptance condition
 	 */
-	public AcceptanceStreett complement()
+	public AcceptanceStreett complementToStreett()
 	{
 		AcceptanceStreett accRabin = new AcceptanceStreett();
 
@@ -189,6 +194,15 @@ public class AcceptanceRabin
 		return accRabin;
 	}
 
+	@Override
+	public AcceptanceOmega complement(int numStates, AcceptanceType... allowedAcceptance) throws PrismException
+	{
+		if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.STREETT)) {
+			return complementToStreett();
+		}
+		throw new PrismNotSupportedException("Can not complement " + getTypeName() + " acceptance to a supported acceptance type");
+	}
+
 	/**
 	 * 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.,

prism/src/acceptance/AcceptanceReach.java

@@ -28,6 +28,8 @@ package acceptance;
 
 import java.util.BitSet;
 
+import prism.PrismException;
+import prism.PrismNotSupportedException;
 import jdd.JDDVars;
 
 /**
@@ -76,6 +78,54 @@ public class AcceptanceReach implements AcceptanceOmega
 		return bscc_states.intersects(goalStates);
 	}
 
+	/**
+	 * 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.
+	 *
+	 * @param numStates the number of states in the underlying model / automaton (needed for complementing BitSets)
+	 * @return the complement Rabin acceptance condition
+	 */
+	public AcceptanceRabin complementToRabin(int numStates)
+	{
+		AcceptanceRabin rabin = new AcceptanceRabin();
+		BitSet allStates = new BitSet();
+		allStates.set(0, numStates-1);
+		rabin.add(new AcceptanceRabin.RabinPair((BitSet) goalStates.clone(), allStates));
+		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.
+	 *
+	 * @param numStates the number of states in the underlying model / automaton (needed for complementing BitSets)
+	 * @return the complement Streett acceptance condition
+	 */
+	public AcceptanceStreett complementToStreett(int numStates)
+	{
+		AcceptanceStreett streett = new AcceptanceStreett();
+		streett.add(new AcceptanceStreett.StreettPair((BitSet) goalStates.clone(), new BitSet()));
+		return streett;
+	}
+
+	@Override
+	public AcceptanceOmega complement(int numStates, AcceptanceType... allowedAcceptance) throws PrismException
+	{
+		if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.RABIN)) {
+			return complementToRabin(numStates);
+		} else if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.STREETT)) {
+			return complementToStreett(numStates);
+		} else if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.GENERIC)) {
+			return new AcceptanceGeneric(AcceptanceGeneric.ElementType.FIN, (BitSet) goalStates.clone());
+		}
+		throw new PrismNotSupportedException("Can not complement " + getTypeName() + " acceptance to a supported acceptance type");
+	}
 
 	@Override
 	public void lift(LiftBitSet lifter)

prism/src/acceptance/AcceptanceStreett.java

@@ -29,6 +29,8 @@ package acceptance;
 import java.util.ArrayList;
 import java.util.BitSet;
 
+import prism.PrismException;
+import prism.PrismNotSupportedException;
 import jdd.JDDVars;
 
 /**
@@ -58,7 +60,10 @@ public class AcceptanceStreett
 		/** State set G */
 		private BitSet G;
 
-		/** Constructor with R and G state sets */
+		/**
+		 * Constructor with R and G state sets.
+		 * 	 (G F "R") -> (G F "G")
+		 */
 		public StreettPair(BitSet R, BitSet G)
 		{
 			this.R = R;
@@ -179,7 +184,7 @@ public class AcceptanceStreett
 	 * any word that is accepted by this condition is rejected by the returned Rabin condition.
 	 * @return the complement Rabin acceptance condition
 	 */
-	public AcceptanceRabin complement()
+	public AcceptanceRabin complementToRabin()
 	{
 		AcceptanceRabin accRabin = new AcceptanceRabin();
 
@@ -192,6 +197,16 @@ public class AcceptanceStreett
 		return accRabin;
 	}
 	
+	@Override
+	public AcceptanceOmega complement(int numStates, AcceptanceType... allowedAcceptance) throws PrismException
+	{
+		if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.RABIN)) {
+			return complementToRabin();
+		}
+		throw new PrismNotSupportedException("Can not complement " + getTypeName() + " acceptance to a supported acceptance type");
+	}
+
+
 	/**
 	 * 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.,