From be4f4e337019361d6bb33e86d94aa796e5bc3b69 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 15 Apr 2004 09:12:11 +0000 Subject: [PATCH] * iface/gspn/eesrg.cc (connected_component_eesrg::has_state): Free filtered states. (emptiness_check_shy_eesrg): New class. (emptiness_check_eesrg_shy): New function. * iface/gspn/eesrg.hh (emptiness_check_eesrg_shy): New function. * iface/gspn/ltlgspn.cc (main) [EESRG]: Handle -e3, -e4, and -e5. * * src/tgbaalgos/gtec/gtec.hh, src/tgbaalgos/gtec/gtec.cc (emptiness_check_shy::check): Move arc, num, succ_queue, and todo as attributes. (emptiness_check_shy::find_state): New virtual function. --- ChangeLog | 14 ++++++ iface/gspn/eesrg.cc | 90 +++++++++++++++++++++++++++++++++++++- iface/gspn/eesrg.hh | 2 + iface/gspn/ltlgspn.cc | 59 ++++++++++++++++++++----- src/tgbaalgos/gtec/gtec.cc | 41 ++++++----------- src/tgbaalgos/gtec/gtec.hh | 25 +++++++++++ 6 files changed, 189 insertions(+), 42 deletions(-) diff --git a/ChangeLog b/ChangeLog index fc566b53a..712b1045f 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,17 @@ +2004-04-15 Soheib Baarir + Alexandre Duret-Lutz + + * iface/gspn/eesrg.cc (connected_component_eesrg::has_state): + Free filtered states. + (emptiness_check_shy_eesrg): New class. + (emptiness_check_eesrg_shy): New function. + * iface/gspn/eesrg.hh (emptiness_check_eesrg_shy): New function. + * iface/gspn/ltlgspn.cc (main) [EESRG]: Handle -e3, -e4, and -e5. + * * src/tgbaalgos/gtec/gtec.hh, src/tgbaalgos/gtec/gtec.cc + (emptiness_check_shy::check): Move arc, num, succ_queue, and todo + as attributes. + (emptiness_check_shy::find_state): New virtual function. + 2004-04-14 Soheib Baarir Alexandre Duret-Lutz diff --git a/iface/gspn/eesrg.cc b/iface/gspn/eesrg.cc index a95e1bd91..fd601b66c 100644 --- a/iface/gspn/eesrg.cc +++ b/iface/gspn/eesrg.cc @@ -440,7 +440,7 @@ namespace spot size_t size_tgba_ = 0; int j, conj; - succ(s->left(), props_ ,nb_arc_props, &succ_tgba_, &size_tgba_); + succ(s->left(), props_, nb_arc_props, &succ_tgba_, &size_tgba_); for (j = 0; j < nb_arc_props; j++) { @@ -580,7 +580,11 @@ namespace spot && old_state->left() && new_state->left()) if (spot_inclusion(new_state->left(), old_state->left())) - return (*i); + { + if (*i != s) + delete s; + return *i; + } } return 0; } @@ -732,6 +736,7 @@ namespace spot hash_type h; ///< Map of visited states. friend class numbered_state_heap_eesrg_const_iterator; + friend class emptiness_check_shy_eesrg; }; @@ -784,6 +789,7 @@ namespace spot const numbered_state_heap_eesrg_semi::hash_type& h; }; + numbered_state_heap_const_iterator* numbered_state_heap_eesrg_semi::iterator() const { @@ -824,6 +830,79 @@ namespace spot }; + class emptiness_check_shy_eesrg : public emptiness_check_shy + { + public: + emptiness_check_shy_eesrg(const tgba* a) + : emptiness_check_shy(a, + numbered_state_heap_eesrg_factory_semi::instance()) + { + } + + protected: + virtual int* + find_state(const state* s) + { + typedef numbered_state_heap_eesrg_semi::hash_type hash_type; + hash_type& h = dynamic_cast(ecs_->h)->h; + + hash_type::iterator i; + for (i = h.begin(); i != h.end(); ++i) + { + const state_gspn_eesrg* old_state = + dynamic_cast(i->first); + const state_gspn_eesrg* new_state = + dynamic_cast(s); + assert(old_state); + assert(new_state); + + if ((old_state->right())->compare(new_state->right()) == 0) + { + if (old_state->left() == new_state->left()) + break; + + if (old_state->left() && new_state->left()) + { + if (i->second == -1) + { + if (spot_inclusion(new_state->left(), old_state->left())) + break; + } + else + { + if (spot_inclusion(old_state->left(), new_state->left())) + { + State* succ_tgba_ = NULL; + size_t size_tgba_ = 0; + succ_queue& queue = todo.top().second; + + Diff_succ(old_state->left(), new_state->left(), + &succ_tgba_, &size_tgba_); + + for (size_t i = 0; i < size_tgba_; i++) + { + state_gspn_eesrg* s = + new state_gspn_eesrg + (succ_tgba_[i], + old_state->right()->clone()); + queue.push_back(successor(queue.begin()->acc, s)); + } + if (size_tgba_ != 0) + diff_succ_free(succ_tgba_); + break; + } + } + } + } + } + if (i == h.end()) + return 0; + return &i->second; + } + }; + + + emptiness_check* emptiness_check_eesrg_semi(const tgba* eesrg_automata) { @@ -843,6 +922,13 @@ namespace spot numbered_state_heap_eesrg_factory_semi::instance()); } + emptiness_check* + emptiness_check_eesrg_shy(const tgba* eesrg_automata) + { + assert(dynamic_cast(eesrg_automata)); + return new emptiness_check_shy_eesrg(eesrg_automata); + } + counter_example* counter_example_eesrg(const emptiness_check_status* status) { diff --git a/iface/gspn/eesrg.hh b/iface/gspn/eesrg.hh index 285cedbe3..0c4228cc5 100644 --- a/iface/gspn/eesrg.hh +++ b/iface/gspn/eesrg.hh @@ -48,6 +48,8 @@ namespace spot emptiness_check* emptiness_check_eesrg_semi(const tgba* eesrg_automata); emptiness_check* emptiness_check_eesrg_shy_semi(const tgba* eesrg_automata); + emptiness_check* emptiness_check_eesrg_shy(const tgba* eesrg_automata); + counter_example* counter_example_eesrg(const emptiness_check_status* status); } diff --git a/iface/gspn/ltlgspn.cc b/iface/gspn/ltlgspn.cc index c1c079f5c..05c7040b9 100644 --- a/iface/gspn/ltlgspn.cc +++ b/iface/gspn/ltlgspn.cc @@ -53,7 +53,15 @@ syntax(char* prog) << " (instead of just checking for emptiness)" << std::endl << std::endl << " -e use Couvreur's emptiness-check (default)" << std::endl - << " -e2 use Couvreur's emptiness-check variant" << std::endl + << " -e2 use Couvreur's emptiness-check's shy variant" << std::endl +#ifdef EESRG + << " -e3 use semi-d. incl. Couvreur's emptiness-check" + << std::endl + << " -e4 use semi-d. incl. Couvreur's emptiness-check's shy variant" + << std::endl + << " -e5 use d. incl. Couvreur's emptiness-check's shy variant" + << std::endl +#endif << " -m degeneralize and perform a magic-search" << std::endl << std::endl << " -l use Couvreur's LaCIM algorithm for translation (default)" @@ -68,7 +76,8 @@ main(int argc, char **argv) try { int formula_index = 1; - enum { Couvreur, Couvreur2, Magic } check = Couvreur; + enum { Couvreur, Couvreur2, Couvreur3, + Couvreur4, Couvreur5, Magic } check = Couvreur; enum { Lacim, Fm } trans = Lacim; bool compute_counter_example = false; bool proj = true; @@ -89,6 +98,18 @@ main(int argc, char **argv) { check = Couvreur2; } + else if (!strcmp(argv[formula_index], "-e3")) + { + check = Couvreur3; + } + else if (!strcmp(argv[formula_index], "-e4")) + { + check = Couvreur4; + } + else if (!strcmp(argv[formula_index], "-e5")) + { + check = Couvreur5; + } else if (!strcmp(argv[formula_index], "-m")) { check = Magic; @@ -169,20 +190,34 @@ main(int argc, char **argv) { case Couvreur: case Couvreur2: + case Couvreur3: + case Couvreur4: + case Couvreur5: { spot::emptiness_check* ec; -#ifndef EESRG - if (check == Couvreur) - ec = new spot::emptiness_check(prod); - else - ec = new spot::emptiness_check_shy(prod); -#else - if (check == Couvreur) - ec = spot::emptiness_check_eesrg_semi(prod); - else - ec = spot::emptiness_check_eesrg_shy_semi(prod); + switch (check) + { + case Couvreur: + ec = new spot::emptiness_check(prod); + break; + case Couvreur2: + ec = new spot::emptiness_check_shy(prod); + break; +#ifdef EESRG + case Couvreur3: + ec = spot::emptiness_check_eesrg_semi(prod); + break; + case Couvreur4: + ec = spot::emptiness_check_eesrg_shy_semi(prod); + break; + case Couvreur5: + ec = spot::emptiness_check_eesrg_shy(prod); + break; #endif + default: + assert(0); + } bool res = ec->check(); diff --git a/src/tgbaalgos/gtec/gtec.cc b/src/tgbaalgos/gtec/gtec.cc index 1e7658571..3fa90d720 100644 --- a/src/tgbaalgos/gtec/gtec.cc +++ b/src/tgbaalgos/gtec/gtec.cc @@ -237,43 +237,21 @@ namespace spot emptiness_check_shy::emptiness_check_shy(const tgba* a, const numbered_state_heap_factory* nshf) - : emptiness_check(a, nshf) + : emptiness_check(a, nshf), num(1) { + // Setup depth-first search from the initial state. + todo.push(pair_state_successors(0, succ_queue())); + todo.top().second.push_front(successor(bddtrue, + ecs_->aut->get_init_state())); } emptiness_check_shy::~emptiness_check_shy() { } - struct successor { - bdd acc; - const spot::state* s; - successor(bdd acc, const spot::state* s): acc(acc), s(s) {} - }; - bool emptiness_check_shy::check() { - // We use five main data in this algorithm: - // * emptiness_check::root, a stack of strongly connected components (SCC), - // * emptiness_check::h, a hash of all visited nodes, with their order, - // (it is called "Hash" in Couvreur's paper) - // * arc, a stack of acceptance conditions between each of these SCC, - std::stack arc; - // * num, the number of visited nodes. Used to set the order of each - // visited node, - int num = 1; - // * todo, the depth-first search stack. This holds pairs of the - // form (STATE, SUCCESSORS) where SUCCESSORS is a list of - // (ACCEPTANCE_CONDITIONS, STATE) pairs. - typedef std::list succ_queue; - typedef std::pair pair_state_successors; - std::stack todo; - - // Setup depth-first search from the initial state. - todo.push(pair_state_successors(0, succ_queue())); - todo.top().second.push_front(successor(bddtrue, - ecs_->aut->get_init_state())); for (;;) { @@ -288,7 +266,7 @@ namespace spot succ_queue::iterator q = queue.begin(); while (q != queue.end()) { - int* i = ecs_->h->find(q->s); + int* i = find_state(q->s); if (!i) { // Skip unknown states. @@ -414,4 +392,11 @@ namespace spot delete iter; } } + + int* + emptiness_check_shy::find_state(const state* s) + { + return ecs_->h->find(s); + } + } diff --git a/src/tgbaalgos/gtec/gtec.hh b/src/tgbaalgos/gtec/gtec.hh index 003e93b87..22dbfec8e 100644 --- a/src/tgbaalgos/gtec/gtec.hh +++ b/src/tgbaalgos/gtec/gtec.hh @@ -111,6 +111,31 @@ namespace spot virtual ~emptiness_check_shy(); virtual bool check(); + + protected: + struct successor { + bdd acc; + const spot::state* s; + successor(bdd acc, const spot::state* s): acc(acc), s(s) {} + }; + + // We use five main data in this algorithm: + // * emptiness_check::root, a stack of strongly connected components (SCC), + // * emptiness_check::h, a hash of all visited nodes, with their order, + // (it is called "Hash" in Couvreur's paper) + // * arc, a stack of acceptance conditions between each of these SCC, + std::stack arc; + // * num, the number of visited nodes. Used to set the order of each + // visited node, + int num; + // * todo, the depth-first search stack. This holds pairs of the + // form (STATE, SUCCESSORS) where SUCCESSORS is a list of + // (ACCEPTANCE_CONDITIONS, STATE) pairs. + typedef std::list succ_queue; + typedef std::pair pair_state_successors; + std::stack todo; + + virtual int* find_state(const state* s); }; }