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

* src/tgbaalgos/emptiness_stats.hh (ars_statistics): New class.

Browse source 
* src/tgbaalgos/ndfs_result.hh (ndfs_result): Inherit from
ars_statistics.
(ndfs_result::dfs): Call inc_ars_states().
(ndfs_result::test_path, ndfs_result::min_path): Update ars_statistics.
* tgbaalgos/gtec/ce.hh (couvreur99_check_result): Inherit
from ars_statistics.
* tgbaalgos/gtec/ce.cc (shortest_path,
couvreur99_check_result::accepting_cycle::scc_bfs):
Update ars_statistics.
* src/tgbatest/randtgba.cc: Display statistics about accepting run
search.
This commit is contained in:
Alexandre Duret-Lutz 2005-01-03 15:49:50 +00:00
parent 6feb92090d
commit 55c08790fd
6 changed files with 249 additions and 121 deletions
Download patch file Download diff file Expand all files Collapse all files

13
ChangeLog
View file

@ -1,5 +1,18 @@
2005-01-03 Alexandre Duret-Lutz <adl@src.lip6.fr> 2005-01-03 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/emptiness_stats.hh (ars_statistics): New class.
* src/tgbaalgos/ndfs_result.hh (ndfs_result): Inherit from
ars_statistics.
(ndfs_result::dfs): Call inc_ars_states().
(ndfs_result::test_path, ndfs_result::min_path): Update ars_statistics.
* tgbaalgos/gtec/ce.hh (couvreur99_check_result): Inherit
from ars_statistics.
* tgbaalgos/gtec/ce.cc (shortest_path,
couvreur99_check_result::accepting_cycle::scc_bfs):
Update ars_statistics.
* src/tgbatest/randtgba.cc: Display statistics about accepting run
search.
* src/tgbaalgos/bfssteps.hh (bfs_steps::finalize): Document. * src/tgbaalgos/bfssteps.hh (bfs_steps::finalize): Document.
* src/tgbaalgos/emptiness_stats.hh (accs_statistics): New class. * src/tgbaalgos/emptiness_stats.hh (accs_statistics): New class.

35
src/tgbaalgos/emptiness_stats.hh
View file

@ -28,6 +28,7 @@ namespace spot
/// \addtogroup ec_misc /// \addtogroup ec_misc
/// @{ /// @{
/// Emptiness-check statistics
class ec_statistics class ec_statistics
{ {
public : public :
@ -87,19 +88,45 @@ namespace spot
} }
private : private :
unsigned states_; /// number of disctint visited states unsigned states_; /// number of disctint visited states
unsigned transitions_; /// number of visited transitions unsigned transitions_; /// number of visited transitions
unsigned depth_; /// maximal depth of the stack(s) unsigned depth_; /// maximal depth of the stack(s)
unsigned max_depth_; /// maximal depth of the stack(s) unsigned max_depth_; /// maximal depth of the stack(s)
}; };
/// Accepting Cycle Search Space statistics /// Accepting Cycle Search Space statistics
class acss_statistics class acss_statistics
{ {
public: public:
/// Number of states in the search space for the accepting cycle.
virtual int acss_states() const = 0; virtual int acss_states() const = 0;
}; };
/// Accepting Run Search statistics.
class ars_statistics
{
public:
ars_statistics()
: states_(0)
{
}
void
inc_ars_states()
{
++states_;
}
int
ars_states() const
{
return states_;
}
private:
unsigned states_; /// number of states visited
};
/// @} /// @}
} }

20
src/tgbaalgos/gtec/ce.cc
View file

