* src/ltlvisit/simpfg.cc, src/ltlvisit/simpfg.hh: New files,

extracted from ...
* src/ltlvisit/lunabbrev.cc: ... this one, which now work as documented
again.
* src/ltlvisit/reduce.cc, src/ltlvisit/syntimpl.cc: Adjust to call
simplify_f_g() in addition to unabbreviate_logic().
* src/ltlvisit/Makefile.am (ltlvisit_HEADERS, libltlvisit_la_SOURCES):
Add simpfg.cc and simpfg.hh.

ChangeLog

@@ -1,5 +1,14 @@
 2004-06-23  Alexandre Duret-Lutz  <adl@gnu.org>
 
+	* src/ltlvisit/simpfg.cc, src/ltlvisit/simpfg.hh: New files,
+	extracted from ...
+	* src/ltlvisit/lunabbrev.cc: ... this one, which now work as documented
+	again.
+	* src/ltlvisit/reduce.cc, src/ltlvisit/syntimpl.cc: Adjust to call
+	simplify_f_g() in addition to unabbreviate_logic().
+	* src/ltlvisit/Makefile.am (ltlvisit_HEADERS, libltlvisit_la_SOURCES):
+	Add simpfg.cc and simpfg.hh.
+
 	* src/ltlvisit/reducform.hh, src/ltlvisit/reducform.cc: Rename to ...
 	* src/ltlvisit/reduce.hh, src/ltlvisit/reduce.cc: ... this, to match
 	the function name.

src/ltlvisit/Makefile.am

@@ -35,6 +35,7 @@ ltlvisit_HEADERS = \
   nenoform.hh \
   postfix.hh \
   reduce.hh \
+  simpfg.hh \
   syntimpl.hh \
   tostring.hh \
   tunabbrev.hh
@@ -51,6 +52,7 @@ libltlvisit_la_SOURCES = \
   nenoform.cc \
   postfix.cc \
   reduce.cc \
+  simpfg.cc \
   syntimpl.cc \
   tostring.cc \
   tunabbrev.cc

src/ltlvisit/lunabbrev.cc

@@ -71,19 +71,11 @@ namespace spot
 						      unop::instance(unop::Not,
 								     f2)));
 	  return;
-	  /* true U f2 == F(f2) */
+          /* f1 U f2 == f1 U f2 */
-	case binop::U:
+	  /* f1 R f2 == f1 R f2 */
-	  if (f1 == constant::true_instance())
+   	case binop::U:
-	    result_ = unop::instance(unop::F, f2);
-	  else
-	    result_ = binop::instance(bo->op(), f1, f2);
-	  return;
-	  /* false R f2 == G(f2) */
 	case binop::R:
-	  if (f1 == constant::false_instance())
+	  result_ = binop::instance(bo->op(), f1, f2);
-	    result_ = unop::instance(unop::G, f2);
-	  else
-	    result_ = binop::instance(bo->op(), f1, f2);
 	  return;
 	}
       /* Unreachable code. */

src/ltlvisit/reduce.cc

@@ -26,6 +26,7 @@
 #include <cassert>
 
 #include "lunabbrev.hh"
+#include "simpfg.hh"
 #include "nenoform.hh"
 #include "ltlvisit/destroy.hh"
 
@@ -293,8 +294,11 @@ namespace spot
       formula* f2;
 
       f1 = unabbreviate_logic(f);
-      f2 = negative_normal_form(f1);
+      f2 = simplify_f_g(f1);
       destroy(f1);
