Remove deprecated algorithms.
* src/ltlvisit/destroy.cc, src/ltlvisit/destroy.hh, src/ltlvisit/reduce.cc, src/ltlvisit/reduce.hh: Delete. * src/ltlvisit/Makefile.am: Adjust. * src/ltlvisit/clone.cc, src/ltlvisit/clone.hh (clone): Remove. * src/ltlvisit/contain.hh (reduce_tau03): Remove.
This commit is contained in:
Alexandre Duret-Lutz
parent
e6ea90e326
commit
a63612a515
8 changed files with 3 additions and 309 deletions
|
|
@ -1,6 +1,6 @@
|
||||||
## -*- coding: utf-8 -*-
|
## -*- coding: utf-8 -*-
|
||||||
## Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et
|
## Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche
|
||||||
## Developpement de l'Epita (LRDE).
|
## et Developpement de l'Epita (LRDE).
|
||||||
## Copyright (C) 2004, 2005, 2006 Laboratoire d'Informatique de Paris
|
## Copyright (C) 2004, 2005, 2006 Laboratoire d'Informatique de Paris
|
||||||
## 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
|
## 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
|
||||||
## Université Pierre et Marie Curie.
|
## Université Pierre et Marie Curie.
|
||||||
|
|
@ -29,7 +29,6 @@ ltlvisit_HEADERS = \
|
||||||
apcollect.hh \
|
apcollect.hh \
|
||||||
contain.hh \
|
contain.hh \
|
||||||
clone.hh \
|
clone.hh \
|
||||||
destroy.hh \
|
|
||||||
dotty.hh \
|
dotty.hh \
|
||||||
dump.hh \
|
dump.hh \
|
||||||
lbt.hh \
|
lbt.hh \
|
||||||
|
|
@ -38,7 +37,6 @@ ltlvisit_HEADERS = \
|
||||||
nenoform.hh \
|
nenoform.hh \
|
||||||
postfix.hh \
|
postfix.hh \
|
||||||
randomltl.hh \
|
randomltl.hh \
|
||||||
reduce.hh \
|
|
||||||
relabel.hh \
|
relabel.hh \
|
||||||
remove_x.hh \
|
remove_x.hh \
|
||||||
simpfg.hh \
|
simpfg.hh \
|
||||||
|
|
@ -53,7 +51,6 @@ libltlvisit_la_SOURCES = \
|
||||||
apcollect.cc \
|
apcollect.cc \
|
||||||
contain.cc \
|
contain.cc \
|
||||||
clone.cc \
|
clone.cc \
|
||||||
destroy.cc \
|
|
||||||
dotty.cc \
|
dotty.cc \
|
||||||
dump.cc \
|
dump.cc \
|
||||||
lbt.cc \
|
lbt.cc \
|
||||||
|
|
@ -64,7 +61,6 @@ libltlvisit_la_SOURCES = \
|
||||||
nenoform.cc \
|
nenoform.cc \
|
||||||
postfix.cc \
|
postfix.cc \
|
||||||
randomltl.cc \
|
randomltl.cc \
|
||||||
reduce.cc \
|
|
||||||
relabel.cc \
|
relabel.cc \
|
||||||
remove_x.cc \
|
remove_x.cc \
|
||||||
simpfg.cc \
|
simpfg.cc \
|
||||||
|
|
|
||||||
|
|
@ -91,11 +91,5 @@ namespace spot
|
||||||
f->accept(*this);
|
f->accept(*this);
|
||||||
return result_;
|
return result_;
|
||||||
}
|
}
|
||||||
|
|
||||||
const formula*
|
|
||||||
clone(const formula* f)
|
|
||||||
{
|
|
||||||
return f->clone();
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -57,12 +57,6 @@ namespace spot
|
||||||
protected:
|
protected:
|
||||||
const formula* result_;
|
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));
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- 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).
|
// Developpement de l'Epita (LRDE).
|
||||||
// Copyright (C) 2006 Laboratoire d'Informatique de Paris 6 (LIP6),
|
// Copyright (C) 2006 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
|
||||||
|
|
@ -80,36 +80,6 @@ namespace spot
|
||||||
/* Translation Maps */
|
/* Translation Maps */
|
||||||
trans_map translated_;
|
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);
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -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 <http://www.gnu.org/licenses/>.
|
|
||||||
|
|
||||||
#include "ltlvisit/destroy.hh"
|
|
||||||
|
|
||||||
namespace spot
|
|
||||||
{
|
|
||||||
namespace ltl
|
|
||||||
{
|
|
||||||
void
|
|
||||||
destroy(const formula* f)
|
|
||||||
{
|
|
||||||
f->destroy();
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
@ -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 <http://www.gnu.org/licenses/>.
|
|
||||||
|
|
||||||
#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
|
|
||||||
|
|
@ -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 <http://www.gnu.org/licenses/>.
|
|
||||||
|
|
||||||
#include <cassert>
|
|
||||||
#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();
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
@ -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 <http://www.gnu.org/licenses/>.
|
|
||||||
|
|
||||||
#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
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue