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

* src/tgbaalgos/simulation.cc: Merge two loops.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2013-02-12 19:16:55 +01:00
parent 08c77318ae
commit ca94168540
1 changed files with 4 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/tgbaalgos/simulation.cc
View file

@ -1280,6 +1280,9 @@ namespace spot
list_bdd_bdd dont_care_now_to_now; list_bdd_bdd dont_care_now_to_now;
map_bdd_state class2state; map_bdd_state class2state;
list_bdd_bdd now_to_now;
bdd_lstate_.clear();
// Compute the don't care signature for all the states. // Compute the don't care signature for all the states.
for (std::list<const state*>::const_iterator my_it = order_.begin(); for (std::list<const state*>::const_iterator my_it = order_.begin();
my_it != order_.end(); my_it != order_.end();
@ -1293,19 +1296,8 @@ namespace spot
dont_care_state2sig[src] = sig; dont_care_state2sig[src] = sig;
dont_care_now_to_now.push_back(std::make_pair(sig, it->second)); dont_care_now_to_now.push_back(std::make_pair(sig, it->second));
class2state[it->second] = it->first; class2state[it->second] = it->first;
}
list_bdd_bdd now_to_now; sig = compute_sig(src);
bdd_lstate_.clear();
// Compute the signature for all the states.
for (std::list<const state*>::const_iterator my_it = order_.begin();
my_it != order_.end();
++my_it)
{
map_state_bdd::iterator it = previous_class_.find(*my_it);
const state* src = it->first;
bdd sig = compute_sig(src);
bdd_lstate_[sig].push_back(src); bdd_lstate_[sig].push_back(src);
state2sig[src] = sig; state2sig[src] = sig;
now_to_now.push_back(std::make_pair(sig, it->second)); now_to_now.push_back(std::make_pair(sig, it->second));