Commit a2cd1de2 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

* 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.
parent 579c343e
2004-04-14 Alexandre Duret-Lutz <adl@src.lip6.fr>
* 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,
......
......@@ -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
......
......@@ -28,9 +28,10 @@ namespace spot
typedef std::pair<const spot::state*, tgba_succ_iterator*> 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()));
......
......@@ -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();
......
......@@ -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;
}
}
......@@ -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
......@@ -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;
......
......@@ -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;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment