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

Optimize previous patch.

Browse source 
* src/tgbaalgos/scc.hh (scc_map::scc::supp_rec): Initialize to
bddfalse, since this cannot occur in reallife.
* src/tgbaalgos/scc.cc (scc_map::update_supp_rec): Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2009-09-18 10:39:07 +02:00
parent fa8dd7f160
commit fd0de04d24
3 changed files with 12 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
ChangeLog
View file

@ -1,3 +1,11 @@
2009-09-18 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Optimize previous patch.
* src/tgbaalgos/scc.hh (scc_map::scc::supp_rec): Initialize to
bddfalse, since this cannot occur in reallife.
* src/tgbaalgos/scc.cc (scc_map::update_supp_rec): Adjust.
2009-09-17 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Have scc_map keep track of APs that are reachable from a SCC.

6
src/tgbaalgos/scc.cc
View file

@ -112,15 +112,15 @@ namespace spot
bdd& res = scc_map_[state].supp_rec;
if (res == bddtrue)
if (res == bddfalse)
{
const succ_type& s = succ(state);
succ_type::const_iterator it;
res = scc_map_[state].supp;
for (it = s.begin(); it != s.end(); ++it)
res &= update_supp_rec(it->first);
res &= scc_map_[state].supp;
}
return res;

2
src/tgbaalgos/scc.hh
View file

@ -150,7 +150,7 @@ namespace spot
{
public:
scc(int index) : index(index), acc(bddfalse),
supp(bddtrue), supp_rec(bddtrue) {};
supp(bddtrue), supp_rec(bddfalse) {};
/// Index of the SCC.
int index;
/// The union of all acceptance conditions of transitions which