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

* src/tgbaalgos/emptinesscheck.cc (connected_component): Split

into ...
(emptiness_check::connected_component,
emptiness_check::connected_component_set): ... these.
* src/tgbaalgos/emptinesscheck.cc: Adjust.
parent dd720e97
2003-10-27 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/emptinesscheck.cc (connected_component): Split
into ...
(emptiness_check::connected_component,
emptiness_check::connected_component_set): ... these.
* src/tgbaalgos/emptinesscheck.cc: Adjust.
* src/tgbaalgos/emptinesscheck.cc (emptiness_check::h_filt,
emptiness_check::~emptiness_check) New methods.
(emptiness_check::check): Release all iterators in todo on exit.
......
......@@ -10,16 +10,16 @@ namespace spot
typedef std::pair<const spot::state*, tgba_succ_iterator*> pair_state_iter;
typedef std::pair<pair_state_iter, bdd> triplet;
connected_component::connected_component(int i)
emptiness_check::connected_component::connected_component(int i)
{
index = i;
condition = bddfalse;
}
bool
connected_component::has_state(const state* s) const
emptiness_check::connected_component_set::has_state(const state* s) const
{
return state_set.find(s) != state_set.end();
return states.find(s) != states.end();
}
......@@ -289,10 +289,11 @@ namespace spot
int comp_size = root.size();
// Transform the stack of connected component into an array.
connected_component* scc = new connected_component[comp_size];
connected_component_set* scc = new connected_component_set[comp_size];
for (int j = comp_size - 1; 0 <= j; --j)
{
scc[j] = root.top();
scc[j].index = root.top().index;
scc[j].condition = root.top().condition;
root.pop();
}
assert(root.empty());
......@@ -311,7 +312,7 @@ namespace spot
for (j = 1; j < comp_size; ++j)
if (index < scc[j].index)
break;
scc[j - 1].state_set.insert(i->first);
scc[j - 1].states.insert(i->first);
}
suffix.push_front(h_filt(aut_->get_init_state()));
......@@ -398,7 +399,7 @@ namespace spot
}
void
emptiness_check::complete_cycle(const connected_component& comp_path,
emptiness_check::complete_cycle(const connected_component_set& comp_path,
const state* from_state,
const state* to_state)
{
......@@ -452,7 +453,7 @@ namespace spot
// FIXME: Derecursive this function.
void
emptiness_check::accepting_path(const connected_component& comp_path,
emptiness_check::accepting_path(const connected_component_set& comp_path,
const state* start_path, bdd to_accept)
{
hash_type seen_priority;
......
......@@ -11,28 +11,6 @@
namespace spot
{
class connected_component
{
// During the Depth path we keep the connected component that we met.
public:
connected_component(int index = -1);
public:
int index;
/// The bdd condition is the union of all accepting condition of
/// transitions which connect the states of the connected component.
bdd condition;
typedef Sgi::hash_set<const state*,
state_ptr_hash, state_ptr_equal> set_type;
/// for the counter example we need to know all the states of the
/// component
set_type state_set;
/// Check if the SCC contains states \a s.
bool has_state(const state* s) const;
};
/// \brief Check whether the language of an automate is empty.
///
/// This is based on the following paper.
......@@ -73,6 +51,31 @@ namespace spot
const tgba* restrict = 0) const;
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 accepting condition of
/// transitions which connect the states of the connected component.
bdd condition;
};
struct connected_component_set: public connected_component
{
typedef Sgi::hash_set<const state*,
state_ptr_hash, state_ptr_equal> set_type;
/// for the counter example we need to know all the states of the
/// component
set_type states;
/// Check if the SCC contains states \a s.
bool has_state(const state* s) const;
};
const tgba* aut_;
std::stack<connected_component> root;
state_sequence suffix;
......@@ -98,12 +101,12 @@ namespace spot
/// Called by counter_example to find a path which traverses all
/// accepting conditions in the accepted SCC.
void accepting_path (const connected_component& comp_path,
void accepting_path (const connected_component_set& comp_path,
const state* start_path, bdd to_accept);
/// Complete a cycle that caraterise the period of the counter
/// example. Append a sequence to the path given by accepting_path.
void complete_cycle(const connected_component& comp_path,
void complete_cycle(const connected_component_set& comp_path,
const state* from_state,const state* to_state);
};
}
......
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