diff --git a/src/ltlvisit/Makefile.am b/src/ltlvisit/Makefile.am index a5572a827..1e32b7c3d 100644 --- a/src/ltlvisit/Makefile.am +++ b/src/ltlvisit/Makefile.am @@ -1,6 +1,6 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et -## Developpement de l'Epita (LRDE). +## Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche +## et Developpement de l'Epita (LRDE). ## Copyright (C) 2004, 2005, 2006 Laboratoire d'Informatique de Paris ## 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), ## Université Pierre et Marie Curie. @@ -29,7 +29,6 @@ ltlvisit_HEADERS = \ apcollect.hh \ contain.hh \ clone.hh \ - destroy.hh \ dotty.hh \ dump.hh \ lbt.hh \ @@ -38,7 +37,6 @@ ltlvisit_HEADERS = \ nenoform.hh \ postfix.hh \ randomltl.hh \ - reduce.hh \ relabel.hh \ remove_x.hh \ simpfg.hh \ @@ -53,7 +51,6 @@ libltlvisit_la_SOURCES = \ apcollect.cc \ contain.cc \ clone.cc \ - destroy.cc \ dotty.cc \ dump.cc \ lbt.cc \ @@ -64,7 +61,6 @@ libltlvisit_la_SOURCES = \ nenoform.cc \ postfix.cc \ randomltl.cc \ - reduce.cc \ relabel.cc \ remove_x.cc \ simpfg.cc \ diff --git a/src/ltlvisit/clone.cc b/src/ltlvisit/clone.cc index 14c5fbdbd..74650a831 100644 --- a/src/ltlvisit/clone.cc +++ b/src/ltlvisit/clone.cc @@ -91,11 +91,5 @@ namespace spot f->accept(*this); return result_; } - - const formula* - clone(const formula* f) - { - return f->clone(); - } } } diff --git a/src/ltlvisit/clone.hh b/src/ltlvisit/clone.hh index da81779d0..96a50fe95 100644 --- a/src/ltlvisit/clone.hh +++ b/src/ltlvisit/clone.hh @@ -57,12 +57,6 @@ namespace spot protected: const formula* result_; }; - - /// \ingroup ltl_essential - /// \brief Clone a formula. - /// \deprecated Use f->clone() instead. - SPOT_API SPOT_DEPRECATED - const formula* clone(const formula* f) __attribute__ ((deprecated)); } } diff --git a/src/ltlvisit/contain.hh b/src/ltlvisit/contain.hh index e2fab0cf4..7376aa6e0 100644 --- a/src/ltlvisit/contain.hh +++ b/src/ltlvisit/contain.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012, 2013 Laboratoire de Recherche et +// Copyright (C) 2011, 2012, 2013, 2014 Laboratoire de Recherche et // Developpement de l'Epita (LRDE). // Copyright (C) 2006 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -80,36 +80,6 @@ namespace spot /* Translation Maps */ trans_map translated_; }; - - /// \brief Reduce a formula using language containment relationships. - /// - /// The method is taken from table 4.1 in - /** \verbatim - @TechReport{ tauriainen.03.a83, - author = {Heikki Tauriainen}, - title = {On Translating Linear Temporal Logic into Alternating and - Nondeterministic Automata}, - institution = {Helsinki University of Technology, Laboratory for - Theoretical Computer Science}, - address = {Espoo, Finland}, - month = dec, - number = {A83}, - pages = {132}, - type = {Research Report}, - year = {2003}, - note = {Reprint of Licentiate's thesis} - } - \endverbatim */ - /// - /// (The "dagged" cells in the tables are not handled here.) - /// - /// If \a stronger is set, additional rules are used to further - /// reduce some U, R, and X usages. - /// - /// \deprecated Use spot::ltl::ltl_simplifier instead. - SPOT_API SPOT_DEPRECATED - const formula* reduce_tau03(const formula* f, - bool stronger = true); } } diff --git a/src/ltlvisit/destroy.cc b/src/ltlvisit/destroy.cc deleted file mode 100644 index 0094990ed..000000000 --- a/src/ltlvisit/destroy.cc +++ /dev/null @@ -1,34 +0,0 @@ -// Copyright (C) 2009 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. -// -// 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 "ltlvisit/destroy.hh" - -namespace spot -{ - namespace ltl - { - void - destroy(const formula* f) - { - f->destroy(); - } - } -} diff --git a/src/ltlvisit/destroy.hh b/src/ltlvisit/destroy.hh deleted file mode 100644 index caf688d4c..000000000 --- a/src/ltlvisit/destroy.hh +++ /dev/null @@ -1,41 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2009, 2013 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. -// -// 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 . - -#ifndef SPOT_LTLVISIT_DESTROY_HH -# define SPOT_LTLVISIT_DESTROY_HH - -# include "misc/common.hh" -# include "ltlvisit/postfix.hh" - -namespace spot -{ - namespace ltl - { - /// \ingroup ltl_essential - /// \brief Destroys a formula - /// \deprecated Use f->destroy() instead. - SPOT_API SPOT_DEPRECATED - void destroy(const formula *f); - } -} - -#endif // SPOT_LTLVISIT_DESTROY_HH diff --git a/src/ltlvisit/reduce.cc b/src/ltlvisit/reduce.cc deleted file mode 100644 index 0087f558f..000000000 --- a/src/ltlvisit/reduce.cc +++ /dev/null @@ -1,56 +0,0 @@ -// Copyright (C) 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). -// Copyright (C) 2004, 2006, 2007 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 -#include "simplify.hh" -#define SKIP_DEPRECATED_WARNING -#include "reduce.hh" - -namespace spot -{ - namespace ltl - { - const formula* - reduce(const formula* f, int opt) - { - ltl_simplifier_options o; - o.reduce_basics = opt & Reduce_Basics; - o.synt_impl = opt & Reduce_Syntactic_Implications; - o.event_univ = opt & Reduce_Eventuality_And_Universality; - o.containment_checks = opt & Reduce_Containment_Checks; - o.containment_checks_stronger = opt & Reduce_Containment_Checks_Stronger; - ltl_simplifier simplifier(o); - return simplifier.simplify(f); - } - - bool - is_eventual(const formula* f) - { - return f->is_eventual(); - } - - bool - is_universal(const formula* f) - { - return f->is_universal(); - } - } -} diff --git a/src/ltlvisit/reduce.hh b/src/ltlvisit/reduce.hh deleted file mode 100644 index 4093178be..000000000 --- a/src/ltlvisit/reduce.hh +++ /dev/null @@ -1,129 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). -// Copyright (C) 2004, 2006 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 . - -#ifndef SPOT_LTLVISIT_REDUCE_HH -# define SPOT_LTLVISIT_REDUCE_HH - -#include "ltlast/formula.hh" -#include "ltlast/visitor.hh" - -#if __GNUC__ -#ifndef SKIP_DEPRECATED_WARNING -#warning This file and its functions are deprecated. \ - The functionality moved to ltlvisit/simplify.hh -#endif -#endif - -namespace spot -{ - namespace ltl - { - - /// \addtogroup ltl_rewriting - /// @{ - - /// Options for spot::ltl::reduce. - enum reduce_options - { - /// No reduction. - Reduce_None = 0, - /// Basic reductions. - Reduce_Basics = 1, - /// Somenzi & Bloem syntactic implication. - Reduce_Syntactic_Implications = 2, - /// Etessami & Holzmann eventuality and universality reductions. - Reduce_Eventuality_And_Universality = 4, - /// Tauriainen containment checks. - Reduce_Containment_Checks = 8, - /// Tauriainen containment checks (stronger version). - Reduce_Containment_Checks_Stronger = 16, - /// All reductions. - Reduce_All = -1U - }; - - /// \brief Reduce a formula \a f. - /// - /// \param f the formula to reduce - /// \param opt a conjonction of spot::ltl::reduce_options specifying - /// which optimizations to apply. - /// \return the reduced formula - /// - /// \deprecated Use spot::ltl::ltl_simplifier instead. - SPOT_API SPOT_DEPRECATED const formula* - reduce(const formula* f, int opt = Reduce_All); - /// @} - - /// \ingroup ltl_misc - /// \brief Check whether a formula is a pure eventuality. - /// - /// Pure eventuality formulae are defined in - /** \verbatim - @InProceedings{ etessami.00.concur, - author = {Kousha Etessami and Gerard J. Holzmann}, - title = {Optimizing {B\"u}chi Automata}, - booktitle = {Proceedings of the 11th International Conference on - Concurrency Theory (Concur'2000)}, - pages = {153--167}, - year = {2000}, - editor = {C. Palamidessi}, - volume = {1877}, - series = {Lecture Notes in Computer Science}, - publisher = {Springer-Verlag} - } - \endverbatim */ - /// - /// A word that satisfies a pure eventuality can be prefixed by - /// anything and still satisfies the formula. - /// - /// \deprecated Use f->is_eventual() instead. - SPOT_API SPOT_DEPRECATED - bool is_eventual(const formula* f); - - /// \ingroup ltl_misc - /// \brief Check whether a formula is purely universal. - /// - /// Purely universal formulae are defined in - /** \verbatim - @InProceedings{ etessami.00.concur, - author = {Kousha Etessami and Gerard J. Holzmann}, - title = {Optimizing {B\"u}chi Automata}, - booktitle = {Proceedings of the 11th International Conference on - Concurrency Theory (Concur'2000)}, - pages = {153--167}, - year = {2000}, - editor = {C. Palamidessi}, - volume = {1877}, - series = {Lecture Notes in Computer Science}, - publisher = {Springer-Verlag} - } - \endverbatim */ - /// - /// Any (non-empty) suffix of a word that satisfies if purely - /// universal formula also satisfies the formula. - /// - /// \deprecated Use f->is_universal() instead. - SPOT_API SPOT_DEPRECATED - bool is_universal(const formula* f); - } -} - -#endif // SPOT_LTLVISIT_REDUCE_HH