From 7a54e048008a58a115a8c15cea94e8d278cea668 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 9 Jan 2004 10:56:56 +0000 Subject: [PATCH] * src/tgbaalgos/emptinesscheck.cc (emptiness_check::print_stats): New function. * src/tgbaalgos/emptinesscheck.hh (emptiness_check::print_stats): Likewise. * iface/gspn/ltlgspn.cc (main) : Call print_stats(). * iface/gspn/ltleesrg.cc (main): Likewise. --- ChangeLog | 7 +++++++ iface/gspn/ltleesrg.cc | 5 ++++- iface/gspn/ltlgspn.cc | 5 ++++- src/tgbaalgos/emptinesscheck.cc | 13 +++++++++++++ src/tgbaalgos/emptinesscheck.hh | 8 +++++++- 5 files changed, 35 insertions(+), 3 deletions(-) diff --git a/ChangeLog b/ChangeLog index f391aea14..568aeee39 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,12 @@ 2004-01-09 Alexandre Duret-Lutz + * src/tgbaalgos/emptinesscheck.cc (emptiness_check::print_stats): + New function. + * src/tgbaalgos/emptinesscheck.hh (emptiness_check::print_stats): + Likewise. + * iface/gspn/ltlgspn.cc (main) : Call print_stats(). + * iface/gspn/ltleesrg.cc (main): Likewise. + * iface/gspn/ltlgspn.cc: Add option -P. 2004-01-08 Alexandre Duret-Lutz diff --git a/iface/gspn/ltleesrg.cc b/iface/gspn/ltleesrg.cc index 91618593f..95d5bc473 100644 --- a/iface/gspn/ltleesrg.cc +++ b/iface/gspn/ltleesrg.cc @@ -75,12 +75,15 @@ main(int argc, char **argv) { ec.counter_example(); ec.print_result(std::cout, &a); - exit(1); } else { std::cout << "empty" << std::endl; } + std::cout << std::endl; + ec.print_stats(std::cout); + if (!res) + exit(1); } delete prod; diff --git a/iface/gspn/ltlgspn.cc b/iface/gspn/ltlgspn.cc index a92950163..b7a540dea 100644 --- a/iface/gspn/ltlgspn.cc +++ b/iface/gspn/ltlgspn.cc @@ -146,12 +146,15 @@ main(int argc, char **argv) { std::cout << "non empty" << std::endl; } - exit(1); } else { std::cout << "empty" << std::endl; } + std::cout << std::endl; + ec.print_stats(std::cout); + if (!res) + exit(1); } break; case Magic: diff --git a/src/tgbaalgos/emptinesscheck.cc b/src/tgbaalgos/emptinesscheck.cc index 15a957289..6dac90d6b 100644 --- a/src/tgbaalgos/emptinesscheck.cc +++ b/src/tgbaalgos/emptinesscheck.cc @@ -633,4 +633,17 @@ namespace spot // forming a cycle. complete_cycle(scc, start, suffix.back()); } + + + void + emptiness_check::print_stats(std::ostream& os) const + { + os << h.size() << " unique states visited" << std::endl; + os << suffix.size() << " states in suffix" << std::endl; + os << period.size() << " states in period" << std::endl; + os << root.size() + << " strongly connected components in search stack" + << std::endl; + } + } diff --git a/src/tgbaalgos/emptinesscheck.hh b/src/tgbaalgos/emptinesscheck.hh index c1366d297..8c784bb29 100644 --- a/src/tgbaalgos/emptinesscheck.hh +++ b/src/tgbaalgos/emptinesscheck.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -68,9 +68,15 @@ namespace spot /// Compute a counter example if tgba_emptiness_check() returned false. void counter_example(); + /// \brief Display the example computed by counter_example(). + /// + /// \param restrict optional automaton to project the example on. std::ostream& print_result(std::ostream& os, const tgba* restrict = 0) const; + /// Output statistics about this object. + void print_stats(std::ostream& os) const; + private: struct connected_component