Merge prism-hoaf branch back into trunk.

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

prism/.classpath

@@ -5,6 +5,7 @@
 	<classpathentry kind="lib" path="lib/epsgraphics.jar"/>
 	<classpathentry kind="lib" path="lib/jcommon.jar"/>
 	<classpathentry kind="lib" path="lib/jfreechart.jar" sourcepath="/jfreechart/source"/>
+	<classpathentry kind="lib" path="lib/jhoafparser-1.1.0-rc3.jar"/>
 	<classpathentry kind="lib" path="lib/colt.jar" sourcepath="/Users/dxp/colt/src"/>
 	<classpathentry kind="lib" path="lib/pepa.zip"/>
 	<classpathentry kind="lib" path="lib/lpsolve55j.jar"/>

prism/etc/scripts/hoa-ltl2dstar-with-ltl2ba-for-prism

@@ -0,0 +1,23 @@
+#! /bin/bash
+
+# Interface wrapper for calling ltl2dstar with ltl2ba as the LTL->NBA tool
+# Invoke from PRISM with
+#  -ltl2datool hoa-ltl2dstar-with-ltl2ba-for-prism -ltl2dasyntax lbt
+#
+# Expects ltl2dstar and ltl2ba executables on the PATH, otherwise
+# specify their location using
+#  export LTL2DSTAR=path/to/ltl2dstar
+#  export LTL2BA=path/to/ltl2ba
+
+
+# Take ltl2dstar executable from the LTL2DSTAR environment variable
+# Otherwise, default to "ltl2dstar", which will search the PATH
+LTL2DSTAR_BIN=${LTL2DSTAR-ltl2dstar}
+
+# Take the ltl2ba executable from the LTL2BA environment variable
+# Otherwise, default to "ltl2ba", which will search the PATH
+LTL2BA_BIN=${LTL2BA-ltl2ba}
+
+# --output=automaton = we want the automaton
+# --output-format=hoa = ... in HOA
+$LTL2DSTAR_BIN --output=automaton --output-format=hoa "--ltl2nba=spin:$LTL2BA_BIN" "$@"

prism/etc/scripts/hoa-ltl2dstar-with-ltl2tgba-for-prism

@@ -0,0 +1,25 @@
+#! /bin/bash
+
+# Interface wrapper for calling ltl2dstar with Spot's ltl2tgba as the LTL->NBA tool
+# Invoke from PRISM with
+#  -ltl2datool hoa-ltl2dstar-with-ltl2tgba-for-prism -ltl2dasyntax lbt
+#
+# Expects ltl2dstar and ltl2tgba executables on the PATH, otherwise
+# specify their location using
+#  export LTL2DSTAR=path/to/ltl2dstar
+#  export LTL2TGBA=path/to/ltl2tgba
+
+
+# Take ltl2dstar executable from the LTL2DSTAR environment variable
+# Otherwise, default to "ltl2dstar", which will search the PATH
+LTL2DSTAR_BIN=${LTL2DSTAR-ltl2dstar}
+
+# Take the ltl2tgba executable from the LTL2TGBA environment variable
+# Otherwise, default to "ltl2tgba", which will search the PATH
+LTL2TGBA_BIN=${LTL2TGBA-ltl2tgba}
+
+# --output=automaton = we want the automaton
+# --output-format=hoa = ... in HOA
+# --ltl2nba = with ltl2tgba as LTL->NBA
+#              -s -B = as Spin neverclaim, NBA output
+$LTL2DSTAR_BIN --output=automaton --output-format=hoa "--ltl2nba=spin:${LTL2TGBA_BIN}@-s -B" "$@"

prism/etc/scripts/hoa-ltl2dstar-with-ltl3ba-for-prism

@@ -0,0 +1,36 @@
+#! /bin/bash
+
+# Interface wrapper for calling ltl2dstar with ltl3ba as the LTL->NBA tool
+# Invoke from PRISM with
+#  -ltl2datool hoa-ltl2dstar-with-ltl3ba-for-prism -ltl2dasyntax lbt
+#
+# Expects ltl2dstar and ltl3ba executables on the PATH, otherwise
+# specify their location using
+#  export LTL2DSTAR=path/to/ltl2dstar
+#  export LTL3BA=path/to/ltl3ba
+#
+# If ltl3ba is not statically compiled, you can specify the path
+# to the Buddy library using
+#  export BUDDY_LIB=path/to/library-dir
+
+# Take ltl2dstar executable from the LTL2DSTAR environment variable
+# Otherwise, default to "ltl2dstar", which will search the PATH
+LTL2DSTAR_BIN=${LTL2DSTAR-ltl2dstar}
+
+# Take the ltl3ba executable from the LTL3BA environment variable
+# Otherwise, default to "ltl3ba", which will search the PATH
+LTL3BA_BIN=${LTL3BA-ltl3ba}
+
+# If BUDDY_LIB environment variable is set, add to appropriate path
+if [ ! -z "$BUDDY_LIB" ]; then
+    if [ "$(uname)" == "Darwin" ]; then
+	export DYLD_LIBRARY_PATH="$DYLD_LIBRARY_PATH":"$BUDDY_LIB"
+    else
+	export LD_LIBRARY_PATH="$DYLD_LIBRARY_PATH":"$BUDDY_LIB"
+    fi
+fi
+
+# --output=automaton = we want the automaton
+# --output-format=hoa = ... in HOA
+# --ltl2nba = with ltl3ba as LTL->NBA
+$LTL2DSTAR_BIN --output=automaton --output-format=hoa "--ltl2nba=spin:$LTL3BA_BIN" "$@"

prism/etc/scripts/hoa-ltl3dra-dra-for-prism

@@ -0,0 +1,30 @@
+#! /bin/bash
+
+# Interface wrapper for calling ltl3dra (state-based DRA)
+# Invoke from PRISM with
+#  -ltl2datool hoa-ltl3dra-dra-for-prism -ltl2dasyntax spin
+#
+# Expects the ltl3dra on the PATH, otherwise
+# specify its location using
+#  export LTL3DRA=path/to/ltl3dra
+#
+# Expects the dynamic buddy library to be in the library PATH, otherwise
+# specify its location using
+#  export BUDDY_LIB=path/to/buddy-lib-dir
+
+
+# Take ltl3dra executable from the LTL3DRA environment variable
+# Otherwise, default to "ltl3dra", which will search the PATH
+LTL3DRA_BIN=${LTL3DRA-ltl3dra}
+
+# If BUDDY_LIB environment variable is set, add to appropriate path
+if [ ! -z "$BUDDY_LIB" ]; then
+    if [ "$(uname)" == "Darwin" ]; then
+	export DYLD_LIBRARY_PATH="$DYLD_LIBRARY_PATH":"$BUDDY_LIB"
+    else
+	export LD_LIBRARY_PATH="$DYLD_LIBRARY_PATH":"$BUDDY_LIB"
+    fi
+fi
+
+# -H3 = output deterministic state-based Rabin in HOA format
+$LTL3DRA_BIN  -H3 -F "$1" > "$2"

prism/etc/scripts/hoa-ltl3dra-tgdra-for-prism

@@ -0,0 +1,30 @@
+#! /bin/bash
+
+# Interface wrapper for calling ltl3dra (transition-based DRA)
+# Invoke from PRISM with
+#  -ltl2datool hoa-ltl3dra-tgdra-for-prism -ltl2dasyntax spin
+#
+# Expects the ltl3dra on the PATH, otherwise
+# specify its location using
+#  export LTL3DRA=path/to/ltl3dra
+#
+# Expects the dynamic buddy library to be in the library PATH, otherwise
+# specify its location using
+#  export BUDDY_LIB=path/to/buddy-lib-dir
+
+
+# Take ltl3dra executable from the LTL3DRA environment variable
+# Otherwise, default to "ltl3dra", which will search the PATH
+LTL3DRA_BIN=${LTL3DRA-ltl3dra}
+
+# If BUDDY_LIB environment variable is set, add to appropriate path
+if [ ! -z "$BUDDY_LIB" ]; then
+    if [ "$(uname)" == "Darwin" ]; then
+	export DYLD_LIBRARY_PATH="$DYLD_LIBRARY_PATH":"$BUDDY_LIB"
+    else
+	export LD_LIBRARY_PATH="$DYLD_LIBRARY_PATH":"$BUDDY_LIB"
+    fi
+fi
+
+# -H2 = output deterministic transition-based Rabin in HOA format
+$LTL3DRA_BIN  -H2 -F "$1" > "$2"

prism/etc/scripts/hoa-rabinizer3-dgra-for-prism

@@ -0,0 +1,17 @@
+#! /bin/bash
+
+# Interface wrapper for calling Rabinizer3 (state-based DGRA)
+# Invoke from PRISM with
+#  -ltl2datool hoa-rabinizer3-dra-for-prism -ltl2dasyntax rabinizer
+#
+# Expects the rabinizer.jar file of Rabinizer3 in the current directory, otherwise
+# specify its location using
+#  export RABINIZER3=path/to/rabinizer.jar
+
+# Take location of the jar file from RABINIZER3 environment variable
+# Otherwise, default to current directory
+RABINIZER3_JAR=${RABINIZER3-./rabinizer.jar}
+
+# -hoa = output HOA
+# -gen-states = output state-based generalized Rabin
+java -jar $RABINIZER3_JAR -hoa -gen-states "$1"   &&  mv "$1.hoa" "$2"

prism/etc/scripts/hoa-rabinizer3-dra-for-prism

@@ -0,0 +1,17 @@
+#! /bin/bash
+
+# Interface wrapper for calling Rabinizer3 (state-based DRA)
+# Invoke from PRISM with
+#  -ltl2datool hoa-rabinizer3-dra-for-prism -ltl2dasyntax rabinizer
+#
+# Expects the rabinizer.jar file of Rabinizer3 in the current directory, otherwise
+# specify its location using
+#  export RABINIZER3=path/to/rabinizer.jar
+
+# Take location of the jar file from RABINIZER3 environment variable
+# Otherwise, default to current directory
+RABINIZER3_JAR=${RABINIZER3-./rabinizer.jar}
+
+# -hoa = output HOA
+# -rabin-states = output state-based DRA
+java -jar $RABINIZER3_JAR -hoa -rabin-states "$1"   &&  mv "$1.hoa" "$2"

prism/etc/scripts/hoa-rabinizer3-tdra-for-prism

@@ -0,0 +1,17 @@
+#! /bin/bash
+
+# Interface wrapper for calling Rabinizer3 (transition-based DRA)
+# Invoke from PRISM with
+#  -ltl2datool hoa-rabinizer3-tdra-for-prism -ltl2dasyntax rabinizer
+#
+# Expects the rabinizer.jar file of Rabinizer3 in the current directory, otherwise
+# specify its location using
+#  export RABINIZER3=path/to/rabinizer.jar
+
+# Take location of the jar file from RABINIZER3 environment variable
+# Otherwise, default to current directory
+RABINIZER3_JAR=${RABINIZER3-./rabinizer.jar}
+
+# -hoa = output HOA
+# -rabin-edges = output transition-based Rabin
+java -jar $RABINIZER3_JAR -hoa -rabin-edges "$1"   &&  mv "$1.hoa" "$2"

prism/etc/scripts/hoa-rabinizer3-tgdra-for-prism

@@ -0,0 +1,17 @@
+#! /bin/bash
+
+# Interface wrapper for calling Rabinizer3 (transition-based DGRA)
+# Invoke from PRISM with
+#  -ltl2datool hoa-rabinizer3-tgdra-for-prism -ltl2dasyntax rabinizer
+#
+# Expects the rabinizer.jar file of Rabinizer3 in the current directory, otherwise
+# specify its location using
+#  export RABINIZER3=path/to/rabinizer.jar
+
+# Take location of the jar file from RABINIZER3 environment variable
+# Otherwise, default to current directory
+RABINIZER3_JAR=${RABINIZER3-./rabinizer.jar}
+
+# -hoa = output HOA
+# -gen-edges = output transition-based generalized Rabin
+java -jar $RABINIZER3_JAR -hoa -gen-edges "$1"   &&  mv "$1.hoa" "$2"

prism/src/acceptance/AcceptanceGenRabin.java

