From 8068a54e382e0e583e411657432c578f8527b8d1 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 18 Nov 2004 19:05:41 +0000 Subject: [PATCH] * src/tgbatest/randtgba.cc (main): Add options -z and -Z for statistics. (ce_stat): New struct. --- ChangeLog | 5 ++ src/tgbatest/randtgba.cc | 138 ++++++++++++++++++++++++++++++++++++++- 2 files changed, 141 insertions(+), 2 deletions(-) diff --git a/ChangeLog b/ChangeLog index 10858acad..c69491f78 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,8 @@ +2004-11-18 Alexandre Duret-Lutz + + * src/tgbatest/randtgba.cc (main): Add options -z and -Z for statistics. + (ce_stat): New struct. + 2004-11-17 Poitrenaud Denis * src/tgbaalgos/se05.hh, src/tgbaalgos/tau03.hh: Typo. diff --git a/src/tgbatest/randtgba.cc b/src/tgbatest/randtgba.cc index 6ed9989d5..60a2413d8 100644 --- a/src/tgbatest/randtgba.cc +++ b/src/tgbatest/randtgba.cc @@ -21,7 +21,9 @@ #include #include +#include #include +#include #include "ltlvisit/apcollect.hh" #include "ltlvisit/destroy.hh" #include "tgbaalgos/randomgraph.hh" @@ -46,7 +48,8 @@ syntax(char* prog) << std::endl << "Options:" << std::endl << " -a N F number of acceptance conditions and probability that" - << " one is true [0 0.0]" << std::endl + << " one is true" << std::endl + << " [0 0.0]" << std::endl << " -d F density of the graph [0.2]" << std::endl << " -e N compare result of all " << "emptiness checks on N randomly generated graphs" << std::endl @@ -57,6 +60,10 @@ syntax(char* prog) << " -s N seed for the random number generator" << std::endl << " -t F probability of the atomic propositions to be true" << " [0.5]" << std::endl + << " -z display statistics about computed counter-examples" + << std::endl + << " -Z like -z, but print extra statistics after the run" + << " of each algorithm" << std::endl << "Where:" << std::endl << " F are floats between 0.0 and 1.0 inclusive" << std::endl << " N are positive integers" << std::endl @@ -91,6 +98,48 @@ to_float(const char* s) return res; } +struct ce_stat +{ + int min_prefix; + int max_prefix; + int tot_prefix; + int min_cycle; + int max_cycle; + int tot_cycle; + int min_run; + int max_run; + int n; + + ce_stat() + : n(0) + { + } + + void + count(const spot::tgba_run* run) + { + int p = run->prefix.size(); + int c = run->cycle.size(); + if (n++) + { + min_prefix = std::min(min_prefix, p); + max_prefix = std::max(max_prefix, p); + tot_prefix += p; + min_cycle = std::min(min_cycle, c); + max_cycle = std::max(max_cycle, c); + tot_cycle += c; + min_run = std::min(min_run, c + p); + max_run = std::max(max_run, c + p); + } + else + { + min_prefix = max_prefix = tot_prefix = p; + min_cycle = max_cycle = tot_cycle = c; + min_run = max_run = c + p; + } + } +}; + int main(int argc, char** argv) { @@ -100,6 +149,9 @@ main(int argc, char** argv) int opt_n = 20; float opt_t = 0.5; + bool opt_z = false; + bool opt_Z = false; + bool opt_dot = false; int opt_ec = 0; int opt_ec_seed = 0; @@ -109,6 +161,9 @@ main(int argc, char** argv) int exit_code = 0; + typedef std::map stats_type; + stats_type stats; + spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::ltl::atomic_prop_set* ap = new spot::ltl::atomic_prop_set; @@ -165,6 +220,14 @@ main(int argc, char** argv) syntax(argv[0]); opt_t = to_float(argv[++argn]); } + else if (!strcmp(argv[argn], "-z")) + { + opt_z = true; + } + else if (!strcmp(argv[argn], "-Z")) + { + opt_Z = opt_z = true; + } else { ap->insert(static_cast @@ -245,8 +308,9 @@ main(int argc, char** argv) for (int i = 0; i < n_ec; ++i) { + std::string algo = ec_name[i]; std::cout.width(32); - std::cout << ec_name[i] << ": "; + std::cout << algo << ": "; spot::emptiness_check_result* res = ec_obj[i]->check(); if (res) { @@ -266,7 +330,13 @@ main(int argc, char** argv) else { std::cout << ", computed OK"; + if (opt_z) + stats[algo].count(run); } + if (opt_z) + std::cout << " [" << run->prefix.size() + << " + " << run->cycle.size() + << "]"; delete run; } else @@ -291,6 +361,9 @@ main(int argc, char** argv) } } + + if (opt_Z) + ec_obj[i]->print_stats(std::cout); delete ec_obj[i]; } @@ -313,6 +386,67 @@ main(int argc, char** argv) } } while (opt_ec); + + if (!stats.empty()) + { + std::cout << "Statistics about counter-examples:" << std::endl; + std::cout << std::setw(32) << "" + << " | prefix | cycle |" + << std::endl << std::setw(32) << "algorithm" + << " | min < mean < max | min < mean < max | n " + << std::endl + << std::setw(79) << std::setfill('-') << "" << std::setfill(' ') + << std::endl << std::setprecision(3); + for (stats_type::const_iterator i = stats.begin(); i != stats.end(); ++i) + std::cout << std::setw(32) << i->first << " |" + << std::setw(5) << i->second.min_prefix + << " " + << std::setw(6) + << static_cast(i->second.tot_prefix) / i->second.n + << " " + << std::setw(5) << i->second.max_prefix + << " |" + << std::setw(5) << i->second.min_cycle + << " " + << std::setw(6) + << static_cast(i->second.tot_cycle) / i->second.n + << " " + << std::setw(5) << i->second.max_cycle + << " |" + << std::setw(5) << i->second.n + << std::endl; + std::cout << std::setw(79) << std::setfill('-') << "" << std::setfill(' ') + << std::endl + << std::setw(32) << "" + << " | runs | total |" + << std::endl << std::setw(32) << "algorithm" + << " | min < mean < max | pre. cyc. runs | n " + << std::endl + << std::setw(79) << std::setfill('-') << "" << std::setfill(' ') + << std::endl; + for (stats_type::const_iterator i = stats.begin(); i != stats.end(); ++i) + std::cout << std::setw(32) << i->first << " |" + << std::setw(5) + << i->second.min_run + << " " + << std::setw(6) + << static_cast(i->second.tot_prefix + + i->second.tot_cycle) / i->second.n + << " " + << std::setw(5) + << i->second.max_run + << " |" + << std::setw(5) << i->second.tot_prefix + << " " + << std::setw(5) << i->second.tot_cycle + << " " + << std::setw(5) << i->second.tot_prefix + i->second.tot_cycle + << " |" + << std::setw(5) << i->second.n + << std::endl; + + } + if (!failed_seeds.empty()) { exit_code = 1;