diff --git a/ChangeLog b/ChangeLog index 02c47cdcc..ed8bae91f 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,14 @@ +2009-11-07 Alexandre Duret-Lutz + + Make it easier to debug reference counts in LTL nodes. + + * src/ltlast/automatop.cc, src/ltlast/automatop.hh, + src/ltlast/binop.cc, src/ltlast/binop.hh, src/ltlast/multop.cc, + src/ltlast/multop.hh, src/ltlast/unop.cc, src/ltlast/unop.hh: + Add a dump_instance() static method to all class. + * src/ltltest/readltl.cc: Add option -r to dump all instances + with their reference count, after parsing and after deletion. + 2009-11-07 Alexandre Duret-Lutz Better types for instance maps. diff --git a/src/ltlast/automatop.cc b/src/ltlast/automatop.cc index 4d8823da6..f5b8b8c5e 100644 --- a/src/ltlast/automatop.cc +++ b/src/ltlast/automatop.cc @@ -117,5 +117,19 @@ namespace spot { return instances.size(); } + + std::ostream& + automatop::dump_instances(std::ostream& os) + { + for (map::iterator i = instances.begin(); i != instances.end(); ++i) + { + os << i->second << " = " + << i->second->ref_count_() << " * " + << i->second->dump() + << std::endl; + } + return os; + } + } } diff --git a/src/ltlast/automatop.hh b/src/ltlast/automatop.hh index a65842168..93667fb8c 100644 --- a/src/ltlast/automatop.hh +++ b/src/ltlast/automatop.hh @@ -24,6 +24,7 @@ # define SPOT_LTLAST_AUTOMATOP_HH # include +# include # include # include "nfa.hh" # include "refformula.hh" @@ -72,6 +73,10 @@ namespace spot /// Number of instantiated multop operators. For debugging. static unsigned instance_count(); + /// Dump all instances. For debugging. + static std::ostream& dump_instances(std::ostream& os); + + protected: typedef std::pair, vec*> triplet; /// Comparison functor used internally by ltl::automatop. diff --git a/src/ltlast/binop.cc b/src/ltlast/binop.cc index 65dfad1e3..04692d726 100644 --- a/src/ltlast/binop.cc +++ b/src/ltlast/binop.cc @@ -1,6 +1,6 @@ -// Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. +// Copyright (C) 2003, 2005, 2009 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. // @@ -23,6 +23,7 @@ #include #include "binop.hh" #include "visitor.hh" +#include namespace spot { @@ -149,5 +150,21 @@ namespace spot { return instances.size(); } + + std::ostream& + binop::dump_instances(std::ostream& os) + { + for (map::iterator i = instances.begin(); i != instances.end(); ++i) + { + os << i->second << " = " + << i->second->ref_count_() << " * " + << i->second->dump() + << std::endl; + } + return os; + + } + + } } diff --git a/src/ltlast/binop.hh b/src/ltlast/binop.hh index 9fdd195c7..23f5872d5 100644 --- a/src/ltlast/binop.hh +++ b/src/ltlast/binop.hh @@ -1,6 +1,6 @@ -// 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. +// Copyright (C) 2003, 2004, 2009 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. // @@ -28,6 +28,7 @@ # define SPOT_LTLAST_BINOP_HH #include +#include #include "refformula.hh" namespace spot @@ -70,6 +71,9 @@ namespace spot /// Number of instantiated binary operators. For debugging. static unsigned instance_count(); + /// Dump all instances. For debugging. + static std::ostream& dump_instances(std::ostream& os); + protected: typedef std::pair pairf; typedef std::pair pair; diff --git a/src/ltlast/multop.cc b/src/ltlast/multop.cc index 1e00d07cb..47363cced 100644 --- a/src/ltlast/multop.cc +++ b/src/ltlast/multop.cc @@ -1,6 +1,6 @@ -// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. +// Copyright (C) 2003, 2004, 2005, 2009 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. // @@ -22,6 +22,7 @@ #include #include #include +#include #include "multop.hh" #include "constant.hh" #include "visitor.hh" @@ -208,5 +209,19 @@ namespace spot { return instances.size(); } + + std::ostream& + multop::dump_instances(std::ostream& os) + { + for (map::iterator i = instances.begin(); i != instances.end(); ++i) + { + os << i->second << " = " + << i->second->ref_count_() << " * " + << i->second->dump() + << std::endl; + } + return os; + } + } } diff --git a/src/ltlast/multop.hh b/src/ltlast/multop.hh index 97f531ba8..0ab9b72ca 100644 --- a/src/ltlast/multop.hh +++ b/src/ltlast/multop.hh @@ -1,6 +1,6 @@ -// 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. +// Copyright (C) 2003, 2004, 2009 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. // @@ -26,6 +26,7 @@ #include #include +#include #include "refformula.hh" namespace spot @@ -95,6 +96,9 @@ namespace spot /// Number of instantiated multi-operand operators. For debugging. static unsigned instance_count(); + /// Dump all instances. For debugging. + static std::ostream& dump_instances(std::ostream& os); + protected: typedef std::pair pair; /// Comparison functor used internally by ltl::multop. diff --git a/src/ltlast/unop.cc b/src/ltlast/unop.cc index 14e946f25..17846baee 100644 --- a/src/ltlast/unop.cc +++ b/src/ltlast/unop.cc @@ -1,6 +1,6 @@ -// Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. +// Copyright (C) 2003, 2005, 2009 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. // @@ -22,6 +22,7 @@ #include "unop.hh" #include "visitor.hh" #include +#include namespace spot { @@ -117,5 +118,19 @@ namespace spot { return instances.size(); } + + std::ostream& + unop::dump_instances(std::ostream& os) + { + for (map::iterator i = instances.begin(); i != instances.end(); ++i) + { + os << i->second << " = " + << i->second->ref_count_() << " * " + << i->second->dump() + << std::endl; + } + return os; + } + } } diff --git a/src/ltlast/unop.hh b/src/ltlast/unop.hh index 8a650d77a..e0bbf8879 100644 --- a/src/ltlast/unop.hh +++ b/src/ltlast/unop.hh @@ -1,6 +1,6 @@ -// 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. +// Copyright (C) 2003, 2004, 2009 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. // @@ -25,6 +25,7 @@ # define SPOT_LTLAST_UNOP_HH #include +#include #include "refformula.hh" namespace spot @@ -59,6 +60,9 @@ namespace spot /// Number of instantiated unary operators. For debugging. static unsigned instance_count(); + /// Dump all instances. For debugging. + static std::ostream& dump_instances(std::ostream& os); + protected: typedef std::pair pair; typedef std::map map; diff --git a/src/ltltest/readltl.cc b/src/ltltest/readltl.cc index b32e6b1d6..b4eebfa21 100644 --- a/src/ltltest/readltl.cc +++ b/src/ltltest/readltl.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2008 Laboratoire d'Informatique de Paris 6 +// Copyright (C) 2003, 2008, 2009 Laboratoire d'Informatique de Paris 6 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université // Pierre et Marie Curie. // @@ -36,6 +36,16 @@ syntax(char* prog) exit(2); } +void +dump_instances(const std::string& label) +{ + std::cerr << "=== " << label << " ===" << std::endl; + spot::ltl::atomic_prop::dump_instances(std::cerr); + spot::ltl::unop::dump_instances(std::cerr); + spot::ltl::binop::dump_instances(std::cerr); + spot::ltl::multop::dump_instances(std::cerr); +} + int main(int argc, char** argv) { @@ -45,6 +55,7 @@ main(int argc, char** argv) syntax(argv[0]); bool debug = false; + bool debug_ref = false; int formula_index = 1; if (!strcmp(argv[1], "-d")) @@ -54,6 +65,13 @@ main(int argc, char** argv) syntax(argv[0]); formula_index = 2; } + else if (!strcmp(argv[1], "-r")) + { + debug_ref = true; + if (argc < 3) + syntax(argv[0]); + formula_index = 2; + } spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::ltl::parse_error_list pel; @@ -63,8 +81,12 @@ main(int argc, char** argv) exit_code = spot::ltl::format_parse_errors(std::cerr, argv[formula_index], pel); + if (f) { + if (debug_ref) + dump_instances("before"); + #ifdef DOTTY spot::ltl::dotty(std::cout, f); #else @@ -72,6 +94,9 @@ main(int argc, char** argv) std::cout << std::endl; #endif spot::ltl::destroy(f); + + if (debug_ref) + dump_instances("after"); } else {