diff --git a/ChangeLog b/ChangeLog index 87142532f..56759cb3d 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,20 @@ +2003-08-29 Alexandre Duret-Lutz + + * src/tgba/tgbaexplicit.cc (tgba_explicit::all_accepting_conditions) + Compute all_accepting_conditions_ from neg_accepting_conditions_, + not by browsing the dictionary. The dictionary also contains + accepting conditions from other automata... This bug was a + consequence of the change from 2003-07-14. + * src/tgbaalgos/save.cc (save_bfs::start()): Likewise, do not + browse the dictionary to print accepting conditions. Call + ->all_accepting_conditions() instead. + * src/tgba/tgbaproduct.cc (tgba_product::tgba_product): Typo + from 2003-08-22 in the computation of all_accepting_conditions_. + * src/tgbatest/explpro3.test: New file. + * src/tgbatest/Makefile.am (TESTS): Add explpro3.test. + * src/tgbatest/explprod.test, src/tgbatest/explpro2.test, + src/tgbatest/tripprod.test: Sort the output using Perl. + 2003-08-28 Alexandre Duret-Lutz Rewrite all std::map as @@ -413,7 +430,7 @@ * iface/gspn/gspn.cc (EVENT_TRUE): Undefine. (tgba_gspn_private_::~tgba_gspn_private_): Free all_indexes. * iface/gspn/dottygspn.cc (main): Destroy the automaton before - its dictionnary. + its dictionary. 2003-07-17 Alexandre Duret-Lutz diff --git a/src/tgba/tgbaexplicit.cc b/src/tgba/tgbaexplicit.cc index a78e34da0..a81d42931 100644 --- a/src/tgba/tgbaexplicit.cc +++ b/src/tgba/tgbaexplicit.cc @@ -307,11 +307,22 @@ namespace spot if (!all_accepting_conditions_computed_) { bdd all = bddfalse; - bdd_dict::fv_map::const_iterator i; - for (i = dict_->acc_map.begin(); i != dict_->acc_map.end(); ++i) + + // Build all_accepting_conditions_ from neg_accepting_conditions_ + // I.e., transform !A & !B & !C into + // A & !B & !C + // + !A & B & !C + // + !A & !B & C + bdd cur = neg_accepting_conditions_; + while (cur != bddtrue) { - bdd v = bdd_ithvar(i->second); + assert(cur != bddfalse); + + bdd v = bdd_ithvar(bdd_var(cur)); all |= v & bdd_exist(neg_accepting_conditions_, v); + + assert(bdd_high(cur) != bddtrue); + cur = bdd_low(cur); } all_accepting_conditions_ = all; all_accepting_conditions_computed_ = true; diff --git a/src/tgba/tgbaproduct.cc b/src/tgba/tgbaproduct.cc index d08fd3f3a..a5a959d49 100644 --- a/src/tgba/tgbaproduct.cc +++ b/src/tgba/tgbaproduct.cc @@ -154,9 +154,9 @@ namespace spot right_acc_complement_ = bdd_exist(rna, bdd_support(lna)); all_accepting_conditions_ = ((left_->all_accepting_conditions() - & left_acc_complement_) + & right_acc_complement_) | (right_->all_accepting_conditions() - & right_acc_complement_)); + & left_acc_complement_)); neg_accepting_conditions_ = lna & rna; dict_->register_all_variables_of(&left_, this); diff --git a/src/tgbaalgos/save.cc b/src/tgbaalgos/save.cc index afc1a5a55..e9042e722 100644 --- a/src/tgbaalgos/save.cc +++ b/src/tgbaalgos/save.cc @@ -20,11 +20,29 @@ namespace spot { const bdd_dict* d = automata_->get_dict(); os_ << "acc ="; - for (bdd_dict::fv_map::const_iterator ai = d->acc_map.begin(); - ai != d->acc_map.end(); ++ai) + + bdd acc = automata_->all_accepting_conditions(); + while (acc != bddfalse) { - os_ << " \""; - ltl::to_string(ai->first, os_) << "\""; + bdd cube = bdd_satone(acc); + acc -= cube; + while (cube != bddtrue) + { + assert(cube != bddfalse); + // Display the first variable that is positive. + // There should be only one per satisfaction. + if (bdd_high(cube) != bddfalse) + { + int v = bdd_var(cube); + bdd_dict::vf_map::const_iterator vi = + d->acc_formula_map.find(v); + assert(vi != d->acc_formula_map.end()); + os_ << " \""; + ltl::to_string(vi->second, os_) << "\""; + break; + } + cube = bdd_low(cube); + } } os_ << ";" << std::endl; } @@ -37,7 +55,7 @@ namespace spot for (si->first(); !si->done(); si->next()) { state* dest = si->current_state(); - os_ << "\"" << cur << "\", \"" + os_ << "\"" << cur << "\", \"" << automata_->format_state(dest) << "\", "; bdd_print_sat(os_, d, si->current_condition()) << ","; bdd_print_acc(os_, d, si->current_accepting_conditions()); diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index f43ae09ef..f49786096 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -39,6 +39,7 @@ TESTS = \ bddprod.test \ explprod.test \ explpro2.test \ + explpro3.test \ tripprod.test \ mixprod.test \ ltlmagic.test \ diff --git a/src/tgbatest/explpro2.test b/src/tgbatest/explpro2.test index 960bc96be..ac3d0a09e 100755 --- a/src/tgbatest/explpro2.test +++ b/src/tgbatest/explpro2.test @@ -18,16 +18,16 @@ EOF cat >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 +perl -pe 's/("\w+") ("\w+")(?: ("\w+"))?/@{[sort $1, $2, $3]}/g' \ + stdout > tmp_ && mv tmp_ stdout cat stdout diff stdout expected diff --git a/src/tgbatest/explpro3.test b/src/tgbatest/explpro3.test new file mode 100755 index 000000000..9f1d922f3 --- /dev/null +++ b/src/tgbatest/explpro3.test @@ -0,0 +1,33 @@ +#!/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/"p3" "p2"/"p2" "p3"/g' stdout > tmp_ && mv tmp_ stdout + +cat stdout +diff stdout expected +rm input1 input2 stdout expected diff --git a/src/tgbatest/explprod.test b/src/tgbatest/explprod.test index 239e6e335..6811ecf48 100755 --- a/src/tgbatest/explprod.test +++ b/src/tgbatest/explprod.test @@ -20,17 +20,16 @@ EOF cat >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" "p1"/"p1" "p3"/g;s/"p3" "p2"/"p2" "p3"/g;s/"p2" "p1"/"p1" "p2"/g' stdout > tmp_ && - mv tmp_ stdout +perl -pe 's/("\w+") ("\w+")(?: ("\w+"))?/@{[sort $1, $2, $3]}/g' \ + stdout > tmp_ && mv tmp_ stdout cat stdout diff stdout expected diff --git a/src/tgbatest/tripprod.test b/src/tgbatest/tripprod.test index 9aa0f05cf..ae4c4a55a 100755 --- a/src/tgbatest/tripprod.test +++ b/src/tgbatest/tripprod.test @@ -28,25 +28,20 @@ EOF cat >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/"p4" "p1"/"p1" "p4"/g; - s/"p3" "p1"/"p1" "p3"/g; - s/"p2" "p1"/"p1" "p2"/g; - s/"p4" "p2"/"p2" "p4"/g; - s/"p3" "p2"/"p2" "p3"/g; - s/"p4" "p3"/"p3" "p4"/g' stdout > tmp_ && +perl -pe 's/c a/a c/g;s/b a/a b/g;s/("\w+") ("\w+")(?: ("\w+"))?(?: ("\w+"))?/@{[sort $1, $2, $3, $4]}/g' \ + stdout > tmp_ && mv tmp_ stdout cat stdout