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

* src/tgbaalgos/emptinesscheck.hh (explicit_connected_component):

New class.
(counter_example::connected_component_set): Rename as ...
(connected_component_hash_set): ... this, and inherit from
explicit_connected_component.
(counter_example::accepting_path, counter_example::complete_cycle):
parent 1ea3c2ce
2004-04-13 Alexandre Duret-Lutz <adl@src.lip6.fr> 2004-04-13 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/emptinesscheck.hh (explicit_connected_component):
New class.
(counter_example::connected_component_set): Rename as ...
(connected_component_hash_set): ... this, and inherit from
explicit_connected_component.
(counter_example::accepting_path, counter_example::complete_cycle):
* src/tgbaalgos/emptinesscheck.hh * src/tgbaalgos/emptinesscheck.hh
(counter_example::connected_component_set::has_state): Return (counter_example::connected_component_set::has_state): Return
a const state* and behave like h_filt. a const state* and behave like h_filt.
......
...@@ -492,7 +492,7 @@ namespace spot ...@@ -492,7 +492,7 @@ namespace spot
////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////
const state* const state*
counter_example::connected_component_set::has_state(const state* s) const connected_component_hash_set::has_state(const state* s) const
{ {
set_type::const_iterator it = states.find(s); set_type::const_iterator it = states.find(s);
if (it != states.end()) if (it != states.end())
...@@ -505,6 +505,12 @@ namespace spot ...@@ -505,6 +505,12 @@ namespace spot
return 0; return 0;
} }
void
connected_component_hash_set::insert(const state* s)
{
states.insert(s);
}
////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////
counter_example::counter_example(const emptiness_check_status* ecs) counter_example::counter_example(const emptiness_check_status* ecs)
...@@ -516,11 +522,13 @@ namespace spot ...@@ -516,11 +522,13 @@ namespace spot
scc_stack::stack_type root = ecs_->root.s; scc_stack::stack_type root = ecs_->root.s;
int comp_size = root.size(); int comp_size = root.size();
// Transform the stack of connected component into an array. // Transform the stack of connected component into an array.
connected_component_set* scc = new connected_component_set[comp_size]; explicit_connected_component** scc =
new (explicit_connected_component*)[comp_size];
for (int j = comp_size - 1; 0 <= j; --j) for (int j = comp_size - 1; 0 <= j; --j)
{ {
scc[j].index = root.top().index; scc[j] = new connected_component_hash_set();
scc[j].condition = root.top().condition; scc[j]->index = root.top().index;
scc[j]->condition = root.top().condition;
root.pop(); root.pop();
} }
assert(root.empty()); assert(root.empty());
...@@ -538,9 +546,9 @@ namespace spot ...@@ -538,9 +546,9 @@ namespace spot
// Find the SCC this state belongs to. // Find the SCC this state belongs to.
int j; int j;
for (j = 1; j < comp_size; ++j) for (j = 1; j < comp_size; ++j)
if (index < scc[j].index) if (index < scc[j]->index)
break; break;
scc[j - 1].states.insert(i->first); scc[j - 1]->insert(i->first);
} }
suffix.push_front(ecs_->h_filt(ecs_->aut->get_init_state())); suffix.push_front(ecs_->h_filt(ecs_->aut->get_init_state()));
...@@ -579,12 +587,12 @@ namespace spot ...@@ -579,12 +587,12 @@ namespace spot
const state* dest = i->current_state(); const state* dest = i->current_state();
// Are we leaving this SCC? // Are we leaving this SCC?
const state* h_dest = scc[k].has_state(dest); const state* h_dest = scc[k]->has_state(dest);
if (!h_dest) if (!h_dest)
{ {
// If we have found a state in the next SCC. // If we have found a state in the next SCC.
// Unwind the path and populate SUFFIX. // Unwind the path and populate SUFFIX.
h_dest = scc[k+1].has_state(dest); h_dest = scc[k+1]->has_state(dest);
if (h_dest) if (h_dest)
{ {
state_sequence seq; state_sequence seq;
...@@ -611,8 +619,8 @@ namespace spot ...@@ -611,8 +619,8 @@ namespace spot
if (father.find(h_dest) == father.end()) if (father.find(h_dest) == father.end())
{ {
todo.push_back(pair_state_iter(h_dest, todo.push_back
ecs_->aut->succ_iter(dest))); (pair_state_iter(h_dest, ecs_->aut->succ_iter(h_dest)));
father[h_dest] = src; father[h_dest] = src;
} }
} }
...@@ -621,13 +629,16 @@ namespace spot ...@@ -621,13 +629,16 @@ namespace spot
} }
accepting_path(scc[comp_size - 1], suffix.back(), accepting_path(scc[comp_size - 1], suffix.back(),
scc[comp_size - 1].condition); scc[comp_size - 1]->condition);
for (int j = comp_size - 1; 0 <= j; --j)
delete scc[j];
delete[] scc; delete[] scc;
} }
void void
counter_example::complete_cycle(const connected_component_set& scc, counter_example::complete_cycle(const explicit_connected_component* scc,
const state* from, const state* from,
const state* to) const state* to)
{ {
...@@ -660,7 +671,7 @@ namespace spot ...@@ -660,7 +671,7 @@ namespace spot
const state* dest = i->current_state(); const state* dest = i->current_state();
// Do not escape this SCC or visit a state already visited. // Do not escape this SCC or visit a state already visited.
const state* h_dest = scc.has_state(dest); const state* h_dest = scc->has_state(dest);
if (!h_dest) if (!h_dest)
{ {
delete dest; delete dest;
...@@ -722,11 +733,13 @@ namespace spot ...@@ -722,11 +733,13 @@ namespace spot
} }
void void
counter_example::accepting_path(const connected_component_set& scc, counter_example::accepting_path(const explicit_connected_component* scc,
const state* start, bdd acc_to_traverse) const state* start, bdd acc_to_traverse)
{ {
// State seen during the DFS. // State seen during the DFS.
connected_component_set::set_type seen; typedef Sgi::hash_set<const state*,
state_ptr_hash, state_ptr_equal> set_type;
set_type seen;
// DFS stack. // DFS stack.
std::stack<triplet> todo; std::stack<triplet> todo;
...@@ -768,7 +781,7 @@ namespace spot ...@@ -768,7 +781,7 @@ namespace spot
// We must not escape the current SCC. // We must not escape the current SCC.
const state* dest = iter->current_state(); const state* dest = iter->current_state();
const state* h_dest = scc.has_state(dest); const state* h_dest = scc->has_state(dest);
if (!h_dest) if (!h_dest)
{ {
delete dest; delete dest;
......
...@@ -154,6 +154,33 @@ namespace spot ...@@ -154,6 +154,33 @@ namespace spot
//@} //@}
class explicit_connected_component: public scc_stack::connected_component
{
public:
virtual ~explicit_connected_component() {};
/// \brief Check if the SCC contains states \a s.
///
/// Return the representative of \a s in the SCC, and delete \a
/// s if it is different (acting like
/// emptiness_check_status::h_filt), or 0 otherwise.
virtual const state* has_state(const state* s) const = 0;
/// Insert a new state in the SCC.
virtual void insert(const state* s) = 0;
};
class connected_component_hash_set: public explicit_connected_component
{
public:
virtual ~connected_component_hash_set() {};
virtual const state* has_state(const state* s) const;
virtual void insert(const state* s);
protected:
typedef Sgi::hash_set<const state*,
state_ptr_hash, state_ptr_equal> set_type;
set_type states;
};
class counter_example class counter_example
{ {
public: public:
...@@ -175,30 +202,14 @@ namespace spot ...@@ -175,30 +202,14 @@ namespace spot
void print_stats(std::ostream& os) const; void print_stats(std::ostream& os) const;
protected: protected:
struct connected_component_set: public scc_stack::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;
/// \brief Check if the SCC contains states \a s.
///
/// Return the representative of \a s in the SCC, and delete \a
/// s if it is different (acting like
/// emptiness_check_status::h_filt), or 0 otherwise.
const state* has_state(const state* s) const;
};
/// Called by counter_example to find a path which traverses all /// Called by counter_example to find a path which traverses all
/// acceptance conditions in the accepted SCC. /// acceptance conditions in the accepted SCC.
void accepting_path (const connected_component_set& scc, void accepting_path (const explicit_connected_component* scc,
const state* start, bdd acc_to_traverse); const state* start, bdd acc_to_traverse);
/// Complete a cycle that caraterise the period of the counter /// Complete a cycle that caraterise the period of the counter
/// example. Append a sequence to the path given by accepting_path. /// example. Append a sequence to the path given by accepting_path.
void complete_cycle(const connected_component_set& scc, void complete_cycle(const explicit_connected_component* scc,
const state* from, const state* to); const state* from, const state* to);
private: private:
......
Supports Markdown
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