From 8ff4ca08ce80406ddef53f10edaa26045b64a986 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 15 Apr 2004 11:50:29 +0000 Subject: [PATCH] * src/tgbaalgos/gtec/nsheap.cc (numbered_state_heap_hash_map::find): Rewrite. (numbered_state_heap_hash_map::index): New functions. (numbered_state_heap_hash_map::filter): Delete. * src/tgbaalgos/gtec/nsheap.hh (numbered_state_heap_hash_map::index): New functions. (numbered_state_heap_hash_map::filter): Delete. * iface/gspn/eesrg.cc (numbered_state_heap_eesrg_semi::find, numbered_state_heap_eesrg_semi::index): Rewrite. (numbered_state_heap_eesrg_semi::filter): Remove. * src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/ce.cc: Adjust to use find() and index() instead of filter().. --- ChangeLog | 14 ++++ iface/gspn/eesrg.cc | 134 +++++++++++++++++++++++++---------- src/tgbaalgos/gtec/ce.cc | 6 +- src/tgbaalgos/gtec/gtec.cc | 65 ++++++++--------- src/tgbaalgos/gtec/nsheap.cc | 60 +++++++++++----- src/tgbaalgos/gtec/nsheap.hh | 53 +++++++++----- 6 files changed, 223 insertions(+), 109 deletions(-) diff --git a/ChangeLog b/ChangeLog index 712b1045f..55a1325d7 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,6 +1,20 @@ 2004-04-15 Soheib Baarir Alexandre Duret-Lutz + * src/tgbaalgos/gtec/nsheap.cc (numbered_state_heap_hash_map::find): + Rewrite. + (numbered_state_heap_hash_map::index): New functions. + (numbered_state_heap_hash_map::filter): Delete. + * src/tgbaalgos/gtec/nsheap.hh + (numbered_state_heap_hash_map::index): New functions. + (numbered_state_heap_hash_map::filter): Delete. + * iface/gspn/eesrg.cc (numbered_state_heap_eesrg_semi::find, + numbered_state_heap_eesrg_semi::index): Rewrite. + (numbered_state_heap_eesrg_semi::filter): Remove. + * src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/ce.cc: + Adjust to use find() and index() instead of filter().. + + * iface/gspn/eesrg.cc (connected_component_eesrg::has_state): Free filtered states. (emptiness_check_shy_eesrg): New class. diff --git a/iface/gspn/eesrg.cc b/iface/gspn/eesrg.cc index fd601b66c..6e3952e82 100644 --- a/iface/gspn/eesrg.cc +++ b/iface/gspn/eesrg.cc @@ -650,9 +650,11 @@ namespace spot } } - virtual const int* + virtual numbered_state_heap::state_index find(const state* s) const { + state_index res; + hash_type::const_iterator i; for (i = h.begin(); i != h.end(); ++i) { @@ -674,16 +676,106 @@ namespace spot break; } } + if (i == h.end()) - return 0; - return &i->second; + { + res.first = 0; + res.second = 0; + } + else + { + res.first = i->first; + res.second = i->second; + + if (s != i->first) + delete s; + } + return res; } - virtual int* + virtual numbered_state_heap::state_index_p find(const state* s) { - return const_cast - (const_cast(this)->find(s)); + state_index_p res; + + 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() + && spot_inclusion(new_state->left(),old_state->left())) + break; + } + } + + if (i == h.end()) + { + res.first = 0; + res.second = 0; + } + else + { + res.first = i->first; + res.second = &i->second; + + if (s != i->first) + delete s; + } + return res; + } + + virtual numbered_state_heap::state_index + index(const state* s) const + { + state_index res; + hash_type::const_iterator i = h.find(s); + if (i == h.end()) + { + res.first = 0; + res.second = 0; + } + else + { + res.first = i->first; + res.second = i->second; + + if (s != i->first) + delete s; + } + return res; + } + + virtual numbered_state_heap::state_index_p + index(const state* s) + { + state_index_p res; + hash_type::iterator i = h.find(s); + if (i == h.end()) + { + res.first = 0; + res.second = 0; + } + else + { + res.first = i->first; + res.second = &i->second; + + if (s != i->first) + delete s; + } + return res; } virtual void @@ -700,36 +792,6 @@ namespace spot virtual numbered_state_heap_const_iterator* iterator() const; - virtual const state* - filter(const state* s) const - { - hash_type::const_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() - && spot_inclusion(new_state->left(),old_state->left())) - break; - } - } - assert(i != h.end()); - if (s != i->first) - delete s; - return i->first; - } - protected: typedef Sgi::hash_map hash_type; diff --git a/src/tgbaalgos/gtec/ce.cc b/src/tgbaalgos/gtec/ce.cc index b5ebff896..cd4e0d422 100644 --- a/src/tgbaalgos/gtec/ce.cc +++ b/src/tgbaalgos/gtec/ce.cc @@ -71,7 +71,10 @@ namespace spot } delete i; - suffix.push_front(ecs_->h->filter(ecs_->aut->get_init_state())); + numbered_state_heap::state_index_p spi = + ecs_->h->index(ecs_->aut->get_init_state()); + assert(spi.first); + suffix.push_front(spi.first); // We build a path trough each SCC in the stack. For the // first SCC, the starting state is the initial state of the @@ -134,6 +137,7 @@ namespace spot break; } // Restrict the BFS to state inside the SCC. + delete dest; continue; } diff --git a/src/tgbaalgos/gtec/gtec.cc b/src/tgbaalgos/gtec/gtec.cc index 3fa90d720..210ddfc3e 100644 --- a/src/tgbaalgos/gtec/gtec.cc +++ b/src/tgbaalgos/gtec/gtec.cc @@ -51,10 +51,10 @@ namespace spot // (FROM should be in H, otherwise it means all reachable // states from FROM have already been removed and there is no // point in calling remove_component.) - int* hi = ecs_->h->find(from); - assert(hi); - assert(*hi != -1); - *hi = -1; + numbered_state_heap::state_index_p spi = ecs_->h->index(from); + assert(spi.first); + assert(*spi.second != -1); + *spi.second = -1; tgba_succ_iterator* i = ecs_->aut->succ_iter(from); for (;;) @@ -63,15 +63,13 @@ namespace spot for (i->first(); !i->done(); i->next()) { state* s = i->current_state(); - int *hi = ecs_->h->find(s); - assert(hi); - - if (*hi != -1) + numbered_state_heap::state_index_p spi = ecs_->h->index(s); + assert(spi.second); + if (*spi.second != -1) { - *hi = -1; - to_remove.push(ecs_->aut->succ_iter(s)); + *spi.second = -1; + to_remove.push(ecs_->aut->succ_iter(spi.first)); } - delete s; } delete i; if (to_remove.empty()) @@ -130,10 +128,10 @@ namespace spot // When backtracking the root of an SCC, we must also // remove that SCC from the ARC/ROOT stacks. We must // discard from H all reachable states from this SCC. - int* i = ecs_->h->find(curr); - assert(i); + numbered_state_heap::state_index_p spi = ecs_->h->index(curr); + assert(spi.first); assert(!ecs_->root.empty()); - if (ecs_->root.top().index == *i) + if (ecs_->root.top().index == *spi.second) { assert(!arc.empty()); arc.pop(); @@ -157,8 +155,8 @@ namespace spot // We do not need SUCC from now on. // Are we going to a new state? - int* i = ecs_->h->find(dest); - if (!i) + numbered_state_heap::state_index_p spi = ecs_->h->find(dest); + if (!spi.first) { // Yes. Number it, stack it, and register its successors // for later processing. @@ -171,13 +169,8 @@ namespace spot continue; } - // We know the state exists. Since a state can have several - // representations (i.e., objects), make sure we delete - // anything but the first one seen (the one used as key in H). - (void) ecs_->h->filter(dest); - // If we have reached a dead component, ignore it. - if (*i == -1) + if (*spi.second == -1) continue; // Now this is the most interesting case. We have reached a @@ -191,7 +184,7 @@ namespace spot // ROOT is ascending: we just have to merge all SCCs from the // top of ROOT that have an index greater to the one of // the SCC of S2 (called the "threshold"). - int threshold = *i; + int threshold = *spi.second; while (threshold < ecs_->root.top().index) { assert(!ecs_->root.empty()); @@ -314,6 +307,8 @@ namespace spot if (ecs_->root.top().condition == ecs_->aut->all_acceptance_conditions()) { + /// q->s has already been freed by find_state(). + queue.erase(q); // We have found an accepting SCC. Clean up TODO. // We must delete all states of apparing in TODO // unless they are used as keys in H. @@ -323,23 +318,19 @@ namespace spot for (succ_queue::iterator q = queue.begin(); q != queue.end(); ++q) { - int* i = ecs_->h->find(q->s); - if (!i) + // Delete the state if it is a clone of a + // state in the heap... + numbered_state_heap::state_index_p spi + = ecs_->h->index(q->s); + // ... or if it is an unknown state. + if (spi.first == 0) delete q->s; - else - // Delete the state if it is a clone - // of a state in the heap. - (void) ecs_->h->filter(q->s); } todo.pop(); } return false; } } - // We know the state exists. Since a state can have several - // representations (i.e., objects), make sure we delete - // anything but the first one seen (the one used as key in H). - (void) ecs_->h->filter(q->s); // Remove that state from the queue, so we do not // recurse into it. succ_queue::iterator old = q++; @@ -360,10 +351,10 @@ namespace spot // When backtracking the root of an SCC, we must also // remove that SCC from the ARC/ROOT stacks. We must // discard from H all reachable states from this SCC. - int* i = ecs_->h->find(curr); - assert(i); + numbered_state_heap::state_index_p spi = ecs_->h->index(curr); + assert(spi.first); assert(!ecs_->root.empty()); - if (ecs_->root.top().index == *i) + if (ecs_->root.top().index == *spi.second) { assert(!arc.empty()); arc.pop(); @@ -396,7 +387,7 @@ namespace spot int* emptiness_check_shy::find_state(const state* s) { - return ecs_->h->find(s); + return ecs_->h->find(s).second; } } diff --git a/src/tgbaalgos/gtec/nsheap.cc b/src/tgbaalgos/gtec/nsheap.cc index 3dde0dcf1..47159096f 100644 --- a/src/tgbaalgos/gtec/nsheap.cc +++ b/src/tgbaalgos/gtec/nsheap.cc @@ -85,22 +85,60 @@ namespace spot } } - const int* + numbered_state_heap::state_index numbered_state_heap_hash_map::find(const state* s) const { + state_index res; hash_type::const_iterator i = h.find(s); + if (i == h.end()) - return 0; - return &i->second; + { + res.first = 0; + res.second = 0; + } + else + { + res.first = i->first; + res.second = i->second; + + if (s != i->first) + delete s; + } + return res; } - int* + numbered_state_heap::state_index_p numbered_state_heap_hash_map::find(const state* s) { + state_index_p res; hash_type::iterator i = h.find(s); + if (i == h.end()) - return 0; - return &i->second; + { + res.first = 0; + res.second = 0; + } + else + { + res.first = i->first; + res.second = &i->second; + + if (s != i->first) + delete s; + } + return res; + } + + numbered_state_heap::state_index + numbered_state_heap_hash_map::index(const state* s) const + { + return this->numbered_state_heap_hash_map::find(s); + } + + numbered_state_heap::state_index_p + numbered_state_heap_hash_map::index(const state* s) + { + return this->numbered_state_heap_hash_map::find(s); } void @@ -121,16 +159,6 @@ namespace spot return new numbered_state_heap_hash_map_const_iterator(h); } - const state* - numbered_state_heap_hash_map::filter(const state* s) const - { - hash_type::const_iterator i = h.find(s); - assert(i != h.end()); - if (s != i->first) - delete s; - return i->first; - } - numbered_state_heap_hash_map_factory::numbered_state_heap_hash_map_factory() : numbered_state_heap_factory() { diff --git a/src/tgbaalgos/gtec/nsheap.hh b/src/tgbaalgos/gtec/nsheap.hh index 468604b88..aab8294ca 100644 --- a/src/tgbaalgos/gtec/nsheap.hh +++ b/src/tgbaalgos/gtec/nsheap.hh @@ -51,14 +51,39 @@ namespace spot class numbered_state_heap { public: + typedef std::pair state_index_p; + typedef std::pair state_index; + virtual ~numbered_state_heap() {} //@{ /// \brief Is state in the heap? /// - /// Returns 0 if \a s is not in the heap. or a pointer to - /// its number if it is. - virtual const int* find(const state* s) const = 0; - virtual int* find(const state* s) = 0; + /// Returns a pair (0,0) if \a s is not in the heap. + /// or a pair (p, i) if there is a clone \a p of \a s \a i + /// in the heap with index. \a s will be freed if it is + /// different of \a p. + /// + /// There are called by the algorithm to check whether a + /// successor is a new state to explore or an already visited + /// state. + /// + /// These functions can be redefined to search for more + /// than an equal match. For example we could redefine + /// it to check state inclusion. + virtual state_index find(const state* s) const = 0; + virtual state_index_p find(const state* s) = 0; + //@} + + //@{ + /// \brief Return the index of an existing state. + /// + /// This is mostly similar to find(), except it will + /// be called for state which we know are already in + /// the heap, or for state which may not be in the + /// heap but for which it is always OK to do equality + /// checks. + virtual state_index index(const state* s) const = 0; + virtual state_index_p index(const state* s) = 0; //@} /// Add a new state \a s with index \a index @@ -69,16 +94,6 @@ namespace spot /// Return an iterator on the states/indexes pairs. virtual numbered_state_heap_const_iterator* iterator() const = 0; - - /// \brief Filter state clones. - /// - /// Return a state which is equal to \a s, but is an actual key in - /// the heap, and free \a s if it is a clone of that state. - /// - /// Doing so simplify memory management, because we don't have to - /// track which state need to be kept or deallocated: all key in - /// the heap should last for the whole life of the emptiness-check. - virtual const state* filter(const state* s) const = 0; }; /// Abstract factory for numbered_state_heap @@ -95,15 +110,15 @@ namespace spot public: virtual ~numbered_state_heap_hash_map(); - virtual const int* find(const state* s) const; - virtual int* find(const state* s); + virtual state_index find(const state* s) const; + virtual state_index_p find(const state* s); + virtual state_index index(const state* s) const; + virtual state_index_p index(const state* s); + virtual void insert(const state* s, int index); virtual int size() const; virtual numbered_state_heap_const_iterator* iterator() const; - - virtual const state* filter(const state* s) const; - protected: typedef Sgi::hash_map hash_type;