From db8bfe65c4ff5309eaaadfa760076dd8c11e01b9 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Fri, 19 Dec 2014 10:47:26 +0000
Subject: [PATCH] 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             | 14 ++++++++++++++
 prism/src/prism/LTLModelChecker.java | 21 +++++++++++++++++++++
 2 files changed, 35 insertions(+)

diff --git a/prism/src/prism/DRA.java b/prism/src/prism/DRA.java
index 5a65fa75..604879df 100644
--- a/prism/src/prism/DRA.java
+++ b/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.
 	 */
diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java
index a204a2ff..23dc30dc 100644
--- a/prism/src/prism/LTLModelChecker.java
+++ b/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