From f2be64dd2c0241280e4a4b6edfbb8069984e7140 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 13 Nov 2009 18:13:59 +0100 Subject: [PATCH] Replace the hash key construction of LTL formulae by a simple counter updated each time we create a new (unique) formula. Doing so saves a lot of memory during the translation of the ltlcounter formulae, because the formulae are quite big and storing a string representation of each formula on its node was a bad idea. For instance with n=12, the translation now uses 40MB where it used 290MB. (Note: in both cases, 20MB is being used by the BDD cache.) * src/ltlast/formula.hh (hash_key_): Rename as ... (count_): ... this. (hash): Adjust. (max_count): New static variable to count the number of formulae created. (formula): Update max_count and set count_. (dump): Make it a virtual pure method. (set_key_): Remove. (formula_ptr_less_than): Speed up and return false when the two formula pointer are equal. * src/ltlast/formula.cc (set_key_, dump): Remove. * src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh, src/ltlast/automatop.cc, src/ltlast/automatop.hh, src/ltlast/binop.cc, src/ltlast/binop.hh, src/ltlast/constant.cc, src/ltlast/constant.hh, src/ltlast/multop.cc, src/ltlast/multop.hh, src/ltlast/unop.cc, src/ltlast/unop.hh: Empty the constructor (do not precompute the dump_ anymore), and add a dump() implementation. --- ChangeLog | 31 +++++++++++++++++++++++++++++++ src/ltlast/atomic_prop.cc | 8 ++++++-- src/ltlast/atomic_prop.hh | 5 ++++- src/ltlast/automatop.cc | 21 +++++++++++++-------- src/ltlast/automatop.hh | 4 ++++ src/ltlast/binop.cc | 12 ++++++++---- src/ltlast/binop.hh | 3 +++ src/ltlast/constant.cc | 34 ++++++++++++++++++---------------- src/ltlast/constant.hh | 4 +++- src/ltlast/formula.cc | 16 ++-------------- src/ltlast/formula.hh | 34 ++++++++++++++++++++++------------ src/ltlast/multop.cc | 21 ++++++++++++--------- src/ltlast/multop.hh | 3 +++ src/ltlast/unop.cc | 10 ++++++---- src/ltlast/unop.hh | 3 +++ 15 files changed, 138 insertions(+), 71 deletions(-) diff --git a/ChangeLog b/ChangeLog index e22c8a4d9..c1128d07a 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,34 @@ +2009-11-13 Alexandre Duret-Lutz + + Replace the hash key construction of LTL formulae by a simple + counter updated each time we create a new (unique) formula. + + Doing so saves a lot of memory during the translation of the + ltlcounter formulae, because the formulae are quite big and + storing a string representation of each formula on its node was a + bad idea. For instance with n=12, the translation now uses 40MB + where it used 290MB. (Note: in both cases, 20MB is being used by + the BDD cache.) + + * src/ltlast/formula.hh (hash_key_): Rename as ... + (count_): ... this. + (hash): Adjust. + (max_count): New static variable to count the number of + formulae created. + (formula): Update max_count and set count_. + (dump): Make it a virtual pure method. + (set_key_): Remove. + (formula_ptr_less_than): Speed up and return false when + the two formula pointer are equal. + * src/ltlast/formula.cc (set_key_, dump): Remove. + * src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh, + src/ltlast/automatop.cc, src/ltlast/automatop.hh, + src/ltlast/binop.cc, src/ltlast/binop.hh, src/ltlast/constant.cc, + src/ltlast/constant.hh, src/ltlast/multop.cc, + src/ltlast/multop.hh, src/ltlast/unop.cc, src/ltlast/unop.hh: + Empty the constructor (do not precompute the dump_ anymore), + and add a dump() implementation. + 2009-11-12 Alexandre Duret-Lutz Use -l wherever we where expecting ltl2tgba to default to LaCIM. diff --git a/src/ltlast/atomic_prop.cc b/src/ltlast/atomic_prop.cc index 9526f3806..b40d02920 100644 --- a/src/ltlast/atomic_prop.cc +++ b/src/ltlast/atomic_prop.cc @@ -32,8 +32,6 @@ namespace spot atomic_prop::atomic_prop(const std::string& name, environment& env) : name_(name), env_(&env) { - dump_ = "AP(" + name + ")"; - set_key_(); } atomic_prop::~atomic_prop() @@ -45,6 +43,12 @@ namespace spot instances.erase(i); } + std::string + atomic_prop::dump() const + { + return "AP(" + name() + ")"; + } + void atomic_prop::accept(visitor& v) { diff --git a/src/ltlast/atomic_prop.hh b/src/ltlast/atomic_prop.hh index 984c37619..78e032e79 100644 --- a/src/ltlast/atomic_prop.hh +++ b/src/ltlast/atomic_prop.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. // @@ -52,6 +52,9 @@ namespace spot /// Get the environment of the atomic proposition. environment& env() const; + /// Return a canonic representation of the atomic proposition + virtual std::string dump() const; + /// Number of instantiated atomic propositions. For debugging. static unsigned instance_count(); /// List all instances of atomic propositions. For debugging. diff --git a/src/ltlast/automatop.cc b/src/ltlast/automatop.cc index 56e902c98..5f1122dd9 100644 --- a/src/ltlast/automatop.cc +++ b/src/ltlast/automatop.cc @@ -30,14 +30,6 @@ namespace spot automatop::automatop(const nfa::ptr nfa, vec* v, bool negated) : nfa_(nfa), children_(v), negated_(negated) { - dump_ = negated ? "!" : ""; - dump_ += nfa->get_name(); - dump_ += "("; - dump_ += (*v)[0]->dump(); - for (unsigned n = 1; n < v->size(); ++n) - dump_ += ", " + (*v)[n]->dump(); - dump_ += ")"; - set_key_(); } automatop::~automatop() @@ -55,6 +47,19 @@ namespace spot delete children_; } + std::string + automatop::dump() const + { + std::string r = is_negated() ? "!" : ""; + r += nfa()->get_name(); + r += "("; + r += nth(0)->dump(); + for (unsigned n = 1; n < size(); ++n) + r += ", " + nth(n)->dump(); + r += ")"; + return r; + } + void automatop::accept(visitor& v) { diff --git a/src/ltlast/automatop.hh b/src/ltlast/automatop.hh index 93667fb8c..cb371dd29 100644 --- a/src/ltlast/automatop.hh +++ b/src/ltlast/automatop.hh @@ -68,8 +68,12 @@ namespace spot /// Get the NFA of this operator. const spot::ltl::nfa::ptr nfa() const; + /// Whether the automaton is negated. bool is_negated() const; + /// Return a canonic representation of the atomic proposition + std::string dump() const; + /// Number of instantiated multop operators. For debugging. static unsigned instance_count(); diff --git a/src/ltlast/binop.cc b/src/ltlast/binop.cc index 9615a36cd..1009c1170 100644 --- a/src/ltlast/binop.cc +++ b/src/ltlast/binop.cc @@ -32,10 +32,6 @@ namespace spot binop::binop(type op, formula* first, formula* second) : op_(op), first_(first), second_(second) { - dump_ = "binop("; - dump_ += op_name(); - dump_ += ", " + first->dump() + ", " + second->dump() + ")"; - set_key_(); } binop::~binop() @@ -52,6 +48,14 @@ namespace spot second()->destroy(); } + std::string + binop::dump() const + { + return (std::string("binop(") + op_name() + + ", " + first()->dump() + + ", " + second()->dump() + ")"); + } + void binop::accept(visitor& v) { diff --git a/src/ltlast/binop.hh b/src/ltlast/binop.hh index 23f5872d5..44b5567e4 100644 --- a/src/ltlast/binop.hh +++ b/src/ltlast/binop.hh @@ -68,6 +68,9 @@ namespace spot /// Get the type of this operator, as a string. const char* op_name() const; + /// Return a canonic representation of the atomic proposition + virtual std::string dump() const; + /// Number of instantiated binary operators. For debugging. static unsigned instance_count(); diff --git a/src/ltlast/constant.cc b/src/ltlast/constant.cc index 50573a3cd..4487c1064 100644 --- a/src/ltlast/constant.cc +++ b/src/ltlast/constant.cc @@ -1,6 +1,6 @@ -// Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. +// Copyright (C) 2003, 2005, 2009 Laboratoire d'Informatique de Paris +// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), +// Université Pierre et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -30,25 +30,27 @@ namespace spot constant::constant(type val) : val_(val) { - switch (val) - { - case True: - dump_ = "constant(1)"; - set_key_(); - return; - case False: - dump_ = "constant(0)"; - set_key_(); - return; - } - // Unreachable code. - assert(0); } constant::~constant() { } + std::string + constant::dump() const + { + switch (val()) + { + case True: + return "constant(1)"; + case False: + return "constant(0)"; + } + // Unreachable code. + assert(0); + return "BUG"; + } + void constant::accept(visitor& v) { diff --git a/src/ltlast/constant.hh b/src/ltlast/constant.hh index 46b15e698..f95568a46 100644 --- a/src/ltlast/constant.hh +++ b/src/ltlast/constant.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. // @@ -45,6 +45,8 @@ namespace spot /// Return the value of the constant as a string. const char* val_name() const; + virtual std::string dump() const; + /// Get the sole instance of spot::ltl::constant::constant(True). static constant* true_instance(); /// Get the sole instance of spot::ltl::constant::constant(False). diff --git a/src/ltlast/formula.cc b/src/ltlast/formula.cc index b42d7823a..2fa6182df 100644 --- a/src/ltlast/formula.cc +++ b/src/ltlast/formula.cc @@ -26,6 +26,8 @@ namespace spot { namespace ltl { + size_t formula::max_count = 0; + formula* formula::clone() const { @@ -56,19 +58,5 @@ namespace spot // Not reference counted by default. return false; } - - const std::string& - formula::dump() const - { - return dump_; - } - - void - formula::set_key_() - { - string_hash sh; - hash_key_ = sh(dump_); - } - } } diff --git a/src/ltlast/formula.hh b/src/ltlast/formula.hh index c0743fa4d..03d36c0a1 100644 --- a/src/ltlast/formula.hh +++ b/src/ltlast/formula.hh @@ -71,6 +71,8 @@ namespace spot class formula { public: + formula() : count_(++max_count) {} + /// Entry point for vspot::ltl::visitor instances. virtual void accept(visitor& v) = 0; /// Entry point for vspot::ltl::const_visitor instances. @@ -88,13 +90,13 @@ namespace spot void destroy() const; /// Return a canonic representation of the formula - const std::string& dump() const; + virtual std::string dump() const = 0; - /// Return a hash_key for the formula. + /// Return a hash key for the formula. size_t hash() const { - return hash_key_; + return count_; } protected: virtual ~formula(); @@ -105,16 +107,12 @@ namespace spot /// the instance must be deleted (usually when the counter hits 0). virtual bool unref_(); - /// \brief Compute key_ from dump_. - /// - /// Should be called once in each object, after dump_ has been set. - void set_key_(); - /// The canonic representation of the formula - std::string dump_; /// \brief The hash key of this formula. - /// - /// Initialized by set_key_(). - size_t hash_key_; + size_t count_; + + private: + /// \brief Number of formulae created so far. + static size_t max_count; }; /// \brief Strict Weak Ordering for const formula*. @@ -138,10 +136,22 @@ namespace spot { assert(left); assert(right); + if (left == right) + return false; size_t l = left->hash(); size_t r = right->hash(); if (l != r) return l < r; + // Because the hash code assigned to each formula is the + // number of formulae constructed so far, it is very unlikely + // that we will ever reach a case were two different formulae + // have the same hash. This will happen only ever with have + // produced 256**sizeof(size_t) formulae (i.e. max_count has + // looped back to 0 and started over). In that case we can + // order two formulae by looking at their text representation. + // We could be more efficient and look at their AST, but it's + // not worth the burden. (Also ordering pointers is ruled out + // because it breaks the determinism of the implementation.) return left->dump() < right->dump(); } }; diff --git a/src/ltlast/multop.cc b/src/ltlast/multop.cc index 9a10be5f3..91e3ee66c 100644 --- a/src/ltlast/multop.cc +++ b/src/ltlast/multop.cc @@ -34,15 +34,6 @@ namespace spot multop::multop(type op, vec* v) : op_(op), children_(v) { - dump_ = "multop("; - dump_ += op_name(); - unsigned max = v->size(); - for (unsigned n = 0; n < max; ++n) - { - dump_ += ", " + (*v)[n]->dump(); - } - dump_ += ")"; - set_key_(); } multop::~multop() @@ -60,6 +51,18 @@ namespace spot delete children_; } + std::string + multop::dump() const + { + std::string r = "multop("; + r += op_name(); + unsigned max = size(); + for (unsigned n = 0; n < max; ++n) + r += ", " + nth(n)->dump(); + r += ")"; + return r; + } + void multop::accept(visitor& v) { diff --git a/src/ltlast/multop.hh b/src/ltlast/multop.hh index 0ab9b72ca..d941373e3 100644 --- a/src/ltlast/multop.hh +++ b/src/ltlast/multop.hh @@ -93,6 +93,9 @@ namespace spot /// Get the type of this operator, as a string. const char* op_name() const; + /// Return a canonic representation of the atomic proposition + virtual std::string dump() const; + /// Number of instantiated multi-operand operators. For debugging. static unsigned instance_count(); diff --git a/src/ltlast/unop.cc b/src/ltlast/unop.cc index e731b9cba..4e69cfe33 100644 --- a/src/ltlast/unop.cc +++ b/src/ltlast/unop.cc @@ -31,10 +31,6 @@ namespace spot unop::unop(type op, formula* child) : op_(op), child_(child) { - dump_ = "unop("; - dump_ += op_name(); - dump_ += ", " + child->dump() + ")"; - set_key_(); } unop::~unop() @@ -49,6 +45,12 @@ namespace spot child()->destroy(); } + std::string + unop::dump() const + { + return std::string("unop(") + op_name() + ", " + child()->dump() + ")"; + } + void unop::accept(visitor& v) { diff --git a/src/ltlast/unop.hh b/src/ltlast/unop.hh index e0bbf8879..4357fff94 100644 --- a/src/ltlast/unop.hh +++ b/src/ltlast/unop.hh @@ -57,6 +57,9 @@ namespace spot /// Get the type of this operator, as a string. const char* op_name() const; + /// Return a canonic representation of the atomic proposition + virtual std::string dump() const; + /// Number of instantiated unary operators. For debugging. static unsigned instance_count();