From 8cbec95253eea177530f5b0a962c7c8cefbb2ab8 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 19 Jul 2006 16:07:54 +0000
Subject: [PATCH] * src/tgba/tgbaproduct.cc: Fix computation of common
 acceptance conditions.

---
 ChangeLog               | 12 ++++++++++++
 src/tgba/tgbaproduct.cc | 18 +++++++++++-------
 2 files changed, 23 insertions(+), 7 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index a7195c297..2fca4c107 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,5 +1,17 @@
 2006-07-19  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
+	* src/tgba/tgbaproduct.cc: Fix computation of common acceptance
+	conditions.
+
+	* src/tgba/bdddict.cc, src/tgba/bdddict.cc (register_clone_acc):
+	New function.
+	* src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh: Use it to
+	distinguish acceptance conditions that are identical in both
+	operands.
+
+	* src/tgbatest/explpro4.test: New file.
+	* src/tgbatest/explpro2.test, src/tgbatest/Makefile.am: Adjust.
+
 	* src/tgbaalgos/ltl2tgba_fm.cc (language_containment_checker): Move ...
 	* src/ltlvisit/contain.cc, src/ltlvisit/contain.hh
 	(spot::ltl::language_containment_checker): ... in these new files.
diff --git a/src/tgba/tgbaproduct.cc b/src/tgba/tgbaproduct.cc
index 4439eea97..5977ba605 100644
--- a/src/tgba/tgbaproduct.cc
+++ b/src/tgba/tgbaproduct.cc
@@ -182,14 +182,18 @@ namespace spot
     bdd rna = right_->neg_acceptance_conditions();
 
     right_common_acc_ = bdd_newpair();
-    bdd common = bdd_exist(lna, bdd_exist(lna, rna));
-    while (common != bddtrue)
+
+    bdd tmp = lna;
+    while (tmp != bddtrue)
       {
-	assert(bdd_high(common) == bddfalse);
-	int var = bdd_var(common);
-	int varclone = dict_->register_clone_acc(var, this);
-	bdd_setpair(right_common_acc_, var, varclone);
-	common = bdd_low(common);
+	assert(bdd_high(tmp) == bddfalse);
+	int var = bdd_var(tmp);
+	if ((bdd_nithvar(var) & rna) == rna)
+	  {
+	    int varclone = dict_->register_clone_acc(var, this);
+	    bdd_setpair(right_common_acc_, var, varclone);
+	  }
+	tmp = bdd_low(tmp);
       }
 
     bdd lac = left_->all_acceptance_conditions();