diff --git a/ChangeLog b/ChangeLog index e80635baf..139ad8e7c 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,6 +1,15 @@ 2004-01-29 Alexandre Duret-Lutz - After this changes, degeneralized automata are 40% smaller + * src/tgba/tgbaexplicit.cc (tgba_explicit::get_acceptance_condition): + Do not treat true and false specially. Otherwise it breaks + translation of F(false). + * src/tgbatest/explprod.test, src/tgbatest/tripprod.test: Do not + use true as acceptance condition. + + * src/tgbaalgos/ltl2tgba_fm.cc (ltl_trad_visitor): Use Acc[b] as + acceptance condition for Fb, not Acc[Fb]. + + After this change, degeneralized automata are 40% smaller in LBTT's statistics. * src/tgba/tgbatba.cc (state_tba_proxy): Store an iterator, diff --git a/src/tgba/tgbaexplicit.cc b/src/tgba/tgbaexplicit.cc index 03e78404a..3a2edaa3e 100644 --- a/src/tgba/tgbaexplicit.cc +++ b/src/tgba/tgbaexplicit.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -260,19 +260,6 @@ namespace spot bdd tgba_explicit::get_acceptance_condition(const ltl::formula* f) { - const ltl::constant* c = dynamic_cast(f); - if (c) - { - switch (c->val()) - { - case ltl::constant::True: - return bddtrue; - case ltl::constant::False: - return bddfalse; - } - /* Unreachable code. */ - assert(0); - } bdd_dict::fv_map::iterator i = dict_->acc_map.find(f); assert(has_acceptance_condition(f)); /* If this second assert fails and the first doesn't, diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index 563adf0c2..21735f1de 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -312,8 +312,9 @@ namespace spot case unop::F: { // r(Fy) = r(y) + a(y)r(XFy) - bdd y = recurse(node->child()); - int a = dict_.register_a_variable(node); + const formula* child = node->child(); + bdd y = recurse(child); + int a = dict_.register_a_variable(child); int x = dict_.register_next_variable(node); res_ = y | (bdd_ithvar(a) & bdd_ithvar(x)); return; diff --git a/src/tgbatest/explprod.test b/src/tgbatest/explprod.test index 7f510dd2a..6bb5f4b3d 100755 --- a/src/tgbatest/explprod.test +++ b/src/tgbatest/explprod.test @@ -27,10 +27,10 @@ set -e cat >input1 <input2 <input1 <