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

* src/tgbaalgos/emptinesscheck.cc (emptiness_check::check,

Browse source 
emptiness_check::counter_example): Simplify access to hashes
after calls to find() for the same element..
This commit is contained in:
Alexandre Duret-Lutz 2003-10-23 16:05:51 +00:00
parent fb4873d92e
commit 071cb5d62c
2 changed files with 11 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

5
ChangeLog
View file

@ -1,5 +1,9 @@
2003-10-23 Alexandre Duret-Lutz <adl@src.lip6.fr> 2003-10-23 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/emptinesscheck.cc (emptiness_check::check,
emptiness_check::counter_example): Simplify access to hashes
after calls to find() for the same element..
* src/tgbaalgos/emptinesscheck.hh (connected_component::set_of_state): * src/tgbaalgos/emptinesscheck.hh (connected_component::set_of_state):
Rename as ... Rename as ...
(connected_component::set_type): ... this, and define as a hash_set. (connected_component::set_type): ... this, and define as a hash_set.
@ -8,7 +12,6 @@
New method. New method.
(emptiness_check::counter_example, emptiness_check::complete_cycle, (emptiness_check::counter_example, emptiness_check::complete_cycle,
emptiness_check::accepting_path): Simplify using has_state(). emptiness_check::accepting_path): Simplify using has_state().
* src/tgbaalgos/emptinesscheck.hh (emptiness_check::seen_state_num): * src/tgbaalgos/emptinesscheck.hh (emptiness_check::seen_state_num):
Rename as ... Rename as ...
(emptiness_check::h): ... this, and define as a hash_map. (emptiness_check::h): ... this, and define as a hash_map.

15
src/tgbaalgos/emptinesscheck.cc
View file

@ -80,7 +80,7 @@ namespace spot
root_component.pop(); root_component.pop();
hash_type::iterator i_0 = h.find(step.first); hash_type::iterator i_0 = h.find(step.first);
assert(i_0 != h.end()); assert(i_0 != h.end());
if (comp_tmp.index == h[step.first]) if (comp_tmp.index == i_0->second)
{ {
// The current node is a root of a Strong Connected Component. // The current node is a root of a Strong Connected Component.
emptiness_check::remove_component(step.first); emptiness_check::remove_component(step.first);
@ -113,14 +113,14 @@ namespace spot
iter2->first(); iter2->first();
todo.push(pair_state_iter(current_state, iter2)); todo.push(pair_state_iter(current_state, iter2));
} }
else if (h[current_state] != -1) else if (i->second != -1)
{ {
// A node with order != -1 (a seen node not removed). // A node with order != -1 (a seen node not removed).
assert(!root_component.empty()); assert(!root_component.empty());
connected_component comp = root_component.top(); connected_component comp = root_component.top();
root_component.pop(); root_component.pop();
bdd new_condition = current_accepting; bdd new_condition = current_accepting;
int current_index = h[current_state]; int current_index = i->second;
while (comp.index > current_index) while (comp.index > current_index)
{ {
// root_component and arc_accepting are popped // root_component and arc_accepting are popped
@ -267,13 +267,12 @@ namespace spot
seq.push_front(curr_father); seq.push_front(curr_father);
hash_type::iterator i_2 = h.find(curr_father); hash_type::iterator i_2 = h.find(curr_father);
assert(i_2 != h.end()); assert(i_2 != h.end());
while ((vec_component[k].index < h[curr_father]) while (vec_component[k].index < i_2->second)
&& (h[curr_father] != 1))
{ {
assert(i_2->second != 1);
seq.push_front(path_map[curr_father]); seq.push_front(path_map[curr_father]);
curr_father = path_map[curr_father]; curr_father = path_map[curr_father];
hash_type::iterator i_3 = h.find(curr_father); assert(h.find(curr_father) != h.end());
assert(i_3 != h.end());
} }
vec_sequence[k] = seq; vec_sequence[k] = seq;
seq.clear(); seq.clear();
@ -289,7 +288,7 @@ namespace spot
hash_type::iterator i_seen = h.find(curr_state); hash_type::iterator i_seen = h.find(curr_state);
if (i_seen != h.end() if (i_seen != h.end()
&& h[curr_state] > 0 && i_seen->second > 0
&& i_path == path_map.end()) && i_path == path_map.end())
{ {
todo_trace. todo_trace.