diff --git a/ChangeLog b/ChangeLog index 56aed88c3..5541d258a 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,14 @@ +2003-08-22 Alexandre Duret-Lutz + + 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 * tgba/tgbaproduct.cc, tgba/tgbaproduct.hh: diff --git a/src/tgba/tgbaproduct.cc b/src/tgba/tgbaproduct.cc index 02ad81176..d08fd3f3a 100644 --- a/src/tgba/tgbaproduct.cc +++ b/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())); - neg_accepting_conditions_ = (left_->neg_accepting_conditions() - & right_->neg_accepting_conditions()); + & right_acc_complement_)); + neg_accepting_conditions_ = lna & rna; + 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(), - right_->neg_accepting_conditions()); + left_acc_complement_, + right_acc_complement_); } bdd diff --git a/src/tgba/tgbaproduct.hh b/src/tgba/tgbaproduct.hh index ad424e2f4..6b7a19e90 100644 --- a/src/tgba/tgbaproduct.hh +++ b/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. diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 11e68ba57..f43ae09ef 100644 --- a/src/tgbatest/Makefile.am +++ b/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) diff --git a/src/tgbatest/explpro2.test b/src/tgbatest/explpro2.test new file mode 100755 index 000000000..960bc96be --- /dev/null +++ b/src/tgbatest/explpro2.test @@ -0,0 +1,34 @@ +#!/bin/sh + +. ./defs + +set -e + +cat >input1 <input2 <expected < 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