diff --git a/iface/dve2/dve2check.cc b/iface/dve2/dve2check.cc index 897f69b54..a1c95bac5 100644 --- a/iface/dve2/dve2check.cc +++ b/iface/dve2/dve2check.cc @@ -379,12 +379,10 @@ main(int argc, char **argv) spot::ltl::unop::dump_instances(std::cerr); spot::ltl::binop::dump_instances(std::cerr); spot::ltl::multop::dump_instances(std::cerr); - spot::ltl::automatop::dump_instances(std::cerr); assert(spot::ltl::atomic_prop::instance_count() == 0); assert(spot::ltl::unop::instance_count() == 0); assert(spot::ltl::binop::instance_count() == 0); assert(spot::ltl::multop::instance_count() == 0); - assert(spot::ltl::automatop::instance_count() == 0); exit(exit_code); } diff --git a/src/ltlast/Makefile.am b/src/ltlast/Makefile.am index b2b49b2b0..5ac7cace9 100644 --- a/src/ltlast/Makefile.am +++ b/src/ltlast/Makefile.am @@ -1,6 +1,6 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2009, 2010, 2011, 2013 Laboratoire de Recherche et -## Développement de l'Epita (LRDE). +## Copyright (C) 2009, 2010, 2011, 2013, 2014 Laboratoire de Recherche +## et Développement de l'Epita (LRDE). ## Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), ## département Systèmes Répartis Coopératifs (SRC), Université Pierre ## et Marie Curie. @@ -29,13 +29,11 @@ ltlastdir = $(pkgincludedir)/ltlast ltlast_HEADERS = \ allnodes.hh \ atomic_prop.hh \ - automatop.hh \ binop.hh \ bunop.hh \ constant.hh \ formula.hh \ multop.hh \ - nfa.hh \ predecl.hh \ refformula.hh \ unop.hh \ @@ -44,14 +42,10 @@ ltlast_HEADERS = \ noinst_LTLIBRARIES = libltlast.la libltlast_la_SOURCES = \ atomic_prop.cc \ - automatop.cc \ binop.cc \ bunop.cc \ constant.cc \ formula.cc \ - formula_tree.cc \ - formula_tree.hh \ multop.cc \ - nfa.cc \ refformula.cc \ unop.cc diff --git a/src/ltlast/allnodes.hh b/src/ltlast/allnodes.hh index 4e71c2621..30c4bbcaa 100644 --- a/src/ltlast/allnodes.hh +++ b/src/ltlast/allnodes.hh @@ -1,5 +1,8 @@ -// Copyright (C) 2003, 2004, 2010 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// -*- coding: utf-8 -*- +// Copyright (C) 2010, 2014 Laboratoire de Recherche et Développement +// 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. @@ -31,7 +34,6 @@ # include "multop.hh" # include "atomic_prop.hh" # include "constant.hh" -# include "automatop.hh" # include "bunop.hh" #endif // SPOT_LTLAST_ALLNODES_HH diff --git a/src/ltlast/automatop.cc b/src/ltlast/automatop.cc deleted file mode 100644 index fcc7930a1..000000000 --- a/src/ltlast/automatop.cc +++ /dev/null @@ -1,137 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire -// de Recherche et Développement de l'Epita (LRDE) -// -// 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 -#include -#include "automatop.hh" -#include "nfa.hh" -#include "visitor.hh" - -namespace spot -{ - namespace ltl - { - automatop::automatop(const nfa::ptr nfa, vec* v, bool negated) - : ref_formula(AutomatOp), nfa_(nfa), children_(v), negated_(negated) - { - assert(nfa); - - is.boolean = false; - is.sugar_free_boolean = true; - is.in_nenoform = true; - is.X_free = true; - is.sugar_free_ltl = true; - is.ltl_formula = false; - is.eltl_formula = true; - is.psl_formula = false; - is.sere_formula = false; - is.finite = false; - is.eventual = false; - is.universal = false; - is.syntactic_safety = false; - is.syntactic_guarantee = false; - is.syntactic_obligation = false; - is.syntactic_recurrence = false; - is.syntactic_persistence = false; - is.not_marked = true; - is.accepting_eword = false; - - unsigned s = v->size(); - for (unsigned i = 0; i < s; ++i) - props &= (*v)[i]->get_props(); - } - - automatop::~automatop() - { - // Get this instance out of the instance map. - size_t c = instances.erase(key(get_nfa(), negated_, children_)); - assert(c == 1); - (void) c; // For the NDEBUG case. - - // Dereference children. - unsigned s = size(); - for (unsigned n = 0; n < s; ++n) - nth(n)->destroy(); - - delete children_; - } - - std::string - automatop::dump() const - { - std::string r = is_negated() ? "!" : ""; - r += get_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) const - { - v.visit(this); - } - - automatop::map automatop::instances; - - const automatop* - automatop::instance(const nfa::ptr nfa, vec* v, bool negated) - { - assert(nfa); - const automatop* res; - auto ires = instances.insert(std::make_pair(key(nfa, negated, v), - nullptr)); - if (!ires.second) - { - // The instance already exists. - for (vec::iterator vi = v->begin(); vi != v->end(); ++vi) - (*vi)->destroy(); - delete v; - res = ires.first->second; - } - else - { - res = ires.first->second = new automatop(nfa, v, negated); - } - res->clone(); - return res; - } - - unsigned - automatop::instance_count() - { - return instances.size(); - } - - std::ostream& - automatop::dump_instances(std::ostream& os) - { - for (const auto& i: instances) - os << i.second << " = " - << i.second->ref_count_() << " * " - << i.second->dump() - << std::endl; - return os; - } - } -} diff --git a/src/ltlast/automatop.hh b/src/ltlast/automatop.hh deleted file mode 100644 index 3b27f7854..000000000 --- a/src/ltlast/automatop.hh +++ /dev/null @@ -1,121 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2008, 2009, 2012, 2013, 2014 Laboratoire de Recherche et -// Développement de l'Epita (LRDE) -// -// 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/automatop.hh -/// \brief ELTL automaton operators -#ifndef SPOT_LTLAST_AUTOMATOP_HH -# define SPOT_LTLAST_AUTOMATOP_HH - -# include "refformula.hh" -# include -# include -# include -# include -# include "nfa.hh" - -namespace spot -{ - namespace ltl - { - /// \ingroup eltl_ast - /// \brief Automaton operators. - /// - class SPOT_API automatop : public ref_formula - { - public: - /// List of formulae. - typedef std::vector vec; - - /// \brief Build a spot::ltl::automatop with many children. - /// - /// This vector is acquired by the spot::ltl::automatop class, - /// the caller should allocate it with \c new, but not use it - /// (especially not destroy it) after it has been passed to - /// spot::ltl::automatop. - static const automatop* - instance(const nfa::ptr nfa, vec* v, bool negated); - - virtual void accept(visitor& v) const; - - /// Get the number of arguments. - unsigned size() const - { - return children_->size(); - } - - /// \brief Get the nth argument. - /// - /// Starting with \a n = 0. - const formula* nth(unsigned n) const - { - return (*children_)[n]; - } - - /// Get the NFA of this operator. - const spot::ltl::nfa::ptr get_nfa() const - { - return nfa_; - } - - /// Whether the automaton is negated. - bool is_negated() const - { - return negated_; - } - - /// Return a canonic representation of the atomic proposition - std::string dump() const; - - /// Number of instantiated multop operators. For debugging. - static unsigned instance_count(); - - /// Dump all instances. For debugging. - static std::ostream& dump_instances(std::ostream& os); - - - protected: - typedef std::tuple key; - /// Comparison functor used internally by ltl::automatop. - struct tripletcmp - { - bool - operator()(const key& p1, const key& p2) const - { - if (std::get<0>(p1) != std::get<0>(p2)) - return std::get<0>(p1) < std::get<0>(p2); - if (std::get<1>(p1) != std::get<1>(p2)) - return std::get<1>(p1) < std::get<1>(p2); - return *std::get<2>(p1) < *std::get<2>(p2); - } - }; - typedef std::map map; - static map instances; - - automatop(const nfa::ptr, vec* v, bool negated); - virtual ~automatop(); - - private: - const nfa::ptr nfa_; - vec* children_; - bool negated_; - }; - } -} - -#endif // SPOT_LTLAST_AUTOMATOP_HH diff --git a/src/ltlast/formula.hh b/src/ltlast/formula.hh index 3170842bb..85d95ec75 100644 --- a/src/ltlast/formula.hh +++ b/src/ltlast/formula.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013 Laboratoire de -// Recherche et Développement de l'Epita (LRDE). +// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire +// de Recherche et Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de // // This file is part of Spot, a model checking library. @@ -78,8 +78,7 @@ namespace spot UnOp, BinOp, MultOp, - BUnOp, - AutomatOp }; + BUnOp }; protected: formula(opkind k) : count_(max_count++), kind_(k) diff --git a/src/ltlast/formula_tree.cc b/src/ltlast/formula_tree.cc deleted file mode 100644 index 1920a9582..000000000 --- a/src/ltlast/formula_tree.cc +++ /dev/null @@ -1,82 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2009, 2012, 2013, 2014 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). -// -// 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 -#include "formula_tree.hh" -#include "allnodes.hh" - -namespace spot -{ - namespace ltl - { - namespace formula_tree - { - const formula* - instanciate(const node_ptr np, const std::vector& v) - { - if (node_atomic* n = dynamic_cast(np.get())) - return n->i == True ? constant::true_instance() : - 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)); - if (node_nfa* n = dynamic_cast(np.get())) - { - automatop::vec* va = new automatop::vec; - std::vector::const_iterator i = n->children.begin(); - while (i != n->children.end()) - va->push_back(instanciate(*i++, v)); - return automatop::instance(n->nfa, va, false); - } - if (node_binop* n = dynamic_cast(np.get())) - return binop::instance(n->op, - instanciate(n->lhs, v), - instanciate(n->rhs, v)); - if (node_multop* n = dynamic_cast(np.get())) - return multop::instance(n->op, - instanciate(n->lhs, v), - instanciate(n->rhs, v)); - SPOT_UNREACHABLE(); - } - - size_t - arity(const node_ptr np) - { - if (node_atomic* n = dynamic_cast(np.get())) - return std::max(n->i + 1, 0); - if (node_unop* n = dynamic_cast(np.get())) - return arity(n->child); - if (node_nfa* n = dynamic_cast(np.get())) - { - size_t res = 0; - std::vector::const_iterator i = n->children.begin(); - while (i != n->children.end()) - res = std::max(arity(*i++), res); - return res; - } - if (node_binop* n = dynamic_cast(np.get())) - return std::max(arity(n->lhs), arity(n->rhs)); - if (node_multop* n = dynamic_cast(np.get())) - return std::max(arity(n->lhs), arity(n->rhs)); - SPOT_UNREACHABLE(); - } - } - } -} diff --git a/src/ltlast/formula_tree.hh b/src/ltlast/formula_tree.hh deleted file mode 100644 index 120260917..000000000 --- a/src/ltlast/formula_tree.hh +++ /dev/null @@ -1,89 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2009, 2012, 2013, 2014 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). -// -// 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/formula_tree.hh -/// \brief Trees representing formulae where atomic propositions are unknown -#ifndef SPOT_LTLAST_FORMULA_TREE_HH -# define SPOT_LTLAST_FORMULA_TREE_HH - -# include "formula.hh" -# include -# include -# include "multop.hh" -# include "binop.hh" -# include "unop.hh" -# include "nfa.hh" - -namespace spot -{ - namespace ltl - { - /// Trees representing formulae where atomic propositions are unknown. - namespace formula_tree - { - // These struct should not need to be made public using - // SPOT_API, unfortunately dynamic_cast<> with g++-4.0.1 fails - // on Darwin if we do not. - struct SPOT_API node - { - virtual ~node() {}; - }; - typedef std::shared_ptr node_ptr; - - struct SPOT_API node_unop : node - { - unop::type op; - node_ptr child; - }; - struct SPOT_API node_binop : node - { - binop::type op; - node_ptr lhs; - node_ptr rhs; - }; - struct SPOT_API node_multop : node - { - multop::type op; - node_ptr lhs; - node_ptr rhs; - }; - struct SPOT_API node_nfa : node - { - std::vector children; - spot::ltl::nfa::ptr nfa; - }; - /// Integer values for True and False used in node_atomic. - enum { True = -1, False = -2 }; - struct SPOT_API node_atomic : node - { - int i; - }; - - /// Instanciate the formula corresponding to the node with - /// atomic propositions taken from \a v. - const formula* instanciate(const node_ptr np, - const std::vector& v); - - /// Get the arity. - size_t arity(const node_ptr np); - } - } -} - -#endif // SPOT_LTLAST_FORMULA_TREE_HH_ diff --git a/src/ltlast/nfa.cc b/src/ltlast/nfa.cc deleted file mode 100644 index 36eca99c4..000000000 --- a/src/ltlast/nfa.cc +++ /dev/null @@ -1,145 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2008, 2013, 2014 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). -// -// 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 -#include "nfa.hh" -#include "formula_tree.hh" - -namespace spot -{ - namespace ltl - { - nfa::nfa() - : is_(), si_(), arity_(0), name_(), init_(0), finals_() - { - } - - nfa::~nfa() - { - is_map::iterator i; - for (i = is_.begin(); i != is_.end(); ++i) - { - state::iterator i2; - for (i2 = i->second->begin(); i2 != i->second->end(); ++i2) - delete *i2; - delete i->second; - } - } - - nfa::state* - nfa::add_state(int name) - { - is_map::iterator i = is_.find(name); - if (i == is_.end()) - { - state* s = new nfa::state; - is_[name] = s; - si_[s] = name; - - if (!init_) - init_ = s; - return s; - } - return i->second; - } - - void - nfa::add_transition(int src, int dst, const label lbl) - { - state* s = add_state(src); - nfa::transition* t = new transition; - t->dst = add_state(dst); - t->lbl = lbl; - s->push_back(t); - size_t arity = formula_tree::arity(formula_tree::node_ptr(lbl)); - if (arity >= arity_) - arity_ = arity; - } - - void - nfa::set_init_state(int name) - { - init_ = add_state(name); - } - - void - nfa::set_final(int name) - { - finals_.insert(name); - } - - bool - nfa::is_final(const state* s) - { - return finals_.find(format_state(s)) != finals_.end(); - } - - bool - nfa::is_loop() - { - return finals_.empty(); - } - - unsigned - nfa::arity() - { - return arity_; - } - - const nfa::state* - nfa::get_init_state() - { - assert(init_); - return init_; - } - - nfa::iterator - nfa::begin(const state* s) const - { - return nfa::iterator(s->begin()); - } - - nfa::iterator - nfa::end(const state* s) const - { - return nfa::iterator(s->end()); - } - - int - nfa::format_state(const state* s) const - { - si_map::const_iterator i = si_.find(s); - assert(i != si_.end()); - return i->second; - } - - const std::string& - nfa::get_name() const - { - return name_; - } - - void - nfa::set_name(const std::string& name) - { - name_ = name; - } - } -} diff --git a/src/ltlast/nfa.hh b/src/ltlast/nfa.hh deleted file mode 100644 index c8097304f..000000000 --- a/src/ltlast/nfa.hh +++ /dev/null @@ -1,155 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2008, 2010, 2013, 2014 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). -// -// 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/nfa.hh -/// \brief NFA interface used by automatop -#ifndef SPOT_LTLAST_NFA_HH -# define SPOT_LTLAST_NFA_HH - -# include "misc/common.hh" -# include "misc/hash.hh" -# include -# include -# include -# include - -namespace spot -{ - namespace ltl - { - /// Forward declaration. See below. - class succ_iterator; - /// Forward declaration. NFA's labels are reprensented by nodes - /// which are defined in formula_tree.hh, included in nfa.cc. - namespace formula_tree - { - struct node; - } - - /// \brief Nondeterministic Finite Automata used by automata operators. - /// - /// States are represented by integers. - /// Labels are represented by formula_tree's nodes. - /// Currently, only one initial state is possible. - class SPOT_API nfa - { - public: - struct transition; - typedef std::list state; - typedef std::shared_ptr label; - /// Iterator over the successors of a state. - typedef succ_iterator iterator; - typedef std::shared_ptr ptr; - - /// Explicit transitions. - struct transition - { - label lbl; - const state* dst; - }; - - nfa(); - ~nfa(); - - void add_transition(int src, int dst, const label lbl); - void set_init_state(int name); - void set_final(int name); - - /// \brief Get the initial state of the NFA. - const state* get_init_state(); - - /// \brief Tell whether the given state is final or not. - bool is_final(const state* s); - - /// \brief Tell whether the NFA is `loop', i.e. without any final state. - bool is_loop(); - - /// \brief Get the `arity' i.e. max t.cost, for each transition t. - unsigned arity(); - - /// \brief Return an iterator on the first succesor (if any) of \a state. - /// - /// The usual way to do this with a \c for loop. - /// \code - /// for (nfa::iterator i = a.begin(s); i != a.end(s); ++i); - /// \endcode - iterator begin(const state* s) const; - - /// \brief Return an iterator just past the last succesor of \a state. - iterator end(const state* s) const; - - int format_state(const state* s) const; - - const std::string& get_name() const; - void set_name(const std::string&); - - private: - state* add_state(int name); - - typedef std::unordered_map> is_map; - typedef std::unordered_map> si_map; - - is_map is_; - si_map si_; - - size_t arity_; - std::string name_; - - state* init_; - std::set finals_; - - /// Explicitly disllow use of implicity generated member functions - /// we don't want. - nfa(const nfa& other); - nfa& operator=(const nfa& other); - }; - - class SPOT_API succ_iterator - { - public: - succ_iterator(const nfa::state::const_iterator s) - : i_(s) - { - } - - void - operator++() - { - ++i_; - } - - bool - operator!=(const succ_iterator& rhs) const - { - return i_ != rhs.i_; - } - - const nfa::transition* operator*() const - { - return *i_; - } - - private: - nfa::state::const_iterator i_; - }; - - } -} - -#endif // SPOT_LTLAST_NFA_HH_ diff --git a/src/ltlast/predecl.hh b/src/ltlast/predecl.hh index 1f746fffe..26359e3e6 100644 --- a/src/ltlast/predecl.hh +++ b/src/ltlast/predecl.hh @@ -1,7 +1,8 @@ -// Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2010, 2012, 2014 Laboratoire de Recherche et +// Développement 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 +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -36,7 +37,6 @@ namespace spot struct visitor; class atomic_prop; - class automatop; class binop; class bunop; class constant; diff --git a/src/ltlast/visitor.hh b/src/ltlast/visitor.hh index 91ac6462e..9f8fbe952 100644 --- a/src/ltlast/visitor.hh +++ b/src/ltlast/visitor.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2012, 2013 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2012, 2013, 2014 Laboratoire de Recherche +// et 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. @@ -46,7 +46,6 @@ namespace spot virtual void visit(const binop* node) = 0; virtual void visit(const unop* node) = 0; virtual void visit(const multop* node) = 0; - virtual void visit(const automatop* node) = 0; virtual void visit(const bunop* node) = 0; }; } diff --git a/src/ltltest/equals.cc b/src/ltltest/equals.cc index f359d2584..b88589330 100644 --- a/src/ltltest/equals.cc +++ b/src/ltltest/equals.cc @@ -195,11 +195,9 @@ main(int argc, char** argv) spot::ltl::unop::dump_instances(std::cerr); spot::ltl::binop::dump_instances(std::cerr); spot::ltl::multop::dump_instances(std::cerr); - spot::ltl::automatop::dump_instances(std::cerr); assert(spot::ltl::atomic_prop::instance_count() == 0); assert(spot::ltl::unop::instance_count() == 0); assert(spot::ltl::binop::instance_count() == 0); assert(spot::ltl::multop::instance_count() == 0); - assert(spot::ltl::automatop::instance_count() == 0); return exit_code; } diff --git a/src/ltltest/ltlrel.cc b/src/ltltest/ltlrel.cc index d97f322ef..a8d9d55e6 100644 --- a/src/ltltest/ltlrel.cc +++ b/src/ltltest/ltlrel.cc @@ -67,11 +67,9 @@ main(int argc, char **argv) spot::ltl::unop::dump_instances(std::cerr); spot::ltl::binop::dump_instances(std::cerr); spot::ltl::multop::dump_instances(std::cerr); - spot::ltl::automatop::dump_instances(std::cerr); assert(spot::ltl::atomic_prop::instance_count() == 0); assert(spot::ltl::unop::instance_count() == 0); assert(spot::ltl::binop::instance_count() == 0); assert(spot::ltl::multop::instance_count() == 0); - assert(spot::ltl::automatop::instance_count() == 0); return 0; } diff --git a/src/ltltest/reduc.cc b/src/ltltest/reduc.cc index 89f884403..ad537f7fe 100644 --- a/src/ltltest/reduc.cc +++ b/src/ltltest/reduc.cc @@ -319,12 +319,9 @@ main(int argc, char** argv) spot::ltl::unop::dump_instances(std::cerr); spot::ltl::binop::dump_instances(std::cerr); spot::ltl::multop::dump_instances(std::cerr); - spot::ltl::automatop::dump_instances(std::cerr); assert(spot::ltl::atomic_prop::instance_count() == 0); assert(spot::ltl::unop::instance_count() == 0); assert(spot::ltl::binop::instance_count() == 0); assert(spot::ltl::multop::instance_count() == 0); - assert(spot::ltl::automatop::instance_count() == 0); - return exit_code; } diff --git a/src/ltlvisit/clone.cc b/src/ltlvisit/clone.cc index 8b4408050..14c5fbdbd 100644 --- a/src/ltlvisit/clone.cc +++ b/src/ltlvisit/clone.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2012, 2013 Laboratoire de Recherche et +// Copyright (C) 2009, 2010, 2012, 2013, 2014 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -74,16 +74,6 @@ namespace spot first, recurse(bo->second())); } - void - clone_visitor::visit(const automatop* ao) - { - automatop::vec* res = new automatop::vec; - unsigned aos = ao->size(); - for (unsigned i = 0; i < aos; ++i) - res->push_back(recurse(ao->nth(i))); - result_ = automatop::instance(ao->get_nfa(), res, ao->is_negated()); - } - void clone_visitor::visit(const multop* mo) { diff --git a/src/ltlvisit/clone.hh b/src/ltlvisit/clone.hh index 5efca2671..da81779d0 100644 --- a/src/ltlvisit/clone.hh +++ b/src/ltlvisit/clone.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2012, 2013 Laboratoire de Recherche et +// Copyright (C) 2009, 2010, 2012, 2013, 2014 Laboratoire de Recherche et // Développement 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 @@ -48,7 +48,6 @@ namespace spot void visit(const atomic_prop* ap); void visit(const unop* uo); void visit(const binop* bo); - void visit(const automatop* mo); void visit(const multop* mo); void visit(const constant* c); void visit(const bunop* c); diff --git a/src/ltlvisit/dotty.cc b/src/ltlvisit/dotty.cc index 4a2bb2c3e..b4cf6cc58 100644 --- a/src/ltlvisit/dotty.cc +++ b/src/ltlvisit/dotty.cc @@ -92,12 +92,6 @@ namespace spot } } - void - visit(const automatop*) - { - SPOT_UNIMPLEMENTED(); - } - void visit(const multop* mo) { diff --git a/src/ltlvisit/lbt.cc b/src/ltlvisit/lbt.cc index 012ae0422..5c54a4dc1 100644 --- a/src/ltlvisit/lbt.cc +++ b/src/ltlvisit/lbt.cc @@ -170,12 +170,6 @@ namespace spot uo->child()->accept(*this); } - void - visit(const automatop*) - { - SPOT_UNIMPLEMENTED(); - } - void visit(const multop* mo) { diff --git a/src/ltlvisit/mark.cc b/src/ltlvisit/mark.cc index 0fc2e3e7a..a4b7384f7 100644 --- a/src/ltlvisit/mark.cc +++ b/src/ltlvisit/mark.cc @@ -77,12 +77,6 @@ namespace spot result_ = uo->clone(); } - void - visit(const automatop* ao) - { - result_ = ao->clone(); - } - void visit(const multop* mo) { @@ -256,12 +250,6 @@ namespace spot SPOT_UNREACHABLE(); } - void - visit(const automatop* ao) - { - result_ = ao->clone(); - } - void visit(const multop* mo) { diff --git a/src/ltlvisit/postfix.cc b/src/ltlvisit/postfix.cc index a9386603a..4fe5f3c13 100644 --- a/src/ltlvisit/postfix.cc +++ b/src/ltlvisit/postfix.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2011, 2012, 2014 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -56,15 +56,6 @@ namespace spot doit(bo); } - void - postfix_visitor::visit(const automatop* ao) - { - unsigned s = ao->size(); - for (unsigned i = 0; i < s; ++i) - ao->nth(i)->accept(*this); - doit(ao); - } - void postfix_visitor::visit(const multop* mo) { @@ -111,12 +102,6 @@ namespace spot doit_default(mo); } - void - postfix_visitor::doit(const automatop* ao) - { - doit_default(ao); - } - void postfix_visitor::doit(const bunop* so) { diff --git a/src/ltlvisit/postfix.hh b/src/ltlvisit/postfix.hh index 860aceccb..6d5eec16c 100644 --- a/src/ltlvisit/postfix.hh +++ b/src/ltlvisit/postfix.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2012, 2013 Laboratoire de Recherche et +// Copyright (C) 2009, 2010, 2012, 2013, 2014 Laboratoire de Recherche et // Développement 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 @@ -46,7 +46,6 @@ namespace spot void visit(const unop* uo); void visit(const binop* bo); void visit(const multop* mo); - void visit(const automatop* c); void visit(const constant* c); void visit(const bunop* c); @@ -54,7 +53,6 @@ namespace spot virtual void doit(const unop* uo); virtual void doit(const binop* bo); virtual void doit(const multop* mo); - virtual void doit(const automatop* mo); virtual void doit(const constant* c); virtual void doit(const bunop* c); virtual void doit_default(const formula* f); diff --git a/src/ltlvisit/relabel.cc b/src/ltlvisit/relabel.cc index a269d1e31..c239c9e3e 100644 --- a/src/ltlvisit/relabel.cc +++ b/src/ltlvisit/relabel.cc @@ -24,6 +24,7 @@ #include "ltlenv/defaultenv.hh" #include "ltlast/allnodes.hh" #include +#include #include #include @@ -287,13 +288,6 @@ namespace spot } } - void - visit(const automatop* ao) - { - for (unsigned i = 0; i < ao->size(); ++i) - recurse(ao->nth(i)); - } - void visit(const multop* mo) { diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc index ce50db590..b18fc8606 100644 --- a/src/ltlvisit/simplify.cc +++ b/src/ltlvisit/simplify.cc @@ -250,7 +250,6 @@ namespace spot break; } case formula::BUnOp: - case formula::AutomatOp: SPOT_UNIMPLEMENTED(); break; } @@ -630,18 +629,6 @@ namespace spot SPOT_UNREACHABLE(); } - void - visit(const automatop* ao) - { - bool negated = negated_; - negated_ = false; - automatop::vec* res = new automatop::vec; - unsigned aos = ao->size(); - for (unsigned i = 0; i < aos; ++i) - res->push_back(recurse(ao->nth(i))); - result_ = automatop::instance(ao->get_nfa(), res, negated); - } - void visit(const multop* mo) { @@ -2747,12 +2734,6 @@ namespace spot result_ = binop::instance(op, a, b); } - void - visit(const automatop* aut) - { - result_ = aut->clone(); - } - void visit(const multop* mo) { @@ -4302,7 +4283,6 @@ namespace spot case formula::Constant: case formula::AtomicProp: case formula::BUnOp: - case formula::AutomatOp: break; case formula::UnOp: @@ -4524,7 +4504,6 @@ namespace spot case formula::Constant: case formula::AtomicProp: case formula::BUnOp: - case formula::AutomatOp: break; case formula::UnOp: diff --git a/src/ltlvisit/snf.cc b/src/ltlvisit/snf.cc index 43555e749..624237a6c 100644 --- a/src/ltlvisit/snf.cc +++ b/src/ltlvisit/snf.cc @@ -85,12 +85,6 @@ namespace spot SPOT_UNIMPLEMENTED(); } - void - visit(const automatop*) - { - SPOT_UNIMPLEMENTED(); - } - void visit(const multop* mo) { diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc index d17776a58..5a1170df0 100644 --- a/src/ltlvisit/tostring.cc +++ b/src/ltlvisit/tostring.cc @@ -723,28 +723,6 @@ namespace spot os_ << "Ì…"; } - void - visit(const automatop* ao) - { - // Warning: this string isn't parsable because the automaton - // operators used may not be defined. - bool top_level = top_level_; - top_level_ = false; - if (!top_level) - os_ << '('; - os_ << ao->get_nfa()->get_name() << '('; - unsigned max = ao->size(); - ao->nth(0)->accept(*this); - for (unsigned n = 1; n < max; ++n) - { - os_ << ','; - ao->nth(n)->accept(*this); - } - os_ << ')'; - if (!top_level) - os_ << ')'; - } - void resugar_concat(const multop* mo) { diff --git a/src/tgba/formula2bdd.cc b/src/tgba/formula2bdd.cc index b6a29e6aa..0a2845286 100644 --- a/src/tgba/formula2bdd.cc +++ b/src/tgba/formula2bdd.cc @@ -125,12 +125,6 @@ namespace spot SPOT_UNREACHABLE(); } - virtual void - visit(const automatop*) - { - SPOT_UNIMPLEMENTED(); - } - virtual void visit(const multop* node) { diff --git a/src/tgbaalgos/ltl2taa.cc b/src/tgbaalgos/ltl2taa.cc index c67a24b1f..56f940b99 100644 --- a/src/tgbaalgos/ltl2taa.cc +++ b/src/tgbaalgos/ltl2taa.cc @@ -334,12 +334,6 @@ namespace spot SPOT_UNREACHABLE(); } - void - visit(const automatop*) - { - SPOT_UNIMPLEMENTED(); - } - ltl2taa_visitor recurse(const formula* f) { diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index b5848ef99..e0580458a 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -732,12 +732,6 @@ namespace spot SPOT_UNREACHABLE(); // Not a rational operator } - void - visit(const automatop*) - { - SPOT_UNREACHABLE(); // Not a rational operator - } - void visit(const multop* node) { @@ -1640,12 +1634,6 @@ namespace spot } } - void - visit(const automatop*) - { - SPOT_UNIMPLEMENTED(); - } - void visit(const multop* node) { @@ -1833,12 +1821,6 @@ namespace spot SPOT_UNREACHABLE(); } - void - visit(const automatop*) - { - SPOT_UNIMPLEMENTED(); - } - void visit(const bunop*) { diff --git a/src/tgbaalgos/ltl2tgba_lacim.cc b/src/tgbaalgos/ltl2tgba_lacim.cc index b4dda91b5..356feddfa 100644 --- a/src/tgbaalgos/ltl2tgba_lacim.cc +++ b/src/tgbaalgos/ltl2tgba_lacim.cc @@ -233,12 +233,6 @@ namespace spot SPOT_UNREACHABLE(); } - void - visit(const automatop*) - { - SPOT_UNIMPLEMENTED(); - } - void visit(const multop* node) { diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 5108df74c..85bf6f755 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -2035,12 +2035,10 @@ main(int argc, char** argv) spot::ltl::unop::dump_instances(std::cerr); spot::ltl::binop::dump_instances(std::cerr); spot::ltl::multop::dump_instances(std::cerr); - spot::ltl::automatop::dump_instances(std::cerr); assert(spot::ltl::atomic_prop::instance_count() == 0); assert(spot::ltl::unop::instance_count() == 0); assert(spot::ltl::binop::instance_count() == 0); assert(spot::ltl::multop::instance_count() == 0); - assert(spot::ltl::automatop::instance_count() == 0); delete dict; return exit_code; }