From 622fe08f00faa3d9545daeb0010324e5849269a3 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 19 Nov 2014 16:38:14 +0100
Subject: [PATCH] ltlcross: add support for reading TGBA as HOA

* src/bin/ltlcross.cc: Add a %H modifier.
* src/tgbatest/ltlcross2.test: Exercise it.
---
 src/bin/ltlcross.cc         | 35 +++++++++++++++++++++++++++++++----
 src/tgbatest/ltlcross2.test | 14 +++++++-------
 2 files changed, 38 insertions(+), 11 deletions(-)

diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc
index 206c50ed7..04bb19e32 100644
--- a/src/bin/ltlcross.cc
+++ b/src/bin/ltlcross.cc
@@ -38,6 +38,7 @@
 #include "common_finput.hh"
 #include "neverparse/public.hh"
 #include "dstarparse/public.hh"
+#include "hoaparse/public.hh"
 #include "ltlast/unop.hh"
 #include "ltlvisit/tostring.hh"
 #include "ltlvisit/apcollect.hh"
@@ -709,7 +710,7 @@ namespace
     public spot::printable_value<spot::temporary_file*>
   {
     unsigned translator_num;
-    enum output_format { None, Spin, Lbtt, Dstar };
+    enum output_format { None, Spin, Lbtt, Dstar, Hoa };
     mutable output_format format;
 
     printable_result_filename()
@@ -744,6 +745,8 @@ namespace
 	format = Lbtt;
       else if (*pos == 'D')
 	format = Dstar;
+      else if (*pos == 'H')
+	format = Hoa;
       else
 	SPOT_UNREACHABLE();
 
@@ -752,7 +755,8 @@ namespace
 	  // It's OK to use a specified multiple time, but it's not OK
 	  // to mix the formats.
 	  if (format != old_format)
-	    error(2, 0, "you may not mix %%D, %%N, and %%T specifiers: %s",
+	    error(2, 0,
+		  "you may not mix %%D, %%H, %%N, and %%T specifiers: %s",
 		  translators[translator_num].spec);
 	}
       else
@@ -796,6 +800,7 @@ namespace
       declare('L', &filename_ltl_lbt);
       declare('W', &filename_ltl_wring);
       declare('D', &output);
+      declare('H', &output);
       declare('N', &output);
       declare('T', &output);
 
@@ -814,9 +819,9 @@ namespace
 		  "one of %%f,%%s,%%l,%%w,%%F,%%S,%%L,%%W to indicate how "
 		  "to pass the formula.", t.spec);
 	  bool has_d = has['D'];
-	  if (!(has_d || has['N'] || has['T']))
+	  if (!(has_d || has['N'] || has['T'] || has['H']))
 	    error(2, 0, "no output %%-sequence in '%s'.\n      Use one of "
-		  "%%D,%%N,%%T to indicate where the automaton is saved.",
+		  "%%D,%%H,%%N,%%T to indicate where the automaton is saved.",
 		  t.spec);
 	  has_sr |= has_d;
 
@@ -1034,6 +1039,28 @@ namespace
 		  }
 		break;
 	      }
+	    case printable_result_filename::Hoa:
+	      {
+		spot::hoa_parse_error_list pel;
+		std::string filename = output.val()->name();
+		auto aut = spot::hoa_parse(filename, pel, dict);
+		if (!pel.empty())
+		  {
+		    status_str = "parse error";
+		    problem = true;
+		    es = -1;
+		    std::ostream& err = global_error();
+		    err << "error: failed to parse the produced HOA file.\n";
+		    spot::format_hoa_parse_errors(err, filename, pel);
+		    end_error();
+		    res = nullptr;
+		  }
+		else
+		  {
+		    res = aut->aut;
+		  }
+		break;
+	      }
 	    case printable_result_filename::None:
 	      SPOT_UNREACHABLE();
 	    }
diff --git a/src/tgbatest/ltlcross2.test b/src/tgbatest/ltlcross2.test
index 43427c495..6d34a9983 100755
--- a/src/tgbatest/ltlcross2.test
+++ b/src/tgbatest/ltlcross2.test
@@ -27,19 +27,19 @@ ltl2tgba=../../bin/ltl2tgba
 ../../bin/ltlcross --products=3 --timeout=60 \
 "$ltl2tgba --lbtt --any --low %f > %T" \
 "$ltl2tgba --lbtt --any --medium %f > %T" \
-"$ltl2tgba --lbtt --any --high %f > %T" \
+"$ltl2tgba --hoa  --any --high %f > %H" \
 "$ltl2tgba --lbtt --deterministic --low %f > %T" \
 "$ltl2tgba --lbtt --deterministic --medium %f > %T" \
 "$ltl2tgba --lbtt --deterministic --high %f > %T" \
 "$ltl2tgba --lbtt --small --low %f > %T" \
-"$ltl2tgba --lbtt --small --medium %f > %T" \
+"$ltl2tgba --hoa  --small --medium %f > %H" \
 "$ltl2tgba --lbtt --small --high %f > %T" \
 "$ltl2tgba --lbtt -x comp-susp --small %f >%T" \
-"$ltl2tgba --lbtt -x comp-susp,!skel-wdba --lbtt --small %f >%T" \
-"$ltl2tgba --lbtt -x comp-susp,early-susp --lbtt --small %f >%T" \
-"$ltl2tgba --lbtt -x comp-susp,!skel-wdba,!skel-simul --lbtt --small %f >%T" \
-"$ltl2tgba --lbtt --ba -x degen-skip=0 --lbtt %f >%T" \
+"$ltl2tgba --lbtt -x comp-susp,!skel-wdba --small %f >%T" \
+"$ltl2tgba --lbtt -x comp-susp,early-susp --small %f >%T" \
+"$ltl2tgba --lbtt -x comp-susp,!skel-wdba,!skel-simul --small %f >%T" \
+"$ltl2tgba --spin --ba -x degen-skip=0 %f >%N" \
 "$ltl2tgba --lbtt --ba --high %f > %T" \
-"$ltl2tgba --lbtt -BDC %f > %T" \
+"$ltl2tgba --hoa  -BDC %f > %H" \
 "$ltl2tgba --lbtt -BC %f > %T" \
 --json=output.json --csv=output.csv