alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* src/tgbaalgos/ltl2tgba.cc (ltl_trad_visitor::visit(multop)):

Browse source 
Forward root_ to children of And.
(ltl_trad_visitor::recurse): Take a root argument.
This commit is contained in:
Alexandre Duret-Lutz 2003-07-10 14:27:19 +00:00
parent b963af66f1
commit 9a4da5ffd4
2 changed files with 13 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

4
ChangeLog
View file

@ -1,5 +1,9 @@
2003-07-10 Alexandre Duret-Lutz <aduret@src.lip6.fr> 2003-07-10 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* 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 * src/tgba/tgbabddconcretefactory.hh
(tgba_bdd_concrete_factory::add_relation): Rename as ... (tgba_bdd_concrete_factory::add_relation): Rename as ...
(tgba_bdd_concrete_factory::constrain_relation): ... this. (tgba_bdd_concrete_factory::constrain_relation): ... this.

12
src/tgbaalgos/ltl2tgba.cc
View file

@ -191,11 +191,17 @@ namespace spot
visit(const multop* node) visit(const multop* node)
{ {
int op = -1; int op = -1;
bool root = false;
switch (node->op()) switch (node->op())
{ {
case multop::And: case multop::And:
op = bddop_and; op = bddop_and;
res_ = bddtrue; 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; break;
case multop::Or: case multop::Or:
op = bddop_or; op = bddop_or;
@ -206,14 +212,14 @@ namespace spot
unsigned s = node->size(); unsigned s = node->size();
for (unsigned n = 0; n < s; ++n) 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 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); f->accept(v);
return v.result(); return v.result();
} }