From 8d947a87820a3b295b397b9872669c295ada7b77 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 25 Oct 2014 16:47:44 +0200 Subject: [PATCH] ltl: get rid of ltl::ref_formula Instead, manage all reference counting from ltl::formula. It ridance of virtual calls to clone() and destroy() easily compensate the extra test in destroy() to not delete constant nodes. * src/ltlast/refformula.cc, src/ltlast/refformula.hh: Delete. * src/ltlast/Makefile.am, wrap/python/spot.i: Adjust. * src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh, src/ltlast/binop.cc, src/ltlast/binop.hh, src/ltlast/bunop.cc, src/ltlast/bunop.hh, src/ltlast/formula.cc, src/ltlast/formula.hh, src/ltlast/multop.cc, src/ltlast/multop.hh, src/ltlast/unop.cc, src/ltlast/unop.hh: Ajust the reference counting code. --- src/ltlast/Makefile.am | 2 -- src/ltlast/atomic_prop.cc | 16 +++++++---- src/ltlast/atomic_prop.hh | 4 +-- src/ltlast/binop.cc | 12 ++++---- src/ltlast/binop.hh | 4 +-- src/ltlast/bunop.cc | 9 +++--- src/ltlast/bunop.hh | 4 +-- src/ltlast/formula.cc | 32 --------------------- src/ltlast/formula.hh | 50 +++++++++++++++++++------------- src/ltlast/multop.cc | 11 ++++--- src/ltlast/multop.hh | 4 +-- src/ltlast/refformula.cc | 60 --------------------------------------- src/ltlast/refformula.hh | 53 ---------------------------------- src/ltlast/unop.cc | 12 ++++---- src/ltlast/unop.hh | 5 ++-- wrap/python/spot.i | 2 -- 16 files changed, 70 insertions(+), 210 deletions(-) delete mode 100644 src/ltlast/refformula.cc delete mode 100644 src/ltlast/refformula.hh diff --git a/src/ltlast/Makefile.am b/src/ltlast/Makefile.am index 5ac7cace9..76586e592 100644 --- a/src/ltlast/Makefile.am +++ b/src/ltlast/Makefile.am @@ -35,7 +35,6 @@ ltlast_HEADERS = \ formula.hh \ multop.hh \ predecl.hh \ - refformula.hh \ unop.hh \ visitor.hh @@ -47,5 +46,4 @@ libltlast_la_SOURCES = \ constant.cc \ formula.cc \ multop.cc \ - refformula.cc \ unop.cc diff --git a/src/ltlast/atomic_prop.cc b/src/ltlast/atomic_prop.cc index c801591cf..8c8775bf4 100644 --- a/src/ltlast/atomic_prop.cc +++ b/src/ltlast/atomic_prop.cc @@ -33,7 +33,7 @@ namespace spot { atomic_prop::atomic_prop(const std::string& name, environment& env) - : ref_formula(AtomicProp), name_(name), env_(&env) + : formula(AtomicProp), name_(name), env_(&env) { is.boolean = true; is.sugar_free_boolean = true; @@ -93,10 +93,14 @@ namespace spot const atomic_prop* ap; auto ires = instances.emplace(key(name, &env), nullptr); if (!ires.second) - ap = ires.first->second; + { + ap = ires.first->second; + ap->clone(); + } else - ap = ires.first->second = new atomic_prop(name, env); - ap->clone(); + { + ap = ires.first->second = new atomic_prop(name, env); + } return ap; } @@ -110,9 +114,9 @@ namespace spot atomic_prop::dump_instances(std::ostream& os) { for (const auto& i: instances) - os << i.second << " = " << i.second->ref_count_() + os << i.second << " = " << 1 + i.second->refs_ << " * atomic_prop(" << i.first.first << ", " - << i.first.second->name() << ')' << std::endl; + << i.first.second->name() << ")\n"; return os; } diff --git a/src/ltlast/atomic_prop.hh b/src/ltlast/atomic_prop.hh index 10744f116..6262f2245 100644 --- a/src/ltlast/atomic_prop.hh +++ b/src/ltlast/atomic_prop.hh @@ -25,7 +25,7 @@ #ifndef SPOT_LTLAST_ATOMIC_PROP_HH # define SPOT_LTLAST_ATOMIC_PROP_HH -#include "refformula.hh" +#include "formula.hh" #include #include #include @@ -38,7 +38,7 @@ namespace spot /// \ingroup ltl_ast /// \brief Atomic propositions. - class SPOT_API atomic_prop : public ref_formula + class SPOT_API atomic_prop : public formula { public: /// Build an atomic proposition with name \a name in diff --git a/src/ltlast/binop.cc b/src/ltlast/binop.cc index 40f2003ec..3e6723172 100644 --- a/src/ltlast/binop.cc +++ b/src/ltlast/binop.cc @@ -36,7 +36,7 @@ namespace spot namespace ltl { binop::binop(type op, const formula* first, const formula* second) - : ref_formula(BinOp), op_(op), first_(first), second_(second) + : formula(BinOp), op_(op), first_(first), second_(second) { // Beware: (f U g) is a pure eventuality if both operands // are pure eventualities, unlike in the proceedings of @@ -503,20 +503,19 @@ namespace spot break; } - const binop* res; + const formula* res; auto ires = instances.emplace(key(op, first, second), nullptr); if (!ires.second) { // This instance already exists. first->destroy(); second->destroy(); - res = ires.first->second; + res = ires.first->second->clone(); } else { res = ires.first->second = new binop(op, first, second); } - res->clone(); return res; } @@ -531,9 +530,8 @@ namespace spot { for (const auto& i: instances) os << i.second << " = " - << i.second->ref_count_() << " * " - << i.second->dump() - << std::endl; + << 1 + i.second->refs_ << " * " + << i.second->dump() << '\n'; return os; } diff --git a/src/ltlast/binop.hh b/src/ltlast/binop.hh index a88c2dfdf..ccecef3ab 100644 --- a/src/ltlast/binop.hh +++ b/src/ltlast/binop.hh @@ -28,7 +28,7 @@ #ifndef SPOT_LTLAST_BINOP_HH # define SPOT_LTLAST_BINOP_HH -#include "refformula.hh" +#include "formula.hh" #include #include #include @@ -40,7 +40,7 @@ namespace spot /// \ingroup ltl_ast /// \brief Binary operator. - class SPOT_API binop : public ref_formula + class SPOT_API binop : public formula { public: /// Different kinds of binary opertaors diff --git a/src/ltlast/bunop.cc b/src/ltlast/bunop.cc index 399f1e02e..b5c385124 100644 --- a/src/ltlast/bunop.cc +++ b/src/ltlast/bunop.cc @@ -36,7 +36,7 @@ namespace spot const formula* bunop::one_star_ = 0; bunop::bunop(type op, const formula* child, unsigned min, unsigned max) - : ref_formula(BUnOp), op_(op), child_(child), min_(min), max_(max) + : formula(BUnOp), op_(op), child_(child), min_(min), max_(max) { props = child->get_props(); @@ -242,13 +242,12 @@ namespace spot { // This instance already exists. child->destroy(); - res = ires.first->second; + res = ires.first->second->clone(); } else { res = ires.first->second = new bunop(op, child, min, max); } - res->clone(); return res; } @@ -299,9 +298,9 @@ namespace spot { for (const auto& i: instances) os << i.second << " = " - << i.second->ref_count_() << " * " + << 1 + i.second->refs_ << " * " << i.second->dump() - << std::endl; + << '\n'; return os; } diff --git a/src/ltlast/bunop.hh b/src/ltlast/bunop.hh index 75cbb086b..d3b157c1b 100644 --- a/src/ltlast/bunop.hh +++ b/src/ltlast/bunop.hh @@ -22,7 +22,7 @@ #ifndef SPOT_LTLAST_BUNOP_HH # define SPOT_LTLAST_BUNOP_HH -#include "refformula.hh" +#include "formula.hh" #include #include #include @@ -35,7 +35,7 @@ namespace spot /// \ingroup ltl_ast /// \brief Bounded unary operator. - class SPOT_API bunop : public ref_formula + class SPOT_API bunop : public formula { public: enum type { Star }; diff --git a/src/ltlast/formula.cc b/src/ltlast/formula.cc index 80152afde..fbae5fe01 100644 --- a/src/ltlast/formula.cc +++ b/src/ltlast/formula.cc @@ -35,38 +35,6 @@ namespace spot { size_t formula::max_serial = 0; - const formula* - formula::clone() const - { - this->ref_(); - return this; - } - - formula::~formula() - { - } - - void - formula::destroy() const - { - if (this->unref_()) - delete this; - } - - void - formula::ref_() const - { - // Not reference counted by default. - } - - bool - formula::unref_() const - { - // Not reference counted by default. - return false; - } - - #define printprops \ proprint(is_boolean, "B", "Boolean formula"); \ proprint(is_sugar_free_boolean, "&", "without Boolean sugar"); \ diff --git a/src/ltlast/formula.hh b/src/ltlast/formula.hh index 9714078ae..359bfbf2a 100644 --- a/src/ltlast/formula.hh +++ b/src/ltlast/formula.hh @@ -97,14 +97,27 @@ namespace spot /// \brief clone this node /// - /// This increments the reference counter of this node (if one is - /// used). - const formula* clone() const; - /// \brief release this node - /// - /// This decrements the reference counter of this node (if one is - /// used) and can free the object. - void destroy() const; + /// This increments the reference counter of the node. + const formula* clone() const + { + ++refs_; + return this; + } + + /// \brief Release this node + void destroy() const + { + // Delete if this is the last node, and it is not a constant. + if (!refs_) + { + if (kind() != Constant) + delete this; + } + else + { + --refs_; + } + } /// Return a canonic representation of the formula virtual std::string dump() const = 0; @@ -293,17 +306,19 @@ namespace spot return serial_; } protected: - virtual ~formula(); - - /// \brief increment reference counter if any - virtual void ref_() const; - /// \brief decrement reference counter if any, return true when - /// the instance must be deleted (usually when the counter hits 0). - virtual bool unref_() const; + virtual ~formula() + { + } /// \brief The hash key of this formula. size_t serial_; + // The number of actual references is refs_ + 1. + mutable unsigned refs_ = 0; + /// \brief Number of formulae created so far. + static size_t max_serial; + opkind kind_; + struct ltl_prop { // All properties here should be expressed in such a a way @@ -346,11 +361,6 @@ namespace spot unsigned props; ltl_prop is; }; - - private: - /// \brief Number of formulae created so far. - static size_t max_serial; - opkind kind_; }; diff --git a/src/ltlast/multop.cc b/src/ltlast/multop.cc index 0f203895d..5284704c4 100644 --- a/src/ltlast/multop.cc +++ b/src/ltlast/multop.cc @@ -36,7 +36,7 @@ namespace spot namespace ltl { multop::multop(type op, vec* v) - : ref_formula(MultOp), op_(op), children_(v) + : formula(MultOp), op_(op), children_(v) { unsigned s = v->size(); assert(s > 1); @@ -592,7 +592,7 @@ namespace spot v->insert(v->begin(), constant::true_instance()); } - const multop* res; + const formula* res; // Insert the key with the dummy nullptr just // to check if p already exists. auto ires = instances.emplace(key(op, v), nullptr); @@ -602,14 +602,13 @@ namespace spot for (auto f: *v) f->destroy(); delete v; - res = ires.first->second; + res = ires.first->second->clone(); } else { // The instance did not already exist. res = ires.first->second = new multop(op, v); } - res->clone(); return res; } @@ -633,9 +632,9 @@ namespace spot { for (const auto& i: instances) os << i.second << " = " - << i.second->ref_count_() << " * " + << 1 + i.second->refs_ << " * " << i.second->dump() - << std::endl; + << '\n'; return os; } diff --git a/src/ltlast/multop.hh b/src/ltlast/multop.hh index ab2a8d3aa..f8772dc1c 100644 --- a/src/ltlast/multop.hh +++ b/src/ltlast/multop.hh @@ -25,7 +25,7 @@ #ifndef SPOT_LTLAST_MULTOP_HH # define SPOT_LTLAST_MULTOP_HH -#include "refformula.hh" +#include "formula.hh" #include #include #include @@ -37,7 +37,7 @@ namespace spot /// \ingroup ltl_ast /// \brief Multi-operand operators. - class SPOT_API multop : public ref_formula + class SPOT_API multop : public formula { public: enum type { Or, OrRat, And, AndRat, AndNLM, Concat, Fusion }; diff --git a/src/ltlast/refformula.cc b/src/ltlast/refformula.cc deleted file mode 100644 index b57438d3b..000000000 --- a/src/ltlast/refformula.cc +++ /dev/null @@ -1,60 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2010, 2012, 2013 Laboratoire de Recherche de -// Developpement de l'EPITA (LRDE). -// 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. -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 3 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - -#include "config.h" -#include "refformula.hh" -#include - -namespace spot -{ - namespace ltl - { - ref_formula::ref_formula(opkind k) - : formula(k), ref_counter_(0) - { - } - - ref_formula::~ref_formula() - { - } - - void - ref_formula::ref_() const - { - ++ref_counter_; - } - - bool - ref_formula::unref_() const - { - assert(ref_counter_ > 0); - return !--ref_counter_; - } - - unsigned - ref_formula::ref_count_() const - { - return ref_counter_; - } - - } -} diff --git a/src/ltlast/refformula.hh b/src/ltlast/refformula.hh deleted file mode 100644 index 3755d1ee5..000000000 --- a/src/ltlast/refformula.hh +++ /dev/null @@ -1,53 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2010, 2012, 2013 Laboratoire de Recherche de -// Développement de l'EPITA (LRDE). -// 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. -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 3 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - -/// \file ltlast/refformula.hh -/// \brief Reference-counted LTL formulae -#ifndef SPOT_LTLAST_REFFORMULA_HH -# define SPOT_LTLAST_REFFORMULA_HH - -#include "formula.hh" - -namespace spot -{ - namespace ltl - { - - /// \ingroup ltl_ast - /// \brief A reference-counted LTL formula. - class SPOT_API ref_formula : public formula - { - protected: - virtual ~ref_formula(); - ref_formula(opkind k); - void ref_() const; - bool unref_() const; - /// Number of references to this formula. - unsigned ref_count_() const; - private: - mutable unsigned ref_counter_; - }; - - } -} - -#endif // SPOT_LTLAST_REFFORMULA_HH diff --git a/src/ltlast/unop.cc b/src/ltlast/unop.cc index 0e9e21d1b..d96f989b3 100644 --- a/src/ltlast/unop.cc +++ b/src/ltlast/unop.cc @@ -28,13 +28,14 @@ #include #include "constant.hh" #include "atomic_prop.hh" +#include "bunop.hh" namespace spot { namespace ltl { unop::unop(type op, const formula* child) - : ref_formula(UnOp), op_(op), child_(child) + : formula(UnOp), op_(op), child_(child) { props = child->get_props(); switch (op) @@ -299,19 +300,18 @@ namespace spot break; } - const unop* res; + const formula* res; auto ires = instances.emplace(key(op, child), nullptr); if (!ires.second) { // This instance already exists. child->destroy(); - res = ires.first->second; + res = ires.first->second->clone(); } else { res = ires.first->second = new unop(op, child); } - res->clone(); return res; } @@ -326,9 +326,9 @@ namespace spot { for (const auto& i: instances) os << i.second << " = " - << i.second->ref_count_() << " * " + << 1 + i.second->refs_ << " * " << i.second->dump() - << std::endl; + << '\n'; return os; } diff --git a/src/ltlast/unop.hh b/src/ltlast/unop.hh index c24eb951c..6b56966d3 100644 --- a/src/ltlast/unop.hh +++ b/src/ltlast/unop.hh @@ -27,8 +27,7 @@ #include #include -#include "refformula.hh" -#include "bunop.hh" +#include "formula.hh" namespace spot { @@ -37,7 +36,7 @@ namespace spot /// \ingroup ltl_ast /// \brief Unary operators. - class SPOT_API unop : public ref_formula + class SPOT_API unop : public formula { public: enum type { diff --git a/wrap/python/spot.i b/wrap/python/spot.i index fb5277e1f..5e2e00310 100644 --- a/wrap/python/spot.i +++ b/wrap/python/spot.i @@ -79,7 +79,6 @@ namespace std { #include "misc/random.hh" #include "ltlast/formula.hh" -#include "ltlast/refformula.hh" #include "ltlast/atomic_prop.hh" #include "ltlast/binop.hh" #include "ltlast/constant.hh" @@ -198,7 +197,6 @@ using namespace spot; %include "misc/random.hh" %include "ltlast/formula.hh" -%include "ltlast/refformula.hh" %include "ltlast/atomic_prop.hh" %include "ltlast/binop.hh" %include "ltlast/constant.hh"