From 78d37fa126e007902e1b6419e2e3af8498e43ead Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 19 Apr 2007 16:45:51 +0000
Subject: [PATCH] * 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                   |  7 +++++++
 src/ltltest/reduc.cc        | 28 +++++++++++++++++++++++++---
 src/ltlvisit/basicreduce.cc | 17 ++++++++++++-----
 src/ltlvisit/contain.cc     |  6 ++----
 4 files changed, 46 insertions(+), 12 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index aa04d637c..9b63ed856 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,5 +1,12 @@
 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.
 
diff --git a/src/ltltest/reduc.cc b/src/ltltest/reduc.cc
index 1688a0e4b..a6388f3f7 100644
--- a/src/ltltest/reduc.cc
+++ b/src/ltltest/reduc.cc
@@ -1,6 +1,6 @@
-// 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.
+// Copyright (C) 2004, 2006, 2007 Laboratoire d'Informatique de Paris
+// 6 (LIP6), département Systèmes Répartis Coopératifs (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;
   }
diff --git a/src/ltlvisit/basicreduce.cc b/src/ltlvisit/basicreduce.cc
index 8f0883d00..b5ed9bfc2 100644
--- a/src/ltlvisit/basicreduce.cc
+++ b/src/ltlvisit/basicreduce.cc
@@ -1,4 +1,4 @@
-// Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2004, 2007  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (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;
 		}
 
diff --git a/src/ltlvisit/contain.cc b/src/ltlvisit/contain.cc
index afa772fc7..dbb0ac3b8 100644
--- a/src/ltlvisit/contain.cc
+++ b/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;