diff --git a/README b/README
index 671c2df9f..67b9f33eb 100644
--- a/README
+++ b/README
@@ -188,6 +188,7 @@ doc/              Documentation for libspot.
    userdoc/       HTML documentation about the command-line tools.
    spot.html/     HTML reference manual for the library.
 bench/            Benchmarks for ...
+   dtgbasat/      ... SAT-based minimization of DTGBA,
    emptchk/       ... emptiness-check algorithms,
    ltl2tgba/      ... LTL-to-Büchi translation algorithms,
    ltlcounter/    ... translation of a class of LTL formulae,
diff --git a/bench/Makefile.am b/bench/Makefile.am
index 9afdd3188..59beb61b6 100644
--- a/bench/Makefile.am
+++ b/bench/Makefile.am
@@ -20,4 +20,4 @@
 ## along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 SUBDIRS = emptchk ltl2tgba scc-stats split-product ltlcounter	\
-          ltlclasses wdba spin13
+          ltlclasses wdba spin13 dtgbasat
diff --git a/bench/dtgbasat/Makefile.am b/bench/dtgbasat/Makefile.am
new file mode 100644
index 000000000..8a4cea8a3
--- /dev/null
+++ b/bench/dtgbasat/Makefile.am
@@ -0,0 +1,22 @@
+## Copyright (C) 2013 Laboratoire de Recherche et Développement de
+## l'Epita (LRDE).
+##
+## This file is part of Spot, a model checking library.
+##
+## Spot is free software; you can redistribute it and/or modify it
+## under the terms of the GNU General Public License as published by
+## the Free Software Foundation; either version 3 of the License, or
+## (at your option) any later version.
+##
+## Spot is distributed in the hope that it will be useful, but WITHOUT
+## ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+## or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+## License for more details.
+##
+## You should have received a copy of the GNU General Public License
+## along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+EXTRA_DIST = formulas prepare.sh rundbamin.pl stat.sh stats.sh tabl.pl \
+             tabl1.pl tabl2.pl tabl3.pl tabl4.pl
+
+
diff --git a/bench/dtgbasat/README b/bench/dtgbasat/README
new file mode 100644
index 000000000..653a1fc68
--- /dev/null
+++ b/bench/dtgbasat/README
@@ -0,0 +1,64 @@
+These are the benchmark for our submission to VMCAI'14.
+
+To reproduce, follow these instructions:
+
+1) Compile Spot and install if it is not already done.
+
+2) Compile Glucose from https://www.lri.fr/~simon/?page=glucose
+   and make sure the 'glucose' binary is in your PATH.
+
+3) Compile ltl2dstar from http://www.ltl2dstar.de/ and
+   make sure the 'ltl2dstar' binary is in your path.
+
+4) Compile DBAminimizer from
+   http://www.react.uni-saarland.de/tools/dbaminimizer
+
+   and define the path to minimize.py with
+
+   % export DBA_MINIMIZER=$HOME/dbaminimizer/minimize.py
+
+5) Then make sure you are in this directory:
+
+   % cd bench/dtgbasat/
+
+6) Classify the set of formulas with
+
+   % ./prepare.sh
+
+   This will read the formulas from file "formulas" and output a file
+   "info.ltl", in which each formula is associated to a class (the â‘ ,
+   â‘¡, â‘¡, and â‘£ of the paper), and a number of acceptance conditions
+   (the "m" of the paper).
+
+7) Build a makefile to run all experiments
+
+   % ./stats.sh
+
+8) You may optionally change the directory that contains temporary
+    files with
+
+   % export TMPDIR=someplace
+
+   (These temporary files can be several GB large.)
+
+   Note that runtime will be limited to 2h, but memory is not bounded.
+   You should set such a limit with "ulimit" if you like.  For instance
+   % ulimit -v 41943040
+
+9) Actually run all experiments
+
+   % make -j4 stat.mk
+
+   This will build a CSV file called "all.log".
+
+10) You may generate LaTeX code for the tables with the scripts:
+   - tabl.pl: Full data.
+   - tabl1.pl, tabl2.pl, tabl3.pl, tabl4.pl: Partial tables as shown
+   in the paper.
+
+   All these script takes the CSV file all.log as first argument, and
+   output LaTeX to their standard output.
+
+
+For more instruction about how to use ltl2tgba and dstar2tgba to
+compute minimal DTGBA or DTBA, please read doc/userdoc/satmin.html
diff --git a/bench/dtgbasat/formulas b/bench/dtgbasat/formulas
new file mode 100644
index 000000000..3a5a04e52
--- /dev/null
+++ b/bench/dtgbasat/formulas
@@ -0,0 +1,132 @@
+# Formulas from Gasier et al., "Rabinizer: Small deterministic
+# automata for LTL(F,G)" (ATVA'12)
+G(a | Fb)
+FGa | FGb | GFc
+F(a | b)
+GF(a | b)
+G(a | Fa)
+G(a | b | c)
+G(a | F(b | c))
+Fa | Gb
+G(a | F(b & c))
+FGa | GFb
+GF(a | b) & GF(b | c)
+
+FF(a & G!a) | (GG!a & Fa)
+GFa & FGb
+(GFa & FGb) | (FG!a & GF!b)
+FGa & GFa
+G(Fa & Fb)
+Fa & F!a
+G(b | GFa) & G(c | GF!a) | Gb | Gc
+G(b | FGa) & G(c | FG!a) | Gb | Gc
+F(b & FGa) | F(c & FG!a) & Fb & Fc
+F(b & GFa) | F(c & GF!a) & Fb & Fc
+
+GFa -> GFb
+(GFa -> GFb) & (GFc -> GFd)
+
+GF(Fa | GFb | FG(a | b))
+FG(Fa | GFb | FG(a | b))
+FG(Fa | GFb | FG(a | b) | FGb)
+
+# formulas from DBA minimizer
+XXa
+GF(a -> XXXb)
+F(p & XF(q & XF(r & XFs)))
+F(q & X(p U r))
+F(p & X(q & XFr))
+p U (q & X(r U s))
+G(a -> Fb) & G(c -> Fd)
+GFa & GFb
+GFa | GFb | GFc
+GFa
+a U b U c U d
+G(a -> Fb) & Gc
+(Ga -> Fb) & (G!a -> F!b)
+p U (q & X(r & F(s & XF(u & XF(v & XFw)))))
+G(a -> Fb) & G(b -> Fc)
+G(a -> Fb) & G(!a -> F!b)
+GFp && GFq && GF r && GF u
+GF(a <-> XXXb)
+G(p -> q U r)
+GF(a <-> XXb)
+G!c & G(a -> Fb) & G(b -> Fc)
+G(a -> XXXb)
+G(a -> Fb)
+G(a U b U !a U !b)
+(p U q U r) || (q U r U p) || (r U p U q)
+
+# Some random formulas that are determinizable with tba-det
+X((a M F((!c & !b) | (c & b))) W (G!c U b))
+X(((a & b) R (!a U !c)) R b)
+XXG(Fa U Xb)
+(!a M !b) W F!c
+(b & Fa & GFc) R a
+(a R (b W a)) W G(!a M (c | b))
+(Fa W b) R (Fc | !a)
+X(G(!a M !b) | G(a | G!a))
+Fa W Gb
+Ga | GFb
+a M G(F!b | X!a)
+G!a R XFb
+XF(!a | GFb)
+G(F!a U !a) U Xa
+(a | G(a M !b)) W Fc
+Fa W Xb
+X(a R ((!b & F!c) M X!a))
+XG!a R Fb
+GFc | (a & Fb)
+X(a R (Fb R F!b))
+G(Xa M Fa)
+X(Gb | GFa)
+X(Gc | XG((b & Ga) | (!b & F!a)))
+Ga R Fb
+G(a U (b | X((!c & !a) | (a & c))))
+XG((G!a & F!b) | (Fa & (a | Gb)))
+(a U X!a) | XG(!b & XFc)
+X(G!a | GFa)
+G(G!a | F!c | G!b)
+
+# Some random formulas that should only be determinizable via dstar2tgba
+# Generated with
+# randltl -n -1 a b c |
+# ltlfilt --remove-wm -r -u --size-min=3 --size-max=15 --syntactic-recurrence |
+# ltlfilt -v --obligation |
+# ../../src/bin/ltl2tgba -F - -x tba-det -D --stats='%d,%f' |
+# grep 0, | head -n 30
+
+X(Fc W b) R Fa
+!b & ((Fa U b) W Xc)
+G(F!c | (Fb U a))
+(c R (b R Fa)) W XGb
+X((Fb & XFa) R XFc)
+(Ga R (F!c U b)) W b
+X(!b | G(b & !a)) R F(c & Fa)
+G(Fc | Ga | XXF!b)
+G(F(!a & Fa) U (b U Xc))
+G(F!c U X(Xb & F!b))
+G(XXFa U (b | a | Fc))
+G(c | F!a | (b U Xb))
+G(a U X(a | (F!b U Xc)))
+XF!a R F(b | (!a & F!c))
+(c & Xc) R ((!b | XFc) U a)
+G(Gb | (b & c) | F(!a & XXa))
+G(X(Fc & Xa) M Fb)
+X(!c & Fc) R (c M Fa)
+G(Ga | X(Fc U (b | X!b)))
+G(XXFb U (c | (!c & F!a)))
+((Fc U b) R Fa) W X!a
+G(a | X(a R (GFb | (Fc U a))))
+(F!c R F!b) W G!a
+(Fb & !b) R (!a R XFc)
+F(Fb & c) W Xa
+G(G!c | ((Fb U a) U c))
+(Fa & XXb) R Fc
+Gc R (F!a & (b U a))
+(c R Fa) U X!b
+GF(b & XXXFc)
+
+# Extra ones
+G(F(a & F(b & Fc)))
+(GFa & GFb) | (GFc & GFd)
diff --git a/bench/dtgbasat/prepare.sh b/bench/dtgbasat/prepare.sh
new file mode 100755
index 000000000..37819ce95
--- /dev/null
+++ b/bench/dtgbasat/prepare.sh
@@ -0,0 +1,24 @@
+#!/bin/sh
+
+ltlfilt=../../src/bin/ltlfilt
+ltl2tgba=../../src/bin/ltl2tgba
+dstar2tgba=../../src/bin/dstar2tgba
+
+# Rename all formulas using a b c... suppress duplicates.
+$ltlfilt -q --relabel=abc -u formulas > nodups.ltl
+
+while read f; do
+  acc=`$ltl2tgba "$f" --low -a --stats="%a"`
+  acc2=`$ltl2tgba "$f" -D --stats="%a"`
+  if $ltlfilt -f "$f" --obligation >/dev/null; then
+     echo "$f, WDBA, $acc, $acc2"
+  elif test `$ltl2tgba "$f" -D --stats="%d"` = 1; then
+     echo "$f, trad, $acc, $acc2"
+  elif test `$ltl2tgba "$f" -x tba-det -D --stats="%d"` = 1; then
+     echo "$f, TCONG, $acc, $acc2"
+  elif test `$ltlfilt --remove-wm -f "$f" -l | ltl2dstar --ltl2nba=spin:$ltl2tgba@-sD - - | $dstar2tgba -D --low --stats="%d"` = 1; then
+     echo "$f, DRA, $acc, $acc2"
+  else
+     echo "$f, not DBA-realizable, $acc, $acc2"
+  fi
+done < nodups.ltl | tee info.ltl
diff --git a/bench/dtgbasat/rundbamin.pl b/bench/dtgbasat/rundbamin.pl
new file mode 100755
index 000000000..833194826
--- /dev/null
+++ b/bench/dtgbasat/rundbamin.pl
@@ -0,0 +1,17 @@
+#!/usr/bin/perl -w
+
+use strict;
+use Time::HiRes;
+
+my $start = Time::HiRes::gettimeofday();
+my $res = `@ARGV` || die;
+my $end = Time::HiRes::gettimeofday();
+
+if ($res =~ /States:\s*(\d+)\w*$/som)
+{
+    printf("%d, %f\n", $1, $end - $start);
+}
+else
+{
+    printf("-, -\n");
+}
diff --git a/bench/dtgbasat/stat.sh b/bench/dtgbasat/stat.sh
new file mode 100755
index 000000000..e8a5e4538
--- /dev/null
+++ b/bench/dtgbasat/stat.sh
@@ -0,0 +1,105 @@
+#!/bin/sh
+
+ltlfilt=../../src/bin/ltlfilt
+ltl2tgba=../../src/bin/ltl2tgba
+dstar2tgba=../../src/bin/dstar2tgba
+timeout='timeout -sKILL 2h'
+stats=--stats="%s, %e, %t, %a, %c, %d, %p, %r"
+empty='-, -, -, -, -, -, -, -'
+tomany='!, !, !, !, !, !, !, !'
+dbamin=${DBA_MINIMIZER-/home/adl/projs/dbaminimizer/minimize.py}
+
+get_stats()
+{
+   $timeout "$@" "$stats" > stdin.$$ 2>stderr.$$
+   if grep -q 'INT_MAX' stderr.$$; then
+       # Too many SAT-clause?
+       echo "$tomany"
+   else
+       tmp=`cat stdin.$$`
+       echo ${tmp:-$empty}
+   fi
+   rm -f stdin.$$ stderr.$$
+}
+
+get_dbamin_stats()
+{
+    tmp=`./rundbamin.pl $timeout $dbamin "$@"`
+    mye='-, -'
+    echo ${tmp:-$mye}
+}
+
+
+f=$1
+type=$2
+accmax=$3
+
+case $type in
+    *WDBA*)
+	echo "$f, $accmax, $type..." 1>&2
+	input=`get_stats $ltl2tgba "$f" -BD`
+	dba=$input
+	echo "$f, $accmax, $type, $input, DBA, $dba, minDBA..." 1>&2
+	mindba=`get_stats $ltl2tgba "$f" -BD -x 'sat-minimize=-1'`
+	echo "$f, $accmax, $type, $input, DBA, $dba, minDBA, $mindba, minDTGBA..." 1>&2
+	mindtgba=`get_stats $ltl2tgba "$f" -D -x 'sat-minimize=-1'`
+	echo "$f, $accmax, $type, $input, DBA, $dba, minDBA, $mindba, minDTGBA, $mindtgba, minDTBA..." 1>&2
+	mindtba=`get_stats $ltl2tgba "$f" -D -x 'sat-minimize=-1,sat-acc=1'`
+	echo "$f, $accmax, $type, $input, DBA, $dba, minDBA, $mindba, minDTGBA, $mindtgba, minDTBA, $mindtba, dbaminimizer..." 1>&2
+	$ltlfilt --remove-wm -f "$f" -l |
+	ltl2dstar --ltl2nba=spin:$ltl2tgba@-sD - dra.$$
+	dbamin=`get_dbamin_stats dra.$$`
+	dra=`sed -n 's/States: \(.*\)/\1/p' dra.$$`
+	rm dra.$$
+	;;
+    *TCONG*|*trad*)  # Not in WDBA
+	echo "$f, $accmax, $type..." 1>&2
+	input=`get_stats $ltl2tgba "$f" -D -x '!wdba-minimize,tba-det'`
+	echo "$f, $accmax, $type, $input, DBA, ..." 1>&2
+	dba=`get_stats $ltl2tgba "$f" -BD -x '!wdba-minimize,tba-det'`
+	echo "$f, $accmax, $type, $input, DBA, $dba, minDBA..." 1>&2
+	mindba=`get_stats $ltl2tgba "$f" -BD -x '!wdba-minimize,sat-minimize'`
+	echo "$f, $accmax, $type, $input, DBA, $dba, minDBA, $mindba, minDTGBA..." 1>&2
+	mindtgba=`get_stats $ltl2tgba "$f" -D -x '!wdba-minimize,sat-minimize'`
+	echo "$f, $accmax, $type, $input, DBA, $dba, minDBA, $mindba, minDTGBA, $mindtgba, minDTBA..." 1>&2
+	mindtba=`get_stats $ltl2tgba "$f" -D -x '!wdba-minimize,sat-minimize,sat-acc=1'`
+	echo "$f, $accmax, $type, $input, DBA, $dba, minDBA, $mindba, minDTGBA, $mindtgba, minDTBA, $mindtba, dbaminimizer..." 1>&2
+	case $type in
+	    *TCONG*)   dbamin="n/a, n/a"  dra="n/a";;
+            *trad*)
+	       $ltlfilt --remove-wm -f "$f" -l |
+	       ltl2dstar --ltl2nba=spin:$ltl2tgba@-sD - dra.$$
+	       dbamin=`get_dbamin_stats dra.$$`
+	       dra=`sed -n 's/States: \(.*\)/\1/p' dra.$$`
+	       rm dra.$$
+	       ;;
+	esac
+	;;
+    *DRA*)
+	echo "$f, $accmax, $type... " 1>&2
+	$ltlfilt --remove-wm -f "$f" -l |
+	ltl2dstar --ltl2nba=spin:$ltl2tgba@-sD - dra.$$
+	input=`get_stats $dstar2tgba dra.$$ -D -x '!wdba-minimize'`
+	echo "$f, $accmax, $type, $input, DBA, ... " 1>&2
+	dba=`get_stats $dstar2tgba dra.$$ -BD -x '!wdba-minimize'`
+	echo "$f, $accmax, $type, $input, DBA, $dba, minDBA... " 1>&2
+	mindba=`get_stats $dstar2tgba dra.$$ -BD -x '!wdba-minimize,sat-minimize'`
+	echo "$f, $accmax, $type, $input, DBA, $dba, minDBA, $mindba, minDTGBA..." 1>&2
+	mindtgba=`get_stats $dstar2tgba dra.$$ -D -x '!wdba-minimize,sat-acc='$accmax`
+	echo "$f, $accmax, $type, $input, DBA, $dba, minDBA, $mindba, minDTGBA, $mindtgba, minDTBA..." 1>&2
+	mindtba=`get_stats $dstar2tgba dra.$$ -D -x '!wdba-minimize,sat-acc=1'`
+	echo "$f, $accmax, $type, $input, DBA, $dba, minDBA, $mindba, minDTGBA, $mindtgba, minDTBA, $mindtba, dbaminimizer..." 1>&2
+	dbamin=`get_dbamin_stats dra.$$`
+	dra=`sed -n 's/States: \(.*\)/\1/p' dra.$$`
+	rm -f dra.$$
+	;;
+    *not*)
+	exit 0
+	;;
+    *)
+	echo "SHOULD NOT HAPPEND"
+	exit 2
+	;;
+esac
+echo "$f, $accmax, $type, $input, DBA, $dba, minDBA, $mindba, minDTGBA, $mindtgba, minDTBA, $mindtba, dbaminimizer, $dbamin, DRA, $dra" 1>&2
+echo "$f, $accmax, $type, $input, DBA, $dba, minDBA, $mindba, minDTGBA, $mindtgba, minDTBA, $mindtba, dbaminimizer, $dbamin, DRA, $dra"
diff --git a/bench/dtgbasat/stats.sh b/bench/dtgbasat/stats.sh
new file mode 100755
index 000000000..337d312e5
--- /dev/null
+++ b/bench/dtgbasat/stats.sh
@@ -0,0 +1,42 @@
+#!/bin/sh
+
+ltlfilt=../../src/bin/ltlfilt
+ltl2tgba=../../src/bin/ltl2tgba
+dstar2tgba=../../src/bin/dstar2tgba
+timeout='timeout -sKILL 1h'
+stats=--stats="%s, %e, %t, %a, %c, %d, %p, %r"
+empty='-, -, -, -, -, -, -, -'
+
+rm -f stats.mk stats.tmp
+
+n=1
+all=
+
+while IFS=, read f type accmax accmin; do
+  unset IFS
+
+  case $type in
+  *TCONG*)
+    echo "$n.log:; ./stat.sh '$f' $type $accmax >\$@" >> stats.tmp
+    all="$all $n.log"
+    n=`expr $n + 1`
+    echo "$n.log:; ./stat.sh '$f' DRA-CONG $accmax >\$@" >> stats.tmp
+    all="$all $n.log"
+    n=`expr $n + 1`
+    ;;
+  *)
+    echo "$n.log:; ./stat.sh '$f' $type $accmax >\$@" >> stats.tmp
+    all="$all $n.log"
+    n=`expr $n + 1`
+    ;;
+  esac
+done < info.ltl
+
+cat > stats.mk <<EOF
+ALL = $all
+all.log: \$(ALL)
+	cat \$(ALL) >\$@
+EOF
+cat stats.tmp >> stats.mk
+
+echo "Now, run something like: make -j8 -f stats.mk"
diff --git a/bench/dtgbasat/tabl.pl b/bench/dtgbasat/tabl.pl
new file mode 100755
index 000000000..01006ff03
--- /dev/null
+++ b/bench/dtgbasat/tabl.pl
@@ -0,0 +1,235 @@
+#!/usr/bin/perl -w
+
+use strict;
+
+my $num = 0;
+my @v = ();
+while (<>)
+{
+    # G(a | Fb), 1, trad, 2, 4, 8, 1, 1, 1, 1, 0.00165238, DBA, 2, 4, 8, 1, 1, 1, 1, 0.00197852, minDBA, 2, 4, 8, 1, 1, 1, 1, 0.00821457, minDTGBA, 2, 4, 8, 1, 1, 1, 1, 0.0081701
+    chomp;
+    next if /.*realizable.*/;
+    $v[$num] = [split /,/];
+#    print $v[$num]->[48], " ",  $#{$v[$num]}, "\n";
+#    if ($#{$v[$num]} != 49)
+#    {
+#	pop $v[$num];
+#	push $v[$num], '-', '-';
+#   }
+#    print $v[$num]->[48], " ",  $#{$v[$num]}, "\n";
+
+    ++$num;
+}
+
+sub dratcong($$)
+{
+    my ($a, $b) = @_;
+    return 0 if ($a =~ /.*CONG/ && $b =~ /.*CONG/);
+    return $a cmp $b;
+}
+
+sub mycmp()
+{
+    my $v = dratcong($b->[2], $a->[2]);
+    return $v if $v;
+    my $n1 = lc $a->[0];
+    $n1 =~ s/\W//g;
+    my $n2 = lc $b->[0];
+    $n2 =~ s/\W//g;
+    return $n1 cmp $n2 || $a->[0] cmp $b->[0] || $b->[2] cmp $a->[2];;
+}
+
+my @w = sort mycmp @v;
+
+print "\\documentclass{standalone}\n
+\\usepackage{amsmath}
+\\usepackage{colortbl}
+\\definecolor{mygray}{gray}{0.75} % 1 = white, 0 = black
+\\definecolor{lightgray}{gray}{0.7} % 1 = white, 0 = black
+\\def\\E{\\cellcolor{mygray}}
+\\def\\P{\\cellcolor{red}}
+\\def\\PP{\\cellcolor{yellow}}
+\\def\\F{\\mathsf{F}} % in future
+\\def\\G{\\mathsf{G}} % globally
+\\def\\X{\\mathsf{X}} % next
+\\DeclareMathOperator{\\W}{\\mathbin{\\mathsf{W}}} % weak until
+\\DeclareMathOperator{\\M}{\\mathbin{\\mathsf{M}}} % strong release
+\\DeclareMathOperator{\\U}{\\mathbin{\\mathsf{U}}} % until
+\\DeclareMathOperator{\\R}{\\mathbin{\\mathsf{R}}} % release
+";
+
+print "\\begin{document}\n";
+print "\\begin{tabular}{lrcr|r|rrrr|rrr|rr|rrr|rrr|rrrr}";
+print "\\multicolumn{24}{l}{Column \\textbf{type} shows how the initial deterministic automaton was obtained: T = translation produces DTGBA; W = WDBA minimization works; P = powerset construction transforms TBA to DTBA; R = DRA to DBA.}\\\\\n";
+print "\\multicolumn{24}{l}{Column \\textbf{C.} tells whether the output automaton is complete: rejecting sink states are always omitted (add 1 state when C=0 if you want the size of the complete automaton).}\\\\\n";
+print "&&&&DRA&\\multicolumn{4}{|c}{DTGBA} & \\multicolumn{3}{|c}{DBA} &  \\multicolumn{2}{|c}{DBA\\footnotesize minimizer}&  \\multicolumn{3}{|c}{min DBA} & \\multicolumn{3}{|c}{minDTBA} & \\multicolumn{4}{|c}{minDTGBA}\\\\\n";
+print "formula & \$m\$ & type & C. & st. & st. & tr. & acc. & time & st. & tr. & time & st. & time & st. & tr. & time & st. & tr. & time & st. & tr. & acc. & time \\\\\n";
+
+sub nonnull($)
+{
+    return 1 if $_[0] == 0;
+    return $_[0];
+}
+
+
+my $lasttype = '';
+my $linenum = 0;
+foreach my $tab (@w)
+{
+    sub val($)
+    {
+	my ($n) = @_;
+	my $v = $tab->[$n];
+	return 0+'inf' if !defined($v) || $v =~ /\s*-\s*/;
+	return $v;
+    }
+
+    if (dratcong($lasttype, $tab->[2]))
+    {
+	print "\\hline\n";
+	$linenum = 0;
+    }
+    $lasttype = $tab->[2];
+    if ($linenum++ % 4 == 0)
+    {
+	print "\\arrayrulecolor{lightgray}\\hline\\arrayrulecolor{black}";
+    }
+
+    my $f = $tab->[0];
+    $f =~ s/\&/\\land /g;
+    $f =~ s/\|/\\lor /g;
+    $f =~ s/!/\\bar /g;
+    $f =~ s/<->/\\leftrightarrow /g;
+    $f =~ s/->/\\rightarrow /g;
+    $f =~ s/[XRWMGFU]/\\$& /g;
+    print "\$$f\$\t& ";
+    print "$tab->[1] & ";
+    if ($tab->[2] =~ /trad/) { print "T & "; }
+    elsif ($tab->[2] =~ /TCONG/) { print "P & "; }
+    elsif ($tab->[2] =~ /DRA/) { print "R & "; }
+    elsif ($tab->[2] =~ /WDBA/) { print "W & "; }
+    else { print "$tab->[2]& "; }
+    # If one of the automata is not deterministic highlight the "Complete" column.
+    print "{\\P}" if val(8) == 0 || val(17) == 0 || val(26) == 0 || val(35) == 0  || val(44) == 0;
+    print "$tab->[9] & ";
+
+    if ($tab->[51] =~ m:\s*n/a\s*:) #  DRA
+    {
+	print "&";
+	$tab->[51] = 0+'inf';
+    }
+    else
+    {
+	# Remove sink state if not complete.
+	my $st = $tab->[51] - 1 + $tab->[9] || 1;
+	print "$st & ";
+    }
+
+    print "$tab->[3] & "; # states
+    print "$tab->[5] & "; # transitions
+    print "$tab->[6] & "; # acc
+    printf("%.2f &", $tab->[10]);
+
+    if ($tab->[12] =~ /\s*-\s*/)  # DBA
+    {
+	print "- & - & - &";
+	$tab->[12] = 0+'inf';
+    }
+    elsif ($tab->[12] =~ /\s*!\s*/)  # DBA
+    {
+	print "! & ! & ! &";
+	$tab->[12] = 0+'inf';
+    }
+    else
+    {
+	print "$tab->[12] & "; # states
+	print "$tab->[14] & "; # transitions
+	printf("%.2f &", $tab->[19]);
+    }
+
+    if ($tab->[48] =~ /\s*-\s*/) #  DBAminimizer
+    {
+	print "\\multicolumn{2}{c|}{(killed)}&";
+	$tab->[48] = 0+'inf';
+    }
+    elsif ($tab->[48] =~ m:\s*n/a\s*:) #  DBAminimizer
+    {
+	print " & &";
+	$tab->[48] = 0+'inf';
+    }
+    else
+    {
+	# Remove sink state if not complete.
+	my $st = $tab->[48] - 1 + $tab->[9] || 1;
+	print "{\\E}" if ($st < $tab->[12]);
+	print "{\\P}" if ($st > $tab->[12]);
+	print "$st & "; # states
+	printf("%.2f &", $tab->[49]);
+    }
+
+    if ($tab->[21] =~ /\s*-\s*/) #  minDBA
+    {
+	print "\\multicolumn{3}{c|}{(killed)}&";
+	$tab->[21] = 0+'inf';
+    }
+    elsif ($tab->[21] =~ /\s*!\s*/) #  minDBA
+    {
+	print "\\multicolumn{3}{c|}{(intmax)}&";
+	$tab->[21] = 0+'inf';
+    }
+    else
+    {
+	print "{\\E}" if ($tab->[21] < $tab->[12]);
+	print "{\\P}" if ($tab->[21] > $tab->[12]);
+	print "$tab->[21] & "; # states
+	print "$tab->[23] & "; # transitions
+	printf("%.2f &", $tab->[28]);
+    }
+
+    if ($tab->[39] =~ /\s*-\s*/) # min DTBA
+    {
+	print "\\multicolumn{3}{c|}{(killed)}&";
+	$tab->[39] = 0+'inf';
+    }
+    elsif ($tab->[39] =~ /\s*!\s*/) # min DTBA
+    {
+	print "\\multicolumn{3}{c|}{(intmax)}&";
+	$tab->[39] = 0+'inf';
+    }
+    else
+    {
+	print "{\\E}" if ($tab->[39] < $tab->[3]);
+	print "{\\P}" if ($tab->[39] > $tab->[3] * nonnull($tab->[6])) or ($tab->[39] > $tab->[12]);
+	print "\\textbf" if ($tab->[39] < $tab->[21]);
+	print "{$tab->[39]} & "; # states
+	print "$tab->[41] & "; # transitions
+	printf("%.2f &", $tab->[46]);
+    }
+
+    if ($tab->[30] =~ /\s*-\s*/)   # minTGBA
+    {
+	print "\\multicolumn{4}{c}{(killed)}";
+	$tab->[30] = 0+'inf';
+    }
+    elsif ($tab->[30] =~ /\s*!\s*/)   # minTGBA
+    {
+	print "\\multicolumn{4}{c}{(intmax)}";
+	$tab->[30] = 0+'inf';
+    }
+    else
+    {
+	print "{\\E}" if ($tab->[30] < $tab->[3]);
+	print "{\\P}" if ($tab->[30] > $tab->[3]) or ($tab->[30] > $tab->[12]) or ($tab->[30] > $tab->[21]) or ($tab->[30] > $tab->[39]);
+	print "{\\PP}" if ($tab->[21] ne 'inf' && $tab->[30] * ($tab->[33] + 1) < $tab->[21]);
+	print "\\textbf" if ($tab->[30] < $tab->[39]);
+	print "{$tab->[30]} & "; # states
+	print "$tab->[32] & "; # transitions
+	print "\\textbf" if ($tab->[33] > $tab->[6]);
+	print "{$tab->[33]} & "; # acc
+	printf("%.2f ", $tab->[37]);
+    }
+
+    print "\\\\\n";
+}
+print "\\end{tabular}\n";
+print "\\end{document}\n";
diff --git a/bench/dtgbasat/tabl1.pl b/bench/dtgbasat/tabl1.pl
new file mode 100755
index 000000000..9e2ebcda7
--- /dev/null
+++ b/bench/dtgbasat/tabl1.pl
@@ -0,0 +1,170 @@
+#!/usr/bin/perl -w
+
+use strict;
+
+my $num = 0;
+my @v = ();
+while (<>)
+{
+    # G(a | Fb), 1, trad, 2, 4, 8, 1, 1, 1, 1, 0.00165238, DBA, 2, 4, 8, 1, 1, 1, 1, 0.00197852, minDBA, 2, 4, 8, 1, 1, 1, 1, 0.00821457, minDTGBA, 2, 4, 8, 1, 1, 1, 1, 0.0081701
+    chomp;
+    next if /.*realizable.*/;
+    next unless /WDBA/;
+    $v[$num] = [split /,/];
+    ++$num;
+}
+
+sub dratcong($$)
+{
+    my ($a, $b) = @_;
+    return 0 if ($a =~ /.*CONG/ && $b =~ /.*CONG/);
+    return $a cmp $b;
+}
+
+sub mycmp()
+{
+    my $v = dratcong($b->[2], $a->[2]);
+    return $v if $v;
+    my $n1 = lc $a->[0];
+    $n1 =~ s/\W//g;
+    my $n2 = lc $b->[0];
+    $n2 =~ s/\W//g;
+    return $n1 cmp $n2 || $a->[0] cmp $b->[0] || $b->[2] cmp $a->[2];;
+}
+
+my @w = sort mycmp @v;
+
+print "\\documentclass{standalone}\n
+\\usepackage{amsmath}
+\\usepackage{colortbl}
+\\usepackage{booktabs}
+\\definecolor{mygray}{gray}{0.75} % 1 = white, 0 = black
+\\definecolor{lightgray}{gray}{0.7} % 1 = white, 0 = black
+\\def\\E{\\cellcolor{mygray}}
+\\def\\P{\\cellcolor{red}}
+\\def\\PP{\\cellcolor{yellow}}
+\\def\\F{\\mathsf{F}} % in future
+\\def\\G{\\mathsf{G}} % globally
+\\def\\X{\\mathsf{X}} % next
+\\DeclareMathOperator{\\W}{\\mathbin{\\mathsf{W}}} % weak until
+\\DeclareMathOperator{\\M}{\\mathbin{\\mathsf{M}}} % strong release
+\\DeclareMathOperator{\\U}{\\mathbin{\\mathsf{U}}} % until
+\\DeclareMathOperator{\\R}{\\mathbin{\\mathsf{R}}} % release
+";
+
+print "\\begin{document}\n";
+print "\\begin{tabular}{lc|c|rr|c|r}";
+print "&& \\multicolumn{1}{c|}{minDBA} & trad & +SAT & DRA & {DBA\\footnotesize m..zer} \\\\\n";
+print " & C. & \$|Q|\$ & time & time & \$|Q|\$ & time \\\\\n";
+print "\\midrule\n";
+
+sub nonnull($)
+{
+    return 1 if $_[0] == 0;
+    return $_[0];
+}
+
+
+my $lasttype = '';
+my $linenum = 0;
+foreach my $tab (@w)
+{
+    sub val($)
+    {
+	my ($n) = @_;
+	my $v = $tab->[$n];
+	return 0+'inf' if !defined($v) || $v =~ /\s*-\s*/;
+	return $v;
+    }
+
+    $lasttype = $tab->[2];
+    if ($linenum++ % 4 == 0)
+    {
+	# print "\\arrayrulecolor{lightgray}\\hline\\arrayrulecolor{black}";
+    }
+
+    my $f = $tab->[0];
+    $f =~ s/\&/\\land /g;
+    $f =~ s/\|/\\lor /g;
+    $f =~ s/!/\\bar /g;
+    $f =~ s/<->/\\leftrightarrow /g;
+    $f =~ s/->/\\rightarrow /g;
+    $f =~ s/[XRWMGFU]/\\$& /g;
+    print "\$$f\$\t& ";
+    # If one of the automata is not deterministic highlight the "Complete" column.
+    print "{\\P}" if val(8) == 0 || val(17) == 0 || val(26) == 0 || val(35) == 0  || val(44) == 0;
+    print "$tab->[9] & ";
+
+    # print "$tab->[3] & "; # states
+    # print "$tab->[5] & "; # transitions
+    # print "$tab->[6] & "; # acc
+    # printf("%.2f &", $tab->[10]);
+
+    if ($tab->[12] =~ /\s*-\s*/)  # DBA
+    {
+	print "- & - &";
+	$tab->[12] = 0+'inf';
+    }
+    elsif ($tab->[12] =~ /\s*!\s*/)  # DBA
+    {
+	print "! & ! &";
+	$tab->[12] = 0+'inf';
+    }
+    else
+    {
+	print "$tab->[12] & "; # states
+	# print "$tab->[14] & "; # transitions
+	printf("%.2f &", $tab->[19]);
+    }
+
+    if ($tab->[21] =~ /\s*-\s*/) #  minDBA
+    {
+	print "\\multicolumn{1}{c|}{(killed)}&";
+	$tab->[21] = 0+'inf';
+    }
+    elsif ($tab->[21] =~ /\s*!\s*/) #  minDBA
+    {
+	print "\\multicolumn{1}{c|}{(\$>\$INTMAX)}&";
+	$tab->[21] = 0+'inf';
+    }
+    else
+    {
+	printf("%.2f &", $tab->[28]);
+    }
+
+    if ($tab->[51] =~ m:\s*n/a\s*:) #  DRA
+    {
+	print "&";
+	$tab->[51] = 0+'inf';
+    }
+    else
+    {
+	# Remove sink state if not complete.
+	my $st = $tab->[51] - 1 + $tab->[9] || 1;
+	print "\\textbf" if ($st > $tab->[12]);
+	print "{$st} & ";
+    }
+
+    if ($tab->[48] =~ /\s*-\s*/) #  DBAminimizer
+    {
+	print "\\multicolumn{1}{c}{(killed)}&";
+	$tab->[48] = 0+'inf';
+    }
+    elsif ($tab->[48] =~ m:\s*n/a\s*:) #  DBAminimizer
+    {
+	print " &";
+	$tab->[48] = 0+'inf';
+    }
+    else
+    {
+	# Remove sink state if not complete.
+	my $st = $tab->[48] - 1 + $tab->[9] || 1;
+	print "{\\E}" if ($st < $tab->[12]);
+	print "{\\P}" if ($st > $tab->[12]);
+	printf("%.2f", $tab->[49]);
+    }
+
+    print "\\\\\n";
+}
+print "\\end{tabular}\n";
+print "\\end{document}\n";
diff --git a/bench/dtgbasat/tabl2.pl b/bench/dtgbasat/tabl2.pl
new file mode 100755
index 000000000..cd98d8a97
--- /dev/null
+++ b/bench/dtgbasat/tabl2.pl
@@ -0,0 +1,245 @@
+#!/usr/bin/perl -w
+
+use strict;
+
+my $num = 0;
+my @v = ();
+while (<>)
+{
+    # G(a | Fb), 1, trad, 2, 4, 8, 1, 1, 1, 1, 0.00165238, DBA, 2, 4, 8, 1, 1, 1, 1, 0.00197852, minDBA, 2, 4, 8, 1, 1, 1, 1, 0.00821457, minDTGBA, 2, 4, 8, 1, 1, 1, 1, 0.0081701
+    chomp;
+    next if /.*realizable.*/;
+    next unless /trad/;
+    $v[$num] = [split /,/];
+#    print $v[$num]->[48], " ",  $#{$v[$num]}, "\n";
+#    if ($#{$v[$num]} != 49)
+#    {
+#	pop $v[$num];
+#	push $v[$num], '-', '-';
+#   }
+#    print $v[$num]->[48], " ",  $#{$v[$num]}, "\n";
+
+    ++$num;
+}
+
+sub dratcong($$)
+{
+    my ($a, $b) = @_;
+    return 0 if ($a =~ /.*CONG/ && $b =~ /.*CONG/);
+    return $a cmp $b;
+}
+
+sub mycmp()
+{
+    my $v = dratcong($b->[2], $a->[2]);
+    return $v if $v;
+    my $n1 = lc $a->[0];
+    $n1 =~ s/\W//g;
+    my $n2 = lc $b->[0];
+    $n2 =~ s/\W//g;
+    return $n1 cmp $n2 || $a->[0] cmp $b->[0] || $b->[2] cmp $a->[2];;
+}
+
+my @w = sort mycmp @v;
+
+print "\\documentclass{standalone}\n
+\\usepackage{amsmath}
+\\usepackage{colortbl}
+\\usepackage{booktabs}
+\\definecolor{mygray}{gray}{0.75} % 1 = white, 0 = black
+\\definecolor{lightgray}{gray}{0.7} % 1 = white, 0 = black
+\\def\\E{\\cellcolor{mygray}}
+\\def\\P{\\cellcolor{red}}
+\\def\\PP{\\cellcolor{yellow}}
+\\def\\F{\\mathsf{F}} % in future
+\\def\\G{\\mathsf{G}} % globally
+\\def\\X{\\mathsf{X}} % next
+\\newcommand{\\CF}{\\ensuremath{\\mathcal{F}}}
+\\DeclareMathOperator{\\W}{\\mathbin{\\mathsf{W}}} % weak until
+\\DeclareMathOperator{\\M}{\\mathbin{\\mathsf{M}}} % strong release
+\\DeclareMathOperator{\\U}{\\mathbin{\\mathsf{U}}} % until
+\\DeclareMathOperator{\\R}{\\mathbin{\\mathsf{R}}} % release
+\\usepackage{adjustbox}
+\\usepackage{array}
+\\def\\clap#1{\\hbox to 0pt{\\hss#1\\hss}}
+
+\\newcolumntype{R}[2]{%
+    >{\\adjustbox{angle=#1,lap=\\width-(#2)}\\bgroup}%
+    l%
+    <{\\egroup}%
+}
+\\newcommand*\\rot{\\multicolumn{1}{R{90}{0em}}}%
+";
+
+print "\\begin{document}\n";
+print "\\begin{tabular}{lcc|rr|r|r|rr|r|rr|rrr}";
+print "&&&\\multicolumn{2}{R{20}{0em}}{{DTGBA}} & \\multicolumn{1}{R{20}{0em}}{{DBA}} &\\multicolumn{1}{R{20}{0em}}{{DRA}}& \\multicolumn{2}{R{20}{0em}}{DBA\\footnotesize m..zer} & \\multicolumn{1}{R{20}{0em}}{minDBA} & \\multicolumn{2}{R{20}{0em}}{{minDTBA}} & \\multicolumn{3}{R{20}{0em}}{minDTGBA}\\\\\n";
+print "& \$m\$ & C. & \$|Q|\$ & \$|\\CF|\$ & \$|Q|\$ & \$|Q|\$ & \$|Q|\$ & time & time & \$|Q|\$ & time & \$|Q|\$ & \$|\\CF|\$ & time \\\\\n";
+print "\\midrule\n";
+
+sub nonnull($)
+{
+    return 1 if $_[0] == 0;
+    return $_[0];
+}
+
+
+my $lasttype = '';
+my $linenum = 0;
+foreach my $tab (@w)
+{
+    sub val($)
+    {
+	my ($n) = @_;
+	my $v = $tab->[$n];
+	return 0+'inf' if !defined($v) || $v =~ /\s*-\s*/;
+	return $v;
+    }
+
+    if (dratcong($lasttype, $tab->[2]))
+    {
+#	print "\\hline\n";
+	$linenum = 0;
+    }
+    $lasttype = $tab->[2];
+    if ($linenum++ % 4 == 0)
+    {
+#	print "\\arrayrulecolor{lightgray}\\hline\\arrayrulecolor{black}";
+    }
+
+    my $f = $tab->[0];
+    $f =~ s/\&/\\land /g;
+    $f =~ s/\|/\\lor /g;
+    $f =~ s/!/\\bar /g;
+    $f =~ s/<->/\\leftrightarrow /g;
+    $f =~ s/->/\\rightarrow /g;
+    $f =~ s/[XRWMGFU]/\\$& /g;
+    print "\$$f\$\t& ";
+    print "$tab->[1] & ";
+    # If one of the automata is not deterministic highlight the "Complete" column.
+    print "{\\P}" if val(8) == 0 || val(17) == 0 || val(26) == 0 || val(35) == 0  || val(44) == 0;
+    print "$tab->[9] & ";
+
+    #TGBA
+    print "$tab->[3] & "; # states
+    #print "$tab->[5] & "; # transitions
+    print "$tab->[6] & "; # acc
+    #printf("%.2f &", $tab->[10]); # time
+
+    if ($tab->[12] =~ /\s*-\s*/)  # DBA
+    {
+	print "- & - &";
+	$tab->[12] = 0+'inf';
+    }
+    elsif ($tab->[12] =~ /\s*!\s*/)  # DBA
+    {
+	print "! & ! &";
+	$tab->[12] = 0+'inf';
+    }
+    else
+    {
+	print "$tab->[12] & "; # states
+	#print "$tab->[14] & "; # transitions
+	#printf("%.2f &", $tab->[19]);
+    }
+
+    if ($tab->[51] =~ m:\s*n/a\s*:) #  DRA
+    {
+	print "&";
+	$tab->[51] = 0+'inf';
+    }
+    else
+    {
+	# Remove sink state if not complete.
+	my $st = $tab->[51] - 1 + $tab->[9] || 1;
+	print "$st & ";
+    }
+
+    if ($tab->[48] =~ /\s*-\s*/) #  DBAminimizer
+    {
+	print "\\multicolumn{2}{c|}{(killed)}&";
+	$tab->[48] = 0+'inf';
+    }
+    elsif ($tab->[48] =~ m:\s*n/a\s*:) #  DBAminimizer
+    {
+	print " &";
+	$tab->[48] = 0+'inf';
+    }
+    else
+    {
+	# Remove sink state if not complete.
+	my $st = $tab->[48] - 1 + $tab->[9] || 1;
+	print "{\\E}" if ($st < $tab->[12]);
+	print "{\\P}" if ($st > $tab->[12]);
+	print "$st & "; # states
+	printf("%.2f &", $tab->[49]);
+    }
+
+
+    if ($tab->[21] =~ /\s*-\s*/) #  minDBA
+    {
+	print "\\multicolumn{1}{c|}{(killed)}&";
+	$tab->[21] = 0+'inf';
+    }
+    elsif ($tab->[21] =~ /\s*!\s*/) #  minDBA
+    {
+	print "\\multicolumn{1}{c|}{(INTMAX)}&";
+	$tab->[21] = 0+'inf';
+    }
+    else
+    {
+	print "{\\E}" if ($tab->[21] < $tab->[12]);
+	print "{\\P}" if ($tab->[21] > $tab->[12]);
+	#print "$tab->[21] & "; # states
+	#print "$tab->[23] & "; # transitions
+	printf("%.2f &", $tab->[28]);
+    }
+
+
+    if ($tab->[39] =~ /\s*-\s*/) # min DTBA
+    {
+	print "\\multicolumn{2}{c|}{(killed)}&";
+	$tab->[39] = 0+'inf';
+    }
+    elsif ($tab->[39] =~ /\s*!\s*/) # min DTBA
+    {
+	print "\\multicolumn{2}{c|}{(INTMAX)}&";
+	$tab->[39] = 0+'inf';
+    }
+    else
+    {
+	print "{\\E}" if ($tab->[39] < $tab->[3]);
+	print "{\\P}" if ($tab->[39] > $tab->[3] * nonnull($tab->[6])) or ($tab->[39] > $tab->[12]);
+	print "\\textbf" if ($tab->[39] < $tab->[21]);
+	print "{$tab->[39]} & "; # states
+	#print "$tab->[41] & "; # transitions
+	printf("%.2f &", $tab->[46]);
+    }
+
+    if ($tab->[30] =~ /\s*-\s*/)   # minTGBA
+    {
+	print "\\multicolumn{3}{c}{(killed)}";
+	$tab->[30] = 0+'inf';
+    }
+    elsif ($tab->[30] =~ /\s*!\s*/)   # minTGBA
+    {
+	print "\\multicolumn{3}{c}{(INTMAX)}";
+	$tab->[30] = 0+'inf';
+    }
+    else
+    {
+	print "{\\E}" if ($tab->[30] < $tab->[3]);
+	print "{\\P}" if ($tab->[30] > $tab->[3]) or ($tab->[30] > $tab->[12]) or ($tab->[30] > $tab->[21]) or ($tab->[30] > $tab->[39]);
+	print "{\\PP}" if ($tab->[21] ne 'inf' && $tab->[30] * ($tab->[33] + 1) < $tab->[21]);
+	print "\\textbf" if ($tab->[30] < $tab->[39]);
+	print "{$tab->[30]} & "; # states
+	#print "$tab->[32] & "; # transitions
+	print "\\textbf" if ($tab->[33] > $tab->[6]);
+	print "{$tab->[33]} & "; # acc
+	printf("%.2f ", $tab->[37]);
+    }
+
+    print "\\\\\n";
+}
+print "\\end{tabular}\n";
+print "\\end{document}\n";
diff --git a/bench/dtgbasat/tabl3.pl b/bench/dtgbasat/tabl3.pl
new file mode 100755
index 000000000..617feaad8
--- /dev/null
+++ b/bench/dtgbasat/tabl3.pl
@@ -0,0 +1,246 @@
+#!/usr/bin/perl -w
+
+use strict;
+
+my $num = 0;
+my @v = ();
+while (<>)
+{
+    # G(a | Fb), 1, trad, 2, 4, 8, 1, 1, 1, 1, 0.00165238, DBA, 2, 4, 8, 1, 1, 1, 1, 0.00197852, minDBA, 2, 4, 8, 1, 1, 1, 1, 0.00821457, minDTGBA, 2, 4, 8, 1, 1, 1, 1, 0.0081701
+    chomp;
+    next if /.*realizable.*/;
+    next unless /^[^,]*,[^,]*, DRA,/;
+    my $t = [split /,/];
+    next if $t->[12] >= 40;
+    $v[$num] = $t;
+#    print $v[$num]->[48], " ",  $#{$v[$num]}, "\n";
+#    if ($#{$v[$num]} != 49)
+#    {
+#	pop $v[$num];
+#	push $v[$num], '-', '-';
+#   }
+#    print $v[$num]->[48], " ",  $#{$v[$num]}, "\n";
+
+    ++$num;
+}
+
+sub dratcong($$)
+{
+    my ($a, $b) = @_;
+    return 0 if ($a =~ /.*CONG/ && $b =~ /.*CONG/);
+    return $a cmp $b;
+}
+
+sub mycmp()
+{
+    my $v = dratcong($b->[2], $a->[2]);
+    return $v if $v;
+    my $n1 = lc $a->[0];
+    $n1 =~ s/\W//g;
+    my $n2 = lc $b->[0];
+    $n2 =~ s/\W//g;
+    return $n1 cmp $n2 || $a->[0] cmp $b->[0] || $b->[2] cmp $a->[2];;
+}
+
+my @w = sort mycmp @v;
+
+print "\\documentclass{standalone}\n
+\\usepackage{amsmath}
+\\usepackage{colortbl}
+\\usepackage{booktabs}
+\\definecolor{mygray}{gray}{0.75} % 1 = white, 0 = black
+\\definecolor{lightgray}{gray}{0.7} % 1 = white, 0 = black
+\\def\\E{\\cellcolor{mygray}}
+\\def\\P{\\cellcolor{red}}
+\\def\\PP{\\cellcolor{yellow}}
+\\def\\F{\\mathsf{F}} % in future
+\\def\\G{\\mathsf{G}} % globally
+\\def\\X{\\mathsf{X}} % next
+\\newcommand{\\CF}{\\ensuremath{\\mathcal{F}}}
+\\DeclareMathOperator{\\W}{\\mathbin{\\mathsf{W}}} % weak until
+\\DeclareMathOperator{\\M}{\\mathbin{\\mathsf{M}}} % strong release
+\\DeclareMathOperator{\\U}{\\mathbin{\\mathsf{U}}} % until
+\\DeclareMathOperator{\\R}{\\mathbin{\\mathsf{R}}} % release
+\\usepackage{adjustbox}
+\\usepackage{array}
+\\def\\clap#1{\\hbox to 0pt{\\hss#1\\hss}}
+
+\\newcolumntype{R}[2]{%
+    >{\\adjustbox{angle=#1,lap=\\width-(#2)}\\bgroup}%
+    l%
+    <{\\egroup}%
+}
+\\newcommand*\\rot{\\multicolumn{1}{R{90}{0em}}}%
+";
+
+print "\\begin{document}\n";
+print "\\begin{tabular}{lcc|r|r|rr|rr|rr|rrr}";
+print "&&&\\multicolumn{1}{R{25}{0em}}{{DRA}}& \\multicolumn{1}{R{25}{0em}}{{DBA}} & \\multicolumn{2}{R{25}{0em}}{DBA\\footnotesize m..zer} &\\multicolumn{2}{R{25}{0em}}{minDBA} & \\multicolumn{2}{R{25}{0em}}{{minDTBA}} & \\multicolumn{3}{R{25}{0em}}{minDTGBA}\\\\\n";
+print "& \$m\$ & C. & \$|Q|\$ & \$|Q|\$ & \$|Q|\$ & time & \$|Q|\$ & time & \$|Q|\$ & time & \$|Q|\$ & \$|\\CF|\$ & time \\\\\n";
+print "\\midrule\n";
+
+sub nonnull($)
+{
+    return 1 if $_[0] == 0;
+    return $_[0];
+}
+
+
+my $lasttype = '';
+my $linenum = 0;
+foreach my $tab (@w)
+{
+    sub val($)
+    {
+	my ($n) = @_;
+	my $v = $tab->[$n];
+	return 0+'inf' if !defined($v) || $v =~ /\s*-\s*/;
+	return $v;
+    }
+
+    if (dratcong($lasttype, $tab->[2]))
+    {
+#	print "\\hline\n";
+	$linenum = 0;
+    }
+    $lasttype = $tab->[2];
+    if ($linenum++ % 4 == 0)
+    {
+#	print "\\arrayrulecolor{lightgray}\\hline\\arrayrulecolor{black}";
+    }
+
+    my $f = $tab->[0];
+    $f =~ s/\&/\\land /g;
+    $f =~ s/\|/\\lor /g;
+    $f =~ s/!/\\bar /g;
+    $f =~ s/<->/\\leftrightarrow /g;
+    $f =~ s/->/\\rightarrow /g;
+    $f =~ s/[XRWMGFU]/\\$& /g;
+    print "\$$f\$\t& ";
+    print "$tab->[1] & ";
+    # If one of the automata is not deterministic highlight the "Complete" column.
+    print "{\\P}" if val(8) == 0 || val(17) == 0 || val(26) == 0 || val(35) == 0  || val(44) == 0;
+    print "$tab->[9] & ";
+
+    if ($tab->[51] =~ m:\s*n/a\s*:) #  DRA
+    {
+	print "&";
+	$tab->[51] = 0+'inf';
+    }
+    else
+    {
+	# Remove sink state if not complete.
+	my $st = $tab->[51] - 1 + $tab->[9] || 1;
+	print "$st & ";
+    }
+
+    #TGBA
+    #print "$tab->[3] & "; # states
+    #print "$tab->[5] & "; # transitions
+    #print "$tab->[6] & "; # acc
+    #printf("%.2f &", $tab->[10]); # time
+
+    if ($tab->[12] =~ /\s*-\s*/)  # DBA
+    {
+	print "- & - &";
+	$tab->[12] = 0+'inf';
+    }
+    elsif ($tab->[12] =~ /\s*!\s*/)  # DBA
+    {
+	print "! & ! &";
+	$tab->[12] = 0+'inf';
+    }
+    else
+    {
+	print "$tab->[12] & "; # states
+	#print "$tab->[14] & "; # transitions
+	#printf("%.0f &", $tab->[19]);
+    }
+
+    if ($tab->[48] =~ /\s*-\s*/) #  DBAminimizer
+    {
+	print "\\multicolumn{2}{c|}{(killed)}&";
+	$tab->[48] = 0+'inf';
+    }
+    elsif ($tab->[48] =~ m:\s*n/a\s*:) #  DBAminimizer
+    {
+	print " &";
+	$tab->[48] = 0+'inf';
+    }
+    else
+    {
+	# Remove sink state if not complete.
+	my $st = $tab->[48] - 1 + $tab->[9] || 1;
+	print "{\\E}" if ($st < $tab->[12]);
+	print "{\\P}" if ($st > $tab->[12]);
+	print "$st & "; # states
+	printf("%.0f &", $tab->[49]);
+    }
+
+    if ($tab->[21] =~ /\s*-\s*/) #  minDBA
+    {
+	print "\\multicolumn{2}{c|}{(killed)}&";
+	$tab->[21] = 0+'inf';
+    }
+    elsif ($tab->[21] =~ /\s*!\s*/) #  minDBA
+    {
+	print "\\multicolumn{2}{c|}{(intmax)}&";
+	$tab->[21] = 0+'inf';
+    }
+    else
+    {
+	print "{\\E}" if ($tab->[21] < $tab->[12]);
+	print "{\\P}" if ($tab->[21] > $tab->[12]);
+	print "$tab->[21] & "; # states
+	#print "$tab->[23] & "; # transitions
+	printf("%.0f &", $tab->[28]);
+    }
+
+
+    if ($tab->[39] =~ /\s*-\s*/) # min DTBA
+    {
+	print "\\multicolumn{2}{c|}{(killed)}&";
+	$tab->[39] = 0+'inf';
+    }
+    elsif ($tab->[39] =~ /\s*!\s*/) # min DTBA
+    {
+	print "\\multicolumn{2}{c|}{(intmax)}&";
+	$tab->[39] = 0+'inf';
+    }
+    else
+    {
+	print "{\\E}" if ($tab->[39] < $tab->[3]);
+	print "{\\P}" if ($tab->[39] > $tab->[3] * nonnull($tab->[6])) or ($tab->[39] > $tab->[12]);
+	print "\\textbf" if ($tab->[39] < $tab->[21]);
+	print "{$tab->[39]} & "; # states
+	#print "$tab->[41] & "; # transitions
+	printf("%.0f &", $tab->[46]);
+    }
+
+    if ($tab->[30] =~ /\s*-\s*/)   # minTGBA
+    {
+	print "\\multicolumn{3}{c}{(killed)}";
+	$tab->[30] = 0+'inf';
+    }
+    elsif ($tab->[30] =~ /\s*!\s*/)   # minTGBA
+    {
+	print "\\multicolumn{3}{c}{(intmax)}";
+	$tab->[30] = 0+'inf';
+    }
+    else
+    {
+	print "{\\E}" if ($tab->[30] < $tab->[3]);
+	print "{\\P}" if ($tab->[30] > $tab->[3]) or ($tab->[30] > $tab->[12]) or ($tab->[30] > $tab->[21]) or ($tab->[30] > $tab->[39]);
+	print "{\\PP}" if ($tab->[21] ne 'inf' && $tab->[30] * ($tab->[33] + 1) < $tab->[21]);
+	print "\\textbf" if ($tab->[30] < $tab->[39]);
+	print "{$tab->[30]} & "; # states
+	#print "$tab->[32] & "; # transitions
+	print "\\textbf" if ($tab->[33] > $tab->[6]);
+	print "{$tab->[33]} & "; # acc
+	printf("%.0f ", $tab->[37]);
+    }
+
+    print "\\\\\n";
+}
+print "\\end{tabular}\n";
+print "\\end{document}\n";
diff --git a/bench/dtgbasat/tabl4.pl b/bench/dtgbasat/tabl4.pl
new file mode 100755
index 000000000..234c10434
--- /dev/null
+++ b/bench/dtgbasat/tabl4.pl
@@ -0,0 +1,248 @@
+#!/usr/bin/perl -w
+
+use strict;
+
+my $num = 0;
+my @v = ();
+while (<>)
+{
+    # G(a | Fb), 1, trad, 2, 4, 8, 1, 1, 1, 1, 0.00165238, DBA, 2, 4, 8, 1, 1, 1, 1, 0.00197852, minDBA, 2, 4, 8, 1, 1, 1, 1, 0.00821457, minDTGBA, 2, 4, 8, 1, 1, 1, 1, 0.0081701
+    chomp;
+    next if /.*realizable.*/;
+    next unless /CONG/;
+    $v[$num] = [split /,/];
+#    print $v[$num]->[48], " ",  $#{$v[$num]}, "\n";
+#    if ($#{$v[$num]} != 49)
+#    {
+#	pop $v[$num];
+#	push $v[$num], '-', '-';
+#   }
+#    print $v[$num]->[48], " ",  $#{$v[$num]}, "\n";
+
+    ++$num;
+}
+
+sub dratcong($$)
+{
+    my ($a, $b) = @_;
+    return 0 if ($a =~ /.*CONG/ && $b =~ /.*CONG/);
+    return $a cmp $b;
+}
+
+sub mycmp()
+{
+    my $v = dratcong($b->[2], $a->[2]);
+    return $v if $v;
+    my $n1 = lc $a->[0];
+    $n1 =~ s/\W//g;
+    my $n2 = lc $b->[0];
+    $n2 =~ s/\W//g;
+    return $n1 cmp $n2 || $a->[0] cmp $b->[0] || $b->[2] cmp $a->[2];;
+}
+
+my @w = sort mycmp @v;
+
+print "\\documentclass{standalone}\n
+\\usepackage{amsmath}
+\\usepackage{colortbl}
+\\usepackage{booktabs}
+\\usepackage{multirow}
+\\definecolor{mygray}{gray}{0.75} % 1 = white, 0 = black
+\\definecolor{lightgray}{gray}{0.7} % 1 = white, 0 = black
+\\def\\E{\\cellcolor{mygray}}
+\\def\\P{\\cellcolor{red}}
+\\def\\PP{\\cellcolor{yellow}}
+\\def\\F{\\mathsf{F}} % in future
+\\def\\G{\\mathsf{G}} % globally
+\\def\\X{\\mathsf{X}} % next
+\\newcommand{\\CF}{\\ensuremath{\\mathcal{F}}}
+\\DeclareMathOperator{\\W}{\\mathbin{\\mathsf{W}}} % weak until
+\\DeclareMathOperator{\\M}{\\mathbin{\\mathsf{M}}} % strong release
+\\DeclareMathOperator{\\U}{\\mathbin{\\mathsf{U}}} % until
+\\DeclareMathOperator{\\R}{\\mathbin{\\mathsf{R}}} % release
+\\usepackage{adjustbox}
+\\usepackage{array}
+\\def\\clap#1{\\hbox to 0pt{\\hss#1\\hss}}
+
+\\newcolumntype{R}[2]{%
+    >{\\adjustbox{angle=#1,lap=\\width-(#2)}\\bgroup}%
+    l%
+    <{\\egroup}%
+}
+\\newcommand*\\rot{\\multicolumn{1}{R{90}{0em}}}%
+";
+
+print "\\begin{document}\n";
+print "\\begin{tabular}{lcc|r|r|r|rr|rr|rr|rrr}";
+print "&&&\\multicolumn{1}{R{25}{0em}}{{DRA}}&  \\multicolumn{1}{R{25}{0em}}{{DTBA}} & \\multicolumn{1}{R{25}{0em}}{{DBA}} & \\multicolumn{2}{R{25}{0em}}{\\rlap{DBA\\footnotesize m..zer}} &\\multicolumn{2}{R{25}{0em}}{\\rlap{minDBA}} & \\multicolumn{2}{R{25}{0em}}{\\rlap{minDTBA}} & \\multicolumn{3}{R{25}{0em}}{\\rlap{minDTGBA}}\\\\\n";
+print "& \$m\$ & C. & \$|Q|\$ & \$|Q|\$ & \$|Q|\$ & \$|Q|\$ & time & \$|Q|\$ & time & \$|Q|\$ & time & \$|Q|\$ & \$|\\CF|\$ & time \\\\\n";
+print "\\midrule\n";
+
+sub nonnull($)
+{
+    return 1 if $_[0] == 0;
+    return $_[0];
+}
+
+
+my $lasttype = '';
+my $linenum = 0;
+foreach my $tab (@w)
+{
+    sub val($)
+    {
+	my ($n) = @_;
+	my $v = $tab->[$n];
+	return 0+'inf' if !defined($v) || $v =~ /\s*-\s*/;
+	return $v;
+    }
+
+    $lasttype = $tab->[2];
+    if ($linenum > 0 && $linenum % 2 == 0)
+    {
+	print "\\arrayrulecolor{lightgray}\\hline\\arrayrulecolor{black}";
+    }
+    ++$linenum;
+
+    my $f = $tab->[0];
+    next if length($f) > 60;
+    $f =~ s/\&/\\land /g;
+    $f =~ s/\|/\\lor /g;
+    $f =~ s/!/\\bar /g;
+    $f =~ s/<->/\\leftrightarrow /g;
+    $f =~ s/->/\\rightarrow /g;
+    $f =~ s/[XRWMGFU]/\\$& /g;
+
+    if ($linenum % 2 == 1)
+    {
+      print "\\multirow{2}{*}{\$$f\$}& ";
+      print "\\multirow{2}{*}{$tab->[1]}& ";
+      print "\\multirow{2}{*}{$tab->[9]}& ";
+    }
+    else
+    {
+      print "&&& ";
+    }
+
+    if ($tab->[51] =~ m:\s*n/a\s*:) #  DRA
+    {
+	print "&";
+	$tab->[51] = 0+'inf';
+    }
+    else
+    {
+	# Remove sink state if not complete.
+	my $st = $tab->[51] - 1 + $tab->[9] || 1;
+	print "$st & ";
+    }
+
+    #TGBA
+    print "$tab->[3] & "; # states
+    #print "$tab->[5] & "; # transitions
+    #print "$tab->[6] & "; # acc
+    #printf("%.2f &", $tab->[10]); # time
+
+    if ($tab->[12] =~ /\s*-\s*/)  # DBA
+    {
+	print "- & - &";
+	$tab->[12] = 0+'inf';
+    }
+    elsif ($tab->[12] =~ /\s*!\s*/)  # DBA
+    {
+	print "! & ! &";
+	$tab->[12] = 0+'inf';
+    }
+    else
+    {
+	print "$tab->[12] & "; # states
+	#print "$tab->[14] & "; # transitions
+	#printf("%.1f &", $tab->[19]);
+    }
+
+    if ($tab->[48] =~ /\s*-\s*/) #  DBAminimizer
+    {
+	print "\\multicolumn{2}{c|}{(killed)}&";
+	$tab->[48] = 0+'inf';
+    }
+    elsif ($tab->[48] =~ m:\s*n/a\s*:) #  DBAminimizer
+    {
+	print " &&";
+	$tab->[48] = 0+'inf';
+    }
+    else
+    {
+	# Remove sink state if not complete.
+	my $st = $tab->[48] - 1 + $tab->[9] || 1;
+	print "{\\E}" if ($st < $tab->[12]);
+	print "{\\P}" if ($st > $tab->[12]);
+	print "$st & "; # states
+	printf("%.1f &", $tab->[49]);
+    }
+
+    if ($tab->[21] =~ /\s*-\s*/) #  minDBA
+    {
+	print "\\multicolumn{2}{c|}{(killed)}&";
+	$tab->[21] = 0+'inf';
+    }
+    elsif ($tab->[21] =~ /\s*!\s*/) #  minDBA
+    {
+	print "\\multicolumn{2}{c|}{(intmax)}&";
+	$tab->[21] = 0+'inf';
+    }
+    else
+    {
+	print "{\\E}" if ($tab->[21] < $tab->[12]);
+	print "{\\P}" if ($tab->[21] > $tab->[12]);
+	print "$tab->[21] & "; # states
+	#print "$tab->[23] & "; # transitions
+	printf("%.1f &", $tab->[28]);
+    }
+
+
+    if ($tab->[39] =~ /\s*-\s*/) # min DTBA
+    {
+	print "\\multicolumn{2}{c|}{(killed)}&";
+	$tab->[39] = 0+'inf';
+    }
+    elsif ($tab->[39] =~ /\s*!\s*/) # min DTBA
+    {
+	print "\\multicolumn{2}{c|}{(intmax)}&";
+	$tab->[39] = 0+'inf';
+    }
+    else
+    {
+	print "{\\E}" if ($tab->[39] < $tab->[3]);
+	print "{\\P}" if ($tab->[39] > $tab->[3] * nonnull($tab->[6])) or ($tab->[39] > $tab->[12]);
+	print "\\textbf" if ($tab->[39] < $tab->[21]);
+	print "{$tab->[39]} & "; # states
+	#print "$tab->[41] & "; # transitions
+	printf("%.1f &", $tab->[46]);
+    }
+
+    if ($tab->[30] =~ /\s*-\s*/)   # minTGBA
+    {
+	print "\\multicolumn{3}{c}{(killed)}";
+	$tab->[30] = 0+'inf';
+    }
+    elsif ($tab->[30] =~ /\s*!\s*/)   # minTGBA
+    {
+	print "\\multicolumn{3}{c}{(intmax)}";
+	$tab->[30] = 0+'inf';
+    }
+    else
+    {
+	print "{\\E}" if ($tab->[30] < $tab->[3]);
+	print "{\\P}" if ($tab->[30] > $tab->[3]) or ($tab->[30] > $tab->[12]) or ($tab->[30] > $tab->[21]) or ($tab->[30] > $tab->[39]);
+	print "{\\PP}" if ($tab->[21] ne 'inf' && $tab->[30] * ($tab->[33] + 1) < $tab->[21]);
+	print "\\textbf" if ($tab->[30] < $tab->[39]);
+	print "{$tab->[30]} & "; # states
+	#print "$tab->[32] & "; # transitions
+	print "\\textbf" if ($tab->[33] > $tab->[6]);
+	print "{$tab->[33]} & "; # acc
+	printf("%.1f ", $tab->[37]);
+    }
+
+    print "\\\\\n";
+}
+print "\\end{tabular}\n";
+print "\\end{document}\n";
diff --git a/configure.ac b/configure.ac
index 59227c9e6..b0d2b3644 100644
--- a/configure.ac
+++ b/configure.ac
@@ -125,6 +125,7 @@ AC_SUBST([CROSS_COMPILING], [$cross_compiling])
 AC_CONFIG_FILES([
   Makefile
   bench/Makefile
+  bench/dtgbasat/Makefile
   bench/emptchk/Makefile
   bench/emptchk/defs
   bench/ltlcounter/Makefile