@ -32,8 +32,10 @@ namespace spot
class shortest_path: public bfs_steps class shortest_path: public bfs_steps
{ {
public: public:
shortest_path(const state_set* t, const couvreur99_check_status* ecs) shortest_path(const state_set* t,
: bfs_steps(ecs->aut), target(t), ecs(ecs) const couvreur99_check_status* ecs,
couvreur99_check_result* r)
: bfs_steps(ecs->aut), target(t), ecs(ecs), r(r)
{ {
} }
@ -46,6 +48,7 @@ namespace spot
const state* const state*
filter(const state* s) filter(const state* s)
{ {
r->inc_ars_states();
numbered_state_heap::state_index_p sip = ecs->h->find(s); numbered_state_heap::state_index_p sip = ecs->h->find(s);
// Ignore unknown states ... // Ignore unknown states ...
if (!sip.first) if (!sip.first)
@ -69,6 +72,7 @@ namespace spot
state_set seen; state_set seen;
const state_set* target; const state_set* target;
const couvreur99_check_status* ecs; const couvreur99_check_status* ecs;
couvreur99_check_result* r;
}; };
} }
@ -109,7 +113,7 @@ namespace spot
for (tgba_run::steps::const_iterator i = run_->cycle.begin(); for (tgba_run::steps::const_iterator i = run_->cycle.begin();
i != run_->cycle.end(); ++i) i != run_->cycle.end(); ++i)
ss.insert(i->s); ss.insert(i->s);
shortest_path shpath(&ss, ecs_); shortest_path shpath(&ss, ecs_, this);
const state* prefix_start = ecs_->aut->get_init_state(); const state* prefix_start = ecs_->aut->get_init_state();
// There are two cases: either the initial state is already on // There are two cases: either the initial state is already on
@ -161,11 +165,14 @@ namespace spot
struct scc_bfs: bfs_steps struct scc_bfs: bfs_steps
{ {
const couvreur99_check_status* ecs; const couvreur99_check_status* ecs;
couvreur99_check_result* r;
bdd& acc_to_traverse; bdd& acc_to_traverse;
int scc_root; int scc_root;
scc_bfs(const couvreur99_check_status* ecs, scc_bfs(const couvreur99_check_status* ecs,
bdd& acc_to_traverse) couvreur99_check_result* r, bdd& acc_to_traverse)
: bfs_steps(ecs->aut), ecs(ecs), acc_to_traverse(acc_to_traverse), : bfs_steps(ecs->aut), ecs(ecs), r(r),
acc_to_traverse(acc_to_traverse),
scc_root(ecs->root.s.top().index) scc_root(ecs->root.s.top().index)
{ {
} }
@ -173,6 +180,7 @@ namespace spot
virtual const state* virtual const state*
filter(const state* s) filter(const state* s)
{ {
r->inc_ars_states();
numbered_state_heap::state_index_p sip = ecs->h->find(s); numbered_state_heap::state_index_p sip = ecs->h->find(s);
// Ignore unknown states. // Ignore unknown states.
if (!sip.first) if (!sip.first)
@ -200,7 +208,7 @@ namespace spot
return false; return false;
} }
} b(ecs_, acc_to_traverse); } b(ecs_, this, acc_to_traverse);
substart = b.search(substart, run_->cycle); substart = b.search(substart, run_->cycle);
} }

3
src/tgbaalgos/gtec/ce.hh
View file

