From 6e6b6b1e01fa74e3c7dbf320e11ee7e575ba6ca1 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sun, 20 Feb 2011 17:15:37 +0100
Subject: [PATCH] Disable LTL reductions on SERE formulae.

* src/ltlvisit/contain.cc (recurse, reduce_tau03): Do not
run on non-PSL formulae.
* src/ltlvisit/reduce.cc (reduce_visitor::visit): Skip
multop::Fusion operators, and do not run syntactic_implication_neg
on SERE formulae.
* src/ltlvisit/syntimpl.cc (inf_right_recurse_visitor::visit):
Skip [*0].
---
 src/ltlvisit/contain.cc  |  9 +++++++-
 src/ltlvisit/reduce.cc   | 46 +++++++++++++++++++++++-----------------
 src/ltlvisit/syntimpl.cc |  4 ++--
 3 files changed, 36 insertions(+), 23 deletions(-)

diff --git a/src/ltlvisit/contain.cc b/src/ltlvisit/contain.cc
index d8d87c82f..44b0e0877 100644
--- a/src/ltlvisit/contain.cc
+++ b/src/ltlvisit/contain.cc
@@ -1,4 +1,4 @@
-// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
+// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 // Copyright (C) 2006, 2007 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -30,6 +30,7 @@
 #include "tgba/tgbaproduct.hh"
 #include "tgbaalgos/gtec/gtec.hh"
 #include "tgbaalgos/save.hh"
+
 namespace spot
 {
   namespace ltl
@@ -381,6 +382,9 @@ namespace spot
 	formula*
 	recurse(formula* f)
 	{
+	  if (!f->is_psl_formula())
+	    return f->clone();
+
 	  reduce_tau03_visitor v(stronger, lcc);
 	  const_cast<formula*>(f)->accept(v);
 	  return v.result();
@@ -391,6 +395,9 @@ namespace spot
     formula*
     reduce_tau03(const formula* f, bool stronger)
     {
+      if (!f->is_psl_formula())
+	return f->clone();
+
       bdd_dict b;
       reduce_tau03_visitor v(stronger,
 			     new language_containment_checker(&b,
diff --git a/src/ltlvisit/reduce.cc b/src/ltlvisit/reduce.cc
index d322a8009..fd1c7553e 100644
--- a/src/ltlvisit/reduce.cc
+++ b/src/ltlvisit/reduce.cc
@@ -325,7 +325,8 @@ namespace spot
 	    res->push_back(recurse(mo->nth(i)));
 
 	  if ((opt_ & Reduce_Syntactic_Implications)
-	      && (mo->op() != multop::Concat))
+	      && (mo->op() != multop::Concat)
+	      && (mo->op() != multop::Fusion))
 	    {
 
 	      bool removed = true;
@@ -369,25 +370,30 @@ namespace spot
 		    }
 		}
 
-	      /* f1 < !f2 => f1 & f2 = false
-		 !f1 < f2 => f1 | f2 = true */
-	      for (f1 = res->begin(); f1 != res->end(); f1++)
-		for (f2 = res->begin(); f2 != res->end(); f2++)
-		  if (f1 != f2 &&
-		      c_->syntactic_implication_neg(*f1, *f2,
-						    mo->op() !=  multop::Or))
-		    {
-		      for (multop::vec::iterator j = res->begin();
-			   j != res->end(); j++)
-			(*j)->destroy();
-		      res->clear();
-		      delete res;
-		      if (mo->op() == multop::Or)
-			result_ = constant::true_instance();
-		      else
-			result_ = constant::false_instance();
-		      return;
-		    }
+	      // We cannot run syntactic_implication_neg on SERE
+	      // formulae, unless they are just Boolean formulae.
+	      if (mo->is_boolean() || !mo->is_sere_formula())
+		{
+		  bool is_and = mo->op() != multop::Or;
+		  /* f1 < !f2 => f1 & f2 = false
+		     !f1 < f2 => f1 | f2 = true */
+		  for (f1 = res->begin(); f1 != res->end(); f1++)
+		    for (f2 = res->begin(); f2 != res->end(); f2++)
+		      if (f1 != f2 &&
+			  c_->syntactic_implication_neg(*f1, *f2, is_and))
+			{
+			  for (multop::vec::iterator j = res->begin();
+			       j != res->end(); j++)
+			    (*j)->destroy();
+			  res->clear();
+			  delete res;
+			  if (is_and)
+			    result_ = constant::false_instance();
+			  else
+			    result_ = constant::true_instance();
+			  return;
+			}
+		}
 
 	    }
 
diff --git a/src/ltlvisit/syntimpl.cc b/src/ltlvisit/syntimpl.cc
index 0f5b8fe9b..e0c96efb2 100644
--- a/src/ltlvisit/syntimpl.cc
+++ b/src/ltlvisit/syntimpl.cc
@@ -1,4 +1,4 @@
-// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
+// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -76,7 +76,7 @@ namespace spot
 	      result_ = false;
 	      return;
 	    case constant::EmptyWord:
-	      result_ = true;
+	      result_ = false;
 	    }
 	}