Some utility methods for dealing with DRAs that are actually DBAs (or DFAs).

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

prism/src/prism/DRA.java

@@ -196,6 +196,20 @@ public class DRA<Symbol>
 		return acceptanceK.get(i);
 	}
 
+	/**
+	 * Is this Rabin automaton actually a Buchi automaton? This check is done syntactically:
+	 * it returns true if L_i is empty for any acceptance paairs (L_i,K_i).
+	 */
+	public boolean isDBA()
+	{
+		int n = getNumAcceptancePairs();
+		for (int i = 0; i < n; i++) {
+			if (!getAcceptanceL(i).isEmpty())
+				return false;
+		}
+		return true;
+	}
+	
 	/**
 	 * Print DRA in DOT format to an output stream.
 	 */

prism/src/prism/LTLModelChecker.java

@@ -664,6 +664,27 @@ public class LTLModelChecker extends PrismComponent
 		return statesKi;
 	}
 
+	/**
+	 * Find the set of states in a model corresponding to the "target" part of a Rabin acceptance condition,
+	 * i.e. just the union of the K_i parts of the (L_i,K_i) pairs.  
+	 * @param dra The DRA storing the Rabin acceptance condition
+	 * @param model The model
+	 * @param draDDRowVars BDD row variables for the DRA part of the model
+	 * @param draDDColVars BDD column variables for the DRA part of the model
+	 * @return
+	 */
+	public JDDNode findTargetStatesForRabin(DRA<BitSet> dra, Model model, JDDVars draDDRowVars, JDDVars draDDColVars)
+	{
+		JDDNode acceptingStates = JDD.Constant(0);
+		for (int i = 0; i < dra.getNumAcceptancePairs(); i++) {
+			JDDNode tmpK = buildKStatesForRabinPair(draDDRowVars, dra, i);
+			acceptingStates = JDD.Or(acceptingStates, tmpK);
+		}
+		JDD.Ref(model.getReach());
+		acceptingStates = JDD.And(model.getReach(), acceptingStates);
+		return acceptingStates;
+	}
+	
 	/**
 	 * Find the set of accepting BSCCs in a model wrt a Rabin acceptance condition.
 	 * @param dra The DRA storing the Rabin acceptance condition