* src/misc/timer.cc, src/tgbatest/randtgba.cc: Format the statistics.
This commit is contained in:
Denis Poitrenaud
parent
0fc279c56e
commit
0222c5e186
3 changed files with 123 additions and 103 deletions
|
|
@ -1,3 +1,7 @@
|
||||||
|
2004-12-10 Denis Poitrenaud <Denis.Poitrenaud@lip6.fr>
|
||||||
|
|
||||||
|
* src/misc/timer.cc, src/tgbatest/randtgba.cc: Format the statistics.
|
||||||
|
|
||||||
2004-12-10 Alexandre Duret-Lutz <adl@src.lip6.fr>
|
2004-12-10 Alexandre Duret-Lutz <adl@src.lip6.fr>
|
||||||
|
|
||||||
* src/tgbatest/emptchkr.test: Tune the "big degeneralized" test
|
* src/tgbatest/emptchkr.test: Tune the "big degeneralized" test
|
||||||
|
|
|
||||||
|
|
@ -29,6 +29,9 @@ namespace spot
|
||||||
std::ostream&
|
std::ostream&
|
||||||
timer_map::print(std::ostream& os) const
|
timer_map::print(std::ostream& os) const
|
||||||
{
|
{
|
||||||
|
std::ios::fmtflags old = std::cout.flags();
|
||||||
|
std::cout << std::right << std::fixed << std::setprecision(1);
|
||||||
|
|
||||||
time_info total;
|
time_info total;
|
||||||
for (tm_type::const_iterator i = tm.begin(); i != tm.end(); ++i)
|
for (tm_type::const_iterator i = tm.begin(); i != tm.end(); ++i)
|
||||||
{
|
{
|
||||||
|
|
@ -37,47 +40,49 @@ namespace spot
|
||||||
}
|
}
|
||||||
clock_t grand_total = total.utime + total.stime;
|
clock_t grand_total = total.utime + total.stime;
|
||||||
|
|
||||||
os << std::setw(33) << ""
|
os << std::setw(23) << ""
|
||||||
<< "| user time | sys. time | total |"
|
<< "| user time | sys. time | total |"
|
||||||
<< std::endl
|
<< std::endl
|
||||||
<< std::setw(33) << "name "
|
<< std::setw(23) << "name "
|
||||||
<< "| ticks % | tics % | tics % | n"
|
<< "| ticks % | ticks % | ticks % | n"
|
||||||
<< std::endl
|
<< std::endl
|
||||||
<< std::setw(79) << std::setfill('-') << "" << std::setfill(' ')
|
<< std::setw(79) << std::setfill('-') << "" << std::setfill(' ')
|
||||||
<< std::endl;
|
<< std::endl;
|
||||||
for (tm_type::const_iterator i = tm.begin(); i != tm.end(); ++i)
|
for (tm_type::const_iterator i = tm.begin(); i != tm.end(); ++i)
|
||||||
{
|
{
|
||||||
const spot::timer& t = i->second.first;
|
const spot::timer& t = i->second.first;
|
||||||
os << std::setw(32) << i->first << " |"
|
os << std::setw(22) << i->first << " |"
|
||||||
<< std::setw(6) << t.utime()
|
<< std::setw(6) << t.utime() << " "
|
||||||
<< std::setw(5) << (total.utime ?
|
<< std::setw(8) << (total.utime ?
|
||||||
100.0 * t.utime() / total.utime : 0)
|
100.0 * t.utime() / total.utime : 0.)
|
||||||
<< " |"
|
<< " |"
|
||||||
<< std::setw(6) << t.stime()
|
<< std::setw(6) << t.stime() << " "
|
||||||
<< std::setw(5) << (total.stime ?
|
<< std::setw(8) << (total.stime ?
|
||||||
100.0 * t.stime() / total.stime : 0)
|
100.0 * t.stime() / total.stime : 0.)
|
||||||
<< " |"
|
<< " |"
|
||||||
<< std::setw(6) << t.utime() + t.stime()
|
<< std::setw(6) << t.utime() + t.stime() << " "
|
||||||
<< std::setw(5) << (grand_total ?
|
<< std::setw(8) << (grand_total ?
|
||||||
(100.0 * (t.utime() + t.stime()) /
|
(100.0 * (t.utime() + t.stime()) /
|
||||||
grand_total) : 0)
|
grand_total) : 0.)
|
||||||
<< " |"
|
<< " |"
|
||||||
<< std::setw(4) << i->second.second
|
<< std::setw(4) << i->second.second
|
||||||
<< std::endl;
|
<< std::endl;
|
||||||
}
|
}
|
||||||
os << std::setw(79) << std::setfill('-') << "" << std::setfill(' ')
|
os << std::setw(79) << std::setfill('-') << "" << std::setfill(' ')
|
||||||
<< std::endl
|
<< std::endl
|
||||||
<< std::setw(32) << "TOTAL" << " |"
|
<< std::setw(22) << "TOTAL" << " |"
|
||||||
<< std::setw(6) << total.utime
|
<< std::setw(6) << total.utime << " "
|
||||||
<< std::setw(5) << 100
|
<< std::setw(8) << 100.
|
||||||
<< " |"
|
<< " |"
|
||||||
<< std::setw(6) << total.stime
|
<< std::setw(6) << total.stime << " "
|
||||||
<< std::setw(5) << 100
|
<< std::setw(8) << 100.
|
||||||
<< " |"
|
<< " |"
|
||||||
<< std::setw(6) << grand_total
|
<< std::setw(6) << grand_total << " "
|
||||||
<< std::setw(5) << 100
|
<< std::setw(8) << 100.
|
||||||
<< " |"
|
<< " |"
|
||||||
<< std::endl;
|
<< std::endl;
|
||||||
|
|
||||||
|
std::cout << std::setiosflags(old);
|
||||||
return os;
|
return os;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -91,11 +91,9 @@ ec_algo ec_algos[] =
|
||||||
{ "couvreur99_shy-", couvreur99_shy_minus_cons, 0, -1U, true },
|
{ "couvreur99_shy-", couvreur99_shy_minus_cons, 0, -1U, true },
|
||||||
{ "couvreur99_shy", couvreur99_shy_cons, 0, -1U, true },
|
{ "couvreur99_shy", couvreur99_shy_cons, 0, -1U, true },
|
||||||
{ "explicit_magic_search", spot::explicit_magic_search, 0, 1, true },
|
{ "explicit_magic_search", spot::explicit_magic_search, 0, 1, true },
|
||||||
{ "bit_state_hashing_magic_search",
|
{ "bsh_magic_search", bsh_ms_cons, 0, 1, false },
|
||||||
bsh_ms_cons, 0, 1, false },
|
|
||||||
{ "explicit_se05", spot::explicit_se05_search, 0, 1, true },
|
{ "explicit_se05", spot::explicit_se05_search, 0, 1, true },
|
||||||
{ "bit_state_hashing_se05",
|
{ "bsh_se05", bsh_se05_cons, 0, 1, false },
|
||||||
bsh_se05_cons, 0, 1, false },
|
|
||||||
{ "explicit_gv04", spot::explicit_gv04_check, 0, 1, true },
|
{ "explicit_gv04", spot::explicit_gv04_check, 0, 1, true },
|
||||||
{ "explicit_tau03", spot::explicit_tau03_search, 1, -1U, true },
|
{ "explicit_tau03", spot::explicit_tau03_search, 1, -1U, true },
|
||||||
{ "explicit_tau03_opt", spot::explicit_tau03_opt_search, 0, -1U, true },
|
{ "explicit_tau03_opt", spot::explicit_tau03_opt_search, 0, -1U, true },
|
||||||
|
|
@ -276,62 +274,69 @@ ar_stats_type mar_stats; // ... about minimized accepting runs.
|
||||||
void
|
void
|
||||||
print_ar_stats(ar_stats_type& ar_stats)
|
print_ar_stats(ar_stats_type& ar_stats)
|
||||||
{
|
{
|
||||||
std::cout << std::setw(32) << ""
|
std::ios::fmtflags old = std::cout.flags();
|
||||||
<< " | prefix | cycle |"
|
std::cout << std::right << std::fixed << std::setprecision(1);
|
||||||
<< std::endl << std::setw(32) << "algorithm"
|
|
||||||
<< " | min < mean < max | min < mean < max | n "
|
std::cout << std::setw(22) << ""
|
||||||
<< std::endl
|
<< " | prefix | cycle |"
|
||||||
<< std::setw(79) << std::setfill('-') << "" << std::setfill(' ')
|
<< std::endl
|
||||||
<< std::endl << std::setprecision(3);
|
<< std::setw(22) << "algorithm"
|
||||||
for (ar_stats_type::const_iterator i = ar_stats.begin();
|
<< " | min < mean < max | min < mean < max | n "
|
||||||
i != ar_stats.end(); ++i)
|
<< std::endl
|
||||||
std::cout << std::setw(32) << i->first << " |"
|
<< std::setw(79) << std::setfill('-') << "" << std::setfill(' ')
|
||||||
<< std::setw(5) << i->second.min_prefix
|
<< std::endl;
|
||||||
<< " "
|
for (ar_stats_type::const_iterator i = ar_stats.begin();
|
||||||
<< std::setw(6)
|
i != ar_stats.end(); ++i)
|
||||||
<< static_cast<float>(i->second.tot_prefix) / i->second.n
|
std::cout << std::setw(22) << i->first << " |"
|
||||||
<< " "
|
<< std::setw(6) << i->second.min_prefix
|
||||||
<< std::setw(5) << i->second.max_prefix
|
<< " "
|
||||||
<< " |"
|
<< std::setw(8)
|
||||||
<< std::setw(5) << i->second.min_cycle
|
<< static_cast<float>(i->second.tot_prefix) / i->second.n
|
||||||
<< " "
|
<< " "
|
||||||
<< std::setw(6)
|
<< std::setw(6) << i->second.max_prefix
|
||||||
<< static_cast<float>(i->second.tot_cycle) / i->second.n
|
<< " |"
|
||||||
<< " "
|
<< std::setw(6) << i->second.min_cycle
|
||||||
<< std::setw(5) << i->second.max_cycle
|
<< " "
|
||||||
<< " |"
|
<< std::setw(8)
|
||||||
<< std::setw(5) << i->second.n
|
<< static_cast<float>(i->second.tot_cycle) / i->second.n
|
||||||
<< std::endl;
|
<< " "
|
||||||
std::cout << std::setw(79) << std::setfill('-') << "" << std::setfill(' ')
|
<< std::setw(6) << i->second.max_cycle
|
||||||
<< std::endl
|
<< " |"
|
||||||
<< std::setw(32) << ""
|
<< std::setw(4) << i->second.n
|
||||||
<< " | runs | total |"
|
<< std::endl;
|
||||||
<< std::endl << std::setw(32) << "algorithm"
|
std::cout << std::setw(79) << std::setfill('-') << "" << std::setfill(' ')
|
||||||
<< " | min < mean < max | pre. cyc. runs | n "
|
<< std::endl
|
||||||
<< std::endl
|
<< std::setw(22) << ""
|
||||||
<< std::setw(79) << std::setfill('-') << "" << std::setfill(' ')
|
<< " | runs | total |"
|
||||||
<< std::endl;
|
<< std::endl <<
|
||||||
for (ar_stats_type::const_iterator i = ar_stats.begin();
|
std::setw(22) << "algorithm"
|
||||||
i != ar_stats.end(); ++i)
|
<< " | min < mean < max | pre. cyc. runs | n "
|
||||||
std::cout << std::setw(32) << i->first << " |"
|
<< std::endl
|
||||||
<< std::setw(5)
|
<< std::setw(79) << std::setfill('-') << "" << std::setfill(' ')
|
||||||
<< i->second.min_run
|
<< std::endl;
|
||||||
<< " "
|
for (ar_stats_type::const_iterator i = ar_stats.begin();
|
||||||
<< std::setw(6)
|
i != ar_stats.end(); ++i)
|
||||||
<< static_cast<float>(i->second.tot_prefix
|
std::cout << std::setw(22) << i->first << " |"
|
||||||
+ i->second.tot_cycle) / i->second.n
|
<< std::setw(6)
|
||||||
<< " "
|
<< i->second.min_run
|
||||||
<< std::setw(5)
|
<< " "
|
||||||
<< i->second.max_run
|
<< std::setw(8)
|
||||||
<< " |"
|
<< static_cast<float>(i->second.tot_prefix
|
||||||
<< std::setw(5) << i->second.tot_prefix
|
+ i->second.tot_cycle) / i->second.n
|
||||||
<< " "
|
<< " "
|
||||||
<< std::setw(5) << i->second.tot_cycle
|
<< std::setw(6)
|
||||||
<< " "
|
<< i->second.max_run
|
||||||
<< std::setw(5) << i->second.tot_prefix + i->second.tot_cycle
|
<< " |"
|
||||||
<< " |"
|
<< std::setw(6) << i->second.tot_prefix
|
||||||
<< std::setw(5) << i->second.n
|
<< " "
|
||||||
<< std::endl;
|
<< std::setw(6) << i->second.tot_cycle
|
||||||
|
<< " "
|
||||||
|
<< std::setw(8) << i->second.tot_prefix + i->second.tot_cycle
|
||||||
|
<< " |"
|
||||||
|
<< std::setw(4) << i->second.n
|
||||||
|
<< std::endl;
|
||||||
|
|
||||||
|
std::cout << std::setiosflags(old);
|
||||||
}
|
}
|
||||||
|
|
||||||
int
|
int
|
||||||
|
|
@ -629,56 +634,62 @@ main(int argc, char** argv)
|
||||||
|
|
||||||
if (!ec_stats.empty())
|
if (!ec_stats.empty())
|
||||||
{
|
{
|
||||||
|
std::ios::fmtflags old = std::cout.flags();
|
||||||
|
std::cout << std::right << std::fixed << std::setprecision(1);
|
||||||
|
|
||||||
std::cout << "Statistics about emptiness checkers:" << std::endl;
|
std::cout << "Statistics about emptiness checkers:" << std::endl;
|
||||||
std::cout << std::setw(32) << ""
|
std::cout << std::setw(22) << ""
|
||||||
<< " | states | transitions |"
|
<< " | states | transitions |"
|
||||||
<< std::endl << std::setw(32) << "algorithm"
|
<< std::endl << std::setw(22) << "algorithm"
|
||||||
<< " | min < mean < max | min < mean < max | n "
|
<< " | min < mean < max | min < mean < max | n "
|
||||||
<< std::endl
|
<< std::endl
|
||||||
<< std::setw(79) << std::setfill('-') << "" << std::setfill(' ')
|
<< std::setw(79) << std::setfill('-') << "" << std::setfill(' ')
|
||||||
<< std::endl << std::setprecision(3);
|
<< std::endl;
|
||||||
for (ec_stats_type::const_iterator i = ec_stats.begin();
|
for (ec_stats_type::const_iterator i = ec_stats.begin();
|
||||||
i != ec_stats.end(); ++i)
|
i != ec_stats.end(); ++i)
|
||||||
std::cout << std::setw(32) << i->first << " |"
|
std::cout << std::setw(22) << i->first << " |"
|
||||||
<< std::setw(5) << i->second.min_states
|
<< std::setw(6) << i->second.min_states
|
||||||
<< " "
|
<< " "
|
||||||
<< std::setw(6)
|
<< std::setw(8)
|
||||||
<< static_cast<float>(i->second.tot_states) / i->second.n
|
<< static_cast<float>(i->second.tot_states) / i->second.n
|
||||||
<< " "
|
<< " "
|
||||||
<< std::setw(5) << i->second.max_states
|
<< std::setw(6) << i->second.max_states
|
||||||
<< " |"
|
<< " |"
|
||||||
<< std::setw(5) << i->second.min_transitions
|
<< std::setw(6) << i->second.min_transitions
|
||||||
<< " "
|
<< " "
|
||||||
<< std::setw(6)
|
<< std::setw(8)
|
||||||
<< static_cast<float>(i->second.tot_transitions) / i->second.n
|
<< static_cast<float>(i->second.tot_transitions) / i->second.n
|
||||||
<< " "
|
<< " "
|
||||||
<< std::setw(5) << i->second.max_transitions
|
<< std::setw(6) << i->second.max_transitions
|
||||||
<< " |"
|
<< " |"
|
||||||
<< std::setw(5) << i->second.n
|
<< std::setw(4) << i->second.n
|
||||||
<< std::endl;
|
<< std::endl;
|
||||||
std::cout << std::setw(79) << std::setfill('-') << "" << std::setfill(' ')
|
std::cout << std::setw(79) << std::setfill('-') << "" << std::setfill(' ')
|
||||||
<< std::endl
|
<< std::endl
|
||||||
<< std::setw(32) << ""
|
<< std::setw(22) << ""
|
||||||
<< " | maximal depth |"
|
<< " | maximal depth |"
|
||||||
<< std::endl << std::setw(32) << "algorithm"
|
<< std::endl
|
||||||
<< " | min < mean < max | n "
|
<< std::setw(22) << "algorithm"
|
||||||
|
<< " | min < mean < max | n "
|
||||||
<< std::endl
|
<< std::endl
|
||||||
<< std::setw(59) << std::setfill('-') << "" << std::setfill(' ')
|
<< std::setw(59) << std::setfill('-') << "" << std::setfill(' ')
|
||||||
<< std::endl;
|
<< std::endl;
|
||||||
for (ec_stats_type::const_iterator i = ec_stats.begin();
|
for (ec_stats_type::const_iterator i = ec_stats.begin();
|
||||||
i != ec_stats.end(); ++i)
|
i != ec_stats.end(); ++i)
|
||||||
std::cout << std::setw(32) << i->first << " |"
|
std::cout << std::setw(22) << i->first << " |"
|
||||||
<< std::setw(5)
|
<< std::setw(6)
|
||||||
<< i->second.min_max_depth
|
<< i->second.min_max_depth
|
||||||
<< " "
|
<< " "
|
||||||
<< std::setw(6)
|
<< std::setw(8)
|
||||||
<< static_cast<float>(i->second.tot_max_depth) / i->second.n
|
<< static_cast<float>(i->second.tot_max_depth) / i->second.n
|
||||||
<< " "
|
<< " "
|
||||||
<< std::setw(5)
|
<< std::setw(6)
|
||||||
<< i->second.max_max_depth
|
<< i->second.max_max_depth
|
||||||
<< " |"
|
<< " |"
|
||||||
<< std::setw(5) << i->second.n
|
<< std::setw(4) << i->second.n
|
||||||
<< std::endl;
|
<< std::endl;
|
||||||
|
|
||||||
|
std::cout << std::setiosflags(old);
|
||||||
}
|
}
|
||||||
|
|
||||||
if (!ar_stats.empty())
|
if (!ar_stats.empty())
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue