diff --git a/ChangeLog b/ChangeLog index 32de0c1b1..8fd2b761e 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,9 @@ 2004-10-29 Alexandre Duret-Lutz + * src/tgbaalgos/gtec/gtec.cc, + src/tgbaalgos/gtec/gtec.hh (couvreur99_check::print_stats): New. + * src/tgbatest/ltl2tgba.cc: Print emptiness-check statistics. + * src/sanity/style.test: Diagnose superfluous constructs such as `if (x) delete x;'. * iface/gspn/gspn.cc, iface/gspn/ssp.cc, src/ltlvisit/basicreduce.cc, diff --git a/src/tgbaalgos/gtec/gtec.cc b/src/tgbaalgos/gtec/gtec.cc index a60eee5ca..cc8e33013 100644 --- a/src/tgbaalgos/gtec/gtec.cc +++ b/src/tgbaalgos/gtec/gtec.cc @@ -234,6 +234,13 @@ namespace spot return ecs_; } + std::ostream& + couvreur99_check::print_stats(std::ostream& os) const + { + ecs_->print_stats(os); + return os; + } + ////////////////////////////////////////////////////////////////////// couvreur99_check_shy::couvreur99_check_shy(const tgba* a, diff --git a/src/tgbaalgos/gtec/gtec.hh b/src/tgbaalgos/gtec/gtec.hh index 91916fa93..f3fdbe720 100644 --- a/src/tgbaalgos/gtec/gtec.hh +++ b/src/tgbaalgos/gtec/gtec.hh @@ -79,6 +79,8 @@ namespace spot /// Check whether the automaton's language is empty. virtual emptiness_check_result* check(); + virtual std::ostream& print_stats(std::ostream& os) const; + /// \brief Return the status of the emptiness-check. /// /// When check() succeed, the status should be passed along diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index e75f2d5af..39b2ef60e 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -58,9 +58,10 @@ syntax(char* prog) << " -A same as -a, but as a set" << std::endl << " -d turn on traces during parsing" << std::endl << " -D degeneralize the automaton" << std::endl - << " -eALGO emptiness-check, expect and compute an accepting run" + << " -e[ALGO] emptiness-check, expect and compute an " + << "accepting run" << std::endl + << " -E[ALGO] emptiness-check, expect no accepting run" << std::endl - << " -EALGO emptiness-check, expect no accepting run" << std::endl << " -f use Couvreur's FM algorithm for translation" << std::endl << " -F read the formula from the file" << std::endl @@ -113,7 +114,7 @@ syntax(char* prog) << "(implies -f)" << std::endl << std::endl << "Where ALGO should be one of:" << std::endl - << " couvreur99" << std::endl + << " couvreur99 (the default)" << std::endl << " couvreur99_shy" << std::endl << " magic_search" << std::endl << " magic_search_repeated" << std::endl; @@ -560,6 +561,7 @@ main(int argc, char** argv) do { spot::emptiness_check_result* res = ec->check(); + ec->print_stats(std::cout); if (expect_counter_example != !!res) exit_code = 1;