From 77df39b4ddda0418159b808a1a0a56cfd05e701d Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 9 Nov 2009 06:54:52 +0100 Subject: [PATCH] Deprecate ltl::destroy(f) in favor of f->destroy() * src/ltlast/formula.cc, src/ltlast/formula.hh (formula::clone): Transform this static function into a member function. * src/ltlvisit/destroy.hh (destroy): Document and declare as deprecated. * bench/split-product/cutscc.cc, iface/gspn/ltlgspn.cc, src/eltlparse/eltlparse.yy, src/eltltest/acc.cc, src/evtgbaalgos/tgba2evtgba.cc, src/evtgbatest/ltl2evtgba.cc, src/ltlast/automatop.cc, src/ltlast/binop.cc, src/ltlast/multop.cc, src/ltlast/unop.cc, src/ltlenv/declenv.cc, src/ltlenv/declenv.hh, src/ltlparse/ltlparse.yy, src/ltltest/equals.cc, src/ltltest/randltl.cc, src/ltltest/readltl.cc, src/ltltest/reduc.cc, src/ltltest/syntimpl.cc, src/ltltest/tostring.cc, src/ltlvisit/destroy.cc src/ltlvisit/basicreduce.cc, src/ltlvisit/contain.cc, src/ltlvisit/reduce.cc, src/ltlvisit/syntimpl.cc, src/tgba/bdddict.cc, src/tgba/bddprint.cc, src/tgba/taa.cc, src/tgba/tgbabddconcretefactory.cc, src/tgba/tgbaexplicit.cc, src/tgba/tgbafromfile.cc, src/tgbaalgos/eltl2tgba_lacim.cc, src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_lacim.cc, src/tgbaalgos/neverclaim.cc, src/tgbaalgos/randomgraph.cc, src/tgbaparse/tgbaparse.yy, src/tgbatest/complementation.cc, src/tgbatest/eltl2tgba.cc, src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlprod.cc, src/tgbatest/mixprod.cc, src/tgbatest/randtgba.cc, src/tgbatest/reductgba.cc, wrap/python/cgi/ltl2tgba.in, wrap/python/tests/ltl2tgba.py, wrap/python/tests/ltlparse.py, wrap/python/tests/ltlsimple.py: Adjust destroy() usage, and remove the #include "destroy.hh" when appropriate. --- ChangeLog | 34 ++++++++++++++++++++++++++ bench/split-product/cutscc.cc | 1 - iface/gspn/ltlgspn.cc | 5 ++-- src/eltlparse/eltlparse.yy | 14 +++++------ src/eltltest/acc.cc | 14 +++++------ src/evtgbaalgos/tgba2evtgba.cc | 3 +-- src/evtgbatest/ltl2evtgba.cc | 7 +++--- src/ltlast/atomic_prop.cc | 6 ++--- src/ltlast/automatop.cc | 4 ++-- src/ltlast/binop.cc | 8 +++---- src/ltlast/formula.cc | 6 ++--- src/ltlast/formula.hh | 2 +- src/ltlast/multop.cc | 8 +++---- src/ltlast/unop.cc | 4 ++-- src/ltlenv/declenv.cc | 2 +- src/ltlenv/declenv.hh | 3 +-- src/ltlparse/ltlparse.yy | 5 ++-- src/ltltest/equals.cc | 19 +++++++-------- src/ltltest/randltl.cc | 9 ++++--- src/ltltest/readltl.cc | 3 +-- src/ltltest/reduc.cc | 25 ++++++++++---------- src/ltltest/syntimpl.cc | 11 ++++----- src/ltltest/tostring.cc | 7 +++--- src/ltlvisit/basicreduce.cc | 38 ++++++++++++++---------------- src/ltlvisit/contain.cc | 33 +++++++++++++------------- src/ltlvisit/destroy.cc | 2 +- src/ltlvisit/destroy.hh | 10 +++++++- src/ltlvisit/reduce.cc | 33 +++++++++++++------------- src/ltlvisit/syntimpl.cc | 25 ++++++++++---------- src/tgba/bdddict.cc | 5 ++-- src/tgba/bddprint.cc | 5 ++-- src/tgba/taa.cc | 5 ++-- src/tgba/tgbabddconcretefactory.cc | 4 ++-- src/tgba/tgbaexplicit.cc | 9 ++++--- src/tgba/tgbafromfile.cc | 4 +--- src/tgbaalgos/eltl2tgba_lacim.cc | 9 ++++--- src/tgbaalgos/ltl2taa.cc | 7 +++--- src/tgbaalgos/ltl2tgba_fm.cc | 21 ++++++++--------- src/tgbaalgos/ltl2tgba_lacim.cc | 7 +++--- src/tgbaalgos/neverclaim.cc | 5 ++-- src/tgbaalgos/randomgraph.cc | 3 +-- src/tgbaparse/tgbaparse.yy | 5 ++-- src/tgbatest/complementation.cc | 11 ++++----- src/tgbatest/eltl2tgba.cc | 5 ++-- src/tgbatest/ltl2tgba.cc | 7 +++--- src/tgbatest/ltlprod.cc | 11 ++++----- src/tgbatest/mixprod.cc | 5 ++-- src/tgbatest/randtgba.cc | 15 ++++++------ src/tgbatest/reductgba.cc | 5 ++-- wrap/python/cgi/ltl2tgba.in | 6 ++--- wrap/python/tests/ltl2tgba.py | 4 ++-- wrap/python/tests/ltlparse.py | 6 ++--- wrap/python/tests/ltlsimple.py | 14 +++++------ 53 files changed, 260 insertions(+), 259 deletions(-) diff --git a/ChangeLog b/ChangeLog index 44f2a5496..429af0c8c 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,37 @@ +2009-11-08 Alexandre Duret-Lutz + + Deprecate ltl::destroy(f) in favor of f->destroy() + + * src/ltlast/formula.cc, src/ltlast/formula.hh (formula::clone): + Transform this static function into a member function. + * src/ltlvisit/destroy.hh (destroy): Document and declare as + deprecated. + * bench/split-product/cutscc.cc, iface/gspn/ltlgspn.cc, + src/eltlparse/eltlparse.yy, src/eltltest/acc.cc, + src/evtgbaalgos/tgba2evtgba.cc, src/evtgbatest/ltl2evtgba.cc, + src/ltlast/automatop.cc, src/ltlast/binop.cc, + src/ltlast/multop.cc, src/ltlast/unop.cc, src/ltlenv/declenv.cc, + src/ltlenv/declenv.hh, src/ltlparse/ltlparse.yy, + src/ltltest/equals.cc, src/ltltest/randltl.cc, + src/ltltest/readltl.cc, src/ltltest/reduc.cc, + src/ltltest/syntimpl.cc, src/ltltest/tostring.cc, + src/ltlvisit/destroy.cc src/ltlvisit/basicreduce.cc, + src/ltlvisit/contain.cc, src/ltlvisit/reduce.cc, + src/ltlvisit/syntimpl.cc, src/tgba/bdddict.cc, + src/tgba/bddprint.cc, src/tgba/taa.cc, + src/tgba/tgbabddconcretefactory.cc, src/tgba/tgbaexplicit.cc, + src/tgba/tgbafromfile.cc, src/tgbaalgos/eltl2tgba_lacim.cc, + src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2tgba_fm.cc, + src/tgbaalgos/ltl2tgba_lacim.cc, src/tgbaalgos/neverclaim.cc, + src/tgbaalgos/randomgraph.cc, src/tgbaparse/tgbaparse.yy, + src/tgbatest/complementation.cc, src/tgbatest/eltl2tgba.cc, + src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlprod.cc, + src/tgbatest/mixprod.cc, src/tgbatest/randtgba.cc, + src/tgbatest/reductgba.cc, wrap/python/cgi/ltl2tgba.in, + wrap/python/tests/ltl2tgba.py, wrap/python/tests/ltlparse.py, + wrap/python/tests/ltlsimple.py: Adjust destroy() usage, and remove + the #include "destroy.hh" when appropriate. + 2009-11-08 Alexandre Duret-Lutz Deprecate ltl::clone(f) in favor of f->clone(). diff --git a/bench/split-product/cutscc.cc b/bench/split-product/cutscc.cc index 46aef34c2..e8a04a658 100644 --- a/bench/split-product/cutscc.cc +++ b/bench/split-product/cutscc.cc @@ -25,7 +25,6 @@ #include "tgbaalgos/scc.hh" #include "tgba/tgbafromfile.hh" #include "tgbaalgos/dotty.hh" -#include "ltlvisit/destroy.hh" #include "tgbaalgos/randomgraph.hh" #include "tgbaalgos/emptiness.hh" #include "tgba/tgbaproduct.hh" diff --git a/iface/gspn/ltlgspn.cc b/iface/gspn/ltlgspn.cc index f8ff4cd1c..63de32c59 100644 --- a/iface/gspn/ltlgspn.cc +++ b/iface/gspn/ltlgspn.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004, 2006, 2007, 2008 Laboratoire +// Copyright (C) 2003, 2004, 2006, 2007, 2008, 2009 Laboratoire // d'Informatique de Paris 6 (LIP6), département Systèmes Répartis // Coopératifs (SRC), Université Pierre et Marie Curie. // @@ -29,7 +29,6 @@ #include "tgbaparse/public.hh" #endif #include "ltlparse/public.hh" -#include "ltlvisit/destroy.hh" #include "tgba/tgbatba.hh" #include "tgba/tgbaproduct.hh" #include "tgbaalgos/ltl2tgba_lacim.hh" @@ -265,7 +264,7 @@ main(int argc, char **argv) a_f = spot::ltl_to_tgba_lacim(f, dict); break; } - spot::ltl::destroy(f); + f->destroy(); #ifndef SSP spot::tgba* model = gspn.automaton(); diff --git a/src/eltlparse/eltlparse.yy b/src/eltlparse/eltlparse.yy index 6bf2ba1df..6e9781289 100644 --- a/src/eltlparse/eltlparse.yy +++ b/src/eltlparse/eltlparse.yy @@ -1,4 +1,4 @@ -/* Copyright (C) 2008 Laboratoire d'Informatique de +/* Copyright (C) 2008, 2009 Laboratoire d'Informatique de ** Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), ** Université Pierre et Marie Curie. ** @@ -37,8 +37,6 @@ #include "public.hh" #include "ltlast/allnodes.hh" #include "ltlast/formula_tree.hh" -#include "ltlvisit/destroy.hh" -#include "ltlvisit/clone.hh" namespace spot { @@ -234,7 +232,7 @@ using namespace spot::ltl; %type nfa_arg_list %destructor { delete $$; } "atomic proposition" -%destructor { spot::ltl::destroy($$); } subformula +%destructor { $$->destroy(); } subformula %printer { debug_stream() << *$$; } "atomic proposition" @@ -425,8 +423,8 @@ subformula: ATOMIC_PROP v.push_back($1); v.push_back($3); $$ = instanciate(i->second, v); - spot::ltl::destroy($1); - spot::ltl::destroy($3); + $1->destroy(); + $3->destroy(); } else { @@ -449,7 +447,7 @@ subformula: ATOMIC_PROP $$ = instanciate(i->second, *$3); automatop::vec::iterator it = $3->begin(); while (it != $3->end()) - spot::ltl::destroy(*it++); + (*it++)->destroy(); delete $3; } else @@ -463,7 +461,7 @@ subformula: ATOMIC_PROP { automatop::vec::iterator it = $3->begin(); while (it != $3->end()) - spot::ltl::destroy(*it++); + (*it++)->destroy(); delete $3; } diff --git a/src/eltltest/acc.cc b/src/eltltest/acc.cc index 029928ea2..68775aa6c 100644 --- a/src/eltltest/acc.cc +++ b/src/eltltest/acc.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. // @@ -22,7 +21,6 @@ #include #include #include "eltlparse/public.hh" -#include "ltlvisit/destroy.hh" #include "ltlvisit/lunabbrev.hh" #include "ltlvisit/nenoform.hh" @@ -38,20 +36,20 @@ main(int argc, char** argv) if (f != 0) { std::cout << f->dump() << std::endl; - spot::ltl::destroy(f); + f->destroy(); } return 1; } const spot::ltl::formula* f1 = spot::ltl::unabbreviate_logic(f); const spot::ltl::formula* f2 = spot::ltl::negative_normal_form(f1); - spot::ltl::destroy(f1); + f1->destroy(); assert(f != 0); std::cout << f->dump() << std::endl; - spot::ltl::destroy(f); + f->destroy(); assert(f2 != 0); std::cout << f2->dump() << std::endl; - spot::ltl::destroy(f2); + f2->destroy(); } diff --git a/src/evtgbaalgos/tgba2evtgba.cc b/src/evtgbaalgos/tgba2evtgba.cc index 65789a99c..5353a5df2 100644 --- a/src/evtgbaalgos/tgba2evtgba.cc +++ b/src/evtgbaalgos/tgba2evtgba.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004, 2009 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -24,7 +24,6 @@ #include "evtgba/explicit.hh" #include "tgbaalgos/reachiter.hh" #include "ltlvisit/tostring.hh" -#include "ltlvisit/destroy.hh" namespace spot { diff --git a/src/evtgbatest/ltl2evtgba.cc b/src/evtgbatest/ltl2evtgba.cc index 2777caf74..1a4161cb8 100644 --- a/src/evtgbatest/ltl2evtgba.cc +++ b/src/evtgbatest/ltl2evtgba.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2004, 2008 Laboratoire d'Informatique de Paris 6 +// Copyright (C) 2004, 2008, 2009 Laboratoire d'Informatique de Paris 6 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université // Pierre et Marie Curie. // @@ -23,7 +23,6 @@ #include #include #include -#include "ltlvisit/destroy.hh" #include "ltlast/allnodes.hh" #include "ltlparse/public.hh" #include "evtgbaparse/public.hh" @@ -114,7 +113,7 @@ main(int argc, char** argv) post_branching, fair_loop_approx, unobservables); - spot::ltl::destroy(f); + f->destroy(); spot::evtgba* e = spot::tgba_to_evtgba(a); if (dotty_opt) @@ -128,7 +127,7 @@ main(int argc, char** argv) for (spot::ltl::atomic_prop_set::iterator i = unobservables->begin(); i != unobservables->end(); ++i) - spot::ltl::destroy(*i); + (*i)->destroy(); delete unobservables; delete dict; diff --git a/src/ltlast/atomic_prop.cc b/src/ltlast/atomic_prop.cc index 29a91cfaa..9526f3806 100644 --- a/src/ltlast/atomic_prop.cc +++ b/src/ltlast/atomic_prop.cc @@ -1,6 +1,6 @@ -// 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. +// 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. // diff --git a/src/ltlast/automatop.cc b/src/ltlast/automatop.cc index fea815d30..56e902c98 100644 --- a/src/ltlast/automatop.cc +++ b/src/ltlast/automatop.cc @@ -50,7 +50,7 @@ namespace spot // Dereference children. for (unsigned n = 0; n < size(); ++n) - formula::destroy(nth(n)); + nth(n)->destroy(); delete children_; } @@ -79,7 +79,7 @@ namespace spot { // The instance already exists. for (vec::iterator vi = v->begin(); vi != v->end(); ++vi) - formula::destroy(*vi); + (*vi)->destroy(); delete v; return static_cast(i->second->clone()); } diff --git a/src/ltlast/binop.cc b/src/ltlast/binop.cc index 9018239a3..9615a36cd 100644 --- a/src/ltlast/binop.cc +++ b/src/ltlast/binop.cc @@ -48,8 +48,8 @@ namespace spot instances.erase(i); // Dereference children. - formula::destroy(first()); - formula::destroy(second()); + first()->destroy(); + second()->destroy(); } void @@ -143,8 +143,8 @@ namespace spot if (i != instances.end()) { // This instance already exists. - formula::destroy(first); - formula::destroy(second); + first->destroy(); + second->destroy(); return static_cast(i->second->clone()); } binop* ap = new binop(op, first, second); diff --git a/src/ltlast/formula.cc b/src/ltlast/formula.cc index 7cee80f7f..b42d7823a 100644 --- a/src/ltlast/formula.cc +++ b/src/ltlast/formula.cc @@ -38,10 +38,10 @@ namespace spot } void - formula::destroy(formula* f) + formula::destroy() const { - if (f->unref_()) - delete f; + if (const_cast(this)->unref_()) + delete this; } void diff --git a/src/ltlast/formula.hh b/src/ltlast/formula.hh index fb92a119a..c0743fa4d 100644 --- a/src/ltlast/formula.hh +++ b/src/ltlast/formula.hh @@ -85,7 +85,7 @@ namespace spot /// /// This decrements the reference counter of this node (if one is /// used) and can free the object. - static void destroy(formula* f); + void destroy() const; /// Return a canonic representation of the formula const std::string& dump() const; diff --git a/src/ltlast/multop.cc b/src/ltlast/multop.cc index 3b62d6ed2..9a10be5f3 100644 --- a/src/ltlast/multop.cc +++ b/src/ltlast/multop.cc @@ -55,7 +55,7 @@ namespace spot // Dereference children. for (unsigned n = 0; n < size(); ++n) - formula::destroy(nth(n)); + nth(n)->destroy(); delete children_; } @@ -131,7 +131,7 @@ namespace spot unsigned ps = p->size(); for (unsigned n = 0; n < ps; ++n) inlined.push_back(p->nth(n)->clone()); - formula::destroy(*i); + (*i)->destroy(); i = v->erase(i); } else @@ -153,7 +153,7 @@ namespace spot { if (*i == last) { - formula::destroy(*i); + (*i)->destroy(); i = v->erase(i); } else @@ -193,7 +193,7 @@ namespace spot { // The instance already exists. for (vec::iterator vi = v->begin(); vi != v->end(); ++vi) - formula::destroy(*vi); + (*vi)->destroy(); delete v; return static_cast(i->second->clone()); } diff --git a/src/ltlast/unop.cc b/src/ltlast/unop.cc index 63bed9cda..e731b9cba 100644 --- a/src/ltlast/unop.cc +++ b/src/ltlast/unop.cc @@ -46,7 +46,7 @@ namespace spot instances.erase(i); // Dereference child. - formula::destroy(child()); + child()->destroy(); } void @@ -110,7 +110,7 @@ namespace spot if (i != instances.end()) { // This instance already exists. - formula::destroy(child); + child->destroy(); return static_cast(i->second->clone()); } unop* ap = new unop(op, child); diff --git a/src/ltlenv/declenv.cc b/src/ltlenv/declenv.cc index 71c795166..003b146c7 100644 --- a/src/ltlenv/declenv.cc +++ b/src/ltlenv/declenv.cc @@ -33,7 +33,7 @@ namespace spot declarative_environment::~declarative_environment() { for (prop_map::iterator i = props_.begin(); i != props_.end(); ++i) - ltl::destroy(i->second); + i->second->destroy(); } bool diff --git a/src/ltlenv/declenv.hh b/src/ltlenv/declenv.hh index 27ff98e01..964dd39f4 100644 --- a/src/ltlenv/declenv.hh +++ b/src/ltlenv/declenv.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004, 2009 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -25,7 +25,6 @@ # include "environment.hh" # include # include -# include "ltlvisit/destroy.hh" # include "ltlast/atomic_prop.hh" namespace spot diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy index 08fcd3824..0a1a27301 100644 --- a/src/ltlparse/ltlparse.yy +++ b/src/ltlparse/ltlparse.yy @@ -31,7 +31,6 @@ #include #include "public.hh" #include "ltlast/allnodes.hh" -#include "ltlvisit/destroy.hh" } %parse-param {spot::ltl::parse_error_list &error_list} @@ -68,7 +67,7 @@ using namespace spot::ltl; #define missing_right_binop(res, left, op, str) \ do \ { \ - destroy(left); \ + left->destroy(); \ missing_right_op(res, op, str); \ } \ while (0); @@ -114,7 +113,7 @@ using namespace spot::ltl; proposition"), then the %destructor should refer to that name. References to ATOMIC_PROP are silently ignored. */ %destructor { delete $$; } "atomic proposition" -%destructor { spot::ltl::destroy($$); } subformula +%destructor { $$->destroy(); } subformula %printer { debug_stream() << *$$; } "atomic proposition" diff --git a/src/ltltest/equals.cc b/src/ltltest/equals.cc index 32cb4d5fd..665ee8704 100644 --- a/src/ltltest/equals.cc +++ b/src/ltltest/equals.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004, 2006, 2008 Laboratoire d'Informatique de +// Copyright (C) 2003, 2004, 2006, 2008, 2009 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. // @@ -28,7 +28,6 @@ #include "ltlvisit/tunabbrev.hh" #include "ltlvisit/dump.hh" #include "ltlvisit/nenoform.hh" -#include "ltlvisit/destroy.hh" #include "ltlvisit/contain.hh" #include "ltlast/allnodes.hh" #include "ltlvisit/reduce.hh" @@ -74,21 +73,21 @@ main(int argc, char** argv) #ifdef LUNABBREV tmp = f1; f1 = spot::ltl::unabbreviate_logic(f1); - spot::ltl::destroy(tmp); + tmp->destroy(); spot::ltl::dump(std::cout, f1); std::cout << std::endl; #endif #ifdef TUNABBREV tmp = f1; f1 = spot::ltl::unabbreviate_ltl(f1); - spot::ltl::destroy(tmp); + tmp->destroy(); spot::ltl::dump(std::cout, f1); std::cout << std::endl; #endif #ifdef NENOFORM tmp = f1; f1 = spot::ltl::negative_normal_form(f1); - spot::ltl::destroy(tmp); + tmp->destroy(); spot::ltl::dump(std::cout, f1); std::cout << std::endl; #endif @@ -96,28 +95,28 @@ main(int argc, char** argv) spot::ltl::formula* tmp; tmp = f1; f1 = spot::ltl::reduce(f1); - spot::ltl::destroy(tmp); + tmp->destroy(); spot::ltl::dump(std::cout, f1); #endif #ifdef REDUC_TAU spot::ltl::formula* tmp; tmp = f1; f1 = spot::ltl::reduce_tau03(f1, false); - spot::ltl::destroy(tmp); + tmp->destroy(); spot::ltl::dump(std::cout, f1); #endif #ifdef REDUC_TAUSTR spot::ltl::formula* tmp; tmp = f1; f1 = spot::ltl::reduce_tau03(f1, true); - spot::ltl::destroy(tmp); + tmp->destroy(); spot::ltl::dump(std::cout, f1); #endif int exit_code = f1 != f2; - spot::ltl::destroy(f1); - spot::ltl::destroy(f2); + f1->destroy(); + f2->destroy(); assert(spot::ltl::atomic_prop::instance_count() == 0); assert(spot::ltl::unop::instance_count() == 0); assert(spot::ltl::binop::instance_count() == 0); diff --git a/src/ltltest/randltl.cc b/src/ltltest/randltl.cc index dca13c368..0be2babf0 100644 --- a/src/ltltest/randltl.cc +++ b/src/ltltest/randltl.cc @@ -28,7 +28,6 @@ #include "ltlast/atomic_prop.hh" #include "ltlvisit/randomltl.hh" #include "ltlvisit/tostring.hh" -#include "ltlvisit/destroy.hh" #include "ltlvisit/length.hh" #include "ltlvisit/reduce.hh" #include "ltlenv/defaultenv.hh" @@ -179,10 +178,10 @@ main(int argc, char** argv) if (opt_r) { spot::ltl::formula* g = reduce(f); - spot::ltl::destroy(f); + f->destroy(); if (spot::ltl::length(g) < opt_r) { - spot::ltl::destroy(g); + g->destroy(); continue; } f = g; @@ -201,7 +200,7 @@ main(int argc, char** argv) exit(2); } std::string txt = spot::ltl::to_string(f); - spot::ltl::destroy(f); + f->destroy(); if (!opt_u || unique.insert(txt).second) { std::cout << txt << std::endl; @@ -223,7 +222,7 @@ main(int argc, char** argv) { spot::ltl::atomic_prop_set::const_iterator j = i; ++i; - spot::ltl::destroy(*j); + (*j)->destroy(); } delete ap; } diff --git a/src/ltltest/readltl.cc b/src/ltltest/readltl.cc index b4eebfa21..7930814bb 100644 --- a/src/ltltest/readltl.cc +++ b/src/ltltest/readltl.cc @@ -26,7 +26,6 @@ #include "ltlparse/public.hh" #include "ltlvisit/dump.hh" #include "ltlvisit/dotty.hh" -#include "ltlvisit/destroy.hh" #include "ltlast/allnodes.hh" void @@ -93,7 +92,7 @@ main(int argc, char** argv) spot::ltl::dump(std::cout, f); std::cout << std::endl; #endif - spot::ltl::destroy(f); + f->destroy(); if (debug_ref) dump_instances("after"); diff --git a/src/ltltest/reduc.cc b/src/ltltest/reduc.cc index 75ee28ab8..b0cd20da9 100644 --- a/src/ltltest/reduc.cc +++ b/src/ltltest/reduc.cc @@ -1,6 +1,6 @@ -// Copyright (C) 2004, 2006, 2007, 2008 Laboratoire d'Informatique de Paris -// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), -// Université Pierre et Marie Curie. +// Copyright (C) 2004, 2006, 2007, 2008, 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. // @@ -27,7 +27,6 @@ #include "ltlvisit/tunabbrev.hh" #include "ltlvisit/dump.hh" #include "ltlvisit/nenoform.hh" -#include "ltlvisit/destroy.hh" #include "ltlvisit/tostring.hh" #include "ltlvisit/reduce.hh" #include "ltlvisit/length.hh" @@ -135,8 +134,8 @@ main(int argc, char** argv) f1 = unabbreviate_logic(f1); ftmp2 = f1; f1 = negative_normal_form(f1); - spot::ltl::destroy(ftmp1); - spot::ltl::destroy(ftmp2); + ftmp1->destroy(); + ftmp2->destroy(); int length_f1_before = spot::ltl::length(f1); @@ -146,8 +145,8 @@ main(int argc, char** argv) f1 = spot::ltl::reduce(f1, o); ftmp2 = f1; f1 = spot::ltl::unabbreviate_logic(f1); - spot::ltl::destroy(ftmp1); - spot::ltl::destroy(ftmp2); + ftmp1->destroy(); + ftmp2->destroy(); int length_f1_after = spot::ltl::length(f1); std::string f1s_after = spot::ltl::to_string(f1); @@ -160,11 +159,11 @@ main(int argc, char** argv) f2 = unabbreviate_logic(f2); ftmp2 = f2; f2 = negative_normal_form(f2); - spot::ltl::destroy(ftmp1); - spot::ltl::destroy(ftmp2); + ftmp1->destroy(); + ftmp2->destroy(); ftmp1 = f2; f2 = unabbreviate_logic(f2); - spot::ltl::destroy(ftmp1); + ftmp1->destroy(); f2s = spot::ltl::to_string(f2); } @@ -204,9 +203,9 @@ main(int argc, char** argv) exit_code = 0; } - spot::ltl::destroy(f1); + f1->destroy(); if (f2) - spot::ltl::destroy(f2); + f2->destroy(); assert(spot::ltl::atomic_prop::instance_count() == 0); diff --git a/src/ltltest/syntimpl.cc b/src/ltltest/syntimpl.cc index 4e0dcf474..869dfac3a 100644 --- a/src/ltltest/syntimpl.cc +++ b/src/ltltest/syntimpl.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2004, 2008 Laboratoire d'Informatique de Paris 6 +// Copyright (C) 2004, 2008, 2009 Laboratoire d'Informatique de Paris 6 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université // Pierre et Marie Curie. // @@ -26,7 +26,6 @@ #include "ltlvisit/lunabbrev.hh" #include "ltlvisit/tunabbrev.hh" #include "ltlvisit/dump.hh" -#include "ltlvisit/destroy.hh" #include "ltlvisit/tostring.hh" #include "ltlvisit/syntimpl.hh" #include "ltlast/allnodes.hh" @@ -102,10 +101,10 @@ main(int argc, char** argv) spot::ltl::dump(std::cout, f1) << std::endl; spot::ltl::dump(std::cout, f2) << std::endl; - spot::ltl::destroy(f1); - spot::ltl::destroy(f2); - spot::ltl::destroy(ftmp1); - spot::ltl::destroy(ftmp2); + f1->destroy(); + f2->destroy(); + ftmp1->destroy(); + ftmp2->destroy(); assert(spot::ltl::atomic_prop::instance_count() == 0); assert(spot::ltl::unop::instance_count() == 0); assert(spot::ltl::binop::instance_count() == 0); diff --git a/src/ltltest/tostring.cc b/src/ltltest/tostring.cc index 43cf021d7..5e19eb11c 100644 --- a/src/ltltest/tostring.cc +++ b/src/ltltest/tostring.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), +// 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. // @@ -24,7 +24,6 @@ #include #include "ltlparse/public.hh" #include "ltlvisit/tostring.hh" -#include "ltlvisit/destroy.hh" #include "ltlast/allnodes.hh" void @@ -70,8 +69,8 @@ main(int argc, char **argv) if (f2s != f1s) return 1; - spot::ltl::destroy(f1); - spot::ltl::destroy(f2); + f1->destroy(); + f2->destroy(); assert(spot::ltl::atomic_prop::instance_count() == 0); assert(spot::ltl::unop::instance_count() == 0); assert(spot::ltl::binop::instance_count() == 0); diff --git a/src/ltlvisit/basicreduce.cc b/src/ltlvisit/basicreduce.cc index 5196d1c74..fa2c18e25 100644 --- a/src/ltlvisit/basicreduce.cc +++ b/src/ltlvisit/basicreduce.cc @@ -1,6 +1,6 @@ -// Copyright (C) 2004, 2007, 2008, 2009 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. +// Copyright (C) 2004, 2007, 2008, 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. // @@ -24,8 +24,6 @@ #include "ltlast/allnodes.hh" #include -#include "destroy.hh" - namespace spot { namespace ltl @@ -97,7 +95,7 @@ namespace spot resGF->push_back(mo->nth(i)->clone()); else res1->push_back(mo->nth(i)->clone()); - destroy(mo); + mo->destroy(); multop::vec* res3 = new multop::vec; if (!res1->empty()) res3->push_back(unop::instance(op, @@ -162,10 +160,10 @@ namespace spot unop::instance(unop::X, unop::instance(unop::F, basic_reduce(u->child()))); - destroy(u); + u->destroy(); // FXX(a) = XXF(a) ... result_ = basic_reduce(res); - destroy(res); + res->destroy(); return; } @@ -192,7 +190,7 @@ namespace spot { result_ = unop::instance(unop::G, basic_reduce(bo->second())); - destroy(bo); + bo->destroy(); return; } @@ -204,11 +202,11 @@ namespace spot unop::instance(unop::X, unop::instance(unop::G, basic_reduce(u->child()))); - destroy(u); + u->destroy(); // GXX(a) = XXG(a) ... // GXF(a) = XGF(a) = GF(a) ... result_ = basic_reduce(res); - destroy(res); + res->destroy(); return; } @@ -275,9 +273,9 @@ namespace spot basic_reduce(fu1->child()), basic_reduce(fu2->child())); result_ = unop::instance(unop::X, basic_reduce(ftmp)); - destroy(f1); - destroy(f2); - destroy(ftmp); + f1->destroy(); + f2->destroy(); + ftmp->destroy(); return; } @@ -362,7 +360,7 @@ namespace spot ->push_back(bo2->first()->clone()); if (j != i) { - destroy(*j); + (*j)->destroy(); *j = 0; } } @@ -393,7 +391,7 @@ namespace spot ->push_back(bo2->second()->clone()); if (j != i) { - destroy(*j); + (*j)->destroy(); *j = 0; } } @@ -414,7 +412,7 @@ namespace spot { tmpOther->push_back((*i)->clone()); } - destroy(*i); + (*i)->destroy(); } delete tmpGF; @@ -473,7 +471,7 @@ namespace spot ->push_back(bo2->second()->clone()); if (j != i) { - destroy(*j); + (*j)->destroy(); *j = 0; } } @@ -502,7 +500,7 @@ namespace spot ->push_back(bo2->first()->clone()); if (j != i) { - destroy(*j); + (*j)->destroy(); *j = 0; } } @@ -523,7 +521,7 @@ namespace spot { tmpOther->push_back((*i)->clone()); } - destroy(*i); + (*i)->destroy(); } break; diff --git a/src/ltlvisit/contain.cc b/src/ltlvisit/contain.cc index c0af7c3bd..faad5f937 100644 --- a/src/ltlvisit/contain.cc +++ b/src/ltlvisit/contain.cc @@ -20,7 +20,6 @@ // 02111-1307, USA. #include "contain.hh" -#include "destroy.hh" #include "tunabbrev.hh" #include "ltlast/unop.hh" #include "ltlast/binop.hh" @@ -51,7 +50,7 @@ namespace spot delete i->second.translation; const formula* f = i->first; translated_.erase(i); - destroy(f); + f->destroy(); } } @@ -89,7 +88,7 @@ namespace spot record_* rl = register_formula_(l); const formula* ng = unop::instance(unop::Not, g->clone()); record_* rng = register_formula_(ng); - destroy(ng); + ng->destroy(); return incompatible_(rl, rng); } @@ -102,8 +101,8 @@ namespace spot record_* rnl = register_formula_(nl); const formula* ng = unop::instance(unop::Not, g->clone()); record_* rng = register_formula_(ng); - destroy(nl); - destroy(ng); + nl->destroy(); + ng->destroy(); return incompatible_(rnl, rng); } @@ -181,19 +180,19 @@ namespace spot // if (a U b) => b, then keep b ! if (stronger && lcc->contained(bo, b)) { - destroy(a); + a->destroy(); result_ = b; } // if a => b, then a U b = b. else if ((!stronger) && lcc->contained(a, b)) { - destroy(a); + a->destroy(); result_ = b; } // if !a => b, then a U b = Fb else if (lcc->neg_contained(a, b)) { - destroy(a); + a->destroy(); result_ = unop::instance(unop::F, b); } else @@ -205,19 +204,19 @@ namespace spot // if (a R b) => b, then keep b ! if (stronger && lcc->contained(b, bo)) { - destroy(a); + a->destroy(); result_ = b; } // if b => a, then a R b = b. else if ((!stronger) && lcc->contained(b, a)) { - destroy(a); + a->destroy(); result_ = b; } // if a => !b, then a R b = Gb else if (lcc->contained_neg(a, b)) { - destroy(a); + a->destroy(); result_ = unop::instance(unop::G, b); } else @@ -266,7 +265,7 @@ namespace spot // if i => j, then i|j = j else if (lcc->contained((*res)[i], (*res)[j])) { - destroy((*res)[i]); + (*res)[i]->destroy(); (*res)[i] = 0; changed = true; break; @@ -274,7 +273,7 @@ namespace spot // if j => i, then i|j = i else if (lcc->contained((*res)[j], (*res)[i])) { - destroy((*res)[j]); + (*res)[j]->destroy(); (*res)[j] = 0; changed = true; } @@ -299,14 +298,14 @@ namespace spot // if i => j, then i&j = i else if (lcc->contained((*res)[i], (*res)[j])) { - destroy((*res)[j]); + (*res)[j]->destroy(); (*res)[j] = 0; changed = true; } // if j => i, then i&j = j else if (lcc->contained((*res)[j], (*res)[i])) { - destroy((*res)[i]); + (*res)[i]->destroy(); (*res)[i] = 0; changed = true; break; @@ -329,7 +328,7 @@ namespace spot constant_: for (unsigned i = 0; i < mos; ++i) if ((*res)[i]) - destroy((*res)[i]); + (*res)[i]->destroy(); delete res; } @@ -354,7 +353,7 @@ namespace spot // reduce_tau03_visitor does not handle Xor, Implies, and Equiv. f = unabbreviate_ltl(f); const_cast(f)->accept(v); - destroy(f); + f->destroy(); delete v.lcc; return v.result(); } diff --git a/src/ltlvisit/destroy.cc b/src/ltlvisit/destroy.cc index 9f61cd808..c3c2520e4 100644 --- a/src/ltlvisit/destroy.cc +++ b/src/ltlvisit/destroy.cc @@ -28,7 +28,7 @@ namespace spot void destroy(const formula* f) { - formula::destroy(const_cast(f)); + f->destroy(); } } } diff --git a/src/ltlvisit/destroy.hh b/src/ltlvisit/destroy.hh index 7b076fc01..b9ac61235 100644 --- a/src/ltlvisit/destroy.hh +++ b/src/ltlvisit/destroy.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// 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. // @@ -28,9 +28,17 @@ namespace spot { namespace ltl { +#if __GNUC__ /// \brief Destroys a formula /// \ingroup ltl_essential + /// \deprecated Use f->destroy() instead. + void destroy(const formula *f) __attribute__ ((deprecated)); +#else + /// \brief Destroys a formula + /// \ingroup ltl_essential + /// \deprecated Use f->destroy() instead. void destroy(const formula *f); +#endif } } diff --git a/src/ltlvisit/reduce.cc b/src/ltlvisit/reduce.cc index 197e3f0b9..31260f18a 100644 --- a/src/ltlvisit/reduce.cc +++ b/src/ltlvisit/reduce.cc @@ -28,7 +28,6 @@ #include "lunabbrev.hh" #include "simpfg.hh" #include "nenoform.hh" -#include "ltlvisit/destroy.hh" #include "contain.hh" namespace spot @@ -137,14 +136,14 @@ namespace spot if (syntactic_implication(f1, f2)) { result_ = f2; - destroy(f1); + f1->destroy(); return; } /* !b < a => a U b = Fb */ if (syntactic_implication_neg(f2, f1, false)) { result_ = unop::instance(unop::F, f2); - destroy(f1); + f1->destroy(); return; } /* a < b => a U (b U c) = (b U c) */ @@ -154,7 +153,7 @@ namespace spot && syntactic_implication(f1, bo->first())) { result_ = f2; - destroy(f1); + f1->destroy(); return; } } @@ -165,14 +164,14 @@ namespace spot if (syntactic_implication(f2, f1)) { result_ = f2; - destroy(f1); + f1->destroy(); return; } /* b < !a => a R b = Gb */ if (syntactic_implication_neg(f2, f1, true)) { result_ = unop::instance(unop::G, f2); - destroy(f1); + f1->destroy(); return; } /* b < a => a R (b R c) = b R c */ @@ -182,7 +181,7 @@ namespace spot && syntactic_implication(bo->first(), f1)) { result_ = f2; - destroy(f1); + f1->destroy(); return; } } @@ -230,7 +229,7 @@ namespace spot (mo->op() == multop::And))) { // We keep f2 - destroy(*f1); + (*f1)->destroy(); res->erase(f1); removed = true; break; @@ -241,7 +240,7 @@ namespace spot (mo->op() == multop::And))) { // We keep f1 - destroy(*f2); + (*f2)->destroy(); res->erase(f2); removed = true; break; @@ -261,7 +260,7 @@ namespace spot { for (multop::vec::iterator j = res->begin(); j != res->end(); j++) - destroy(*j); + (*j)->destroy(); res->clear(); delete res; if (mo->op() == multop::Or) @@ -309,7 +308,7 @@ namespace spot assert(n < 100); if (prev) { - destroy(prev); + prev->destroy(); prev = const_cast(f); } else @@ -318,15 +317,15 @@ namespace spot } f1 = unabbreviate_logic(f); f2 = simplify_f_g(f1); - destroy(f1); + f1->destroy(); f1 = negative_normal_form(f2); - destroy(f2); + f2->destroy(); f2 = f1; if (opt & Reduce_Basics) { f1 = basic_reduce(f2); - destroy(f2); + f2->destroy(); f2 = f1; } @@ -336,7 +335,7 @@ namespace spot reduce_visitor v(opt); f2->accept(v); f1 = v.result(); - destroy(f2); + f2->destroy(); f2 = f1; } @@ -347,12 +346,12 @@ namespace spot formula* f1 = reduce_tau03(f2, opt & Reduce_Containment_Checks_Stronger); - destroy(f2); + f2->destroy(); f2 = f1; } f = f2; } - destroy(prev); + prev->destroy(); return const_cast(f); } } diff --git a/src/ltlvisit/syntimpl.cc b/src/ltlvisit/syntimpl.cc index cc58b8c57..77caeec6f 100644 --- a/src/ltlvisit/syntimpl.cc +++ b/src/ltlvisit/syntimpl.cc @@ -26,7 +26,6 @@ #include "lunabbrev.hh" #include "simpfg.hh" #include "nenoform.hh" -#include "ltlvisit/destroy.hh" namespace spot { @@ -408,12 +407,12 @@ namespace spot if (special_case(tmp)) { result_ = true; - destroy(tmp); + tmp->destroy(); return; } if (syntactic_implication(tmp, f)) result_ = true; - destroy(tmp); + tmp->destroy(); return; } case unop::G: @@ -425,12 +424,12 @@ namespace spot if (special_case(tmp)) { result_ = true; - destroy(tmp); + tmp->destroy(); return; } if (syntactic_implication(tmp, f)) result_ = true; - destroy(tmp); + tmp->destroy(); return; } case unop::Finish: @@ -581,24 +580,24 @@ namespace spot l = unop::instance(unop::Not, l); formula* tmp = unabbreviate_logic(l); - destroy(l); + l->destroy(); l = simplify_f_g(tmp); - destroy(tmp); + tmp->destroy(); tmp = negative_normal_form(l); - destroy(l); + l->destroy(); l = tmp; tmp = unabbreviate_logic(r); - destroy(r); + r->destroy(); r = simplify_f_g(tmp); - destroy(tmp); + tmp->destroy(); tmp = negative_normal_form(r); - destroy(r); + r->destroy(); r = tmp; bool result = syntactic_implication(l, r); - destroy(l); - destroy(r); + l->destroy(); + r->destroy(); return result; } } diff --git a/src/tgba/bdddict.cc b/src/tgba/bdddict.cc index dbb195bd1..30f40b380 100644 --- a/src/tgba/bdddict.cc +++ b/src/tgba/bdddict.cc @@ -22,7 +22,6 @@ #include #include #include -#include #include #include #include @@ -156,7 +155,7 @@ namespace spot ltl::atomic_prop::instance(s.str(), ltl::default_environment::instance()); int res = register_acceptance_variable(f, for_me); - ltl::destroy(f); + f->destroy(); return res; } @@ -278,7 +277,7 @@ namespace spot // formula itself. release_variables(var, n); if (f) - ltl::destroy(f); + f->destroy(); var_refs.erase(cur); } diff --git a/src/tgba/bddprint.cc b/src/tgba/bddprint.cc index 4be59eb21..a96fd30d1 100644 --- a/src/tgba/bddprint.cc +++ b/src/tgba/bddprint.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// 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. // @@ -25,7 +25,6 @@ #include "bddprint.hh" #include "ltlvisit/tostring.hh" #include "formula2bdd.hh" -#include "ltlvisit/destroy.hh" namespace spot { @@ -202,7 +201,7 @@ namespace spot { const ltl::formula* f = bdd_to_formula(b, d); to_string(f, os); - destroy(f); + f->destroy(); return os; } diff --git a/src/tgba/taa.cc b/src/tgba/taa.cc index 6b52f4901..15207423d 100644 --- a/src/tgba/taa.cc +++ b/src/tgba/taa.cc @@ -23,7 +23,6 @@ #include #include #include -#include "ltlvisit/destroy.hh" #include "tgba/formula2bdd.hh" #include "misc/bddop.hh" #include "taa.hh" @@ -99,7 +98,7 @@ namespace spot taa::add_condition(transition* t, const ltl::formula* f) { t->condition &= formula_to_bdd(f, dict_, this); - ltl::destroy(f); + f->destroy(); } void @@ -125,7 +124,7 @@ namespace spot bdd_dict::fv_map::iterator i = dict_->acc_map.find(f); assert(i != dict_->acc_map.end()); - ltl::destroy(f); + f->destroy(); bdd v = bdd_ithvar(i->second); t->acceptance_conditions |= v & bdd_exist(neg_acceptance_conditions_, v); } diff --git a/src/tgba/tgbabddconcretefactory.cc b/src/tgba/tgbabddconcretefactory.cc index 40c2f4a66..879f60fc6 100644 --- a/src/tgba/tgbabddconcretefactory.cc +++ b/src/tgba/tgbabddconcretefactory.cc @@ -19,8 +19,8 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -#include "ltlvisit/destroy.hh" #include "tgbabddconcretefactory.hh" + namespace spot { tgba_bdd_concrete_factory::tgba_bdd_concrete_factory(bdd_dict* dict) @@ -32,7 +32,7 @@ namespace spot { acc_map_::iterator ai; for (ai = acc_.begin(); ai != acc_.end(); ++ai) - destroy(ai->first); + ai->first->destroy(); get_dict()->unregister_all_my_variables(this); } diff --git a/src/tgba/tgbaexplicit.cc b/src/tgba/tgbaexplicit.cc index ffbfc687b..291f4791b 100644 --- a/src/tgba/tgbaexplicit.cc +++ b/src/tgba/tgbaexplicit.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// 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. // @@ -21,7 +21,6 @@ #include "ltlast/atomic_prop.hh" #include "ltlast/constant.hh" -#include "ltlvisit/destroy.hh" #include "tgbaexplicit.hh" #include "tgba/formula2bdd.hh" #include "misc/bddop.hh" @@ -187,7 +186,7 @@ namespace spot tgba_explicit::add_condition(transition* t, const ltl::formula* f) { t->condition &= formula_to_bdd(f, dict_, this); - ltl::destroy(f); + f->destroy(); } void @@ -201,7 +200,7 @@ namespace spot tgba_explicit::declare_acceptance_condition(const ltl::formula* f) { int v = dict_->register_acceptance_variable(f, this); - ltl::destroy(f); + f->destroy(); bdd neg = bdd_nithvar(v); neg_acceptance_conditions_ &= neg; @@ -287,7 +286,7 @@ namespace spot /* If this second assert fails and the first doesn't, things are badly broken. This has already happened. */ assert(i != dict_->acc_map.end()); - ltl::destroy(f); + f->destroy(); bdd v = bdd_ithvar(i->second); v &= bdd_exist(neg_acceptance_conditions_, v); return v; diff --git a/src/tgba/tgbafromfile.cc b/src/tgba/tgbafromfile.cc index 1288c2f88..5895988f0 100644 --- a/src/tgba/tgbafromfile.cc +++ b/src/tgba/tgbafromfile.cc @@ -21,7 +21,6 @@ #include "tgba/public.hh" #include "tgbafromfile.hh" -#include "ltlvisit/destroy.hh" namespace spot { @@ -56,7 +55,7 @@ namespace spot { if (f_) { - ltl::destroy(f_); + f_->destroy(); f_ = 0; } std::string line = ""; @@ -94,4 +93,3 @@ namespace spot return formula_; } } - diff --git a/src/tgbaalgos/eltl2tgba_lacim.cc b/src/tgbaalgos/eltl2tgba_lacim.cc index 9f0590331..cfa5b4d0d 100644 --- a/src/tgbaalgos/eltl2tgba_lacim.cc +++ b/src/tgbaalgos/eltl2tgba_lacim.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2008 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2008, 2009 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -24,7 +24,6 @@ #include "ltlast/formula_tree.hh" #include "ltlvisit/lunabbrev.hh" #include "ltlvisit/nenoform.hh" -#include "ltlvisit/destroy.hh" #include "tgba/tgbabddconcretefactory.hh" #include @@ -240,7 +239,7 @@ namespace spot { const formula* lbl = formula_tree::instanciate((*i)->lbl, v); bdd f = recurse(lbl); - destroy(lbl); + lbl->destroy(); if (nfa->is_final((*i)->dst)) { tmp1 |= f; @@ -285,13 +284,13 @@ namespace spot // would involve negations at the BDD level. const ltl::formula* f1 = ltl::unabbreviate_logic(f); const ltl::formula* f2 = ltl::negative_normal_form(f1); - ltl::destroy(f1); + f1->destroy(); // Traverse the formula and draft the automaton in a factory. tgba_bdd_concrete_factory fact(dict); eltl_trad_visitor v(fact, true); f2->accept(v); - ltl::destroy(f2); + f2->destroy(); fact.finish(); // Finally setup the resulting automaton. diff --git a/src/tgbaalgos/ltl2taa.cc b/src/tgbaalgos/ltl2taa.cc index d1df651a4..4623688d2 100644 --- a/src/tgbaalgos/ltl2taa.cc +++ b/src/tgbaalgos/ltl2taa.cc @@ -25,7 +25,6 @@ #include "ltlvisit/lunabbrev.hh" #include "ltlvisit/tunabbrev.hh" #include "ltlvisit/nenoform.hh" -#include "ltlvisit/destroy.hh" #include "ltlvisit/tostring.hh" #include "ltlvisit/contain.hh" #include "ltl2taa.hh" @@ -56,7 +55,7 @@ namespace spot result() { for (unsigned i = 0; i < to_free_.size(); ++i) - destroy(to_free_[i]); + to_free_[i]->destroy(); res_->set_init_state(init_); return res_; } @@ -380,14 +379,14 @@ namespace spot // TODO: s/unabbreviate_ltl/unabbreviate_logic/ const ltl::formula* f1 = ltl::unabbreviate_ltl(f); const ltl::formula* f2 = ltl::negative_normal_form(f1); - ltl::destroy(f1); + f1->destroy(); spot::taa* res = new spot::taa(dict); language_containment_checker* lcc = new language_containment_checker(dict, false, false, false, false); ltl2taa_visitor v(res, lcc, refined_rules); f2->accept(v); - ltl::destroy(f2); + f2->destroy(); delete lcc; return v.result(); diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index abe98d908..26a06caca 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -27,7 +27,6 @@ #include "ltlast/allnodes.hh" #include "ltlvisit/lunabbrev.hh" #include "ltlvisit/nenoform.hh" -#include "ltlvisit/destroy.hh" #include "ltlvisit/tostring.hh" #include "ltlvisit/postfix.hh" #include "ltlvisit/apcollect.hh" @@ -66,7 +65,7 @@ namespace spot { fv_map::iterator i; for (i = next_map.begin(); i != next_map.end(); ++i) - destroy(i->first); + i->first->destroy(); dict->unregister_all_my_variables(this); } @@ -574,7 +573,7 @@ namespace spot formula_to_bdd_map::iterator i = f2b_.begin(); const formula* f = i->first; f2b_.erase(i); - destroy(f); + f->destroy(); } } @@ -626,7 +625,7 @@ namespace spot if (i->second != f) { // The translated bdd maps to an already seen formula. - destroy(f); + f->destroy(); f = i->second->clone(); } else if (new_variable && lcc_) @@ -640,7 +639,7 @@ namespace spot { f2b_[f] = j->second; i->second = j->first; - destroy(f); + f->destroy(); f = i->second->clone(); break; } @@ -687,7 +686,7 @@ namespace spot else { i->second[promises] |= conds; - destroy(dest); + dest->destroy(); } } @@ -706,13 +705,13 @@ namespace spot // would involve negations at the BDD level. formula* f1 = unabbreviate_logic(f); formula* f2 = negative_normal_form(f1); - destroy(f1); + f1->destroy(); // Simplify the formula, if requested. if (reduce_ltl) { formula* tmp = reduce(f2, reduce_ltl); - destroy(f2); + f2->destroy(); f2 = tmp; } @@ -864,7 +863,7 @@ namespace spot if (reduce_ltl) { formula* tmp = reduce(dest, reduce_ltl); - destroy(dest); + dest->destroy(); dest = tmp; // Ignore the arc if the destination reduces to false. if (dest == constant::false_instance()) @@ -982,7 +981,7 @@ namespace spot } else { - destroy(dest); + dest->destroy(); } } } @@ -990,7 +989,7 @@ namespace spot // Free all formulae. for (std::set::iterator i = formulae_seen.begin(); i != formulae_seen.end(); ++i) - destroy(*i); + (*i)->destroy(); // Turn all promises into real acceptance conditions. a->complement_all_acceptance_conditions(); diff --git a/src/tgbaalgos/ltl2tgba_lacim.cc b/src/tgbaalgos/ltl2tgba_lacim.cc index 4e00732b0..e21ae3ad9 100644 --- a/src/tgbaalgos/ltl2tgba_lacim.cc +++ b/src/tgbaalgos/ltl2tgba_lacim.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// 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. // @@ -23,7 +23,6 @@ #include "ltlast/allnodes.hh" #include "ltlvisit/lunabbrev.hh" #include "ltlvisit/nenoform.hh" -#include "ltlvisit/destroy.hh" #include "tgba/tgbabddconcretefactory.hh" #include @@ -271,13 +270,13 @@ namespace spot // would involve negations at the BDD level. const ltl::formula* f1 = ltl::unabbreviate_logic(f); const ltl::formula* f2 = ltl::negative_normal_form(f1); - ltl::destroy(f1); + f1->destroy(); // Traverse the formula and draft the automaton in a factory. tgba_bdd_concrete_factory fact(dict); ltl_trad_visitor v(fact, true); f2->accept(v); - ltl::destroy(f2); + f2->destroy(); fact.finish(); // Finally setup the resulting automaton. diff --git a/src/tgbaalgos/neverclaim.cc b/src/tgbaalgos/neverclaim.cc index ab2c30437..379341016 100644 --- a/src/tgbaalgos/neverclaim.cc +++ b/src/tgbaalgos/neverclaim.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004, 2009 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -28,7 +28,6 @@ #include "reachiter.hh" #include "ltlvisit/tostring.hh" #include "tgba/formula2bdd.hh" -#include "ltlvisit/destroy.hh" namespace spot { @@ -167,7 +166,7 @@ namespace spot const ltl::formula* f = bdd_to_formula(si->current_condition(), automata_->get_dict()); to_spin_string(f, os_); - destroy(f); + f->destroy(); state* current = si->current_state(); os_ << ") -> goto " << get_state_label(current, out) << std::endl; delete current; diff --git a/src/tgbaalgos/randomgraph.cc b/src/tgbaalgos/randomgraph.cc index f85e5e5b8..eeee47223 100644 --- a/src/tgbaalgos/randomgraph.cc +++ b/src/tgbaalgos/randomgraph.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2004, 2005, 2007, 2008 Laboratoire d'Informatique de +// Copyright (C) 2004, 2005, 2007, 2008, 2009 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. // @@ -23,7 +23,6 @@ #include "tgba/tgbaexplicit.hh" #include "misc/random.hh" #include "ltlast/atomic_prop.hh" -#include "ltlvisit/destroy.hh" #include #include #include diff --git a/src/tgbaparse/tgbaparse.yy b/src/tgbaparse/tgbaparse.yy index ad56e9d80..b2fdd6155 100644 --- a/src/tgbaparse/tgbaparse.yy +++ b/src/tgbaparse/tgbaparse.yy @@ -54,7 +54,6 @@ typedef std::map formula_cache; %code { #include "ltlast/constant.hh" -#include "ltlvisit/destroy.hh" /* Unfortunately Bison 2.3 uses the same guards in all parsers :( */ #undef BISON_POSITION_HH #undef BISON_LOCATION_HH @@ -87,7 +86,7 @@ typedef std::pair pair; %destructor { for (std::list::iterator i = $$->begin(); i != $$->end(); ++i) - spot::ltl::destroy(*i); + (*i)->destroy(); delete $$; } acc_list @@ -192,7 +191,7 @@ acc_list: { error_list.push_back(spot::tgba_parse_error(@2, "undeclared acceptance condition `" + *$2 + "'")); - destroy(f); + f->destroy(); // $2 will be destroyed on error recovery. YYERROR; } diff --git a/src/tgbatest/complementation.cc b/src/tgbatest/complementation.cc index e3b09aca0..74917d0c8 100644 --- a/src/tgbatest/complementation.cc +++ b/src/tgbatest/complementation.cc @@ -11,7 +11,6 @@ #include "ltlast/unop.hh" #include "tgbaalgos/stats.hh" #include "tgbaalgos/emptiness_stats.hh" -#include "ltlvisit/destroy.hh" #include "tgba/tgbatba.hh" #include "tgba/tgbasafracomplement.hh" @@ -146,7 +145,7 @@ int main(int argc, char* argv[]) complement = new spot::tgba_complement(a); spot::dotty_reachable(std::cout, complement); - spot::ltl::destroy(f1); + f1->destroy(); delete complement; delete a; } @@ -226,8 +225,8 @@ int main(int argc, char* argv[]) << std::endl; delete a2; - spot::ltl::destroy(f1); - spot::ltl::destroy(nf1); + f1->destroy(); + nf1->destroy(); } } else @@ -283,8 +282,8 @@ int main(int argc, char* argv[]) delete nAnf; delete Anf; - spot::ltl::destroy(nf1); - spot::ltl::destroy(f1); + nf1->destroy(); + f1->destroy(); } diff --git a/src/tgbatest/eltl2tgba.cc b/src/tgbatest/eltl2tgba.cc index 9a58a231e..22b4b0ccb 100644 --- a/src/tgbatest/eltl2tgba.cc +++ b/src/tgbatest/eltl2tgba.cc @@ -29,7 +29,6 @@ #include "tgbaalgos/dotty.hh" #include "tgbaalgos/lbtt.hh" #include "tgbaalgos/save.hh" -#include "ltlvisit/destroy.hh" #include "ltlvisit/tostring.hh" #include "ltlast/allnodes.hh" @@ -99,7 +98,7 @@ main(int argc, char** argv) input = ltl_defs(); input += "%"; input += spot::ltl::to_string(f, true); - spot::ltl::destroy(f); + f->destroy(); f = spot::eltl::parse_string(input, p, env, false); formula_index = 2; @@ -140,7 +139,7 @@ main(int argc, char** argv) } } - spot::ltl::destroy(f); + f->destroy(); delete concrete; assert(spot::ltl::atomic_prop::instance_count() == 0); diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index a78bcf793..a149ff646 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -25,7 +25,6 @@ #include #include #include -#include "ltlvisit/destroy.hh" #include "ltlvisit/contain.hh" #include "ltlvisit/tostring.hh" #include "ltlvisit/apcollect.hh" @@ -578,7 +577,7 @@ main(int argc, char** argv) if (redopt != spot::ltl::Reduce_None) { spot::ltl::formula* t = spot::ltl::reduce(f, redopt); - spot::ltl::destroy(f); + f->destroy(); f = t; if (display_reduce_form) std::cout << spot::ltl::to_string(f) << std::endl; @@ -902,7 +901,7 @@ main(int argc, char** argv) if (show_fc) delete a; if (f) - spot::ltl::destroy(f); + f->destroy(); delete product_degeneralized; delete product_to_free; delete system; @@ -922,7 +921,7 @@ main(int argc, char** argv) { for (spot::ltl::atomic_prop_set::iterator i = unobservables->begin(); i != unobservables->end(); ++i) - spot::ltl::destroy(*i); + (*i)->destroy(); delete unobservables; } diff --git a/src/tgbatest/ltlprod.cc b/src/tgbatest/ltlprod.cc index 2bc0e4a49..ceddb42f6 100644 --- a/src/tgbatest/ltlprod.cc +++ b/src/tgbatest/ltlprod.cc @@ -1,6 +1,6 @@ -// Copyright (C) 2003, 2004, 2008 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, 2008, 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,7 +22,6 @@ #include #include #include -#include "ltlvisit/destroy.hh" #include "ltlast/allnodes.hh" #include "ltlparse/public.hh" #include "tgbaalgos/ltl2tgba_lacim.hh" @@ -63,8 +62,8 @@ main(int argc, char** argv) { spot::tgba_bdd_concrete* a1 = spot::ltl_to_tgba_lacim(f1, dict); spot::tgba_bdd_concrete* a2 = spot::ltl_to_tgba_lacim(f2, dict); - spot::ltl::destroy(f1); - spot::ltl::destroy(f2); + f1->destroy(); + f2->destroy(); #ifdef BDD_CONCRETE_PRODUCT spot::tgba_bdd_concrete* p = spot::product(a1, a2); diff --git a/src/tgbatest/mixprod.cc b/src/tgbatest/mixprod.cc index dc246c2e2..c0abb2422 100644 --- a/src/tgbatest/mixprod.cc +++ b/src/tgbatest/mixprod.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004, 2008 Laboratoire d'Informatique de Paris +// Copyright (C) 2003, 2004, 2008, 2009 Laboratoire d'Informatique de Paris // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. // @@ -22,7 +22,6 @@ #include #include #include -#include "ltlvisit/destroy.hh" #include "ltlast/allnodes.hh" #include "ltlparse/public.hh" #include "tgbaalgos/ltl2tgba_lacim.hh" @@ -62,7 +61,7 @@ main(int argc, char** argv) { spot::tgba_bdd_concrete* a1 = spot::ltl_to_tgba_lacim(f1, dict); - spot::ltl::destroy(f1); + f1->destroy(); spot::tgba_product p(a1, a2); spot::tgba_save_reachable(std::cout, &p); delete a1; diff --git a/src/tgbatest/randtgba.cc b/src/tgbatest/randtgba.cc index 6080da701..91749a6ad 100644 --- a/src/tgbatest/randtgba.cc +++ b/src/tgbatest/randtgba.cc @@ -32,7 +32,6 @@ #include #include "ltlparse/public.hh" #include "ltlvisit/apcollect.hh" -#include "ltlvisit/destroy.hh" #include "ltlvisit/randomltl.hh" #include "ltlvisit/tostring.hh" #include "ltlvisit/length.hh" @@ -505,10 +504,10 @@ generate_formula(const spot::ltl::random_ltl& rl, int opt_f, int opt_s, if (opt_l) { spot::ltl::formula* g = reduce(f); - spot::ltl::destroy(f); + f->destroy(); if (spot::ltl::length(g) < opt_l) { - spot::ltl::destroy(g); + g->destroy(); continue; } f = g; @@ -531,7 +530,7 @@ generate_formula(const spot::ltl::random_ltl& rl, int opt_f, int opt_s, { return f; } - spot::ltl::destroy(f); + f->destroy(); } assert(opt_u); std::cerr << "Failed to generate another unique formula." @@ -853,7 +852,7 @@ main(int argc, char** argv) if (!f) exit(1); formula = spot::ltl_to_tgba_fm(f, dict, true); - spot::ltl::destroy(f); + f->destroy(); } else if (opt_i) { @@ -878,7 +877,7 @@ main(int argc, char** argv) i != tmp->end(); ++i) apf->insert(dynamic_cast ((*i)->clone())); - spot::ltl::destroy(f); + f->destroy(); delete tmp; } else @@ -1157,7 +1156,7 @@ main(int argc, char** argv) opt_ec = init_opt_ec; for (spot::ltl::atomic_prop_set::iterator i = apf->begin(); i != apf->end(); ++i) - spot::ltl::destroy(*i); + (*i)->destroy(); apf->clear(); } while (opt_F || opt_i); @@ -1304,7 +1303,7 @@ main(int argc, char** argv) for (spot::ltl::atomic_prop_set::iterator i = ap->begin(); i != ap->end(); ++i) - spot::ltl::destroy(*i); + (*i)->destroy(); if (opt_i && strcmp(opt_i, "-")) { diff --git a/src/tgbatest/reductgba.cc b/src/tgbatest/reductgba.cc index 26e92266f..9f6ffcf30 100644 --- a/src/tgbatest/reductgba.cc +++ b/src/tgbatest/reductgba.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004, 2006, 2008 Laboratoire d'Informatique de +// Copyright (C) 2003, 2004, 2006, 2008, 2009 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. // @@ -25,7 +25,6 @@ #include "tgbaalgos/reductgba_sim.hh" #include "tgba/tgbareduc.hh" -#include "ltlvisit/destroy.hh" #include "ltlvisit/reduce.hh" #include "ltlast/allnodes.hh" #include "ltlparse/public.hh" @@ -166,7 +165,7 @@ main(int argc, char** argv) delete automatareduc; #ifndef REDUCCMP if (f != 0) - spot::ltl::destroy(f); + f->destroy(); #endif assert(spot::ltl::atomic_prop::instance_count() == 0); diff --git a/wrap/python/cgi/ltl2tgba.in b/wrap/python/cgi/ltl2tgba.in index 8080369a3..15ee20ab5 100644 --- a/wrap/python/cgi/ltl2tgba.in +++ b/wrap/python/cgi/ltl2tgba.in @@ -1,6 +1,6 @@ #!@PYTHON@ # -*- mode: python; coding: iso-8859-1 -*- -# Copyright (C) 2003, 2004, 2006, 2007 Laboratoire d'Informatique de +# Copyright (C) 2003, 2004, 2006, 2007, 2009 Laboratoire d'Informatique de # Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), # Université Pierre et Marie Curie. # @@ -453,7 +453,7 @@ if reduce_eventuniv: opt = opt + spot.Reduce_Eventuality_And_Universality if opt != spot.Reduce_None: f2 = spot.reduce(f, opt) - spot.destroy(f) + f.destroy() f = f2 print "

