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

* src/tgbaalgo/semptinesscheck.hh (scc_stack): New class, extracted

from ...
(emptiness_check): ... here.
(emptiness_check::root): Redefined as a scc_stack object.
* src/tgbaalgos/emptinesscheck.cc: Adjust.
parent 7fd9459a
2004-04-13 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgo/semptinesscheck.hh (scc_stack): New class, extracted
from ...
(emptiness_check): ... here.
(emptiness_check::root): Redefined as a scc_stack object.
* src/tgbaalgos/emptinesscheck.cc: Adjust.
2004-04-05 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/emptinesscheck.cc (emptiness_check::complete_cycle):
......
......@@ -29,14 +29,45 @@
namespace spot
{
typedef std::pair<const spot::state*, tgba_succ_iterator*> pair_state_iter;
emptiness_check::connected_component::connected_component(int i)
scc_stack::connected_component::connected_component(int i)
{
index = i;
condition = bddfalse;
}
scc_stack::connected_component&
scc_stack::top()
{
return s.top();
}
void
scc_stack::pop()
{
s.pop();
}
void
scc_stack::push(int index)
{
s.push(connected_component(index));
}
size_t
scc_stack::size() const
{
return s.size();
}
bool
scc_stack::empty() const
{
return s.empty();
}
typedef std::pair<const spot::state*, tgba_succ_iterator*> pair_state_iter;
bool
emptiness_check::connected_component_set::has_state(const state* s) const
{
......@@ -136,7 +167,7 @@ namespace spot
{
state* init = aut_->get_init_state();
h[init] = 1;
root.push(connected_component(1));
root.push(1);
arc.push(bddfalse);
tgba_succ_iterator* iter = aut_->succ_iter(init);
iter->first();
......@@ -195,7 +226,7 @@ namespace spot
// Yes. Number it, stack it, and register its successors
// for later processing.
h[dest] = ++num;
root.push(connected_component(num));
root.push(num);
arc.push(acc);
tgba_succ_iterator* iter = aut_->succ_iter(dest);
iter->first();
......@@ -411,7 +442,7 @@ namespace spot
successor succ = queue.front();
queue.pop_front();
h[succ.s] = ++num;
root.push(connected_component(num));
root.push(num);
arc.push(succ.acc);
todo.push(pair_state_successors(succ.s, succ_queue()));
succ_queue& new_queue = todo.top().second;
......
......@@ -32,6 +32,30 @@
namespace spot
{
class scc_stack
{
public:
struct connected_component
{
// During the Depth path we keep the connected component that we met.
public:
connected_component(int index = -1);
int index;
/// The bdd condition is the union of all acceptance conditions of
/// transitions which connect the states of the connected component.
bdd condition;
};
connected_component& top();
void pop();
void push(int index);
size_t size() const;
bool empty() const;
std::stack<connected_component> s;
};
/// \brief Check whether the language of an automate is empty.
///
/// This is based on the following paper.
......@@ -100,19 +124,7 @@ namespace spot
private:
struct connected_component
{
// During the Depth path we keep the connected component that we met.
public:
connected_component(int index = -1);
int index;
/// The bdd condition is the union of all acceptance conditions of
/// transitions which connect the states of the connected component.
bdd condition;
};
struct connected_component_set: public connected_component
struct connected_component_set: public scc_stack::connected_component
{
typedef Sgi::hash_set<const state*,
state_ptr_hash, state_ptr_equal> set_type;
......@@ -125,7 +137,7 @@ namespace spot
};
const tgba* aut_;
std::stack<connected_component> root;
scc_stack root;
state_sequence suffix;
cycle_path period;
......
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