@@ -0,0 +1,293 @@
+//==============================================================================
+//	
+//	Copyright (c) 2014-
+//	Authors:
+//	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
+//	* Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham/Oxford)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package acceptance;
+
+import java.util.ArrayList;
+import java.util.BitSet;
+
+import jdd.JDDVars;
+
+/**
+ * A Generalized Rabin acceptance condition (based on BitSet state sets)
+ * This is a list of GenRabinPairs, which can be manipulated with the usual List interface.
+ * <br>
+ * Semantics: Each Generalized Rabin pair has state sets L and K_1,...,K_n and is accepting iff
+ * L is not visited infinitely often and all K_j are visited infinitely often:
+ *   (F G !"L") & (G F "K_1") & ... & (G F "K_n").
+ *
+ * The Generalized Rabin condition is accepting if at least one of the pairs is accepting.
+ */
+@SuppressWarnings("serial")
+public class AcceptanceGenRabin
+       extends ArrayList<AcceptanceGenRabin.GenRabinPair>
+       implements AcceptanceOmega
+{
+
+	/**
+	 * A pair in a Generalized Rabin acceptance condition, i.e., with
+	 *  (F G !"L") & (G F "K_1") & ... & (G F "K_n").
+	 **/
+	public static class GenRabinPair {
+		/** State set L (should be visited only finitely often) */
+		private BitSet L;
+
+		/** State sets K_j (should all be visited infinitely often) */
+		private ArrayList<BitSet> K_list;
+
+		/** Constructor with L and K_j state sets */
+		public GenRabinPair(BitSet L, ArrayList<BitSet> K_list) {
+			this.L = L;
+			this.K_list = K_list;
+		}
+
+		/** Get the state set L */
+		public BitSet getL()
+		{
+			return L;
+		}
+
+		/** Get the number of K_j sets */
+		public int getNumK()
+		{
+			return K_list.size();
+		}
+		
+		/** Get the state set K_j */
+		public BitSet getK(int j)
+		{
+			return K_list.get(j);
+		}
+
+		/** Returns true if the bottom strongly connected component
+		 * given by bscc_states is accepting for this pair.
+		 */
+		public boolean isBSCCAccepting(BitSet bscc_states)
+		{
+			if (L.intersects(bscc_states)) {
+				// there is some state in bscc_states that is
+				// forbidden by L
+				return false;
+			}
+
+			for (BitSet K_j : K_list) {
+				if (!K_j.intersects(bscc_states)) {
+					// there is some state in bscc_states that is
+					// contained in K -> infinitely often visits to K
+					return false;
+				}
+			}
+
+			return true;
+		}
+
+		/** Generate signature for this Rabin pair and the given state.
+		 *  If the state is a member of L, returns "-pairIndex".
+		 *  If the state is a member of K, returns "+pairIndex".
+		 *  @param stateIndex the state index
+		 *  @param pairIndex the index of this Rabin pair
+		 **/
+		public String getSignatureForState(int stateIndex, int pairIndex)
+		{
+			// TODO: (What is the correct syntax here?)
+			/*if (L.get(stateIndex)) {
+				return "-"+pairIndex;
+			} else if (K.get(stateIndex)) {
+				return "+"+pairIndex;
+			} else {
+				return "";
+			}*/
+			return "?";
+		}
+
+		@Override
+		public GenRabinPair clone()
+		{
+			ArrayList<BitSet> newK_list = new ArrayList<BitSet>();
+			for (BitSet K_j : K_list)
+				newK_list.add((BitSet) K_j.clone());
+			return new GenRabinPair((BitSet)L.clone(), newK_list);
+		}
+
+		public AcceptanceGeneric toAcceptanceGeneric()
+		{
+			AcceptanceGeneric genericL = new AcceptanceGeneric(AcceptanceGeneric.ElementType.FIN, (BitSet) L.clone());
+			if (getNumK() == 0) {
+				return genericL;
+			}
+			AcceptanceGeneric genericKs = null;
+			for (BitSet K : K_list) {
+				AcceptanceGeneric genericK = new AcceptanceGeneric(AcceptanceGeneric.ElementType.INF, (BitSet) K.clone());
+				if (genericKs == null) {
+					genericKs = genericK;
+				} else {
+					genericKs = new AcceptanceGeneric(AcceptanceGeneric.ElementType.AND, genericKs, genericK);
+				}
+			}
+			return new AcceptanceGeneric(AcceptanceGeneric.ElementType.AND, genericL, genericKs);
+		}
+	
+		/** Returns a textual representation of this Generalized Rabin pair. */
+		@Override
+		public String toString() {
+			String s = "(" + L;
+			for (BitSet K_j : K_list)
+				s += "," + K_j;
+			s += ")";
+			return s;
+		}
+	}
+
+	/** Make a copy of the acceptance condition. */
+	public AcceptanceGenRabin clone()
+	{
+		AcceptanceGenRabin result = new AcceptanceGenRabin();
+		for (GenRabinPair pair : this) {
+			result.add(pair.clone());
+		}
+
+		return result;
+	}
+
+	/** Returns true if the bottom strongly connected component
+	 * given by bscc_states is accepting for this Rabin condition,
+	 * i.e., there is a pair that accepts for bscc_states.
+	 */
+	public boolean isBSCCAccepting(BitSet bscc_states)
+	{
+		for (GenRabinPair pair : this) {
+			if (pair.isBSCCAccepting(bscc_states)) {
+				return true;
+			}
+		}
+
+		return false;
+	}
+
+	@Override
+	public void lift(LiftBitSet lifter) {
+		for (GenRabinPair pair : this) {
+			pair.L = lifter.lift(pair.L);
+			int n = pair.K_list.size();
+			for (int j = 0; j < n; j++)
+				pair.K_list.set(j, lifter.lift(pair.K_list.get(j)));
+		}
+	}
+
+	/**
+	 * Returns a new Generalized Rabin acceptance condition that corresponds to the disjunction
+	 * of this and the other Generalized Rabin acceptance condition. The GenRabinPairs are cloned, i.e.,
+	 * not shared with the argument acceptance condition.
+	 * @param other the other GeneralizedRabin acceptance condition
+	 * @return new AcceptanceGenRabin, disjunction of this and other
+	 */
+	public AcceptanceGenRabin or(AcceptanceGenRabin other)
+	{
+		AcceptanceGenRabin result = new AcceptanceGenRabin();
+		for (GenRabinPair pair : this) {
+			result.add((GenRabinPair) pair.clone());
+		}
+		for (GenRabinPair pair : other) {
+			result.add((GenRabinPair) pair.clone());
+		}
+		return result;
+	}
+
+	@Override
+	public AcceptanceGenRabinDD toAcceptanceDD(JDDVars ddRowVars)
+	{
+		return new AcceptanceGenRabinDD(this, ddRowVars);
+	}
+
+	@Override
+	public AcceptanceGeneric toAcceptanceGeneric()
+	{
+		if (size() == 0) {
+			return new AcceptanceGeneric(false);
+		}
+		AcceptanceGeneric genericPairs = null;
+		for (GenRabinPair pair : this) {
+			AcceptanceGeneric genericPair = pair.toAcceptanceGeneric();
+			if (genericPairs == null) {
+				genericPairs = genericPair;
+			} else {
+				genericPairs = new AcceptanceGeneric(AcceptanceGeneric.ElementType.OR, genericPairs, genericPair);
+			}
+		}
+		return genericPairs;
+	}
+
+	/**
+	 * Get the acceptance signature for state stateIndex.
+	 **/
+	public String getSignatureForState(int stateIndex)
+	{
+		String result = "";
+
+		for (int pairIndex=0; pairIndex<size(); pairIndex++) {
+			GenRabinPair pair = get(pairIndex);
+			result += pair.getSignatureForState(stateIndex,  pairIndex);
+		}
+
+		return result;
+	}
+
+	/** Returns a textual representation of this acceptance condition. */
+	@Override
+	public String toString()
+	{
+		String result = "";
+		for (GenRabinPair pair : this) {
+			result += pair.toString();
+		}
+		return result;
+	}
+
+	@Override
+	public String getSizeStatistics()
+	{
+		return size() + " Generalized Rabin pairs";
+	}
+
+	@Override
+	public AcceptanceType getType()
+	{
+		return AcceptanceType.GENERALIZED_RABIN;
+	}
+
+	@Override
+	public String getTypeAbbreviated()
+	{
+		return "GR";
+	}
+
+	@Override
+	public String getTypeName()
+	{
+		return "Generalized Rabin";
+	}
+}

prism/src/acceptance/AcceptanceGenRabinDD.java

@@ -0,0 +1,226 @@
+//==============================================================================
+//	
+//	Copyright (c) 2014-
+//	Authors:
+//	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
+//	* Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham/Oxford)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package acceptance;
+
+import java.util.ArrayList;
+
+import common.IterableBitSet;
+
+import jdd.JDD;
+import jdd.JDDNode;
+import jdd.JDDVars;
+
+/**
+ * A Generalized Rabin acceptance condition (based on JDD state sets)
+ * This is a list of GenRabinPairs, which can be manipulated with the usual List interface.
+ * <br>
+ * Semantics: Each Generalized Rabin pair has state sets L and K_1,...,K_n and is accepting iff
+ * L is not visited infinitely often and all K_j are visited infinitely often:
+ *   (F G !"L") & (G F "K_1") & ... & (G F "K_n").
+ *
+ * The Generalized Rabin condition is accepting if at least one of the pairs is accepting.
+ */
+@SuppressWarnings("serial")
+public class AcceptanceGenRabinDD
+       extends ArrayList<AcceptanceGenRabinDD.GenRabinPairDD>
+       implements AcceptanceOmegaDD
+{
+
+	/**
+	 * A pair in a Generalized Rabin acceptance condition, i.e., with
+	 *  (F G !"L") & (G F "K_1") & ... & (G F "K_n").
+	 **/
+	public static class GenRabinPairDD {
+		/** State set L (should be visited only finitely often) */
+		private JDDNode L;
+
+		/** State sets K_j (should all be visited infinitely often) */
+		private ArrayList<JDDNode> K_list;
+
+		/**
+		 * Constructor with L and K_j state sets.
+		 * Becomes owner of the references of L and K_j's.
+		 */
+		public GenRabinPairDD(JDDNode L, ArrayList<JDDNode> K_list)
+		{
+			this.L = L;
+			this.K_list = K_list;
+		}
+
+		/** Clear resources of the state sets */
+		public void clear()
+		{
+			if (L!=null) JDD.Deref(L);
+			for (JDDNode K_j : K_list)
+				JDD.Deref(K_j);
+		}
+
+		/** Get a referenced copy of the state set L.
+		 * <br>[ REFS: <i>result</i>, DEREFS: <i>none</i> ]
+		 */
+		public JDDNode getL()
+		{
+			JDD.Ref(L);
+			return L;
+		}
+
+		/** Get the number of K_j sets */
+		public int getNumK()
+		{
+			return K_list.size();
+		}
+		
+		/** Get a referenced copy of the state set K_j.
+		 * <br>[ REFS: <i>result</i>, DEREFS: <i>none</i> ]
+		 */
+		public JDDNode getK(int j)
+		{
+			JDD.Ref(K_list.get(j));
+			return K_list.get(j);
+		}
+
+		/** Returns true if the bottom strongly connected component
+		 * given by bscc_states is accepting for this pair.
+		 * <br>[ REFS: <i>none</i>, DEREFS: <i>none</i> ]
+		 */
+		public boolean isBSCCAccepting(JDDNode bscc_states)
+		{
+			if (JDD.AreInterecting(L, bscc_states)) {
+				// there is some state in bscc_states that is
+				// forbidden by L
+				return false;
+			}
+
+			for (JDDNode K_j : K_list) {
+				if (!JDD.AreInterecting(K_j, bscc_states)) {
+					// there is some state in bscc_states that is
+					// contained in K_j -> infinitely often visits to K_j
+					return false;
+				}
+			}
+
+			return true;
+		}
+
+		/** Returns a textual representation of this Rabin pair. */
+		@Override
+		public String toString()
+		{
+			String s = "(" + L;
+			for (JDDNode K_j : K_list)
+				s += "," + K_j;
+			s += ")";
+			return s;
+		}
+	}
+
+	/**
+	 * Constructor, from a BitSet-based AcceptanceGenRabin.
+	 *
+	 * @param acceptance the BitSet-based acceptance condition
+	 * @param ddRowVars JDDVars of the row variables corresponding to the bits in the bit set
+	 */
+	public AcceptanceGenRabinDD(AcceptanceGenRabin acceptance, JDDVars ddRowVars)
+	{
+		for (AcceptanceGenRabin.GenRabinPair pair : acceptance) {
+			// get BDD based newL and newK from the bit sets
+			JDDNode newL = JDD.Constant(0);
+			for (int i : IterableBitSet.getSetBits(pair.getL())) {
+				newL = JDD.SetVectorElement(newL, ddRowVars, i, 1.0);
+			}
+
+			ArrayList<JDDNode> newK_list = new ArrayList<JDDNode>();
+			int n = pair.getNumK();
+			for (int j = 0; j < n; j++) {
+				JDDNode newK_j = JDD.Constant(0);
+				for (int i : IterableBitSet.getSetBits(pair.getK(j))) {
+					newK_j = JDD.SetVectorElement(newK_j, ddRowVars, i, 1.0);
+				}
+				newK_list.add(newK_j);
+			}
+
+			GenRabinPairDD newPair = new GenRabinPairDD(newL, newK_list);
+			this.add(newPair);
+		}
+	}
+
+	@Override
+	public boolean isBSCCAccepting(JDDNode bscc_states)
+	{
+		for (GenRabinPairDD pair : this) {
+			if (pair.isBSCCAccepting(bscc_states)) {
+				return true;
+			}
+		}
+		return false;
+	}
+
+	@Override
+	public void clear()
+	{
+		for (GenRabinPairDD pair : this) {
+			pair.clear();
+		}
+		super.clear();
+	}
+
+	/** Returns a textual representation of this acceptance condition. */
+	@Override
+	public String toString()
+	{
+		String result = "";
+		for (GenRabinPairDD pair : this) {
+			result += pair.toString();
+		}
+		return result;
+	}
+
+	@Override
+	public String getSizeStatistics()
+	{
+		return size() + " Generalized Rabin pairs";
+	}
+
+	@Override
+	public AcceptanceType getType()
+	{
+		return AcceptanceType.GENERALIZED_RABIN;
+	}
+
+	@Override
+	public String getTypeAbbreviated()
+	{
+		return "GR";
+	}
+
+	@Override
+	public String getTypeName()
+	{
+		return "Generalized Rabin";
+	}
+}