Reduced formula is", f, "

" @@ -626,7 +626,7 @@ if draw_acc_run or print_acc_run: sys.stdout.flush() -spot.destroy(f) +f.destroy() # Make sure degen is cleared before automaton. del degen del automaton diff --git a/wrap/python/tests/ltl2tgba.py b/wrap/python/tests/ltl2tgba.py index 5f289aca6..5a1967ad0 100755 --- a/wrap/python/tests/ltl2tgba.py +++ b/wrap/python/tests/ltl2tgba.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: iso-8859-1 -*- -# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +# 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. # @@ -100,7 +100,7 @@ if f: concrete = 0 else: a = concrete = spot.ltl_to_tgba_lacim(f, dict) - spot.destroy(f) + f.destroy() del f degeneralized = None diff --git a/wrap/python/tests/ltlparse.py b/wrap/python/tests/ltlparse.py index 250f736d2..ba40531f3 100755 --- a/wrap/python/tests/ltlparse.py +++ b/wrap/python/tests/ltlparse.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: iso-8859-1 -*- -# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +# 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. # @@ -34,14 +34,14 @@ for str1 in l: if spot.format_parse_errors(spot.get_cout(), str1, p): sys.exit(1) str2 = str(f) - spot.destroy(f) + f.destroy() print str2 # Try to reparse the stringified formula f = spot.parse(str2, p, e) if spot.format_parse_errors(spot.get_cout(), str2, p): sys.exit(1) print f - spot.destroy(f) + f.destroy() assert spot.atomic_prop.instance_count() == 0 assert spot.binop.instance_count() == 0 diff --git a/wrap/python/tests/ltlsimple.py b/wrap/python/tests/ltlsimple.py index a282c2499..3ea90ba15 100755 --- a/wrap/python/tests/ltlsimple.py +++ b/wrap/python/tests/ltlsimple.py @@ -60,7 +60,7 @@ del op2, op3 assert spot.atomic_prop.instance_count() == 3 assert spot.multop.instance_count() == 1 -spot.destroy(op4) +op4.destroy() del op4 assert spot.atomic_prop.instance_count() == 0 @@ -83,11 +83,11 @@ assert spot.binop.instance_count() == 3 assert spot.unop.instance_count() == 1 assert spot.multop.instance_count() == 0 -spot.destroy(a) +a.destroy() del a -spot.destroy(b) +b.destroy() del b -spot.destroy(c) +c.destroy() del c assert spot.atomic_prop.instance_count() == 3 @@ -95,7 +95,7 @@ assert spot.binop.instance_count() == 3 assert spot.unop.instance_count() == 1 assert spot.multop.instance_count() == 0 -spot.destroy(f1) +f1.destroy() del f1 assert spot.atomic_prop.instance_count() == 2 @@ -103,7 +103,7 @@ assert spot.binop.instance_count() == 2 assert spot.unop.instance_count() == 1 assert spot.multop.instance_count() == 0 -spot.destroy(f4) +f4.destroy() del f4 assert spot.atomic_prop.instance_count() == 1 @@ -111,7 +111,7 @@ assert spot.binop.instance_count() == 1 assert spot.unop.instance_count() == 0 assert spot.multop.instance_count() == 0 -spot.destroy(f2) +f2.destroy() del f2 assert spot.atomic_prop.instance_count() == 0