diff --git a/ChangeLog b/ChangeLog index 53501e694..8ed9ae254 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,11 @@ +2008-06-12 Alexandre Duret-Lutz + + * src/ltlast/atomic_prop.cc, src/ltlast/binop.cc, + src/ltlast/constant.cc, src/ltlast/formula.cc, + src/ltlast/multop.cc, src/ltlast/predecl.hh, + src/ltlast/refformula.cc, src/ltlast/unop.cc: Delete these files, + not used anymore since 2008-04-16. + 2008-06-11 Alexandre Duret-Lutz * iface/nips/dottynips.cc: Include ctsdlib for exit(). diff --git a/src/ltlast/atomic_prop.cc b/src/ltlast/atomic_prop.cc deleted file mode 100644 index 8fd0d2384..000000000 --- a/src/ltlast/atomic_prop.cc +++ /dev/null @@ -1,108 +0,0 @@ -// 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 2 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 Spot; see the file COPYING. If not, write to the Free -// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA -// 02111-1307, USA. - -#include "atomic_prop.hh" -#include "visitor.hh" -#include -#include - -namespace spot -{ - namespace ltl - { - - atomic_prop::atomic_prop(const std::string& name, environment& env) - : name_(name), env_(&env) - { - dump_ = "AP(" + name + ")"; - set_key_(); - } - - atomic_prop::~atomic_prop() - { - // Get this instance out of the instance map. - pair p(name(), &env()); - map::iterator i = instances.find(p); - assert (i != instances.end()); - instances.erase(i); - } - - void - atomic_prop::accept(visitor& v) - { - v.visit(this); - } - - void - atomic_prop::accept(const_visitor& v) const - { - v.visit(this); - } - - const std::string& - atomic_prop::name() const - { - return name_; - } - - environment& - atomic_prop::env() const - { - return *env_; - } - - atomic_prop::map atomic_prop::instances; - - atomic_prop* - atomic_prop::instance(const std::string& name, environment& env) - { - pair p(name, &env); - map::iterator i = instances.find(p); - if (i != instances.end()) - { - return static_cast(i->second->ref()); - } - atomic_prop* ap = new atomic_prop(name, env); - instances[p] = ap; - return static_cast(ap->ref()); - } - - unsigned - atomic_prop::instance_count() - { - return instances.size(); - } - - std::ostream& - atomic_prop::dump_instances(std::ostream& os) - { - - for (map::iterator i = instances.begin(); i != instances.end(); ++i) - { - os << i->second << " = " << i->second->ref_count_() - << " * atomic_prop(" << i->first.first << ", " - << i->first.second->name() << ")" << std::endl; - } - return os; - } - - } -} diff --git a/src/ltlast/binop.cc b/src/ltlast/binop.cc deleted file mode 100644 index 65dfad1e3..000000000 --- a/src/ltlast/binop.cc +++ /dev/null @@ -1,153 +0,0 @@ -// 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. -// -// 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 2 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 Spot; see the file COPYING. If not, write to the Free -// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA -// 02111-1307, USA. - -#include -#include -#include "binop.hh" -#include "visitor.hh" - -namespace spot -{ - namespace ltl - { - 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() - { - // Get this instance out of the instance map. - pairf pf(first(), second()); - pair p(op(), pf); - map::iterator i = instances.find(p); - assert (i != instances.end()); - instances.erase(i); - } - - void - binop::accept(visitor& v) - { - v.visit(this); - } - - void - binop::accept(const_visitor& v) const - { - v.visit(this); - } - - const formula* - binop::first() const - { - return first_; - } - - formula* - binop::first() - { - return first_; - } - - const formula* - binop::second() const - { - return second_; - } - - formula* - binop::second() - { - return second_; - } - - binop::type - binop::op() const - { - return op_; - } - - const char* - binop::op_name() const - { - switch (op_) - { - case Xor: - return "Xor"; - case Implies: - return "Implies"; - case Equiv: - return "Equiv"; - case U: - return "U"; - case R: - return "R"; - } - // Unreachable code. - assert(0); - return 0; - } - - binop::map binop::instances; - - binop* - binop::instance(type op, formula* first, formula* second) - { - // Sort the operands of associative operators, so that for - // example the formula instance for 'a xor b' is the same as - // that for 'b xor a'. - switch (op) - { - case Xor: - case Equiv: - if (second < first) - std::swap(first, second); - break; - case Implies: - case U: - case R: - // Non associative operators. - break; - } - - pairf pf(first, second); - pair p(op, pf); - map::iterator i = instances.find(p); - if (i != instances.end()) - { - return static_cast(i->second->ref()); - } - binop* ap = new binop(op, first, second); - instances[p] = ap; - return static_cast(ap->ref()); - } - - unsigned - binop::instance_count() - { - return instances.size(); - } - } -} diff --git a/src/ltlast/constant.cc b/src/ltlast/constant.cc deleted file mode 100644 index 50573a3cd..000000000 --- a/src/ltlast/constant.cc +++ /dev/null @@ -1,99 +0,0 @@ -// 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. -// -// 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 2 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 Spot; see the file COPYING. If not, write to the Free -// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA -// 02111-1307, USA. - -#include "constant.hh" -#include "visitor.hh" -#include - -namespace spot -{ - namespace ltl - { - 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() - { - } - - void - constant::accept(visitor& v) - { - v.visit(this); - } - - void - constant::accept(const_visitor& v) const - { - v.visit(this); - } - - constant::type - constant::val() const - { - return val_; - } - - const char* - constant::val_name() const - { - switch (val_) - { - case True: - return "1"; - case False: - return "0"; - } - // Unreachable code. - assert(0); - return 0; - } - - constant* - constant::false_instance() - { - static constant f(constant::False); - return &f; - } - - constant* - constant::true_instance() - { - static constant t(constant::True); - return &t; - } - } -} diff --git a/src/ltlast/formula.cc b/src/ltlast/formula.cc deleted file mode 100644 index e194c2c72..000000000 --- a/src/ltlast/formula.cc +++ /dev/null @@ -1,74 +0,0 @@ -// 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. -// -// 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 2 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 Spot; see the file COPYING. If not, write to the Free -// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA -// 02111-1307, USA. - -#include "formula.hh" -#include "misc/hash.hh" - -namespace spot -{ - namespace ltl - { - formula* - formula::ref() - { - ref_(); - return this; - } - - formula::~formula() - { - } - - void - formula::unref(formula* f) - { - if (f->unref_()) - delete f; - } - - void - formula::ref_() - { - // Not reference counted by default. - } - - bool - formula::unref_() - { - // 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/multop.cc b/src/ltlast/multop.cc deleted file mode 100644 index 1e00d07cb..000000000 --- a/src/ltlast/multop.cc +++ /dev/null @@ -1,212 +0,0 @@ -// 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 2 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 Spot; see the file COPYING. If not, write to the Free -// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA -// 02111-1307, USA. - -#include -#include -#include -#include "multop.hh" -#include "constant.hh" -#include "visitor.hh" -#include "ltlvisit/destroy.hh" - -namespace spot -{ - namespace ltl - { - 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() - { - // Get this instance out of the instance map. - pair p(op(), children_); - map::iterator i = instances.find(p); - assert (i != instances.end()); - instances.erase(i); - - delete children_; - } - - void - multop::accept(visitor& v) - { - v.visit(this); - } - - void - multop::accept(const_visitor& v) const - { - v.visit(this); - } - - unsigned - multop::size() const - { - return children_->size(); - } - - const formula* - multop::nth(unsigned n) const - { - return (*children_)[n]; - } - - formula* - multop::nth(unsigned n) - { - return (*children_)[n]; - } - - multop::type - multop::op() const - { - return op_; - } - - const char* - multop::op_name() const - { - switch (op_) - { - case And: - return "And"; - case Or: - return "Or"; - } - // Unreachable code. - assert(0); - return 0; - } - - multop::map multop::instances; - - formula* - multop::instance(type op, vec* v) - { - pair p(op, v); - - // Inline children of same kind. - { - vec inlined; - vec::iterator i = v->begin(); - while (i != v->end()) - { - multop* p = dynamic_cast(*i); - if (p && p->op() == op) - { - unsigned ps = p->size(); - for (unsigned n = 0; n < ps; ++n) - inlined.push_back(p->nth(n)); - // That sub-formula is now useless, drop it. - // Note that we use unref(), not destroy(), because we've - // adopted its children and don't want to destroy these. - formula::unref(*i); - i = v->erase(i); - } - else - { - ++i; - } - } - v->insert(v->end(), inlined.begin(), inlined.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. - { - formula* last = 0; - vec::iterator i = v->begin(); - while (i != v->end()) - { - if (*i == last) - { - destroy(*i); - i = v->erase(i); - } - else - { - last = *i++; - } - } - } - - vec::size_type s = v->size(); - if (s == 0) - { - delete v; - switch (op) - { - case And: - return constant::true_instance(); - case Or: - return constant::false_instance(); - } - /* Unreachable code. */ - assert(0); - } - else if (s == 1) - { - formula* res = (*v)[0]; - delete v; - return res; - } - - map::iterator i = instances.find(p); - if (i != instances.end()) - { - delete v; - return static_cast(i->second->ref()); - } - multop* ap = new multop(op, v); - instances[p] = ap; - return static_cast(ap->ref()); - - } - - formula* - multop::instance(type op, formula* first, formula* second) - { - vec* v = new vec; - v->push_back(first); - v->push_back(second); - return instance(op, v); - } - - unsigned - multop::instance_count() - { - return instances.size(); - } - } -} diff --git a/src/ltlast/predecl.hh b/src/ltlast/predecl.hh deleted file mode 100644 index 121c9ef5d..000000000 --- a/src/ltlast/predecl.hh +++ /dev/null @@ -1,48 +0,0 @@ -// 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 2 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 Spot; see the file COPYING. If not, write to the Free -// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA -// 02111-1307, USA. - -/// \file ltlast/predecl.hh -/// \brief Predeclare all LTL node types. -/// -/// This file is usually used when \b declaring methods and functions -/// over LTL nodes. -/// Use ltlast/allnodes.hh or an individual header when the definition of -/// the node is actually needed. -#ifndef SPOT_LTLAST_PREDECL_HH -# define SPOT_LTLAST_PREDECL_HH - -namespace spot -{ - namespace ltl - { - struct visitor; - struct const_visitor; - - struct atomic_prop; - struct unop; - struct constant; - struct binop; - struct formula; - struct multop; - } -} - -#endif // SPOT_LTLAST_PREDECL_HH diff --git a/src/ltlast/refformula.cc b/src/ltlast/refformula.cc deleted file mode 100644 index 06ad2dad7..000000000 --- a/src/ltlast/refformula.cc +++ /dev/null @@ -1,58 +0,0 @@ -// 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 2 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 Spot; see the file COPYING. If not, write to the Free -// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA -// 02111-1307, USA. - -#include "refformula.hh" -#include - -namespace spot -{ - namespace ltl - { - ref_formula::ref_formula() - : ref_counter_(0) - { - } - - ref_formula::~ref_formula() - { - } - - void - ref_formula::ref_() - { - ++ref_counter_; - } - - bool - ref_formula::unref_() - { - assert(ref_counter_ > 0); - return !--ref_counter_; - } - - unsigned - ref_formula::ref_count_() - { - return ref_counter_; - } - - } -} diff --git a/src/ltlast/unop.cc b/src/ltlast/unop.cc deleted file mode 100644 index f4cd9f2a4..000000000 --- a/src/ltlast/unop.cc +++ /dev/null @@ -1,119 +0,0 @@ -// 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. -// -// 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 2 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 Spot; see the file COPYING. If not, write to the Free -// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA -// 02111-1307, USA. - -#include "unop.hh" -#include "visitor.hh" -#include - -namespace spot -{ - namespace ltl - { - unop::unop(type op, formula* child) - : op_(op), child_(child) - { - dump_ = "unop("; - dump_ += op_name(); - dump_ += ", " + child->dump() + ")"; - set_key_(); - } - - unop::~unop() - { - // Get this instance out of the instance map. - pair p(op(), child()); - map::iterator i = instances.find(p); - assert (i != instances.end()); - instances.erase(i); - } - - void - unop::accept(visitor& v) - { - v.visit(this); - } - - void - unop::accept(const_visitor& v) const - { - v.visit(this); - } - - const formula* - unop::child() const - { - return child_; - } - - formula* - unop::child() - { - return child_; - } - - unop::type - unop::op() const - { - return op_; - } - - const char* - unop::op_name() const - { - switch (op_) - { - case Not: - return "Not"; - case X: - return "X"; - case F: - return "F"; - case G: - return "G"; - } - // Unreachable code. - assert(0); - return 0; - } - - unop::map unop::instances; - - unop* - unop::instance(type op, formula* child) - { - pair p(op, child); - map::iterator i = instances.find(p); - if (i != instances.end()) - { - return static_cast(i->second->ref()); - } - unop* ap = new unop(op, child); - instances[p] = ap; - return static_cast(ap->ref()); - } - - unsigned - unop::instance_count() - { - return instances.size(); - } - } -}