* src/evtgbaparse/public.hh: Work around Bison 2.3 unique guards.

* src/ltlvisit/reduce.hh, src/ltlvisit/reduce.hh:
Add Reduce_Containment_Checks and Reduce_Containment_Checks_Stronger
flags, and call reduce_tau03.
* src/ltlvisit/contain.hh (reduce_tau03): Make "stronger" the
default.
* src/ltlvisit/contain.cc: Style.
* src/ltltest/reduc.cc: Simplify using the reduce() interface
instead of reduce_tau03.
* src/tgbatest/ltl2tgba.cc: Likewise.  Add -fr5, -fr6, and -fr7
options.
* src/tgbatest/spotlbtt.test: Remove cases using "-c", since its
current implementation is not always correct (and apparently
reduces less than -fr7).

ChangeLog

@@ -1,3 +1,20 @@
+2006-08-16  Alexandre Duret-Lutz  <adl@gnu.org>
+
+	* src/evtgbaparse/public.hh: Work around Bison 2.3 unique guards.
+	* src/ltlvisit/reduce.hh, src/ltlvisit/reduce.hh:
+	Add Reduce_Containment_Checks and Reduce_Containment_Checks_Stronger
+	flags, and call reduce_tau03.
+	* src/ltlvisit/contain.hh (reduce_tau03): Make "stronger" the
+	default.
+	* src/ltlvisit/contain.cc: Style.
+	* src/ltltest/reduc.cc: Simplify using the reduce() interface
+	instead of reduce_tau03.
+	* src/tgbatest/ltl2tgba.cc: Likewise.  Add -fr5, -fr6, and -fr7
+	options.
+	* src/tgbatest/spotlbtt.test: Remove cases using "-c", since its
+	current implementation is not always correct (and apparently
+	reduces less than -fr7).
+
 2006-08-01  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
 	* src/evtgbatest/evtgbaparse.yy, src/evtgbaparse/evtgbascan.ll,

src/evtgbaparse/public.hh

@@ -1,6 +1,6 @@
-// Copyright (C) 2003, 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
-// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
-// et Marie Curie.
+// Université Pierre et Marie Curie.
 //
 // This file is part of Spot, a model checking library.
 //
@@ -23,6 +23,9 @@
 # define SPOT_EVTGBAPARSE_PUBLIC_HH
 
 # include "evtgba/explicit.hh"
+// Unfortunately Bison 2.3 uses the same guards in all parsers :(
+# undef BISON_LOCATION_HH
+# undef BISON_POSITION_HH
 # include "location.hh"
 # include <string>
 # include <list>

src/ltltest/reduc.cc

@@ -43,9 +43,6 @@ syntax(char* prog)
 int
 main(int argc, char** argv)
 {
-  bool tau03 = false;
-  bool stronger = false;
-
   if (argc < 3)
     syntax(argv[0]);
 
@@ -61,11 +58,10 @@ main(int argc, char** argv)
     case 2:
       o = spot::ltl::Reduce_Eventuality_And_Universality;
       break;
-    case 9:
-      tau03 = stronger = true;
-      /* fall through */
     case 3:
-      o = spot::ltl::Reduce_All;
+      o = spot::ltl::Reduce_Basics
+	| spot::ltl::Reduce_Syntactic_Implications
+	| spot::ltl::Reduce_Eventuality_And_Universality;
       break;
     case 4:
       o = spot::ltl::Reduce_Basics | spot::ltl::Reduce_Syntactic_Implications;
@@ -78,11 +74,14 @@ main(int argc, char** argv)
       o = (spot::ltl::Reduce_Syntactic_Implications
 	   | spot::ltl::Reduce_Eventuality_And_Universality);
       break;
-    case 8:
-      stronger = true;
-      /* fall through */
     case 7:
-      tau03 = true;
+      o = spot::ltl::Reduce_Containment_Checks;
+      break;
+    case 8:
+      o = spot::ltl::Reduce_Containment_Checks_Stronger;
+      break;
+    case 9:
+      o = spot::ltl::Reduce_All;
       break;
     default:
       return 2;
@@ -127,13 +126,6 @@ main(int argc, char** argv)
   spot::ltl::destroy(ftmp1);
   spot::ltl::destroy(ftmp2);
 
-  if (tau03)
-    {
-      ftmp1 = f1;
-      f1 = spot::ltl::reduce_tau03(f1, stronger);
-      spot::ltl::destroy(ftmp1);
-    }
-
   int length_f1_after = spot::ltl::length(f1);
   std::string f1s_after = spot::ltl::to_string(f1);
 

src/ltlvisit/contain.cc

@@ -124,7 +124,7 @@ namespace spot
     bool
     language_containment_checker::equal(const formula* l, const formula* g)
     {
-      return contained(l,g) && contained(g,l);
+      return contained(l, g) && contained(g, l);
     }
 
     language_containment_checker::record_*
@@ -143,7 +143,8 @@ namespace spot
     }
 
 
