jltl2dstar.DA: printHOA

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

prism/src/jltl2dstar/DA.java

@@ -25,9 +25,9 @@ import java.io.PrintStream;
 import java.util.*;
 
 import jltl2ba.APElement;
-import jltl2ba.APElementIterator;
 import jltl2ba.APSet;
 import prism.PrismException;
+import prism.PrismNotSupportedException;
 
 public class DA {
 
@@ -300,7 +300,39 @@ public class DA {
 			}
 		}
 	}
-	
+
+	/**
+	 * Print the DA in HOA format to the output stream.
+	 * This functions expects that the DA is compact.
+	 * @param da_type a string specifying the type of automaton ("DRA", "DSA").
+	 * @param out the output stream
+	 */
+	public void printHOA(String da_type, PrintStream out) throws PrismException {
+		if (!da_type.equals("DRA")) throw new PrismNotSupportedException("HOA printing for "+da_type+" currently not supported");
+
+		out.println("HOA: v1");
+		out.println("States: "+size());
+		_ap_set.print_hoa(out);
+		out.println("Start: "+getStartState().getName());
+		_acceptance.outputAcceptanceHeaderHOA(out);
+		out.println("properties: trans-labels explicit-labels state-acc no-univ-branch deterministic");
+		out.println("--BODY--");
+		for (DA_State state : _index) {
+			out.print("State: "+state.getName()+ " ");  // id
+			_acceptance.outputAcceptanceForStateHOA(out, state.getName());
+
+			for (Map.Entry<APElement, DA_State> edge : state.edges().entrySet()) {
+				APElement label = edge.getKey();
+				String labelString = "["+label.toStringHOA(_ap_set.size())+"]";
+				DA_State to = edge.getValue();
+				out.print(labelString);
+				out.print(" ");
+				out.println(to);
+			}
+		}
+		out.println("--END--");
+	}
+
 	/**
 	 * Print the DA in dot format to the output stream.
 	 * This functions expects that the DA is compact.

prism/src/jltl2dstar/RabinAcceptance.java

@@ -125,6 +125,26 @@ public class RabinAcceptance implements Iterable<Integer> {
 		out.println("Acceptance-Pairs: " + size());
 	}
 
+	/**
+	 * Print the Acceptance: header in the HOA format
+	 * @param out the output stream.
+	 */
+	public void outputAcceptanceHeaderHOA(PrintStream out) throws PrismException
+	{
+		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();
+	}
+
 	/**
 	 * Print the Acc-Sig: line for a state (part of interface AcceptanceCondition).
 	 * @param out the output stream.
@@ -143,6 +163,28 @@ public class RabinAcceptance implements Iterable<Integer> {
 		out.println();
 	}
 
+	/**
+	 * Print the acceptance signature for a state (HOA format)
+	 * @param out the output stream.
+	 * @param state_index the state
+	 */
+	public void outputAcceptanceForStateHOA(PrintStream out, int state_index) throws PrismException
+	{
+		String signature = "";
+		for (int pair_index = 0; pair_index < size(); pair_index++) {
+			if (isStateInAcceptance_L(pair_index, state_index)) {
+				signature += (!signature.isEmpty() ? " " :"")+(pair_index*2+1);
+			}
+			if (isStateInAcceptance_U(pair_index, state_index)) {
+				signature += (!signature.isEmpty() ? " " :"")+(pair_index*2);
+			}
+		}
+
+		if (!signature.isEmpty()) {
+			out.println("{" + signature + "}");
+		}
+	}
+
 	/**
 	 * Add a state (part of interface AcceptanceCondition).
 	 * @param state_index the index of the added state.