diff --git a/ChangeLog b/ChangeLog index 9a7dcd52a..ae2166f9f 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,10 @@ +2003-10-23 Alexandre Duret-Lutz + + * src/tgbaalgos/emptinesscheck.cc + (emptiness_check::tgba_emptiness_check): Do not print anything. + (emptiness_check::counter_example): Assume that tgba_emptiness_check + has already been called. + 2003-10-22 Alexandre Duret-Lutz * src/tgbaalgos/emptinesscheck.hh, src/tgbaalgos/emptinesscheck.cc diff --git a/src/tgbaalgos/emptinesscheck.cc b/src/tgbaalgos/emptinesscheck.cc index 6819a7564..ff23b3694 100644 --- a/src/tgbaalgos/emptinesscheck.cc +++ b/src/tgbaalgos/emptinesscheck.cc @@ -170,11 +170,8 @@ namespace spot comp.condition |= new_condition; if (aut_check->all_accepting_conditions() == comp.condition) { - // A failure SCC is find, the automata is not empty. - // spot::bdd_print_dot(std::cout, aut_check->get_dict(), - // comp.condition); + // A failure SCC was found, the automata is not empty. root_component.push(comp); - std::cout << "CONSISTENT AUTOMATA" << std::endl; return false; } root_component.push(comp); @@ -183,7 +180,6 @@ namespace spot } } // The automata is empty. - std::cout << "EMPTY LANGUAGE" << std::endl; return true; } @@ -197,7 +193,7 @@ namespace spot os << "======================" << std::endl; const bdd_dict* d = aut->get_dict(); for (state_sequence::const_iterator i_se = suffix.begin(); - i_se != suffix.end(); i_se++) + i_se != suffix.end(); ++i_se) { if (restrict) { @@ -213,7 +209,7 @@ namespace spot os << "Cycle:" < path_state; path_state path_map; - if (!root_component.empty()) + assert(!root_component.empty()); + + int comp_size = root_component.size(); + typedef std::vector vec_compo; + vec_compo vec_component; + vec_component.resize(comp_size); + vec_sequence.resize(comp_size); + state_sequence seq; + state_sequence tmp_lst; + state_sequence best_lst; + bdd tmp_acc = bddfalse; + std::stack todo_accept; + + for (int j = comp_size - 1; j >= 0; j--) { - int comp_size = root_component.size(); - typedef std::vector vec_compo; - vec_compo vec_component; - vec_component.resize(comp_size); - vec_sequence.resize(comp_size); - state_sequence seq; - state_sequence tmp_lst; - state_sequence best_lst; - bdd tmp_acc = bddfalse; - std::stack todo_accept; + vec_component[j] = root_component.top(); + root_component.pop(); + } - for (int j = comp_size -1; j >= 0; j--) + int q_index; + int tmp_int = 0; + // Fill the SCC in the stack root_component. + for (seen::iterator iter_map = seen_state_num.begin(); + iter_map != seen_state_num.end(); ++iter_map) + { + q_index = (*iter_map).second; + tmp_int = 0; + if (q_index > 0) { - vec_component[j] = root_component.top(); - root_component.pop(); + while ((tmp_int < comp_size) + && (vec_component[tmp_int].index <= q_index)) + tmp_int = tmp_int+1; + if (tmp_int < comp_size) + vec_component[tmp_int - 1].state_set.insert((*iter_map).first); + else + vec_component[comp_size - 1].state_set.insert((*iter_map).first); } + } - int q_index; - int tmp_int = 0; - // Fill the SCC in the stack root_component. - for (seen::iterator iter_map = seen_state_num.begin(); - iter_map != seen_state_num.end(); iter_map++) + state* start_state = aut_counter->get_init_state(); + if (comp_size != 1) + { + tgba_succ_iterator* i = aut_counter->succ_iter(start_state); + todo_trace.push_back(pair_state_iter(start_state, i)); + + for (int k = 0; k < comp_size - 1; ++k) { - q_index = (*iter_map).second; - tmp_int = 0; - if (q_index > 0) + // We build a path trought all SCC in the stack: a + // possible prefix for a counter example. + while (!todo_trace.empty()) { - while ((tmp_int < comp_size) - && (vec_component[tmp_int].index <= q_index)) - tmp_int = tmp_int+1; - if (tmp_int < comp_size) - vec_component[tmp_int-1].state_set.insert((*iter_map).first); - else - vec_component[comp_size-1].state_set - .insert((*iter_map).first); - } - } + pair_state_iter started_from = todo_trace.front(); + todo_trace.pop_front(); + started_from.second->first(); - state* start_state = aut_counter->get_init_state(); - if (comp_size != 1) - { - tgba_succ_iterator* i = aut_counter->succ_iter(start_state); - todo_trace.push_back(pair_state_iter(start_state, i)); - - for (int k = 0; k < comp_size-1; k++) - { - // We build a path trought all SCC in the stack: a - // possible prefix for a counter example. - while (!todo_trace.empty()) + for (started_from.second->first(); + !started_from.second->done(); + started_from.second->next()) { - pair_state_iter started_from = todo_trace.front(); - todo_trace.pop_front(); - started_from.second->first(); - - for (started_from.second->first(); - !started_from.second->done(); - started_from.second->next()) + const state* curr_state = + started_from.second->current_state(); + connected_component::set_of_state::iterator iter_set = + vec_component[k+1].state_set.find(curr_state); + if (iter_set != vec_component[k+1].state_set.end()) { - const state* curr_state = - started_from.second->current_state(); - connected_component::set_of_state::iterator iter_set = - vec_component[k+1].state_set.find(curr_state); - if (iter_set != vec_component[k+1].state_set.end()) + const state* curr_father = started_from.first; + seq.push_front(*iter_set); + seq.push_front(curr_father); + seen::iterator i_2 = + seen_state_num.find(curr_father); + assert(i_2 != seen_state_num.end()); + while ((vec_component[k].index + < seen_state_num[curr_father]) + && (seen_state_num[curr_father] != 1)) { - const state* curr_father = started_from.first; - seq.push_front(*iter_set); - seq.push_front(curr_father); - seen::iterator i_2 = + seq.push_front(path_map[curr_father]); + curr_father = path_map[curr_father]; + seen::iterator i_3 = seen_state_num.find(curr_father); - assert(i_2 != seen_state_num.end()); - while ((vec_component[k].index - < seen_state_num[curr_father]) - && (seen_state_num[curr_father] != 1)) - { - seq.push_front(path_map[curr_father]); - curr_father = path_map[curr_father]; - seen::iterator i_3 = - seen_state_num.find(curr_father); - assert(i_3 != seen_state_num.end()); - } - vec_sequence[k] = seq; - seq.clear(); - todo_trace.clear(); - break; + assert(i_3 != seen_state_num.end()); } - else + vec_sequence[k] = seq; + seq.clear(); + todo_trace.clear(); + break; + } + else + { + connected_component::set_of_state::iterator i_s = + vec_component[k].state_set.find(curr_state); + if (i_s != vec_component[k].state_set.end()) { - connected_component::set_of_state::iterator i_s = - vec_component[k].state_set.find(curr_state); - if (i_s != vec_component[k].state_set.end()) - { - path_state::iterator i_path = - path_map.find(curr_state); - seen::iterator i_seen = - seen_state_num.find(curr_state); + path_state::iterator i_path = + path_map.find(curr_state); + seen::iterator i_seen = + seen_state_num.find(curr_state); - if (i_seen != seen_state_num.end() - && seen_state_num[curr_state] > 0 - && i_path == path_map.end()) - { - todo_trace. - push_back(pair_state_iter(curr_state, - aut_counter->succ_iter(curr_state))); - path_map[curr_state] = started_from.first; - } + if (i_seen != seen_state_num.end() + && seen_state_num[curr_state] > 0 + && i_path == path_map.end()) + { + todo_trace. + push_back(pair_state_iter(curr_state, + aut_counter->succ_iter(curr_state))); + path_map[curr_state] = started_from.first; } } } } - todo_trace. - push_back(pair_state_iter(vec_sequence[k].back(), - aut_counter->succ_iter(vec_sequence[k].back()))); } + todo_trace. + push_back(pair_state_iter(vec_sequence[k].back(), + aut_counter->succ_iter(vec_sequence[k].back()))); } - else - { - suffix.push_front(start_state); - } - for (int n_ = 0; n_ < comp_size-1; n_++) - { - for (state_sequence::iterator it = vec_sequence[n_].begin(); - it != vec_sequence[n_].end(); it++) - { - suffix.push_back(*it); - } - } - suffix.unique(); - emptiness_check::accepting_path(aut_counter, - vec_component[comp_size-1], - suffix.back(), - vec_component[comp_size-1].condition); } else { - std::cout << "EMPTY LANGUAGE NO COUNTER EXEMPLE" << std::endl; + suffix.push_front(start_state); } + for (int n_ = 0; n_ < comp_size - 1; ++n_) + for (state_sequence::iterator it = vec_sequence[n_].begin(); + it != vec_sequence[n_].end(); ++it) + suffix.push_back(*it); + suffix.unique(); + emptiness_check::accepting_path(aut_counter, + vec_component[comp_size - 1], + suffix.back(), + vec_component[comp_size - 1].condition); } /// \brief complete the path build by accepting_path to get the period. @@ -450,7 +436,7 @@ namespace spot std::stack todo_path; tgba_succ_iterator* t_s_i = aut_counter->succ_iter(start_path); t_s_i->first(); - todo_path.push(triplet(pair_state_iter(start_path,t_s_i), bddfalse)); + todo_path.push(triplet(pair_state_iter(start_path, t_s_i), bddfalse)); bdd tmp_acc = bddfalse; bdd best_acc = bddfalse; cycle_path tmp_lst; @@ -460,11 +446,11 @@ namespace spot while (!todo_path.empty()) { triplet step_ = todo_path.top(); - tgba_succ_iterator* iter_ = (step_.first).second; + tgba_succ_iterator* iter_ = step_.first.second; if (iter_->done()) { todo_path.pop(); - seen_priority.erase((step_.first).first); + seen_priority.erase(step_.first.first); tmp_lst.pop_back(); } else @@ -504,9 +490,6 @@ namespace spot { cycle_path tmp(tmp_lst); best_lst = tmp; - spot::bdd_print_dot(std::cout, - aut_counter->get_dict(), - step_.second); } } else @@ -537,7 +520,7 @@ namespace spot } } for (cycle_path::iterator it = best_lst.begin(); - it != best_lst.end(); it++) + it != best_lst.end(); ++it) emptiness_check::period.push_back(*it); if (best_acc != to_accept)