From b6b6582b059ff75ed6e82b1052dcb16d00bcac8a Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sat, 2 Mar 2013 15:15:47 +0100
Subject: [PATCH] bin: Fix handling of LTL simplification options.

Enable LTL simplifications by default for ltl2tgba & ltl2tgta, and make
sure the ltl_simplifier_options are all false initially.  Before this
patch --low/-r1 had the same effect as --medium/-r2 with respect to LTL
simplification.

* src/bin/ltl2tgba.cc, src/bin/ltl2tgta.cc (simplification_level): Set
to 3 by default.
* src/bin/common_r.cc: Disable all ltl_simplifier options initially.
---
 src/bin/common_r.cc | 6 +++---
 src/bin/ltl2tgba.cc | 2 ++
 src/bin/ltl2tgta.cc | 6 ++++--
 3 files changed, 9 insertions(+), 5 deletions(-)

diff --git a/src/bin/common_r.cc b/src/bin/common_r.cc
index a204f2d74..fea33d061 100644
--- a/src/bin/common_r.cc
+++ b/src/bin/common_r.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012 Laboratoire de Recherche et Développement de
-// l'Epita (LRDE).
+// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
+// de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -42,7 +42,7 @@ parse_r(const char* arg)
 spot::ltl::ltl_simplifier_options
 simplifier_options()
 {
-  spot::ltl::ltl_simplifier_options options;
+  spot::ltl::ltl_simplifier_options options(false, false, false);
   switch (simplification_level)
     {
     case 3:
diff --git a/src/bin/ltl2tgba.cc b/src/bin/ltl2tgba.cc
index 0507c96b6..266548e77 100644
--- a/src/bin/ltl2tgba.cc
+++ b/src/bin/ltl2tgba.cc
@@ -247,6 +247,8 @@ main(int argc, char** argv)
   const argp ap = { options, parse_opt, "[FORMULA...]",
 		    argp_program_doc, children, 0, 0 };
 
+  simplification_level = 3;
+
   if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, 0, 0))
     exit(err);
 
diff --git a/src/bin/ltl2tgta.cc b/src/bin/ltl2tgta.cc
index 5a7bffd4a..35f4636f0 100644
--- a/src/bin/ltl2tgta.cc
+++ b/src/bin/ltl2tgta.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012 Laboratoire de Recherche et Développement de
-// l'Epita (LRDE).
+// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
+// de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -244,6 +244,8 @@ main(int argc, char** argv)
   const argp ap = { options, parse_opt, "[FORMULA...]",
 		    argp_program_doc, children, 0, 0 };
 
+  simplification_level = 3;
+
   if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, 0, 0))
     exit(err);