diff --git a/ChangeLog b/ChangeLog index 82571cbbb..81d75f617 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,18 @@ 2004-04-14 Alexandre Duret-Lutz + * src/tgbaalgos/gtec/nsheap.hh (numbered_state_heap_factory, + numbered_state_heap_hash_map_factory): New class. + * src/tgbaalgos/gtec/nsheap.cc (numbered_state_heap_hash_map_factory): + Implement it. + * src/tgbaalgos/gtec/gtec.hh (emptiness_check::emptiness_check, + emptiness_check_shy::emptiness_check_shy): Take a + numbered_state_heap_factory argument. + * tgbaalgos/gtec/status.hh + (emptiness_check_status::emptiness_check_status): Likewise. + (emptiness_check_status::h): Make it a numbered_state_heap*. + * src/tgbaalgos/gtec/ce.cc, tgbaalgos/gtec/gtec.cc, + tgbaalgos/gtec/status.cc: Adjust uses of ecs_->h. + * src/tgbaalgos/emptinesscheck.hh, src/tgbaalgos/emptinesscheck.cc: Delete and split into ... * src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/ce.hh, diff --git a/src/tgbaalgos/gtec/ce.cc b/src/tgbaalgos/gtec/ce.cc index b55d71029..b5ebff896 100644 --- a/src/tgbaalgos/gtec/ce.cc +++ b/src/tgbaalgos/gtec/ce.cc @@ -53,7 +53,7 @@ namespace spot assert(root.empty()); // Build the set of states for all SCCs. - numbered_state_heap_const_iterator* i = ecs_->h.iterator(); + numbered_state_heap_const_iterator* i = ecs_->h->iterator(); for (i->first(); !i->done(); i->next()) { int index = i->get_index(); @@ -71,7 +71,7 @@ namespace spot } delete i; - suffix.push_front(ecs_->h.filter(ecs_->aut->get_init_state())); + suffix.push_front(ecs_->h->filter(ecs_->aut->get_init_state())); // We build a path trough each SCC in the stack. For the // first SCC, the starting state is the initial state of the diff --git a/src/tgbaalgos/gtec/gtec.cc b/src/tgbaalgos/gtec/gtec.cc index f85145947..1e7658571 100644 --- a/src/tgbaalgos/gtec/gtec.cc +++ b/src/tgbaalgos/gtec/gtec.cc @@ -28,9 +28,10 @@ namespace spot typedef std::pair pair_state_iter; } - emptiness_check::emptiness_check(const tgba* a) + emptiness_check::emptiness_check(const tgba* a, + const numbered_state_heap_factory* nshf) { - ecs_ = new emptiness_check_status(a); + ecs_ = new emptiness_check_status(a, nshf); } emptiness_check::~emptiness_check() @@ -50,7 +51,7 @@ 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); + int* hi = ecs_->h->find(from); assert(hi); assert(*hi != -1); *hi = -1; @@ -62,7 +63,7 @@ namespace spot for (i->first(); !i->done(); i->next()) { state* s = i->current_state(); - int *hi = ecs_->h.find(s); + int *hi = ecs_->h->find(s); assert(hi); if (*hi != -1) @@ -102,7 +103,7 @@ namespace spot // Setup depth-first search from the initial state. { state* init = ecs_->aut->get_init_state(); - ecs_->h.insert(init, 1); + ecs_->h->insert(init, 1); ecs_->root.push(1); arc.push(bddfalse); tgba_succ_iterator* iter = ecs_->aut->succ_iter(init); @@ -129,7 +130,7 @@ 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); + int* i = ecs_->h->find(curr); assert(i); assert(!ecs_->root.empty()); if (ecs_->root.top().index == *i) @@ -156,12 +157,12 @@ namespace spot // We do not need SUCC from now on. // Are we going to a new state? - int* i = ecs_->h.find(dest); + int* i = ecs_->h->find(dest); if (!i) { // Yes. Number it, stack it, and register its successors // for later processing. - ecs_->h.insert(dest, ++num); + ecs_->h->insert(dest, ++num); ecs_->root.push(num); arc.push(acc); tgba_succ_iterator* iter = ecs_->aut->succ_iter(dest); @@ -173,7 +174,7 @@ namespace spot // 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); + (void) ecs_->h->filter(dest); // If we have reached a dead component, ignore it. if (*i == -1) @@ -233,8 +234,10 @@ namespace spot ////////////////////////////////////////////////////////////////////// - emptiness_check_shy::emptiness_check_shy(const tgba* a) - : emptiness_check(a) + emptiness_check_shy::emptiness_check_shy(const tgba* a, + const numbered_state_heap_factory* + nshf) + : emptiness_check(a, nshf) { } @@ -285,7 +288,7 @@ namespace spot succ_queue::iterator q = queue.begin(); while (q != queue.end()) { - int* i = ecs_->h.find(q->s); + int* i = ecs_->h->find(q->s); if (!i) { // Skip unknown states. @@ -342,13 +345,13 @@ namespace spot for (succ_queue::iterator q = queue.begin(); q != queue.end(); ++q) { - int* i = ecs_->h.find(q->s); + int* i = ecs_->h->find(q->s); if (!i) delete q->s; else // Delete the state if it is a clone // of a state in the heap. - (void) ecs_->h.filter(q->s); + (void) ecs_->h->filter(q->s); } todo.pop(); } @@ -358,7 +361,7 @@ namespace spot // 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); + (void) ecs_->h->filter(q->s); // Remove that state from the queue, so we do not // recurse into it. succ_queue::iterator old = q++; @@ -379,7 +382,7 @@ 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); + int* i = ecs_->h->find(curr); assert(i); assert(!ecs_->root.empty()); if (ecs_->root.top().index == *i) @@ -399,7 +402,7 @@ namespace spot // stacks. successor succ = queue.front(); queue.pop_front(); - ecs_->h.insert(succ.s, ++num); + ecs_->h->insert(succ.s, ++num); ecs_->root.push(num); arc.push(succ.acc); todo.push(pair_state_successors(succ.s, succ_queue())); diff --git a/src/tgbaalgos/gtec/gtec.hh b/src/tgbaalgos/gtec/gtec.hh index 01589d537..003e93b87 100644 --- a/src/tgbaalgos/gtec/gtec.hh +++ b/src/tgbaalgos/gtec/gtec.hh @@ -70,7 +70,9 @@ namespace spot class emptiness_check { public: - emptiness_check(const tgba* a); + emptiness_check(const tgba* a, + const numbered_state_heap_factory* nshf + = numbered_state_heap_hash_map_factory::instance()); virtual ~emptiness_check(); /// Check whether the automaton's language is empty. @@ -103,7 +105,9 @@ namespace spot class emptiness_check_shy : public emptiness_check { public: - emptiness_check_shy(const tgba* a); + emptiness_check_shy(const tgba* a, + const numbered_state_heap_factory* nshf + = numbered_state_heap_hash_map_factory::instance()); virtual ~emptiness_check_shy(); virtual bool check(); diff --git a/src/tgbaalgos/gtec/nsheap.cc b/src/tgbaalgos/gtec/nsheap.cc index 0e5c1e062..3dde0dcf1 100644 --- a/src/tgbaalgos/gtec/nsheap.cc +++ b/src/tgbaalgos/gtec/nsheap.cc @@ -130,4 +130,22 @@ namespace spot delete s; return i->first; } + + numbered_state_heap_hash_map_factory::numbered_state_heap_hash_map_factory() + : numbered_state_heap_factory() + { + } + + numbered_state_heap_hash_map* + numbered_state_heap_hash_map_factory::build() const + { + return new numbered_state_heap_hash_map(); + } + + const numbered_state_heap_hash_map_factory* + numbered_state_heap_hash_map_factory::instance() + { + static numbered_state_heap_hash_map_factory f; + return &f; + } } diff --git a/src/tgbaalgos/gtec/nsheap.hh b/src/tgbaalgos/gtec/nsheap.hh index 408074da5..468604b88 100644 --- a/src/tgbaalgos/gtec/nsheap.hh +++ b/src/tgbaalgos/gtec/nsheap.hh @@ -81,6 +81,14 @@ namespace spot virtual const state* filter(const state* s) const = 0; }; + /// Abstract factory for numbered_state_heap + class numbered_state_heap_factory + { + public: + virtual ~numbered_state_heap_factory() {} + virtual numbered_state_heap* build() const = 0; + }; + /// A straightforward implementation of numbered_state_heap with a hash map. class numbered_state_heap_hash_map : public numbered_state_heap { @@ -103,6 +111,23 @@ namespace spot friend class numbered_state_heap_hash_map_const_iterator; }; + + /// \brief Factory for numbered_state_heap_hash_map. + /// + /// This class is a singleton. Retrieve the instance using instance(). + class numbered_state_heap_hash_map_factory: + public numbered_state_heap_factory + { + public: + virtual numbered_state_heap_hash_map* build() const; + + /// Get the unique instance of this class. + static const numbered_state_heap_hash_map_factory* instance(); + protected: + virtual ~numbered_state_heap_hash_map_factory() {} + numbered_state_heap_hash_map_factory(); + }; + } #endif // SPOT_TGBAALGOS_GTEC_NSHEAP_HH diff --git a/src/tgbaalgos/gtec/status.cc b/src/tgbaalgos/gtec/status.cc index 49783139c..0e0ae8f28 100644 --- a/src/tgbaalgos/gtec/status.cc +++ b/src/tgbaalgos/gtec/status.cc @@ -23,19 +23,23 @@ namespace spot { - emptiness_check_status::emptiness_check_status(const tgba* aut) - : aut(aut) + emptiness_check_status::emptiness_check_status + (const tgba* aut, + const numbered_state_heap_factory* nshf) + : aut(aut), + h(nshf->build()) { } emptiness_check_status::~emptiness_check_status() { + delete h; } void emptiness_check_status::print_stats(std::ostream& os) const { - os << h.size() << " unique states visited" << std::endl; + os << h->size() << " unique states visited" << std::endl; os << root.size() << " strongly connected components in search stack" << std::endl; diff --git a/src/tgbaalgos/gtec/status.hh b/src/tgbaalgos/gtec/status.hh index 9b0f79256..b0d416548 100644 --- a/src/tgbaalgos/gtec/status.hh +++ b/src/tgbaalgos/gtec/status.hh @@ -37,12 +37,13 @@ namespace spot class emptiness_check_status { public: - emptiness_check_status(const tgba* aut); + emptiness_check_status(const tgba* aut, + const numbered_state_heap_factory* nshf); ~emptiness_check_status(); const tgba* aut; scc_stack root; - numbered_state_heap_hash_map h; ///< Map of visited states. + numbered_state_heap* h; ///< Heap of visited states. /// Output statistics about this object. void print_stats(std::ostream& os) const;