From 55b693e1239e239be4b8a9c89139ec70d0586d1c Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sat, 30 Jan 2010 11:20:27 +0100
Subject: [PATCH] Make Couvreur/FM the default translation.

* src/tgbatest/ltl2tgba.cc (syntax, main): Do it.
* NEWS: Mention it.
---
 ChangeLog                 | 8 ++++++++
 NEWS                      | 2 +-
 src/tgbatest/emptchk.test | 8 ++++----
 src/tgbatest/ltl2tgba.cc  | 4 ++--
 4 files changed, 15 insertions(+), 7 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index 032739f41..0238f1003 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,11 @@
+2010-01-30  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Make Couvreur/FM the default translation.
+
+	* src/tgbatest/ltl2tgba.cc (syntax, main): Do it.
+	* NEWS: Mention it.
+	* src/tgbatest/emptchk.test: Add missing -l.
+
 2010-01-30  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	Overhaul LaCIM's ELTL options.
diff --git a/NEWS b/NEWS
index 1bd1b503f..4c222bc93 100644
--- a/NEWS
+++ b/NEWS
@@ -33,7 +33,7 @@ New in spot 0.5 (2010-01-31):
       step will produce a generalized automaton in the end.
   * ltl2tgba has gained several options and the help text has been
     reorganized.  Please run src/tgbatest/ltl2tgba without arguments
-    for details.
+    for details.  Couvreur/FM is now the default translation.
   * Automata using BDD-encoded transitions relation can now be pruned
     for useless states symbolically using the delete_unaccepting_scc()
     function.  This is ltl2tgba's -R3b option.
diff --git a/src/tgbatest/emptchk.test b/src/tgbatest/emptchk.test
index 0bf550614..02ad9a00f 100755
--- a/src/tgbatest/emptchk.test
+++ b/src/tgbatest/emptchk.test
@@ -54,8 +54,8 @@ expect_ce()
   run 0 ../ltl2tgba -eTau03_opt -f "$1"
   run 0 ../ltl2tgba -eGV04 -f "$1"
   # Expect multiple accepting runs
-  test `../ltl2tgba -e'CVWY90(repeated)' "$1" | grep Prefix: | wc -l` -ge $2
-  test `../ltl2tgba -e'SE05(repeated)' "$1" | grep Prefix: | wc -l` -ge $2
+  test `../ltl2tgba -e'CVWY90(repeated)' -l "$1" | grep Prefix: | wc -l` -ge $2
+  test `../ltl2tgba -e'SE05(repeated)' -l "$1" | grep Prefix: | wc -l` -ge $2
 }
 
 expect_no()
@@ -78,9 +78,9 @@ expect_no()
   run 0 ../ltl2tgba -E'SE05(bsh=10M)' -f "$1"
   run 0 ../ltl2tgba -ETau03_opt -f "$1"
   run 0 ../ltl2tgba -EGV04 -f "$1"
-  test `../ltl2tgba -e'CVWY90(repeated)' "!($1)" |
+  test `../ltl2tgba -e'CVWY90(repeated)' -l "!($1)" |
         grep Prefix: | wc -l` -ge $2
-  test `../ltl2tgba -e'SE05(repeated)' "!($1)" |
+  test `../ltl2tgba -e'SE05(repeated)' -l "!($1)" |
         grep Prefix: | wc -l` -ge $2
 }
 
diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc
index 5c7dc9931..68ddec072 100644
--- a/src/tgbatest/ltl2tgba.cc
+++ b/src/tgbatest/ltl2tgba.cc
@@ -110,9 +110,9 @@ syntax(char* prog)
 
 	    << "Translation algorithm:" << std::endl
             << "  -f    use Couvreur's FM algorithm for LTL"
+	    << "(default)"
 	    << std::endl
             << "  -l    use Couvreur's LaCIM algorithm for LTL "
-	    << "(default)"
 	    << std::endl
 	    << "  -le   use Couvreur's LaCIM algorithm for ELTL"
 	    << std::endl
@@ -268,7 +268,7 @@ main(int argc, char** argv)
   enum { NoDegen, DegenTBA, DegenSBA } degeneralize_opt = NoDegen;
   enum { TransitionLabeled, StateLabeled } labeling_opt = TransitionLabeled;
   enum { TransFM, TransLaCIM, TransLaCIM_ELTL, TransLaCIM_ELTL_ops, TransTAA }
-    translation = TransLaCIM;
+    translation = TransFM;
   int fm_red = spot::ltl::Reduce_None;
   bool fm_exprop_opt = false;
   bool fm_symb_merge_opt = true;