diff --git a/ChangeLog b/ChangeLog index 6eec90381..a32b7d73b 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,15 @@ +2009-11-07 Alexandre Duret-Lutz + + Add missing instance_count() in automatop and eltl2tgba. + + * src/ltlast/automatop.hh, src/ltlast/automatop.cc: Add missing + instance_count() functions. + * src/tgbatests/eltl2tgba.cc: Add missing instance_count() + assertions at the end. + * src/tgbatests/ltl2tgba.cc: Also call automatop::instance_count(), + even if automatop are not used in ltl2tgba yet. This way we won't + forget once eltl2tgba and ltl2tgba are merged. + 2009-11-07 Damien Lefortier * src/tgba/taa.cc, src/tgbatest/taa.cc: Adjust. diff --git a/src/ltlast/automatop.cc b/src/ltlast/automatop.cc index 113ec89fd..4d8823da6 100644 --- a/src/ltlast/automatop.cc +++ b/src/ltlast/automatop.cc @@ -1,6 +1,5 @@ -// Copyright (C) 2008 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. +// Copyright (C) 2008, 2009 Laboratoire de Recherche et Developpement +// de l'Epita (LRDE) // // This file is part of Spot, a model checking library. // @@ -112,5 +111,11 @@ namespace spot { return negated_; } + + unsigned + automatop::instance_count() + { + return instances.size(); + } } } diff --git a/src/ltlast/automatop.hh b/src/ltlast/automatop.hh index ae1305cd2..c25721462 100644 --- a/src/ltlast/automatop.hh +++ b/src/ltlast/automatop.hh @@ -1,6 +1,5 @@ -// Copyright (C) 2008 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. +// Copyright (C) 2008, 2009 Laboratoire de Recherche et Developpement +// de l'Epita (LRDE) // // This file is part of Spot, a model checking library. // @@ -70,6 +69,9 @@ namespace spot bool is_negated() const; + /// Number of instantiated multop operators. For debugging. + static unsigned instance_count(); + protected: typedef std::pair, vec*> triplet; /// Comparison functor used internally by ltl::automatop. diff --git a/src/tgbatest/eltl2tgba.cc b/src/tgbatest/eltl2tgba.cc index a5d604d58..9a58a231e 100644 --- a/src/tgbatest/eltl2tgba.cc +++ b/src/tgbatest/eltl2tgba.cc @@ -1,6 +1,5 @@ -// Copyright (C) 2008 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. +// Copyright (C) 2008, 2009 Laboratoire de Recherche et Developpement +// de l'Epita (LRDE) // // This file is part of Spot, a model checking library. // @@ -32,6 +31,7 @@ #include "tgbaalgos/save.hh" #include "ltlvisit/destroy.hh" #include "ltlvisit/tostring.hh" +#include "ltlast/allnodes.hh" void syntax(char* prog) @@ -142,5 +142,11 @@ main(int argc, char** argv) spot::ltl::destroy(f); delete concrete; + + assert(spot::ltl::atomic_prop::instance_count() == 0); + assert(spot::ltl::unop::instance_count() == 0); + assert(spot::ltl::binop::instance_count() == 0); + assert(spot::ltl::multop::instance_count() == 0); + assert(spot::ltl::automatop::instance_count() == 0); delete dict; } diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 3d22e70be..a78bcf793 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -930,6 +930,7 @@ main(int argc, char** argv) assert(spot::ltl::unop::instance_count() == 0); assert(spot::ltl::binop::instance_count() == 0); assert(spot::ltl::multop::instance_count() == 0); + assert(spot::ltl::automatop::instance_count() == 0); delete dict; return exit_code; }