From 7f3c113130b1a9b5545160250c04b271a4018906 Mon Sep 17 00:00:00 2001 From: rebiha Date: Thu, 25 Sep 2003 15:12:44 +0000 Subject: [PATCH] * src/tgbatest/emptinesscheckexplicit.test (acc): New file. * src/tgbatest/emptinesscheckexplicit.cc (main): New file. * src/tgbatest/emptinesscheck.test: New file. * src/tgbatest/emptinesscheck.cc (main): New file. * src/tgbaalgos/emptinesscheck.cc (spot): New method. * src/tgbaalgos/emptinesscheck.hh: New interface. --- ChangeLog | 14 + src/tgbaalgos/Makefile.am | 2 + src/tgbaalgos/emptinesscheck.cc | 578 +++++++++++++++++++++++ src/tgbaalgos/emptinesscheck.hh | 139 ++++++ src/tgbatest/Makefile.am | 6 + src/tgbatest/emptinesscheck.cc | 145 ++++++ src/tgbatest/emptinesscheck.test | 20 + src/tgbatest/emptinesscheckexplicit.cc | 46 ++ src/tgbatest/emptinesscheckexplicit.test | 14 + 9 files changed, 964 insertions(+) create mode 100644 src/tgbaalgos/emptinesscheck.cc create mode 100644 src/tgbaalgos/emptinesscheck.hh create mode 100644 src/tgbatest/emptinesscheck.cc create mode 100755 src/tgbatest/emptinesscheck.test create mode 100644 src/tgbatest/emptinesscheckexplicit.cc create mode 100755 src/tgbatest/emptinesscheckexplicit.test diff --git a/ChangeLog b/ChangeLog index fbcefcf2c..1e0f416dc 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,17 @@ +2003-09-25 Rachid REBIHA + + * src/tgbatest/emptinesscheckexplicit.test (acc): New file. + + * src/tgbatest/emptinesscheckexplicit.cc (main): New file. + + * src/tgbatest/emptinesscheck.test: New file. + + * src/tgbatest/emptinesscheck.cc (main): New file. + + * src/tgbaalgos/emptinesscheck.cc (spot): New method. + + * src/tgbaalgos/emptinesscheck.hh: New interface. + 2003-09-22 Alexandre Duret-Lutz * src/tgbaalgos/ltl2tgba.cc, src/tgbaalgos/ltl2tgba.hh: Rename as ... diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index b3a87b68e..2eb5877b5 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -10,6 +10,7 @@ tgbaalgos_HEADERS = \ ltl2tgba_fm.hh \ ltl2tgba_lacim.hh \ magic.hh \ + emptinesscheck.hh \ save.hh noinst_LTLIBRARIES = libtgbaalgos.la @@ -20,4 +21,5 @@ libtgbaalgos_la_SOURCES = \ ltl2tgba_fm.cc \ ltl2tgba_lacim.cc \ magic.cc \ + emptinesscheck.cc \ save.cc diff --git a/src/tgbaalgos/emptinesscheck.cc b/src/tgbaalgos/emptinesscheck.cc new file mode 100644 index 000000000..b834c0a7a --- /dev/null +++ b/src/tgbaalgos/emptinesscheck.cc @@ -0,0 +1,578 @@ +#include "emptinesscheck.hh" +#include "tgba/tgba.hh" +#include "tgba/state.hh" +#include "tgba/bddprint.hh" +#include "tgba/tgbabddfactory.hh" +#include "tgba/succiterconcrete.hh" +#include "tgba/tgbabddconcrete.hh" +#include "bdd.h" +#include +#include +#include +#include +#include +#include +#include +#include + +namespace spot +{ + connected_component::connected_component() + { + 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() + { + } + + 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; + } + + void + emptiness_check::remove_component(const tgba& aut, seen& state_map, const spot::state* start_delete) + { + /// \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. + + 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()) + { + tgba_succ_iterator* succ_delete = to_remove.top(); + to_remove.pop(); + if (!succ_delete->done()) + { + to_remove.push(succ_delete); + state* curr_state = succ_delete->current_state(); + succ_delete->next(); + if (state_map[curr_state] != -1) + { + state_map[curr_state] = -1; + tgba_succ_iterator* succ_delete2 = aut.succ_iter(curr_state); + succ_delete2->first(); + to_remove.push(succ_delete2); + } + } + } + } + + emptiness_check::~emptiness_check() + { + } +emptiness_check::emptiness_check() + { + } + + bool + emptiness_check::tgba_emptiness_check(const spot::tgba* aut_check) + { + /// \brief On-the-fly emptiness check. + /// + /// The algorithm used here is adapted from Jean-Michel Couvreur's + /// Probataf tool. + int nbstate = 1; + state* init = aut_check->get_init_state(); + seen_state_num[init] = 1; + root_component.push(spot::connected_component(1,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()) + { + pair_state_iter step = todo.top(); + if ((step.second)->done()) + { + todo.pop(); + 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()); + 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); + assert(!arc_accepting.empty()); + arc_accepting.pop(); + assert(root_component.size() == arc_accepting.size()); + } + else + { + root_component.push(comp_tmp); + assert(root_component.size() == arc_accepting.size()); + } + } + else + { + iter_ = step.second; + state* current_state = iter_->current_state(); + bdd current_accepting = iter_->current_accepting_conditions(); + seen::iterator i = seen_state_num.find(current_state); + iter_->next(); + if (i == seen_state_num.end()) + { + /// New node. + nbstate = nbstate + 1; + assert(nbstate != 0); + seen_state_num[current_state] = nbstate; + root_component.push(connected_component(nbstate, bddfalse)); + arc_accepting.push(current_accepting); + tgba_succ_iterator* iter2 = aut_check->succ_iter(current_state); + iter2->first(); + todo.push(pair_state_iter(current_state, iter2 )); + } + else if (seen_state_num[current_state] != -1) + { + /// 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); + 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. + assert(!root_component.empty()); + comp = root_component.top(); + root_component.pop(); + 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); + } + 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); + root_component.push(comp); + return false; + } + root_component.push(comp); + assert(root_component.size() == arc_accepting.size()); + } + } + } + spot::bdd_print_dot(std::cout, aut_check->get_dict(),aut_check->all_accepting_conditions()); + /// The automata is empty. + return true; + } + + + void + emptiness_check::counter_example(const spot::tgba* aut_counter) + { + /// \brief Build a possible prefixe and period for a counter example. + bool emptiness = tgba_emptiness_check(aut_counter); + std::deque todo_trace; + typedef std::map path_state; + path_state path_map; + + if (!emptiness){ + int comp_size = root_component.size(); + std::cout << "*****COUNTER-EXAMPLE*****" << comp_size << std::endl; + 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(); +spot::bdd_print_dot(std::cout, aut_counter->get_dict(),root_component.top().condition); + root_component.pop(); + } + + for (int p = 0; p < comp_size; p++) + { + std::cout << "*****" << vec_component[p].index << "*****" << std::endl; + } + 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); + } + } + } + + for (int m = 0; m < comp_size; m++) + { + std::cout << "*****CONNECTED COMPONENT :" <format_state(*i_seq) << "*****" << std::endl; + seen::iterator i_1 = seen_state_num.find((*i_seq)); + assert(i_1 != seen_state_num.end()); + std::cout << "***** NUM :" << seen_state_num[*i_seq] << "*****" << std::endl; + } + std::cout << "_________________________________" << std::endl; + } + + 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()))); + } + } + else + { + seq_counter.push_front(start_state); + } + // vec_sequence[0].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.splice(seq_counter.end(), vec_sequence[n_]); + } + seq_counter.unique(); + for (state_sequence::iterator i_se = seq_counter.begin(); i_se != seq_counter.end(); i_se++) + { + std::cout << "*****STATE :" << aut_counter->format_state(*i_se) << "*****" << std::endl; + std::cout << "***** NUM :" << seen_state_num[(*i_se)] << "*****" << std::endl; + } + + std::cout << "ACCEPTING PATH BEGIN " << std::endl; + /// Call accepting_path to build the period of the counter example. + emptiness_check::accepting_path(aut_counter, vec_component[comp_size-1], seq_counter.back(),vec_component[comp_size-1].condition); +std::cout << "ACCEPTING PATH END " << std::endl; + + } + else + { + std::cout << "Nothings in vec_sequence " << std::endl; + std::cout << "******************************************" << std::endl; + std::cout << "*****SEEN STATE NUM :" << "*****" << std::endl; + for (seen::iterator i_sd = seen_state_num.begin(); i_sd != seen_state_num.end(); i_sd++) + { + std::cout << "*****STATE :" << aut_counter->format_state((*i_sd).first) << "*****" << std::endl; + std::cout << "***** NUM :" << seen_state_num[(*i_sd).first] << "*****" << std::endl; + } + std::cout << "_________________________________" << std::endl; + } + } + + void + emptiness_check::complete_cycle(const spot::tgba* aut_counter, const connected_component& comp_path, const state* from_state,const state* to_state) + { + /// \brief complete the path build by accepting_path to get the + ///period (cycle). + if (seen_state_num[from_state] != seen_state_num[to_state]) + { + std::cout << "COMPLETE CYCLE BEGIN" << std::endl; + 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)); + // tmp_comp.push_front(state_proposition(curr_father, complete_map[curr_father].second)); + while (curr_father->compare(from_state) != 0) + { + //emptiness_check::periode.push_front(state_proposition(curr_father, complete_map[curr_father].second)); + 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()); + } + } + } + } + // emptiness_check::periode = state_prop; + } + std::cout << "END COMPLETE CYCLE " << std::endl; + } + + +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. + seen seen_priority; + 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)); + bdd tmp_acc = bddfalse; + bdd best_acc = bddfalse; + cycle_path tmp_lst; + cycle_path best_lst; + bool ok = false; + seen_priority[start_path] = seen_state_num[start_path]; + for (seen::iterator i_ss = seen_priority.begin(); i_ss != seen_priority.end(); i_ss++) + { + std::cout << "*****STATE :" << aut_counter->format_state((*i_ss).first) << "*****" << std::endl; + std::cout << "***** NUM :" << seen_priority[(*i_ss).first] << "*****" << std::endl; + } + while (!todo_path.empty()) + { + triplet step_ = todo_path.top(); + tgba_succ_iterator* iter_ = (step_.first).second; + std::cout << "WHILE BEGIN " << iter_ << std::endl; + if (iter_->done()) + { + std::cout << "IF BEGIN " << std::endl; + todo_path.pop(); + seen_priority.erase((step_.first).first); + for (seen::iterator i_ss = seen_priority.begin(); i_ss != seen_priority.end(); i_ss++) + { + std::cout << "*****STATE :" << aut_counter->format_state((*i_ss).first) << "*****" << std::endl; + std::cout << "***** NUM :" << seen_priority[(*i_ss).first] << "*****" << std::endl; + } + //seen_priority.[(step_.first).first] = -2; + //delete(tmp_lst.back().first); + tmp_lst.pop_back(); + std::cout << "IF END " << std::endl; + } + else + { + std::cout << "ELSE BEGIN " << std::endl; + state* curr_state = iter_->current_state(); + connected_component::set_of_state::iterator it_set = comp_path.state_set.find(curr_state); + if (it_set != comp_path.state_set.end()) + { + std::cout << "IN COMPONENT " << std::endl; + seen::iterator i = seen_priority.find(curr_state); + if (i == seen_priority.end()) + { + std::cout << "NOT IN MAP " << std::endl; + std::cout <<"STATE:" << aut_counter->format_state(curr_state) << "*****" << std::endl; + // spot::bdd_print_dot(std::cout, aut_counter->get_dict(),aut_counter->succ_iter(curr_state)->current_accepting_conditions()); + tgba_succ_iterator* c_iter = aut_counter->succ_iter(curr_state); + bdd curr_bdd = bdd_apply(iter_->current_accepting_conditions(), step_.second, bddop_or); + std::cout << "*****TODO PATH PUSH STATE : BEFORE" << aut_counter->format_state((todo_path.top().first).first) << "*****" << std::endl; + c_iter->first(); + todo_path.push(triplet(pair_state_iter(curr_state, c_iter), curr_bdd)); +std::cout << "*****TODO PATH PUSH STATE : AFTER" << aut_counter->format_state((todo_path.top().first).first) << "*****" << std::endl; + tmp_lst.push_back(state_proposition(curr_state, iter_->current_condition())); + seen_priority[curr_state] = seen_state_num[curr_state]; + } + else + { + std::cout << "IN MAP " << std::endl; + if (ok) + { + std::cout << "NOT FIRST TIME " << std::endl; + bdd last_ = iter_->current_accepting_conditions(); + bdd prop_ = iter_->current_condition(); + tmp_lst.push_back(state_proposition(curr_state, prop_)); + tmp_acc = bdd_apply(last_, step_.second, bddop_or); +// tmp_lst.push_back(state_proposition(curr_state->clone(), last_)); + bdd curr_in = bdd_apply(tmp_acc, to_accept, bddop_and); + bdd best_in = bdd_apply(best_acc, to_accept, bddop_and); + if (curr_in == best_in) + { + if (tmp_lst.size() < best_lst.size()) + { + std::cout << "tmp_lst.size() < best_lst.size() " << std::endl; + cycle_path tmp(tmp_lst); + best_lst = tmp; + spot::bdd_print_dot(std::cout, aut_counter->get_dict(),step_.second); + } + } + else + { + if (bddtrue == bdd_apply(best_in, curr_in, bddop_imp)) + { + cycle_path tmp(tmp_lst); + best_lst = tmp; + best_acc = tmp_acc; + } + } + } + else + { + std::cout << "FIRST TIME " << std::endl; + 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_)); + cycle_path tmp(tmp_lst); + best_lst = tmp; + best_acc = tmp_acc; + ok = true; + } + } + } + iter_->next(); + std::cout << "ELSE END " << std::endl; + } + } + for (cycle_path::iterator it = best_lst.begin(); it != best_lst.end(); it++) + { + emptiness_check::periode.push_back(*it); + } + // emptiness_check::periode.splice(periode.end(), best_lst); + std::cout << "POINTEUR:" << periode.back().first << "*STATE :" << aut_counter->format_state( periode.back().first) << "*****" << std::endl; + if (best_acc != to_accept) + { + std::cout << "IN RECURSE " << std::endl; + bdd rec_to_acc = bdd_apply(to_accept, !best_acc, bddop_and); + std::cout << "BEST_ACC " << std::endl; + spot::bdd_print_dot(std::cout, aut_counter->get_dict(),best_acc); + std::cout << "TO_ACCEPT " << std::endl; + spot::bdd_print_dot(std::cout, aut_counter->get_dict(),to_accept); + std::cout << "TO_ACCEPT - BEST_ACC " << std::endl; + spot::bdd_print_dot(std::cout, aut_counter->get_dict(),rec_to_acc); + emptiness_check::accepting_path(aut_counter, comp_path, periode.back().first, rec_to_acc); + std::cout << "IN RECURSE " << std::endl; + } + else + { + bdd rec_to_acc = bdd_apply(to_accept, !best_acc, bddop_and); + std::cout << "TO_ACCEPT - BEST_ACC " << std::endl; + spot::bdd_print_dot(std::cout, aut_counter->get_dict(),rec_to_acc); + if (!periode.empty()) + { + + std::cout << "IN COMPLETE CYCLE " << std::endl; + /// The paht 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()); + for (cycle_path::iterator it = periode.begin(); it != periode.end(); it++) + { + std::cout << "*****STATE :" << aut_counter->format_state((*it).first) << "*****" << std::endl; + std::cout << "PROPOSITION TRANSITION :" << std::endl; + spot::bdd_print_dot(std::cout, aut_counter->get_dict(), (*it).second); + } + } + } + } +} diff --git a/src/tgbaalgos/emptinesscheck.hh b/src/tgbaalgos/emptinesscheck.hh new file mode 100644 index 000000000..e0ab204e4 --- /dev/null +++ b/src/tgbaalgos/emptinesscheck.hh @@ -0,0 +1,139 @@ +#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" +#include "tgba/succiterconcrete.hh" +#include "tgba/tgbabddconcrete.hh" +#include +#include +#include +#include +#include + +namespace spot +{ + /// \brief Emptiness check on spot::tgba + + class connected_component + { + /// 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); + + 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; + /// for the counter example we need to know all the states of the + ///component + set_of_state state_set; + int transition_acc; + int nb_transition; + int nb_state; + bool not_null; + }; + + class emptiness_check + { + + typedef std::pair pair_state_iter; + typedef std::pair triplet; + 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. + void + remove_component(const tgba& aut, seen& state_map, const spot::state* start_delete); + + /// \brief Emptiness check on spot::tgba + /// 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); + + /// 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. + + void + counter_example(const spot::tgba* aut_counter); + + std::stack arc_accepting; + std::stack root_component; + seen seen_state_num; + state_sequence seq_counter; + cycle_path periode; + private: + 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). + + 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); + }; +} +#endif // SPOT_EMPTINESS_CHECK_HH diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index f49786096..8596646f0 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -6,6 +6,8 @@ check_SCRIPTS = defs check_PROGRAMS = \ bddprod \ explicit \ + emptinesscheck \ +emptinesscheckexplicit \ explprod \ ltl2tgba \ ltlmagic \ @@ -18,6 +20,8 @@ check_PROGRAMS = \ # Keep this sorted alphabetically. bddprod_SOURCES = ltlprod.cc bddprod_CXXFLAGS = -DBDD_CONCRETE_PRODUCT +emptinesscheck_SOURCES = emptinesscheck.cc +emptinesscheckexplicit_SOURCES = emptinesscheckexplicit.cc explicit_SOURCES = explicit.cc explprod_SOURCES = explprod.cc ltl2tgba_SOURCES = ltl2tgba.cc @@ -42,6 +46,8 @@ TESTS = \ explpro3.test \ tripprod.test \ mixprod.test \ + emptinesscheck.test \ + emptinesscheckexplicit.test \ ltlmagic.test \ spotlbtt.test diff --git a/src/tgbatest/emptinesscheck.cc b/src/tgbatest/emptinesscheck.cc new file mode 100644 index 000000000..ee1b98018 --- /dev/null +++ b/src/tgbatest/emptinesscheck.cc @@ -0,0 +1,145 @@ + +#include +#include +#include "ltlvisit/destroy.hh" +#include "ltlast/allnodes.hh" +#include "ltlparse/public.hh" +#include "tgbaalgos/ltl2tgba_fm.hh" +#include "tgbaalgos/emptinesscheck.hh" +#include "tgba/bddprint.hh" +//#include "tgba/tgbabddtranslatefactory.hh" +#include "tgbaalgos/dotty.hh" + +void +syntax(char* prog) +{ std::cerr << "Usage: "<< prog << " [OPTIONS...] formula" << std::endl + << std::endl + << "Options:" << std::endl + << " -a display the accepting_conditions BDD, not the reachability graph" + << std::endl + << " -A same as -a, but as a set" << std::endl + << " -d turn on traces during parsing" << std::endl + << " -c emptinesschecking + counter example" << std::endl + << " -e emptinesschecking for the automaton" << std::endl + << " -o re-order BDD variables in the automata" << std::endl + << std::endl + << " -r display the relation BDD, not the reachability graph" + << std::endl + << " -R same as -r, but as a set" << std::endl + << " -v display the BDD variables used by the automaton" + << std::endl; + exit(2); +} + +std::string +print_emptiness_check_ans (bool ans) +{ + if (ans) + { + return "EMPTY-LANGAGE"; + } + else + { + return "CONSISTENT-AUTOMATA"; + } +} + +int +main(int argc, char** argv) +{ + int exit_code = 0; + + bool debug_opt = false; + bool defrag_opt = false; + spot::emptiness_check* empty_check = new spot::emptiness_check(); + bool emptiness = true; + int output = 0; + int formula_index = 0; + + for (;;) + { + if (argc < formula_index + 2) + syntax(argv[0]); + + ++formula_index; + + if (!strcmp(argv[formula_index], "-a")) + { + output = 2; + } + else if (!strcmp(argv[formula_index], "-A")) + { + output = 4; + } + else if (!strcmp(argv[formula_index], "-d")) + { + debug_opt = true; + } + else if (!strcmp(argv[formula_index], "-e")) + { + output = 6; + } + else if (!strcmp(argv[formula_index], "-c")) + { + output = 7; + } + else if (!strcmp(argv[formula_index], "-o")) + { + defrag_opt = true; + } + else if (!strcmp(argv[formula_index], "-r")) + { + output = 1; + } + else if (!strcmp(argv[formula_index], "-R")) + { + output = 3; + } + else if (!strcmp(argv[formula_index], "-v")) + { + output = 5; + } + else + { + break; + } + } + + + spot::ltl::environment& env(spot::ltl::default_environment::instance()); + spot::ltl::parse_error_list pel; + spot::ltl::formula* f = spot::ltl::parse(argv[formula_index], + pel, env, debug_opt); + + exit_code = spot::ltl::format_parse_errors(std::cerr, argv[formula_index], pel); + spot::bdd_dict* dict = new spot::bdd_dict(); + if (f) + { + spot::tgba_explicit* a = spot::ltl_to_tgba_fm(f, dict); + spot::ltl::destroy(f); + switch (output) + { + case 6: + emptiness = empty_check->tgba_emptiness_check(a); + std::cout << print_emptiness_check_ans(emptiness) << std::endl; + break; + case 7: + empty_check->counter_example(a); + break; + default: + assert(!"unknown output option"); + } + delete a; + delete empty_check; + } + else + { + exit_code = 1; + } + assert(spot::ltl::atomic_prop::instance_count() == 0); + assert(spot::ltl::unop::instance_count() == 0); + assert(spot::ltl::binop::instance_count() == 0); + assert(spot::ltl::multop::instance_count() == 0); + delete dict; + return exit_code; +} diff --git a/src/tgbatest/emptinesscheck.test b/src/tgbatest/emptinesscheck.test new file mode 100755 index 000000000..3840861ab --- /dev/null +++ b/src/tgbatest/emptinesscheck.test @@ -0,0 +1,20 @@ +#!/bin/sh + +. ./defs + +set -e + +# We don't check the output, but just running these might be enough to +# trigger assertions. + +./emptinesscheck -e 'a' +./emptinesscheck -e 'a U b' +./emptinesscheck -e 'X a' +./emptinesscheck -e 'a & b & c' +./emptinesscheck -e 'a | b | (c U (d & (g U (h ^ i))))' +./emptinesscheck -e 'Xa & (b U !a) & (b U !a)' +./emptinesscheck -e 'Fa & Xb & GFc & Gd' +./emptinesscheck -e 'Fa & Xa & GFc & Gc' +./emptinesscheck -e 'Fc & X(a | Xb) & GF(a | Xb) & Gc' +./emptinesscheck -e '!((FF a) <=> (F x))' +./emptinesscheck -e '!((FF a) <=> (F a))' \ No newline at end of file diff --git a/src/tgbatest/emptinesscheckexplicit.cc b/src/tgbatest/emptinesscheckexplicit.cc new file mode 100644 index 000000000..2572c161e --- /dev/null +++ b/src/tgbatest/emptinesscheckexplicit.cc @@ -0,0 +1,46 @@ +#include +#include "tgbaparse/public.hh" +#include "tgba/tgbaexplicit.hh" +#include "tgbaalgos/dotty.hh" +#include "tgbaalgos/emptinesscheck.hh" + +void +syntax(char* prog) +{ + std::cerr << prog << " [-d] filename" << std::endl; + exit(2); +} + +int +main(int argc, char** argv) +{ + int exit_code = 0; + + if (argc < 2) + syntax(argv[0]); + + bool debug = false; + int filename_index = 1; + bool emptiness = false; + + if (!strcmp(argv[1], "-d")) + { + debug = true; + if (argc < 3) + syntax(argv[0]); + filename_index = 2; + } + + spot::ltl::environment& env(spot::ltl::default_environment::instance()); + spot::tgba_parse_error_list pel; + spot::bdd_dict* dict = new spot::bdd_dict(); + spot::tgba_explicit* a = spot::tgba_parse(argv[filename_index], + pel, dict, env, debug); + spot::emptiness_check empty_check; + + if (spot::format_tgba_parse_errors(std::cerr, pel)) + return 2; + empty_check.counter_example(a); + delete a; + return 0; +} diff --git a/src/tgbatest/emptinesscheckexplicit.test b/src/tgbatest/emptinesscheckexplicit.test new file mode 100755 index 000000000..29555f314 --- /dev/null +++ b/src/tgbatest/emptinesscheckexplicit.test @@ -0,0 +1,14 @@ +#!/bin/sh + +. ./defs + +set -e + +cat >input <<'EOF' +acc = c d; +s1, "s2", a!b, c d; +"s2", "state 3", a, c; +"state 3", s1,,; +EOF + +./emptinesscheckexplicit input > stdout