-    namespace {
+    namespace
+    {
       struct reduce_tau03_visitor : public clone_visitor {
 	bool stronger;
 	language_containment_checker* lcc;

src/ltlvisit/contain.hh

@@ -101,7 +101,7 @@ namespace spot
     /// If \a stronger is set, additional rules are used to further
     /// reduce some U, R, and X usages.
     /// \endverbatim
-    formula* reduce_tau03(const formula* f, bool stronger = false);
+    formula* reduce_tau03(const formula* f, bool stronger = true);
   }
 }
 

src/ltlvisit/reduce.cc

@@ -1,4 +1,4 @@
-// Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2004, 2006  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
@@ -29,6 +29,7 @@
 #include "simpfg.hh"
 #include "nenoform.hh"
 #include "ltlvisit/destroy.hh"
+#include "contain.hh"
 
 namespace spot
 {
@@ -331,6 +332,17 @@ namespace spot
 	      f2 = f1;
 	    }
 	}
+
+
+      if (opt & (Reduce_Containment_Checks
+		 | Reduce_Containment_Checks_Stronger))
+	{
+	  formula* f1 = reduce_tau03(f2,
+				     opt & Reduce_Containment_Checks_Stronger);
+	  destroy(f2);
+	  f2 = f1;
+	}
+
       return f2;
     }
   }

src/ltlvisit/reduce.hh

@@ -1,4 +1,4 @@
-// Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2004, 2006  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
@@ -44,6 +44,10 @@ namespace spot
 	Reduce_Syntactic_Implications = 2,
 	/// Etessami & Holzmann eventuality and universality reductions.
 	Reduce_Eventuality_And_Universality = 4,
+	/// Tauriainen containment checks.
+	Reduce_Containment_Checks = 8,
+	/// Tauriainen containment checks (stronger version).
+	Reduce_Containment_Checks_Stronger = 16,
 	/// All reductions.
 	Reduce_All = -1U
       };

src/tgbaparse/public.hh

@@ -23,7 +23,7 @@
 # define SPOT_TGBAPARSE_PUBLIC_HH
 
 # include "tgba/tgbaexplicit.hh"
-  /* Unfortunately Bison 2.3 uses the same guards in all parsers :( */
+// Unfortunately Bison 2.3 uses the same guards in all parsers :(
 # undef BISON_LOCATION_HH
 # undef BISON_POSITION_HH
 # include "tgbaparse/location.hh"

src/tgbatest/ltl2tgba.cc

@@ -25,7 +25,6 @@
 #include <fstream>
 #include <string>
 #include "ltlvisit/destroy.hh"
-#include "ltlvisit/reduce.hh"
 #include "ltlvisit/contain.hh"
 #include "ltlvisit/tostring.hh"
 #include "ltlvisit/apcollect.hh"
@@ -81,6 +80,9 @@ syntax(char* prog)
 	    << "  -fr2  use -r2 (see below) at each step of FM" << std::endl
 	    << "  -fr3  use -r3 (see below) at each step of FM" << std::endl
 	    << "  -fr4  use -r4 (see below) at each step of FM" << std::endl
+	    << "  -fr5  use -r5 (see below) at each step of FM" << std::endl
+	    << "  -fr6  use -r6 (see below) at each step of FM" << std::endl
+	    << "  -fr7  use -r7 (see below) at each step of FM" << std::endl
             << "  -F    read the formula from the file" << std::endl
 	    << "  -g    graph the accepting run on the automaton (requires -e)"
 	    << std::endl
@@ -167,8 +169,6 @@ main(int argc, char** argv)
   bool from_file = false;
   int reduc_aut = spot::Reduce_None;
   int redopt = spot::ltl::Reduce_None;
-  bool redtau = false;
-  bool stronger = false;
   bool display_reduce_form = false;
   bool display_rel_sim = false;
   bool display_parity_game = false;
