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

* src/tgbaalgos/degen.cc (outgoing_acc): Fill both caches at once.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2012-06-05 08:05:18 +02:00
parent 5dbee4faab
commit 59a2763f41
1 changed files with 30 additions and 32 deletions
Download patch file Download diff file Expand all files Collapse all files

62
src/tgbaalgos/degen.cc
View file

@ -97,50 +97,48 @@ namespace spot
class outgoing_acc class outgoing_acc
{ {
const tgba* a_; const tgba* a_;
typedef Sgi::hash_map<const state*, bdd, typedef std::pair<bdd, bdd> cache_entry;
state_ptr_hash, state_ptr_equal> accmap_t; typedef Sgi::hash_map<const state*, cache_entry,
mutable accmap_t accmap_; state_ptr_hash, state_ptr_equal> cache_t;
mutable accmap_t accmapu_; cache_t cache_;
public: public:
outgoing_acc(const tgba* a): a_(a) outgoing_acc(const tgba* a): a_(a)
{ {
} }
bdd common_acc(const state* s) cache_t::const_iterator fill_cache(const state* s)
{ {
// Lookup cache
accmap_t::const_iterator i = accmap_.find(s);
if (i != accmap_.end())
return i->second;
bdd common = a_->all_acceptance_conditions(); bdd common = a_->all_acceptance_conditions();
tgba_succ_iterator* it = a_->succ_iter(s); bdd union_ = bddfalse;
for (it->first(); !it->done() && common != bddfalse; it->next())
common &= it->current_acceptance_conditions();
delete it;
// Populate cache
accmap_[s->clone()] = common;
return common;
}
bdd union_acc(const state* s)
{
// Lookup cache
accmap_t::const_iterator i = accmapu_.find(s);
if (i != accmapu_.end())
return i->second;
bdd common = bddfalse;
tgba_succ_iterator* it = a_->succ_iter(s); tgba_succ_iterator* it = a_->succ_iter(s);
for (it->first(); !it->done(); it->next()) for (it->first(); !it->done(); it->next())
common |= it->current_acceptance_conditions(); {
bdd set = it->current_acceptance_conditions();
common &= set;
union_ |= set;
}
delete it; delete it;
cache_entry e(common, union_);
return cache_.insert(std::make_pair(s, e)).first;
}
// Populate cache // Intersection of all outgoing acceptance sets
accmapu_[s->clone()] = common; bdd common_acc(const state* s)
return common; {
cache_t::const_iterator i = cache_.find(s);
if (i == cache_.end())
i = fill_cache(s);
return i->second.first;
}
// Union of all outgoing acceptance sets
bdd union_acc(const state* s)
{
cache_t::const_iterator i = cache_.find(s);
if (i == cache_.end())
i = fill_cache(s);
return i->second.second;
} }
}; };
} }