diff --git a/ChangeLog b/ChangeLog index 2af1b7f8f..3b1d9e6e6 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,8 @@ +2005-01-24 Denis Poitrenaud + + * src/tgbatest/randtgba.cc, src/tgbatest/ltl2tgba.cc: Add options + dedicated to display of stats. + 2005-01-24 Alexandre Duret-Lutz * src/tgbatest/randtgba.cc: Some fixes from Denis for ratio stats. diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 9bc3e9302..23f5444c8 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -20,6 +20,7 @@ // 02111-1307, USA. #include +#include #include #include #include @@ -52,6 +53,9 @@ #include "tgbaalgos/replayrun.hh" #include "tgbaalgos/rundotdec.hh" +#include "tgbaalgos/stats.hh" +#include "tgbaalgos/emptiness_stats.hh" + void syntax(char* prog) { @@ -60,6 +64,8 @@ syntax(char* prog) << " "<< prog << " -X [OPTIONS...] file" << std::endl << std::endl << "Options:" << std::endl + << " -0 produce minimal output dedicated to the paper" + << std::endl << " -a display the acceptance_conditions BDD, not the " << "reachability graph" << std::endl @@ -154,6 +160,7 @@ main(int argc, char** argv) int exit_code = 0; bool debug_opt = false; + bool paper_opt = false; enum { NoDegen, DegenTBA, DegenSBA } degeneralize_opt = NoDegen; bool degeneralize_maybe = false; bool fm_opt = false; @@ -186,6 +193,7 @@ main(int argc, char** argv) spot::ltl::atomic_prop_set* unobservables = 0; spot::tgba_explicit* system = 0; spot::tgba* product = 0; + spot::tgba* product_to_free = 0; spot::bdd_dict* dict = new spot::bdd_dict(); for (;;) @@ -195,7 +203,11 @@ main(int argc, char** argv) ++formula_index; - if (!strcmp(argv[formula_index], "-a")) + if (!strcmp(argv[formula_index], "-0")) + { + paper_opt = true; + } + else if (!strcmp(argv[formula_index], "-a")) { output = 2; } @@ -641,8 +653,22 @@ main(int argc, char** argv) break; } + spot::tgba* product_degeneralized = 0; + if (system) - a = product = new spot::tgba_product(system, a); + { + a = product = product_to_free = new spot::tgba_product(system, a); + if (degeneralize_maybe + && degeneralize_opt == NoDegen + && product->number_of_acceptance_conditions() > 1) + degeneralize_opt = DegenTBA; + if (degeneralize_opt == DegenTBA) + a = product = product_degeneralized = + new spot::tgba_tba_proxy(product); + else if (degeneralize_opt == DegenSBA) + a = product = product_degeneralized = + new spot::tgba_sba_proxy(product); + } switch (output) { @@ -726,9 +752,12 @@ main(int argc, char** argv) case Tau03Search: if (a->number_of_acceptance_conditions() == 0) { - std::cout << "To apply tau03_search, the automaton must have at " - << "least one accepting condition. Try with another " - << "algorithm." << std::endl; + if (!paper_opt) + std::cout << "To apply tau03_search, the automaton must have at" + << " least one accepting condition. Try with another" + << " algorithm." << std::endl; + else + std::cout << std::endl; } else { @@ -748,63 +777,100 @@ main(int argc, char** argv) do { spot::emptiness_check_result* res = ec->check(); - if (!graph_run_opt && !graph_run_tgba_opt) - ec->print_stats(std::cout); - if (expect_counter_example != !!res && - (!bit_state_hashing || !expect_counter_example)) - exit_code = 1; - - if (!res) - { - std::cout << "no accepting run found"; - if (bit_state_hashing && expect_counter_example) - { - std::cout << " even if expected" << std::endl; - std::cout << "this is maybe due to the use of the bit " - << "state hashing technic" << std::endl; - std::cout << "you can try to increase the heap size " - << "or use an explicit storage" << std::endl; - } + if (paper_opt) + { + std::ios::fmtflags old = std::cout.flags(); + std::cout << std::left << std::setw(20) + << echeck_algo << ", "; + spot::tgba_statistics a_size = + spot::stats_reachable(ec->automaton()); + std::cout << std::right << std::setw(10) + << a_size.states << ", " + << std::right << std::setw(10) + << a_size.transitions << ", "; + std::cout << + ec->automaton()->number_of_acceptance_conditions() + << ", "; + const spot::ec_statistics* ecs = + dynamic_cast(ec); + if (ecs) + std::cout << std::right << std::setw(10) + << ecs->states() << ", " + << std::right << std::setw(10) + << ecs->transitions() << ", " + << std::right << std::setw(10) + << ecs->max_depth(); + else + std::cout << "no stats,, "; + if (res) + std::cout << ", accepting run found"; + else + std::cout << ", no accepting run found"; std::cout << std::endl; - break; - } - else - { + std::cout << std::setiosflags(old); + } + else + { + if (!graph_run_opt && !graph_run_tgba_opt) + ec->print_stats(std::cout); + if (expect_counter_example != !!res && + (!bit_state_hashing || !expect_counter_example)) + exit_code = 1; - spot::tgba_run* run = res->accepting_run(); - if (!run) - { - std::cout << "an accepting run exists" << std::endl; - } - else - { - if (opt_reduce) - { - spot::tgba_run* redrun = - spot::reduce_run(res->automaton(), run); - delete run; - run = redrun; - } - if (graph_run_opt) - { - spot::tgba_run_dotty_decorator deco(run); - spot::dotty_reachable(std::cout, a, &deco); - } - else if (graph_run_tgba_opt) - { - spot::tgba* ar = spot::tgba_run_to_tgba(a, run); - spot::dotty_reachable(std::cout, ar); - delete ar; - } - else - { - spot::print_tgba_run(std::cout, a, run); - if (!spot::replay_tgba_run(std::cout, a, run, true)) - exit_code = 1; - } - delete run; - } - } + if (!res) + { + std::cout << "no accepting run found"; + if (bit_state_hashing && expect_counter_example) + { + std::cout << " even if expected" << std::endl; + std::cout << "this is maybe due to the use of the bit" + << " state hashing technic" << std::endl; + std::cout << "you can try to increase the heap size " + << "or use an explicit storage" + << std::endl; + } + std::cout << std::endl; + break; + } + else + { + + spot::tgba_run* run = res->accepting_run(); + if (!run) + { + std::cout << "an accepting run exists" << std::endl; + } + else + { + if (opt_reduce) + { + spot::tgba_run* redrun = + spot::reduce_run(res->automaton(), run); + delete run; + run = redrun; + } + if (graph_run_opt) + { + spot::tgba_run_dotty_decorator deco(run); + spot::dotty_reachable(std::cout, a, &deco); + } + else if (graph_run_tgba_opt) + { + spot::tgba* ar = spot::tgba_run_to_tgba(a, run); + spot::dotty_reachable(std::cout, ar); + delete ar; + } + else + { + spot::print_tgba_run(std::cout, a, run); + if (!spot::replay_tgba_run(std::cout, a, run, + true)) + exit_code = 1; + } + delete run; + } + } + } delete res; } while (search_many); @@ -813,7 +879,8 @@ main(int argc, char** argv) if (f) spot::ltl::destroy(f); - delete product; + delete product_degeneralized; + delete product_to_free; delete system; delete expl; delete degeneralized; diff --git a/src/tgbatest/randtgba.cc b/src/tgbatest/randtgba.cc index 379c834f7..807eff267 100644 --- a/src/tgbatest/randtgba.cc +++ b/src/tgbatest/randtgba.cc @@ -133,6 +133,7 @@ syntax(char* prog) << "Options:" << std::endl << " -0 suppress default output, just generate the graph" << " in memory" << std::endl + << " -1 produce minimal output dedicated to the paper" << " -a N F number of acceptance conditions and probability that" << " one is true" << std::endl << " [0 0.0]" << std::endl @@ -492,70 +493,95 @@ print_ar_stats(ar_stats_type& ar_stats) } void -print_ratio_stats(const std::string& s, const ratio_stat_type& ratio_stats) +print_ratio_stats(const std::string& s, const ratio_stat_type& ratio_stats, + bool opt_paper = false) { - std::cout << std::endl; std::ios::fmtflags old = std::cout.flags(); - std::cout << std::right << std::fixed << std::setprecision(1); - - std::cout << "Ratios in case of non-emptiness (" << s << ")" - << std::endl; - std::cout << "" << std::endl; - std::cout << std::setw(22) << "" - << " | % states | % transitions |" - << std::endl << std::setw(22) << "algorithm" - << " | min < mean < max | min < mean < max | n" - << std::endl - << std::setw(79) << std::setfill('-') << "" << std::setfill(' ') - << std::endl; - for (ratio_stat_type::const_iterator i = ratio_stats.begin(); - i != ratio_stats.end(); ++i) - std::cout << std::setw(22) << i->first << " |" - << std::setw(6) << i->second.min_ratio_states * 100. - << " " - << std::setw(8) - << (static_cast(i->second.tot_ratio_states) / - i->second.n) * 100. - << " " - << std::setw(6) << i->second.max_ratio_states * 100. - << " |" - << std::setw(6) << i->second.min_ratio_transitions * 100. - << " " - << std::setw(8) - << (static_cast(i->second.tot_ratio_transitions) / - i->second.n) * 100. - << " " - << std::setw(6) << i->second.max_ratio_transitions * 100. - << " |" - << std::setw(4) << i->second.n - << std::endl; - std::cout << std::setw(79) << std::setfill('-') << "" << std::setfill(' ') - << std::endl - << std::setw(22) << "" - << " | % maximal depth |" - << std::endl - << std::setw(22) << "algorithm" - << " | min < mean < max | n" - << std::endl - << std::setw(53) << std::setfill('-') << "" << std::setfill(' ') - << std::endl; - for (ratio_stat_type::const_iterator i = ratio_stats.begin(); - i != ratio_stats.end(); ++i) - std::cout << std::setw(22) << i->first << " |" - << std::setw(6) - << i->second.min_ratio_depth * 100. - << " " - << std::setw(8) - << (static_cast(i->second.tot_ratio_depth) / - i->second.n) * 100. - << " " - << std::setw(6) - << i->second.max_ratio_depth * 100. - << " |" - << std::setw(4) << i->second.n - << std::endl; - + if (opt_paper) + { + std::cout << "ratios (" << s << ")" << std::endl; + std::cout << std::right << std::fixed << std::setprecision(1); + for (ratio_stat_type::const_iterator i = ratio_stats.begin(); + i != ratio_stats.end(); ++i) + { + std::cout << std::setw(22) << i->first << " " + << std::setw(8) + << (static_cast(i->second.tot_ratio_states) / + i->second.n) * 100. + << " " + << std::setw(8) + << (static_cast(i->second.tot_ratio_transitions) / + i->second.n) * 100. + << " " + << std::setw(8) + << (static_cast(i->second.tot_ratio_depth) / + i->second.n) * 100. + << std::setw(4) << i->second.n + << std::endl; + } + } + else + { + std::cout << std::endl; + std::cout << std::right << std::fixed << std::setprecision(1); + std::cout << "Ratios in case of non-emptiness (" << s << ")" + << std::endl; + std::cout << "" << std::endl; + std::cout << std::setw(22) << "" + << " | % states | % transitions |" + << std::endl << std::setw(22) << "algorithm" + << " | min < mean < max | min < mean < max | n" + << std::endl + << std::setw(79) << std::setfill('-') << "" + << std::setfill(' ') << std::endl; + for (ratio_stat_type::const_iterator i = ratio_stats.begin(); + i != ratio_stats.end(); ++i) + std::cout << std::setw(22) << i->first << " |" + << std::setw(6) << i->second.min_ratio_states * 100. + << " " + << std::setw(8) + << (static_cast(i->second.tot_ratio_states) / + i->second.n) * 100. + << " " + << std::setw(6) << i->second.max_ratio_states * 100. + << " |" + << std::setw(6) << i->second.min_ratio_transitions * 100. + << " " + << std::setw(8) + << (static_cast(i->second.tot_ratio_transitions) / + i->second.n) * 100. + << " " + << std::setw(6) << i->second.max_ratio_transitions * 100. + << " |" + << std::setw(4) << i->second.n + << std::endl; + std::cout << std::setw(79) << std::setfill('-') << "" + << std::setfill(' ') << std::endl + << std::setw(22) << "" + << " | % maximal depth |" + << std::endl + << std::setw(22) << "algorithm" + << " | min < mean < max | n" + << std::endl + << std::setw(53) << std::setfill('-') << "" + << std::setfill(' ') << std::endl; + for (ratio_stat_type::const_iterator i = ratio_stats.begin(); + i != ratio_stats.end(); ++i) + std::cout << std::setw(22) << i->first << " |" + << std::setw(6) + << i->second.min_ratio_depth * 100. + << " " + << std::setw(8) + << (static_cast(i->second.tot_ratio_depth) / + i->second.n) * 100. + << " " + << std::setw(6) + << i->second.max_ratio_depth * 100. + << " |" + << std::setw(4) << i->second.n + << std::endl; + } std::cout << std::setiosflags(old); } @@ -614,6 +640,7 @@ generate_formula(const spot::ltl::random_ltl& rl, int opt_f, int opt_s, int main(int argc, char** argv) { + bool opt_paper = false; bool opt_dp = false; int opt_f = 15; int opt_F = 0; @@ -663,6 +690,10 @@ main(int argc, char** argv) { opt_0 = true; } + else if (!strcmp(argv[argn], "-1")) + { + opt_paper = true; + } else if (!strcmp(argv[argn], "-a")) { if (argc < argn + 3) @@ -889,7 +920,8 @@ main(int argc, char** argv) { if (opt_ec) { - std::cout << "seed: " << opt_ec_seed << std::endl; + if (!opt_paper) + std::cout << "seed: " << opt_ec_seed << std::endl; spot::srand(opt_ec_seed); } @@ -932,8 +964,11 @@ main(int argc, char** argv) continue; ++n_ec; std::string algo = ec_algos[i].name; - std::cout.width(32); - std::cout << algo << ": "; + if (!opt_paper) + { + std::cout.width(32); + std::cout << algo << ": "; + } tm_ec.start(algo); for (int count = opt_R;;) { @@ -960,7 +995,8 @@ main(int argc, char** argv) } if (res) { - std::cout << "acc. run"; + if (!opt_paper) + std::cout << "acc. run"; ++n_non_empty; const spot::acss_statistics* acss = dynamic_cast(res); @@ -991,7 +1027,8 @@ main(int argc, char** argv) if (!run) { tm_ar.cancel(algo); - std::cout << " exists, not computed"; + if (!opt_paper) + std::cout << " exists, not computed"; } else { @@ -1000,17 +1037,19 @@ main(int argc, char** argv) if (!spot::replay_tgba_run(s, res->automaton(), run)) { - std::cout << ", but could not replay it " - << "(ERROR!)"; + if (!opt_paper) + std::cout << ", but could not replay it " + << "(ERROR!)"; failed_seeds.insert(opt_ec_seed); } else { - std::cout << ", computed"; + if (!opt_paper) + std::cout << ", computed"; if (opt_z) ar_stats[algo].count(run); } - if (opt_z) + if (opt_z && !opt_paper) std::cout << " [" << run->prefix.size() << "+" << run->cycle.size() << "]"; @@ -1022,8 +1061,9 @@ main(int argc, char** argv) if (!spot::replay_tgba_run(s, res->automaton(), redrun)) { - std::cout << ", but could not replay " - << "its minimization (ERROR!)"; + if (!opt_paper) + std::cout << ", but could not replay " + << "its minimization (ERROR!)"; failed_seeds.insert(opt_ec_seed); } else @@ -1032,7 +1072,7 @@ main(int argc, char** argv) if (opt_z) mar_stats[algo].count(redrun); } - if (opt_z) + if (opt_z && !opt_paper) { std::cout << " [" << redrun->prefix.size() << "+" << redrun->cycle.size() @@ -1043,25 +1083,28 @@ main(int argc, char** argv) delete run; } } - std::cout << std::endl; + if (!opt_paper) + std::cout << std::endl; delete res; } else { if (ec_algos[i].safe) { - std::cout << "empty language" << std::endl; + if (!opt_paper) + std::cout << "empty language" << std::endl; ++n_empty; } else { - std::cout << "maybe empty language" << std::endl; + if (!opt_paper) + std::cout << "maybe empty language" << std::endl; ++n_maybe_empty; } } - if (opt_Z) + if (opt_Z && !opt_paper) ec->print_stats(std::cout); delete ec; } @@ -1100,7 +1143,7 @@ main(int argc, char** argv) } while (opt_F || opt_i); - if (!ec_stats.empty()) + if (!opt_paper && !ec_stats.empty()) { std::cout << std::endl; std::ios::fmtflags old = std::cout.flags(); @@ -1163,20 +1206,19 @@ main(int argc, char** argv) if (!glob_ratio_stats.empty()) { - print_ratio_stats("all tests", glob_ratio_stats); + print_ratio_stats("all tests", glob_ratio_stats, opt_paper); if (ratio_stats.size() > 1) for (ratio_stats_type::const_iterator i = ratio_stats.begin(); i != ratio_stats.end(); ++i) { std::ostringstream s; s << "tests with " << i->first << " acceptance conditions"; - print_ratio_stats(s.str(), i->second); + print_ratio_stats(s.str(), i->second, opt_paper); } } - - if (!acss_stats.empty()) + if (!opt_paper && !acss_stats.empty()) { std::cout << std::endl; std::ios::fmtflags old = std::cout.flags(); @@ -1207,7 +1249,8 @@ main(int argc, char** argv) << std::endl; std::cout << std::setiosflags(old); } - if (!ars_stats.empty()) + + if (!opt_paper && !ars_stats.empty()) { std::cout << std::endl; std::ios::fmtflags old = std::cout.flags(); @@ -1239,20 +1282,20 @@ main(int argc, char** argv) std::cout << std::setiosflags(old); } - if (!ar_stats.empty()) + if (!opt_paper && !ar_stats.empty()) { std::cout << std::endl << "Statistics about accepting runs:" << std::endl; print_ar_stats(ar_stats); } - if (!mar_stats.empty()) + if (!opt_paper && !mar_stats.empty()) { std::cout << std::endl << "Statistics about reduced accepting runs:" << std::endl; print_ar_stats(mar_stats); } - if (opt_z) + if (!opt_paper && opt_z) { if (!tm_ec.empty()) {