prism/src/acceptance/AcceptanceGeneric.java

@@ -0,0 +1,275 @@
+//==============================================================================
+//	
+//	Copyright (c) 2014-
+//	Authors:
+//	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
+//	* Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham/Oxford)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package acceptance;
+
+import java.util.BitSet;
+
+import jdd.JDDVars;
+
+/**
+ * A generic acceptance condition (based on BitSet state sets).
+ * This is an AST of a boolean formula (conjunction and disjunction) over
+ * atoms of the form Inf(states), Inf(!states), Fin(states) and Fin(!states).
+ * <br>
+ * Semantics:
+ *  Inf(states)  <=> G F states
+ *  Inf(!states) <=> G F !states
+ *  Fin(states)  <=> F G !states
+ *  Fin(!states) <=> F G states
+ */
+public class AcceptanceGeneric implements AcceptanceOmega {
+	
+	/** The types of elements in the AST */
+	public enum ElementType {
+		FALSE,
+		TRUE, 
+
+		OR,
+		AND,
+
+		INF,
+		FIN,
+		INF_NOT,
+		FIN_NOT;
+	}
+	
+	/** The type of this node in the AST */
+	private ElementType kind;
+
+	/** The left child (if it exists) */ 
+	private AcceptanceGeneric left = null;
+
+	/** The right child (if it exists) */ 
+	private AcceptanceGeneric right = null;
+
+	/** The set of states (if this is one of INF, FIN, INF_NOT, FIN_NOT) */
+	private BitSet states = null;
+
+	/**
+	 * Constructor for TRUE or FALSE
+	 * @param value true or false?
+	 */
+	public AcceptanceGeneric(boolean value) {
+		kind = value ? ElementType.TRUE : ElementType.FALSE;
+	}
+	
+	/** 
+	 * Constructor for an INF, FIN, INF_NOT or FIN_NOT element. 
+	 */
+	public AcceptanceGeneric(ElementType kind, BitSet states) {
+		this.kind = kind;
+
+		this.states = states;
+	}
+
+	/**
+	 * Constructor for a binary operator (AND/OR).
+	 * @param kind
+	 * @param left
+	 * @param right
+	 */
+	public AcceptanceGeneric(ElementType kind, AcceptanceGeneric left, AcceptanceGeneric right) {
+		this.kind = kind;
+		this.left = left;
+		this.right = right;
+	}
+
+	/** Get the ElementType of this AST element */
+	public ElementType getKind() {
+		return kind;
+	}
+
+	/** Get the left child of this AST element */
+	public AcceptanceGeneric getLeft() {
+		return left;
+	}
+
+	/** Get the right child of this AST element */
+	public AcceptanceGeneric getRight() {
+		return right;
+	}
+
+	/** Get the state set of this element (if kind is one of INF, FIN, INF_NOT, FIN_NOT).
+	 */
+	public BitSet getStates() {
+		return states;
+	}
+
+	@Override
+	public boolean isBSCCAccepting(BitSet bscc) {
+		switch(kind) {
+			case TRUE: return true;
+			case FALSE: return false;
+			case AND: return left.isBSCCAccepting(bscc) && right.isBSCCAccepting(bscc);
+			case OR: return left.isBSCCAccepting(bscc) || right.isBSCCAccepting(bscc);
+			case INF:
+				// bscc |= G F states?
+				// there exists a state in bscc and states
+				return bscc.intersects(states);
+			case INF_NOT: {
+				// bscc_state |= G F !states?
+				// the BSCC does not consist only of states
+				BitSet bs = (BitSet) bscc.clone();
+				bs.andNot(states);
+				return !bs.isEmpty();
+			}
+			case FIN: {
+				// bscc |= F G !states?
+				// <=> there exists no states state in BSCC
+				return !bscc.intersects(states);
+			}
+			case FIN_NOT: {
+				// bscc |= F G states?
+				// the BSCC consists entirely of states
+				BitSet bs = (BitSet) bscc.clone();
+				bs.and(states);
+				return bs.equals(bscc);
+			}
+		}
+		return false;
+	}
+
+	@Override
+	public String getSignatureForState(int i) {
+		return "";
+	}
+
+	@Override
+	public String getSizeStatistics() {
+		return "generic acceptance with " + countAcceptanceSets() + " acceptance sets";
+	}
+
+	@Override
+	public AcceptanceType getType() {
+		return AcceptanceType.GENERIC;
+	}
+
+	@Override
+	public String getTypeAbbreviated() {
+		return "";
+	}
+
+	@Override
+	public String getTypeName() {
+		return "generic";
+	}
+
+	@Override
+	public AcceptanceGeneric clone() {
+		switch (kind) {
+			case FIN:
+			case FIN_NOT:
+			case INF:
+			case INF_NOT:
+				return new AcceptanceGeneric(kind, states);
+			case AND:
+			case OR:
+				return new AcceptanceGeneric(kind, left.clone(), right.clone());
+			case FALSE:
+				return new AcceptanceGeneric(false);
+			case TRUE:
+				return new AcceptanceGeneric(true);
+		}
+		throw new UnsupportedOperationException("Unsupported operator in generic acceptance condition");
+	}
+
+	@Override
+	public void lift(LiftBitSet lifter) {
+		switch(kind) {
+			case TRUE:
+			case FALSE:
+				return;
+			case INF:
+			case INF_NOT:
+			case FIN:
+			case FIN_NOT:
+				states = lifter.lift(states);
+				return;
+			case AND:
+			case OR:
+				left.lift(lifter);
+				right.lift(lifter);
+				return;
+		}
+		throw new UnsupportedOperationException("Unsupported operator in generic acceptance condition");
+	}
+
+	/** Count the number of state sets in this acceptance condition */
+	public int countAcceptanceSets() {
+		switch(kind) {
+			case FALSE:
+			case TRUE:
+				return 0;
+			case INF:
+			case FIN: 
+			case INF_NOT:
+			case FIN_NOT:
+				return 1;
+			case OR:
+			case AND: 
+				return left.countAcceptanceSets() + right.countAcceptanceSets();
+		}
+		throw new UnsupportedOperationException("Unsupported operator in generic acceptance condition");
+	}
+
+	@Override
+	public AcceptanceOmegaDD toAcceptanceDD(JDDVars ddRowVars) {
+		return new AcceptanceGenericDD(this, ddRowVars);
+	}
+
+	@Override
+	public AcceptanceGeneric toAcceptanceGeneric()
+	{
+		return this.clone();
+	}
+
+	@Override
+	public String toString() {
+		switch(kind) {
+			case TRUE:
+				return "true";
+			case FALSE:
+				return "false";
+			case AND:
+				return  "(" + left.toString() + " & " + right.toString() + ")";
+			case OR:
+				return  "(" + left.toString() + " | " + right.toString() + ")";
+			case INF:
+				return "Inf(" + states.toString() + ")";
+			case FIN:
+				return "Fin(" + states.toString() + ")";
+			case INF_NOT:
+				return "Inf(!" + states.toString() + ")";
+			case FIN_NOT:
+				return "Fin(!" + states.toString() + ")";
+			default:
+				return null;
+		}
+	}
+
+}

prism/src/acceptance/AcceptanceGenericDD.java

@@ -0,0 +1,206 @@
+//==============================================================================
+//	
+//	Copyright (c) 2014-
+//	Authors:
+//	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
+//	* Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham/Oxford)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package acceptance;
+
+import common.IterableBitSet;
+import acceptance.AcceptanceGeneric.ElementType;
+import jdd.JDD;
+import jdd.JDDNode;
+import jdd.JDDVars;
+
+/**
+ * A generic acceptance condition (based on JDD state sets).
+ * This is an AST of a boolean formula (conjunction and disjunction) over
+ * atoms of the form Inf(states), Inf(!states), Fin(states) and Fin(!states).
+ * <br>
+ * Semantics:
+ *  Inf(states)  <=> G F states
+ *  Inf(!states) <=> G F !states
+ *  Fin(states)  <=> F G !states
+ *  Fin(!states) <=> F G states
+ */
+public class AcceptanceGenericDD implements AcceptanceOmegaDD {
+
+	private ElementType kind;
+	private AcceptanceGenericDD left = null;
+	private AcceptanceGenericDD right = null;
+	private JDDNode states = null;
+
+	public AcceptanceGenericDD(AcceptanceGeneric acceptance, JDDVars ddRowVars)
+	{
+		switch(acceptance.getKind()) {
+			case AND:
+			case OR:
+				kind = acceptance.getKind();
+				left = (AcceptanceGenericDD) acceptance.getLeft().toAcceptanceDD(ddRowVars);
+				right = (AcceptanceGenericDD) acceptance.getRight().toAcceptanceDD(ddRowVars);
+				return;
+			case TRUE:
+				kind = ElementType.TRUE;
+				return;
+			case FALSE:
+				kind = ElementType.FALSE;
+				return;
+			case INF:
+			case INF_NOT:
+			case FIN:
+			case FIN_NOT:
+				kind = acceptance.getKind();
+				states = JDD.Constant(0);
+				for (int i : IterableBitSet.getSetBits(acceptance.getStates())) {
+					states = JDD.SetVectorElement(states, ddRowVars, i, 1.0);
+				}
+				return;
+		}
+		throw new UnsupportedOperationException("Unsupported operatator in generic acceptance condition");
+	}
+
+	/** Get the ElementType of this AST element */
+	public ElementType getKind()
+	{
+		return kind;
+	}
+
+	/** Get the left child of this AST element */
+	public AcceptanceGenericDD getLeft()
+	{
+		return left;
+	}
+
+	/** Get the right child of this AST element */
+	public AcceptanceGenericDD getRight()
+	{
+		return right;
+	}
+
+	/** Get a referenced copy of the state sets (if kind is one of INF, FIN, INF_NOT, FIN_NOT).
+	 * <br>[ REFS: <i>result</i>, DEREFS: <i>none</i> ]
+	 */
+	public JDDNode getStates()
+	{
+		if (states != null) {
+			JDD.Ref(states);
+		}
+		return states;
+	}
+
+	@Override
+	public boolean isBSCCAccepting(JDDNode bscc)
+	{
+		switch(kind) {
+		case TRUE: 
+			return true;
+		case FALSE: 
+			return false;
+		case AND: 
+			return left.isBSCCAccepting(bscc) && right.isBSCCAccepting(bscc);
+		case OR: 
+			return left.isBSCCAccepting(bscc) || right.isBSCCAccepting(bscc);
+		case INF:
+			// bscc |= G F states?
+			// there exists a state in bscc and states
+			return JDD.AreInterecting(states, bscc);
+		case INF_NOT:
+			// bscc_state |= G F !states?
+			// the BSCC intersects Not(states)
+			JDD.Ref(states);
+			return JDD.AreInterecting(JDD.Not(states), bscc);
+		case FIN:
+			// bscc |= F G !states?
+			// the BSCC consists only of !states
+			return !JDD.AreInterecting(states, bscc);
+		case FIN_NOT:
+			// bscc |= F G states?
+			// the BSCC consists entirely of states
+			JDD.Ref(states);
+			return !JDD.AreInterecting(JDD.Not(states), bscc);
+		}
+		throw new UnsupportedOperationException("Unsupported operator in generic acceptance expression");
+	}
+
+	@Override
+	public String getSizeStatistics() {
+		return "generic acceptance with " + countAcceptanceSets() + " acceptance sets";
+	}
+
+	@Override
+	public AcceptanceType getType() {
+		return AcceptanceType.GENERIC;
+	}
+
+	@Override
+	public String getTypeAbbreviated() {
+		return "";
+	}
+
+	@Override
+	public String getTypeName() {
+		return "generic";
+	}
+
+	@Override
+	public void clear() {
+		switch (kind) {
+			case TRUE:
+			case FALSE:
+				return;
+			case AND:
+			case OR:
+				left.clear();
+				right.clear();
+				return;
+			case INF_NOT:
+			case FIN:
+			case FIN_NOT:
+			case INF:
+				if (states != null) JDD.Deref(states);
+				states = null;
+				return;
+		}
+		throw new UnsupportedOperationException("Unsupported operator in generic acceptance expression");
+	}
+
+	/** Count the number of state sets in this acceptance condition */
+	public int countAcceptanceSets() {
+		switch(kind) {
+			case FALSE:
+			case TRUE:
+				return 0;
+			case INF:
+			case FIN: 
+			case INF_NOT:
+			case FIN_NOT:
+				return 1;
+			case OR:
+			case AND: 
+				return left.countAcceptanceSets() + right.countAcceptanceSets();
+		}
+		throw new UnsupportedOperationException("Unsupported operator in generic acceptance expression");
+	}
+
+}

