From 6314b682ba62386790bea1f70422d1f83df290d1 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 18 Feb 2005 12:28:42 +0000 Subject: [PATCH] * src/tgbatest/randtgba.cc: Remplace the -O option by -A, reading all algorithms from a file. Use the emptiness_check_instantiator syntax as name in the output. * bench/emptchk/defs.in: DEfine ALGORITHMS here. * bench/emptchk/ltl-human.sh, bench/emptchk/ltl-random.sh, bench/emptchk/pml-clserv.sh, bench/emptchk/pml-clserv.sh: Use $ALGORITHMS. * src/misc/timer.cc: Truncate long keys in display. --- ChangeLog | 9 +++ bench/emptchk/README | 64 +++++++-------- bench/emptchk/defs.in | 1 + bench/emptchk/ltl-human.sh | 4 +- bench/emptchk/ltl-random.sh | 4 +- bench/emptchk/pml-clserv.sh | 1 - bench/emptchk/pml-eeaean.sh | 1 - src/misc/timer.cc | 9 ++- src/tgbatest/randtgba.cc | 156 +++++++++++++++++++++--------------- 9 files changed, 144 insertions(+), 105 deletions(-) diff --git a/ChangeLog b/ChangeLog index edc337752..02cdd6a1c 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,14 @@ 2005-02-18 Alexandre Duret-Lutz + * src/tgbatest/randtgba.cc: Remplace the -O option by -A, reading + all algorithms from a file. Use the emptiness_check_instantiator + syntax as name in the output. + * bench/emptchk/defs.in: DEfine ALGORITHMS here. + * bench/emptchk/ltl-human.sh, bench/emptchk/ltl-random.sh, + bench/emptchk/pml-clserv.sh, bench/emptchk/pml-clserv.sh: Use + $ALGORITHMS. + * src/misc/timer.cc: Truncate long keys in display. + * src/tgbatest/ltl2tgba.cc: Simplify using emptiness_check_instantiator. * src/tgba/tgba.cc, src/tgba/tgba.hh diff --git a/bench/emptchk/README b/bench/emptchk/README index 29e3c77f5..e42b16788 100644 --- a/bench/emptchk/README +++ b/bench/emptchk/README @@ -175,51 +175,42 @@ This directory contains: INTERPRETING THE RESULTS ========================== - Here are the short names for the algorithms used in the outputs. - ltl-*.sh tests use names from the left column, and pml-*.sh tests - use names from the right column. + Here are the short names for the algorithms presented in the outputs. - Cou99 Cou99 - Cou99_shy- Cou99(shy !group) - Cou99_shy Cou99(shy group) - > Cou99_rem Cou99(poprem) - > Cou99_rem_shy- Cou99(poprem shy !group) - > Cou99_rem_shy Cou99(poprem shy group) - > CVWY90 CVWY90 - CVWY90_bsh CVWY90(bsh=4K) - > GV04 GV04 - > SE05 SE05 - SE05_bsh SE05(bsh=4K) - > Tau03 Tau03 - > Tau03_opt Tau03_opt + Cou99 + Cou99(shy !group) + Cou99(shy group) + > Cou99(poprem) # called `Cou99' in the paper + > Cou99(poprem shy !group) # called `Cou99 Shy-' in the paper + > Cou99(poprem shy group) # called `Cou99 Shy' in the paper + > CVWY90 + > GV04 + > SE05 + > Tau03 + > Tau03_opt Only the algorithms marked with a `>' have been shown in the paper. - `bsh' stands for `bit-state hashing'. - `Cou99_rem*' algorithms are using the `rem' field to remove - the SCC without recomputing the SCC as described in the paper. - The other `Cou99*' algorithms are not. (Beware that in the paper - we presented the `Cou99_rem*' variants and called them `Cou99*'.) + `Cou99(poprem*)' algorithms are using the `rem' field to remove the + SCC without recomputing the SCC as described in the paper. The + other `Cou99' algorithms are not. (Beware that in the paper we + presented the `Cou99(poprem*)' variants and called them `Cou99*'.) The ltl-*.sh tests output look as follows: | density: 0.001 | Emptiness check ratios - | CVWY90 5.5 4.4 6.3 25 - | CVWY90_bsh 5.7 4.8 6.3 25 - | Cou99 5.5 3.3 4.3 25 - | Cou99_rem 5.5 3.0 4.3 25 + | Cou99 18.9 9.6 10.4 29 + | Cou99(shy !group) 16.7 16.3 25.7 29 | ... - (A) (B) (C) (D) + (A) (B) (C) (D) | | Accepting run ratios - | CVWY90 5.5 2.6 - | Cou99 2.0 2.6 - | Cou99_rem 2.0 2.1 - | Cou99_rem_shy 1.2 2.1 + | Cou99 8.6 13.5 + | Cou99(shy !group) 7.3 12.2 | ... - (E) (F) + (E) (F) (A) mean number of distinct states visited expressed as a % of the number of state of the product space @@ -237,10 +228,10 @@ This directory contains: The pml-*.sh tests output look as follows: - | Cou99 , 783, 2371, 5, 783, 4742, 237, no accepting run found - | Cou99_shy- , 783, 2371, 5, 783, 4742, 537, no accepting run found + | Cou99 , 92681, 391160, 1, 92681, 391160, 46471, no accepting run found + | Cou99(shy !group) , 92681, 391160, 1, 92681, 391160, 47148, no accepting run found | ... - (G) (H) (I) (K) (L) (M) (N) + (G) (H) (I) (K) (L) (M) (N) (G) Number of states in the product. (H) Number of transitions in the product. @@ -260,5 +251,10 @@ This directory contains: shown above. Try removing the `-1' option from the script, or toying with randtgba itself. + CVWY90 and SE05 have bit-state hashing implementations. Edit the + file `algorithms' and add lines like `CVWY90(bsh=5M)' or + `SE05(bsh=512K)' to try these. + (The `bsh=' argument gives the hash table size in bytes.) + Besides randtgba, two other tools that you might find handy we experimenting are src/ltltest/randltl and src/tgbatest/ltl2tgba. diff --git a/bench/emptchk/defs.in b/bench/emptchk/defs.in index 35ab0706b..7694da253 100644 --- a/bench/emptchk/defs.in +++ b/bench/emptchk/defs.in @@ -37,3 +37,4 @@ test -f "$srcdir/defs.in" || { RANDTGBA='@top_builddir@/src/tgbatest/randtgba@EXEEXT@' LTL2TGBA='@top_builddir@/src/tgbatest/ltl2tgba@EXEEXT@' FORMULAE=$srcdir/formulae.ltl +ALGORITHMS=$srcdir/algorithms diff --git a/bench/emptchk/ltl-human.sh b/bench/emptchk/ltl-human.sh index f0dd6cda6..faf89124d 100644 --- a/bench/emptchk/ltl-human.sh +++ b/bench/emptchk/ltl-human.sh @@ -29,12 +29,12 @@ echo "WITHOUT ADDITIONAL ACCEPTING CONDITIONS" for d in 0.001 0.002 0.01; do echo "density: $d" - $RANDTGBA -d $d $opts + $RANDTGBA -A "$ALGORITHMS" -d $d $opts done echo "WITH 3 ADDITIONAL ACCEPTING CONDITIONS" for d in 0.001 0.002 0.01; do echo "density: $d" - $RANDTGBA -a 3 0.0133333 -d $d $opts + $RANDTGBA -A "$ALGORITHMS" -a 3 0.0133333 -d $d $opts done diff --git a/bench/emptchk/ltl-random.sh b/bench/emptchk/ltl-random.sh index c630636d4..34c40a516 100644 --- a/bench/emptchk/ltl-random.sh +++ b/bench/emptchk/ltl-random.sh @@ -29,12 +29,12 @@ echo "WITHOUT ADDITIONAL ACCEPTING CONDITIONS" for d in 0.001 0.002 0.01; do echo "density: $d" - $RANDTGBA -d $d $opts + $RANDTGBA -A "$ALGORITHMS" -d $d $opts done echo "WITH 3 ADDITIONAL ACCEPTING CONDITIONS" for d in 0.001 0.002 0.01; do echo "density: $d" - $RANDTGBA -a 3 0.0133333 -d $d $opts + $RANDTGBA -A "$ALGORITHMS" -a 3 0.0133333 -d $d $opts done diff --git a/bench/emptchk/pml-clserv.sh b/bench/emptchk/pml-clserv.sh index d5d1409a0..b439efae5 100644 --- a/bench/emptchk/pml-clserv.sh +++ b/bench/emptchk/pml-clserv.sh @@ -24,7 +24,6 @@ set -e FORMULAE=$srcdir/models/clserv.ltl -ALGORITHMS=$srcdir/algorithms opts='-f -x -m' diff --git a/bench/emptchk/pml-eeaean.sh b/bench/emptchk/pml-eeaean.sh index 82e51d35a..967522d94 100644 --- a/bench/emptchk/pml-eeaean.sh +++ b/bench/emptchk/pml-eeaean.sh @@ -24,7 +24,6 @@ set -e FORMULAE=$srcdir/models/eeaean.ltl -ALGORITHMS=$srcdir/algorithms opts='-f -x -m' diff --git a/src/misc/timer.cc b/src/misc/timer.cc index 572fc017f..719f0b3a0 100644 --- a/src/misc/timer.cc +++ b/src/misc/timer.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -50,8 +50,13 @@ namespace spot << std::endl; for (tm_type::const_iterator i = tm.begin(); i != tm.end(); ++i) { + // truncate long keys + std::string name = i->first; + if (name.size() > 22) + name.erase(22); + const spot::timer& t = i->second.first; - os << std::setw(22) << i->first << " |" + os << std::setw(22) << name << " |" << std::setw(6) << t.utime() << " " << std::setw(8) << (total.utime ? 100.0 * t.utime() / total.utime : 0.) diff --git a/src/tgbatest/randtgba.cc b/src/tgbatest/randtgba.cc index 63f2208ef..481f8ab0b 100644 --- a/src/tgbatest/randtgba.cc +++ b/src/tgbatest/randtgba.cc @@ -58,27 +58,28 @@ struct ec_algo { - const char* name; - const char* options; + std::string name; spot::emptiness_check_instantiator* inst; }; -ec_algo ec_algos[] = - { - { "Cou99", "Cou99(!poprem)", 0 }, - { "Cou99_shy-", "Cou99(!poprem shy !group)", 0 }, - { "Cou99_shy", "Cou99(!poprem shy group)", 0 }, - { "Cou99_rem", "Cou99(poprem)", 0 }, - { "Cou99_rem_shy-", "Cou99(poprem shy !group)", 0 }, - { "Cou99_rem_shy", "Cou99(poprem shy group)", 0 }, - { "CVWY90", "CVWY90", 0 }, - { "CVWY90_bsh", "CVWY90(bsh=4K)", 0 }, - { "GV04", "GV04", 0 }, - { "SE05", "SE05", 0 }, - { "SE05_bsh", "SE05(bsh=4K)", 0 }, - { "Tau03", "Tau03", 0 }, - { "Tau03_opt", "Tau03_opt", 0 }, - }; +const char* default_algos[] = { + "Cou99(!poprem)", + "Cou99(!poprem shy !group)", + "Cou99(!poprem shy group)", + "Cou99(poprem)", + "Cou99(poprem shy !group)", + "Cou99(poprem shy group)", + "CVWY90", + "CVWY90(bsh=4K)", + "GV04", + "SE05", + "SE05(bsh=4K)", + "Tau03", + "Tau03_opt", + 0 +}; + +std::vector ec_algos; spot::emptiness_check* cons_emptiness_check(int num, const spot::tgba* a, @@ -132,6 +133,7 @@ syntax(char* prog) << " -u generate unique formulae" << std::endl << std::endl << "Emptiness-Check Options:" << std::endl + << " -A FILE use all algorithms listed in FILE" << std::endl << " -D degeneralize TGBA for emptiness-check algorithms that" << " would" << std::endl << " otherwise be skipped (implies -e)" << std::endl @@ -139,7 +141,6 @@ syntax(char* prog) << "emptiness checks on N randomly generated graphs" << std::endl << " -m try to reduce runs, in a second pass (implies -r)" << std::endl - << " -O ALGO run Only ALGO" << std::endl << " -R N repeat each emptiness-check and accepting run " << "computation N times" << std::endl << " -r compute and replay accepting runs (implies -e)" @@ -306,18 +307,18 @@ struct stat_collector bool total = true) const { std::ios::fmtflags old = os.flags(); - os << std::setw(22) << "" << " | " + os << std::setw(25) << "" << " | " << std::setw(30) << std::left << title << std::right << "|" << std::endl - << std::setw(22) << "algorithm" + << std::setw(25) << "algorithm" << " | min < mean < max | total | n" << std::endl - << std::setw(61) << std::setfill('-') << "" << std::setfill(' ') + << std::setw(64) << std::setfill('-') << "" << std::setfill(' ') << std::endl; os << std::right << std::fixed << std::setprecision(1); for (typename alg_1stat_map::const_iterator i = m.begin(); i != m.end(); ++i) { - os << std::setw(22) << i->first << " |" + os << std::setw(25) << i->first << " |" << std::setw(6) << i->second.min << " " << std::setw(8) @@ -333,7 +334,7 @@ struct stat_collector << std::setw(4) << i->second.n << std::endl; } - os << std::setw(61) << std::setfill('-') << "" << std::setfill(' ') + os << std::setw(64) << std::setfill('-') << "" << std::setfill(' ') << std::endl; os << std::setiosflags(old); return os; @@ -415,17 +416,17 @@ print_ar_stats(ar_stats_type& ar_stats, const std::string s) std::cout << std::endl << s << std::endl; std::cout << std::right << std::fixed << std::setprecision(1); - std::cout << std::setw(22) << "" + std::cout << std::setw(25) << "" << " | prefix | cycle |" << std::endl - << std::setw(22) << "algorithm" + << std::setw(25) << "algorithm" << " | min < mean < max | min < mean < max | n" << std::endl << std::setw(79) << std::setfill('-') << "" << std::setfill(' ') << std::endl; for (ar_stats_type::const_iterator i = ar_stats.begin(); i != ar_stats.end(); ++i) - std::cout << std::setw(22) << i->first << " |" + std::cout << std::setw(25) << i->first << " |" << std::setw(6) << i->second.min_prefix << " " << std::setw(8) @@ -444,17 +445,17 @@ print_ar_stats(ar_stats_type& ar_stats, const std::string s) << std::endl; std::cout << std::setw(79) << std::setfill('-') << "" << std::setfill(' ') << std::endl - << std::setw(22) << "" + << std::setw(25) << "" << " | runs | total |" << std::endl << - std::setw(22) << "algorithm" + std::setw(25) << "algorithm" << " | min < mean < max | pre. cyc. runs | n" << std::endl << std::setw(79) << std::setfill('-') << "" << std::setfill(' ') << std::endl; for (ar_stats_type::const_iterator i = ar_stats.begin(); i != ar_stats.end(); ++i) - std::cout << std::setw(22) << i->first << " |" + std::cout << std::setw(25) << i->first << " |" << std::setw(6) << i->second.min_run << " " @@ -531,6 +532,7 @@ generate_formula(const spot::ltl::random_ltl& rl, int opt_f, int opt_s, int main(int argc, char** argv) { + bool opt_A; bool opt_paper = false; bool opt_dp = false; int opt_f = 15; @@ -553,8 +555,6 @@ main(int argc, char** argv) int opt_R = 0; - const char* opt_O = 0; - bool opt_dot = false; int opt_ec = 0; int opt_ec_seed = 0; @@ -595,6 +595,41 @@ main(int argc, char** argv) opt_n_acc = to_int_nonneg(argv[++argn], "-a"); opt_a = to_float_nonneg(argv[++argn], "-a"); } + else if (!strcmp(argv[argn], "-A")) + { + if (argc < argn + 2) + syntax(argv[0]); + opt_A = true; + std::istream* in; + if (strcmp(argv[++argn], "-")) + { + in = new std::ifstream(argv[argn]); + if (!*in) + { + delete in; + std::cerr << "Failed to open " << argv[argn] << std::endl; + exit(2); + } + } + else + { + in = &std::cin; + } + + while (in->good()) + { + std::string input; + if (std::getline(*in, input, '\n').fail()) + break; + else if (input == "") + break; + ec_algo a = { input, 0 }; + ec_algos.push_back(a); + } + + if (in != &std::cin) + delete in; + } else if (!strncmp(argv[argn], "ar:", 3)) { if (options.parse_options(argv[argn])) @@ -656,25 +691,6 @@ main(int argc, char** argv) syntax(argv[0]); opt_n = to_int_pos(argv[++argn], "-n"); } - else if (!strcmp(argv[argn], "-O")) - { - if (argc < argn + 2) - syntax(argv[0]); - opt_O = argv[++argn]; - int s = sizeof(ec_algos) / sizeof(*ec_algos); - int i; - for (i = 0; i < s; ++i) - if (!strcmp(opt_O, ec_algos[i].name)) - break; - if (i == s) - { - std::cerr << "Unknown algorithm. Available algorithms are:" - << std::endl; - for (i = 0; i < s; ++i) - std::cerr << " " << ec_algos[i].name << std::endl; - exit(1); - } - } else if (!strcmp(argv[argn], "-r")) { opt_replay = true; @@ -769,6 +785,16 @@ main(int argc, char** argv) exit(0); } + if (ec_algos.empty()) + { + const char** i = default_algos; + while (*i) + { + ec_algo a = { *i++, 0 }; + ec_algos.push_back(a); + } + } + spot::timer_map tm_ec; spot::timer_map tm_ar; std::set failed_seeds; @@ -777,11 +803,12 @@ main(int argc, char** argv) if (opt_ec) { - for (unsigned i = 0; i < sizeof(ec_algos) / sizeof(*ec_algos); ++i) + for (unsigned i = 0; i < ec_algos.size(); ++i) { const char* err; ec_algos[i].inst = - spot::emptiness_check_instantiator::construct(ec_algos[i].options, + spot::emptiness_check_instantiator::construct(ec_algos[i] + .name.c_str(), &err); if (ec_algos[i].inst == 0) { @@ -871,7 +898,7 @@ main(int argc, char** argv) if (opt_degen && real_n_acc > 1) degen = new spot::tgba_tba_proxy(a); - int n_alg = sizeof(ec_algos) / sizeof(*ec_algos); + int n_alg = ec_algos.size(); int n_ec = 0; int n_empty = 0; int n_non_empty = 0; @@ -881,13 +908,11 @@ main(int argc, char** argv) { spot::emptiness_check* ec; spot::emptiness_check_result* res; - if (opt_O && strcmp(opt_O, ec_algos[i].name)) - continue; ec = cons_emptiness_check(i, a, degen, real_n_acc); if (!ec) continue; ++n_ec; - const char* algo = ec_algos[i].name; + const std::string algo = ec_algos[i].name; if (!opt_paper) { std::cout.width(32); @@ -1139,13 +1164,13 @@ main(int argc, char** argv) ec_ratio_stat_type::stats_alg_map& stats = glob_ec_ratio_stats.stats; typedef ec_ratio_stat_type::alg_1stat_map::const_iterator ec_iter; - for (unsigned i = 0; i < sizeof(ec_algos) / sizeof(*ec_algos); ++i) + for (unsigned i = 0; i < ec_algos.size(); ++i) { - const char* algo = ec_algos[i].name; + const std::string algo = ec_algos[i].name; int n = -1; - std::cout << std::setw(22) << algo << " " << std::setw(8); + std::cout << std::setw(25) << algo << " " << std::setw(8); ec_iter i = stats["states"].find(algo); if (i != stats["states"].end()) @@ -1184,11 +1209,11 @@ main(int argc, char** argv) std::cout << std::right << std::fixed << std::setprecision(1); ec_ratio_stat_type::stats_alg_map& stats2 = arc_ratio_stats.stats; - for (unsigned i = 0; i < sizeof(ec_algos) / sizeof(*ec_algos); ++i) + for (unsigned i = 0; i < ec_algos.size(); ++i) { - const char* algo = ec_algos[i].name; + const std::string algo = ec_algos[i].name; - std::cout << std::setw(22) << algo << " " << std::setw(8); + std::cout << std::setw(25) << algo << " " << std::setw(8); ec_iter i = stats2["search space states"].find(algo); if (i != stats2["search space states"].end()) @@ -1225,6 +1250,11 @@ main(int argc, char** argv) dynamic_cast(formula_file)->close(); delete formula_file; } + + if (opt_ec) + for (unsigned i = 0; i < ec_algos.size(); ++i) + delete ec_algos[i].inst; + delete ap; delete apf; delete dict;