From 48fb19ea4478a3d4086f95a12138ba0f37882351 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 8 Nov 2009 19:41:40 +0100 Subject: [PATCH] Deprecate ltl::clone(f) in favor of f->clone(). * src/ltlvisit/clone.hh (clone): Document and declare as deprecated. * src/ltlast/formula_tree.cc, src/ltlvisit/basicreduce.cc, src/ltlvisit/clone.cc, src/ltlvisit/contain.cc, src/ltlvisit/lunabbrev.cc, src/ltlvisit/reduce.cc, src/ltlvisit/syntimpl.cc, src/tgba/bdddict.cc, src/tgba/formula2bdd.cc, src/tgba/tgbabddconcretefactory.cc, src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2tgba_fm.cc, src/tgbatest/complementation.cc, wrap/python/tests/ltlsimple.py: Adjust clone() usage, and remove the #include "clone.hh" when appropriate. --- ChangeLog | 15 +++++++++++ src/ltlast/formula_tree.cc | 3 +-- src/ltlvisit/basicreduce.cc | 43 +++++++++++++++--------------- src/ltlvisit/clone.cc | 2 +- src/ltlvisit/clone.hh | 12 +++++++-- src/ltlvisit/contain.cc | 9 +++---- src/ltlvisit/lunabbrev.cc | 9 +++---- src/ltlvisit/reduce.cc | 2 +- src/ltlvisit/syntimpl.cc | 10 +++---- src/tgba/bdddict.cc | 9 +++---- src/tgba/formula2bdd.cc | 9 +++---- src/tgba/tgbabddconcretefactory.cc | 5 ++-- src/tgbaalgos/ltl2taa.cc | 33 +++++++++++------------ src/tgbaalgos/ltl2tgba_fm.cc | 16 +++++------ src/tgbatest/complementation.cc | 5 ++-- wrap/python/tests/ltlsimple.py | 12 ++++----- 16 files changed, 103 insertions(+), 91 deletions(-) diff --git a/ChangeLog b/ChangeLog index e5d7390fe..44f2a5496 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,18 @@ +2009-11-08 Alexandre Duret-Lutz + + Deprecate ltl::clone(f) in favor of f->clone(). + + * src/ltlvisit/clone.hh (clone): Document and declare as deprecated. + * src/ltlast/formula_tree.cc, src/ltlvisit/basicreduce.cc, + src/ltlvisit/clone.cc, src/ltlvisit/contain.cc, + src/ltlvisit/lunabbrev.cc, src/ltlvisit/reduce.cc, + src/ltlvisit/syntimpl.cc, src/tgba/bdddict.cc, + src/tgba/formula2bdd.cc, src/tgba/tgbabddconcretefactory.cc, + src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2tgba_fm.cc, + src/tgbatest/complementation.cc, wrap/python/tests/ltlsimple.py: + Adjust clone() usage, and remove the #include "clone.hh" when + appropriate. + 2009-11-08 Alexandre Duret-Lutz Make it possible to clone const formulae. diff --git a/src/ltlast/formula_tree.cc b/src/ltlast/formula_tree.cc index ddd199ede..ed323f593 100644 --- a/src/ltlast/formula_tree.cc +++ b/src/ltlast/formula_tree.cc @@ -22,7 +22,6 @@ #include #include "formula_tree.hh" #include "allnodes.hh" -#include "ltlvisit/clone.hh" namespace spot { @@ -35,7 +34,7 @@ namespace spot { if (node_atomic* n = dynamic_cast(np.get())) return n->i == True ? constant::true_instance() : - n->i == False ? constant::false_instance() : clone(v.at(n->i)); + n->i == False ? constant::false_instance() : v.at(n->i)->clone(); if (node_unop* n = dynamic_cast(np.get())) return unop::instance(n->op, instanciate(n->child, v)); diff --git a/src/ltlvisit/basicreduce.cc b/src/ltlvisit/basicreduce.cc index 0eaea337b..5196d1c74 100644 --- a/src/ltlvisit/basicreduce.cc +++ b/src/ltlvisit/basicreduce.cc @@ -24,7 +24,6 @@ #include "ltlast/allnodes.hh" #include -#include "clone.hh" #include "destroy.hh" namespace spot @@ -95,9 +94,9 @@ namespace spot unsigned mos = mo->size(); for (unsigned i = 0; i < mos; ++i) if (is_GF(mo->nth(i))) - resGF->push_back(clone(mo->nth(i))); + resGF->push_back(mo->nth(i)->clone()); else - res1->push_back(clone(mo->nth(i))); + res1->push_back(mo->nth(i)->clone()); destroy(mo); multop::vec* res3 = new multop::vec; if (!res1->empty()) @@ -330,17 +329,17 @@ namespace spot if (uo && uo->op() == unop::X) { // Xa & Xb = X(a & b) - tmpX->push_back(clone(uo->child())); + tmpX->push_back(uo->child()->clone()); } else if (is_FG(*i)) { // FG(a) & FG(b) = FG(a & b) unop* uo2 = dynamic_cast(uo->child()); - tmpFG->push_back(clone(uo2->child())); + tmpFG->push_back(uo2->child()->clone()); } else { - tmpOther->push_back(clone(*i)); + tmpOther->push_back((*i)->clone()); } } else if (bo) @@ -360,7 +359,7 @@ namespace spot && ftmp == bo2->second()) { tmpUright - ->push_back(clone(bo2->first())); + ->push_back(bo2->first()->clone()); if (j != i) { destroy(*j); @@ -374,7 +373,7 @@ namespace spot instance(multop:: And, tmpUright), - clone(ftmp))); + ftmp->clone())); } else if (bo->op() == binop::R) { @@ -391,7 +390,7 @@ namespace spot && ftmp == bo2->first()) { tmpRright - ->push_back(clone(bo2->second())); + ->push_back(bo2->second()->clone()); if (j != i) { destroy(*j); @@ -401,19 +400,19 @@ namespace spot } tmpR ->push_back(binop::instance(binop::R, - clone(ftmp), + ftmp->clone(), multop:: instance(multop::And, tmpRright))); } else { - tmpOther->push_back(clone(*i)); + tmpOther->push_back((*i)->clone()); } } else { - tmpOther->push_back(clone(*i)); + tmpOther->push_back((*i)->clone()); } destroy(*i); } @@ -436,22 +435,22 @@ namespace spot if (uo && uo->op() == unop::X) { // Xa | Xb = X(a | b) - tmpX->push_back(clone(uo->child())); + tmpX->push_back(uo->child()->clone()); } else if (is_GF(*i)) { // GF(a) | GF(b) = GF(a | b) unop* uo2 = dynamic_cast(uo->child()); - tmpGF->push_back(clone(uo2->child())); + tmpGF->push_back(uo2->child()->clone()); } else if (is_FG(*i)) { // FG(a) | FG(b) = F(Ga | Gb) - tmpFG->push_back(clone(uo->child())); + tmpFG->push_back(uo->child()->clone()); } else { - tmpOther->push_back(clone(*i)); + tmpOther->push_back((*i)->clone()); } } else if (bo) @@ -471,7 +470,7 @@ namespace spot && ftmp == bo2->first()) { tmpUright - ->push_back(clone(bo2->second())); + ->push_back(bo2->second()->clone()); if (j != i) { destroy(*j); @@ -480,7 +479,7 @@ namespace spot } } tmpU->push_back(binop::instance(binop::U, - clone(ftmp), + ftmp->clone(), multop:: instance(multop::Or, tmpUright))); @@ -500,7 +499,7 @@ namespace spot && ftmp == bo2->second()) { tmpRright - ->push_back(clone(bo2->first())); + ->push_back(bo2->first()->clone()); if (j != i) { destroy(*j); @@ -513,16 +512,16 @@ namespace spot multop:: instance(multop::Or, tmpRright), - clone(ftmp))); + ftmp->clone())); } else { - tmpOther->push_back(clone(*i)); + tmpOther->push_back((*i)->clone()); } } else { - tmpOther->push_back(clone(*i)); + tmpOther->push_back((*i)->clone()); } destroy(*i); } diff --git a/src/ltlvisit/clone.cc b/src/ltlvisit/clone.cc index 8c6339662..0c9ba7065 100644 --- a/src/ltlvisit/clone.cc +++ b/src/ltlvisit/clone.cc @@ -87,7 +87,7 @@ namespace spot formula* clone_visitor::recurse(formula* f) { - return clone(f); + return f->clone(); } formula* diff --git a/src/ltlvisit/clone.hh b/src/ltlvisit/clone.hh index 43cf4597b..b00e1c639 100644 --- a/src/ltlvisit/clone.hh +++ b/src/ltlvisit/clone.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. // @@ -35,7 +35,7 @@ namespace spot /// This visitor is public, because it's convenient /// to derive from it and override part of its methods. /// But if you just want the functionality, consider using - /// spot::ltl::clone instead. + /// spot::ltl::formula::clone instead, it is way faster. class clone_visitor : public visitor { public: @@ -57,9 +57,17 @@ namespace spot formula* result_; }; +#if __GNUC__ /// \brief Clone a formula. /// \ingroup ltl_essential + /// \deprecated Use f->clone() instead. + formula* clone(const formula* f) __attribute__ ((deprecated)); +#else + /// \brief Clone a formula. + /// \ingroup ltl_essential + /// \deprecated Use f->clone() instead. formula* clone(const formula* f); +#endif } } diff --git a/src/ltlvisit/contain.cc b/src/ltlvisit/contain.cc index 3b30008af..c0af7c3bd 100644 --- a/src/ltlvisit/contain.cc +++ b/src/ltlvisit/contain.cc @@ -21,7 +21,6 @@ #include "contain.hh" #include "destroy.hh" -#include "clone.hh" #include "tunabbrev.hh" #include "ltlast/unop.hh" #include "ltlast/binop.hh" @@ -88,7 +87,7 @@ namespace spot language_containment_checker::contained(const formula* l, const formula* g) { record_* rl = register_formula_(l); - const formula* ng = unop::instance(unop::Not, clone(g)); + const formula* ng = unop::instance(unop::Not, g->clone()); record_* rng = register_formula_(ng); destroy(ng); return incompatible_(rl, rng); @@ -99,9 +98,9 @@ namespace spot language_containment_checker::neg_contained(const formula* l, const formula* g) { - const formula* nl = unop::instance(unop::Not, clone(l)); + const formula* nl = unop::instance(unop::Not, l->clone()); record_* rnl = register_formula_(nl); - const formula* ng = unop::instance(unop::Not, clone(g)); + const formula* ng = unop::instance(unop::Not, g->clone()); record_* rng = register_formula_(ng); destroy(nl); destroy(ng); @@ -135,7 +134,7 @@ namespace spot const tgba_explicit* e = ltl_to_tgba_fm(f, dict_, exprop_, symb_merge_, branching_postponement_, fair_loop_approx_); - record_& r = translated_[clone(f)]; + record_& r = translated_[f->clone()]; r.translation = e; return &r; } diff --git a/src/ltlvisit/lunabbrev.cc b/src/ltlvisit/lunabbrev.cc index 7c006a1e5..56849a263 100644 --- a/src/ltlvisit/lunabbrev.cc +++ b/src/ltlvisit/lunabbrev.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. // @@ -20,7 +20,6 @@ // 02111-1307, USA. #include "ltlast/allnodes.hh" -#include "ltlvisit/clone.hh" #include "lunabbrev.hh" #include @@ -48,10 +47,10 @@ namespace spot /* f1 ^ f2 == (f1 & !f2) | (f2 & !f1) */ case binop::Xor: result_ = multop::instance(multop::Or, - multop::instance(multop::And, clone(f1), + multop::instance(multop::And, f1->clone(), unop::instance(unop::Not, f2)), - multop::instance(multop::And, clone(f2), + multop::instance(multop::And, f2->clone(), unop::instance(unop::Not, f1))); return; @@ -64,7 +63,7 @@ namespace spot case binop::Equiv: result_ = multop::instance(multop::Or, multop::instance(multop::And, - clone(f1), clone(f2)), + f1->clone(), f2->clone()), multop::instance(multop::And, unop::instance(unop::Not, f1), diff --git a/src/ltlvisit/reduce.cc b/src/ltlvisit/reduce.cc index ad364059c..197e3f0b9 100644 --- a/src/ltlvisit/reduce.cc +++ b/src/ltlvisit/reduce.cc @@ -314,7 +314,7 @@ namespace spot } else { - prev = clone(f); + prev = f->clone(); } f1 = unabbreviate_logic(f); f2 = simplify_f_g(f1); diff --git a/src/ltlvisit/syntimpl.cc b/src/ltlvisit/syntimpl.cc index 7fc7bdf7f..cc58b8c57 100644 --- a/src/ltlvisit/syntimpl.cc +++ b/src/ltlvisit/syntimpl.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004, 2005, 2009 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -404,7 +404,7 @@ namespace spot /* F(a) = true U a */ const formula* tmp = binop::instance(binop::U, constant::true_instance(), - clone(f1)); + f1->clone()); if (special_case(tmp)) { result_ = true; @@ -421,7 +421,7 @@ namespace spot /* G(a) = false R a */ const formula* tmp = binop::instance(binop::R, constant::false_instance(), - clone(f1)); + f1->clone()); if (special_case(tmp)) { result_ = true; @@ -573,8 +573,8 @@ namespace spot bool syntactic_implication_neg(const formula* f1, const formula* f2, bool right) { - formula* l = clone(f1); - formula* r = clone(f2); + formula* l = f1->clone(); + formula* r = f2->clone(); if (right) r = unop::instance(unop::Not, r); else diff --git a/src/tgba/bdddict.cc b/src/tgba/bdddict.cc index e4ff5a61b..dbb195bd1 100644 --- a/src/tgba/bdddict.cc +++ b/src/tgba/bdddict.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de +// Copyright (C) 2003, 2004, 2005, 2006, 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 #include #include #include @@ -59,7 +58,7 @@ namespace spot } else { - f = clone(f); + f = f->clone(); num = allocate_variables(1); var_map[f] = num; var_formula_map[num] = f; @@ -94,7 +93,7 @@ namespace spot } else { - f = ltl::clone(f); + f = f->clone(); num = allocate_variables(2); now_map[f] = num; now_formula_map[num] = f; @@ -120,7 +119,7 @@ namespace spot } else { - f = clone(f); + f = f->clone(); num = allocate_variables(1); acc_map[f] = num; acc_formula_map[num] = f; diff --git a/src/tgba/formula2bdd.cc b/src/tgba/formula2bdd.cc index c4e70d237..c6464a9d6 100644 --- a/src/tgba/formula2bdd.cc +++ b/src/tgba/formula2bdd.cc @@ -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. // @@ -24,7 +24,6 @@ #include "ltlast/allnodes.hh" #include "ltlast/visitor.hh" #include "misc/minato.hh" -#include "ltlvisit/clone.hh" namespace spot { @@ -171,7 +170,7 @@ namespace spot int var = bdd_var(b); bdd_dict::vf_map::const_iterator isi = d->var_formula_map.find(var); assert(isi != d->var_formula_map.end()); - formula* res = clone(isi->second); + formula* res = isi->second->clone(); bdd high = bdd_high(b); if (high == bddfalse) diff --git a/src/tgba/tgbabddconcretefactory.cc b/src/tgba/tgbabddconcretefactory.cc index 8188cdf4b..40c2f4a66 100644 --- a/src/tgba/tgbabddconcretefactory.cc +++ b/src/tgba/tgbabddconcretefactory.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2009 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -19,7 +19,6 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -#include "ltlvisit/clone.hh" #include "ltlvisit/destroy.hh" #include "tgbabddconcretefactory.hh" namespace spot @@ -79,7 +78,7 @@ namespace spot acc_map_::iterator ai = acc_.find(a); if (ai == acc_.end()) { - a = clone(a); + a = a->clone(); acc_[a] = b; } else diff --git a/src/tgbaalgos/ltl2taa.cc b/src/tgbaalgos/ltl2taa.cc index 65951a69f..d1df651a4 100644 --- a/src/tgbaalgos/ltl2taa.cc +++ b/src/tgbaalgos/ltl2taa.cc @@ -27,7 +27,6 @@ #include "ltlvisit/nenoform.hh" #include "ltlvisit/destroy.hh" #include "ltlvisit/tostring.hh" -#include "ltlvisit/clone.hh" #include "ltlvisit/contain.hh" #include "ltl2taa.hh" @@ -68,7 +67,7 @@ namespace spot const formula* f = node; // Handle negation if (negated_) { - f = unop::instance(unop::Not, clone(node)); + f = unop::instance(unop::Not, node->clone()); to_free_.push_back(f); } init_ = to_string(f); @@ -76,7 +75,7 @@ namespace spot dst.push_back(std::string("sink")); taa::transition* t = res_->create_transition(init_, dst); - res_->add_condition(t, clone(f)); + res_->add_condition(t, f->clone()); succ_state ss = { dst, f, constant::true_instance() }; succ_.push_back(ss); } @@ -165,14 +164,14 @@ namespace spot i1->Q.push_back(init_); // Add the initial state i1->acc = node; t = res_->create_transition(init_, i1->Q); - res_->add_condition(t, clone(i1->condition)); - res_->add_acceptance_condition(t, clone(node)); + res_->add_condition(t, i1->condition->clone()); + res_->add_acceptance_condition(t, node->clone()); succ_.push_back(*i1); } for (i2 = v2.succ_.begin(); i2 != v2.succ_.end(); ++i2) { t = res_->create_transition(init_, i2->Q); - res_->add_condition(t, clone(i2->condition)); + res_->add_condition(t, i2->condition->clone()); succ_.push_back(*i2); } return; @@ -185,16 +184,16 @@ namespace spot { std::vector u; // Union std::copy(i1->Q.begin(), i1->Q.end(), ii(u, u.begin())); - formula* f = clone(i1->condition); // Refined rule + formula* f = i1->condition->clone(); // Refined rule if (!refined_ || !contained) { std::copy(i2->Q.begin(), i2->Q.end(), ii(u, u.begin())); - f = multop::instance(multop::And, f, clone(i2->condition)); + f = multop::instance(multop::And, f, i2->condition->clone()); } to_free_.push_back(f); t = res_->create_transition(init_, u); - res_->add_condition(t, clone(f)); + res_->add_condition(t, f->clone()); succ_state ss = { u, f, constant::true_instance() }; succ_.push_back(ss); } @@ -205,9 +204,9 @@ namespace spot i2->Q.push_back(init_); // Add the initial state t = res_->create_transition(init_, i2->Q); - res_->add_condition(t, clone(i2->condition)); + res_->add_condition(t, i2->condition->clone()); if (refined_ && i2->acc != constant::true_instance()) - res_->add_acceptance_condition(t, clone(i2->acc)); + res_->add_acceptance_condition(t, i2->acc->clone()); succ_.push_back(*i2); } return; @@ -262,15 +261,15 @@ namespace spot Q.push_back(p[n].Q[m]); Q.push_back(init_); t = res_->create_transition(init_, Q); - res_->add_condition(t, clone(p[n].condition)); + res_->add_condition(t, p[n].condition->clone()); if (p[n].acc != constant::true_instance()) - res_->add_acceptance_condition(t, clone(p[n].acc)); + res_->add_acceptance_condition(t, p[n].acc->clone()); succ_.push_back(p[n]); return; } } t = res_->create_transition(init_, p[n].Q); - res_->add_condition(t, clone(p[n].condition)); + res_->add_condition(t, p[n].condition->clone()); succ_.push_back(p[n]); } return; @@ -280,7 +279,7 @@ namespace spot for (i = vs[n].succ_.begin(); i != vs[n].succ_.end(); ++i) { t = res_->create_transition(init_, i->Q); - res_->add_condition(t, clone(i->condition)); + res_->add_condition(t, i->condition->clone()); succ_.push_back(*i); } return; @@ -349,8 +348,8 @@ namespace spot continue; const succ_state& ss(vs[i].succ_[pos[i] - 1]); std::copy(ss.Q.begin(), ss.Q.end(), ii(u, u.begin())); - f = multop::instance(multop::And, clone(ss.condition), f); - a = multop::instance(multop::And, clone(ss.acc), a); + f = multop::instance(multop::And, ss.condition->clone(), f); + a = multop::instance(multop::And, ss.acc->clone(), a); } to_free_.push_back(f); to_free_.push_back(a); diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index e23632819..abe98d908 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -110,7 +110,7 @@ namespace spot } else { - f = clone(f); + f = f->clone(); num = dict->register_anonymous_variables(1, this); next_map[f] = num; next_formula_map[num] = f; @@ -139,13 +139,13 @@ namespace spot { vf_map::const_iterator isi = next_formula_map.find(var); if (isi != next_formula_map.end()) - return clone(isi->second); + return isi->second->clone(); isi = dict->acc_formula_map.find(var); if (isi != dict->acc_formula_map.end()) - return clone(isi->second); + return isi->second->clone(); isi = dict->var_formula_map.find(var); if (isi != dict->var_formula_map.end()) - return clone(isi->second); + return isi->second->clone(); assert(0); // Never reached, but some GCC versions complain about // a missing return otherwise. @@ -213,7 +213,7 @@ namespace spot formula* ac = var_to_formula(var); if (!a->has_acceptance_condition(ac)) - a->declare_acceptance_condition(clone(ac)); + a->declare_acceptance_condition(ac->clone()); a->add_acceptance_condition(t, ac); b = high; } @@ -604,7 +604,7 @@ namespace spot res &= all_promises_; } - f2b_[clone(f)] = res; + f2b_[f->clone()] = res; // Register the reverse mapping if it is not already done. if (b2f_.find(res) == b2f_.end()) @@ -627,7 +627,7 @@ namespace spot { // The translated bdd maps to an already seen formula. destroy(f); - f = clone(i->second); + f = i->second->clone(); } else if (new_variable && lcc_) { @@ -641,7 +641,7 @@ namespace spot f2b_[f] = j->second; i->second = j->first; destroy(f); - f = clone(i->second); + f = i->second->clone(); break; } } diff --git a/src/tgbatest/complementation.cc b/src/tgbatest/complementation.cc index ce227af42..e3b09aca0 100644 --- a/src/tgbatest/complementation.cc +++ b/src/tgbatest/complementation.cc @@ -12,7 +12,6 @@ #include "tgbaalgos/stats.hh" #include "tgbaalgos/emptiness_stats.hh" #include "ltlvisit/destroy.hh" -#include "ltlvisit/clone.hh" #include "tgba/tgbatba.hh" #include "tgba/tgbasafracomplement.hh" @@ -217,7 +216,7 @@ int main(int argc, char* argv[]) { spot::ltl::formula* nf1 = spot::ltl::unop::instance(spot::ltl::unop::Not, - spot::ltl::clone(f1)); + f1->clone()); spot::tgba* a2 = spot::ltl_to_tgba_fm(nf1, dict); spot::tgba_statistics a_size = spot::stats_reachable(a2); std::cout << "Not Formula: " @@ -241,7 +240,7 @@ int main(int argc, char* argv[]) spot::tgba* Af = spot::ltl_to_tgba_fm(f1, dict); spot::ltl::formula* nf1 = spot::ltl::unop::instance(spot::ltl::unop::Not, - spot::ltl::clone(f1)); + f1->clone()); spot::tgba* Anf = spot::ltl_to_tgba_fm(nf1, dict); spot::tgba* nAf; diff --git a/wrap/python/tests/ltlsimple.py b/wrap/python/tests/ltlsimple.py index 5a3734da8..a282c2499 100755 --- a/wrap/python/tests/ltlsimple.py +++ b/wrap/python/tests/ltlsimple.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. # @@ -23,8 +23,6 @@ import ltihooks import spot -clone = spot.clone - e = spot.default_environment.instance() #---------------------------------------------------------------------- @@ -36,7 +34,7 @@ c2 = e.require('c') assert c == c2 assert spot.atomic_prop.instance_count() == 3 -op = spot.multop.instance(spot.multop.And, clone(a), clone(b)) +op = spot.multop.instance(spot.multop.And, a.clone(), b.clone()) op2 = spot.multop.instance(spot.multop.And, op, c) # The symbol for a subformula which hasn't been cloned is better @@ -75,9 +73,9 @@ c = e.require('c') T = spot.constant.true_instance() F = spot.constant.false_instance() -f1 = spot.binop.instance(spot.binop.Equiv, T, clone(a)) -f2 = spot.binop.instance(spot.binop.Implies, F, clone(b)) -f3 = spot.binop.instance(spot.binop.Xor, F, clone(c)) +f1 = spot.binop.instance(spot.binop.Equiv, T, a.clone()) +f2 = spot.binop.instance(spot.binop.Implies, F, b.clone()) +f3 = spot.binop.instance(spot.binop.Xor, F, c.clone()) f4 = spot.unop.instance(spot.unop.Not, f3); del f3 assert spot.atomic_prop.instance_count() == 3