prism/src/acceptance/AcceptanceOmega.java

@@ -82,4 +82,9 @@ public interface AcceptanceOmega extends Cloneable
 	 * @param ddRowVars JDDVars of the row variables corresponding to the bits in the bitset
 	 */
 	public AcceptanceOmegaDD toAcceptanceDD(JDDVars ddRowVars);
+	
+	/**
+	 * Convert this acceptance condition to an AcceptanceGeneric condition.
+	 */
+	public AcceptanceGeneric toAcceptanceGeneric();
 }

prism/src/acceptance/AcceptanceRabin.java

@@ -96,6 +96,16 @@ public class AcceptanceRabin
 			return false;
 		}
 
+		public AcceptanceGeneric toAcceptanceGeneric()
+		{
+			AcceptanceGeneric genericL = new AcceptanceGeneric(AcceptanceGeneric.ElementType.FIN, (BitSet)L.clone());
+			AcceptanceGeneric genericK = new AcceptanceGeneric(AcceptanceGeneric.ElementType.INF, (BitSet)K.clone());
+			
+			//      F G ! "L" & G F "K"
+			// <=>  Fin(L) & Inf(K)
+			return new AcceptanceGeneric(AcceptanceGeneric.ElementType.AND, genericL, genericK);
+		}
+
 		/** Generate signature for this Rabin pair and the given state.
 		 *  If the state is a member of L, returns "-pairIndex".
 		 *  If the state is a member of K, returns "+pairIndex".
@@ -204,6 +214,24 @@ public class AcceptanceRabin
 		return new AcceptanceRabinDD(this, ddRowVars);
 	}
 
+	@Override
+	public AcceptanceGeneric toAcceptanceGeneric()
+	{
+		if (size() == 0) {
+			return new AcceptanceGeneric(false);
+		}
+		AcceptanceGeneric genericPairs = null;
+		for (RabinPair pair : this) {
+			AcceptanceGeneric genericPair = pair.toAcceptanceGeneric();
+			if (genericPairs == null) {
+				genericPairs = genericPair;
+			} else {
+				genericPairs = new AcceptanceGeneric(AcceptanceGeneric.ElementType.OR, genericPairs, genericPair);
+			}
+		}
+		return genericPairs;
+	}
+
 	/**
 	 * Get the acceptance signature for state stateIndex.
 	 **/

prism/src/acceptance/AcceptanceRabinDD.java

@@ -98,6 +98,7 @@ public class AcceptanceRabinDD
 
 		/** Returns true if the bottom strongly connected component
 		 * given by bscc_states is accepting for this pair.
+		 * <br>[ REFS: <i>none</i>, DEREFS: <i>none</i> ]
 		 */
 		public boolean isBSCCAccepting(JDDNode bscc_states)
 		{
@@ -149,10 +150,7 @@ public class AcceptanceRabinDD
 		}
 	}
 
