From 558642fe9c54ee830c37baa022cb62a452f2f3a3 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 22 Oct 2003 14:33:12 +0000 Subject: [PATCH] * src/tgbaalgos/emptinesscheck.cc, src/tgbaalgos/emptinesscheck.hh: Reindent. (emptiness_check::~emptiness_check, emptiness_check::emptiness_check): Remove, unused. --- ChangeLog | 7 + src/tgbaalgos/emptinesscheck.cc | 610 +++++++++++++++++--------------- src/tgbaalgos/emptinesscheck.hh | 133 +++---- 3 files changed, 382 insertions(+), 368 deletions(-) diff --git a/ChangeLog b/ChangeLog index 583dabc94..6cf9e3d86 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,10 @@ +2003-10-22 Alexandre Duret-Lutz + + * src/tgbaalgos/emptinesscheck.cc, src/tgbaalgos/emptinesscheck.hh: + Reindent. + (emptiness_check::~emptiness_check, emptiness_check::emptiness_check): + Remove, unused. + 2003-10-15 Alexandre Duret-Lutz * iface/gspn/ltlgspn.cc (main): Allow invocations with diff --git a/src/tgbaalgos/emptinesscheck.cc b/src/tgbaalgos/emptinesscheck.cc index 0e71b1cb0..bb0e6fc0b 100644 --- a/src/tgbaalgos/emptinesscheck.cc +++ b/src/tgbaalgos/emptinesscheck.cc @@ -22,55 +22,48 @@ namespace spot { connected_component::connected_component() { - index = 0; - condition = bddfalse; - transition_acc = -1; - nb_transition = 0; - nb_state = 1; - not_null = false; + index = 0; + condition = bddfalse; + transition_acc = -1; + nb_transition = 0; + nb_state = 1; + not_null = false; } - connected_component::connected_component(int i, bdd a) - { - index = i; - condition = a; - transition_acc = -1; - nb_transition = 0; - nb_state = 1; - not_null = false; - } + connected_component::connected_component(int i, bdd a) + { + index = i; + condition = a; + transition_acc = -1; + nb_transition = 0; + nb_state = 1; + not_null = false; + } connected_component::~connected_component() { } - std::string - connected_component::to_string_component() - { - return "+ index + condition + nbTransition + transitionCondition + notNull +"; - } - bool connected_component::isAccepted(tgba* aut) { return aut->all_accepting_conditions() == condition; } - /// \brief Remove all the nodes accessible from the given node start_delete. - /// - /// The removed graphe is the subgraphe containing nodes store - ///intable state_map with order -1. - + /// \brief Remove all the nodes accessible from the given node start_delete. + /// + /// The removed graph is the subgraph containing nodes stored + /// in table state_map with order -1. void - emptiness_check::remove_component(const tgba& aut, seen& state_map, const spot::state* start_delete) - { - + emptiness_check::remove_component(const tgba& aut, seen& state_map, + const spot::state* start_delete) + { std::stack to_remove; state_map[start_delete] = -1; tgba_succ_iterator* iter_delete = aut.succ_iter(start_delete); iter_delete->first(); to_remove.push(iter_delete); - while (!to_remove.empty()) + while (!to_remove.empty()) { tgba_succ_iterator* succ_delete = to_remove.top(); to_remove.pop(); @@ -88,20 +81,12 @@ namespace spot } } } - } + } - emptiness_check::~emptiness_check() - { - } - -emptiness_check::emptiness_check() - { - } - - /// \brief On-the-fly emptiness check. - /// - /// The algorithm used here is adapted from Jean-Michel Couvreur's - /// Probataf tool. + /// \brief On-the-fly emptiness check. + /// + /// The algorithm used here is adapted from Jean-Michel Couvreur's + /// Probataf tool. bool emptiness_check::tgba_emptiness_check(const spot::tgba* aut_check) { @@ -110,11 +95,11 @@ emptiness_check::emptiness_check() state* init = aut_check->get_init_state(); seen_state_num[init] = 1; root_component.push(spot::connected_component(1,bddfalse)); - arc_accepting.push(bddfalse); + arc_accepting.push(bddfalse); tgba_succ_iterator* iter_ = aut_check->succ_iter(init); iter_->first(); todo.push(pair_state_iter(init, iter_ )); - while (!todo.empty()) + while (!todo.empty()) { pair_state_iter step = todo.top(); if ((step.second)->done()) @@ -123,12 +108,14 @@ emptiness_check::emptiness_check() assert(!root_component.empty()); connected_component comp_tmp = root_component.top(); root_component.pop(); - seen::iterator i_0 = seen_state_num.find(step.first); - assert(i_0 != seen_state_num.end()); + seen::iterator i_0 = seen_state_num.find(step.first); + assert(i_0 != seen_state_num.end()); if (comp_tmp.index == seen_state_num[step.first]) { /// The current node is a root of a Strong Connected Component. - spot::emptiness_check::remove_component(*aut_check, seen_state_num, step.first); + spot::emptiness_check::remove_component(*aut_check, + seen_state_num, + step.first); assert(!arc_accepting.empty()); arc_accepting.pop(); assert(root_component.size() == arc_accepting.size()); @@ -148,9 +135,9 @@ emptiness_check::emptiness_check() iter_->next(); if (i == seen_state_num.end()) { - /// New node. + // New node. nbstate = nbstate + 1; - assert(nbstate != 0); + assert(nbstate != 0); seen_state_num[current_state] = nbstate; root_component.push(connected_component(nbstate, bddfalse)); arc_accepting.push(current_accepting); @@ -160,33 +147,39 @@ emptiness_check::emptiness_check() } else if (seen_state_num[current_state] != -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()); connected_component comp = root_component.top(); root_component.pop(); bdd new_condition = bddfalse; - new_condition = bdd_apply(new_condition, current_accepting, bddop_or); - new_condition = bdd_apply(new_condition, comp.condition, bddop_or); + new_condition = bdd_apply(new_condition, current_accepting, + bddop_or); + new_condition = bdd_apply(new_condition, comp.condition, + bddop_or); int current_index = seen_state_num[current_state]; while (comp.index > current_index) { - /// root_component and arc_accepting are popped - /// until the head of root_component is less or - /// equal to the order of the current state. + // root_component and arc_accepting are popped + // until the head of root_component is less or + // equal to the order of the current state. assert(!root_component.empty()); comp = root_component.top(); root_component.pop(); - new_condition = bdd_apply(new_condition,comp.condition, bddop_or); + new_condition = bdd_apply(new_condition,comp.condition, + bddop_or); assert(!arc_accepting.empty()); bdd arc_acc = arc_accepting.top(); arc_accepting.pop(); - new_condition = bdd_apply(new_condition, arc_acc, bddop_or); + new_condition = bdd_apply(new_condition, arc_acc, + bddop_or); } - comp.condition = bdd_apply(comp.condition, new_condition, bddop_or); + comp.condition = bdd_apply(comp.condition, new_condition, + bddop_or); 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 is find, the automata is not empty. + // spot::bdd_print_dot(std::cout, aut_check->get_dict(), + // comp.condition); root_component.push(comp); std::cout << "CONSISTENT AUTOMATA" << std::endl; return false; @@ -196,232 +189,264 @@ emptiness_check::emptiness_check() } } } - /// The automata is empty. - std::cout << "EMPTY LANGUAGE" << std::endl; + // The automata is empty. + std::cout << "EMPTY LANGUAGE" << std::endl; return true; } -std::ostream& - emptiness_check::print_result(std::ostream& os, const spot::tgba* aut, const tgba* restrict ) const + std::ostream& + emptiness_check::print_result(std::ostream& os, const spot::tgba* aut, + const tgba* restrict) const { os << "======================" << std::endl; os << "Prefix:" << std::endl; os << "======================" << std::endl; - const bdd_dict* d = aut->get_dict(); - for (state_sequence::const_iterator i_se = seq_counter.begin(); i_se != seq_counter.end(); i_se++) - { - if (restrict) - { - os << "*****Projected STATE :" << restrict->format_state(aut->project_state((*i_se), restrict)) << "*****" << std::endl; - } - else - { - os << "*****print STATE :" << aut->format_state((*i_se)) << "*****" << std::endl; - } - } - os << "======================" << std::endl; - os << "Cycle:" <format_state(aut->project_state((*it).first, restrict)) << "*****" << std::endl; - } - else - { - os << " | " << bdd_format_set(d, (*it).second) <format_state((*it).first) << "*****" << std::endl; - } - } - return os; - } - - /// \brief Build a possible prefixe and period for a counter example. - void - emptiness_check::counter_example(const spot::tgba* aut_counter) - { - std::deque todo_trace; - typedef std::map path_state; - path_state path_map; - - if (!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--) + const bdd_dict* d = aut->get_dict(); + for (state_sequence::const_iterator i_se = seq_counter.begin(); + i_se != seq_counter.end(); i_se++) + { + if (restrict) { - vec_component[j] = root_component.top(); - root_component.pop(); - } - - 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) - { - 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); - } - } - } - - state* start_state = aut_counter->get_init_state(); - if (comp_size != 1) - { - todo_trace.push_back(pair_state_iter(start_state, aut_counter->succ_iter(start_state))); - - for (int k = 0; k < comp_size-1; k++) - { - /// We build a path trought all SCC in the stack : a - ///possible prefixe for a counter example. - while (!todo_trace.empty()) - { - 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_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)) - { - 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; - } - - 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()) - { - 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; - } - } - } - } - } - todo_trace.push_back(pair_state_iter(vec_sequence[k].back(), aut_counter->succ_iter(vec_sequence[k].back()))); - } + os << restrict->format_state(aut->project_state((*i_se), restrict)) + << std::endl; } else { - seq_counter.push_front(start_state); + os << aut->format_state((*i_se)) << std::endl; } - for (int n_ = 0; n_ < comp_size-1; n_++) - { - for (state_sequence::iterator it = vec_sequence[n_].begin(); it != vec_sequence[n_].end(); it++) + } + os << "======================" << std::endl; + os << "Cycle:" <format_state(aut->project_state((*it).first, + restrict)) + << std::endl; + } + else + { + os << " | " << bdd_format_set(d, (*it).second) <format_state((*it).first) << std::endl; + } + } + return os; + } + + /// \brief Build a possible prefixe and period for a counter example. + void + emptiness_check::counter_example(const spot::tgba* aut_counter) + { + std::deque todo_trace; + typedef std::map path_state; + path_state path_map; + + if (!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--) + { + vec_component[j] = root_component.top(); + root_component.pop(); + } + + 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) + { + 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); + } + } + + 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 prefixe for a counter example. + while (!todo_trace.empty()) + { + 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_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)) + { + 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; + } + 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()) + { + 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; + } + } + } + } + } + todo_trace. + push_back(pair_state_iter(vec_sequence[k].back(), + aut_counter->succ_iter(vec_sequence[k].back()))); + } + } + else + { + seq_counter.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++) { seq_counter.push_back(*it); } - } - seq_counter.unique(); - emptiness_check::accepting_path(aut_counter, vec_component[comp_size-1], seq_counter.back(),vec_component[comp_size-1].condition); - } - else - { - std::cout << "EMPTY LANGUAGE NO COUNTER EXEMPLE" << std::endl; } + seq_counter.unique(); + emptiness_check::accepting_path(aut_counter, vec_component[comp_size-1], seq_counter.back(),vec_component[comp_size-1].condition); } + else + { + std::cout << "EMPTY LANGUAGE NO COUNTER EXEMPLE" << std::endl; + } + } - /// \brief complete the path build by accepting_path to get the - ///period (cycle). - void - emptiness_check::complete_cycle(const spot::tgba* aut_counter, const connected_component& comp_path, const state* from_state,const state* to_state) - { - if (seen_state_num[from_state] != seen_state_num[to_state]) - { - std::map complete_map; - std::deque todo_complete; - spot::tgba_succ_iterator* ite = aut_counter->succ_iter(from_state); - todo_complete.push_back(pair_state_iter(from_state, ite)); - cycle_path tmp_comp; - while(!todo_complete.empty()) - { - pair_state_iter started_ = todo_complete.front(); - todo_complete.pop_front(); - tgba_succ_iterator* iter_s = started_.second; - iter_s->first(); - for (iter_s->first(); !iter_s->done(); iter_s->next()) - { - const state* curr_state = (started_.second)->current_state(); - connected_component::set_of_state::iterator i_set = comp_path.state_set.find(curr_state); - if (i_set != comp_path.state_set.end()) - { - if (curr_state->compare(to_state) == 0) - { - const state* curr_father = started_.first; - bdd curr_condition = iter_s->current_condition(); - tmp_comp.push_front(state_proposition(curr_state, curr_condition)); - while (curr_father->compare(from_state) != 0) - { - tmp_comp.push_front(state_proposition(curr_father, complete_map[curr_father].second)); - curr_father = complete_map[curr_father].first; - } - emptiness_check::periode.splice(periode.end(), tmp_comp); - todo_complete.clear(); - break; - } - else - { - todo_complete.push_back(pair_state_iter(curr_state, aut_counter->succ_iter(curr_state))); - complete_map[curr_state] = state_proposition(started_.first, iter_s->current_condition()); - } - } - } - } - } - } + /// \brief complete the path build by accepting_path to get the period. + void + emptiness_check::complete_cycle(const spot::tgba* aut_counter, + const connected_component& comp_path, + const state* from_state, + const state* to_state) + { + if (seen_state_num[from_state] != seen_state_num[to_state]) + { + std::map complete_map; + std::deque todo_complete; + spot::tgba_succ_iterator* ite = aut_counter->succ_iter(from_state); + todo_complete.push_back(pair_state_iter(from_state, ite)); + cycle_path tmp_comp; + while(!todo_complete.empty()) + { + pair_state_iter started_ = todo_complete.front(); + todo_complete.pop_front(); + tgba_succ_iterator* iter_s = started_.second; + iter_s->first(); + for (iter_s->first(); !iter_s->done(); iter_s->next()) + { + const state* curr_state = (started_.second)->current_state(); + connected_component::set_of_state::iterator i_set = + comp_path.state_set.find(curr_state); + if (i_set != comp_path.state_set.end()) + { + if (curr_state->compare(to_state) == 0) + { + const state* curr_father = started_.first; + bdd curr_condition = iter_s->current_condition(); + tmp_comp.push_front(state_proposition(curr_state, curr_condition)); + while (curr_father->compare(from_state) != 0) + { + tmp_comp.push_front(state_proposition(curr_father, + complete_map[curr_father].second)); + curr_father = complete_map[curr_father].first; + } + emptiness_check::periode.splice(periode.end(), + tmp_comp); + todo_complete.clear(); + break; + } + else + { + todo_complete.push_back(pair_state_iter(curr_state, + aut_counter->succ_iter(curr_state))); + complete_map[curr_state] = + state_proposition(started_.first, + iter_s->current_condition()); + } + } + } + } + } + } - /// \Brief build recursively a path in the accepting SCC to get - ///all accepting conditions. This path is the first part of the - ///period. -void - emptiness_check::accepting_path(const spot::tgba* aut_counter, const connected_component& comp_path, const spot::state* start_path, bdd to_accept) + /// \Brief build recursively a path in the accepting SCC to get + /// all accepting conditions. This path is the first part of the + /// period. + void + emptiness_check::accepting_path(const spot::tgba* aut_counter, + const connected_component& comp_path, + const spot::state* start_path, bdd to_accept) { seen seen_priority; std::stack todo_path; @@ -447,18 +472,24 @@ void else { state* curr_state = iter_->current_state(); - connected_component::set_of_state::iterator it_set = comp_path.state_set.find(curr_state); + connected_component::set_of_state::iterator it_set = + comp_path.state_set.find(curr_state); if (it_set != comp_path.state_set.end()) { seen::iterator i = seen_priority.find(curr_state); if (i == seen_priority.end()) { - tgba_succ_iterator* c_iter = aut_counter->succ_iter(curr_state); - bdd curr_bdd = bdd_apply(iter_->current_accepting_conditions(), step_.second, bddop_or); - c_iter->first(); - todo_path.push(triplet(pair_state_iter(curr_state, c_iter), curr_bdd)); - tmp_lst.push_back(state_proposition(curr_state, iter_->current_condition())); - seen_priority[curr_state] = seen_state_num[curr_state]; + tgba_succ_iterator* c_iter = + aut_counter->succ_iter(curr_state); + bdd curr_bdd = + bdd_apply(iter_->current_accepting_conditions(), + step_.second, bddop_or); + c_iter->first(); + todo_path.push(triplet(pair_state_iter(curr_state, c_iter), + curr_bdd)); + tmp_lst.push_back(state_proposition(curr_state, + iter_->current_condition())); + seen_priority[curr_state] = seen_state_num[curr_state]; } else { @@ -476,16 +507,19 @@ void { cycle_path tmp(tmp_lst); best_lst = tmp; - spot::bdd_print_dot(std::cout, aut_counter->get_dict(),step_.second); + spot::bdd_print_dot(std::cout, + aut_counter->get_dict(), + step_.second); } } else { - if (bddtrue == bdd_apply(best_in, curr_in, bddop_imp)) + if (bddtrue == bdd_apply(best_in, curr_in, + bddop_imp)) { - cycle_path tmp(tmp_lst); - best_lst = tmp; - best_acc = tmp_acc; + cycle_path tmp(tmp_lst); + best_lst = tmp; + best_acc = tmp_acc; } } } @@ -494,7 +528,8 @@ void bdd last_ = iter_->current_accepting_conditions(); bdd prop_ = iter_->current_condition(); tmp_acc = bdd_apply(last_, step_.second, bddop_or); - tmp_lst.push_back(state_proposition(curr_state, prop_)); + tmp_lst.push_back(state_proposition(curr_state, + prop_)); cycle_path tmp(tmp_lst); best_lst = tmp; best_acc = tmp_acc; @@ -503,17 +538,17 @@ void } } iter_->next(); - } } - for (cycle_path::iterator it = best_lst.begin(); it != best_lst.end(); it++) - { - emptiness_check::periode.push_back(*it); - } + for (cycle_path::iterator it = best_lst.begin(); + it != best_lst.end(); it++) + emptiness_check::periode.push_back(*it); + if (best_acc != to_accept) { bdd rec_to_acc = bdd_apply(to_accept, !best_acc, bddop_and); - emptiness_check::accepting_path(aut_counter, comp_path, periode.back().first, rec_to_acc); + emptiness_check::accepting_path(aut_counter, comp_path, + periode.back().first, rec_to_acc); } else { @@ -522,7 +557,8 @@ void { /// The path contains all accepting conditions. Then we ///complete the cycle in this SCC by calling complete_cycle. - complete_cycle(aut_counter, comp_path, periode.back().first, seq_counter.back()); + complete_cycle(aut_counter, comp_path, periode.back().first, + seq_counter.back()); } } } diff --git a/src/tgbaalgos/emptinesscheck.hh b/src/tgbaalgos/emptinesscheck.hh index 7f5dda417..f986e5511 100644 --- a/src/tgbaalgos/emptinesscheck.hh +++ b/src/tgbaalgos/emptinesscheck.hh @@ -1,6 +1,5 @@ #ifndef SPOT_EMPTINESS_CHECK_HH # define SPOT_EMPTINESS_CHECK_HH -//#include "tgba/bddfactory.hh" #include "tgba/tgba.hh" #include "tgba/statebdd.hh" #include "tgba/tgbabddfactory.hh" @@ -14,31 +13,28 @@ #include #include - /// \brief Emptiness check on spot::tgba namespace spot { class connected_component { - /// During the Depth path we keep the connected component that we met. + // During the Depth path we keep the connected component that we met. public: connected_component(); connected_component(int i, bdd a); - virtual - ~connected_component(); - std::string - to_string_component(); - bool - isAccepted(tgba* aut); + virtual ~connected_component(); + bool isAccepted(tgba* aut); public: int index; /// The bdd condition is the union of all accepting condition of /// transitions which connect the states of the connected component. bdd condition; - typedef std::set set_of_state; + typedef std::set set_of_state; + /// for the counter example we need to know all the states of the - ///component + /// component set_of_state state_set; int transition_acc; int nb_transition; @@ -48,99 +44,74 @@ namespace spot class emptiness_check { - typedef std::pair pair_state_iter; typedef std::pair triplet; - typedef std::map seen; + typedef std::map seen; typedef std::list state_sequence; typedef std::pair state_proposition; typedef std::list cycle_path; public: - -virtual - ~emptiness_check(); - - emptiness_check(); - /// this function remove all accessible state from a given /// state. In other words, it removes the strongly connected /// component that contents this state. - /// \brief Emptiness check on spot::tgba + + /// \brief Emptiness check on spot::tgba void - remove_component(const tgba& aut, seen& state_map, const spot::state* start_delete); + remove_component(const tgba& aut, seen& state_map, + const spot::state* start_delete); - /// This is based on the following papers. - /// \verbatim - /// @InProceedings{ couvreur.00.lacim, - /// author = {Jean-Michel Couvreur}, - /// title = {Un point de vue symbolique sur la logique temporelle - /// lin{\'e}aire}, - /// booktitle = {Actes du Colloque LaCIM 2000}, - /// month = {August}, - /// year = {2000}, - /// pages = {131--140}, - /// volume = {27}, - /// series = {Publications du LaCIM}, - /// publisher = {Universit{\'e} du Qu{\'e}bec {\`a} Montr{\'e}al}, - /// editor = {Pierre Leroux} - /// } - /// \endverbatim - /// and - /// \verbatim - /// @InProceedings{couvreur.99.fm, - /// author = {Jean-Michel Couvreur}, - /// title = {On-the-fly Verification of Temporal Logic}, - /// pages = {253--271}, - /// editor = {Jeannette M. Wing and Jim Woodcock and Jim Davies}, - /// booktitle = {Proceedings of the World Congress on Formal Methods in the - /// Development of Computing Systems (FM'99)}, - /// publisher = {Springer-Verlag}, - /// series = {Lecture Notes in Computer Science}, - /// volume = {1708}, - /// year = {1999}, - /// address = {Toulouse, France}, - /// month = {September}, - /// isbn = {3-540-66587-0} - /// } - /// \endverbatim - /// This function return true if the automata is empty and build a stack of SCC. - bool - tgba_emptiness_check(const spot::tgba* aut_check); + /// This function returns true if the automata's language is empty, + /// and builds a stack of SCC. + /// + /// This is based on the following paper. + /// \verbatim + /// @InProceedings{couvreur.99.fm, + /// author = {Jean-Michel Couvreur}, + /// title = {On-the-fly Verification of Temporal Logic}, + /// pages = {253--271}, + /// editor = {Jeannette M. Wing and Jim Woodcock and Jim Davies}, + /// booktitle = {Proceedings of the World Congress on Formal Methods in + /// the Development of Computing Systems (FM'99)}, + /// publisher = {Springer-Verlag}, + /// series = {Lecture Notes in Computer Science}, + /// volume = {1708}, + /// year = {1999}, + /// address = {Toulouse, France}, + /// month = {September}, + /// isbn = {3-540-66587-0} + /// } + /// \endverbatim + bool tgba_emptiness_check(const spot::tgba* aut_check); - /// counter_example check if the automata is empty. If it is not, - ///then this function return an accepted word (a trace) and an accepted sequence. + /// Compute a counter example if tgba_emptiness_check() returned false. + void counter_example(const spot::tgba* aut_counter); - void - counter_example(const spot::tgba* aut_counter); + std::ostream& print_result(std::ostream& os, const spot::tgba* aut, + const tgba* restrict = 0) const; -std::ostream& - print_result(std::ostream& os, const spot::tgba* aut, const tgba* restrict = 0) const; - - - std::stack arc_accepting; - std::stack root_component; + std::stack arc_accepting; + std::stack root_component; seen seen_state_num; state_sequence seq_counter; cycle_path periode; private: - std::stack todo; + std::stack todo; std::vector vec_sequence; - /// This function is called by counter_example to find a path - /// which contents all accepting conditions in the accepted SCC (get all the - /// accepting conditions). + + /// Called by counter_example to find a path which traverses all + /// accepting conditions in the accepted SCC. void - accepting_path (const spot::tgba* aut_counter, const connected_component& comp_path, const spot::state* start_path, bdd to_accept); - - - /// This function is called by counter_example (after - //accepting_path) to complete the cycle that caraterise the periode - //of the counter example. Append a sequence to the path given by accepting_path. - void - complete_cycle(const spot::tgba* aut_counter, const connected_component& comp_path, const state* from_state,const state* to_state); - + accepting_path (const spot::tgba* aut_counter, + const connected_component& comp_path, + const spot::state* start_path, bdd to_accept); + /// Complete a cycle that caraterise the period of the counter + /// example. Append a sequence to the path given by accepting_path. + void complete_cycle(const spot::tgba* aut_counter, + const connected_component& comp_path, + const state* from_state,const state* to_state); }; } #endif // SPOT_EMPTINESS_CHECK_HH