diff --git a/ChangeLog b/ChangeLog index 140c45163..0714ecac9 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,6 +1,18 @@ +2009-06-10 Guillaume Sadegh + + During the complementation, transform the auxiliary Streett + automaton into a TGBA instead of a TBA. + + * src/tgba/tgbacomplement.hh, src/tgba/tgbacomplement.cc: + Adjust the transformation from Streett to Büchi to support + generalized acceptance conditions. + * src/tgbatest/complementation.cc: Improve output messages. + * src/tgbatest/complementation.test: New tests. + 2009-06-09 Guillaume Sadegh - * src/tgba/tgbacomplement.cc, src/tgbatest/complementation.cc: Fix style. + * src/tgba/tgbacomplement.cc, src/tgbatest/complementation.cc: + Fix style. 2009-06-07 Guillaume Sadegh diff --git a/src/tgba/tgbacomplement.cc b/src/tgba/tgbacomplement.cc index f991c2cb3..c40808d45 100644 --- a/src/tgba/tgbacomplement.cc +++ b/src/tgba/tgbacomplement.cc @@ -901,7 +901,7 @@ namespace spot state_complement::state_complement(bitset_t L, bitset_t U, const safra_tree* tree, bool use_bitset) - : U(U), L(L), tree(tree), use_bitset(use_bitset) + : state(), U(U), L(L), tree(tree), use_bitset(use_bitset) { } @@ -921,8 +921,11 @@ namespace spot const state_complement* s = dynamic_cast(other); if (s == 0) return 1; +#if TRANSFORM_TO_TBA + // When we transform to TBA instead of TGBA, states depend on the U set. if (U != s->U) return (U < s->U) ? -1 : 1; +#endif if (L != s->L) return (L < s->L) ? -1 : 1; if (use_bitset != s->use_bitset) @@ -940,7 +943,9 @@ namespace spot for (unsigned i = 0; i < size_bitset; ++i) { hash ^= wang32_hash(L[i]); - hash ^= wang32_hash(U[i]); // \todo To not apply for TGBAs +#if TRANSFORM_TO_TBA + hash ^= wang32_hash(U[i]); +#endif } return hash; @@ -964,7 +969,13 @@ namespace spot std::stringstream ss; ss << tree; if (use_bitset) - ss << " - I:" << U << " J:" << L; + { + ss << " - I:" << U; +#if TRANSFORM_TO_TBA + ss << " J:" << L; +#endif + } + return ss.str(); } @@ -1102,7 +1113,25 @@ namespace spot // Let's call it Acc[True]. int v = get_dict() ->register_acceptance_variable(ltl::constant::true_instance(), safra_); + +#if TRANSFORM_TO_TBA the_acceptance_cond_ = bdd_ithvar(v); +#endif + +#if TRANSFORM_TO_TGBA + unsigned nb_acc = safra_->get_nb_acceptance_pairs(); + all_acceptance_cond_ = bddfalse; + neg_acceptance_cond_ = bddtrue; + acceptance_cond_vec_.reserve(nb_acc); + for (unsigned i = 0; i < nb_acc; ++i) + { + int r = get_dict()->register_clone_acc(v, safra_); + all_acceptance_cond_ |= bdd_ithvar(r); + acceptance_cond_vec_[i] = r; + neg_acceptance_cond_ &= bdd_nithvar(r); + } +#endif + } tgba_complement::~tgba_complement() @@ -1184,7 +1213,21 @@ namespace spot st = new state_complement(e, e, i->second, true); succ_list.insert(std::make_pair(i->first, st)); } + +#if TRANSFORM_TO_TBA condition = the_acceptance_cond_; +#else + for (unsigned i = 0; i < l.size(); ++i) + { + if (u[i]) + { + if (condition == bddfalse) + condition = bdd_ithvar(acceptance_cond_vec_[i]); + else + condition &= bdd_ithvar(acceptance_cond_vec_[i]); + } + } +#endif } else // \delta'((q, I, J), a) { @@ -1220,13 +1263,21 @@ namespace spot bdd tgba_complement::all_acceptance_conditions() const { +#if TRANSFORM_TO_TBA return the_acceptance_cond_; +#else + return all_acceptance_cond_; +#endif } bdd tgba_complement::neg_acceptance_conditions() const { +#if TRANSFORM_TO_TBA return !the_acceptance_cond_; +#else + return neg_acceptance_cond_; +#endif } bdd diff --git a/src/tgba/tgbacomplement.hh b/src/tgba/tgbacomplement.hh index ae80d69bc..df494379b 100644 --- a/src/tgba/tgbacomplement.hh +++ b/src/tgba/tgbacomplement.hh @@ -1,8 +1,14 @@ #ifndef SPOT_TGBA_TGBACOMPLEMENT_HH # define SPOT_TGBA_TGBACOMPLEMENT_HH +# include # include "tgba/tgba.hh" +#ifndef TRANSFORM_TO_TBA +# define TRANSFORM_TO_TBA 0 +#endif +#define TRANSFORM_TO_TGBA (!TRANSFORM_TO_TBA) + namespace spot { struct safra_tree_automaton; @@ -53,7 +59,16 @@ namespace spot private: const tgba* automaton_; safra_tree_automaton* safra_; +#if TRANSFORM_TO_TBA bdd the_acceptance_cond_; +#endif +#if TRANSFORM_TO_TGBA + bdd all_acceptance_cond_; + bdd neg_acceptance_cond_; + // Map to i the i-th acceptance condition of the final automaton. + std::vector acceptance_cond_vec_; +#endif + }; /// \brief Produce a dot output of the Safra automaton associated diff --git a/src/tgbatest/complementation.cc b/src/tgbatest/complementation.cc index e599afe52..cdb5dc21f 100644 --- a/src/tgbatest/complementation.cc +++ b/src/tgbatest/complementation.cc @@ -137,19 +137,25 @@ int main(int argc, char* argv[]) spot::tgba_statistics a_size = spot::stats_reachable(a); std::cout << "Original: " << a_size.states << ", " - << a_size.transitions << std::endl; + << a_size.transitions << ", " + << a->number_of_acceptance_conditions() + << std::endl; spot::tgba *buchi = new spot::tgba_sba_proxy(a); a_size = spot::stats_reachable(buchi); std::cout << "Buchi: " << a_size.states << ", " - << a_size.transitions << std::endl; + << a_size.transitions << ", " + << buchi->number_of_acceptance_conditions() + << std::endl; delete buchi; spot::tgba_statistics b_size = spot::stats_reachable(complement); std::cout << "Complement: " << b_size.states << ", " - << b_size.transitions << std::endl; + << b_size.transitions << ", " + << complement->number_of_acceptance_conditions() + << std::endl; delete complement; delete a; @@ -162,7 +168,9 @@ int main(int argc, char* argv[]) spot::tgba_statistics a_size = spot::stats_reachable(a2); std::cout << "Not Formula: " << a_size.states << ", " - << a_size.transitions << std::endl; + << a_size.transitions << ", " + << a2->number_of_acceptance_conditions() + << std::endl; delete a2; spot::ltl::destroy(f1); @@ -187,18 +195,20 @@ int main(int argc, char* argv[]) spot::emptiness_check* ec = spot::couvreur99(prod); spot::emptiness_check_result* res = ec->check(); spot::tgba_statistics a_size = spot::stats_reachable(ec->automaton()); - std::cout << std::right << std::setw(10) - << a_size.states << ", " - << std::right << std::setw(10) - << a_size.transitions << ", " - << ec->automaton()->number_of_acceptance_conditions(); + std::cout << "States: " + << a_size.states << std::endl + << "Transitions: " + << a_size.transitions << std::endl + << "Acc Cond: " + << ec->automaton()->number_of_acceptance_conditions() + << std::endl; if (res) { - std::cout << ", FAIL"; + std::cout << "FAIL"; return_value = 1; } else - std::cout << ", OK"; + std::cout << "OK"; std::cout << std::endl; delete res; diff --git a/src/tgbatest/complementation.test b/src/tgbatest/complementation.test index bd42f2e79..934e4df67 100755 --- a/src/tgbatest/complementation.test +++ b/src/tgbatest/complementation.test @@ -24,8 +24,17 @@ set -e -FORMULAE='GFa FGa <>p1->(p0Up1) [](p0-><>p3) GFa&&FGa' - -for f in $FORMULAE; do +while read f; do run 0 ./complement -f "$f" -done +done <p1->(p0Up1) +[](p0-><>p3) +GFa&&FGa +[] ((p2 && ! p1) -> (p0 U (p1 || [] p0))) +[] (p2 -> ((! p0 && ! p1) U (p1 || ((p0 && ! p1) U (p1 || ((! p0 && ! p1) \ + U (p1 || ((p0 && ! p1) U ((p1 || (! p0 U (p1 || [] ! p0))) || [] p0))))))))) +(p0 U (p1 && X (p2 && (true U (p3 && X (true U (p4 && X \ +(true U (p5 && X (true U p6)))))))))) +EOF