-	/** Returns true if the bottom strongly connected component
-	 * given by bscc_states is accepting for this Rabin condition,
-	 * i.e., there is a pair that accepts for bscc_states.
-	 */
+	@Override
 	public boolean isBSCCAccepting(JDDNode bscc_states)
 	{
 		for (RabinPairDD pair : this) {

prism/src/acceptance/AcceptanceReach.java

@@ -28,8 +28,6 @@ package acceptance;
 
 import java.util.BitSet;
 
-import acceptance.AcceptanceRabin.RabinPair;
-
 import jdd.JDDVars;
 
 /**
@@ -91,6 +89,12 @@ public class AcceptanceReach implements AcceptanceOmega
 		return new AcceptanceReachDD(this, ddRowVars);
 	}
 
+	@Override
+	public AcceptanceGeneric toAcceptanceGeneric()
+	{
+		return new AcceptanceGeneric(AcceptanceGeneric.ElementType.INF, (BitSet) goalStates.clone());
+	}
+
 	@Override
 	public String getSignatureForState(int i)
 	{

prism/src/acceptance/AcceptanceReachDD.java

@@ -1,9 +1,9 @@
-package acceptance;
 //==============================================================================
 //
 //Copyright (c) 2014-
 //Authors:
-//* Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
+//	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
+//	* Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham/Oxford)
 //
 //------------------------------------------------------------------------------
 //
@@ -25,6 +25,8 @@ package acceptance;
 //
 //==============================================================================
 
+package acceptance;
+
 import common.IterableBitSet;
 import jdd.JDD;
 import jdd.JDDNode;

prism/src/acceptance/AcceptanceStreett.java

@@ -98,6 +98,17 @@ public class AcceptanceStreett
 			}
 		}
 
+		public AcceptanceGeneric toAcceptanceGeneric()
+		{
+			AcceptanceGeneric genericR = new AcceptanceGeneric(AcceptanceGeneric.ElementType.FIN, (BitSet)R.clone());
+			AcceptanceGeneric genericG = new AcceptanceGeneric(AcceptanceGeneric.ElementType.INF, (BitSet)G.clone());
+			//      G F "R" -> G F "G"
+			// <=>  ! G F "R"  | G F "G"
+			// <=>  F G ! "R"  | G F "G"
+			// <=>  Fin(R) | Inf(G)
+			return new AcceptanceGeneric(AcceptanceGeneric.ElementType.OR, genericR, genericG);
+		}
+
 		/** Generate signature for this Streett pair and the given state.
 		 *  If the state is a member of R, returns "-pairIndex".
 		 *  If the state is a member of G, returns "+pairIndex".
@@ -206,6 +217,24 @@ public class AcceptanceStreett
 		return new AcceptanceStreettDD(this, ddRowVars);
 	}
 
+	@Override
+	public AcceptanceGeneric toAcceptanceGeneric()
+	{
+		if (size() == 0) {
+			return new AcceptanceGeneric(true);
+		}
+		AcceptanceGeneric genericPairs = null;
+		for (StreettPair pair : this) {
+			AcceptanceGeneric genericPair = pair.toAcceptanceGeneric();
+			if (genericPairs == null) {
+				genericPairs = genericPair;
+			} else {
+				genericPairs = new AcceptanceGeneric(AcceptanceGeneric.ElementType.AND, genericPairs, genericPair);
+			}
+		}
+		return genericPairs;
+	}
+
 	/**
 	 * Get the acceptance signature for state stateIndex.
 	 **/

prism/src/acceptance/AcceptanceStreettDD.java

@@ -98,6 +98,7 @@ public class AcceptanceStreettDD
 
 		/** Returns true if the bottom strongly connected component
 		 * given by bscc_states is accepting for this pair.
+		 * <br>[ REFS: <i>none</i>, DEREFS: <i>none</i> ]
 		 */
 		public boolean isBSCCAccepting(JDDNode bscc_states)
 		{

prism/src/acceptance/AcceptanceType.java

@@ -3,6 +3,7 @@
 //	Copyright (c) 2014-
 //	Authors:
 //	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
+//	* Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham/Oxford)
 //	
 //------------------------------------------------------------------------------
 //	
@@ -32,7 +33,9 @@ package acceptance;
 public enum AcceptanceType {
 	RABIN,
  	STREETT,
- 	REACH;
+ 	REACH,
+	GENERALIZED_RABIN,
+ 	GENERIC;
 
 	/**
 	 * Check whether an array of AcceptanceTypes contains a specific element.

prism/src/explicit/DTMCModelChecker.java

@@ -76,7 +76,8 @@ public class DTMCModelChecker extends ProbModelChecker
 		// Build product of Markov chain and automaton
 		AcceptanceType[] allowedAcceptance = {
 				AcceptanceType.RABIN,
-				AcceptanceType.REACH
+				AcceptanceType.REACH,
+				AcceptanceType.GENERIC
 		};
 		product = mcLtl.constructProductMC(this, (DTMC)model, expr, statesOfInterest, allowedAcceptance);
 

prism/src/explicit/LTLModelChecker.java

@@ -54,6 +54,7 @@ import prism.PrismFileLog;
 import prism.PrismLangException;
 import prism.PrismLog;
 import prism.PrismNotSupportedException;
+import acceptance.AcceptanceGenRabin;
 import acceptance.AcceptanceOmega;
 import acceptance.AcceptanceRabin;
 import acceptance.AcceptanceType;
@@ -594,6 +595,8 @@ public class LTLModelChecker extends PrismComponent
 	{
 		if (acceptance instanceof AcceptanceRabin) {
 			return findAcceptingECStatesForRabin(model, (AcceptanceRabin) acceptance);
+		} else if (acceptance instanceof AcceptanceGenRabin) {
+			return findAcceptingECStatesForGeneralizedRabin(model, (AcceptanceGenRabin) acceptance);
 		}
 		throw new PrismNotSupportedException("Computing end components for acceptance type '"+acceptance.getTypeName()+"' currently not supported (explicit engine).");
 	}
@@ -634,6 +637,53 @@ public class LTLModelChecker extends PrismComponent
 		return allAcceptingStates;
 	}
 
+	/**
+	 * Find the set of states in accepting end components (ECs) in a nondeterministic model wrt a Generalized Rabin acceptance condition.
+	 * @param model The model
+	 * @param acceptance The acceptance condition
+	 */
+	public BitSet findAcceptingECStatesForGeneralizedRabin(NondetModel model, AcceptanceGenRabin acceptance) throws PrismException
+	{
+		BitSet allAcceptingStates = new BitSet();
+		int numStates = model.getNumStates();
+		
+		// Go through the GR acceptance pairs (L_i, K_i_1, ..., K_i_n) 
+		for (int i = 0; i < acceptance.size(); i++) {
+			
+			// Find model states *not* satisfying L_i
+			BitSet bitsetLi = acceptance.get(i).getL();
+			BitSet statesLi_not = new BitSet();
+			for (int s = 0; s < numStates; s++) {
+				if (!bitsetLi.get(s)) {
+					statesLi_not.set(s);
+				}
+			}
+			// Skip pairs with empty !L_i
+			if (statesLi_not.cardinality() == 0)
+				continue;
+			// Compute maximum end components (MECs) in !L_i
+			ECComputer ecComputer = ECComputer.createECComputer(this, model);
+			ecComputer.computeMECStates(statesLi_not);
+			List<BitSet> mecs = ecComputer.getMECStates();
+			// Check which MECs contain a state from each K_i_j
+			int n = acceptance.get(i).getNumK();
+			for (BitSet mec : mecs) {
+				boolean allj = true;
+				for (int j = 0; j < n; j++) {
+					if (!mec.intersects(acceptance.get(i).getK(j))) {
+						allj = false;
+						break;
+					}
+				}
+				if (allj) {
+					allAcceptingStates.or(mec);
+				}
+			}
+		}
+
+		return allAcceptingStates;
+	}
+
 	/** Lift the acceptance condition from the automaton to the product states. */
 	private AcceptanceOmega liftAcceptance(final LTLProduct<?> product, AcceptanceOmega acceptance)
 	{

prism/src/explicit/MDPModelChecker.java

@@ -84,6 +84,7 @@ public class MDPModelChecker extends ProbModelChecker
 
 		AcceptanceType[] allowedAcceptance = {
 				AcceptanceType.RABIN,
+				AcceptanceType.GENERALIZED_RABIN,
 				AcceptanceType.REACH
 		};
 

prism/src/jltl2ba/APSet.java

@@ -45,7 +45,7 @@ public class APSet implements Iterable<String> {
    * @param name the name of the AP
    * @return the index of the added AP
    */
-	int addAP(String name) {
+	public int addAP(String name) {
 		int i = vector.indexOf(name);
 		
 		if (i == -1) {

prism/src/jltl2ba/SimpleLTL.java

@@ -587,7 +587,49 @@ public class SimpleLTL {
 		}
 		return rv;
 	}
-	
+
+	/**
+	 * Returns an equivalent SimpleLTL formula with a
+	 * basic set of operators:
+	 *   AP, TRUE, FALSE, AND, OR, NOT, UNTIL, FINALLY, GLOBALLY, NEXT
+	 */
+	public SimpleLTL toBasicOperators() {
+		switch (kind) {
+		case AP:
+		case TRUE:
+		case FALSE:
+			return this;
+		case AND:
+		case OR:
+		case UNTIL:
+			return new SimpleLTL(kind, left.toBasicOperators(), right.toBasicOperators());
+		case FINALLY:
+		case GLOBALLY:
+		case NEXT:
+		case NOT:
+			return new SimpleLTL(kind, left.toBasicOperators());
+		case EQUIV: {
+			SimpleLTL newLeft = left.toBasicOperators();
+			SimpleLTL newRight = right.toBasicOperators();
+			SimpleLTL bothTrue = new SimpleLTL(LTLType.AND, newLeft, newRight);
+			SimpleLTL bothFalse = new SimpleLTL(LTLType.AND,
+			                                    new SimpleLTL(LTLType.NOT, newLeft),
+			                                    new SimpleLTL(LTLType.NOT, newRight));
+			return new SimpleLTL(LTLType.OR, bothTrue, bothFalse);
+		}
+		case IMPLIES: {
+			SimpleLTL newLeft = new SimpleLTL(LTLType.NOT, left.toBasicOperators());
+			return new SimpleLTL(LTLType.OR, newLeft, right.toBasicOperators());
+		}
+		case RELEASE: {
+			SimpleLTL newLeft = new SimpleLTL(LTLType.NOT, left.toBasicOperators());
+			SimpleLTL newRight = new SimpleLTL(LTLType.NOT, right.toBasicOperators());
+			return new SimpleLTL(LTLType.UNTIL, newLeft, newRight);
+		}
+		}
+		throw new UnsupportedOperationException("Unknown operator in SimpleLTL");
+	}
+
 	public SimpleLTL negate() {
 		return new SimpleLTL(LTLType.NOT, this);
 	}
@@ -937,6 +979,202 @@ public class SimpleLTL {
 		}
 	}
 
+	/**
+	 * Renames the atomic propositions apparing in the formula that
+	 * start with {@code prefixFrom}. For these, the prefix is replaced
+	 * by prefixTo. For example, with prefixFrom = "L" and prefixTo = "p",
+	 * "L3" will be renamed to "p3", but "T2" will be left as-is.
+	 */
+	public void renameAP(String prefixFrom, String prefixTo)
+	{
+		switch (kind) {
+		case AP:
+			if (ap.startsWith(prefixFrom)) {
+				ap = prefixTo + ap.substring(prefixFrom.length());
+			}
+			return;
+		case AND:
+		case OR:
+		case EQUIV:
+		case IMPLIES:
+		case RELEASE:
+		case UNTIL:
+			left.renameAP(prefixFrom, prefixTo);
+			right.renameAP(prefixFrom, prefixTo);
+			return;
+		case FINALLY:
+		case GLOBALLY:
+		case NEXT:
+		case NOT:
+			left.renameAP(prefixFrom, prefixTo);
+			return;
+		case TRUE:
+		case FALSE:
+			return;
+		}
+		throw new UnsupportedOperationException("Unknown operator in SimpleLTL formula: "+this);
+	}
+	
+	/**
+	 * Render this LTL formula in LBT syntax, i.e., in prefix notation.
+	 */
+	public String toStringLBT()
+	{
+		String rv = "";
+
+		switch (kind) {
+		case OR:
+			rv = "| " + left.toStringLBT() + " " + right.toStringLBT();
+			break;
+		case AND:
+			rv = "& " + left.toStringLBT() + " " + right.toStringLBT();
+			break;
+		case UNTIL:
+			rv = "U " + left.toStringLBT() + " " + right.toStringLBT();
+			break;
+		case RELEASE:
+			rv = "V " + left.toStringLBT() + " " + right.toStringLBT();
+			break;
+		case IMPLIES:
+			rv = "i " + left.toStringLBT() + " " + right.toStringLBT();
+			break;
+		case EQUIV:
+			rv = "e " + left.toStringLBT() + " " + right.toStringLBT();
+			break;
+		case NEXT:
+			rv = "X " + left.toStringLBT();
+			break;
+		case FINALLY:
+			rv = "F " + left.toStringLBT();
+			break;
+		case GLOBALLY:
+			rv = "G " + left.toStringLBT();
+			break;
+		case NOT:
+			rv = "! " + left.toStringLBT();
+			break;
+		case FALSE:
+			rv = "f";
+			break;
+		case TRUE:
+			rv = "t";
+			break;
+		case AP:
+			rv = ap;
+			break;
+		default:
+			rv = null;
+		}
+		return rv;
+	}
+
+	/**
+	 * Render this LTL formula in Spin syntax.
+	 */
+	public String toStringSpin()
+	{
+		String rv = "";
+
+		switch (kind) {
+		case OR:
+			rv = "(" + left.toStringSpin() + ") || (" + right.toStringSpin() + ")";
+			break;
+		case AND:
+			rv = "(" + left.toStringSpin() + ") && (" + right.toStringSpin() + ")";
+			break;
+		case UNTIL:
+			rv = "(" + left.toStringSpin() + ") U (" + right.toStringSpin() + ")";
+			break;
+		case RELEASE:
+			rv = "(" + left.toStringSpin() + ") V (" + right.toStringSpin() + ")";
+			break;
+		case IMPLIES:
+			rv = "(" + left.toStringSpin() + ") -> (" + right.toStringSpin() + ")";
+			break;
+		case EQUIV:
+			rv = "(" + left.toStringSpin() + ") <-> (" + right.toStringSpin() + ")";
+			break;
+		case NEXT:
+			rv = "X (" + left.toStringSpin() + ")";
+			break;
+		case FINALLY:
+			rv = "<> (" + left.toStringSpin() + ")";
+			break;
+		case GLOBALLY:
+			rv = "[] (" + left.toStringSpin() + ")";
+			break;
+		case NOT:
+			rv = "! (" + left.toStringSpin() + ")";
+			break;
+		case FALSE:
+			rv = "false";
+			break;
+		case TRUE:
+			rv = "true";
+			break;
+		case AP:
+			rv = ap;
+			break;
+		default:
+			rv = null;
+		}
+		return rv;
+	}
+
+	
+	/**
+	 * Render this LTL formula in Spot syntax.
+	 */
+	public String toStringSpot()
+	{
+		String rv = "";
+
+		switch (kind) {
+		case OR:
+			rv = "(" + left.toStringSpot() + ") | (" + right.toStringSpot() + ")";
+			break;
+		case AND:
+			rv = "(" + left.toStringSpot() + ") & (" + right.toStringSpot() + ")";
+			break;
+		case UNTIL:
+			rv = "(" + left.toStringSpot() + ") U (" + right.toStringSpot() + ")";
+			break;
+		case RELEASE:
+			rv = "(" + left.toStringSpot() + ") R (" + right.toStringSpot() + ")";
+			break;
+		case IMPLIES:
+			rv = "(" + left.toStringSpot() + ") -> (" + right.toStringSpot() + ")";
+			break;
+		case EQUIV:
+			rv = "(" + left.toStringSpot() + ") <-> (" + right.toStringSpot() + ")";
+			break;
+		case NEXT:
+			rv = "X (" + left.toStringSpot() + ")";
+			break;
+		case FINALLY:
+			rv = "F (" + left.toStringSpot() + ")";
+			break;
+		case GLOBALLY:
+			rv = "G (" + left.toStringSpot() + ")";
+			break;
+		case NOT:
+			rv = "! (" + left.toStringSpot() + ")";
+			break;
+		case FALSE:
+			rv = "false";
+			break;
+		case TRUE:
+			rv = "true";
+			break;
+		case AP:
+			rv = ap;
+			break;
+		default:
+			rv = null;
+		}
+		return rv;
+	}
+
 	public NBA toNBA(APSet apset) throws PrismException
 	{
 		Alternating a = new Alternating(this, apset);

prism/src/jltl2dstar/APMonom.java

@@ -67,7 +67,8 @@ public class APMonom {
 	 */
 	public boolean isSet(int index) throws PrismException {
 		if (!isNormal()) {
-			throw new PrismException("Can't get AP, is either TRUE/FALSE!");
+			// TRUE / FALSE -> the bit is not set
+			return false;
 		}
 		return bits_set.get(index);
 	}
@@ -77,7 +78,7 @@ public class APMonom {
 	 * @param index index of AP
 	 * @return <b>true</b> if AP is true
 	 */
-	boolean getValue(int index) throws PrismException {
+	public boolean getValue(int index) throws PrismException {
 		if (!isNormal()) {
 			throw new PrismException("Can't get AP, is either TRUE/FALSE!");
 		}

prism/src/prism/DA.java

@@ -5,6 +5,7 @@
 //	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford)
 //	* Hongyang Qu <hongyang.qu@cs.ox.ac.uk> (University of Oxford)
 //	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
+//	* David Mueller <david.mueller@tcs.inf.tu-dresden.de> (TU Dresden)
 //	
 //------------------------------------------------------------------------------
 //	
@@ -31,7 +32,11 @@ package prism;
 import java.io.PrintStream;
 import java.util.*;
 
+import jltl2ba.APElement;
+import jltl2ba.APElementIterator;
 import acceptance.AcceptanceOmega;
+import acceptance.AcceptanceRabin;
+import acceptance.AcceptanceType;
 
 /**
  * Class to store a deterministic automata of some acceptance type Acceptance.
@@ -107,6 +112,14 @@ public class DA<Symbol, Acceptance extends AcceptanceOmega>
 		this.start = start;
 	}
 
+	/**
+	 * Returns true if the automaton has an edge for {@code src} and {@label}.
+	 */
+	public boolean hasEdge(int src, Symbol label)
+	{
+		return edges.get(src).contains(label);
+	}
+	
 	/**
 	 * Add an edge
 	 */
@@ -200,6 +213,53 @@ public class DA<Symbol, Acceptance extends AcceptanceOmega>
 		}
 		out.println("}");
 	}
+	
+	/**
+	 * Print the DRA in ltl2dstar v2 format to the output stream.
+	 * @param out the output stream 
+	 */
+	public static void printLtl2dstar(DA<BitSet, AcceptanceRabin> dra, PrintStream out) throws PrismException {
+		AcceptanceRabin acceptance = dra.getAcceptance();
+
+		if (dra.getStartState() < 0) {
+			// No start state! 
+			throw new PrismException("No start state in DA!");
+		}
+
+		out.println("DRA v2 explicit");
+		out.println("States: " + dra.size());
+		out.println("Acceptance-Pairs: " + acceptance.size());
+		out.println("Start: " + dra.getStartState());
+
+		// Enumerate APSet
+		out.print("AP: " + dra.getAPList().size());
+		for (String ap : dra.getAPList()) {
+			out.print(" \"" + ap + "\"");
+		}
+		out.println();
+
+		out.println("---");
+
+		for (int i_state = 0; i_state < dra.size(); i_state++) {
+			out.println("State: " + i_state);
+
+			out.print("Acc-Sig:");
+			for (int pair = 0; pair < acceptance.size(); pair++) {
+				if (acceptance.get(pair).getL().get(i_state)) {
+					out.print(" -"+pair);
+				} else if (acceptance.get(pair).getK().get(i_state)) {
+					out.print(" +"+pair);
+				}
+			}
+			out.println();
+			
+			APElementIterator it = new APElementIterator(dra.apList.size());
+			while (it.hasNext()) {
+				APElement edge = it.next();
+				out.println(dra.getEdgeDestByLabel(i_state, edge));
+			}
+		}
+	}
 
 	/**
 	 * Print automaton to a PrismLog in a specified format ("dot" or "txt").

prism/src/prism/HOAF2DA.java

@@ -0,0 +1,548 @@
+//==============================================================================
+//	
+//	Copyright (c) 2014-
+//	Authors:
+//	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
+//	* David Mueller <david.mueller@tcs.inf.tu-dresden.de> (TU Dresden)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+
+package prism;
+
+import java.util.ArrayList;
+import java.util.BitSet;
+import java.util.List;
+import java.util.Set;
+
+import jhoafparser.ast.AtomAcceptance;
+import jhoafparser.ast.AtomLabel;
+import jhoafparser.ast.BooleanExpression;
+import jhoafparser.consumer.HOAConsumer;
+import jhoafparser.consumer.HOAConsumerException;
+import jhoafparser.util.ImplicitEdgeHelper;
+import jltl2ba.APElement;
+import jltl2ba.APSet;
+import jltl2dstar.APMonom;
+import jltl2dstar.APMonom2APElements;
+import acceptance.AcceptanceGenRabin;
+import acceptance.AcceptanceGenRabin.GenRabinPair;
+import acceptance.AcceptanceGeneric;
+import acceptance.AcceptanceOmega;
+import acceptance.AcceptanceRabin;
+import acceptance.AcceptanceRabin.RabinPair;
+
+/**
+ * A HOAConsumer for jhoafparser that constructs a prism.DA from the parsed automaton.
+ */
+public class HOAF2DA implements HOAConsumer {
+
+	public class TransitionBasedAcceptanceException extends HOAConsumerException {
+		public TransitionBasedAcceptanceException(String e) {super(e);}
+	}
+
+	private DA<BitSet, ? extends AcceptanceOmega> da;
+	private APSet aps = new APSet();
+
+	/** Size, i.e. number of states */
+	private int size;
+	private boolean knowSize = false;
+	
+	/** Start state (index) */
+	private int startState;
+	private boolean knowStartState = false;
+	
+	private BooleanExpression<AtomAcceptance> accExpr = null;
+	private String accName;
+	private List<Object> extraInfo;
+	
+	private List<BitSet> acceptanceSets = null;
+	// set of acceptance set indizes where state membership has to be inverted
+	private Set<Integer> negateAcceptanceSetMembership = null;
+	private List<String> apList;
+
+	ImplicitEdgeHelper implicitEdgeHelper = null;
+	
+	public void clear() {
+		aps = new APSet();
+
+		implicitEdgeHelper = null;
+
+		size = 0;
+		knowSize = false;
+
+		startState = 0;
+		knowStartState = false;
+
+		accExpr = null;
+		accName = null;
+		extraInfo = null;
+
+		acceptanceSets = null;
+		negateAcceptanceSetMembership = null;
+		apList = null;
+	}
+
+	public HOAF2DA() {
+	}
+	
+	@Override
+	public boolean parserResolvesAliases() {
+		return true;
+	}
+
+	@Override
+	public void notifyHeaderStart(String version) throws HOAConsumerException {
+		// NOP
+	}
+
+	@Override
+	public void setNumberOfStates(int numberOfStates)
+			throws HOAConsumerException {
+		size = numberOfStates;
+		knowSize = true;
+	}
+
+	@Override
+	public void addStartStates(List<Integer> stateConjunction)
+			throws HOAConsumerException {
+		if(stateConjunction.size() > 1 || knowStartState) {
+			throw new HOAConsumerException("Not a deterministic automaton: More then one Start state");
+		}
+		startState = stateConjunction.get(0).intValue();
+		knowStartState = true;
+	}
+
+	@Override
+	public void addAlias(String name, BooleanExpression<AtomLabel> labelExpr)
+			throws HOAConsumerException {
+		// NOP, aliases are already resolved
+	}
+
+	@Override
+	public void setAPs(List<String> aps) throws HOAConsumerException {
+		apList = aps;
+
+		for (String ap : aps) {
+			this.aps.addAP(ap);
+		}
+	}
+
+	@Override
+	public void setAcceptanceCondition(int numberOfSets,
+			BooleanExpression<AtomAcceptance> accExpr)
+			throws HOAConsumerException {
+		this.accExpr = accExpr;
+	}
+
+	@Override
+	public void provideAcceptanceName(String name, List<Object> extraInfo)
+			throws HOAConsumerException {
+		accName = name;
+		this.extraInfo = extraInfo;
+	}
+
+	@Override
+	public void setName(String name) throws HOAConsumerException {
+		// NOP
+	}
+
+	@Override
+	public void setTool(String name, String version) throws HOAConsumerException {
+		// NOP
+	}
+
+	@Override
+	public void addProperties(List<String> properties)
+			throws HOAConsumerException {
+		if(!properties.contains("deterministic")) {
+			// we don't know yet whether the automaton is actually deterministic...
+		}
+		if(properties.contains("univ-branch")) {
+			throw new HOAConsumerException("A HOAF with universal branching is not deterministic");
+		}
+		
+		if(properties.contains("state-labels")) {
+			throw new HOAConsumerException("Can't handle state labelling");
+		}
+	}
+
+	@Override
+	public void addMiscHeader(String name, List<Object> content)
+			throws HOAConsumerException {
+		if (name.substring(0,1).toUpperCase().equals(name.substring(0,1))) {
+			throw new HOAConsumerException("Unknown header "+name+" potentially containing semantic information, can not handle");
+		}
+	}
+
+	@Override
+	public void notifyBodyStart() throws HOAConsumerException {
+		if (!knowSize) {
+			throw new HOAConsumerException("Can currently only parse automata where the number of states is specified in the header");
+		}
+		if (!knowStartState) {
+			throw new HOAConsumerException("Not a deterministic automaton: No initial state specified (Start header)");
+		}
+		if (startState >= size) {
+			throw new HOAConsumerException("Initial state "+startState+" is out of range");
+		}
+
+		da = new DA<BitSet,AcceptanceGeneric>(size);
+		da.setStartState(startState);
+
+		if (apList == null) {
+			// no call to setAPs
+			apList = new ArrayList<String>(0);
+		}
+		da.setAPList(apList);
+		implicitEdgeHelper = new ImplicitEdgeHelper(apList.size());
+		
+		DA.switchAcceptance(da, prepareAcceptance());
+	}
+
+	/**
+	 * Prepare an acceptance condition for the parsed automaton.
+	 * Called in notifyBodyStart()
+	 **/
+	private AcceptanceOmega prepareAcceptance() throws HOAConsumerException
+	{
+		if (accName != null) {
+			if (accName.equals("Rabin")) {
+				return prepareAcceptanceRabin();
+			} else if (accName.equals("generalized-Rabin")) {
+				return prepareAcceptanceGenRabin();
+			}
+		}
+		
+		acceptanceSets = new ArrayList<BitSet>();
+		return prepareAcceptanceGeneric(accExpr);
+	}
+
+	/**
+	 * Prepare a generic acceptance condition for the parsed automaton.
+	 **/
+	private AcceptanceGeneric prepareAcceptanceGeneric(BooleanExpression<AtomAcceptance> expr) throws HOAConsumerException
+	{
+		switch (expr.getType()) {
+		case EXP_TRUE:
+			return new AcceptanceGeneric(true);
+		case EXP_FALSE:
+			return new AcceptanceGeneric(false);
+		case EXP_AND:
+			return new AcceptanceGeneric(AcceptanceGeneric.ElementType.AND,
+                    prepareAcceptanceGeneric(expr.getLeft()),
+                    prepareAcceptanceGeneric(expr.getRight()));
+		case EXP_OR:
+			return new AcceptanceGeneric(AcceptanceGeneric.ElementType.OR,
+                    prepareAcceptanceGeneric(expr.getLeft()),
+                    prepareAcceptanceGeneric(expr.getRight()));
+		case EXP_NOT:
+			throw new HOAConsumerException("Boolean negation not allowed in acceptance expression");
+		case EXP_ATOM: {
+			int index = expr.getAtom().getAcceptanceSet();
+			while (index >= acceptanceSets.size()) {
+				// ensure that the acceptanceSets array is large enough
+				acceptanceSets.add(null);
+			}
+			if (acceptanceSets.get(index) == null) {
+				// this acceptance set index has not been seen yet, create BitSet
+				acceptanceSets.set(index, new BitSet());
+			}
+			BitSet acceptanceSet = acceptanceSets.get(index);
+			switch (expr.getAtom().getType()) {
+			case TEMPORAL_FIN:
+				if (expr.getAtom().isNegated()) {
+					return new AcceptanceGeneric(AcceptanceGeneric.ElementType.FIN_NOT, acceptanceSet);
+				} else {
+					return new AcceptanceGeneric(AcceptanceGeneric.ElementType.FIN, acceptanceSet);
+				}
+			case TEMPORAL_INF:
+				if (expr.getAtom().isNegated()) {
+					return new AcceptanceGeneric(AcceptanceGeneric.ElementType.INF_NOT, acceptanceSet);
+				} else {
+					return new AcceptanceGeneric(AcceptanceGeneric.ElementType.INF, acceptanceSet);
+				}
+			}
+		}
+		}
+
+		throw new UnsupportedOperationException("Unknown operator in acceptance condition: "+expr);
+	}
+
+	/**
+	 * Prepare a Rabin acceptance condition from the acc-name header.
+	 */
+	private AcceptanceRabin prepareAcceptanceRabin() throws HOAConsumerException
+	{
+		if (extraInfo.size() != 1 ||
+		    !(extraInfo.get(0) instanceof Integer)) {
+			throw new HOAConsumerException("Invalid acc-name: Rabin header");
+		}
+
+		int numberOfPairs = (Integer)extraInfo.get(0);
+		AcceptanceRabin acceptanceRabin = new AcceptanceRabin();
+		acceptanceSets = new ArrayList<BitSet>(numberOfPairs*2);
+		for (int i = 0; i< numberOfPairs; i++) {
+			BitSet L = new BitSet();
+			BitSet K = new BitSet();
+
+			acceptanceSets.add(L);   // 2*i   = Fin(L) = F G !L
+			acceptanceSets.add(K);   // 2*i+1 = Inf(K) = G F  K
+
+			acceptanceRabin.add(new RabinPair(L,K));
+		}
+
+		return acceptanceRabin;
+	}
+
+	/**
+	 * Prepare a Generalized Rabin acceptance condition from the acc-name header.
+	 */
+	private AcceptanceGenRabin prepareAcceptanceGenRabin() throws HOAConsumerException
+	{
+		if (extraInfo.size() < 1 ||
+		    !(extraInfo.get(0) instanceof Integer)) {
+			throw new HOAConsumerException("Invalid acc-name: generalized-Rabin header");
+		}
+
+		int numberOfPairs = (Integer)extraInfo.get(0);
+		if (extraInfo.size() != numberOfPairs + 1) {
+			throw new HOAConsumerException("Invalid acc-name: generalized-Rabin header");
+		}
+		int numberOfKs[] = new int[numberOfPairs];
+		for (int i = 0; i < numberOfPairs; i++) {
+			if (!(extraInfo.get(i + 1) instanceof Integer)) {
+				throw new HOAConsumerException("Invalid acc-name: generalized-Rabin header");
+			}
+			numberOfKs[i] = (Integer) extraInfo.get(i + 1);
+		}
+		
+		AcceptanceGenRabin acceptanceGenRabin = new AcceptanceGenRabin();
+		acceptanceSets = new ArrayList<BitSet>(numberOfPairs*2);
+		for (int i = 0; i< numberOfPairs; i++) {
+			BitSet L = new BitSet();
+			acceptanceSets.add(L);   // Fin(L) = F G !L
+			ArrayList<BitSet> K_list = new ArrayList<BitSet>();
+			for (int j = 0; j < numberOfKs[i]; j++) {
+				BitSet K_j = new BitSet();
+				K_list.add(K_j);
+				acceptanceSets.add(K_j);   // Inf(K_j) = G F  K_j
+			}
+			acceptanceGenRabin.add(new GenRabinPair(L, K_list));
+		}
+
+		return acceptanceGenRabin;
+	}
+
+	@Override
+	public void addState(int id, String info,
+			BooleanExpression<AtomLabel> labelExpr, List<Integer> accSignature)
+			throws HOAConsumerException {
+		implicitEdgeHelper.startOfState(id);
+
+		if(labelExpr != null) {
+			throw new HOAConsumerException("State "+id+" has a state label, currently only supports labels on transitions");
+		}
+		
+		if (id >= size) {
+			throw new HOAConsumerException("Illegal state index "+id+", out of range");
+		}
+
+		if (accSignature != null) {
+			for (int index : accSignature) {
+				if (index >= acceptanceSets.size()) {
+					// acceptance set index not used in acceptance condition, ignore
+				}
+				BitSet accSet = acceptanceSets.get(index);
+				if (accSet == null) {
+					// acceptance set index not used in acceptance condition, ignore
+				} else {
+					accSet.set(id);
+				}
+			}
+		}
+	}
+
+	@Override
+	public void addEdgeImplicit(int stateId, List<Integer> conjSuccessors,
+			List<Integer> accSignature) throws HOAConsumerException {
+		if (conjSuccessors.size() != 1) {
+			throw new HOAConsumerException("Not a DA, state "+stateId+" has transition with conjunctive target");
+		}
+
+		if (accSignature != null) {
+			throw new TransitionBasedAcceptanceException("DA has transition-based acceptance (state "+stateId+", currently only state-labeled acceptance is supported");
+		}
+
+		int to = conjSuccessors.get(0);
+
+		BitSet edge = new BitSet();
+		long tmp = implicitEdgeHelper.nextImplicitEdge();
+		int index = 0;
+		while (tmp != 0) {
+			if (tmp % 2 == 1) {
+				edge.set(index);
+			}
+			tmp = tmp >> 1L;
+			index++;
+		}
+		da.addEdge(stateId, edge, to);
+	}
+	
+	/**
+	 * Returns a list of APMonoms for the expression. The expression currently has to be in
+	 * disjunctive normal form. Returns one APMonom for each clause of the DNF.
+	 */
+	private List<APMonom> labelExpressionToAPMonom(BooleanExpression<AtomLabel> expr) throws HOAConsumerException {
+		List<APMonom> result = new ArrayList<APMonom>();
+		
+		switch (expr.getType()) {
+		case EXP_AND:
+		case EXP_ATOM:
+		case EXP_NOT: {
+			APMonom monom = new APMonom();
+			labelExpressionToAPMonom(expr, monom);
+			result.add(monom);
+			return result;
+		}
+		case EXP_TRUE:
+			result.add(new APMonom(true));
+			return result;
+		case EXP_FALSE:
+			result.add(new APMonom(false));
+		case EXP_OR:
+			result.addAll(labelExpressionToAPMonom(expr.getLeft()));
+			result.addAll(labelExpressionToAPMonom(expr.getRight()));
+			return result;
+		}
+		throw new UnsupportedOperationException("Unsupported operator in label expression: "+expr);
+	}
+
+	
+	/**
+	 * Returns a single APMonom for a single clause of the overall DNF formula.
+	 * Modifies APMonom result such that in the end it is correct.
+	 */
+	private void labelExpressionToAPMonom(BooleanExpression<AtomLabel> expr, APMonom result) throws HOAConsumerException {
+		try {
+			switch (expr.getType()) {
+			case EXP_TRUE:
+			case EXP_FALSE:
+			case EXP_OR:
+				throw new HOAConsumerException("Complex transition labels are not yet supported, only disjunctive normal form: "+expr);
+
+			case EXP_AND:
+				labelExpressionToAPMonom(expr.getLeft(), result);
+				labelExpressionToAPMonom(expr.getRight(), result);
+				return;
+			case EXP_ATOM: {
+				int apIndex = expr.getAtom().getAPIndex();
+				if (result.isSet(apIndex) && result.getValue(apIndex)!=true) {
+					throw new HOAConsumerException("Complex transition labels are not yet supported, transition label evaluates to false");
+				}
+				result.setValue(apIndex, true);
+				return;
+			}
+			case EXP_NOT: {
+				if (!expr.getLeft().isAtom()) {
+					throw new HOAConsumerException("Complex transition labels are not yet supported, only conjunction of (negated) labels");
+				}
+				int apIndex = expr.getLeft().getAtom().getAPIndex();
+				if (result.isSet(apIndex) && result.getValue(apIndex)!=false) {
+					throw new HOAConsumerException("Complex transition labels are not yet supported, transition label evaluates to false");
+				}
+				result.setValue(apIndex, false);
+				return;
+			}
+			}
+		} catch (PrismException e) {
+			throw new HOAConsumerException("While parsing, APMonom exception: "+e.getMessage());
+		}
+	}
+	
+	@Override
+	public void addEdgeWithLabel(int stateId,
+			BooleanExpression<AtomLabel> labelExpr,
+			List<Integer> conjSuccessors, List<Integer> accSignature)
+			throws HOAConsumerException {
+
+		if (conjSuccessors.size() != 1) {
+			throw new HOAConsumerException("Not a DA, state "+stateId+" has transition with conjunctive target");
+		}
+
+		if (accSignature != null) {
+			throw new TransitionBasedAcceptanceException("DA has transition-based acceptance (state "+stateId+", currently only state-labeled acceptance is supported");
+		}
+
+		if (labelExpr == null) {
+			throw new HOAConsumerException("Missing label on transition");
+		}
+
+		int to = conjSuccessors.get(0);
+
+		for (APMonom monom : labelExpressionToAPMonom(labelExpr)) {
+			APMonom2APElements it = new APMonom2APElements(aps, monom);
+			while(it.hasNext()) {
+				APElement el = it.next();
+				if (da.hasEdge(stateId, el)) {
+					throw new HOAConsumerException("Not a deterministic automaton, non-determinism detected (state "+stateId+")");
+				}
+				da.addEdge(stateId, el, to);
+			}
+		}
+	}
+
+	@Override
+	public void notifyEndOfState(int stateId) throws HOAConsumerException
+	{
+		implicitEdgeHelper.endOfState();
+	}
+
+	@Override
+	public void notifyEnd() throws HOAConsumerException {
+		// flip acceptance sets that need negating
+		if (negateAcceptanceSetMembership != null) {
+			for (int index : negateAcceptanceSetMembership) {
+				acceptanceSets.get(index).flip(0, size);
+			}
+		}
+
+		clear();
+	}
+
+	@Override
+	public void notifyAbort() {
+		clear();
+		
+	}
+	
+	public DA<BitSet,? extends AcceptanceOmega> getDA() {
+		return da;
+	}
+
+	@Override
+	public void notifyWarning(String warning) throws HOAConsumerException
+	{
+		// warnings are fatal
+		throw new HOAConsumerException(warning);
+	}
+
+}

prism/src/prism/LTL2DA.java

@@ -27,11 +27,24 @@
 
 package prism;
 
+import java.io.File;
+import java.io.FileInputStream;
+import java.io.FileWriter;
+import java.io.IOException;
+import java.io.InputStream;
+import java.util.ArrayList;
 import java.util.BitSet;
+import java.util.List;
 
 import acceptance.AcceptanceOmega;
 import acceptance.AcceptanceRabin;
 import acceptance.AcceptanceType;
+import jhoafparser.consumer.HOAIntermediateStoreAndManipulate;
+import jhoafparser.parser.HOAFParser;
+import jhoafparser.parser.generated.ParseException;
+import jhoafparser.transformations.ToStateAcceptance;
+import jltl2ba.APSet;
+import jltl2ba.SimpleLTL;
 import jltl2dstar.LTL2Rabin;
 import parser.Values;
 import parser.ast.Expression;
@@ -70,7 +83,15 @@ public class LTL2DA extends PrismComponent
 	public DA<BitSet,? extends AcceptanceOmega> convertLTLFormulaToDA(Expression ltl, Values constants, AcceptanceType... allowedAcceptance) throws PrismException
 	{
 		DA<BitSet, ? extends AcceptanceOmega> result = null;
-		if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.RABIN)) {
+		
+		boolean useExternal = useExternal();
+		boolean containsTemporalBounds = Expression.containsTemporalTimeBounds(ltl);
+		if (containsTemporalBounds) {
+			useExternal = false;
+		}
+
+		if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.RABIN) &&
+		    !useExternal) {
 			// If we may construct a Rabin automaton, check the library first
 			try {
 				result = LTL2RabinLibrary.getDRAforLTL(ltl, constants);
@@ -84,9 +105,13 @@ public class LTL2DA extends PrismComponent
 		}
 
 		// TODO (JK): support generation of DSA for simple path formula with time bound
-		if (result == null && !Expression.containsTemporalTimeBounds(ltl)) {
-			// use jltl2dstar LTL2DA
-			result = LTL2Rabin.ltl2da(ltl.convertForJltl2ba(), allowedAcceptance);
+		if (result == null && !containsTemporalBounds) {
+			if (useExternal) {
+				result = convertLTLFormulaToDAWithExternalTool(ltl, constants, allowedAcceptance);
+			} else {
+				// use jltl2dstar LTL2DA
+				result = LTL2Rabin.ltl2da(ltl.convertForJltl2ba(), allowedAcceptance);
+			}
 		}
 
 		if (result == null) {
@@ -97,4 +122,186 @@ public class LTL2DA extends PrismComponent
 
 		return result;
 	}
+
+	public DA<BitSet,? extends AcceptanceOmega> convertLTLFormulaToDAWithExternalTool(Expression ltl, Values constants, AcceptanceType... allowedAcceptance) throws PrismException
+	{
+		String ltl2daTool = getSettings().getString(PrismSettings.PRISM_LTL2DA_TOOL);
+
+		SimpleLTL ltlFormula = ltl.convertForJltl2ba();
+		
+		// switch from the L0, L1, ... APs of PRISM to the
+		// safer p0, p1, ... APs for the external tool
+		SimpleLTL ltlFormulaSafeAP = ltlFormula.clone();
+		ltlFormulaSafeAP.renameAP("L", "p");
+
+		DA<BitSet, ? extends AcceptanceOmega> result = null;
+
+		try {
+			
+			String syntax = getSettings().getString(PrismSettings.PRISM_LTL2DA_SYNTAX);
+			if (syntax == null || syntax.isEmpty()) {
+				throw new PrismException("No LTL syntax option provided");
+			}
+			String ltlOutput;
+			switch (syntax) {
+			case "LBT":
+				ltlOutput = ltlFormulaSafeAP.toStringLBT();
+				break;
+			case "Spin":
+				ltlOutput = ltlFormulaSafeAP.toStringSpin();
+				break;
+			case "Spot":
+				ltlOutput = ltlFormulaSafeAP.toStringSpot();
+				break;
+			case "Rabinizer":
+				ltlFormulaSafeAP = ltlFormulaSafeAP.toBasicOperators();
+				ltlOutput = ltlFormulaSafeAP.toStringSpot();
+				break;
+			default:
+				throw new PrismException("Unknown LTL syntax option \""+syntax+"\"");
+			}
+
+			File ltl_file=File.createTempFile("prism-ltl-external-", ".ltl", null);
+			File da_file=File.createTempFile("prism-ltl-external-",".hoa", null);
+			File tool_output=File.createTempFile("prism-ltl-external-",".output", null);
+
+			FileWriter ltlWriter = new FileWriter(ltl_file);
+			ltlWriter.write(ltlOutput);
+			ltlWriter.close();
+		
+			List<String> arguments = new ArrayList<String>();
+			arguments.add(ltl2daTool);
+
+			getLog().print("Calling external LTL->DA tool: ");
+			for (String s : arguments) {
+				getLog().print(" " + s);
+			}
+			getLog().println();
+
+			getLog().print("LTL formula (in "+syntax+" syntax):  ");
+			getLog().println(ltlOutput);
+			getLog().println();
+
+			arguments.add(ltl_file.getAbsolutePath());
+			arguments.add(da_file.getAbsolutePath());
+		
+
+			ProcessBuilder builder = new ProcessBuilder(arguments);
+			builder.redirectOutput(tool_output);
+			builder.redirectErrorStream(true);
+
+			Process p = builder.start();
+			p.getInputStream().close();
+
+			int rv;
+			while (true) {
+				try {
+					rv = p.waitFor();
+					break;
+				} catch (InterruptedException e) {
+				}
+			}
+			if (rv != 0) {
+				throw new PrismException("Call to external LTL->DA tool failed, return value = "+rv+".\n"
+						+"To investigate, please consult the following files:"
+						+"\n LTL formula:                     "+ltl_file.getAbsolutePath()
+						+"\n Automaton output:                "+da_file.getAbsolutePath()
+						+"\n Tool output (stdout and stderr): "+tool_output.getAbsolutePath()
+						+"\n");
+			}
+
+			tool_output.delete();
+
+		
+			try {
+				try {
+					HOAF2DA consumerDA = new HOAF2DA();
+
+					InputStream input = new FileInputStream(da_file);
+					HOAFParser.parseHOA(input, consumerDA);
+					result = consumerDA.getDA();
+				} catch (HOAF2DA.TransitionBasedAcceptanceException e) {
+					// try again, this time transforming to state acceptance
+					getLog().println("Automaton with transition-based acceptance, automatically converting to state-based acceptance...");
+					HOAF2DA consumerDA = new HOAF2DA();
+					HOAIntermediateStoreAndManipulate consumerTransform = new HOAIntermediateStoreAndManipulate(consumerDA, new ToStateAcceptance());
+
+					InputStream input = new FileInputStream(da_file);
+					HOAFParser.parseHOA(input, consumerTransform);
+					result = consumerDA.getDA();
+				}
+
+				if (result == null) {
+					throw new PrismException("Could not construct DA");
+				}
+				checkAPs(ltlFormulaSafeAP, result.getAPList());
+ 
+				// rename back from safe APs, i.e., p0, p1, ... to L0, L1, ...
+				List<String> automatonAPList = result.getAPList();
+				for (int i = 0; i < automatonAPList.size(); i++) {
+					if (automatonAPList.get(i).startsWith("p")) {
+						String renamed = "L" + automatonAPList.get(i).substring("p".length());
+						automatonAPList.set(i, renamed);
+					}
+				}
+			} catch (ParseException e) {
+				throw new PrismException("Parse error: "+e.getMessage()+".\n"
+						+"To investigate, please consult the following files:\n"
+						+" LTL formula:        "+ltl_file.getAbsolutePath()
+						+"\n Automaton output: "+da_file.getAbsolutePath()
+						+"\n");
+			} catch (PrismException e) {
+				throw new PrismException(e.getMessage()+".\n"
+						+"To investigate, please consult the following files:"
+						+"\n LTL formula: "     +ltl_file.getAbsolutePath()
+						+"\n Automaton output: "+da_file.getAbsolutePath()
+						+"\n");
+			}
+
+			da_file.delete();
+			ltl_file.delete();
+		} catch (IOException e) {
+			throw new PrismException(e.getMessage());
+		}
+
+		AcceptanceOmega acceptance = result.getAcceptance();
+		if (AcceptanceType.contains(allowedAcceptance, acceptance.getType())) {
+			return result;
+		} else if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.GENERIC)) {
+			// The specific acceptance type is not allowed, but GENERIC is allowed
+			//   -> transform to generic acceptance and switch acceptance condition
+			DA.switchAcceptance(result, acceptance.toAcceptanceGeneric());
+			return result;
+		} else {
+			throw new PrismException("The external LTL->DA tool returned an automaton with "+acceptance.getTypeName()+" acceptance, which is not yet supported for model checking this model / property");
+		}
+	}
+	
+	/** Check whether we should use an external LTL->DA tool */
+	private boolean useExternal()
+	{
+		String ltl2da_tool = getSettings().getString(PrismSettings.PRISM_LTL2DA_TOOL);
+		if (ltl2da_tool!=null && !ltl2da_tool.isEmpty()) {
+			return true;
+		}
+		return false;
+	}
+	
+	private void checkAPs(SimpleLTL ltl, List<String> automatonAPs) throws PrismException
+	{
+		APSet ltlAPs = ltl.getAPs();
+		for (String ap : ltlAPs) {
+			if (!automatonAPs.contains(ap)) {
+				throw new PrismException("Generated automaton misses atomic proposition \""+ap+"\"");
+			}
+		}
+		for (String ap : automatonAPs) {
+			if (!ltlAPs.hasAP(ap)) {
+				throw new PrismException("Generated automaton has extra atomic proposition \""+ap+"\"");
+			}
+		}
+	}
+
+	
+	
 }

prism/src/prism/LTLModelChecker.java

@@ -32,6 +32,7 @@ import java.util.BitSet;
 import java.util.List;
 import java.util.Vector;
 
+import acceptance.AcceptanceGenRabinDD;
 import acceptance.AcceptanceOmega;
 import acceptance.AcceptanceOmegaDD;
 import acceptance.AcceptanceRabin;
@@ -708,6 +709,8 @@ public class LTLModelChecker extends PrismComponent
 		switch (acceptance.getType()) {
 		case RABIN:
 			return findAcceptingECStatesForRabin((AcceptanceRabinDD) acceptance, model, daDDRowVars, daDDColVars, fairness);
+		case GENERALIZED_RABIN:
+			return findAcceptingECStatesForGeneralizedRabin((AcceptanceGenRabinDD) acceptance, model, daDDRowVars, daDDColVars, fairness);
 		default:
 			throw new PrismNotSupportedException("Computing the accepting EC states for "+acceptance.getTypeName()+" acceptance is not yet implemented (symbolic engine)");
 		}
@@ -852,6 +855,61 @@ public class LTLModelChecker extends PrismComponent
 		return allAcceptingStates;
 	}
 
+	/**
+	 * Find the set of states in accepting end components (ECs) in a nondeterministic model wrt a Generalized Rabin acceptance condition.
+	 * @param acceptance the Generalized 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
+	 * @param fairness Consider fairness?
+	 * @return A referenced BDD for the union of all states in accepting MECs
+	 */
+	public JDDNode findAcceptingECStatesForGeneralizedRabin(AcceptanceGenRabinDD acceptance, NondetModel model, JDDVars draDDRowVars, JDDVars draDDColVars, boolean fairness)
+			throws PrismException
+	{
+		
+		if (fairness) {
+			throw new PrismException("Accepting end-component computation for generalized Rabin is currently not supported with fairness");
+		}
+
+		JDDNode allAcceptingStates;
+
+		allAcceptingStates = JDD.Constant(0);
+
+		// Go through the GR acceptance pairs (L_i, K_i_1, ..., K_i_n) 
+		for (int i = 0; i < acceptance.size(); i++) {
+					
+			// Filter out L_i states from the model and find the MECs
+			JDDNode notL = JDD.Not(acceptance.get(i).getL());
+			JDD.Ref(model.getTrans01());
+			JDD.Ref(notL);
+			JDDNode candidateStates = JDD.Apply(JDD.TIMES, model.getTrans01(), notL);
+			notL = JDD.PermuteVariables(notL, draDDRowVars, draDDColVars);
+			candidateStates = JDD.Apply(JDD.TIMES, candidateStates,	notL);
+			candidateStates = JDD.ThereExists(candidateStates, model.getAllDDColVars());
+			candidateStates = JDD.ThereExists(candidateStates, model.getAllDDNondetVars());
+			List<JDDNode> mecs = findMECStates(model, candidateStates);
+			JDD.Deref(candidateStates);
+
+			// Check which MECs are accepting for this pair, calculate union
+			JDDNode acceptingStates = JDD.Constant(0);
+			for (int k = 0; k < mecs.size(); k++) {
+				// Is the induced BSCC by this MEC accepting?
+				// (note we only really need to check K_i_1, ..., K_i_n here, not L too,
+				// but this should not really affect efficiency)
+				if (acceptance.get(i).isBSCCAccepting(mecs.get(k))) {
+					acceptingStates = JDD.Or(acceptingStates, mecs.get(k));
+				} else {
+					JDD.Deref(mecs.get(k));
+				}
+			}
+			// Add to the set of accepting states for all pairs
+			allAcceptingStates = JDD.Or(allAcceptingStates, acceptingStates);
+		}
+
+		return allAcceptingStates;
+	}
+
 	public JDDNode findMultiAcceptingStates(DA<BitSet,AcceptanceRabin> dra, NondetModel model, JDDVars draDDRowVars, JDDVars draDDColVars, boolean fairness,
 			List<JDDNode> allecs, List<JDDNode> statesH, List<JDDNode> statesL) throws PrismException
 	{

prism/src/prism/NondetModelChecker.java

@@ -1007,6 +1007,7 @@ public class NondetModelChecker extends NonProbModelChecker
 		LTL2DA ltl2da = new LTL2DA(prism);
 		AcceptanceType[] allowedAcceptance = {
 				AcceptanceType.RABIN,
+				AcceptanceType.GENERALIZED_RABIN,
 				AcceptanceType.REACH
 		};
 		da = ltl2da.convertLTLFormulaToDA(ltl, constantValues, allowedAcceptance);

prism/src/prism/PrismSettings.java

@@ -113,6 +113,9 @@ public class PrismSettings implements Observer
 	public static final	String PRISM_PARETO_EPSILON					= "prism.paretoEpsilon";
 	public static final	String PRISM_EXPORT_PARETO_FILENAME			= "prism.exportParetoFileName";
 	
+	public static final String PRISM_LTL2DA_TOOL					= "prism.ltl2daTool";
+	public static final String PRISM_LTL2DA_SYNTAX					= "prism.ltl2daSyntax";
+	
 	public static final	String PRISM_PARAM_ENABLED					= "prism.param.enabled";
 	public static final	String PRISM_PARAM_PRECISION				= "prism.param.precision";
 	public static final	String PRISM_PARAM_SPLIT					= "prism.param.split";
@@ -304,6 +307,13 @@ public class PrismSettings implements Observer
 			{ STRING_TYPE,		PRISM_EXPORT_ADV_FILENAME,				"Adversary export filename",			"3.3",			"adv.tra",																	"",															
 																			"Name of file for MDP adversary export (if enabled)" },
 																		
+			// LTL2DA TOOLS
+			{ STRING_TYPE,		PRISM_LTL2DA_TOOL,						"Use external LTL->DA tool",		"4.2.1",			"",		null,
+																			"If non-empty, the path to the executable for the external LTL->DA tool."},
+
+			{ STRING_TYPE,		PRISM_LTL2DA_SYNTAX,					"LTL syntax for external LTL->DA tool",		"4.2.1",			"LBT",		"LBT,Spin,Spot,Rabinizer",
+																			"The syntax for LTL formulas passed to the external LTL->DA tool."},
+
 			// PARAMETRIC MODEL CHECKING
 			{ BOOLEAN_TYPE,		PRISM_PARAM_ENABLED,					"Do parametric model checking",			"4.1",			new Boolean(false),															"",
 																			"Perform parametric model checking." },
@@ -1265,6 +1275,40 @@ public class PrismSettings implements Observer
 			}
 		}
 		
+		// LTL2DA TOOLS
+		
+		else if (sw.equals("ltl2datool")) {
+			if (i < args.length - 1) {
+				String filename = args[++i];
+				set(PRISM_LTL2DA_TOOL, filename);
+				System.out.println(getString(PRISM_LTL2DA_TOOL));
+			} else {
+				throw new PrismException("The -" + sw + " switch requires one argument (path to the executable)");
+			}
+		}
+		else if (sw.equals("ltl2dasyntax")) {
+			if (i < args.length - 1) {
+				String syntax = args[++i];
+				switch (syntax) {
+				case "lbt":
+					set(PRISM_LTL2DA_SYNTAX, "LBT");
+					break;
+				case "spin":
+					set(PRISM_LTL2DA_SYNTAX, "Spin");
+					break;
+				case "spot":
+					set(PRISM_LTL2DA_SYNTAX, "Spot");
+				case "rabinizer":
+					set(PRISM_LTL2DA_SYNTAX, "Rabinizer");
+					break;
+				default:
+					throw new PrismException("Unrecognised option for -" + sw + " switch (options are: lbt, spin, spot, rabinizer)");
+				}
+			} else {
+				throw new PrismException("The -" + sw + " switch requires one argument (options are: lbt, spin, spot, rabinizer)");
+			}
+		}
+
 		// PARAMETRIC MODEL CHECKING:
 		
 		else if (sw.equals("param")) {
@@ -1567,6 +1611,9 @@ public class PrismSettings implements Observer
 		mainLog.println("-pathviaautomata ............... Handle all path formulas via automata constructions");
 		mainLog.println("-exportadv <file> .............. Export an adversary from MDP model checking (as a DTMC)");
 		mainLog.println("-exportadvmdp <file> ........... Export an adversary from MDP model checking (as an MDP)");
+		mainLog.println("-ltl2datool <exec> ............. Run executable <exec> to convert LTL formulas to deterministic automata");
+		mainLog.println("-ltl2dasyntax <x> .............. Specify output format for -ltl2datool switch (lbt, spin, spot, rabinizer)");
+		
 		mainLog.println();
 		mainLog.println("MULTI-OBJECTIVE MODEL CHECKING:");
 		mainLog.println("-linprog (or -lp) .............. Use linear programming for multi-objective model checking");

prism/src/prism/ProbModelChecker.java

@@ -541,7 +541,8 @@ public class ProbModelChecker extends NonProbModelChecker
 		LTL2DA ltl2da = new LTL2DA(prism);
 		AcceptanceType[] allowedAcceptance = {
 				AcceptanceType.RABIN,
-				AcceptanceType.REACH
+				AcceptanceType.REACH,
+				AcceptanceType.GENERIC
 		};
 		da = ltl2da.convertLTLFormulaToDA(ltl, constantValues, allowedAcceptance);
 		mainLog.println(da.getAutomataType()+" has " + da.size() + " states, " + da.getAcceptance().getSizeStatistics() + ".");