diff --git a/prism/src/acceptance/AcceptanceGenRabin.java b/prism/src/acceptance/AcceptanceGenRabin.java
index b578f44c..17ba5d9b 100644
--- a/prism/src/acceptance/AcceptanceGenRabin.java
+++ b/prism/src/acceptance/AcceptanceGenRabin.java
@@ -27,6 +27,7 @@
 
 package acceptance;
 
+import java.io.PrintStream;
 import java.util.ArrayList;
 import java.util.BitSet;
 
@@ -333,4 +334,35 @@ public class AcceptanceGenRabin
 	{
 		return "Generalized Rabin";
 	}
+
+	@Override
+	public void outputHOAHeader(PrintStream out)
+	{
+		int sets = 0;
+		out.print("acc-name: generalized-Rabin "+size());
+		for (GenRabinPair pair : this) {
+			sets++;  // the Fin
+			out.print(" "+pair.getNumK());
+			sets += pair.getNumK();
+		}
+		out.println();
+		out.print("Acceptance: " + sets);
+		if (sets == 0) {
+			out.println("f");
+			return;
+		}
+
+		int set_index = 0;
+		for (GenRabinPair pair : this) {
+			if (set_index > 0) out.print(" | ");
+			out.print("( Fin(" + set_index + ")");
+			set_index++;
+			for (int i = 0; i < pair.getNumK(); i++) {
+				out.print(" & Inf(" + set_index +")");
+				set_index++;
+			}
+			out.print(")");
+		}
+		out.println();
+	}
 }
diff --git a/prism/src/acceptance/AcceptanceGeneric.java b/prism/src/acceptance/AcceptanceGeneric.java
index 56a78e77..10cd934f 100644
--- a/prism/src/acceptance/AcceptanceGeneric.java
+++ b/prism/src/acceptance/AcceptanceGeneric.java
@@ -27,6 +27,7 @@
 
 package acceptance;
 
+import java.io.PrintStream;
 import java.util.ArrayList;
 import java.util.BitSet;
 import java.util.Collections;
@@ -363,5 +364,53 @@ public class AcceptanceGeneric implements AcceptanceOmega {
 		}
 	}
 
+	@Override
+	public void outputHOAHeader(PrintStream out)
+	{
+		List<AcceptanceGeneric> leafNodes = getLeafNodes();
+		out.print("Acceptance: "+leafNodes.size()+" ");
+		outputHOAFormula(out, 0);
+		out.println();
+	}
+
+	private int outputHOAFormula(PrintStream out, int nextSetIndex)
+	{
+		switch (kind) {
+		case AND:
+			out.print("(");
+			nextSetIndex = left.outputHOAFormula(out, nextSetIndex);
+			out.print(")&(");
+			nextSetIndex = right.outputHOAFormula(out, nextSetIndex);
+			out.print(")");
+			return nextSetIndex;
+		case OR:
+			out.print("(");
+			nextSetIndex = left.outputHOAFormula(out, nextSetIndex);
+			out.print(")|(");
+			nextSetIndex = right.outputHOAFormula(out, nextSetIndex);
+			out.print(")");
+			return nextSetIndex;
+		case TRUE:
+			out.print("t");
+			return nextSetIndex;
+		case FALSE:
+			out.print("f");
+			return nextSetIndex;
+		case FIN:
+			out.print("Fin("+nextSetIndex+")");
+			return nextSetIndex+1;
+		case FIN_NOT:
+			out.print("Fin(!"+nextSetIndex+")");
+			return nextSetIndex+1;
+		case INF:
+			out.print("Inf("+nextSetIndex+")");
+			return nextSetIndex+1;
+		case INF_NOT:
+			out.print("Inf(!"+nextSetIndex+")");
+			return nextSetIndex+1;
+		}
+		throw new UnsupportedOperationException("Unknown kind");
+	}
+
 
 }
