diff --git a/src/tgbatest/complementation.cc b/src/tgbatest/complementation.cc
index 6f3174d6c..b00a2e9dc 100644
--- a/src/tgbatest/complementation.cc
+++ b/src/tgbatest/complementation.cc
@@ -20,8 +20,8 @@
 #include <iomanip>
 #include <iostream>
 #include "tgbaalgos/dotty.hh"
-#include "tgbaalgos/save.hh"
-#include "tgbaparse/public.hh"
+#include "tgbaalgos/hoa.hh"
+#include "hoaparse/public.hh"
 #include "tgba/tgbaproduct.hh"
 #include "tgbaalgos/gtec/gtec.hh"
 #include "tgbaalgos/ltl2tgba_fm.hh"
@@ -39,7 +39,7 @@ void usage(const char* prog)
 {
   std::cout << "usage: " << prog << " [options]" << std::endl;
   std::cout << "with options" << std::endl
-            << "-b                      Output in spot's format\n"
+            << "-H                      Output in HOA\n"
             << "-s     buchi_automaton  display the safra automaton\n"
             << "-a     buchi_automaton  display the complemented automaton\n"
             << "-astat buchi_automaton  statistics for !a\n"
@@ -58,7 +58,7 @@ int main(int argc, char* argv[])
   bool stats = false;
   bool formula = false;
   bool print_formula = false;
-  bool save_spot = false;
+  bool save_hoa = false;
 
   if (argc < 3)
   {
@@ -70,9 +70,9 @@ int main(int argc, char* argv[])
   {
     if (argv[i][0] == '-')
     {
-      if (strcmp(argv[i] + 1, "b") == 0)
+      if (strcmp(argv[i] + 1, "H") == 0)
       {
-	save_spot = true;
+	save_hoa = true;
 	continue;
       }
 
@@ -121,10 +121,11 @@ int main(int argc, char* argv[])
   if (print_automaton || print_safra)
   {
     spot::ltl::environment& env(spot::ltl::default_environment::instance());
-    spot::tgba_parse_error_list pel;
-    spot::tgba_digraph_ptr a = spot::tgba_parse(file, pel, dict, env);
-    if (spot::format_tgba_parse_errors(std::cerr, file, pel))
+    spot::hoa_parse_error_list pel;
+    auto h = spot::hoa_parse(file, pel, dict, env);
+    if (spot::format_hoa_parse_errors(std::cerr, file, pel))
       return 2;
+    spot::tgba_digraph_ptr a = h->aut;
 
     spot::tgba_ptr complement = 0;
 
@@ -132,8 +133,8 @@ int main(int argc, char* argv[])
 
     if (print_automaton)
       {
-	if (save_spot)
-	  spot::tgba_save_reachable(std::cout, complement);
+	if (save_hoa)
+	  spot::hoa_reachable(std::cout, complement, nullptr);
 	else
 	  spot::dotty_reachable(std::cout, complement);
       }
@@ -177,11 +178,12 @@ int main(int argc, char* argv[])
     }
     else
     {
-      spot::tgba_parse_error_list pel;
+      spot::hoa_parse_error_list pel;
       spot::ltl::environment& env(spot::ltl::default_environment::instance());
-      a = spot::tgba_parse(file, pel, dict, env);
-      if (spot::format_tgba_parse_errors(std::cerr, file, pel))
+      auto h = spot::hoa_parse(file, pel, dict, env);
+      if (spot::format_hoa_parse_errors(std::cerr, file, pel))
         return 2;
+      a = h->aut;
     }
 
     auto safra_complement = spot::make_safra_complement(a);
diff --git a/src/tgbatest/complementation.test b/src/tgbatest/complementation.test
index 898785f90..57438716d 100755
--- a/src/tgbatest/complementation.test
+++ b/src/tgbatest/complementation.test
@@ -39,20 +39,31 @@ EOF
 
 # The following test-case was supplied by Martin Dieguez Lodeiro to
 # demonstrate a bug in our Safra implementation.
-cat >x.tgba <<EOF
-acc = "1";
-"1", "1", "1",;
-"1", "2", "p",;
-"2", "3", "p", "1";
-"2", "2", "1",;
-"3", "3", "p", "1";
-"3", "2", "1",;
+cat >x.hoa <<EOF
+HOA: v1
+States: 3
+Start: 0
+AP: 1 "p"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels trans-acc complete
+--BODY--
+State: 0
+[t] 0
+[0] 1
+State: 1
+[t] 1
+[0] 2 {0}
+State: 2
+[t] 1
+[0] 2 {0}
+--END--
 EOF
 # x.tgba accepts some run
-run 0 ../ltl2tgba -X -e x.tgba
+run 0 ../ltl2tgba -XH -e x.hoa
 # so does its complement
-run 0 ../complement -b -a x.tgba > nx.tgba
-run 0 ../ltl2tgba -X -e nx.tgba
+run 0 ../complement -H -a x.hoa > nx.hoa
+run 0 ../ltl2tgba -XH -e nx.hoa
 # however the intersection of both should not
 # accept any run.
-run 0 ../ltl2tgba -X -E -Pnx.tgba x.tgba
+run 1 ../../bin/autfilt -q nx.hoa --intersect x.hoa
diff --git a/src/tgbatest/cycles.test b/src/tgbatest/cycles.test
index 583073c42..99f8caa43 100755
--- a/src/tgbatest/cycles.test
+++ b/src/tgbatest/cycles.test
@@ -21,63 +21,52 @@
 . ./defs
 set -e
 
-# GNU systems have seq,
-# BSD systems have jot.
-# Neither of those are POSIX...
-if test "*`(seq 1 1 2>/dev/null)`" = "1"; then
-  have_seq=true
-else
-  have_seq=false
-  if test "`(jot 1 1 2>/dev/null)`" = "1"; then
-    have_jot=true
-  else
-    have_jot=false
-  fi
-fi
-
-# enum start end
-enum() {
-  if $have_seq; then
-    seq $1 $2
-  elif $have_jot; then
-    jot `expr $2 - $1 + 1` $1
-  else
-    i=$1
-    while test $i -le $2; do
-      echo $i
-      i=`expr $i + 1`
-    done
-  fi
-}
-
 # Fig.1 from Johnson's SIAM J. Comput. 1975 paper.
+cat >johnson-fig1.hoa <<EOF
+HOA: v1
+States: 12
+Start: 0
+AP: 0
+acc-name: all
+Acceptance: 0 t
+properties: trans-labels explicit-labels state-acc complete
+--BODY--
+State: 0
+[t] 1
+[t] 3
+[t] 4
+State: 1
+[t] 2
+State: 2
+[t] 5
+[t] 6
+State: 3
+[t] 2
+State: 4
+[t] 2
+State: 5
+[t] 6
+[t] 7
+State: 6
+[t] 8
+[t] 10
+[t] 11
+State: 7
+[t] 0
+[t] 6
+State: 8
+[t] 2
+[t] 9
+State: 9
+[t] 6
+State: 10
+[t] 9
+State: 11
+[t] 9
+--END--
+EOF
 
-(
-echo 'acc = ;'
-k=3
-v=`expr $k + 2`
-w=`expr 2 \* $k + 2`
-x=`expr 3 \* $k + 3`
-for i in $(enum 2 `expr $k + 1`); do
-  echo "s1,s$i,,;"
-  echo "s$i,s$v,,;"
-done
-for i in $(enum `expr $k + 2` `expr 2 \* $k`); do
-  echo "s$i,s`expr $i + 1`,,;"
-  echo "s$i,s$w,,;"
-done
-echo "s`expr 2 \* $k + 1`,s$w,,;"
-echo "s`expr 2 \* $k + 1`,s1,,;"
-for i in $(enum `expr 2 \* $k + 3` `expr 3 \* $k + 2`); do
-  echo "s$w,s$i,,;"
-  echo "s$i,s$x,,;"
-done
-echo "s`expr 2 \* $k + 3`,s$v,,;"
-echo "s$x,s$w,,;"
-) > johnson-fig1.tgba
-
-
-run 0 ../ltl2tgba -KC -X johnson-fig1.tgba > out
+run 0 ../ltl2tgba -KC -XH johnson-fig1.hoa > out
 test `wc -l < out` -eq 10
 
 run 0 ../ltl2tgba -KW '(Ga -> Gb) W c' > out
diff --git a/src/tgbatest/dbacomp.test b/src/tgbatest/dbacomp.test
index 7bce350bd..e4e0b0f72 100755
--- a/src/tgbatest/dbacomp.test
+++ b/src/tgbatest/dbacomp.test
@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2013 Laboratoire de Recherche et
+# Copyright (C) 2013, 2015 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -23,25 +23,37 @@ set -e
 
 # This automaton used to trigger a bug in the complementation: its
 # intersection with the complement was not empty!
-cat >input.tgba <<EOF
-acc = "a" "b" "c";
-"1", "1", "(a & d) | (a & b)", "b" "c";
-"1", "2", "a & !d & !c & !b",;
-"1", "1", "(d & !a) | (b & !a)", "a" "b" "c";
-"1", "2", "!a & !d & !c & !b", "a";
-"2", "1", "a & c & b", "b" "c";
-"2", "3", "a & b & !c", "b";
-"2", "2", "a & !c & !b",;
-"2", "1", "c & b & !a", "a" "b" "c";
-"2", "3", "b & !a & !c", "a" "b";
-"2", "2", "!a & !c & !b", "a";
-"3", "1", "(a & d & c) | (a & c & b)", "b" "c";
-"3", "3", "(a & d & !c) | (a & b & !c)", "b";
-"3", "2", "a & !d & !c & !b",;
-"3", "1", "(d & c & !a) | (c & b & !a)", "a" "b" "c";
-"3", "3", "(d & !a & !c) | (b & !a & !c)", "a" "b";
-"3", "2", "!a & !d & !c & !b", "a";
+cat >input.hoa <<EOF
+HOA: v1
+States: 3
+Start: 0
+AP: 4 "a" "d" "b" "c"
+acc-name: generalized-Buchi 3
+Acceptance: 3 Inf(0)&Inf(1)&Inf(2)
+properties: trans-labels explicit-labels trans-acc deterministic
+--BODY--
+State: 0
+[0&1 | 0&2] 0 {1 2}
+[!0&1 | !0&2] 0 {0 1 2}
+[0&!1&!2&!3] 1
+[!0&!1&!2&!3] 1 {0}
+State: 1
+[0&2&3] 0 {1 2}
+[!0&2&3] 0 {0 1 2}
+[0&!2&!3] 1
+[!0&!2&!3] 1 {0}
+[0&2&!3] 2 {1}
+[!0&2&!3] 2 {0 1}
+State: 2
+[0&1&3 | 0&2&3] 0 {1 2}
+[!0&1&3 | !0&2&3] 0 {0 1 2}
+[0&!1&!2&!3] 1
+[!0&!1&!2&!3] 1 {0}
+[0&1&!3 | 0&2&!3] 2 {1}
+[!0&1&!3 | !0&2&!3] 2 {0 1}
+--END--
 EOF
 
 # Check emptiness of product with complement.
-run 0 ../ltl2tgba -Pinput.tgba -DC -E -C -X input.tgba
+run 0 ../ltl2tgba -H -DC -C -XH input.hoa > output.hoa
+run 1 ../../bin/autfilt -q input.hoa --intersect output.hoa
diff --git a/src/tgbatest/degenid.test b/src/tgbatest/degenid.test
index 8f549ac4c..1d7e2b505 100755
--- a/src/tgbatest/degenid.test
+++ b/src/tgbatest/degenid.test
@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2011, 2013, 2014 Laboratoire de Recherche et
+# Copyright (C) 2011, 2013, 2014, 2015 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -26,12 +26,12 @@ set -e
 
 for f in 'FGa|GFb' 'GFa & GFb & GFc' 'GF(a->FGb)&GF(c->FGd)'; do
   for opt in -DS -DT; do
-    ../ltl2tgba $opt -b "$f" > autX.spot
-    ../ltl2tgba -X -kt autX.spot > base.size
+    ../ltl2tgba $opt -H "$f" > autX.spot
+    ../ltl2tgba -XH -kt autX.spot > base.size
     cat base.size
     for x in X XX XXX; do
-      ../ltl2tgba -X $opt -b aut$x.spot > autX$x.spot
-      ../ltl2tgba -X -kt autX$x.spot > new.size
+      ../ltl2tgba -XH $opt -H aut$x.spot > autX$x.spot
+      ../ltl2tgba -XH -kt autX$x.spot > new.size
       cat new.size
       cmp base.size new.size
     done
@@ -42,61 +42,91 @@ done
 # This is another 6-state degeneralized automaton that
 # we used the "redegeneralize" to a 8-state BA...
 cat > bug <<EOF
-acc = "1";
-"1", "2", "!b | !a", "1";
-"1", "5", "a & b", "1";
-"2", "2", "b & !a", "1";
-"2", "3", "!b & !a", "1";
-"2", "4", "a", "1";
-"5", "1", "a & !b",;
-"5", "2", "!b & !a",;
-"5", "5", "a & b",;
-"5", "6", "b & !a",;
-"3", "1", "a & b",;
-"3", "2", "b & !a",;
-"3", "3", "!b & !a",;
-"3", "4", "a & !b",;
-"4", "1", "b",;
-"4", "5", "a & !b",;
-"4", "6", "!b & !a",;
-"6", "1", "!b",;
-"6", "3", "b & !a",;
-"6", "4", "a & b",;
+HOA: v1
+States: 6
+Start: 0
+AP: 2 "a" "b"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc complete deterministic
+--BODY--
+State: 0 {0}
+[!0 | !1] 1
+[0&1] 2
+State: 1 {0}
+[!0&1] 1
+[!0&!1] 3
+[0] 4
+State: 2
+[0&!1] 0
+[!0&!1] 1
+[0&1] 2
+[!0&1] 5
+State: 3
+[0&1] 0
+[!0&1] 1
+[!0&!1] 3
+[0&!1] 4
+State: 4
+[1] 0
+[0&!1] 2
+[!0&!1] 5
+State: 5
+[!1] 0
+[!0&1] 3
+[0&1] 4
+--END--
 EOF
 
-run 0 ../ltl2tgba -ks -X -DS bug > out
+run 0 ../ltl2tgba -ks -XH -DS bug > out
 grep 'states: 6' out
 
 
 # This 8-state degeneralized automaton used
 # to be "degeneralized" to a 9-state BA...
 cat > bug2 <<EOF
-acc = "1";
-"1", "2", "1",;
-"2", "3", "1", "1";
-"3", "3", "a & !b",;
-"3", "4", "a & b",;
-"3", "5", "!a & !b",;
-"3", "6", "b & !a",;
-"4", "3", "a", "1";
-"4", "5", "!a", "1";
-"5", "3", "a & !b",;
-"5", "4", "a & b",;
-"5", "6", "b & !a",;
-"5", "7", "!a & !b",;
-"6", "3", "a & !b", "1";
-"6", "4", "a & b", "1";
-"6", "6", "b & !a", "1";
-"6", "7", "!a & !b", "1";
-"7", "3", "a & !b",;
-"7", "4", "a & b",;
-"7", "8", "b & !a",;
-"7", "7", "!a & !b",;
-"8", "4", "a",;
-"8", "8", "!a",;
+HOA: v1
+States: 8
+Start: 0
+AP: 2 "a" "b"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc complete deterministic
+--BODY--
+State: 0
+[t] 1
+State: 1 {0}
+[t] 2
+State: 2
+[0&!1] 2
+[0&1] 3
+[!0&!1] 4
+[!0&1] 5
+State: 3 {0}
+[0] 2
+[!0] 4
+State: 4
+[0&!1] 2
+[0&1] 3
+[!0&1] 5
+[!0&!1] 6
+State: 5 {0}
+[0&!1] 2
+[0&1] 3
+[!0&1] 5
+[!0&!1] 6
+State: 6
+[0&!1] 2
+[0&1] 3
+[!0&!1] 6
+[!0&1] 7
+State: 7
+[0] 3
+[!0] 7
+--END--
 EOF
 
-run 0 ../ltl2tgba -ks -X -DS bug2 >out
+run 0 ../ltl2tgba -ks -XH -DS bug2 >out
 grep 'states: 8' out
 
 
diff --git a/src/tgbatest/dfs.test b/src/tgbatest/dfs.test
index c36141791..bd9c520a3 100755
--- a/src/tgbatest/dfs.test
+++ b/src/tgbatest/dfs.test
@@ -35,51 +35,68 @@ set -e
 # |_______|
 
 cat >blue_counter <<'EOF'
-acc = a;
-s1, s2,, a;
-s2, s3,,;
-s3, s1,,;
-s3, s4,,;
-s4, s4,,;
-s4, s5,,;
-s4, s6,,;
-s4, s7,,;
-s4, s8,,;
-s4, s9,,;
-s5, s4,,;
-s5, s5,,;
-s5, s6,,;
-s5, s7,,;
-s5, s8,,;
-s5, s9,,;
-s6, s4,,;
-s6, s5,,;
-s6, s6,,;
-s6, s7,,;
-s6, s8,,;
-s6, s9,,;
-s7, s4,,;
-s7, s5,,;
-s7, s6,,;
-s7, s7,,;
-s7, s8,,;
-s7, s9,,;
-s8, s4,,;
-s8, s5,,;
-s8, s6,,;
-s8, s7,,;
-s8, s8,,;
-s8, s9,,;
-s9, s4,,;
-s9, s5,,;
-s9, s6,,;
-s9, s7,,;
-s9, s8,,;
-s9, s9,,;
+HOA: v1
+States: 9
+Start: 0
+AP: 0
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc complete
+--BODY--
+State: 0 {0}
+[t] 1
+State: 1
+[t] 2
+State: 2
+[t] 0
+[t] 3
+State: 3
+[t] 3
+[t] 4
+[t] 5
+[t] 6
+[t] 7
+[t] 8
+State: 4
+[t] 3
+[t] 4
+[t] 5
+[t] 6
+[t] 7
+[t] 8
+State: 5
+[t] 3
+[t] 4
+[t] 5
+[t] 6
+[t] 7
+[t] 8
+State: 6
+[t] 3
+[t] 4
+[t] 5
+[t] 6
+[t] 7
+[t] 8
+State: 7
+[t] 3
+[t] 4
+[t] 5
+[t] 6
+[t] 7
+[t] 8
+State: 8
+[t] 3
+[t] 4
+[t] 5
+[t] 6
+[t] 7
+[t] 8
+--END--
 EOF
 
-run 0 ../ltl2tgba -CR -eSE05 -X blue_counter
-run 0 ../ltl2tgba -CR -eTau03_opt -X blue_counter
+run 0 ../ltl2tgba -CR -eSE05 -XH blue_counter
+run 0 ../ltl2tgba -CR -eTau03_opt -XH blue_counter
 
 # s1->s2->s3->(large composant from s4 to s9)
 # ^       ||
@@ -87,51 +104,68 @@ run 0 ../ltl2tgba -CR -eTau03_opt -X blue_counter
 # ||______||
 
 cat >blue_last <<'EOF'
-acc = a;
-s1, s2,,;
-s2, s3,,;
-s3, s1,, a;
-s3, s4,,;
-s4, s4,,;
-s4, s5,,;
-s4, s6,,;
-s4, s7,,;
-s4, s8,,;
-s4, s9,,;
-s5, s4,,;
-s5, s5,,;
-s5, s6,,;
-s5, s7,,;
-s5, s8,,;
-s5, s9,,;
-s6, s4,,;
-s6, s5,,;
-s6, s6,,;
-s6, s7,,;
-s6, s8,,;
-s6, s9,,;
-s7, s4,,;
-s7, s5,,;
-s7, s6,,;
-s7, s7,,;
-s7, s8,,;
-s7, s9,,;
-s8, s4,,;
-s8, s5,,;
-s8, s6,,;
-s8, s7,,;
-s8, s8,,;
-s8, s9,,;
-s9, s4,,;
-s9, s5,,;
-s9, s6,,;
-s9, s7,,;
-s9, s8,,;
-s9, s9,,;
+HOA: v1
+States: 9
+Start: 0
+AP: 0
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels trans-acc complete
+--BODY--
+State: 0
+[t] 1
+State: 1
+[t] 2
+State: 2
+[t] 0 {0}
+[t] 3
+State: 3
+[t] 3
+[t] 4
+[t] 5
+[t] 6
+[t] 7
+[t] 8
+State: 4
+[t] 3
+[t] 4
+[t] 5
+[t] 6
+[t] 7
+[t] 8
+State: 5
+[t] 3
+[t] 4
+[t] 5
+[t] 6
+[t] 7
+[t] 8
+State: 6
+[t] 3
+[t] 4
+[t] 5
+[t] 6
+[t] 7
+[t] 8
+State: 7
+[t] 3
+[t] 4
+[t] 5
+[t] 6
+[t] 7
+[t] 8
+State: 8
+[t] 3
+[t] 4
+[t] 5
+[t] 6
+[t] 7
+[t] 8
+--END--
 EOF
 
-run 0 ../ltl2tgba -CR -eSE05 -X blue_last
-run 0 ../ltl2tgba -CR -eTau03_opt -X blue_last
+run 0 ../ltl2tgba -CR -eSE05 -XH blue_last
+run 0 ../ltl2tgba -CR -eTau03_opt -XH blue_last
 
 #  _______
 # |       |
@@ -142,51 +176,68 @@ run 0 ../ltl2tgba -CR -eTau03_opt -X blue_last
 # ||______||
 
 cat >red <<'EOF'
-acc = a;
-s1, s2,,;
-s1, s3,, a;
-s2, s3,,;
-s3, s1,,;
-s3, s4,,;
-s4, s4,,;
-s4, s5,,;
-s4, s6,,;
-s4, s7,,;
-s4, s8,,;
-s4, s9,,;
-s5, s4,,;
-s5, s5,,;
-s5, s6,,;
-s5, s7,,;
-s5, s8,,;
-s5, s9,,;
-s6, s4,,;
-s6, s5,,;
-s6, s6,,;
-s6, s7,,;
-s6, s8,,;
-s6, s9,,;
-s7, s4,,;
-s7, s5,,;
-s7, s6,,;
-s7, s7,,;
-s7, s8,,;
-s7, s9,,;
-s8, s4,,;
-s8, s5,,;
-s8, s6,,;
-s8, s7,,;
-s8, s8,,;
-s8, s9,,;
-s9, s4,,;
-s9, s5,,;
-s9, s6,,;
-s9, s7,,;
-s9, s8,,;
-s9, s9,,;
+HOA: v1
+States: 9
+Start: 0
+AP: 0
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels trans-acc complete
+--BODY--
+State: 0
+[t] 1
+[t] 2 {0}
+State: 1
+[t] 2
+State: 2
+[t] 0
+[t] 3
+State: 3
+[t] 3
+[t] 4
+[t] 5
+[t] 6
+[t] 7
+[t] 8
+State: 4
+[t] 3
+[t] 4
+[t] 5
+[t] 6
+[t] 7
+[t] 8
+State: 5
+[t] 3
+[t] 4
+[t] 5
+[t] 6
+[t] 7
+[t] 8
+State: 6
+[t] 3
+[t] 4
+[t] 5
+[t] 6
+[t] 7
+[t] 8
+State: 7
+[t] 3
+[t] 4
+[t] 5
+[t] 6
+[t] 7
+[t] 8
+State: 8
+[t] 3
+[t] 4
+[t] 5
+[t] 6
+[t] 7
+[t] 8
+--END--
 EOF
 
-run 0 ../ltl2tgba -CR -eSE05 -X red
-run 0 ../ltl2tgba -CR -eTau03_opt -X red
+run 0 ../ltl2tgba -CR -eSE05 -XH red
+run 0 ../ltl2tgba -CR -eTau03_opt -XH red
 
 rm -f red blue_counter blue_last
diff --git a/src/tgbatest/emptchke.test b/src/tgbatest/emptchke.test
index 277afe7e9..347e15792 100755
--- a/src/tgbatest/emptchke.test
+++ b/src/tgbatest/emptchke.test
@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2009, 2010, 2014 Laboratoire de Recherche et
+# Copyright (C) 2009, 2010, 2014, 2015 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 # Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de
 # Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@@ -28,21 +28,32 @@ set -e
 
 expect_ce()
 {
-  run 0 ../ltl2tgba -CR -e -X "$1"
-  run 0 ../ltl2tgba -CR -e -DT -X "$1"
-  run 0 ../ltl2tgba -CR -e'Cou99(shy)' -X "$1"
-  run 0 ../ltl2tgba -CR -e'Cou99(shy)' -DT -X "$1"
-  run 0 ../ltl2tgba -CR -eCVWY90 -X "$1"
-  run 0 ../ltl2tgba -CR -eGV04 -X "$1"
-  run 0 ../ltl2tgba -CR -eSE05 -X "$1"
-  run 0 ../ltl2tgba -CR -eTau03 -X "$1"
+  run 0 ../ltl2tgba -CR -e -XH "$1"
+  run 0 ../ltl2tgba -CR -e -DT -XH "$1"
+  run 0 ../ltl2tgba -CR -e'Cou99(shy)' -XH "$1"
+  run 0 ../ltl2tgba -CR -e'Cou99(shy)' -DT -XH "$1"
+  run 0 ../ltl2tgba -CR -eCVWY90 -XH "$1"
+  run 0 ../ltl2tgba -CR -eGV04 -XH "$1"
+  run 0 ../ltl2tgba -CR -eSE05 -XH "$1"
+  run 0 ../ltl2tgba -CR -eTau03 -XH "$1"
 }
 
 cat >input <<'EOF'
-acc = c d;
-s1, "s2", "a & !b", c d;
-"s2", "state 3", "a", c;
-"state 3", s1,,;
+HOA: v1
+States: 3
+Start: 0
+AP: 2 "a" "b"
+acc-name: generalized-Buchi 2
+Acceptance: 2 Inf(0)&Inf(1)
+properties: trans-labels explicit-labels state-acc deterministic
+--BODY--
+State: 0 {0 1}
+[0&!1] 1
+State: 1 {0}
+[0] 2
+State: 2
+[t] 0
+--END--
 EOF
 
 expect_ce input
@@ -55,19 +66,36 @@ expect_ce input
 #  b->c e->f h->i
 #
 cat >input <<'EOF'
-acc = A;
-a, b, "1",;
-b, c, "1",;
-c, a, "1",;
-a, d, "1",;
-d, e, "1",;
-e, f, "1",;
-f, d, "1",;
-d, g, "1",;
-g, h, "1",;
-h, i, "1",;
-i, g, "1", A;
-a, g, "1",;
+HOA: v1
+States: 9
+Start: 0
+AP: 0
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc complete
+--BODY--
+State: 0
+[t] 1
+[t] 3
+[t] 6
+State: 1
+[t] 2
+State: 2
+[t] 0
+State: 3
+[t] 4
+[t] 6
+State: 4
+[t] 5
+State: 5
+[t] 3
+State: 6
+[t] 7
+State: 7
+[t] 8
+State: 8 {0}
+[t] 6
+--END--
 EOF
 
 expect_ce input
@@ -100,15 +128,29 @@ expect_ce input
 # and finally closes the cycle with c->d->a
 #
 cat >input <<'EOF'
-acc = A B;
-a, b, "1",;
-b, c, "1",;
-c, d, "1",;
-d, a, "1",;
-b, e, "1", A;
-e, f, "1",;
-f, b, "1", B;
-e, c, "1", B;
+HOA: v1
+States: 6
+Start: 0
+AP: 0
+acc-name: generalized-Buchi 2
+Acceptance: 2 Inf(0)&Inf(1)
+properties: trans-labels explicit-labels trans-acc complete
+--BODY--
+State: 0
+[t] 1
+State: 1
+[t] 2
+[t] 4 {0}
+State: 2
+[t] 3
+State: 3
+[t] 0
+State: 4
+[t] 2 {1}
+[t] 5
+State: 5
+[t] 1 {1}
+--END--
 EOF
 
 expect_ce input
@@ -118,33 +160,61 @@ expect_ce input
 # It triggered a bug in our implementation of GV04 (that didn't see any
 # accepting path).
 cat >input <<EOF
-acc = "a0";
-"S0", "S12", "1",;
-"S12", "S17", "1",;
-"S12", "S8", "1",;
-"S17", "S6", "1",;
-"S17", "S9", "1", "a0";
-"S17", "S2", "1",;
-"S8", "S14", "1",;
-"S8", "S2", "1",;
-"S6", "S1", "1",;
-"S9", "S18", "1",;
-"S2", "S17", "1",;
-"S14", "S19", "1",;
-"S14", "S10", "1",;
-"S1", "S15", "1",;
-"S18", "S5", "1",;
-"S19", "S5", "1",;
-"S19", "S7", "1",;
-"S19", "S11", "1",;
-"S10", "S17", "1",;
-"S15", "S8", "1",;
-"S5", "S4", "1",;
-"S11", "S6", "1",;
-"S4", "S13", "1",;
-"S13", "S3", "1",;
-"S3", "S16", "1",;
-"S3", "S19", "1",;
+HOA: v1
+States: 20
+Start: 0
+AP: 0
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels trans-acc
+--BODY--
+State: 0
+[t] 1
+State: 1
+[t] 2
+[t] 3
+State: 2
+[t] 4
+[t] 5 {0}
+[t] 6
+State: 3
+[t] 6
+[t] 7
+State: 4
+[t] 8
+State: 5
+[t] 9
+State: 6
+[t] 2
+State: 7
+[t] 10
+[t] 11
+State: 8
+[t] 12
+State: 9
+[t] 13
+State: 10
+[t] 13
+[t] 14
+[t] 15
+State: 11
+[t] 2
+State: 12
+[t] 3
+State: 13
+[t] 16
+State: 14
+State: 15
+[t] 4
+State: 16
+[t] 17
+State: 17
+[t] 18
+State: 18
+[t] 10
+[t] 19
+State: 19
+--END--
 EOF
 
 expect_ce input
diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc
index cc93bf250..92f792ae3 100644
--- a/src/tgbatest/ltl2tgba.cc
+++ b/src/tgbatest/ltl2tgba.cc
@@ -33,14 +33,12 @@
 #include "tgbaalgos/ltl2tgba_fm.hh"
 #include "tgbaalgos/ltl2taa.hh"
 #include "tgba/bddprint.hh"
-#include "tgbaalgos/save.hh"
 #include "tgbaalgos/dotty.hh"
 #include "tgbaalgos/lbtt.hh"
 #include "tgbaalgos/hoa.hh"
 #include "tgbaalgos/degen.hh"
 #include "tgba/tgbaproduct.hh"
 #include "tgbaalgos/reducerun.hh"
-#include "tgbaparse/public.hh"
 #include "dstarparse/public.hh"
 #include "hoaparse/public.hh"
 #include "tgbaalgos/dupexp.hh"
@@ -104,7 +102,7 @@ syntax(char* prog)
 	    << std::endl
             << "       "<< prog << " [-f|-l|-taa] -F [OPTIONS...] file"
 	    << std::endl
-            << "       "<< prog << " -X [OPTIONS...] file" << std::endl
+            << "       "<< prog << " -XH [OPTIONS...] file" << std::endl
 	    << std::endl
 
             << "Translate an LTL formula into an automaton, or read the "
@@ -118,8 +116,6 @@ syntax(char* prog)
             << "Input options:" << std::endl
             << "  -F    read the formula from a file, not from the command line"
 	    << std::endl
-	    << "  -X    do not compute an automaton, read it from a file"
-	    << std::endl
 	    << "  -XD   do not compute an automaton, read it from an"
 	    << " ltl2dstar file" << std::endl
 	    << "  -XDB  read the from an ltl2dstar file and convert it to "
@@ -266,8 +262,6 @@ syntax(char* prog)
 	    << std::endl
 
 	    << "Output options (if no emptiness check):" << std::endl
-	    << "  -b    output the automaton in the format of spot"
-            << std::endl
 	    << "  -ks   display statistics on the automaton (size only)"
 	    << std::endl
 	    << "  -kt   display statistics on the automaton (size + "
@@ -349,7 +343,7 @@ checked_main(int argc, char** argv)
   bool accepting_run = false;
   bool accepting_run_replay = false;
   bool from_file = false;
-  enum { ReadSpot, ReadLbtt, ReadDstar, ReadHoa } readformat = ReadSpot;
+  enum { ReadLbtt, ReadDstar, ReadHoa } readformat = ReadHoa;
   bool nra2nba = false;
   bool dra2dba = false;
   bool scc_filter = false;
@@ -415,11 +409,6 @@ checked_main(int argc, char** argv)
 	  utf8_opt = true;
 	  spot::enable_utf8();
 	}
-
-      else if (!strcmp(argv[formula_index], "-b"))
-	{
-	  output = 7;
-	}
       else if (!strcmp(argv[formula_index], "-c"))
 	{
 	  containment = true;
@@ -610,16 +599,15 @@ checked_main(int argc, char** argv)
 	{
 	  tm.start("reading -P's argument");
 
-	  spot::tgba_parse_error_list pel;
-	  spot::tgba_digraph_ptr s;
-	  s = spot::tgba_parse(argv[formula_index] + 2,
-			       pel, dict, env, debug_opt);
-	  if (spot::format_tgba_parse_errors(std::cerr,
-					     argv[formula_index] + 2, pel))
+	  spot::dstar_parse_error_list pel;
+	  auto daut = spot::hoa_parse(argv[formula_index] + 2, pel,
+				      dict, env, debug_opt);
+	  if (spot::format_hoa_parse_errors(std::cerr,
+					    argv[formula_index] + 2, pel))
 	    return 2;
-	  s->merge_transitions();
+	  daut->aut->merge_transitions();
+	  system_aut = daut->aut;
 	  tm.stop("reading -P's argument");
-	  system_aut = s;
 	}
       else if (!strcmp(argv[formula_index], "-r1"))
 	{
@@ -869,11 +857,6 @@ checked_main(int argc, char** argv)
 	  translation = TransFM;
 	  fm_exprop_opt = true;
 	}
-      else if (!strcmp(argv[formula_index], "-X"))
-	{
-	  from_file = true;
-	  readformat = ReadSpot;
-	}
       else if (!strcmp(argv[formula_index], "-XD"))
 	{
 	  from_file = true;
@@ -984,18 +967,6 @@ checked_main(int argc, char** argv)
 	{
 	  switch (readformat)
 	    {
-	    case ReadSpot:
-		{
-		  spot::tgba_digraph_ptr e;
-		  spot::tgba_parse_error_list pel;
-		  tm.start("parsing automaton");
-		  a = e = spot::tgba_parse(input, pel, dict, env, debug_opt);
-		  tm.stop("parsing automaton");
-		  if (spot::format_tgba_parse_errors(std::cerr, input, pel))
-		    return 2;
-		  e->merge_transitions();
-		}
-	      break;
 	    case ReadLbtt:
 	      {
 		std::string error;
@@ -1530,9 +1501,6 @@ checked_main(int argc, char** argv)
 	    case 6:
 	      spot::lbtt_reachable(std::cout, a);
 	      break;
-	    case 7:
-	      spot::tgba_save_reachable(std::cout, a);
-	      break;
 	    case 8:
 	      {
 		assert(degeneralize_opt == DegenSBA);
diff --git a/src/tgbatest/ltl2tgba.test b/src/tgbatest/ltl2tgba.test
index fdcbf7435..6e43f7a99 100755
--- a/src/tgbatest/ltl2tgba.test
+++ b/src/tgbatest/ltl2tgba.test
@@ -175,14 +175,14 @@ grep 'transitions: 5$' stdout
 grep 'states: 3$' stdout
 
 # Make sure FGa|GFb has the same number of states/transitions when
-# output as a never claim or are a degeneralized BA in Spot's textual
-# format.  The option -R1q -R1t used to cause two degeneralizations to
+# output as a never claim or are a degeneralized BA in HOAF.
+# The option -R1q -R1t used to cause two degeneralizations to
 # occur.
 run 0 ../ltl2tgba -R1q -R1t -N 'FGa|FGb' > out.never
 run 0 ../ltl2tgba -XN -kt out.never > count.never
-run 0 ../ltl2tgba -R1q -R1t -DS -b 'FGa|FGb' > out.spot
-run 0 ../ltl2tgba -X -kt out.spot > count.spot
-cmp count.never count.spot
+run 0 ../ltl2tgba -R1q -R1t -DS -H 'FGa|FGb' > out.hoa
+run 0 ../ltl2tgba -XH -kt out.hoa > count.hoa
+cmp count.never count.hoa
 
 # The following automaton should have only 4 states.
 run 0 ../ltl2tgba -R3 -ks -f '(p&XF!p)|(!p&XFp)|X(Fp&F!p)' >stdout
diff --git a/src/tgbatest/renault.test b/src/tgbatest/renault.test
index edb3d9120..03df482c5 100755
--- a/src/tgbatest/renault.test
+++ b/src/tgbatest/renault.test
@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2012 Laboratoire de Recherche et Développement
+# Copyright (C) 2012, 2015 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -22,28 +22,46 @@
 set -e
 
 cat >file <<EOF
-acc = "IOP.clear_interrupts";
-"1", "2", "a & b",;
-"1", "3", "(!a & !b & !c) | (c & a)",;
-"1", "1", "(!a & !b & !c) | (c & a)", "IOP.clear_interrupts";
-"1", "4", "!a & !c",;
-"1", "5", "!a & !c", "IOP.clear_interrupts";
-"1", "6", "a & b",;
-"2", "2", "a & b",;
-"2", "3", "c & a",;
-"2", "1", "c & a", "IOP.clear_interrupts";
-"2", "6", "a & b",;
-"3", "8", "1",;
-"4", "10", "!c",;
-"4", "8", "!b & !c",;
-"5", "3", "!a & !b & !c",;
-"5", "1", "!a & !b & !c", "IOP.clear_interrupts";
-"5", "4", "!a & !c",;
-"5", "5", "!a & !c", "IOP.clear_interrupts";
-"6", "7", "b",;
-"6", "8", "c",;
-"7", "9", "b & !c & !d",;
-"9", "9", "b & !c",;
+HOA: v1
+States: 10
+Start: 0
+AP: 4 "a" "b" "c" "d"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels trans-acc
+--BODY--
+State: 0
+[!0&!1&!2 | 0&2] 0 {0}
+[0&1] 1
+[!0&!1&!2 | 0&2] 2
+[!0&!2] 3
+[!0&!2] 4 {0}
+[0&1] 5
+State: 1
+[0&2] 0 {0}
+[0&1] 1
+[0&2] 2
+[0&1] 5
+State: 2
+[t] 6
+State: 3
+[!1&!2] 6
+[!2] 7
+State: 4
+[!0&!1&!2] 0 {0}
+[!0&!1&!2] 2
+[!0&!2] 3
+[!0&!2] 4 {0}
+State: 5
+[2] 6
+[1] 8
+State: 6
+State: 7
+State: 8
+[1&!2&!3] 9
+State: 9
+[1&!2] 9
+--END--
 EOF
 
 cat >outexp <<EOF
@@ -51,6 +69,6 @@ transitions: 12
 states: 6
 EOF
 
-run 0 ../ltl2tgba -X -ks -RDS file > out
+run 0 ../ltl2tgba -XH -ks -RDS file > out
 
 cmp out outexp
diff --git a/src/tgbatest/satmin2.test b/src/tgbatest/satmin2.test
index 4bbe3db58..5e37d3475 100755
--- a/src/tgbatest/satmin2.test
+++ b/src/tgbatest/satmin2.test
@@ -1,7 +1,6 @@
-
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2013 Laboratoire de Recherche et Développement
+# Copyright (C) 2013, 2015 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -28,14 +27,25 @@ set -e
 
 # This is a counterexample for one of the optimization idea we had for
 # the SAT-based minimization.
-cat >input.tgba  <<EOF
-acc = "x";
-"1", "2", "a", "x";
-"1", "3", "!a",;
-"2", "1", "!a", "x";
-"2", "3", "a",;
-"3", "3", "a", "x";
-"3", "3", "!a",;
+cat >input.hoa  <<EOF
+HOA: v1
+States: 3
+Start: 0
+AP: 1 "a"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels trans-acc complete deterministic
+--BODY--
+State: 0
+[0] 1 {0}
+[!0] 2
+State: 1
+[!0] 0 {0}
+[0] 2
+State: 2
+[0] 2 {0}
+[!0] 2
+--END--
 EOF
 
 cat >expected <<EOF
@@ -45,6 +55,5 @@ states: 1
 nondeterministic states: 0
 EOF
 
-../ltl2tgba -RS1 -kt -X input.tgba > output
+../ltl2tgba -RS1 -kt -XH input.hoa > output
 diff output expected
-
diff --git a/src/tgbatest/sccsimpl.test b/src/tgbatest/sccsimpl.test
index 4313dc1ef..f9421f79f 100755
--- a/src/tgbatest/sccsimpl.test
+++ b/src/tgbatest/sccsimpl.test
@@ -32,138 +32,207 @@ set -e
 # G((!p0 | !p2 | (!p1 W (!p1 & p3 & X(!p1 U p4)))) U p1)
 # The formula does not really matter (except to show how
 # such automata can occur).  The important point is that the
-# acceptance condition "p4", used a lot, is always present
-# when "p1" is used.  So the "p4" acceptance can be removed.
+# acceptance set "0" contains the acceptance set "1", so
+# "0" can be removed.
 cat <<EOF > aut.txt
-acc = "p4" "p1";
-S1, S1, "p1", "p4" "p1";
-S1, S1, "!p0 | !p2", "p4";
-S1, S2, "p3", "p4";
-S1, S3, "1", "p4";
-S2, S1, "p1 & p4", "p4" "p1";
-S2, S1, "(p4 & !p0) | (p4 & !p2)", "p4";
-S2, S2, "p3 & p4", "p4";
-S2, S2, "(!p1 & !p0) | (!p1 & !p2) | (!p1 & p3)",;
-S2, S3, "p4", "p4";
-S2, S4, "!p1",;
-S3, S2, "!p1 & p3", "p4";
-S3, S3, "!p1", "p4";
-S4, S2, "!p1 & p3 & p4", "p4";
-S4, S2, "!p1 & p3",;
-S4, S3, "!p1 & p4", "p4";
-S4, S4, "!p1",;
+HOA: v1
+States: 4
+Start: 0
+AP: 5 "p1" "p0" "p2" "p3" "p4"
+acc-name: generalized-Buchi 2
+Acceptance: 2 Inf(0)&Inf(1)
+properties: trans-labels explicit-labels trans-acc
+--BODY--
+State: 0
+[0] 0 {0 1}
+[!1 | !2] 0 {0}
+[3] 1 {0}
+[t] 2 {0}
+State: 1
+[0&4] 0 {0 1}
+[!1&4 | !2&4] 0 {0}
+[3&4] 1 {0}
+[!0&!1 | !0&!2 | !0&3] 1
+[4] 2 {0}
+[!0] 3
+State: 2
+[!0&3] 1 {0}
+[!0] 2 {0}
+State: 3
+[!0&3] 1
+[!0&3&4] 1 {0}
+[!0&4] 2 {0}
+[!0] 3
+--END--
 EOF
 
-run 0 ../ltl2tgba -X -R3 -b aut.txt > out.txt
-grep '^acc = "[^"]*";$' out.txt
+run 0 ../ltl2tgba -XH -R3 -H aut.txt > out.txt
+grep '^Acceptance: 1 Inf(0)' out.txt
 
 
-# Here, acceptances A and C can both be removed.
+# Here, acceptance sets 0 and 2 can both be removed.
 cat <<EOF > aut2.txt
-acc = A B C D;
-S1, S1, "a", A;
-S1, S1, "b", A B;
-S1, S1, "c", A B C;
-S1, S1, "d", C D;
+HOA: v1
+States: 1
+Start: 0
+AP: 4 "a" "b" "c" "d"
+acc-name: generalized-Buchi 4
+Acceptance: 4 Inf(0)&Inf(1)&Inf(2)&Inf(3)
+properties: trans-labels explicit-labels trans-acc
+--BODY--
+State: 0
+[0] 0 {0}
+[1] 0 {0 1}
+[2] 0 {0 1 2}
+[3] 0 {2 3}
+--END--
 EOF
-run 0 ../ltl2tgba -X -R3 -b aut2.txt > out2.txt
-grep '^acc = "." ".";$' out2.txt || exit 1
-# only 4 lines output, because the "b" and "c" lines have been merged.
-test `wc -l < out2.txt` = 4
+run 0 ../ltl2tgba -XH -R3 -H aut2.txt > out2.txt
+grep '^Acceptance: 2 ' out2.txt
+# only 3 transitions output, because [1] and [2] have been merged
+test `grep -c '\[.*\]' out2.txt` = 3
 
 
-# Here, acceptances A and B can both be removed.
+# Here, acceptance sets 0 and 1 can both be removed.
 cat <<EOF > aut3.txt
-acc = A B C D;
-S1, S1, "a", A;
-S1, S1, "b", A B;
-S1, S1, "c", A B C;
-S1, S1, "d", B D;
+HOA: v1
+States: 1
+Start: 0
+AP: 4 "a" "b" "c" "d"
+acc-name: generalized-Buchi 4
+Acceptance: 4 Inf(0)&Inf(1)&Inf(2)&Inf(3)
+properties: trans-labels explicit-labels trans-acc
+--BODY--
+State: 0
+[0] 0 {0}
+[1] 0 {0 1}
+[2] 0 {0 1 2}
+[3] 0 {1 3}
+--END--
 EOF
-run 0 ../ltl2tgba -X -R3 -b aut3.txt > out3.txt
-grep '^acc = "." ".";$' out3.txt || exit 1
-# only 4 lines output, because the "a" and "b" lines have been merged.
-test `wc -l < out3.txt` = 4
+run 0 ../ltl2tgba -XH -R3 -H aut3.txt > out3.txt
+grep '^Acceptance: 2 ' out3.txt
+# only 3 transitions output, because [0] and [1] have been merged
+test `grep -c '\[.*\]' out3.txt` = 3
 
 
 # No simplification possible here
 cat <<EOF > aut4.txt
-acc = A B C D;
-S1, S1, "a", A;
-S1, S1, "b", A B;
-S1, S1, "c", A B C;
-S1, S1, "d", B D;
-S1, S1, "e", C D;
+HOA: v1
+States: 1
+Start: 0
+AP: 5 "a" "b" "c" "d" "e"
+acc-name: generalized-Buchi 4
+Acceptance: 4 Inf(0)&Inf(1)&Inf(2)&Inf(3)
+properties: trans-labels explicit-labels trans-acc
+--BODY--
+State: 0
+[0] 0 {0}
+[1] 0 {0 1}
+[2] 0 {0 1 2}
+[3] 0 {1 3}
+[4] 0 {2 3}
+--END--
 EOF
-run 0 ../ltl2tgba -X -R3 -b aut4.txt > out4.txt
-test `grep '^acc' out4.txt | wc -w` = 6
-test `wc -l < out4.txt` = 6
-
+run 0 ../ltl2tgba -XH -R3 -H aut4.txt > out4.txt
+grep '^Acceptance: 4 ' out4.txt
+test `grep -c '\[.*\]' out4.txt` = 5
 
 # Make sure nothing wrong (like an assert())
 # happens when no acceptance conditions are used.
 cat <<EOF > aut5.txt
-acc = ;
-S1, S1, "a", ;
-S1, S1, "b", ;
-S1, S1, "c", ;
+HOA: v1
+States: 1
+Start: 0
+AP: 3 "a" "b" "c"
+acc-name: all
+Acceptance: 0 t
+properties: trans-labels explicit-labels state-acc
+--BODY--
+State: 0
+[0] 0
+[1 | 2] 0
+--END--
 EOF
-run 0 ../ltl2tgba -X -R3 -b aut5.txt > out5.txt
-test `wc -l < out5.txt` = 2
+run 0 ../ltl2tgba -XH -R3 -H aut5.txt > out5.txt
+grep '^Acceptance: 0 t' out5.txt
+test `grep -c '\[.*\]' out5.txt` = 1
 
 
-# Here, one of A,B and one of C,D can be removed.
+# Here, one of 0,1 and one of 2,3 can be removed.
 cat <<EOF > aut6.txt
-acc = A B C D;
-S1, S1, "a", A B;
-S1, S1, "b", A B;
-S1, S1, "c", C D;
-S1, S1, "d", C D;
+HOA: v1
+States: 1
+Start: 0
+AP: 4 "a" "b" "c" "d"
+acc-name: generalized-Buchi 4
+Acceptance: 4 Inf(0)&Inf(1)&Inf(2)&Inf(3)
+properties: trans-labels explicit-labels trans-acc
+--BODY--
+State: 0
+[0] 0 {0 1}
+[1] 0 {0 1}
+[2] 0 {2 3}
+[3] 0 {2 3}
+--END--
 EOF
-run 0 ../ltl2tgba -X -R3 -b aut6.txt > out6.txt
-test `grep '^acc' out6.txt | wc -w` = 4
-test `wc -l < out6.txt` = 3
-
+run 0 ../ltl2tgba -XH -R3 -H aut6.txt > out6.txt
+grep '^Acceptance: 2 ' out6.txt
+test `grep -c '\[.*\]' out6.txt` = 2
 
 # This automaton comes from the formula
 # 1 U (p0 & (!p1 R ((1 U !p2) & (1 U !p3))))
-# and and early implementation of our simplification
+# and an early implementation of our simplification
 # missed the simplification.
 cat <<EOF > aut7.txt
-acc = ZZ "!p3" "!p2";
-S1, S2, "p0 & !p2 & !p3 & !p1", ZZ "!p3" "!p2";
-S1, S1, "!p0 | p1 | p2 | p3", "!p3" "!p2";
-S1, S3, "p0 & p2 & !p3 & !p1", ZZ "!p3";
-S1, S4, "p0 & p3 & !p2 & !p1", ZZ "!p2";
-S1, S5, "(p0 & p2 & !p1) | (p0 & p3 & !p1)", ZZ;
-S1, S6, "p0 & p1 & !p2 & !p3", ZZ "!p3" "!p2";
-S1, S6, "(p0 & p1 & !p3) | (p0 & p2 & !p3)", ZZ "!p3";
-S1, S6, "(p0 & p1 & !p2) | (p0 & p3 & !p2)", ZZ "!p2";
-S1, S6, "(p0 & p1) | (p0 & p2) | (p0 & p3)", ZZ;
-S2, S2, "1", ZZ "!p3" "!p2";
-S3, S2, "!p2", ZZ "!p3" "!p2";
-S3, S3, "p2", ZZ "!p3";
-S4, S2, "!p3", ZZ "!p3" "!p2";
-S4, S4, "p3", ZZ "!p2";
-S5, S2, "!p2 & !p3", ZZ "!p3" "!p2";
-S5, S3, "p2 & !p3", ZZ "!p3";
-S5, S4, "p3 & !p2", ZZ "!p2";
-S5, S5, "p2 | p3", ZZ;
-S6, S2, "!p2 & !p3 & !p1", ZZ "!p3" "!p2";
-S6, S3, "p2 & !p3 & !p1", ZZ "!p3";
-S6, S4, "p3 & !p2 & !p1", ZZ "!p2";
-S6, S5, "(p2 & !p1) | (p3 & !p1)", ZZ;
-S6, S6, "p1 & !p2 & !p3", ZZ "!p3" "!p2";
-S6, S6, "(p1 & !p3) | (p2 & !p3)", ZZ "!p3";
-S6, S6, "(p1 & !p2) | (p3 & !p2)", ZZ "!p2";
-S6, S6, "p1 | p2 | p3", ZZ;
+HOA: v1
+States: 6
+Start: 0
+AP: 4 "p0" "p1" "p2" "p3"
+acc-name: generalized-Buchi 3
+Acceptance: 3 Inf(0)&Inf(1)&Inf(2)
+properties: trans-labels explicit-labels trans-acc complete
+--BODY--
+State: 0
+[!0 | 1 | 2 | 3] 0 {1 2}
+[0&!1&!2&!3] 1 {0 1 2}
+[0&!1&2&!3] 2 {0 1}
+[0&!1&!2&3] 3 {0 2}
+[0&!1&2 | 0&!1&3] 4 {0}
+[0&1&!2&!3] 5 {0 1 2}
+[0&1&!3 | 0&2&!3] 5 {0 1}
+[0&1&!2 | 0&!2&3] 5 {0 2}
+[0&1 | 0&2 | 0&3] 5 {0}
+State: 1
+[t] 1 {0 1 2}
+State: 2
+[!2] 1 {0 1 2}
+[2] 2 {0 1}
+State: 3
+[!3] 1 {0 1 2}
+[3] 3 {0 2}
+State: 4
+[!2&!3] 1 {0 1 2}
+[2&!3] 2 {0 1}
+[!2&3] 3 {0 2}
+[2 | 3] 4 {0}
+State: 5
+[!1&!2&!3] 1 {0 1 2}
+[!1&2&!3] 2 {0 1}
+[!1&!2&3] 3 {0 2}
+[!1&2 | !1&3] 4 {0}
+[1 | 2 | 3] 5 {0}
+[1&!2&!3] 5 {0 1 2}
+[1&!3 | 2&!3] 5 {0 1}
+[1&!2 | !2&3] 5 {0 2}
+--END--
 EOF
-run 0 ../ltl2tgba -X -R3 -b aut7.txt > out7.txt
-test `grep '^acc' out7.txt | wc -w` = 4
+run 0 ../ltl2tgba -XH -R3 -H aut7.txt > out7.txt
+grep '^Acceptance: 2 ' out7.txt
 
 
-run 0 ../ltl2tgba -R3 -b '(GFa&GFb) | (GFc&GFd)' > out8.txt
-test `grep '^acc' out8.txt | wc -w` = 4
+run 0 ../ltl2tgba -R3 -H '(GFa&GFb) | (GFc&GFd)' > out8.txt
+grep 'Acceptance: 2 ' out8.txt
 
 # This formula gives a 12-state automaton in which one acceptance
 # condition can be removed, and after what direct simulation should
diff --git a/src/tgbatest/sim2.test b/src/tgbatest/sim2.test
index d7f4a7db6..eacf6e112 100755
--- a/src/tgbatest/sim2.test
+++ b/src/tgbatest/sim2.test
@@ -1,6 +1,6 @@
 #! /bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement
+# Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -21,8 +21,7 @@
 . ./defs
 set -e
 
-../ltl2tgba -b -x -R3f -RDS '{(a&b)[*3]}<>=>G(a&!b)' > ref
-
+../ltl2tgba -H -x -R3f -RDS '{(a&b)[*3]}<>=>G(a&!b)' > ref
 
 for i in -R3 -R3f '-R3 -RDS' '-R3f -RDS'; do
   ../ltl2tgba -Pref -E -x $i '(X!b R F!a) U (!a | G!b)'