diff --git a/ChangeLog b/ChangeLog index 3b3f56ee2..acf19300c 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,10 @@ +2008-12-05 Alexandre Duret-Lutz + + * src/tgbatest/ltl2tgba.cc (-k): New option that calls + stats_reachable(a).dump(). + * src/tgbaalgos/stats.cc, src/tgbaalgos/stats.hh: + Add tgba_statistics::dump(). + 2008-08-29 Alexandre Duret-Lutz * bench/gspn-ssp/tools/modelgen-create: Remove and fold into ... diff --git a/src/tgbaalgos/stats.cc b/src/tgbaalgos/stats.cc index b8883ea3e..a93a97fe1 100644 --- a/src/tgbaalgos/stats.cc +++ b/src/tgbaalgos/stats.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -19,6 +19,7 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. +#include #include "tgba/tgba.hh" #include "stats.hh" #include "reachiter.hh" @@ -53,6 +54,14 @@ namespace spot }; } // anonymous + + std::ostream& tgba_statistics::dump(std::ostream& out) const + { + out << "transitions: " << transitions << std::endl; + out << "states: " << states << std::endl; + return out; + } + tgba_statistics stats_reachable(const tgba* g) { diff --git a/src/tgbaalgos/stats.hh b/src/tgbaalgos/stats.hh index affcf3e30..50971fd53 100644 --- a/src/tgbaalgos/stats.hh +++ b/src/tgbaalgos/stats.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -23,6 +23,7 @@ # define SPOT_TGBAALGOS_STATS_HH #include "tgba/tgba.hh" +#include namespace spot { @@ -34,6 +35,8 @@ namespace spot { unsigned transitions; unsigned states; + + std::ostream& dump(std::ostream& out) const; }; /// \brief Compute statistics for an automaton. diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index c0d2d5039..937c588a4 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -89,6 +89,8 @@ syntax(char* prog) << std::endl << " -G graph the accepting run seen as an automaton " << " (requires -e)" << std::endl + << " -k display statistics on the TGBA instead of dumping it" + << std::endl << " -L fair-loop approximation (implies -f)" << std::endl << " -m try to reduce accepting runs, in a second pass" << std::endl @@ -318,6 +320,10 @@ main(int argc, char** argv) { graph_run_tgba_opt = true; } + else if (!strcmp(argv[formula_index], "-k")) + { + output = 9; + } else if (!strcmp(argv[formula_index], "-L")) { fair_loop_approx = true; @@ -723,6 +729,9 @@ main(int argc, char** argv) spot::never_claim_reachable(std::cout, s, f); break; } + case 9: + stats_reachable(a).dump(std::cout); + break; default: assert(!"unknown output option"); }