Fix computation of product acceptance conditions, when the

two operands share some acceptance conditions.
* src/tgba/tgbaproduct.hh (tgba_product::left_acc_complement_,
tgba_product::right_acc_complement_): New attribute.
* src/tgba/tgbaproduct.cc (tgba_product::tgba_product): Set them.
(tgba_product::succ_iter): Use them.
* src/tgba/explpro2.test: New file.
* src/tgba/Makefile.am (TESTS): Add it.

ChangeLog

@@ -1,3 +1,14 @@
+2003-08-22  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
+
+	Fix computation of product acceptance conditions, when the
+	two operands share some acceptance conditions.
+	* src/tgba/tgbaproduct.hh (tgba_product::left_acc_complement_,
+	tgba_product::right_acc_complement_): New attribute.
+	* src/tgba/tgbaproduct.cc (tgba_product::tgba_product): Set them.
+	(tgba_product::succ_iter): Use them.
+	* src/tgba/explpro2.test: New file.
+	* src/tgba/Makefile.am (TESTS): Add it.
+
 2003-08-20  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
 
 	* tgba/tgbaproduct.cc, tgba/tgbaproduct.hh:

src/tgba/tgbaproduct.cc

@@ -148,12 +148,17 @@ namespace spot
   {
     assert(dict_ == right->get_dict());
 
+    bdd lna = left_->neg_accepting_conditions();
+    bdd rna = right_->neg_accepting_conditions();
+    left_acc_complement_ = bdd_exist(lna, bdd_support(rna));
+    right_acc_complement_ = bdd_exist(rna, bdd_support(lna));
+
     all_accepting_conditions_ = ((left_->all_accepting_conditions()
-				  & right_->neg_accepting_conditions())
+				  & left_acc_complement_)
 				 | (right_->all_accepting_conditions()
-				    & left_->neg_accepting_conditions()));
+				    & right_acc_complement_));
-    neg_accepting_conditions_ = (left_->neg_accepting_conditions()
+    neg_accepting_conditions_ = lna & rna;
-				 & right_->neg_accepting_conditions());
+
     dict_->register_all_variables_of(&left_, this);
     dict_->register_all_variables_of(&right_, this);
   }
@@ -192,8 +197,8 @@ namespace spot
     tgba_succ_iterator* ri = right_->succ_iter(s->right(),
 					       global_state, global_automaton);
     return new tgba_succ_iterator_product(li, ri,
-					  left_->neg_accepting_conditions(),
+					  left_acc_complement_,
-					  right_->neg_accepting_conditions());
+					  right_acc_complement_);
   }
 
   bdd

src/tgba/tgbaproduct.hh

@@ -122,6 +122,8 @@ namespace spot
     bdd_dict* dict_;
     const tgba* left_;
     const tgba* right_;
+    bdd left_acc_complement_;
+    bdd right_acc_complement_;
     bdd all_accepting_conditions_;
     bdd neg_accepting_conditions_;
     // Disallow copy.

src/tgbatest/Makefile.am

@@ -38,10 +38,11 @@ TESTS = \
   ltlprod.test \
   bddprod.test \
   explprod.test \
+  explpro2.test \
   tripprod.test \
   mixprod.test \
-  spotlbtt.test \
+  ltlmagic.test \
-  ltlmagic.test
+  spotlbtt.test
 
 EXTRA_DIST = $(TESTS)
 

src/tgbatest/explpro2.test

@@ -0,0 +1,34 @@
+#!/bin/sh
+
+. ./defs
+
+set -e
+
+cat >input1 <<EOF
+acc = p1 p2;
+s1, s2, !a, p1;
+s1, s3, !b, p2;
+EOF
+
+cat >input2 <<EOF
+acc = p2 p3;
+s1, s2, b, p2;
+s1, s3, a, p3;
+EOF
+
+cat >expected <<EOF
+acc = "p1" "p2" "p3";
+"s1 * s1", "s2 * s2", ! a b, "p1" "p2";
+"s1 * s1", "s3 * s3", a ! b, "p2" "p3";
+EOF
+
+./explprod input1 input2 > stdout
+
+# Sort out some possible inversions in the output.
+# (The order is not guaranteed by SPOT.)
+sed 's/c a/a c/g;s/b a/a b/g;s/"p3" "p2"/"p2" "p3"/g;s/"p2" "p1"/"p1" "p2"/g' stdout > tmp_ &&
+  mv tmp_ stdout
+
+cat stdout
+diff stdout expected
+rm input1 input2 stdout expected