+      f1 = negative_normal_form(f2);
+      destroy(f2);
+      f2 = f1;
 
       if (opt & Reduce_Basics)
 	{

src/ltlvisit/simpfg.cc

@@ -0,0 +1,86 @@
+// Copyright (C) 2004  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.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 2 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#include "ltlast/allnodes.hh"
+#include "ltlvisit/clone.hh"
+#include "simpfg.hh"
+#include <cassert>
+
+namespace spot
+{
+  namespace ltl
+  {
+
+    simplify_f_g_visitor::simplify_f_g_visitor()
+    {
+    }
+
+    simplify_f_g_visitor::~simplify_f_g_visitor()
+    {
+    }
+
+    void
+    simplify_f_g_visitor::visit(binop* bo)
+    {
+      formula* f1 = recurse(bo->first());
+      formula* f2 = recurse(bo->second());
+
+      switch (bo->op())
+	{
+	case binop::Xor:
+	case binop::Implies:
+	case binop::Equiv:
+	  result_ = binop::instance(bo->op(), f1, f2);
+	  return;
+	  /* true U f2 == F(f2) */
+	case binop::U:
+	  if (f1 == constant::true_instance())
+	    result_ = unop::instance(unop::F, f2);
+	  else
+	    result_ = binop::instance(binop::U, f1, f2);
+	  return;
+	  /* false R f2 == G(f2) */
+	case binop::R:
+	  if (f1 == constant::false_instance())
+	    result_ = unop::instance(unop::G, f2);
+	  else
+	    result_ = binop::instance(binop::R, f1, f2);
+	  return;
+	}
+      /* Unreachable code. */
+      assert(0);
+    }
+
+    formula*
+    simplify_f_g_visitor::recurse(formula* f)
+    {
+      return simplify_f_g(f);
+    }
+
+    formula*
+    simplify_f_g(const formula* f)
+    {
+      simplify_f_g_visitor v;
+      const_cast<formula*>(f)->accept(v);
+      return v.result();
+    }
+  }
+}

src/ltlvisit/simpfg.hh

@@ -0,0 +1,52 @@
+// Copyright (C) 2004  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.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 2 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#ifndef SPOT_LTLVISIT_SIMPFG_HH
+# define SPOT_LTLVISIT_SIMPFG_HH
+
+#include "clone.hh"
+
+namespace spot
+{
+  namespace ltl
+  {
+    /// \brief Replace <code>true U f</code> and <code>false R g</code> by
+    /// <code>F f</code> and <code>G g</code>.
+    class simplify_f_g_visitor : public clone_visitor
+    {
+      typedef clone_visitor super;
+    public:
+      simplify_f_g_visitor();
+      virtual ~simplify_f_g_visitor();
+
+      using super::visit;
+      void visit(binop* bo);
+
+      virtual formula* recurse(formula* f);
+    };
+
+    /// \brief Replace <code>true U f</code> and <code>false R g</code> by
+    /// <code>F f</code> and <code>G g</code>.
+    formula* simplify_f_g(const formula* f);
+  }
+}
+
+#endif // SPOT_LTLVISIT_LUNABBREV_HH

src/ltlvisit/syntimpl.cc

@@ -24,6 +24,7 @@
 #include <cassert>
 
 #include "lunabbrev.hh"
+#include "simpfg.hh"
 #include "nenoform.hh"
 #include "ltlvisit/destroy.hh"
 
@@ -515,33 +516,32 @@ namespace spot
     bool
     syntactic_implication_neg(const formula* f1, const formula* f2, bool right)
     {
-      const formula* ftmp1;
+      formula* l = clone(f1);
-      const formula* ftmp2;
+      formula* r = clone(f2);
-      const formula* ftmp3 = unop::instance(unop::Not,
-					    right ? clone(f2) : clone(f1));
-      const formula* ftmp4 = negative_normal_form(right ? f1 : f2);
-      const formula* ftmp5;
-      const formula* ftmp6;
-      bool result;
-
-      ftmp2 = unabbreviate_logic(ftmp3);
-      ftmp1 = negative_normal_form(ftmp2);
-
-      ftmp5 = unabbreviate_logic(ftmp4);
-      ftmp6 = negative_normal_form(ftmp5);
-
       if (right)
-	result = syntactic_implication(ftmp6, ftmp1);
+	r = unop::instance(unop::Not, r);
       else
-	result = syntactic_implication(ftmp1, ftmp6);
+	l = unop::instance(unop::Not, l);
 
-      destroy(ftmp1);
+      formula* tmp = unabbreviate_logic(l);
-      destroy(ftmp2);
+      destroy(l);
-      destroy(ftmp3);
+      l = simplify_f_g(tmp);
-      destroy(ftmp4);
+      destroy(tmp);
-      destroy(ftmp5);
+      tmp = negative_normal_form(l);
-      destroy(ftmp6);
+      destroy(l);
+      l = tmp;
 
+      tmp = unabbreviate_logic(r);
+      destroy(r);
+      r = simplify_f_g(tmp);
+      destroy(tmp);
+      tmp = negative_normal_form(r);
+      destroy(r);
+      r = tmp;
+
+      bool result = syntactic_implication(l, r);
+      destroy(l);
+      destroy(r);
       return result;
     }
   }