diff --git a/prism/src/acceptance/AcceptanceOmega.java b/prism/src/acceptance/AcceptanceOmega.java
index 2ed9700b..2d7fea54 100644
--- a/prism/src/acceptance/AcceptanceOmega.java
+++ b/prism/src/acceptance/AcceptanceOmega.java
@@ -26,6 +26,7 @@
 
 package acceptance;
 
+import java.io.PrintStream;
 import java.util.BitSet;
 
 import prism.PrismException;
@@ -66,6 +67,9 @@ public interface AcceptanceOmega extends Cloneable
 	/** Returns a full name for this acceptance condition */
 	public String getTypeName();
 
+	/** Print the appropriate Acceptance (and potentially acc-name) header */
+	public void outputHOAHeader(PrintStream out);
+
 	/** Make a copy of the acceptance condition. */
 	public AcceptanceOmega clone();
 
diff --git a/prism/src/acceptance/AcceptanceRabin.java b/prism/src/acceptance/AcceptanceRabin.java
index f9ea6acf..322d5bc9 100644
--- a/prism/src/acceptance/AcceptanceRabin.java
+++ b/prism/src/acceptance/AcceptanceRabin.java
@@ -26,6 +26,7 @@
 
 package acceptance;
 
+import java.io.PrintStream;
 import java.util.ArrayList;
 import java.util.BitSet;
 
@@ -317,4 +318,21 @@ public class AcceptanceRabin
 	{
 		return "Rabin";
 	}
+
+	@Override
+	public void outputHOAHeader(PrintStream out)
+	{
+		out.println("acc-name: Rabin "+size());
+		out.print("Acceptance: " + (size()*2)+" ");
+		if (size() == 0) {
+			out.println("f");
+			return;
+		}
+
+		for (int pair = 0; pair < size(); pair++) {
+			if (pair > 0) out.print(" | ");
+			out.print("( Fin(" + 2*pair + ") & Inf(" + (2*pair+1) +") )");
+		}
+		out.println();
+	}
 }
diff --git a/prism/src/acceptance/AcceptanceReach.java b/prism/src/acceptance/AcceptanceReach.java
index 19993c60..f566e8c1 100644
--- a/prism/src/acceptance/AcceptanceReach.java
+++ b/prism/src/acceptance/AcceptanceReach.java
@@ -26,6 +26,7 @@
 
 package acceptance;
 
+import java.io.PrintStream;
 import java.util.BitSet;
 
 import prism.PrismException;
@@ -192,4 +193,10 @@ public class AcceptanceReach implements AcceptanceOmega
 		return "Finite";
 	}
 
+	@Override
+	public void outputHOAHeader(PrintStream out)
+	{
+		out.println("acc-name: Buchi");
+		out.println("Acceptance: 1 Inf(0)");
+	}
 }
diff --git a/prism/src/acceptance/AcceptanceStreett.java b/prism/src/acceptance/AcceptanceStreett.java
index 9376f75c..28cd9d32 100644
--- a/prism/src/acceptance/AcceptanceStreett.java
+++ b/prism/src/acceptance/AcceptanceStreett.java
@@ -26,6 +26,7 @@
 
 package acceptance;
 
+import java.io.PrintStream;
 import java.util.ArrayList;
 import java.util.BitSet;
 
@@ -319,4 +320,21 @@ public class AcceptanceStreett
 	{
 		return "Streett";
 	}
+
+	@Override
+	public void outputHOAHeader(PrintStream out)
+	{
+		out.println("acc-name: Streett "+size());
+		out.print("Acceptance: " + (size()*2)+" ");
+		if (size() == 0) {
+			out.println("t");
+			return;
+		}
+
+		for (int pair = 0; pair < size(); pair++) {
+			if (pair > 0) out.print(" & ");
+			out.print("( Fin(" + (2*pair) + ") | Inf(" + (2*pair+1) +") )");
+		}
+		out.println();
+	}
 }