diff --git a/prism/src/automata/DA.java b/prism/src/automata/DA.java
index e97f8513..896f7aee 100644
--- a/prism/src/automata/DA.java
+++ b/prism/src/automata/DA.java
@@ -38,6 +38,7 @@ import jltl2ba.APElement;
 import jltl2ba.APElementIterator;
 import prism.PrismException;
 import prism.PrismLog;
+import prism.PrismNotSupportedException;
 import prism.PrismPrintStreamLog;
 import acceptance.AcceptanceOmega;
 import acceptance.AcceptanceRabin;
@@ -270,6 +271,43 @@ public class DA<Symbol, Acceptance extends AcceptanceOmega>
 		}
 	}
 
+	/**
+	 * Print the DA in HOA format to the output stream.
+	 * @param out the output stream
+	 */
+	public void printHOA(PrintStream out) throws PrismException {
+		out.println("HOA: v1");
+		out.println("States: "+size());
+		
+		// AP
+		out.print("AP: "+apList.size());
+		for (String ap : apList) {
+			// TODO(JK): Proper quoting
+			out.print(" \""+ap+"\"");
+		}
+		out.println();
+
+		out.println("Start: "+start);
+		acceptance.outputHOAHeader(out);
+		out.println("properties: trans-labels explicit-labels state-acc no-univ-branch deterministic");
+		out.println("--BODY--");
+		for (int i = 0; i < size(); i++) {
+			out.print("State: "+i+" ");  // id
+			out.println(acceptance.getSignatureForStateHOA(i));
+
+			for (Edge edge : edges.get(i)) {
+				Symbol label = edge.label;
+				if (!(label instanceof BitSet))
+					throw new PrismNotSupportedException("Can not print automaton with "+label.getClass()+" labels");
+				String labelString = "["+APElement.toStringHOA((BitSet)label, apList.size())+"]";
+				out.print(labelString);
+				out.print(" ");
+				out.println(edge.dest);
+			}
+		}
+		out.println("--END--");
+	}
+
 	/**
 	 * Print automaton to a PrismLog in a specified format ("dot" or "txt").
 	 */