@ -31,7 +31,8 @@ namespace spot
/// Compute a counter example from a spot::couvreur99_check_status /// Compute a counter example from a spot::couvreur99_check_status
class couvreur99_check_result: class couvreur99_check_result:
public emptiness_check_result, public emptiness_check_result,
public acss_statistics public acss_statistics,
public ars_statistics
{ {
public: public:
couvreur99_check_result(const couvreur99_check_status* ecs); couvreur99_check_result(const couvreur99_check_status* ecs);

225
src/tgbaalgos/ndfs_result.hh
View file

@ -62,129 +62,127 @@ namespace spot
typedef std::list<stack_item> stack_type; typedef std::list<stack_item> stack_type;
template <typename ndfs_search, typename heap> template <typename ndfs_search, typename heap>
class ndfs_result : public emptiness_check_result class ndfs_result:
public emptiness_check_result,
public ars_statistics
{ {
public: public:
ndfs_result(const ndfs_search& ms) ndfs_result(const ndfs_search& ms)
: emptiness_check_result(ms.automaton()), ms_(ms), h_(ms_.get_heap()) : emptiness_check_result(ms.automaton()), ms_(ms), h_(ms_.get_heap())
{ {
} }
virtual ~ndfs_result() virtual ~ndfs_result()
{ {
} }
virtual tgba_run* accepting_run() virtual tgba_run* accepting_run()
{ {
const stack_type& stb = ms_.get_st_blue(); const stack_type& stb = ms_.get_st_blue();
const stack_type& str = ms_.get_st_red(); const stack_type& str = ms_.get_st_red();
assert(!stb.empty()); assert(!stb.empty());
bdd covered_acc = bddfalse; bdd covered_acc = bddfalse;
accepting_transitions_list acc_trans; accepting_transitions_list acc_trans;
const state* start; const state* start;
if (str.empty()) start = stb.front().s->clone();
start = stb.front().s->clone(); if (!str.empty())
else {
{ if (a_->number_of_acceptance_conditions() == 0)
start = str.front().s->clone(); {
if (a_->number_of_acceptance_conditions() == 0) // take arbitrarily the last transition on the red stack
{ stack_type::const_iterator i, j;
// take arbitrarily the last transition on the red stack i = j = str.begin(); ++i;
stack_type::const_iterator i, j; if (i == str.end())
i = j = str.begin(); ++i; i = stb.begin();
if (i == str.end()) transition t = { i->s->clone(), j->label, j->acc,
i = stb.begin(); j->s->clone() };
transition t = { i->s->clone(), j->label, j->acc, assert(h_.has_been_visited(t.source));
j->s->clone() }; assert(h_.has_been_visited(t.dest));
assert(h_.has_been_visited(t.source)); acc_trans.push_back(t);
assert(h_.has_been_visited(t.dest)); }
acc_trans.push_back(t); else
} {
else // ignore the prefix
{ stack_type::const_reverse_iterator i, j;
// ignore the prefix
stack_type::const_reverse_iterator i, j;
i = j = stb.rbegin(); ++j; i = j = stb.rbegin(); ++j;
for (; i->s->compare(start) != 0; ++i, ++j) while (i->s->compare(start) != 0)
{ ++i, ++j;
}
stack_type::const_reverse_iterator end = stb.rend();
for (; j != end; ++i, ++j)
{
if ((covered_acc & j->acc) != j->acc)
{
transition t = { i->s->clone(), j->label, j->acc,
j->s->clone() };
assert(h_.has_been_visited(t.source));
assert(h_.has_been_visited(t.dest));
acc_trans.push_back(t);
covered_acc |= j->acc;
}
}
stack_type::const_reverse_iterator end = stb.rend(); j = str.rbegin();
for (; j != end; ++i, ++j) if ((covered_acc & j->acc) != j->acc)
{ {
if ((covered_acc & j->acc) != j->acc) transition t = { i->s->clone(), j->label, j->acc,
{ j->s->clone() };
transition t = { i->s->clone(), j->label, j->acc, assert(h_.has_been_visited(t.source));
j->s->clone() }; assert(h_.has_been_visited(t.dest));
assert(h_.has_been_visited(t.source)); acc_trans.push_back(t);
assert(h_.has_been_visited(t.dest)); covered_acc |= j->acc;
acc_trans.push_back(t); }
covered_acc |= j->acc;
}
}
j = str.rbegin(); i = j; ++j;
if ((covered_acc & j->acc) != j->acc) end = str.rend();
{ for (; j != end; ++i, ++j)
transition t = { i->s->clone(), j->label, j->acc, {
j->s->clone() }; if ((covered_acc & j->acc) != j->acc)
assert(h_.has_been_visited(t.source)); {
assert(h_.has_been_visited(t.dest)); transition t = { i->s->clone(), j->label, j->acc,
acc_trans.push_back(t); j->s->clone() };
covered_acc |= j->acc; assert(h_.has_been_visited(t.source));
} assert(h_.has_been_visited(t.dest));
acc_trans.push_back(t);
covered_acc |= j->acc;
}
}
}
}
i = j; ++j; if (a_->all_acceptance_conditions() != covered_acc)
end = str.rend(); {
for (; j != end; ++i, ++j) bool b = dfs(start, acc_trans, covered_acc);
{ assert(b);
if ((covered_acc & j->acc) != j->acc) (void) b;
{ }
transition t = { i->s->clone(), j->label, j->acc,
j->s->clone() };
assert(h_.has_been_visited(t.source));
assert(h_.has_been_visited(t.dest));
acc_trans.push_back(t);
covered_acc |= j->acc;
}
}
}
}
if (a_->all_acceptance_conditions() != covered_acc) delete start;
{
bool b = dfs(start, acc_trans, covered_acc);
assert(b);
(void) b;
}
delete start; assert(!acc_trans.empty());
assert(!acc_trans.empty()); tgba_run* run = new tgba_run;
// construct run->cycle from acc_trans.
construct_cycle(run, acc_trans);
// construct run->prefix (a minimal path from the initial state to any
// state of run->cycle) and adjust the cycle to the state reached by the
// prefix.
construct_prefix(run);
tgba_run* run = new tgba_run; for (typename accepting_transitions_list::const_iterator i =
// construct run->cycle from acc_trans. acc_trans.begin(); i != acc_trans.end(); ++i)
construct_cycle(run, acc_trans); {
// construct run->prefix (a minimal path from the initial state to any delete i->source;
// state of run->cycle) and adjust the cycle to the state reached by the delete i->dest;
// prefix. }
construct_prefix(run);
for (typename accepting_transitions_list::const_iterator i = return run;
acc_trans.begin(); i != acc_trans.end(); ++i) }
{
delete i->source;
delete i->dest;
}
return run;
}
private: private:
const ndfs_search& ms_; const ndfs_search& ms_;
@ -244,6 +242,7 @@ namespace spot
if (!f.it->done()) if (!f.it->done())
{ {
const state *s_prime = f.it->current_state(); const state *s_prime = f.it->current_state();
inc_ars_states();
ndfsr_trace << " Visit the successor: " ndfsr_trace << " Visit the successor: "
<< a_->format_state(s_prime) << std::endl; << a_->format_state(s_prime) << std::endl;
bdd label = f.it->current_condition(); bdd label = f.it->current_condition();
@ -340,9 +339,10 @@ namespace spot
class test_path: public bfs_steps class test_path: public bfs_steps
{ {
public: public:
test_path(const tgba* a, const state* t, test_path(ars_statistics* ars,
const tgba* a, const state* t,
const state_set& d, const heap& h) const state_set& d, const heap& h)
: bfs_steps(a), target(t), dead(d), h(h) : bfs_steps(a), ars(ars), target(t), dead(d), h(h)
{ {
} }
@ -368,6 +368,7 @@ namespace spot
const state* filter(const state* s) const state* filter(const state* s)
{ {
ars->inc_ars_states();
if (!h.has_been_visited(s) if (!h.has_been_visited(s)
|| seen.find(s) != seen.end() || seen.find(s) != seen.end()
|| dead.find(s) != dead.end()) || dead.find(s) != dead.end())
@ -396,6 +397,7 @@ namespace spot
} }
private: private:
ars_statistics* ars;
state_set seen; state_set seen;
const state* target; const state* target;
const state_set& dead; const state_set& dead;
@ -408,7 +410,7 @@ namespace spot
if (start->compare(target) == 0) if (start->compare(target) == 0)
return true; return true;
test_path s(a_, target, dead, h_); test_path s(this, a_, target, dead, h_);
const state* res = s.search(start->clone(), path); const state* res = s.search(start->clone(), path);
if (res) if (res)
{ {
@ -430,8 +432,9 @@ namespace spot
class min_path: public bfs_steps class min_path: public bfs_steps
{ {
public: public:
min_path(const tgba* a, const m_source_trans& target, const heap& h) min_path(ars_statistics* ars,
: bfs_steps(a), target(target), h(h) const tgba* a, const m_source_trans& target, const heap& h)
: bfs_steps(a), ars(ars), target(target), h(h)
{ {
} }
@ -457,6 +460,7 @@ namespace spot
const state* filter(const state* s) const state* filter(const state* s)
{ {
ars->inc_ars_states();
ndfsr_trace << "filter: " << a_->format_state(s); ndfsr_trace << "filter: " << a_->format_state(s);
if (!h.has_been_visited(s) || seen.find(s) != seen.end()) if (!h.has_been_visited(s) || seen.find(s) != seen.end())
{ {
@ -480,6 +484,7 @@ namespace spot
} }
private: private:
ars_statistics* ars;
state_set seen; state_set seen;
const m_source_trans& target; const m_source_trans& target;
const heap& h; const heap& h;
@ -533,7 +538,7 @@ namespace spot
typename m_source_trans::iterator i = target.find(current.dest); typename m_source_trans::iterator i = target.find(current.dest);
if (i == target.end()) if (i == target.end())
{ {
min_path s(a_, target, h_); min_path s(this, a_, target, h_);
const state* res = s.search(current.dest->clone(), run->cycle); const state* res = s.search(current.dest->clone(), run->cycle);
// init current to the corresponding transition. // init current to the corresponding transition.
assert(res); assert(res);
@ -563,7 +568,7 @@ namespace spot
<< a_->format_state(begin) << std::endl; << a_->format_state(begin) << std::endl;
transition tmp; transition tmp;
target.insert(std::make_pair(begin, tmp)); target.insert(std::make_pair(begin, tmp));
min_path s(a_, target, h_); min_path s(this, a_, target, h_);
const state* res = s.search(current.dest->clone(), run->cycle); const state* res = s.search(current.dest->clone(), run->cycle);
assert(res); assert(res);
assert(res->compare(begin) == 0); assert(res->compare(begin) == 0);
@ -598,7 +603,7 @@ namespace spot
else else
{ {
// This initial state is outside the cycle. Compute the prefix. // This initial state is outside the cycle. Compute the prefix.
min_path s(a_, target, h_); min_path s(this, a_, target, h_);
cycle_entry_point = s.search(prefix_start, run->prefix); cycle_entry_point = s.search(prefix_start, run->prefix);
assert(cycle_entry_point); assert(cycle_entry_point);
cycle_entry_point = cycle_entry_point->clone(); cycle_entry_point = cycle_entry_point->clone();

74
src/tgbatest/randtgba.cc
View file

@ -252,6 +252,36 @@ struct acss_stat
} }
}; };
struct ars_stat
{
int min_states;
int max_states;
int tot_states;
int n;
ars_stat()
: n(0)
{
}
void
count(const spot::ars_statistics* acss)
{
int s = acss->ars_states();
if (n++)
{
min_states = std::min(min_states, s);
max_states = std::max(max_states, s);
tot_states += s;
}
else
{
min_states = max_states = tot_states = s;
}
}
};
struct ar_stat struct ar_stat
{ {
int min_prefix; int min_prefix;
@ -299,6 +329,8 @@ ec_stats_type ec_stats;
typedef std::map<std::string, acss_stat> acss_stats_type; typedef std::map<std::string, acss_stat> acss_stats_type;
acss_stats_type acss_stats; acss_stats_type acss_stats;
typedef std::map<std::string, ars_stat> ars_stats_type;
ars_stats_type ars_stats;
typedef std::map<std::string, ar_stat> ar_stats_type; typedef std::map<std::string, ar_stat> ar_stats_type;
ar_stats_type ar_stats; // Statistics about accepting runs. ar_stats_type ar_stats; // Statistics about accepting runs.
@ -586,10 +618,21 @@ main(int argc, char** argv)
if (opt_replay) if (opt_replay)
{ {
spot::tgba_run* run; spot::tgba_run* run;
const spot::ars_statistics* ars =
dynamic_cast<const spot::ars_statistics*>(res);
tm_ar.start(algo); tm_ar.start(algo);
for (int count = opt_R;;) for (int count = opt_R;;)
{ {
run = res->accepting_run(); run = res->accepting_run();
if (opt_z && ars)
{
// Count only the first run (the other way
// would be to divide the stats by opt_R).
ars_stats[algo].count(ars);
ars = 0;
}
if (count-- <= 0 || !run) if (count-- <= 0 || !run)
break; break;
delete run; delete run;
@ -784,6 +827,37 @@ main(int argc, char** argv)
<< std::endl; << std::endl;
std::cout << std::setiosflags(old); std::cout << std::setiosflags(old);
} }
if (!ars_stats.empty())
{
std::cout << std::endl;
std::ios::fmtflags old = std::cout.flags();
std::cout << std::right << std::fixed << std::setprecision(1);
std::cout << "Statistics about accepting run computation:"
<< std::endl;
std::cout << std::setw(22) << ""
<< " | (non unique) states |"
<< std::endl << std::setw(22) << "algorithm"
<< " | min < mean < max | total | n"
<< std::endl
<< std::setw(61) << std::setfill('-') << "" << std::setfill(' ')
<< std::endl;
for (ars_stats_type::const_iterator i = ars_stats.begin();
i != ars_stats.end(); ++i)
std::cout << std::setw(22) << i->first << " |"
<< std::setw(6) << i->second.min_states
<< " "
<< std::setw(8)
<< static_cast<float>(i->second.tot_states) / i->second.n
<< " "
<< std::setw(6) << i->second.max_states
<< " |"
<< std::setw(6) << i->second.tot_states
<< " |"
<< std::setw(4) << i->second.n
<< std::endl;
std::cout << std::setiosflags(old);
}
if (!ar_stats.empty()) if (!ar_stats.empty())
{ {