* src/tgbaalgos/cutscc.cc: Cosmetics.
This commit is contained in:
Alexandre Duret-Lutz
parent
26f48b1df2
commit
7f31d70345
1 changed files with 197 additions and 203 deletions
|
|
@ -1,5 +1,5 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2009, 2011, 2012 Laboratoire de Recherche et
|
// Copyright (C) 2009, 2011, 2012, 2013 Laboratoire de Recherche et
|
||||||
// Developpement de l'Epita (LRDE).
|
// Developpement de l'Epita (LRDE).
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
|
|
@ -25,214 +25,208 @@
|
||||||
|
|
||||||
namespace spot
|
namespace spot
|
||||||
{
|
{
|
||||||
tgba* cut_scc(const tgba* a, const scc_map& m,
|
namespace
|
||||||
const std::set<unsigned>& s)
|
|
||||||
{
|
{
|
||||||
tgba_explicit_string* sub_a = new tgba_explicit_string(a->get_dict());
|
static tgba*
|
||||||
state* cur = a->get_init_state();
|
cut_scc(const tgba* a, const scc_map& m,
|
||||||
std::queue<state*> tovisit;
|
const std::set<unsigned>& s)
|
||||||
typedef Sgi::hash_set<const state*,
|
|
||||||
state_ptr_hash, state_ptr_equal> hash_type;
|
|
||||||
// Setup
|
|
||||||
hash_type seen;
|
|
||||||
unsigned scc_number;
|
|
||||||
std::string cur_format = a->format_state(cur);
|
|
||||||
std::set<unsigned>::iterator it;
|
|
||||||
// Check if we have at least one accepting SCC.
|
|
||||||
for (it = s.begin(); it != s.end() && !m.accepting(*it); ++it)
|
|
||||||
continue;
|
|
||||||
assert(it != s.end());
|
|
||||||
tovisit.push(cur);
|
|
||||||
seen.insert(cur);
|
|
||||||
sub_a->add_state(cur_format);
|
|
||||||
sub_a->copy_acceptance_conditions_of(a);
|
|
||||||
// If the initial is not part of one of the desired SCC, exit
|
|
||||||
assert(s.find(m.scc_of_state(cur)) != s.end());
|
|
||||||
|
|
||||||
// Perform BFS to visit each state.
|
|
||||||
while (!tovisit.empty())
|
|
||||||
{
|
{
|
||||||
cur = tovisit.front();
|
tgba_explicit_string* sub_a = new tgba_explicit_string(a->get_dict());
|
||||||
tovisit.pop();
|
state* cur = a->get_init_state();
|
||||||
tgba_succ_iterator* sit = a->succ_iter(cur);
|
std::queue<state*> tovisit;
|
||||||
for (sit->first(); !sit->done(); sit->next())
|
typedef Sgi::hash_set<const state*,
|
||||||
{
|
state_ptr_hash, state_ptr_equal> hash_type;
|
||||||
cur_format = a->format_state(cur);
|
// Setup
|
||||||
state* dst = sit->current_state();
|
hash_type seen;
|
||||||
std::string dst_format = a->format_state(dst);
|
unsigned scc_number;
|
||||||
scc_number= m.scc_of_state(dst);
|
std::string cur_format = a->format_state(cur);
|
||||||
// Is the successor included in one of the desired SCC ?
|
std::set<unsigned>::iterator it;
|
||||||
if (s.find(scc_number) != s.end())
|
// Check if we have at least one accepting SCC.
|
||||||
|
for (it = s.begin(); it != s.end() && !m.accepting(*it); ++it)
|
||||||
|
continue;
|
||||||
|
assert(it != s.end());
|
||||||
|
tovisit.push(cur);
|
||||||
|
seen.insert(cur);
|
||||||
|
sub_a->add_state(cur_format);
|
||||||
|
sub_a->copy_acceptance_conditions_of(a);
|
||||||
|
// If the initial is not part of one of the desired SCC, exit
|
||||||
|
assert(s.find(m.scc_of_state(cur)) != s.end());
|
||||||
|
|
||||||
|
// Perform BFS to visit each state.
|
||||||
|
while (!tovisit.empty())
|
||||||
{
|
{
|
||||||
if (seen.find(dst) == seen.end())
|
cur = tovisit.front();
|
||||||
{
|
tovisit.pop();
|
||||||
tovisit.push(dst);
|
tgba_succ_iterator* sit = a->succ_iter(cur);
|
||||||
seen.insert(dst); // has_state?
|
for (sit->first(); !sit->done(); sit->next())
|
||||||
}
|
{
|
||||||
|
cur_format = a->format_state(cur);
|
||||||
|
state* dst = sit->current_state();
|
||||||
|
std::string dst_format = a->format_state(dst);
|
||||||
|
scc_number= m.scc_of_state(dst);
|
||||||
|
// Is the successor included in one of the desired SCC ?
|
||||||
|
if (s.find(scc_number) != s.end())
|
||||||
|
{
|
||||||
|
if (seen.find(dst) == seen.end())
|
||||||
|
{
|
||||||
|
tovisit.push(dst);
|
||||||
|
seen.insert(dst); // has_state?
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
dst->destroy();
|
||||||
|
}
|
||||||
|
state_explicit_string::transition* t =
|
||||||
|
sub_a->create_transition(cur_format, dst_format);
|
||||||
|
sub_a->add_conditions(t, sit->current_condition());
|
||||||
|
bdd acc = sit->current_acceptance_conditions();
|
||||||
|
sub_a->add_acceptance_conditions(t, acc);
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
dst->destroy();
|
||||||
|
}
|
||||||
|
}
|
||||||
|
delete sit;
|
||||||
|
}
|
||||||
|
|
||||||
|
hash_type::iterator it2;
|
||||||
|
// Free visited states.
|
||||||
|
for (it2 = seen.begin(); it2 != seen.end(); ++it2)
|
||||||
|
(*it2)->destroy();
|
||||||
|
return sub_a;
|
||||||
|
}
|
||||||
|
|
||||||
|
static unsigned set_distance(const sccs_set* s1,
|
||||||
|
const sccs_set* s2,
|
||||||
|
const std::vector<unsigned>& scc_sizes)
|
||||||
|
{
|
||||||
|
// Compute the distance between two sets.
|
||||||
|
// Formula is : distance = size(s1) + size(s2) - size(s1 inter s2)
|
||||||
|
std::set<unsigned>::iterator it;
|
||||||
|
std::set<unsigned> result;
|
||||||
|
unsigned inter_sum = 0;
|
||||||
|
std::set_intersection(s1->sccs.begin(), s1->sccs.end(),
|
||||||
|
s2->sccs.begin(), s2->sccs.end(),
|
||||||
|
std::inserter(result, result.begin()));
|
||||||
|
for (it = result.begin(); it != result.end(); ++it)
|
||||||
|
inter_sum += scc_sizes[*it];
|
||||||
|
return s1->size + s2->size - 2*inter_sum;
|
||||||
|
}
|
||||||
|
|
||||||
|
static sccs_set* set_union(sccs_set* s1,
|
||||||
|
sccs_set* s2,
|
||||||
|
const std::vector<unsigned>& scc_sizes)
|
||||||
|
{
|
||||||
|
// Perform the union of two sets.
|
||||||
|
sccs_set* result = new sccs_set;
|
||||||
|
set_union(s1->sccs.begin(), s1->sccs.end(),
|
||||||
|
s2->sccs.begin(), s2->sccs.end(),
|
||||||
|
std::inserter(result->sccs, result->sccs.begin()));
|
||||||
|
result->size = 0;
|
||||||
|
std::set<unsigned>::iterator it;
|
||||||
|
for (it = result->sccs.begin(); it != result->sccs.end(); ++it)
|
||||||
|
result->size += scc_sizes[*it];
|
||||||
|
delete s1;
|
||||||
|
return result;
|
||||||
|
}
|
||||||
|
|
||||||
|
struct recurse_data
|
||||||
|
{
|
||||||
|
std::set<unsigned> seen;
|
||||||
|
std::vector<std::vector<sccs_set* > >* rec_paths;
|
||||||
|
};
|
||||||
|
|
||||||
|
static void find_paths_sub(unsigned init_scc,
|
||||||
|
const scc_map& m,
|
||||||
|
recurse_data& d,
|
||||||
|
const std::vector<unsigned>& scc_sizes)
|
||||||
|
{
|
||||||
|
// Find all the paths from the initial states to an accepting SCC
|
||||||
|
// We need two stacks, one to track the current state, the other to track
|
||||||
|
// the current iterator of this state.
|
||||||
|
std::stack<scc_map::succ_type::const_iterator> it_stack;
|
||||||
|
std::stack<unsigned> scc_stack;
|
||||||
|
std::vector<const scc_map::succ_type*> scc_succ;
|
||||||
|
unsigned scc_count = m.scc_count();
|
||||||
|
scc_succ.reserve(scc_count);
|
||||||
|
d.seen.insert(init_scc);
|
||||||
|
unsigned i;
|
||||||
|
for (i = 0; i < scc_count; ++i)
|
||||||
|
scc_succ.push_back(&(m.succ(i)));
|
||||||
|
// Setup the two stacks with the initial SCC.
|
||||||
|
scc_stack.push(init_scc);
|
||||||
|
it_stack.push(scc_succ[init_scc]->begin());
|
||||||
|
while (!scc_stack.empty())
|
||||||
|
{
|
||||||
|
unsigned cur_scc = scc_stack.top();
|
||||||
|
scc_stack.pop();
|
||||||
|
d.seen.insert(cur_scc);
|
||||||
|
scc_map::succ_type::const_iterator it;
|
||||||
|
// Find the next unvisited successor.
|
||||||
|
for (it = it_stack.top(); it != scc_succ[cur_scc]->end()
|
||||||
|
&& d.seen.find(it->first) != d.seen.end(); ++it)
|
||||||
|
continue;
|
||||||
|
it_stack.pop();
|
||||||
|
// If there are no successors and if the SCC is not accepting, this is
|
||||||
|
// an useless path. Throw it away.
|
||||||
|
if (scc_succ[cur_scc]->begin() == scc_succ[cur_scc]->end()
|
||||||
|
&& !m.accepting(cur_scc))
|
||||||
|
continue;
|
||||||
|
std::vector<std::vector<sccs_set* > >* rec_paths = d.rec_paths;
|
||||||
|
// Is there a successor to process ?
|
||||||
|
if (it != scc_succ[cur_scc]->end())
|
||||||
|
{
|
||||||
|
// Yes, add it to the stack for later processing.
|
||||||
|
unsigned dst = it->first;
|
||||||
|
scc_stack.push(cur_scc);
|
||||||
|
++it;
|
||||||
|
it_stack.push(it);
|
||||||
|
if (d.seen.find(dst) == d.seen.end())
|
||||||
|
{
|
||||||
|
scc_stack.push(dst);
|
||||||
|
it_stack.push(scc_succ[dst]->begin());
|
||||||
|
}
|
||||||
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
dst->destroy();
|
// No, all successors have been processed, update the current SCC.
|
||||||
}
|
for (it = scc_succ[cur_scc]->begin();
|
||||||
state_explicit_string::transition* t =
|
it != scc_succ[cur_scc]->end(); ++it)
|
||||||
sub_a->create_transition(cur_format, dst_format);
|
{
|
||||||
sub_a->add_conditions(t, sit->current_condition());
|
unsigned dst = it->first;
|
||||||
sub_a->
|
std::vector<sccs_set*>::iterator lit;
|
||||||
add_acceptance_conditions(t,
|
// Extend all the reachable paths by adding the current SCC.
|
||||||
sit->current_acceptance_conditions());
|
for (lit = (*rec_paths)[dst].begin();
|
||||||
|
lit != (*rec_paths)[dst].end(); ++lit)
|
||||||
|
{
|
||||||
|
sccs_set* path = new sccs_set;
|
||||||
|
path->sccs = (*lit)->sccs;
|
||||||
|
path->size = (*lit)->size + scc_sizes[cur_scc];
|
||||||
|
path->sccs.insert(path->sccs.begin(), cur_scc);
|
||||||
|
(*rec_paths)[cur_scc].push_back(path);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
bool has_succ = false;
|
||||||
|
for (it = scc_succ[cur_scc]->begin();
|
||||||
|
it != scc_succ[cur_scc]->end() && !has_succ; ++it)
|
||||||
|
{
|
||||||
|
has_succ = !(*rec_paths)[it->first].empty();
|
||||||
|
}
|
||||||
|
// Create a new path iff the SCC is accepting and not included
|
||||||
|
// in another path.
|
||||||
|
if (m.accepting(cur_scc) && !has_succ)
|
||||||
|
{
|
||||||
|
sccs_set* path = new sccs_set;
|
||||||
|
path->size = scc_sizes[cur_scc];
|
||||||
|
path->sccs.insert(path->sccs.begin(), cur_scc);
|
||||||
|
(*rec_paths)[cur_scc].push_back(path);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
}
|
}
|
||||||
else
|
return;
|
||||||
{
|
|
||||||
dst->destroy();
|
|
||||||
}
|
|
||||||
}
|
|
||||||
delete sit;
|
|
||||||
}
|
}
|
||||||
|
|
||||||
hash_type::iterator it2;
|
|
||||||
// Free visited states.
|
|
||||||
for (it2 = seen.begin(); it2 != seen.end(); ++it2)
|
|
||||||
(*it2)->destroy();
|
|
||||||
return sub_a;
|
|
||||||
}
|
|
||||||
|
|
||||||
void print_set(const sccs_set* s)
|
|
||||||
{
|
|
||||||
std::cout << "set : ";
|
|
||||||
std::set<unsigned>::iterator vit;
|
|
||||||
for (vit = s->sccs.begin(); vit != s->sccs.end(); ++vit)
|
|
||||||
std::cout << *vit << " ";
|
|
||||||
std::cout << std::endl;
|
|
||||||
}
|
|
||||||
|
|
||||||
unsigned set_distance(const sccs_set* s1,
|
|
||||||
const sccs_set* s2,
|
|
||||||
const std::vector<unsigned>& scc_sizes)
|
|
||||||
{
|
|
||||||
// Compute the distance between two sets.
|
|
||||||
// Formula is : distance = size(s1) + size(s2) - size(s1 inter s2)
|
|
||||||
std::set<unsigned>::iterator it;
|
|
||||||
std::set<unsigned> result;
|
|
||||||
unsigned inter_sum = 0;
|
|
||||||
std::set_intersection(s1->sccs.begin(), s1->sccs.end(),
|
|
||||||
s2->sccs.begin(), s2->sccs.end(),
|
|
||||||
std::inserter(result, result.begin()));
|
|
||||||
for (it = result.begin(); it != result.end(); ++it)
|
|
||||||
inter_sum += scc_sizes[*it];
|
|
||||||
return s1->size + s2->size - 2*inter_sum;
|
|
||||||
}
|
|
||||||
|
|
||||||
sccs_set* set_union(sccs_set* s1,
|
|
||||||
sccs_set* s2,
|
|
||||||
const std::vector<unsigned>& scc_sizes)
|
|
||||||
{
|
|
||||||
// Perform the union of two sets.
|
|
||||||
sccs_set* result = new sccs_set;
|
|
||||||
set_union(s1->sccs.begin(), s1->sccs.end(),
|
|
||||||
s2->sccs.begin(), s2->sccs.end(),
|
|
||||||
std::inserter(result->sccs, result->sccs.begin()));
|
|
||||||
result->size = 0;
|
|
||||||
std::set<unsigned>::iterator it;
|
|
||||||
for (it = result->sccs.begin(); it != result->sccs.end(); ++it)
|
|
||||||
result->size += scc_sizes[*it];
|
|
||||||
delete s1;
|
|
||||||
return result;
|
|
||||||
}
|
|
||||||
|
|
||||||
struct recurse_data
|
|
||||||
{
|
|
||||||
std::set<unsigned> seen;
|
|
||||||
std::vector<std::vector<sccs_set* > >* rec_paths;
|
|
||||||
};
|
|
||||||
|
|
||||||
void find_paths_sub(unsigned init_scc,
|
|
||||||
const scc_map& m,
|
|
||||||
recurse_data& d,
|
|
||||||
const std::vector<unsigned>& scc_sizes)
|
|
||||||
{
|
|
||||||
// Find all the paths from the initial states to an accepting SCC
|
|
||||||
// We need two stacks, one to track the current state, the other to track
|
|
||||||
// the current iterator of this state.
|
|
||||||
std::stack<scc_map::succ_type::const_iterator> it_stack;
|
|
||||||
std::stack<unsigned> scc_stack;
|
|
||||||
std::vector<const scc_map::succ_type*> scc_succ;
|
|
||||||
unsigned scc_count = m.scc_count();
|
|
||||||
scc_succ.reserve(scc_count);
|
|
||||||
d.seen.insert(init_scc);
|
|
||||||
unsigned i;
|
|
||||||
for (i = 0; i < scc_count; ++i)
|
|
||||||
scc_succ.push_back(&(m.succ(i)));
|
|
||||||
// Setup the two stacks with the initial SCC.
|
|
||||||
scc_stack.push(init_scc);
|
|
||||||
it_stack.push(scc_succ[init_scc]->begin());
|
|
||||||
while (!scc_stack.empty())
|
|
||||||
{
|
|
||||||
unsigned cur_scc = scc_stack.top();
|
|
||||||
scc_stack.pop();
|
|
||||||
d.seen.insert(cur_scc);
|
|
||||||
scc_map::succ_type::const_iterator it;
|
|
||||||
// Find the next unvisited successor.
|
|
||||||
for (it = it_stack.top(); it != scc_succ[cur_scc]->end()
|
|
||||||
&& d.seen.find(it->first) != d.seen.end(); ++it)
|
|
||||||
continue;
|
|
||||||
it_stack.pop();
|
|
||||||
// If there are no successors and if the SCC is not accepting, this is
|
|
||||||
// an useless path. Throw it away.
|
|
||||||
if (scc_succ[cur_scc]->begin() == scc_succ[cur_scc]->end()
|
|
||||||
&& !m.accepting(cur_scc))
|
|
||||||
continue;
|
|
||||||
std::vector<std::vector<sccs_set* > >* rec_paths = d.rec_paths;
|
|
||||||
// Is there a successor to process ?
|
|
||||||
if (it != scc_succ[cur_scc]->end())
|
|
||||||
{
|
|
||||||
// Yes, add it to the stack for later processing.
|
|
||||||
unsigned dst = it->first;
|
|
||||||
scc_stack.push(cur_scc);
|
|
||||||
++it;
|
|
||||||
it_stack.push(it);
|
|
||||||
if (d.seen.find(dst) == d.seen.end())
|
|
||||||
{
|
|
||||||
scc_stack.push(dst);
|
|
||||||
it_stack.push(scc_succ[dst]->begin());
|
|
||||||
}
|
|
||||||
}
|
|
||||||
else
|
|
||||||
{
|
|
||||||
// No, all successors have been processed, update the current SCC.
|
|
||||||
for (it = scc_succ[cur_scc]->begin();
|
|
||||||
it != scc_succ[cur_scc]->end(); ++it)
|
|
||||||
{
|
|
||||||
unsigned dst = it->first;
|
|
||||||
std::vector<sccs_set*>::iterator lit;
|
|
||||||
// Extend all the reachable paths by adding the current SCC.
|
|
||||||
for (lit = (*rec_paths)[dst].begin();
|
|
||||||
lit != (*rec_paths)[dst].end(); ++lit)
|
|
||||||
{
|
|
||||||
sccs_set* path = new sccs_set;
|
|
||||||
path->sccs = (*lit)->sccs;
|
|
||||||
path->size = (*lit)->size + scc_sizes[cur_scc];
|
|
||||||
path->sccs.insert(path->sccs.begin(), cur_scc);
|
|
||||||
(*rec_paths)[cur_scc].push_back(path);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
bool has_succ = false;
|
|
||||||
for (it = scc_succ[cur_scc]->begin();
|
|
||||||
it != scc_succ[cur_scc]->end() && !has_succ; ++it)
|
|
||||||
{
|
|
||||||
has_succ = !(*rec_paths)[it->first].empty();
|
|
||||||
}
|
|
||||||
// Create a new path iff the SCC is accepting and not included
|
|
||||||
// in another path.
|
|
||||||
if (m.accepting(cur_scc) && !has_succ)
|
|
||||||
{
|
|
||||||
sccs_set* path = new sccs_set;
|
|
||||||
path->size = scc_sizes[cur_scc];
|
|
||||||
path->sccs.insert(path->sccs.begin(), cur_scc);
|
|
||||||
(*rec_paths)[cur_scc].push_back(path);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
}
|
|
||||||
return;
|
|
||||||
}
|
}
|
||||||
|
|
||||||
std::vector<std::vector<sccs_set* > >* find_paths(tgba* a, const scc_map& m)
|
std::vector<std::vector<sccs_set* > >* find_paths(tgba* a, const scc_map& m)
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue