diff --git a/ChangeLog b/ChangeLog index 396a60d2c..85f181af5 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,16 @@ +2005-01-20 Alexandre Duret-Lutz + + * src/ltlast/formula.hh (hash, dump, dump_, hash_key_): New members. + (formula_ptr_less_than, formula_ptr_hash): New class. + * src/ltlast/atomic_prop.cc, src/ltlast/binop.cc, + src/ltlast/constant.cc, src/ltlast/formula.cc, + src/ltlast/multop.cc, src/ltlast/unop.cc: Adjust to handle dump_. + * src/ltlvisit/apcollect.cc, src/ltlvisit/apcollect.hh: + Sort the set using formula_ptr_less_than. + * src/ltlvisit/dump.cc: Simplify using ->dump(). + * src/tgbaalgos/ltl2tgba_fm.cc: Sort all maps to get deterministic + results. + 2005-01-18 Alexandre Duret-Lutz * src/tgbaalgos/tau03opt.hh (explicit_tau03_opt_search): Doco. diff --git a/src/ltlast/atomic_prop.cc b/src/ltlast/atomic_prop.cc index d37793f1d..8fd0d2384 100644 --- a/src/ltlast/atomic_prop.cc +++ b/src/ltlast/atomic_prop.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// 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. // @@ -32,6 +32,8 @@ 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() diff --git a/src/ltlast/binop.cc b/src/ltlast/binop.cc index ae12259d7..65dfad1e3 100644 --- a/src/ltlast/binop.cc +++ b/src/ltlast/binop.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// 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. // @@ -31,6 +31,10 @@ 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() diff --git a/src/ltlast/constant.cc b/src/ltlast/constant.cc index fb276fe00..50573a3cd 100644 --- a/src/ltlast/constant.cc +++ b/src/ltlast/constant.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// 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. // @@ -30,6 +30,19 @@ 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() diff --git a/src/ltlast/formula.cc b/src/ltlast/formula.cc index d071f6b76..e194c2c72 100644 --- a/src/ltlast/formula.cc +++ b/src/ltlast/formula.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// 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. // @@ -20,6 +20,7 @@ // 02111-1307, USA. #include "formula.hh" +#include "misc/hash.hh" namespace spot { @@ -55,5 +56,19 @@ 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 5cf297ba9..0a678eec6 100644 --- a/src/ltlast/formula.hh +++ b/src/ltlast/formula.hh @@ -24,6 +24,8 @@ #ifndef SPOT_LTLAST_FORMULA_HH # define SPOT_LTLAST_FORMULA_HH +#include +#include #include "predecl.hh" namespace spot @@ -89,6 +91,15 @@ namespace spot /// want to release a whole formula, use spot::ltl::destroy() instead. static void unref(formula* f); + /// Return a canonic representation of the formula + const std::string& dump() const; + + /// Return a hash_key for the formula. + const size_t + hash() const + { + return hash_key_; + } protected: virtual ~formula(); @@ -97,8 +108,70 @@ namespace spot /// \brief decrement reference counter if any, return true when /// 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_; }; + /// \brief Strict Weak Ordering for const formula*. + /// \ingroup ltl_essentials + /// + /// This is meant to be used as a comparison functor for + /// STL \c map whose key are of type const formula*. + /// + /// For instance here is how one could declare + /// a map of \c const::formula*. + /// \code + /// // Remember how many times each formula has been seen. + /// std::map seen; + /// \endcode + struct formula_ptr_less_than: + public std::binary_function + { + bool + operator()(const formula* left, const formula* right) const + { + assert(left); + assert(right); + return left->hash() < right->hash(); + } + }; + + /// \brief Hash Function for const formula*. + /// \ingroup ltl_essentials + /// \ingroup hash_funcs + /// + /// This is meant to be used as a hash functor for + /// Sgi's \c hash_map whose key are of type const formula*. + /// + /// For instance here is how one could declare + /// a map of \c const::formula*. + /// \code + /// // Remember how many times each formula has been seen. + /// Sgi::hash_map seen; + /// \endcode + struct formula_ptr_hash: + public std::unary_function + { + size_t + operator()(const formula* that) const + { + assert(that); + return that->hash(); + } + }; + + } } diff --git a/src/ltlast/multop.cc b/src/ltlast/multop.cc index ea0f99bcc..1e00d07cb 100644 --- a/src/ltlast/multop.cc +++ b/src/ltlast/multop.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// 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. // @@ -34,6 +34,15 @@ 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() @@ -131,7 +140,7 @@ namespace spot v->insert(v->end(), inlined.begin(), inlined.end()); } - std::sort(v->begin(), v->end()); + std::sort(v->begin(), v->end(), formula_ptr_less_than()); // Remove duplicates. We can't use std::unique(), because we // must destroy() any formula we drop. diff --git a/src/ltlast/unop.cc b/src/ltlast/unop.cc index 602d30d95..f4cd9f2a4 100644 --- a/src/ltlast/unop.cc +++ b/src/ltlast/unop.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// 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. // @@ -30,6 +30,10 @@ namespace spot unop::unop(type op, formula* child) : op_(op), child_(child) { + dump_ = "unop("; + dump_ += op_name(); + dump_ += ", " + child->dump() + ")"; + set_key_(); } unop::~unop() diff --git a/src/ltlvisit/apcollect.cc b/src/ltlvisit/apcollect.cc index e41532682..65a886882 100644 --- a/src/ltlvisit/apcollect.cc +++ b/src/ltlvisit/apcollect.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -20,6 +20,7 @@ // 02111-1307, USA. #include "apcollect.hh" +#include "ltlvisit/postfix.hh" namespace spot { diff --git a/src/ltlvisit/apcollect.hh b/src/ltlvisit/apcollect.hh index 0c2b037d3..069afa0e9 100644 --- a/src/ltlvisit/apcollect.hh +++ b/src/ltlvisit/apcollect.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -23,7 +23,7 @@ # define SPOT_LTLVISIT_APCOLLECT_HH #include -#include "ltlvisit/postfix.hh" +#include "ltlast/atomic_prop.hh" namespace spot { @@ -33,7 +33,7 @@ namespace spot /// @{ /// Set of atomic propositions. - typedef std::set atomic_prop_set; + typedef std::set atomic_prop_set; /// \brief Return the set of atomic propositions occurring in a formula. /// diff --git a/src/ltlvisit/dump.cc b/src/ltlvisit/dump.cc index 97f7b866b..3d94732cf 100644 --- a/src/ltlvisit/dump.cc +++ b/src/ltlvisit/dump.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// 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. // @@ -28,74 +28,10 @@ namespace spot { namespace ltl { - namespace - { - class dump_visitor: public const_visitor - { - public: - dump_visitor(std::ostream& os) - : os_(os) - { - } - - virtual - ~dump_visitor() - { - } - - void - visit(const atomic_prop* ap) - { - os_ << "AP(" << ap->name() << ")"; - } - - void - visit(const constant* c) - { - os_ << "constant(" << c->val_name() << ")"; - } - - void - visit(const binop* bo) - { - os_ << "binop(" << bo->op_name() << ", "; - bo->first()->accept(*this); - os_ << ", "; - bo->second()->accept(*this); - os_ << ")"; - } - - void - visit(const unop* uo) - { - os_ << "unop(" << uo->op_name() << ", "; - uo->child()->accept(*this); - os_ << ")"; - } - - void - visit(const multop* mo) - { - os_ << "multop(" << mo->op_name() << ", "; - unsigned max = mo->size(); - mo->nth(0)->accept(*this); - for (unsigned n = 1; n < max; ++n) - { - os_ << ", "; - mo->nth(n)->accept(*this); - } - os_ << ")"; - } - private: - std::ostream& os_; - }; - } - std::ostream& dump(std::ostream& os, const formula* f) { - dump_visitor v(os); - f->accept(v); + os << f->dump(); return os; } diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index 5da00c6cf..348580c4f 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// 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. // @@ -533,7 +533,7 @@ namespace spot } private: - typedef Sgi::hash_map > pfl_map; + typedef Sgi::hash_map pfl_map; pfl_map pfl_; }; @@ -613,7 +613,7 @@ namespace spot } typedef std::map prom_map; - typedef Sgi::hash_map > dest_map; + typedef Sgi::hash_map dest_map; static void fill_dests(translate_dict& d, dest_map& dests, bdd label, const formula* dest) @@ -649,8 +649,9 @@ namespace spot formula* f2 = negative_normal_form(f1); destroy(f1); - std::set formulae_seen; - std::set formulae_to_translate; + typedef std::set set_type; + set_type formulae_seen; + set_type formulae_to_translate; translate_dict d(dict); formula_canonizer fc(d);