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

* src/tgbaalgos/ltl2tgba_fm.cc (ltl_trad_visitor::visit) <unop::G>:

Browse source 
suppress the GFy optimisation introduced on 2003-11-26, it is
generalized by the identification of states with same symbolic
rewriting introduced on 2004-02-02.
This commit is contained in:
Alexandre Duret-Lutz 2004-02-16 12:25:59 +00:00
parent 4741dc02bf
commit 5cb4048120
2 changed files with 19 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

5
ChangeLog
View file

@ -1,5 +1,10 @@
2004-02-16 Alexandre Duret-Lutz <adl@src.lip6.fr> 2004-02-16 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/ltl2tgba_fm.cc (ltl_trad_visitor::visit) <unop::G>:
suppress the GFy optimisation introduced on 2003-11-26, it is
generalized by the identification of states with same symbolic
rewriting introduced on 2004-02-02.
* lbtt/: Merge lbtt 1.0.3. * lbtt/: Merge lbtt 1.0.3.
2004-02-13 Alexandre Duret-Lutz <adl@src.lip6.fr> 2004-02-13 Alexandre Duret-Lutz <adl@src.lip6.fr>

27
src/tgbaalgos/ltl2tgba_fm.cc
View file

@ -321,25 +321,22 @@ namespace spot
} }
case unop::G: case unop::G:
{ {
// The paper suggests that we optimize GFy
// as
// r(GFy) = (r(y) + a(y))r(XGFy)
// instead of
// r(GFy) = (r(y) + a(y)r(XFy)).r(XGFy)
// but this is just a particular case
// of the "merge all states with the same
// symbolic rewriting" optimization we do later.
// (r(Fy).r(GFy) and r(GFy) have the same symbolic
// rewriting.) Let's keep things simple here.
// r(Gy) = r(y)r(XGy)
const formula* child = node->child(); const formula* child = node->child();
int x = dict_.register_next_variable(node); int x = dict_.register_next_variable(node);
// GFy is pretty frequent and easy to optimize, so we
// want to detect it.
const unop* Fy = dynamic_cast<const unop*>(child);
if (Fy && Fy->op() == unop::F)
{
// r(GFy) = (r(y) + a(y))r(XGFy)
const formula* child = Fy->child();
bdd y = recurse(child);
int a = dict_.register_a_variable(child);
res_ = (y | bdd_ithvar(a)) & bdd_ithvar(x);
}
else
{
// r(Gy) = r(y)r(XGy)
bdd y = recurse(child); bdd y = recurse(child);
res_ = y & bdd_ithvar(x); res_ = y & bdd_ithvar(x);
}
return; return;
} }
case unop::Not: case unop::Not: