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

* src/tgbaalgos/minimize.cc: Now use register_anonymous_variables.

Browse source
This commit is contained in:
Felix Abecassis 2010-03-26 17:31:58 +01:00 • committed by Alexandre Duret-Lutz
parent 52090e4875
commit 99c1b607de
2 changed files with 10 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

4
ChangeLog
View file

@ -1,3 +1,7 @@
2010-03-26 Felix Abecassis <abecassis@lrde.epita.fr>
* src/tgbaalgos/minimize.cc: Now use register_anonymous_variables.
2010-03-20 Felix Abecassis <abecassis@lrde.epita.fr> 2010-03-20 Felix Abecassis <abecassis@lrde.epita.fr>
Small fixes. Small fixes.

7
src/tgbaalgos/minimize.cc
View file

@ -143,10 +143,14 @@ namespace spot
hash_set* final = new hash_set; hash_set* final = new hash_set;
hash_set* non_final = new hash_set; hash_set* non_final = new hash_set;
hash_map state_set_map; hash_map state_set_map;
bdd_dict* dict = det_a->get_dict();
std::list<const state*>::iterator li; std::list<const state*>::iterator li;
for (li = acc_list.begin(); li != acc_list.end(); ++li) for (li = acc_list.begin(); li != acc_list.end(); ++li)
final->insert(*li); final->insert(*li);
init_sets(det_a, *final, *non_final, state_set_map); init_sets(det_a, *final, *non_final, state_set_map);
// Size of det_a
unsigned size = final->size() + non_final->size();
unsigned bdd_offset = dict->register_anonymous_variables(size, det_a);
hash_set* final_copy = new hash_set(*final); hash_set* final_copy = new hash_set(*final);
if (final->size() > 1) if (final->size() > 1)
todo.push(final); todo.push(final);
@ -178,7 +182,7 @@ namespace spot
const state* dst = si->current_state(); const state* dst = si->current_state();
unsigned dst_set = state_set_map[dst]; unsigned dst_set = state_set_map[dst];
delete dst; delete dst;
f |= (bdd_ithvar(dst_set) & si->current_condition()); f |= (bdd_ithvar(bdd_offset + dst_set) & si->current_condition());
} }
delete si; delete si;
bdd_states_map::iterator bsi; bdd_states_map::iterator bsi;
@ -227,6 +231,7 @@ namespace spot
// Build the result. // Build the result.
tgba_explicit_number* res = build_result(det_a, done, final_copy); tgba_explicit_number* res = build_result(det_a, done, final_copy);
dict->unregister_variable(bdd_offset, det_a);
// Free all the allocated memory. // Free all the allocated memory.
delete final_copy; delete final_copy;
hash_map::iterator hit; hash_map::iterator hit;