From 834ce05235930c87a07fb4eaa29c5d194141f7f7 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 2 Feb 2004 17:32:01 +0000 Subject: [PATCH] * src/tgbalagos/stats.hh, src/tgbalagos/stats.cc: New files. * src/tgbalagos/Makefile.am: Add them. * wrap/python/spot.i: Include src/tgbalagos/dupexp.hh and src/tgbalagos/stats.hh --- ChangeLog | 5 ++++ src/tgbaalgos/Makefile.am | 6 ++-- src/tgbaalgos/stats.cc | 61 +++++++++++++++++++++++++++++++++++++++ src/tgbaalgos/stats.hh | 39 +++++++++++++++++++++++++ wrap/python/spot.i | 8 ++++- 5 files changed, 116 insertions(+), 3 deletions(-) create mode 100644 src/tgbaalgos/stats.cc create mode 100644 src/tgbaalgos/stats.hh diff --git a/ChangeLog b/ChangeLog index 37495273a..dcba7a52a 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,10 @@ 2004-02-02 Alexandre Duret-Lutz + * src/tgbalagos/stats.hh, src/tgbalagos/stats.cc: New files. + * src/tgbalagos/Makefile.am: Add them. + * wrap/python/spot.i: Include src/tgbalagos/dupexp.hh and + src/tgbalagos/stats.hh + * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Identify states with identical successors. This optimizes the translation of `a R (b R c)', for instance. diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index 966a11eb2..282ed7de3 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -34,7 +34,8 @@ tgbaalgos_HEADERS = \ magic.hh \ powerset.hh \ reachiter.hh \ - save.hh + save.hh \ + stats.hh noinst_LTLIBRARIES = libtgbaalgos.la libtgbaalgos_la_SOURCES = \ @@ -47,4 +48,5 @@ libtgbaalgos_la_SOURCES = \ magic.cc \ powerset.cc \ reachiter.cc \ - save.cc + save.cc \ + stats.cc diff --git a/src/tgbaalgos/stats.cc b/src/tgbaalgos/stats.cc new file mode 100644 index 000000000..3f59de79a --- /dev/null +++ b/src/tgbaalgos/stats.cc @@ -0,0 +1,61 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include "tgba/tgba.hh" +#include "stats.hh" +#include "reachiter.hh" + +namespace spot +{ + + class stats_bfs : public tgba_reachable_iterator_breadth_first + { + public: + stats_bfs(const tgba* a, tgba_statistics& s) + : tgba_reachable_iterator_breadth_first(a), s_(s) + { + } + + void + process_state(const state*, int, tgba_succ_iterator*) + { + ++s_.states; + } + + void + process_link(int, int, const tgba_succ_iterator*) + { + ++s_.transitions; + } + + private: + tgba_statistics& s_; + }; + + tgba_statistics + stats_reachable(const tgba* g) + { + tgba_statistics s = {0, 0}; + stats_bfs d(g, s); + d.run(); + return s; + } +} diff --git a/src/tgbaalgos/stats.hh b/src/tgbaalgos/stats.hh new file mode 100644 index 000000000..b5f7bc020 --- /dev/null +++ b/src/tgbaalgos/stats.hh @@ -0,0 +1,39 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_TGBAALGOS_STATS_HH +# define SPOT_TGBAALGOS_STATS_HH + +#include "tgba/tgba.hh" + +namespace spot +{ + struct tgba_statistics + { + unsigned transitions; + unsigned states; + }; + + /// \brief Compute statistics for an automata. + tgba_statistics stats_reachable(const tgba* g); +} + +#endif // SPOT_TGBAALGOS_STATS_HH diff --git a/wrap/python/spot.i b/wrap/python/spot.i index d2c25b96f..adbe3c73c 100644 --- a/wrap/python/spot.i +++ b/wrap/python/spot.i @@ -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. // @@ -72,9 +72,11 @@ #include "tgbaalgos/ltl2tgba_lacim.hh" #include "tgbaalgos/ltl2tgba_fm.hh" #include "tgbaalgos/dotty.hh" +#include "tgbaalgos/dupexp.hh" #include "tgbaalgos/lbtt.hh" #include "tgbaalgos/magic.hh" #include "tgbaalgos/save.hh" +#include "tgbaalgos/stats.hh" using namespace spot::ltl; using namespace spot; @@ -110,6 +112,8 @@ using namespace spot; %feature("new") spot::tgba::get_init_state; %feature("new") spot::tgba::succ_iter; %feature("new") spot::tgba_succ_iterator::current_state; +%feature("new") spot::tgba_dupexp_bfs; +%feature("new") spot::tgba_dupexp_dfs; // Help SWIG with namespace lookups. #define ltl spot::ltl @@ -129,9 +133,11 @@ using namespace spot; %include "tgbaalgos/ltl2tgba_lacim.hh" %include "tgbaalgos/ltl2tgba_fm.hh" %include "tgbaalgos/dotty.hh" +%include "tgbaalgos/dupexp.hh" %include "tgbaalgos/lbtt.hh" %include "tgbaalgos/magic.hh" %include "tgbaalgos/save.hh" +%include "tgbaalgos/stats.hh" #undef ltl %extend spot::ltl::formula {