diff --git a/ChangeLog b/ChangeLog index 049d61ab5..04980bbcc 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,9 @@ 2003-07-10 Alexandre Duret-Lutz + * src/tgbaalgos/ltl2tgba.cc (ltl_trad_visitor::visit(multop)): + Forward root_ to children of And. + (ltl_trad_visitor::recurse): Take a root argument. + * src/tgba/tgbabddconcretefactory.hh (tgba_bdd_concrete_factory::add_relation): Rename as ... (tgba_bdd_concrete_factory::constrain_relation): ... this. diff --git a/src/tgbaalgos/ltl2tgba.cc b/src/tgbaalgos/ltl2tgba.cc index 3b8986682..00c1383c6 100644 --- a/src/tgbaalgos/ltl2tgba.cc +++ b/src/tgbaalgos/ltl2tgba.cc @@ -191,11 +191,17 @@ namespace spot visit(const multop* node) { int op = -1; + bool root = false; switch (node->op()) { case multop::And: op = bddop_and; res_ = bddtrue; + // When the root formula is a conjunction it's ok to + // consider all children as root formulae. This allows the + // root-G trick to save many more variable. (See the + // translation of G.) + root = root_; break; case multop::Or: op = bddop_or; @@ -206,14 +212,14 @@ namespace spot unsigned s = node->size(); for (unsigned n = 0; n < s; ++n) { - res_ = bdd_apply(res_, recurse(node->nth(n)), op); + res_ = bdd_apply(res_, recurse(node->nth(n), root), op); } } bdd - recurse(const formula* f) + recurse(const formula* f, bool root = false) { - ltl_trad_visitor v(fact_); + ltl_trad_visitor v(fact_, root); f->accept(v); return v.result(); }