diff --git a/ChangeLog b/ChangeLog index 3d79edc1e..e2273d1f5 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,10 @@ +2006-07-18 Alexandre Duret-Lutz + + * src/misc/memusage.cc, src/misc/memusage.hh: New files. + * src/misc/Makefile.am: Add them. + * src/tgbaalgos/gtec/gtec.cc, + src/tgbaalgos/gtec/gtec.hh: Add a "vmsize" statistic. + 2006-07-14 Alexandre Duret-Lutz * src/tgba/bdddict.cc, src/tgba/bdddict.hh (free_annonymous_list_of): diff --git a/src/misc/Makefile.am b/src/misc/Makefile.am index 0e78e6567..41771fd0d 100644 --- a/src/misc/Makefile.am +++ b/src/misc/Makefile.am @@ -1,4 +1,4 @@ -## Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), +## Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de Paris 6 (LIP6), ## département Systèmes Répartis Coopératifs (SRC), Université Pierre ## et Marie Curie. ## @@ -34,6 +34,7 @@ misc_HEADERS = \ hashfunc.hh \ ltstr.hh \ minato.hh \ + memusage.hh \ modgray.hh \ optionmap.hh \ random.hh \ @@ -46,6 +47,7 @@ libmisc_la_SOURCES = \ bddalloc.cc \ escape.cc \ freelist.cc \ + memusage.cc \ minato.cc \ modgray.cc \ optionmap.cc \ diff --git a/src/misc/memusage.cc b/src/misc/memusage.cc new file mode 100644 index 000000000..ce897eb66 --- /dev/null +++ b/src/misc/memusage.cc @@ -0,0 +1,44 @@ +// Copyright (C) 2006 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 "memusage.hh" +#include +#include +#include + +namespace spot +{ + int + memusage() + { + int size; + + FILE* file = fopen("/proc/self/statm", "r"); + if (!file) + return -1; + int res = fscanf(file, "%d", &size); + (void) fclose(file); + if (res != 1) + return -1; + return size; + } + +} diff --git a/src/misc/memusage.hh b/src/misc/memusage.hh new file mode 100644 index 000000000..29f3bfe86 --- /dev/null +++ b/src/misc/memusage.hh @@ -0,0 +1,35 @@ +// Copyright (C) 2006 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_MISC_MEMUSAGE_HH +# define SPOT_MISC_MEMUSAGE_HH + + +namespace spot +{ + /// \brief Total number of pages in use by the program. + /// + /// \return The total number of pages in use by the program if known. + /// -1 otherwise. + int memusage(); +} + +#endif // SPOT_MISC_MEMUSAGE_HH diff --git a/src/tgbaalgos/gtec/gtec.cc b/src/tgbaalgos/gtec/gtec.cc index adb1cb030..c71fbb0ae 100644 --- a/src/tgbaalgos/gtec/gtec.cc +++ b/src/tgbaalgos/gtec/gtec.cc @@ -21,6 +21,7 @@ #include "gtec.hh" #include "ce.hh" +#include "misc/memusage.hh" namespace spot { @@ -40,6 +41,9 @@ namespace spot stats["removed components"] = static_cast (&couvreur99_check::get_removed_components); + stats["vmsize"] = + static_cast + (&couvreur99_check::get_vmsize); } couvreur99_check::~couvreur99_check() @@ -53,6 +57,15 @@ namespace spot return removed_components; } + unsigned + couvreur99_check::get_vmsize() const + { + int size = memusage(); + if (size > 0) + return size; + return 0; + } + void couvreur99_check::remove_component(const state* from) { diff --git a/src/tgbaalgos/gtec/gtec.hh b/src/tgbaalgos/gtec/gtec.hh index 85110aff5..de1918081 100644 --- a/src/tgbaalgos/gtec/gtec.hh +++ b/src/tgbaalgos/gtec/gtec.hh @@ -183,6 +183,7 @@ namespace spot /// Number of dead SCC removed by the algorithm. unsigned removed_components; unsigned get_removed_components() const; + unsigned get_vmsize() const; }; /// \brief A version of spot::couvreur99_check that tries to visit