* src/ltltest/reduc.cc (main): More cases to test.

* src/ltlvisit/basicreduce.cc (basic_reduce_visitor::visit):
Simplify the formula again after FX->XF and GX->XG permutations.
This is so that formulae like GFXXa become GFa and not just GFXa.
* src/ltlvisit/contain.cc (reduce_tau03_visitor): Fix a typo
in the rules for i|j or i&j, resulting in missing simplifications.

ChangeLog

 2007-04-19  Alexandre Duret-Lutz  <adl@gnu.org>
 
+	* src/ltltest/reduc.cc (main): More cases to test.
+	* src/ltlvisit/basicreduce.cc (basic_reduce_visitor::visit):
+	Simplify the formula again after FX->XF and GX->XG permutations.
+	This is so that formulae like GFXXa become GFa and not just GFXa.
+	* src/ltlvisit/contain.cc (reduce_tau03_visitor): Fix a typo
+	in the rules for i|j or i&j, resulting in missing simplifications.
+
 	* src/ltlvisit/contain.cc (reduce_tau03_visitor): Simplify the
 	rules for "a U b" and "a R b", an implication check is enough.
 

src/ltltest/reduc.cc

-// Copyright (C) 2004, 2006  Laboratoire d'Informatique de Paris 6 (LIP6),
-// dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre
-// et Marie Curie.
+// Copyright (C) 2004, 2006, 2007 Laboratoire d'Informatique de Paris
+// 6 (LIP6), dpartement Systmes Rpartis Coopratifs (SRC),
+// Universit Pierre et Marie Curie.
 //
 // This file is part of Spot, a model checking library.
 //
@@ -83,6 +83,28 @@ main(int argc, char** argv)
     case 9:
       o = spot::ltl::Reduce_All;
       break;
+    case 10:
+      o = (spot::ltl::Reduce_Basics
+	   | spot::ltl::Reduce_Containment_Checks_Stronger);
+      break;
+    case 11:
+      o = (spot::ltl::Reduce_Syntactic_Implications
+	   | spot::ltl::Reduce_Containment_Checks_Stronger);
+      break;
+    case 12:
+      o = (spot::ltl::Reduce_Basics
+	   | spot::ltl::Reduce_Syntactic_Implications
+	   | spot::ltl::Reduce_Containment_Checks_Stronger);
+      break;
+    case 13:
+      o = (spot::ltl::Reduce_Eventuality_And_Universality
+	   | spot::ltl::Reduce_Containment_Checks_Stronger);
+      break;
+    case 14:
+      o = (spot::ltl::Reduce_Basics
+	   | spot::ltl::Reduce_Eventuality_And_Universality
+	   | spot::ltl::Reduce_Containment_Checks_Stronger);
+      break;
     default:
       return 2;
   }

src/ltlvisit/basicreduce.cc

-// Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2004, 2007  Laboratoire d'Informatique de Paris 6 (LIP6),
 // dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre
 // et Marie Curie.
 //
@@ -159,13 +159,16 @@ namespace spot
 	      u = dynamic_cast<unop*>(result_);
 	      if (u && u->op() == unop::X)
 		{
-		  result_ =
+		  formula* res =
 		    unop::instance(unop::X,
 				   unop::instance(unop::F,
 						  basic_reduce(u->child())));
 		  destroy(u);
-		return;
-	      }
+		  // FXX(a) = XXF(a) ...
+		  result_ = basic_reduce(res);
+		  destroy(res);
+		  return;
+		}
 
 	      // F(f1 & GF(f2)) = F(f1) & GF(F2)
 	      mo = dynamic_cast<multop*>(result_);
@@ -198,11 +201,15 @@ namespace spot
 	      u = dynamic_cast<unop*>(result_);
 	      if (u && u->op() == unop::X)
 		{
-		  result_ =
+		  formula* res =
 		    unop::instance(unop::X,
 				   unop::instance(unop::G,
 						  basic_reduce(u->child())));
 		  destroy(u);
+		  // GXX(a) = XXG(a) ...
+		  // GXF(a) = XGF(a) = GF(a) ...
+		  result_ = basic_reduce(res);
+		  destroy(res);
 		  return;
 		}
 

src/ltlvisit/contain.cc

@@ -30,8 +30,6 @@
 #include "tgba/tgbaproduct.hh"
 #include "tgbaalgos/gtec/gtec.hh"
 #include "tgbaalgos/save.hh"
-#include "tostring.hh"
-#include <iostream>
 namespace spot
 {
   namespace ltl
@@ -269,7 +267,7 @@ namespace spot
 			  break;
 			}
 		      // if j => i, then i|j = i
-		      else if (lcc->contained((*res)[i], (*res)[j]))
+		      else if (lcc->contained((*res)[j], (*res)[i]))
 			{
 			  destroy((*res)[j]);
 			  (*res)[j] = 0;
@@ -301,7 +299,7 @@ namespace spot
 			  changed = true;
 			}
 		      // if j => i, then i&j = j
-		      else if (lcc->contained((*res)[i], (*res)[j]))
+		      else if (lcc->contained((*res)[j], (*res)[i]))
 			{
 			  destroy((*res)[i]);
 			  (*res)[i] = 0;