@@ -281,6 +281,23 @@ main(int argc, char** argv)
 	  fm_red |= spot::ltl::Reduce_Syntactic_Implications;
 	}
       else if (!strcmp(argv[formula_index], "-fr4"))
+	{
+	  fm_opt = true;
+ 	  fm_red |= spot::ltl::Reduce_Basics
+	    | spot::ltl::Reduce_Eventuality_And_Universality
+	    | spot::ltl::Reduce_Syntactic_Implications;
+	}
+      else if (!strcmp(argv[formula_index], "-fr5"))
+	{
+	  fm_opt = true;
+	  fm_red |= spot::ltl::Reduce_Containment_Checks;
+	}
+      else if (!strcmp(argv[formula_index], "-fr6"))
+	{
+	  fm_opt = true;
+	  fm_red |= spot::ltl::Reduce_Containment_Checks_Stronger;
+	}
+      else if (!strcmp(argv[formula_index], "-fr7"))
 	{
 	  fm_opt = true;
 	  fm_red |= spot::ltl::Reduce_All;
@@ -347,20 +364,21 @@ main(int argc, char** argv)
 	}
       else if (!strcmp(argv[formula_index], "-r4"))
 	{
-	  redopt |= spot::ltl::Reduce_All;
+ 	  redopt |= spot::ltl::Reduce_Basics
+	    | spot::ltl::Reduce_Eventuality_And_Universality
+	    | spot::ltl::Reduce_Syntactic_Implications;
 	}
       else if (!strcmp(argv[formula_index], "-r5"))
 	{
-	  redtau = true;
+	  redopt |= spot::ltl::Reduce_Containment_Checks;
 	}
       else if (!strcmp(argv[formula_index], "-r6"))
 	{
-	  redtau = stronger = true;
+	  redopt |= spot::ltl::Reduce_Containment_Checks_Stronger;
 	}
       else if (!strcmp(argv[formula_index], "-r7"))
 	{
 	  redopt |= spot::ltl::Reduce_All;
-	  redtau = stronger = true;
 	}
       else if (!strcmp(argv[formula_index], "-R"))
 	{
@@ -517,14 +535,6 @@ main(int argc, char** argv)
 	      spot::ltl::formula* t = spot::ltl::reduce(f, redopt);
 	      spot::ltl::destroy(f);
 	      f = t;
-	      if (display_reduce_form && !redtau)
-		std::cout << spot::ltl::to_string(f) << std::endl;
-	    }
-	  if (redtau)
-	    {
-	      spot::ltl::formula* t = spot::ltl::reduce_tau03(f, stronger);
-	      spot::ltl::destroy(f);
-	      f = t;
 	      if (display_reduce_form)
 		std::cout << spot::ltl::to_string(f) << std::endl;
 	    }

src/tgbatest/spotlbtt.test

@@ -1,7 +1,7 @@
 #!/bin/sh
-# Copyright (C) 2003, 2004, 2005, 2006  Laboratoire d'Informatique de Paris 6 (LIP6),
+# Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
-# département Systèmes Répartis Coopératifs (SRC), Université Pierre
+# Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
-# et Marie Curie.
+# Université Pierre et Marie Curie.
 #
 # This file is part of Spot, a model checking library.
 #
@@ -68,14 +68,6 @@ Algorithm
    Enabled = yes
 }
 
-Algorithm
-{
-   Name = "Spot (Couvreur -- FM) containments"
-   Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spot './ltl2tgba -F -f -c -t'"
-   Enabled = yes
-}
-
 Algorithm
 {
    Name = "Spot (Couvreur -- FM), basic reduction of formula"
@@ -116,15 +108,6 @@ Algorithm
    Enabled = yes
 }
 
-Algorithm
-{
-   Name = "Spot (Couvreur -- FM) containments + reduction of formula (pre reduction)"
-   Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spot './ltl2tgba -r7 -F -f -c -t'"
-   Enabled = yes
-}
-
-
 Algorithm
 {
    Name = "Spot (Couvreur -- FM), reduction of formula in FM"
@@ -133,6 +116,16 @@ Algorithm
    Enabled = yes
 }
 
+Algorithm
+{
+   Name = "Spot (Couvreur -- FM) reduction7 of formula in FM"
+   Path = "${LBTT_TRANSLATE}"
+   Parameters = "--spot './ltl2tgba -fr7 -F -f -t'"
+   Enabled = yes
+}
+
+
+
 Algorithm
 {
    Name = "Spot (Couvreur -- FM), post reduction with direct simulation"