alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

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

Browse source 
extracted from ...
(emptiness_check): ... here.
* src/tgbaalgos/emptinesscheck.cc: Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2004-04-13 08:53:10 +00:00
parent f8321633b7
commit 5eb2cf2cac
3 changed files with 131 additions and 98 deletions
Download patch file Download diff file Expand all files Collapse all files

5
ChangeLog
View file

@ -1,5 +1,10 @@
2004-04-13 Alexandre Duret-Lutz <adl@src.lip6.fr> 2004-04-13 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgo/semptinesscheck.hh (emptiness_check_status): New class,
extracted from ...
(emptiness_check): ... here.
* src/tgbaalgos/emptinesscheck.cc: Adjust.
* src/tgbaalgo/semptinesscheck.hh (scc_stack): New class, extracted * src/tgbaalgo/semptinesscheck.hh (scc_stack): New class, extracted
from ... from ...
(emptiness_check): ... here. (emptiness_check): ... here.

190
src/tgbaalgos/emptinesscheck.cc
View file

@ -66,21 +66,14 @@ namespace spot
return s.empty(); return s.empty();
} }
typedef std::pair<const spot::state*, tgba_succ_iterator*> pair_state_iter; //////////////////////////////////////////////////////////////////////
bool emptiness_check_status::emptiness_check_status(const tgba* aut)
emptiness_check::connected_component_set::has_state(const state* s) const : aut(aut)
{
return states.find(s) != states.end();
}
emptiness_check::emptiness_check(const tgba* a)
: aut_(a)
{ {
} }
emptiness_check::~emptiness_check() emptiness_check_status::~emptiness_check_status()
{ {
// Free keys in H. // Free keys in H.
hash_type::iterator i = h.begin(); hash_type::iterator i = h.begin();
@ -94,7 +87,7 @@ namespace spot
} }
const state* const state*
emptiness_check::h_filt(const state* s) const emptiness_check_status::h_filt(const state* s) const
{ {
hash_type::const_iterator i = h.find(s); hash_type::const_iterator i = h.find(s);
assert(i != h.end()); assert(i != h.end());
@ -103,6 +96,32 @@ namespace spot
return i->first; return i->first;
} }
//////////////////////////////////////////////////////////////////////
typedef std::pair<const spot::state*, tgba_succ_iterator*> pair_state_iter;
bool
emptiness_check::connected_component_set::has_state(const state* s) const
{
return states.find(s) != states.end();
}
emptiness_check::emptiness_check(const tgba* a)
{
ecs_ = new emptiness_check_status(a);
}
emptiness_check::~emptiness_check()
{
delete ecs_;
}
void void
emptiness_check::remove_component(const state* from) emptiness_check::remove_component(const state* from)
{ {
@ -115,10 +134,10 @@ namespace spot
// (FROM should be in H, otherwise it means all reachable // (FROM should be in H, otherwise it means all reachable
// states from FROM have already been removed and there is no // states from FROM have already been removed and there is no
// point in calling remove_component.) // point in calling remove_component.)
hash_type::iterator hi = h.find(from); emptiness_check_status::hash_type::iterator hi = ecs_->h.find(from);
assert(hi->second != -1); assert(hi->second != -1);
hi->second = -1; hi->second = -1;
tgba_succ_iterator* i = aut_->succ_iter(from); tgba_succ_iterator* i = ecs_->aut->succ_iter(from);
for (;;) for (;;)
{ {
@ -126,13 +145,13 @@ namespace spot
for (i->first(); !i->done(); i->next()) for (i->first(); !i->done(); i->next())
{ {
state* s = i->current_state(); state* s = i->current_state();
hash_type::iterator hi = h.find(s); emptiness_check_status::hash_type::iterator hi = ecs_->h.find(s);
assert(hi != h.end()); assert(hi != ecs_->h.end());
if (hi->second != -1) if (hi->second != -1)
{ {
hi->second = -1; hi->second = -1;
to_remove.push(aut_->succ_iter(s)); to_remove.push(ecs_->aut->succ_iter(s));
} }
delete s; delete s;
} }
@ -165,18 +184,18 @@ namespace spot
// Setup depth-first search from the initial state. // Setup depth-first search from the initial state.
{ {
state* init = aut_->get_init_state(); state* init = ecs_->aut->get_init_state();
h[init] = 1; ecs_->h[init] = 1;
root.push(1); ecs_->root.push(1);
arc.push(bddfalse); arc.push(bddfalse);
tgba_succ_iterator* iter = aut_->succ_iter(init); tgba_succ_iterator* iter = ecs_->aut->succ_iter(init);
iter->first(); iter->first();
todo.push(pair_state_iter(init, iter)); todo.push(pair_state_iter(init, iter));
} }
while (!todo.empty()) while (!todo.empty())
{ {
assert(root.size() == arc.size()); assert(ecs_->root.size() == arc.size());
// We are looking at the next successor in SUCC. // We are looking at the next successor in SUCC.
tgba_succ_iterator* succ = todo.top().second; tgba_succ_iterator* succ = todo.top().second;
@ -193,14 +212,14 @@ namespace spot
// When backtracking the root of an SCC, we must also // When backtracking the root of an SCC, we must also
// remove that SCC from the ARC/ROOT stacks. We must // remove that SCC from the ARC/ROOT stacks. We must
// discard from H all reachable states from this SCC. // discard from H all reachable states from this SCC.
hash_type::iterator i = h.find(curr); emptiness_check_status::hash_type::iterator i = ecs_->h.find(curr);
assert(i != h.end()); assert(i != ecs_->h.end());
assert(!root.empty()); assert(!ecs_->root.empty());
if (root.top().index == i->second) if (ecs_->root.top().index == i->second)
{ {
assert(!arc.empty()); assert(!arc.empty());
arc.pop(); arc.pop();
root.pop(); ecs_->root.pop();
remove_component(curr); remove_component(curr);
} }
@ -220,15 +239,15 @@ namespace spot
// We do not need SUCC from now on. // We do not need SUCC from now on.
// Are we going to a new state? // Are we going to a new state?
hash_type::iterator i = h.find(dest); emptiness_check_status::hash_type::iterator i = ecs_->h.find(dest);
if (i == h.end()) if (i == ecs_->h.end())
{ {
// Yes. Number it, stack it, and register its successors // Yes. Number it, stack it, and register its successors
// for later processing. // for later processing.
h[dest] = ++num; ecs_->h[dest] = ++num;
root.push(num); ecs_->root.push(num);
arc.push(acc); arc.push(acc);
tgba_succ_iterator* iter = aut_->succ_iter(dest); tgba_succ_iterator* iter = ecs_->aut->succ_iter(dest);
iter->first(); iter->first();
todo.push(pair_state_iter(dest, iter)); todo.push(pair_state_iter(dest, iter));
continue; continue;
@ -256,24 +275,24 @@ namespace spot
// top of ROOT that have an index greater to the one of // top of ROOT that have an index greater to the one of
// the SCC of S2 (called the "threshold"). // the SCC of S2 (called the "threshold").
int threshold = i->second; int threshold = i->second;
while (threshold < root.top().index) while (threshold < ecs_->root.top().index)
{ {
assert(!root.empty()); assert(!ecs_->root.empty());
assert(!arc.empty()); assert(!arc.empty());
acc |= root.top().condition; acc |= ecs_->root.top().condition;
acc |= arc.top(); acc |= arc.top();
root.pop(); ecs_->root.pop();
arc.pop(); arc.pop();
} }
// Note that we do not always have // Note that we do not always have
// threshold == root.top().index // threshold == ecs_->root.top().index
// after this loop, the SCC whose index is threshold might have // after this loop, the SCC whose index is threshold might have
// been merged with a lower SCC. // been merged with a lower SCC.
// Accumulate all acceptance conditions into the merged SCC. // Accumulate all acceptance conditions into the merged SCC.
root.top().condition |= acc; ecs_->root.top().condition |= acc;
if (root.top().condition == aut_->all_acceptance_conditions()) if (ecs_->root.top().condition == ecs_->aut->all_acceptance_conditions())
{ {
// We have found an accepting SCC. // We have found an accepting SCC.
// Release all iterators in TODO. // Release all iterators in TODO.
@ -316,11 +335,11 @@ namespace spot
// Setup depth-first search from the initial state. // Setup depth-first search from the initial state.
todo.push(pair_state_successors(0, succ_queue())); todo.push(pair_state_successors(0, succ_queue()));
todo.top().second.push_front(successor(bddtrue, aut_->get_init_state())); todo.top().second.push_front(successor(bddtrue, ecs_->aut->get_init_state()));
for (;;) for (;;)
{ {
assert(root.size() == arc.size()); assert(ecs_->root.size() == arc.size());
// Get the successors of the current state. // Get the successors of the current state.
succ_queue& queue = todo.top().second; succ_queue& queue = todo.top().second;
@ -331,8 +350,8 @@ namespace spot
succ_queue::iterator q = queue.begin(); succ_queue::iterator q = queue.begin();
while (q != queue.end()) while (q != queue.end())
{ {
hash_type::iterator i = h.find(q->s); emptiness_check_status::hash_type::iterator i = ecs_->h.find(q->s);
if (i == h.end()) if (i == ecs_->h.end())
{ {
// Skip unknown states. // Skip unknown states.
++q; ++q;
@ -358,25 +377,25 @@ namespace spot
// (called the "threshold"). // (called the "threshold").
int threshold = i->second; int threshold = i->second;
bdd acc = q->acc; bdd acc = q->acc;
while (threshold < root.top().index) while (threshold < ecs_->root.top().index)
{ {
assert(!root.empty()); assert(!ecs_->root.empty());
assert(!arc.empty()); assert(!arc.empty());
acc |= root.top().condition; acc |= ecs_->root.top().condition;
acc |= arc.top(); acc |= arc.top();
root.pop(); ecs_->root.pop();
arc.pop(); arc.pop();
} }
// Note that we do not always have // Note that we do not always have
// threshold == root.top().index // threshold == ecs_->root.top().index
// after this loop, the SCC whose index is threshold // after this loop, the SCC whose index is threshold
// might have been merged with a lower SCC. // might have been merged with a lower SCC.
// Accumulate all acceptance conditions into the // Accumulate all acceptance conditions into the
// merged SCC. // merged SCC.
root.top().condition |= acc; ecs_->root.top().condition |= acc;
if (root.top().condition == aut_->all_acceptance_conditions()) if (ecs_->root.top().condition == ecs_->aut->all_acceptance_conditions())
{ {
// We have found an accepting SCC. Clean up TODO. // We have found an accepting SCC. Clean up TODO.
// We must delete all states of apparing in TODO // We must delete all states of apparing in TODO
@ -387,8 +406,8 @@ namespace spot
for (succ_queue::iterator q = queue.begin(); for (succ_queue::iterator q = queue.begin();
q != queue.end(); ++q) q != queue.end(); ++q)
{ {
hash_type::iterator i = h.find(q->s); emptiness_check_status::hash_type::iterator i = ecs_->h.find(q->s);
if (i == h.end() || i->first != q->s) if (i == ecs_->h.end() || i->first != q->s)
delete q->s; delete q->s;
} }
todo.pop(); todo.pop();
@ -421,14 +440,14 @@ namespace spot
// When backtracking the root of an SCC, we must also // When backtracking the root of an SCC, we must also
// remove that SCC from the ARC/ROOT stacks. We must // remove that SCC from the ARC/ROOT stacks. We must
// discard from H all reachable states from this SCC. // discard from H all reachable states from this SCC.
hash_type::iterator i = h.find(curr); emptiness_check_status::hash_type::iterator i = ecs_->h.find(curr);
assert(i != h.end()); assert(i != ecs_->h.end());
assert(!root.empty()); assert(!ecs_->root.empty());
if (root.top().index == i->second) if (ecs_->root.top().index == i->second)
{ {
assert(!arc.empty()); assert(!arc.empty());
arc.pop(); arc.pop();
root.pop(); ecs_->root.pop();
remove_component(curr); remove_component(curr);
} }
continue; continue;
@ -441,12 +460,12 @@ namespace spot
// stacks. // stacks.
successor succ = queue.front(); successor succ = queue.front();
queue.pop_front(); queue.pop_front();
h[succ.s] = ++num; ecs_->h[succ.s] = ++num;
root.push(num); ecs_->root.push(num);
arc.push(succ.acc); arc.push(succ.acc);
todo.push(pair_state_successors(succ.s, succ_queue())); todo.push(pair_state_successors(succ.s, succ_queue()));
succ_queue& new_queue = todo.top().second; succ_queue& new_queue = todo.top().second;
tgba_succ_iterator* iter = aut_->succ_iter(succ.s); tgba_succ_iterator* iter = ecs_->aut->succ_iter(succ.s);
for (iter->first(); ! iter->done(); iter->next()) for (iter->first(); ! iter->done(); iter->next())
new_queue.push_back(successor(iter->current_acceptance_conditions(), new_queue.push_back(successor(iter->current_acceptance_conditions(),
iter->current_state())); iter->current_state()));
@ -459,21 +478,21 @@ namespace spot
emptiness_check::print_result(std::ostream& os, const tgba* restrict) const emptiness_check::print_result(std::ostream& os, const tgba* restrict) const
{ {
os << "Prefix:" << std::endl; os << "Prefix:" << std::endl;
const bdd_dict* d = aut_->get_dict(); const bdd_dict* d = ecs_->aut->get_dict();
for (state_sequence::const_iterator i_se = suffix.begin(); for (state_sequence::const_iterator i_se = suffix.begin();
i_se != suffix.end(); ++i_se) i_se != suffix.end(); ++i_se)
{ {
os << " "; os << " ";
if (restrict) if (restrict)
{ {
const state* s = aut_->project_state(*i_se, restrict); const state* s = ecs_->aut->project_state(*i_se, restrict);
assert(s); assert(s);
os << restrict->format_state(s) << std::endl; os << restrict->format_state(s) << std::endl;
delete s; delete s;
} }
else else
{ {
os << aut_->format_state(*i_se) << std::endl; os << ecs_->aut->format_state(*i_se) << std::endl;
} }
} }
os << "Cycle:" <<std::endl; os << "Cycle:" <<std::endl;
@ -484,14 +503,14 @@ namespace spot
os << " "; os << " ";
if (restrict) if (restrict)
{ {
const state* s = aut_->project_state(it->first, restrict); const state* s = ecs_->aut->project_state(it->first, restrict);
assert(s); assert(s);
os << restrict->format_state(s) << std::endl; os << restrict->format_state(s) << std::endl;
delete s; delete s;
} }
else else
{ {
os << aut_->format_state(it->first) << std::endl; os << ecs_->aut->format_state(it->first) << std::endl;
} }
} }
return os; return os;
@ -500,22 +519,23 @@ namespace spot
void void
emptiness_check::counter_example() emptiness_check::counter_example()
{ {
assert(!root.empty()); assert(!ecs_->root.empty());
assert(suffix.empty()); assert(suffix.empty());
int comp_size = root.size(); int comp_size = ecs_->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]; connected_component_set* scc = new connected_component_set[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].index = ecs_->root.top().index;
scc[j].condition = root.top().condition; scc[j].condition = ecs_->root.top().condition;
root.pop(); ecs_->root.pop();
} }
assert(root.empty()); assert(ecs_->root.empty());
// Build the set of states for all SCCs. // Build the set of states for all SCCs.
for (hash_type::iterator i = h.begin(); i != h.end(); ++i) for (emptiness_check_status::hash_type::iterator i = ecs_->h.begin();
i != ecs_->h.end(); ++i)
{ {
int index = i->second; int index = i->second;
// Skip states from dead SCCs. // Skip states from dead SCCs.
@ -531,7 +551,7 @@ namespace spot
scc[j - 1].states.insert(i->first); scc[j - 1].states.insert(i->first);
} }
suffix.push_front(h_filt(aut_->get_init_state())); suffix.push_front(ecs_->h_filt(ecs_->aut->get_init_state()));
// We build a path trough each SCC in the stack. For the // We build a path trough each SCC in the stack. For the
// first SCC, the starting state is the initial state of the // first SCC, the starting state is the initial state of the
@ -552,7 +572,7 @@ namespace spot
// Initial state of the BFS. // Initial state of the BFS.
const state* start = suffix.back(); const state* start = suffix.back();
{ {
tgba_succ_iterator* i = aut_->succ_iter(start); tgba_succ_iterator* i = ecs_->aut->succ_iter(start);
todo.push_back(pair_state_iter(start, i)); todo.push_back(pair_state_iter(start, i));
} }
@ -575,7 +595,7 @@ namespace spot
{ {
state_sequence seq; state_sequence seq;
seq.push_front(h_filt(dest)); seq.push_front(ecs_->h_filt(dest));
while (src->compare(start)) while (src->compare(start))
{ {
seq.push_front(src); seq.push_front(src);
@ -596,11 +616,11 @@ namespace spot
continue; continue;
} }
dest = h_filt(dest); dest = ecs_->h_filt(dest);
if (father.find(dest) == father.end()) if (father.find(dest) == father.end())
{ {
todo.push_back(pair_state_iter(dest, todo.push_back(pair_state_iter(dest,
aut_->succ_iter(dest))); ecs_->aut->succ_iter(dest)));
father[dest] = src; father[dest] = src;
} }
} }
@ -634,7 +654,7 @@ namespace spot
// Initial state. // Initial state.
{ {
tgba_succ_iterator* i = aut_->succ_iter(from); tgba_succ_iterator* i = ecs_->aut->succ_iter(from);
todo.push_back(pair_state_iter(from, i)); todo.push_back(pair_state_iter(from, i));
} }
@ -653,7 +673,7 @@ namespace spot
delete dest; delete dest;
continue; continue;
} }
dest = h_filt(dest); dest = ecs_->h_filt(dest);
bdd cond = i->current_condition(); bdd cond = i->current_condition();
@ -681,7 +701,7 @@ namespace spot
} }
// Common case: record backlinks and continue BFS. // Common case: record backlinks and continue BFS.
todo.push_back(pair_state_iter(dest, aut_->succ_iter(dest))); todo.push_back(pair_state_iter(dest, ecs_->aut->succ_iter(dest)));
father[dest] = state_proposition(src, cond); father[dest] = state_proposition(src, cond);
} }
delete i; delete i;
@ -719,7 +739,7 @@ namespace spot
{ {
// Initial state. // Initial state.
{ {
tgba_succ_iterator* i = aut_->succ_iter(start); tgba_succ_iterator* i = ecs_->aut->succ_iter(start);
i->first(); i->first();
todo.push(triplet(start, i, bddfalse)); todo.push(triplet(start, i, bddfalse));
seen.insert(start); seen.insert(start);
@ -761,7 +781,7 @@ namespace spot
continue; continue;
} }
dest = h_filt(dest); dest = ecs_->h_filt(dest);
bdd acc = iter->current_acceptance_conditions() | todo.top().acc; bdd acc = iter->current_acceptance_conditions() | todo.top().acc;
path.push_back(state_proposition(dest, iter->current_condition())); path.push_back(state_proposition(dest, iter->current_condition()));
@ -771,7 +791,7 @@ namespace spot
if (seen.find(dest) == seen.end()) if (seen.find(dest) == seen.end())
{ {
// A new state: continue the DFS. // A new state: continue the DFS.
tgba_succ_iterator* di = aut_->succ_iter(dest); tgba_succ_iterator* di = ecs_->aut->succ_iter(dest);
di->first(); di->first();
todo.push(triplet(dest, di, acc)); todo.push(triplet(dest, di, acc));
seen.insert(dest); seen.insert(dest);
@ -845,10 +865,10 @@ namespace spot
void void
emptiness_check::print_stats(std::ostream& os) const emptiness_check::print_stats(std::ostream& os) const
{ {
os << h.size() << " unique states visited" << std::endl; os << ecs_->h.size() << " unique states visited" << std::endl;
os << suffix.size() << " states in suffix" << std::endl; os << suffix.size() << " states in suffix" << std::endl;
os << period.size() << " states in period" << std::endl; os << period.size() << " states in period" << std::endl;
os << root.size() os << ecs_->root.size()
<< " strongly connected components in search stack" << " strongly connected components in search stack"
<< std::endl; << std::endl;
} }

34
src/tgbaalgos/emptinesscheck.hh
View file

@ -56,6 +56,26 @@ namespace spot
std::stack<connected_component> s; std::stack<connected_component> s;
}; };
class emptiness_check_status
{
public:
emptiness_check_status(const tgba* aut);
~emptiness_check_status();
/// \brief Return a state which is equal to \a s, but is in \c h,
/// and free \a s if it is different. Doing so simplify memory
/// management, because we don't have to track which state need
/// to be kept or deallocated: all key in \c h should last for
/// the whole life of the emptiness_check.
const state* h_filt(const state* s) const;
const tgba* aut;
scc_stack root;
typedef Sgi::hash_map<const state*, int,
state_ptr_hash, state_ptr_equal> hash_type;
hash_type h; ///< Map of visited states.
};
/// \brief Check whether the language of an automate is empty. /// \brief Check whether the language of an automate is empty.
/// ///
/// This is based on the following paper. /// This is based on the following paper.
@ -136,22 +156,10 @@ namespace spot
bool has_state(const state* s) const; bool has_state(const state* s) const;
}; };
const tgba* aut_; emptiness_check_status* ecs_;
scc_stack root;
state_sequence suffix; state_sequence suffix;
cycle_path period; cycle_path period;
typedef Sgi::hash_map<const state*, int,
state_ptr_hash, state_ptr_equal> hash_type;
hash_type h; ///< Map of visited states.
/// \brief Return a state which is equal to \a s, but is in \c h,
/// and free \a s if it is different. Doing so simplify memory
/// management, because we don't have to track which state need
/// to be kept or deallocated: all key in \c h should last for
/// the whole life of the emptiness_check.
const state* h_filt(const state* s) const;
/// \brief Remove a strongly component from the hash. /// \brief Remove a strongly component from the hash.
/// ///
/// This function remove all accessible state from a given /// This function remove all accessible state from a given