diff --git a/ChangeLog b/ChangeLog index 9fdfa7201..966eaf68a 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,8 @@ 2005-01-03 Alexandre Duret-Lutz + * src/tgbaalgos/ndfs_result.hh (construct_prefix): Do not call + erase() after splice(), splice() already removes the elements. + * src/evtgba/evtgbaiter.hh, src/ltlast/formula.hh, src/ltlast/refformula.hh, src/ltlenv/defaultenv.hh, src/misc/bareword.hh, src/tgba/succiter.hh, @@ -46,7 +49,7 @@ 2004-12-16 Alexandre Duret-Lutz * src/tgbaalgos/reducerun.cc (reduce_run): Do not call erase() after - splice(), splice() already remove the elements. + splice(), splice() already removes the elements. * src/tgbaalgos/gtec/ce.cc (couvreur99_check_result::accepting_run): Likewise. diff --git a/src/tgbaalgos/ndfs_result.hh b/src/tgbaalgos/ndfs_result.hh index c8283de3f..7de92a234 100644 --- a/src/tgbaalgos/ndfs_result.hh +++ b/src/tgbaalgos/ndfs_result.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -61,7 +61,7 @@ namespace spot typedef std::list stack_type; - template < typename ndfs_search, typename heap > + template class ndfs_result : public emptiness_check_result { public: @@ -161,7 +161,7 @@ namespace spot { bool b = dfs(start, acc_trans, covered_acc); assert(b); - (void)b; + (void) b; } delete start; @@ -177,8 +177,7 @@ namespace spot construct_prefix(run); for (typename accepting_transitions_list::const_iterator i = - acc_trans.begin(); - i != acc_trans.end(); ++i) + acc_trans.begin(); i != acc_trans.end(); ++i) { delete i->source; delete i->dest; @@ -203,146 +202,146 @@ namespace spot state_ptr_hash, state_ptr_equal> state_set; void clean(stack_type& st1, state_set& seen, state_set& dead) - { - while (!st1.empty()) - { - delete st1.front().it; - st1.pop_front(); - } - for (state_set::iterator i = seen.begin(); i != seen.end();) - { - const state* s = *i; - ++i; - delete s; - } - for (state_set::iterator i = dead.begin(); i != dead.end();) - { - const state* s = *i; - ++i; - delete s; - } - } + { + while (!st1.empty()) + { + delete st1.front().it; + st1.pop_front(); + } + for (state_set::iterator i = seen.begin(); i != seen.end();) + { + const state* s = *i; + ++i; + delete s; + } + for (state_set::iterator i = dead.begin(); i != dead.end();) + { + const state* s = *i; + ++i; + delete s; + } + } bool dfs(const state* target, accepting_transitions_list& acc_trans, - bdd& covered_acc) - { - assert(h_.has_been_visited(target)); - stack_type st1; + bdd& covered_acc) + { + assert(h_.has_been_visited(target)); + stack_type st1; - state_set seen, dead; - const state* start = target->clone(); + state_set seen, dead; + const state* start = target->clone(); - seen.insert(start); - tgba_succ_iterator* i = a_->succ_iter(start); - i->first(); - st1.push_front(stack_item(start, i, bddfalse, bddfalse)); + seen.insert(start); + tgba_succ_iterator* i = a_->succ_iter(start); + i->first(); + st1.push_front(stack_item(start, i, bddfalse, bddfalse)); - while (!st1.empty()) - { - stack_item& f = st1.front(); - ndfsr_trace << "DFS1 treats: " << a_->format_state(f.s) - << std::endl; - if (!f.it->done()) - { - const state *s_prime = f.it->current_state(); - ndfsr_trace << " Visit the successor: " - << a_->format_state(s_prime) << std::endl; - bdd label = f.it->current_condition(); - bdd acc = f.it->current_acceptance_conditions(); - f.it->next(); - if (h_.has_been_visited(s_prime)) - { - if (dead.find(s_prime) != dead.end()) - { - ndfsr_trace << " it is dead, pop it" << std::endl; - delete s_prime; - } - else if (seen.find(s_prime) == seen.end()) - { - ndfsr_trace << " it is not seen, go down" << std::endl; - seen.insert(s_prime); - tgba_succ_iterator* i = a_->succ_iter(s_prime); - i->first(); - st1.push_front(stack_item(s_prime, i, label, acc)); - } - else if ((acc & covered_acc) != acc) - { - ndfsr_trace << " a propagation is needed, " - << "start a search" << std::endl; - if (search(s_prime, target, dead)) - { - transition t = { f.s->clone(), label, acc, - s_prime->clone() }; - assert(h_.has_been_visited(t.source)); - assert(h_.has_been_visited(t.dest)); - acc_trans.push_back(t); - covered_acc |= acc; - if (covered_acc == a_->all_acceptance_conditions()) - { - clean(st1, seen, dead); - delete s_prime; - return true; - } - } - delete s_prime; - } - else - { - ndfsr_trace << " already seen, pop it" << std::endl; - delete s_prime; - } - } - else - { - ndfsr_trace << " not seen during the search, pop it" - << std::endl; - delete s_prime; - } - } - else - { - ndfsr_trace << " all the successors have been visited" - << std::endl; - stack_item f_dest(f); - delete st1.front().it; - st1.pop_front(); - if (!st1.empty() && (f_dest.acc & covered_acc) != f_dest.acc) - { - ndfsr_trace << " a propagation is needed, start a search" - << std::endl; - if (search(f_dest.s, target, dead)) - { - transition t = { st1.front().s->clone(), - f_dest.label, f_dest.acc, - f_dest.s->clone() }; - assert(h_.has_been_visited(t.source)); - assert(h_.has_been_visited(t.dest)); - acc_trans.push_back(t); - covered_acc |= f_dest.acc; - if (covered_acc == a_->all_acceptance_conditions()) - { - clean(st1, seen, dead); - return true; - } - } - } - else - { - ndfsr_trace << " no propagation needed, pop it" - << std::endl; - } - } - } + while (!st1.empty()) + { + stack_item& f = st1.front(); + ndfsr_trace << "DFS1 treats: " << a_->format_state(f.s) + << std::endl; + if (!f.it->done()) + { + const state *s_prime = f.it->current_state(); + ndfsr_trace << " Visit the successor: " + << a_->format_state(s_prime) << std::endl; + bdd label = f.it->current_condition(); + bdd acc = f.it->current_acceptance_conditions(); + f.it->next(); + if (h_.has_been_visited(s_prime)) + { + if (dead.find(s_prime) != dead.end()) + { + ndfsr_trace << " it is dead, pop it" << std::endl; + delete s_prime; + } + else if (seen.find(s_prime) == seen.end()) + { + ndfsr_trace << " it is not seen, go down" << std::endl; + seen.insert(s_prime); + tgba_succ_iterator* i = a_->succ_iter(s_prime); + i->first(); + st1.push_front(stack_item(s_prime, i, label, acc)); + } + else if ((acc & covered_acc) != acc) + { + ndfsr_trace << " a propagation is needed, " + << "start a search" << std::endl; + if (search(s_prime, target, dead)) + { + transition t = { f.s->clone(), label, acc, + s_prime->clone() }; + assert(h_.has_been_visited(t.source)); + assert(h_.has_been_visited(t.dest)); + acc_trans.push_back(t); + covered_acc |= acc; + if (covered_acc == a_->all_acceptance_conditions()) + { + clean(st1, seen, dead); + delete s_prime; + return true; + } + } + delete s_prime; + } + else + { + ndfsr_trace << " already seen, pop it" << std::endl; + delete s_prime; + } + } + else + { + ndfsr_trace << " not seen during the search, pop it" + << std::endl; + delete s_prime; + } + } + else + { + ndfsr_trace << " all the successors have been visited" + << std::endl; + stack_item f_dest(f); + delete st1.front().it; + st1.pop_front(); + if (!st1.empty() && (f_dest.acc & covered_acc) != f_dest.acc) + { + ndfsr_trace << " a propagation is needed, start a search" + << std::endl; + if (search(f_dest.s, target, dead)) + { + transition t = { st1.front().s->clone(), + f_dest.label, f_dest.acc, + f_dest.s->clone() }; + assert(h_.has_been_visited(t.source)); + assert(h_.has_been_visited(t.dest)); + acc_trans.push_back(t); + covered_acc |= f_dest.acc; + if (covered_acc == a_->all_acceptance_conditions()) + { + clean(st1, seen, dead); + return true; + } + } + } + else + { + ndfsr_trace << " no propagation needed, pop it" + << std::endl; + } + } + } - clean(st1, seen, dead); - return false; - } + clean(st1, seen, dead); + return false; + } class test_path: public bfs_steps { public: test_path(const tgba* a, const state* t, - const state_set& d, const heap& h) + const state_set& d, const heap& h) : bfs_steps(a), target(t), dead(d), h(h) { } @@ -369,8 +368,9 @@ namespace spot const state* filter(const state* s) { - if (!h.has_been_visited(s) || seen.find(s) != seen.end() || - dead.find(s) != dead.end()) + if (!h.has_been_visited(s) + || seen.find(s) != seen.end() + || dead.find(s) != dead.end()) { delete s; return 0; @@ -379,9 +379,9 @@ namespace spot return s; } - void finalize( - const std::map&, - const tgba_run::step&, const state*, tgba_run::steps&) + void finalize(const std::map&, + const tgba_run::step&, const state*, tgba_run::steps&) { } @@ -403,29 +403,29 @@ namespace spot }; bool search(const state* start, const state* target, state_set& dead) - { - tgba_run::steps path; - if (start->compare(target) == 0) - return true; + { + tgba_run::steps path; + if (start->compare(target) == 0) + return true; - test_path s(a_, target, dead, h_); - const state* res = s.search(start->clone(), path); - if (res) - { - assert(res->compare(target) == 0); - return true; - } - else - { - state_set::const_iterator it; - for (it = s.get_seen().begin(); it != s.get_seen().end(); ++it) - dead.insert((*it)->clone()); - return false; - } - } + test_path s(a_, target, dead, h_); + const state* res = s.search(start->clone(), path); + if (res) + { + assert(res->compare(target) == 0); + return true; + } + else + { + state_set::const_iterator it; + for (it = s.get_seen().begin(); it != s.get_seen().end(); ++it) + dead.insert((*it)->clone()); + return false; + } + } typedef Sgi::hash_multimap m_source_trans; + state_ptr_hash, state_ptr_equal> m_source_trans; class min_path: public bfs_steps { @@ -486,140 +486,137 @@ namespace spot }; void construct_cycle(tgba_run* run, - const accepting_transitions_list& acc_trans) - { - assert(!acc_trans.empty()); - transition current = acc_trans.front(); - // insert the first accepting transition in the cycle - ndfsr_trace << "the initial accepting transition is from " - << a_->format_state(current.source) << " to " - << a_->format_state(current.dest) << std::endl; - const state* begin = current.source; + const accepting_transitions_list& acc_trans) + { + assert(!acc_trans.empty()); + transition current = acc_trans.front(); + // insert the first accepting transition in the cycle + ndfsr_trace << "the initial accepting transition is from " + << a_->format_state(current.source) << " to " + << a_->format_state(current.dest) << std::endl; + const state* begin = current.source; - m_source_trans target; - typename accepting_transitions_list::const_iterator i = - acc_trans.begin(); - ndfsr_trace << "targets are the source states: "; - for (++i; i!=acc_trans.end(); ++i) - { - if (i->source->compare(begin) == 0 && - i->source->compare(i->dest) == 0) - { - ndfsr_trace << "(self loop " << a_->format_state(i->source) - << " -> " << a_->format_state(i->dest) - << " ignored) "; - tgba_run::step st = { i->source->clone(), i->label, i->acc }; - run->cycle.push_back(st); - } - else - { - ndfsr_trace << a_->format_state(i->source) << " (-> " - << a_->format_state(i->dest) << ") "; - target.insert(std::make_pair(i->source, *i)); - } - } - ndfsr_trace << std::endl; + m_source_trans target; + typename accepting_transitions_list::const_iterator i = + acc_trans.begin(); + ndfsr_trace << "targets are the source states: "; + for (++i; i != acc_trans.end(); ++i) + { + if (i->source->compare(begin) == 0 && + i->source->compare(i->dest) == 0) + { + ndfsr_trace << "(self loop " << a_->format_state(i->source) + << " -> " << a_->format_state(i->dest) + << " ignored) "; + tgba_run::step st = { i->source->clone(), i->label, i->acc }; + run->cycle.push_back(st); + } + else + { + ndfsr_trace << a_->format_state(i->source) << " (-> " + << a_->format_state(i->dest) << ") "; + target.insert(std::make_pair(i->source, *i)); + } + } + ndfsr_trace << std::endl; - tgba_run::step st = { current.source->clone(), current.label, - current.acc }; - run->cycle.push_back(st); + tgba_run::step st = { current.source->clone(), current.label, + current.acc }; + run->cycle.push_back(st); - while (!target.empty()) - { - // find a minimal path from current.dest to any source state in - // target. - ndfsr_trace << "looking for a path from " - << a_->format_state(current.dest) << std::endl; - typename m_source_trans::iterator i = target.find(current.dest); - if (i == target.end()) - { - min_path s(a_, target, h_); - const state* res = s.search(current.dest->clone(), run->cycle); - // init current to the corresponding transition. - assert(res); - ndfsr_trace << a_->format_state(res) << " reached" << std::endl; - i = target.find(res); - assert(i != target.end()); - } - else - { - ndfsr_trace << "this is a target" << std::endl; - } - current = i->second; - // complete the path with the corresponding transition - tgba_run::step st = { current.source->clone(), current.label, - current.acc }; - run->cycle.push_back(st); - // remove this source state of target - target.erase(i); - } + while (!target.empty()) + { + // find a minimal path from current.dest to any source state in + // target. + ndfsr_trace << "looking for a path from " + << a_->format_state(current.dest) << std::endl; + typename m_source_trans::iterator i = target.find(current.dest); + if (i == target.end()) + { + min_path s(a_, target, h_); + const state* res = s.search(current.dest->clone(), run->cycle); + // init current to the corresponding transition. + assert(res); + ndfsr_trace << a_->format_state(res) << " reached" << std::endl; + i = target.find(res); + assert(i != target.end()); + } + else + { + ndfsr_trace << "this is a target" << std::endl; + } + current = i->second; + // complete the path with the corresponding transition + tgba_run::step st = { current.source->clone(), current.label, + current.acc }; + run->cycle.push_back(st); + // remove this source state of target + target.erase(i); + } - if (current.dest->compare(begin) != 0) - { - // close the cycle by adding a path from the destination of the - // last inserted transition to the source of the first one - ndfsr_trace << std::endl << "looking for a path from " - << a_->format_state(current.dest) << " to " - << a_->format_state(begin) << std::endl; - transition tmp; - target.insert(std::make_pair(begin, tmp)); - min_path s(a_, target, h_); - const state* res = s.search(current.dest->clone(), run->cycle); - assert(res); - assert(res->compare(begin) == 0); - (void)res; - } - } + if (current.dest->compare(begin) != 0) + { + // close the cycle by adding a path from the destination of the + // last inserted transition to the source of the first one + ndfsr_trace << std::endl << "looking for a path from " + << a_->format_state(current.dest) << " to " + << a_->format_state(begin) << std::endl; + transition tmp; + target.insert(std::make_pair(begin, tmp)); + min_path s(a_, target, h_); + const state* res = s.search(current.dest->clone(), run->cycle); + assert(res); + assert(res->compare(begin) == 0); + (void)res; + } + } void construct_prefix(tgba_run* run) - { - m_source_trans target; - transition tmp; + { + m_source_trans target; + transition tmp; + // Register all states from the cycle as target of the BFS. + for (tgba_run::steps::const_iterator i = run->cycle.begin(); + i != run->cycle.end(); ++i) + target.insert(std::make_pair(i->s, tmp)); - // Register all states from the cycle as target of the BFS. - for (tgba_run::steps::const_iterator i = run->cycle.begin(); - i != run->cycle.end(); ++i) - target.insert(std::make_pair(i->s, tmp)); + const state* prefix_start = a_->get_init_state(); + // There are two cases: either the initial state is already on + // the cycle, or it is not. If it is, we will have to rotate + // the cycle so it begins on this position. Otherwise we will shift + // the cycle so it begins on the state that follows the prefix. + // cycle_entry_point is that state. + const state* cycle_entry_point; + typename m_source_trans::const_iterator ps = target.find(prefix_start); + if (ps != target.end()) + { + // The initial state is on the cycle. + delete prefix_start; + cycle_entry_point = ps->first->clone(); + } + else + { + // This initial state is outside the cycle. Compute the prefix. + min_path s(a_, target, h_); + cycle_entry_point = s.search(prefix_start, run->prefix); + assert(cycle_entry_point); + cycle_entry_point = cycle_entry_point->clone(); + } - const state* prefix_start = a_->get_init_state(); - // There are two cases: either the initial state is already on - // the cycle, or it is not. If it is, we will have to rotate - // the cycle so it begins on this position. Otherwise we will shift - // the cycle so it begins on the state that follows the prefix. - // cycle_entry_point is that state. - const state* cycle_entry_point; - typename m_source_trans::const_iterator ps = target.find(prefix_start); - if (ps != target.end()) - { - // The initial state is on the cycle. - delete prefix_start; - cycle_entry_point = ps->first->clone(); - } - else - { - // This initial state is outside the cycle. Compute the prefix. - min_path s(a_, target, h_); - cycle_entry_point = s.search(prefix_start, run->prefix); - assert(cycle_entry_point); - cycle_entry_point = cycle_entry_point->clone(); - } - - // Locate cycle_entry_point on the cycle. - tgba_run::steps::iterator cycle_ep_it; - for (cycle_ep_it = run->cycle.begin(); - cycle_ep_it != run->cycle.end() - && cycle_entry_point->compare(cycle_ep_it->s); ++cycle_ep_it) - continue; - assert(cycle_ep_it != run->cycle.end()); - delete cycle_entry_point; - - // Now shift the cycle so it starts on cycle_entry_point. - run->cycle.splice(run->cycle.end(), run->cycle, - run->cycle.begin(), cycle_ep_it); - run->cycle.erase(run->cycle.begin(), cycle_ep_it); - } + // Locate cycle_entry_point on the cycle. + tgba_run::steps::iterator cycle_ep_it; + for (cycle_ep_it = run->cycle.begin(); + cycle_ep_it != run->cycle.end() + && cycle_entry_point->compare(cycle_ep_it->s); ++cycle_ep_it) + continue; + assert(cycle_ep_it != run->cycle.end()); + delete cycle_entry_point; + // Now shift the cycle so it starts on cycle_entry_point. + run->cycle.splice(run->cycle.end(), run->cycle, + run->cycle.begin(), cycle_ep_it); + } }; }