From acb454fe6cc3bafd55894831eda13ee00cad5e1f Mon Sep 17 00:00:00 2001
From: martinez <martinez>
Date: Mon, 10 May 2004 16:43:30 +0000
Subject: [PATCH] reverse mistaken commit

---
 src/tgbatest/ltl2tgba.cc | 18 +-----------------
 1 file changed, 1 insertion(+), 17 deletions(-)

diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc
index 663d3773b..d2020eec1 100644
--- a/src/tgbatest/ltl2tgba.cc
+++ b/src/tgbatest/ltl2tgba.cc
@@ -24,7 +24,6 @@
 #include <fstream>
 #include <string>
 #include "ltlvisit/destroy.hh"
-#include "ltlvisit/reducform.hh"
 #include "ltlast/allnodes.hh"
 #include "ltlparse/public.hh"
 #include "tgbaalgos/ltl2tgba_lacim.hh"
@@ -92,9 +91,7 @@ syntax(char* prog)
 	    << "  -X   do not compute an automaton, read it from a file"
 	    << std::endl
 	    << "  -y   do not merge states with same symbolic representation "
-	    << "(implies -f)" << std::endl
-	    << "  -z   to reduce formula "
-	    << std::endl;
+	    << "(implies -f)" << std::endl;
   exit(2);
 }
 
@@ -116,7 +113,6 @@ main(int argc, char** argv)
   bool magic_many = false;
   bool expect_counter_example = false;
   bool from_file = false;
-  bool reduc = false;
   bool post_branching = false;
   bool fair_loop_approx = false;
 
@@ -254,10 +250,6 @@ main(int argc, char** argv)
 	  fm_opt = true;
 	  fm_symb_merge_opt = false;
 	}
-      else if (!strcmp(argv[formula_index], "-z"))
-	{
-	  reduc = true;
-	}
       else
 	{
 	  break;
@@ -320,9 +312,6 @@ main(int argc, char** argv)
 	}
       else
 	{
-	  spot::ltl::formula* ftmp = f;
-	  if (reduc)
-	    f = spot::ltl::reduce(f);
 	  if (fm_opt)
 	    to_free = a = spot::ltl_to_tgba_fm(f, dict, fm_exprop_opt,
 					       fm_symb_merge_opt,
@@ -330,11 +319,6 @@ main(int argc, char** argv)
 					       fair_loop_approx);
 	  else
 	    to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict);
-
-	  if (reduc)
-	    spot::ltl::destroy(ftmp);
-	  spot::ltl::destroy(f);
-
 	}
 
       spot::tgba_tba_proxy* degeneralized = 0;