From 5cb40481202397afbd48ad09cd3f66eb8cbfb16d Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 16 Feb 2004 12:25:59 +0000
Subject: [PATCH] * src/tgbaalgos/ltl2tgba_fm.cc (ltl_trad_visitor::visit)
 <unop::G>: suppress the GFy optimisation introduced on 2003-11-26, it is
 generalized by the identification of states with same symbolic rewriting
 introduced on 2004-02-02.

---
 ChangeLog                    |  5 +++++
 src/tgbaalgos/ltl2tgba_fm.cc | 31 ++++++++++++++-----------------
 2 files changed, 19 insertions(+), 17 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index 077d5925f..04482c08d 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,5 +1,10 @@
 2004-02-16  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
+	* src/tgbaalgos/ltl2tgba_fm.cc (ltl_trad_visitor::visit) <unop::G>:
+	suppress the GFy optimisation introduced on 2003-11-26, it is
+	generalized by the identification of states with same symbolic
+	rewriting introduced on 2004-02-02.
+
 	* lbtt/: Merge lbtt 1.0.3.
 
 2004-02-13  Alexandre Duret-Lutz  <adl@src.lip6.fr>
diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc
index 228664130..fa84cbc65 100644
--- a/src/tgbaalgos/ltl2tgba_fm.cc
+++ b/src/tgbaalgos/ltl2tgba_fm.cc
@@ -321,25 +321,22 @@ namespace spot
 	    }
 	  case unop::G:
 	    {
+	      // The paper suggests that we optimize GFy
+	      // as
+	      //   r(GFy) = (r(y) + a(y))r(XGFy)
+	      // instead of
+	      //   r(GFy) = (r(y) + a(y)r(XFy)).r(XGFy)
+	      // but this is just a particular case
+	      // of the "merge all states with the same
+	      // symbolic rewriting" optimization we do later.
+	      // (r(Fy).r(GFy) and r(GFy) have the same symbolic
+	      // rewriting.)  Let's keep things simple here.
+
+	      // r(Gy) = r(y)r(XGy)
 	      const formula* child = node->child();
 	      int x = dict_.register_next_variable(node);
-	      // GFy is pretty frequent and easy to optimize, so we
-	      // want to detect it.
-	      const unop* Fy = dynamic_cast<const unop*>(child);
-	      if (Fy && Fy->op() == unop::F)
-		{
-		  // r(GFy) = (r(y) + a(y))r(XGFy)
-		  const formula* child = Fy->child();
-		  bdd y = recurse(child);
-		  int a = dict_.register_a_variable(child);
-		  res_ = (y | bdd_ithvar(a)) & bdd_ithvar(x);
-		}
-	      else
-		{
-		  // r(Gy) = r(y)r(XGy)
-		  bdd y = recurse(child);
-		  res_ = y & bdd_ithvar(x);
-		}
+	      bdd y = recurse(child);
+	      res_ = y & bdd_ithvar(x);
 	      return;
 	    }
 	  case unop::Not: