From 25a31142871bf29b64f4d3db96c58b05c4dd7f4f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 12 Jun 2008 16:31:59 +0200 Subject: [PATCH] Merge all ltlast/ files into formula.hh. The forward declaration of visitor was causing error messages too cryptic for users. --- ChangeLog | 30 +++++++++++++ src/ltlast/Makefile.am | 13 +----- src/ltlast/allnodes.hh | 35 --------------- src/ltlast/atomic_prop.hh | 42 ------------------ src/ltlast/binop.hh | 45 ------------------- src/ltlast/constant.hh | 42 ------------------ src/ltlast/formula.hh | 69 ++++++++++++++++++++++++++++- src/ltlast/multop.hh | 44 ------------------- src/ltlast/refformula.hh | 42 ------------------ src/ltlast/unop.hh | 42 ------------------ src/ltlast/visitor.hh | 77 --------------------------------- src/ltlparse/ltlparse.yy | 3 +- src/ltlparse/public.hh | 1 - src/ltltest/equals.cc | 1 - src/ltltest/randltl.cc | 1 - src/ltltest/readltl.cc | 1 - src/ltltest/reduc.cc | 1 - src/ltltest/syntimpl.cc | 1 - src/ltltest/tostring.cc | 1 - src/ltlvisit/apcollect.hh | 4 +- src/ltlvisit/basicreduce.cc | 2 - src/ltlvisit/clone.cc | 3 +- src/ltlvisit/clone.hh | 3 +- src/ltlvisit/contain.cc | 6 +-- src/ltlvisit/dotty.cc | 4 +- src/ltlvisit/dump.cc | 8 ++-- src/ltlvisit/lunabbrev.cc | 3 +- src/ltlvisit/nenoform.cc | 5 +-- src/ltlvisit/nenoform.hh | 3 +- src/ltlvisit/postfix.cc | 3 +- src/ltlvisit/postfix.hh | 3 +- src/ltlvisit/randomltl.cc | 2 - src/ltlvisit/reduce.cc | 1 - src/ltlvisit/reduce.hh | 3 +- src/ltlvisit/simpfg.cc | 4 +- src/ltlvisit/syntimpl.cc | 3 +- src/ltlvisit/tostring.cc | 3 -- src/ltlvisit/tunabbrev.cc | 3 +- src/tgba/bdddict.cc | 3 +- src/tgba/formula2bdd.cc | 4 +- src/tgba/tgbaexplicit.cc | 4 +- src/tgba/tgbatba.cc | 4 +- src/tgbaalgos/ltl2tgba_fm.cc | 2 - src/tgbaalgos/ltl2tgba_lacim.cc | 4 +- src/tgbaalgos/randomgraph.cc | 1 - src/tgbaalgos/randomgraph.hh | 1 - src/tgbaalgos/save.cc | 7 ++- src/tgbaparse/public.hh | 1 - src/tgbaparse/tgbaparse.yy | 3 +- src/tgbatest/explicit.cc | 5 +-- src/tgbatest/explprod.cc | 2 +- src/tgbatest/ltl2tgba.cc | 1 - src/tgbatest/ltlprod.cc | 1 - src/tgbatest/mixprod.cc | 1 - src/tgbatest/powerset.cc | 1 - src/tgbatest/randtgba.cc | 1 - src/tgbatest/readsave.cc | 1 - src/tgbatest/reductgba.cc | 1 - src/tgbatest/tgbaread.cc | 1 - src/tgbatest/tripprod.cc | 1 - 60 files changed, 132 insertions(+), 475 deletions(-) delete mode 100644 src/ltlast/allnodes.hh delete mode 100644 src/ltlast/atomic_prop.hh delete mode 100644 src/ltlast/binop.hh delete mode 100644 src/ltlast/constant.hh delete mode 100644 src/ltlast/multop.hh delete mode 100644 src/ltlast/refformula.hh delete mode 100644 src/ltlast/unop.hh delete mode 100644 src/ltlast/visitor.hh diff --git a/ChangeLog b/ChangeLog index 8ed9ae254..cf0d79a67 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,33 @@ +2008-06-12 Alexandre Duret-Lutz + + Merge all ltlast/ files into formula.hh. The forward declaration + of visitor was causing error messages too cryptic for users. + + * src/ltlast/allnodes.hh, src/ltlast/atomic_prop.hh, + src/ltlast/binop.hh, src/ltlast/constant.hh, src/ltlast/multop.hh, + src/ltlast/refformula.hh, src/ltlast/unop.hh, + src/ltlast/visitor.hh: Delete and merge all these files into ... + * src/ltlast/formula.hh: ... this one. + * src/ltlast/Makefile.am: Adjust. + * ltlparse/ltlparse.yy, ltlparse/public.hh, ltltest/equals.cc, + ltltest/randltl.cc, ltltest/readltl.cc, ltltest/reduc.cc, + ltltest/syntimpl.cc, ltltest/tostring.cc, ltlvisit/apcollect.hh, + ltlvisit/basicreduce.cc, ltlvisit/clone.cc, ltlvisit/clone.hh, + ltlvisit/contain.cc, ltlvisit/dotty.cc, ltlvisit/dump.cc, + ltlvisit/lunabbrev.cc, ltlvisit/nenoform.cc, ltlvisit/nenoform.hh, + ltlvisit/postfix.cc, ltlvisit/postfix.hh, ltlvisit/randomltl.cc, + ltlvisit/reduce.cc, ltlvisit/reduce.hh, ltlvisit/simpfg.cc, + ltlvisit/syntimpl.cc, ltlvisit/tostring.cc, ltlvisit/tunabbrev.cc, + tgba/bdddict.cc, tgba/formula2bdd.cc, tgba/tgbaexplicit.cc, + tgba/tgbatba.cc, tgbaalgos/ltl2tgba_fm.cc, + tgbaalgos/ltl2tgba_lacim.cc, tgbaalgos/randomgraph.cc, + tgbaalgos/randomgraph.hh, tgbaalgos/save.cc, tgbaparse/public.hh, + tgbaparse/tgbaparse.yy, tgbatest/explicit.cc, + tgbatest/explprod.cc, tgbatest/ltl2tgba.cc, tgbatest/ltlprod.cc, + tgbatest/mixprod.cc, tgbatest/powerset.cc, tgbatest/randtgba.cc, + tgbatest/readsave.cc, tgbatest/reductgba.cc, tgbatest/tgbaread.cc, + tgbatest/tripprod.cc: Adjust includes. + 2008-06-12 Alexandre Duret-Lutz * src/ltlast/atomic_prop.cc, src/ltlast/binop.cc, diff --git a/src/ltlast/Makefile.am b/src/ltlast/Makefile.am index 964d070a8..5e595a9ac 100644 --- a/src/ltlast/Makefile.am +++ b/src/ltlast/Makefile.am @@ -1,4 +1,4 @@ -## Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +## Copyright (C) 2003, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), ## département Systèmes Répartis Coopératifs (SRC), Université Pierre ## et Marie Curie. ## @@ -21,13 +21,4 @@ ltlastdir = $(pkgincludedir)/ltlast -ltlast_HEADERS = \ - allnodes.hh \ - atomic_prop.hh \ - binop.hh \ - constant.hh \ - formula.hh \ - multop.hh \ - refformula.hh \ - unop.hh \ - visitor.hh +ltlast_HEADERS = formula.hh diff --git a/src/ltlast/allnodes.hh b/src/ltlast/allnodes.hh deleted file mode 100644 index 53d76103f..000000000 --- a/src/ltlast/allnodes.hh +++ /dev/null @@ -1,35 +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/allnodes.hh -/// \brief Define all LTL node types. -/// -/// This file is usually needed when \b defining a visitor. -#ifndef SPOT_LTLAST_ALLNODES_HH -# define SPOT_LTLAST_ALLNODES_HH - -# include "binop.hh" -# include "unop.hh" -# include "multop.hh" -# include "atomic_prop.hh" -# include "constant.hh" - -#endif // SPOT_LTLAST_ALLNODES_HH diff --git a/src/ltlast/atomic_prop.hh b/src/ltlast/atomic_prop.hh deleted file mode 100644 index e42db59df..000000000 --- a/src/ltlast/atomic_prop.hh +++ /dev/null @@ -1,42 +0,0 @@ -// Copyright (C) 2008 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/atomic_prop.hh -/// \brief LTL atomic propositions -#ifndef SPOT_LTLAST_ATOMIC_PROP_HH -# define SPOT_LTLAST_ATOMIC_PROP_HH - -# include "formula.hh" -# include "internal/atomic_prop.hh" - -namespace spot -{ - namespace ltl - { - - /// \brief Atomic propositions. - /// \ingroup ltl_ast - typedef spot::internal::atomic_prop atomic_prop; - - } -} - -#endif // SPOT_LTLAST_ATOMICPROP_HH diff --git a/src/ltlast/binop.hh b/src/ltlast/binop.hh deleted file mode 100644 index c44a5af73..000000000 --- a/src/ltlast/binop.hh +++ /dev/null @@ -1,45 +0,0 @@ -// Copyright (C) 2008 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/binop.hh -/// \brief LTL binary operators -/// -/// This does not include \c AND and \c OR operators. These are -/// considered to be multi-operand operators (see spot::ltl::multop). -#ifndef SPOT_LTLAST_BINOP_HH -# define SPOT_LTLAST_BINOP_HH - -# include "formula.hh" -# include "internal/binop.hh" - -namespace spot -{ - namespace ltl - { - - /// \brief Binary operator. - /// \ingroup ltl_ast - typedef spot::internal::binop binop; - - } -} - -#endif // SPOT_LTLAST_BINOP_HH diff --git a/src/ltlast/constant.hh b/src/ltlast/constant.hh deleted file mode 100644 index 1c4dc6750..000000000 --- a/src/ltlast/constant.hh +++ /dev/null @@ -1,42 +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/constant.hh -/// \brief LTL constants -#ifndef SPOT_LTLAST_CONSTANT_HH -# define SPOT_LTLAST_CONSTANT_HH - -# include "formula.hh" -# include "internal/constant.hh" - -namespace spot -{ - namespace ltl - { - - /// \brief A constant (True or False) - /// \ingroup ltl_ast - typedef spot::internal::constant constant; - - } -} - -#endif // SPOT_LTLAST_CONSTANT_HH diff --git a/src/ltlast/formula.hh b/src/ltlast/formula.hh index 7ef933c40..8c40ad4ad 100644 --- a/src/ltlast/formula.hh +++ b/src/ltlast/formula.hh @@ -20,11 +20,16 @@ // 02111-1307, USA. /// \file ltlast/formula.hh -/// \brief LTL formula interface +/// \brief LTL formula, AST and visitor interface #ifndef SPOT_LTLAST_FORMULA_HH # define SPOT_LTLAST_FORMULA_HH # include "internal/formula.hh" +# include "internal/atomic_prop.hh" +# include "internal/constant.hh" +# include "internal/unop.hh" +# include "internal/binop.hh" +# include "internal/multop.hh" namespace spot { @@ -118,6 +123,68 @@ namespace spot typedef spot::internal::formula_ptr_less_than formula_ptr_less_than; typedef spot::internal::formula_ptr_hash formula_ptr_hash; + + + + /// \brief Atomic propositions. + /// \ingroup ltl_ast + typedef spot::internal::atomic_prop atomic_prop; + + /// \brief A constant (True or False) + /// \ingroup ltl_ast + typedef spot::internal::constant constant; + + /// \brief Unary operators. + /// \ingroup ltl_ast + typedef spot::internal::unop unop; + + /// \brief Binary operator. + /// \ingroup ltl_ast + typedef spot::internal::binop binop; + + /// \brief Multi-operand operators. + /// \ingroup ltl_ast + /// + /// These operators are considered commutative and associative. + typedef spot::internal::multop multop; + + + /// \brief Formula visitor that can modify the formula. + /// \ingroup ltl_essential + /// + /// Writing visitors is the prefered way + /// to traverse a formula, since it doesn't + /// involve any cast. + /// + /// If you do not need to modify the visited formula, inherit from + /// spot::ltl:const_visitor instead. + struct visitor + { + virtual ~visitor() {} + virtual void visit(atomic_prop* node) = 0; + virtual void visit(constant* node) = 0; + virtual void visit(binop* node) = 0; + virtual void visit(unop* node) = 0; + virtual void visit(multop* node) = 0; + }; + + /// \brief Formula visitor that cannot modify the formula. + /// + /// Writing visitors is the prefered way + /// to traverse a formula, since it doesn't + /// involve any cast. + /// + /// If you want to modify the visited formula, inherit from + /// spot::ltl:visitor instead. + struct const_visitor + { + virtual ~const_visitor() {} + virtual void visit(const atomic_prop* node) = 0; + virtual void visit(const constant* node) = 0; + virtual void visit(const binop* node) = 0; + virtual void visit(const unop* node) = 0; + virtual void visit(const multop* node) = 0; + }; } } diff --git a/src/ltlast/multop.hh b/src/ltlast/multop.hh deleted file mode 100644 index b662e00de..000000000 --- a/src/ltlast/multop.hh +++ /dev/null @@ -1,44 +0,0 @@ -// Copyright (C) 2008 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/multop.hh -/// \brief LTL multi-operand operators -#ifndef SPOT_LTLAST_MULTOP_HH -# define SPOT_LTLAST_MULTOP_HH - -# include "formula.hh" -# include "internal/multop.hh" - -namespace spot -{ - namespace ltl - { - - /// \brief Multi-operand operators. - /// \ingroup ltl_ast - /// - /// These operators are considered commutative and associative. - typedef spot::internal::multop multop; - - } -} - -#endif // SPOT_LTLAST_MULTOP_HH diff --git a/src/ltlast/refformula.hh b/src/ltlast/refformula.hh deleted file mode 100644 index b9dedf9c8..000000000 --- a/src/ltlast/refformula.hh +++ /dev/null @@ -1,42 +0,0 @@ -// Copyright (C) 2008 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/refformula.hh -/// \brief Reference-counted LTL formulae -#ifndef SPOT_LTLAST_REFFORMULA_HH -# define SPOT_LTLAST_REFFORMULA_HH - -# include "formula.hh" -# include "internal/refformula.hh" - -namespace spot -{ - namespace ltl - { - - /// \brief A reference-counted LTL formula. - /// \ingroup ltl_ast - typedef spot::internal::ref_formula ref_formula; - - } -} - -#endif // SPOT_LTLAST_REFFORMULA_HH diff --git a/src/ltlast/unop.hh b/src/ltlast/unop.hh deleted file mode 100644 index 4fe31a392..000000000 --- a/src/ltlast/unop.hh +++ /dev/null @@ -1,42 +0,0 @@ -// Copyright (C) 2008 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/unop.hh -/// \brief LTL unary operators -#ifndef SPOT_LTLAST_UNOP_HH -# define SPOT_LTLAST_UNOP_HH - -# include "formula.hh" -# include "internal/unop.hh" - -namespace spot -{ - namespace ltl - { - - /// \brief Unary operators. - /// \ingroup ltl_ast - typedef spot::internal::unop unop; - - } -} - -#endif // SPOT_LTLAST_UNOP_HH diff --git a/src/ltlast/visitor.hh b/src/ltlast/visitor.hh deleted file mode 100644 index 1a2785ab5..000000000 --- a/src/ltlast/visitor.hh +++ /dev/null @@ -1,77 +0,0 @@ -// Copyright (C) 2003, 2004, 2005, 2008 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/visitor.hh -/// \brief LTL visitor interface -#ifndef SPOT_LTLAST_VISITOR_HH -# define SPOT_LTLAST_VISITOR_HH - -# include "binop.hh" -# include "unop.hh" -# include "multop.hh" -# include "atomic_prop.hh" -# include "constant.hh" - -namespace spot -{ - namespace ltl - { - /// \brief Formula visitor that can modify the formula. - /// \ingroup ltl_essential - /// - /// Writing visitors is the prefered way - /// to traverse a formula, since it doesn't - /// involve any cast. - /// - /// If you do not need to modify the visited formula, inherit from - /// spot::ltl:const_visitor instead. - struct visitor - { - virtual ~visitor() {} - virtual void visit(atomic_prop* node) = 0; - virtual void visit(constant* node) = 0; - virtual void visit(binop* node) = 0; - virtual void visit(unop* node) = 0; - virtual void visit(multop* node) = 0; - }; - - /// \brief Formula visitor that cannot modify the formula. - /// - /// Writing visitors is the prefered way - /// to traverse a formula, since it doesn't - /// involve any cast. - /// - /// If you want to modify the visited formula, inherit from - /// spot::ltl:visitor instead. - struct const_visitor - { - virtual ~const_visitor() {} - virtual void visit(const atomic_prop* node) = 0; - virtual void visit(const constant* node) = 0; - virtual void visit(const binop* node) = 0; - virtual void visit(const unop* node) = 0; - virtual void visit(const multop* node) = 0; - }; - - } -} - -#endif // SPOT_LTLAST_VISITOR_HH diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy index ce74666d0..98e7abbcf 100644 --- a/src/ltlparse/ltlparse.yy +++ b/src/ltlparse/ltlparse.yy @@ -1,4 +1,4 @@ -/* Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de +/* Copyright (C) 2003, 2004, 2005, 2006, 2008 Laboratoire d'Informatique de ** Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), ** Université Pierre et Marie Curie. ** @@ -22,7 +22,6 @@ %{ #include #include "public.hh" -#include "ltlast/allnodes.hh" #include "ltlvisit/destroy.hh" %} diff --git a/src/ltlparse/public.hh b/src/ltlparse/public.hh index 929748e84..8e5daa819 100644 --- a/src/ltlparse/public.hh +++ b/src/ltlparse/public.hh @@ -23,7 +23,6 @@ # define SPOT_LTLPARSE_PUBLIC_HH # include "ltlast/formula.hh" -# include "ltlast/visitor.hh" // Unfortunately Bison 2.3 uses the same guards in all parsers :( # undef BISON_LOCATION_HH # undef BISON_POSITION_HH diff --git a/src/ltltest/equals.cc b/src/ltltest/equals.cc index 32cb4d5fd..f3bb024cd 100644 --- a/src/ltltest/equals.cc +++ b/src/ltltest/equals.cc @@ -30,7 +30,6 @@ #include "ltlvisit/nenoform.hh" #include "ltlvisit/destroy.hh" #include "ltlvisit/contain.hh" -#include "ltlast/allnodes.hh" #include "ltlvisit/reduce.hh" #include "ltlvisit/tostring.hh" diff --git a/src/ltltest/randltl.cc b/src/ltltest/randltl.cc index c0f6109da..acf86ce3e 100644 --- a/src/ltltest/randltl.cc +++ b/src/ltltest/randltl.cc @@ -25,7 +25,6 @@ #include #include #include -#include "ltlast/atomic_prop.hh" #include "ltlvisit/randomltl.hh" #include "ltlvisit/tostring.hh" #include "ltlvisit/destroy.hh" diff --git a/src/ltltest/readltl.cc b/src/ltltest/readltl.cc index b32e6b1d6..d72c2b83d 100644 --- a/src/ltltest/readltl.cc +++ b/src/ltltest/readltl.cc @@ -27,7 +27,6 @@ #include "ltlvisit/dump.hh" #include "ltlvisit/dotty.hh" #include "ltlvisit/destroy.hh" -#include "ltlast/allnodes.hh" void syntax(char* prog) diff --git a/src/ltltest/reduc.cc b/src/ltltest/reduc.cc index 75ee28ab8..242c51fef 100644 --- a/src/ltltest/reduc.cc +++ b/src/ltltest/reduc.cc @@ -32,7 +32,6 @@ #include "ltlvisit/reduce.hh" #include "ltlvisit/length.hh" #include "ltlvisit/contain.hh" -#include "ltlast/allnodes.hh" void syntax(char* prog) diff --git a/src/ltltest/syntimpl.cc b/src/ltltest/syntimpl.cc index 4e0dcf474..77c60969a 100644 --- a/src/ltltest/syntimpl.cc +++ b/src/ltltest/syntimpl.cc @@ -29,7 +29,6 @@ #include "ltlvisit/destroy.hh" #include "ltlvisit/tostring.hh" #include "ltlvisit/syntimpl.hh" -#include "ltlast/allnodes.hh" #include "ltlvisit/nenoform.hh" void diff --git a/src/ltltest/tostring.cc b/src/ltltest/tostring.cc index 43cf021d7..df0995fa1 100644 --- a/src/ltltest/tostring.cc +++ b/src/ltltest/tostring.cc @@ -25,7 +25,6 @@ #include "ltlparse/public.hh" #include "ltlvisit/tostring.hh" #include "ltlvisit/destroy.hh" -#include "ltlast/allnodes.hh" void syntax(char *prog) diff --git a/src/ltlvisit/apcollect.hh b/src/ltlvisit/apcollect.hh index 069afa0e9..756273977 100644 --- a/src/ltlvisit/apcollect.hh +++ b/src/ltlvisit/apcollect.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004, 2005, 2008 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 "ltlast/atomic_prop.hh" +#include "ltlast/formula.hh" namespace spot { diff --git a/src/ltlvisit/basicreduce.cc b/src/ltlvisit/basicreduce.cc index 9140ce506..c47955b0b 100644 --- a/src/ltlvisit/basicreduce.cc +++ b/src/ltlvisit/basicreduce.cc @@ -20,8 +20,6 @@ // 02111-1307, USA. #include "basicreduce.hh" -#include "ltlast/visitor.hh" -#include "ltlast/allnodes.hh" #include #include "clone.hh" diff --git a/src/ltlvisit/clone.cc b/src/ltlvisit/clone.cc index 6a0be0c62..ac2cebc33 100644 --- a/src/ltlvisit/clone.cc +++ b/src/ltlvisit/clone.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -19,7 +19,6 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -#include "ltlast/allnodes.hh" #include "clone.hh" namespace spot diff --git a/src/ltlvisit/clone.hh b/src/ltlvisit/clone.hh index 604f8bf13..7aeafb6b5 100644 --- a/src/ltlvisit/clone.hh +++ b/src/ltlvisit/clone.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -23,7 +23,6 @@ # define SPOT_LTLVISIT_CLONE_HH #include "ltlast/formula.hh" -#include "ltlast/visitor.hh" namespace spot { diff --git a/src/ltlvisit/contain.cc b/src/ltlvisit/contain.cc index dbb0ac3b8..866297177 100644 --- a/src/ltlvisit/contain.cc +++ b/src/ltlvisit/contain.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2006, 2007 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2006, 2007, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -23,10 +23,6 @@ #include "destroy.hh" #include "clone.hh" #include "tunabbrev.hh" -#include "ltlast/unop.hh" -#include "ltlast/binop.hh" -#include "ltlast/multop.hh" -#include "ltlast/constant.hh" #include "tgba/tgbaproduct.hh" #include "tgbaalgos/gtec/gtec.hh" #include "tgbaalgos/save.hh" diff --git a/src/ltlvisit/dotty.cc b/src/ltlvisit/dotty.cc index 67611b00c..12de237b1 100644 --- a/src/ltlvisit/dotty.cc +++ b/src/ltlvisit/dotty.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -21,8 +21,6 @@ #include "misc/hash.hh" #include "dotty.hh" -#include "ltlast/visitor.hh" -#include "ltlast/allnodes.hh" #include namespace spot diff --git a/src/ltlvisit/dump.cc b/src/ltlvisit/dump.cc index 3d94732cf..7823d16f1 100644 --- a/src/ltlvisit/dump.cc +++ b/src/ltlvisit/dump.cc @@ -1,6 +1,6 @@ -// 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. +// Copyright (C) 2003, 2004, 2005, 2008 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. // @@ -20,8 +20,6 @@ // 02111-1307, USA. #include "dump.hh" -#include "ltlast/visitor.hh" -#include "ltlast/allnodes.hh" #include namespace spot diff --git a/src/ltlvisit/lunabbrev.cc b/src/ltlvisit/lunabbrev.cc index 7c006a1e5..0e49410cb 100644 --- a/src/ltlvisit/lunabbrev.cc +++ b/src/ltlvisit/lunabbrev.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -19,7 +19,6 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -#include "ltlast/allnodes.hh" #include "ltlvisit/clone.hh" #include "lunabbrev.hh" #include diff --git a/src/ltlvisit/nenoform.cc b/src/ltlvisit/nenoform.cc index 208992461..26334c6e6 100644 --- a/src/ltlvisit/nenoform.cc +++ b/src/ltlvisit/nenoform.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -19,9 +19,8 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -#include "nenoform.hh" -#include "ltlast/allnodes.hh" #include +#include "nenoform.hh" namespace spot { diff --git a/src/ltlvisit/nenoform.hh b/src/ltlvisit/nenoform.hh index 3569c1359..336064a32 100644 --- a/src/ltlvisit/nenoform.hh +++ b/src/ltlvisit/nenoform.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -23,7 +23,6 @@ # define SPOT_LTLVISIT_NENOFORM_HH #include "ltlast/formula.hh" -#include "ltlast/visitor.hh" namespace spot { diff --git a/src/ltlvisit/postfix.cc b/src/ltlvisit/postfix.cc index 8863e6a80..37f27db06 100644 --- a/src/ltlvisit/postfix.cc +++ b/src/ltlvisit/postfix.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -20,7 +20,6 @@ // 02111-1307, USA. #include "ltlvisit/postfix.hh" -#include "ltlast/allnodes.hh" namespace spot { diff --git a/src/ltlvisit/postfix.hh b/src/ltlvisit/postfix.hh index 4d341f59b..c275ebea0 100644 --- a/src/ltlvisit/postfix.hh +++ b/src/ltlvisit/postfix.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -23,7 +23,6 @@ # define SPOT_LTLVISIT_POSTFIX_HH #include "ltlast/formula.hh" -#include "ltlast/visitor.hh" namespace spot { diff --git a/src/ltlvisit/randomltl.cc b/src/ltlvisit/randomltl.cc index 9b739f429..303d18b23 100644 --- a/src/ltlvisit/randomltl.cc +++ b/src/ltlvisit/randomltl.cc @@ -22,8 +22,6 @@ #include #include #include "randomltl.hh" -#include "ltlast/allnodes.hh" -#include "ltlast/visitor.hh" #include "misc/random.hh" #include #include diff --git a/src/ltlvisit/reduce.cc b/src/ltlvisit/reduce.cc index a34161043..3b4db1886 100644 --- a/src/ltlvisit/reduce.cc +++ b/src/ltlvisit/reduce.cc @@ -22,7 +22,6 @@ #include "reduce.hh" #include "basicreduce.hh" #include "syntimpl.hh" -#include "ltlast/allnodes.hh" #include #include "lunabbrev.hh" diff --git a/src/ltlvisit/reduce.hh b/src/ltlvisit/reduce.hh index 3c6fcf850..aae9d15b9 100644 --- a/src/ltlvisit/reduce.hh +++ b/src/ltlvisit/reduce.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004, 2006, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -23,7 +23,6 @@ # define SPOT_LTLVISIT_REDUCE_HH #include "ltlast/formula.hh" -#include "ltlast/visitor.hh" namespace spot { diff --git a/src/ltlvisit/simpfg.cc b/src/ltlvisit/simpfg.cc index fa143cfd9..928671505 100644 --- a/src/ltlvisit/simpfg.cc +++ b/src/ltlvisit/simpfg.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -19,8 +19,6 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -#include "ltlast/allnodes.hh" -#include "ltlvisit/clone.hh" #include "simpfg.hh" #include diff --git a/src/ltlvisit/syntimpl.cc b/src/ltlvisit/syntimpl.cc index eafc98845..aa9a180ac 100644 --- a/src/ltlvisit/syntimpl.cc +++ b/src/ltlvisit/syntimpl.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004, 2005, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -20,7 +20,6 @@ // 02111-1307, USA. #include "syntimpl.hh" -#include "ltlast/allnodes.hh" #include #include "lunabbrev.hh" diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc index 05b0a3827..2aee59a05 100644 --- a/src/ltlvisit/tostring.cc +++ b/src/ltlvisit/tostring.cc @@ -25,9 +25,6 @@ #include #include #include "tostring.hh" -#include "ltlast/visitor.hh" -#include "ltlast/allnodes.hh" - namespace spot { diff --git a/src/ltlvisit/tunabbrev.cc b/src/ltlvisit/tunabbrev.cc index 7d372148e..477e80e9c 100644 --- a/src/ltlvisit/tunabbrev.cc +++ b/src/ltlvisit/tunabbrev.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -19,7 +19,6 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -#include "ltlast/allnodes.hh" #include "tunabbrev.hh" namespace spot diff --git a/src/tgba/bdddict.cc b/src/tgba/bdddict.cc index e4ff5a61b..a29c69fa0 100644 --- a/src/tgba/bdddict.cc +++ b/src/tgba/bdddict.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de +// Copyright (C) 2003, 2004, 2005, 2006, 2008 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. // @@ -26,7 +26,6 @@ #include #include #include -#include #include #include "bdddict.hh" diff --git a/src/tgba/formula2bdd.cc b/src/tgba/formula2bdd.cc index edc42922e..a7cd8f791 100644 --- a/src/tgba/formula2bdd.cc +++ b/src/tgba/formula2bdd.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -21,8 +21,6 @@ #include #include "formula2bdd.hh" -#include "ltlast/allnodes.hh" -#include "ltlast/visitor.hh" #include "misc/minato.hh" #include "ltlvisit/clone.hh" diff --git a/src/tgba/tgbaexplicit.cc b/src/tgba/tgbaexplicit.cc index 0880cacdd..fff7ea89e 100644 --- a/src/tgba/tgbaexplicit.cc +++ b/src/tgba/tgbaexplicit.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -19,8 +19,6 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -#include "ltlast/atomic_prop.hh" -#include "ltlast/constant.hh" #include "ltlvisit/destroy.hh" #include "tgbaexplicit.hh" #include "tgba/formula2bdd.hh" diff --git a/src/tgba/tgbatba.cc b/src/tgba/tgbatba.cc index 0dc957dc0..938e34833 100644 --- a/src/tgba/tgbatba.cc +++ b/src/tgba/tgbatba.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004, 2005, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -22,8 +22,6 @@ #include #include "tgbatba.hh" #include "bddprint.hh" -#include "ltlast/constant.hh" -#include "ltlast/visitor.hh" #include "misc/hashfunc.hh" namespace spot diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index cc6e3ab3d..d73d48a34 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -23,8 +23,6 @@ #include "misc/bddalloc.hh" #include "misc/bddlt.hh" #include "misc/minato.hh" -#include "ltlast/visitor.hh" -#include "ltlast/allnodes.hh" #include "ltlvisit/lunabbrev.hh" #include "ltlvisit/nenoform.hh" #include "ltlvisit/destroy.hh" diff --git a/src/tgbaalgos/ltl2tgba_lacim.cc b/src/tgbaalgos/ltl2tgba_lacim.cc index fe6ce96b7..a00f81d23 100644 --- a/src/tgbaalgos/ltl2tgba_lacim.cc +++ b/src/tgbaalgos/ltl2tgba_lacim.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -19,8 +19,6 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -#include "ltlast/visitor.hh" -#include "ltlast/allnodes.hh" #include "ltlvisit/lunabbrev.hh" #include "ltlvisit/nenoform.hh" #include "ltlvisit/destroy.hh" diff --git a/src/tgbaalgos/randomgraph.cc b/src/tgbaalgos/randomgraph.cc index f85e5e5b8..365f0f6c4 100644 --- a/src/tgbaalgos/randomgraph.cc +++ b/src/tgbaalgos/randomgraph.cc @@ -22,7 +22,6 @@ #include "randomgraph.hh" #include "tgba/tgbaexplicit.hh" #include "misc/random.hh" -#include "ltlast/atomic_prop.hh" #include "ltlvisit/destroy.hh" #include #include diff --git a/src/tgbaalgos/randomgraph.hh b/src/tgbaalgos/randomgraph.hh index 618c227c8..7f776a61c 100644 --- a/src/tgbaalgos/randomgraph.hh +++ b/src/tgbaalgos/randomgraph.hh @@ -23,7 +23,6 @@ # define SPOT_TGBAALGOS_RANDOMGRAPH_HH #include "ltlvisit/apcollect.hh" -#include "ltlast/visitor.hh" #include "ltlenv/defaultenv.hh" namespace spot diff --git a/src/tgbaalgos/save.cc b/src/tgbaalgos/save.cc index b87a36eff..13bc00763 100644 --- a/src/tgbaalgos/save.cc +++ b/src/tgbaalgos/save.cc @@ -1,6 +1,6 @@ -// 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. +// Copyright (C) 2003, 2004, 2005, 2008 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. // @@ -23,7 +23,6 @@ #include "save.hh" #include "tgba/bddprint.hh" #include "ltlvisit/tostring.hh" -#include "ltlast/atomic_prop.hh" #include "reachiter.hh" #include "misc/escape.hh" diff --git a/src/tgbaparse/public.hh b/src/tgbaparse/public.hh index e6103ea7e..652ae6a28 100644 --- a/src/tgbaparse/public.hh +++ b/src/tgbaparse/public.hh @@ -27,7 +27,6 @@ # undef BISON_LOCATION_HH # undef BISON_POSITION_HH # include "tgbaparse/location.hh" -# include "ltlast/visitor.hh" # include "ltlenv/defaultenv.hh" # include # include diff --git a/src/tgbaparse/tgbaparse.yy b/src/tgbaparse/tgbaparse.yy index 7fe3b4252..8b9a8da5e 100644 --- a/src/tgbaparse/tgbaparse.yy +++ b/src/tgbaparse/tgbaparse.yy @@ -1,4 +1,4 @@ -/* Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de +/* Copyright (C) 2003, 2004, 2005, 2006, 2008 Laboratoire d'Informatique de ** Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), ** Université Pierre et Marie Curie. ** @@ -47,7 +47,6 @@ typedef std::map formula_cache; } %{ -#include "ltlast/constant.hh" #include "ltlvisit/destroy.hh" /* Unfortunately Bison 2.3 uses the same guards in all parsers :( */ #undef BISON_POSITION_HH diff --git a/src/tgbatest/explicit.cc b/src/tgbatest/explicit.cc index 07340a710..ae16ef046 100644 --- a/src/tgbatest/explicit.cc +++ b/src/tgbatest/explicit.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -24,8 +24,7 @@ #include "ltlenv/defaultenv.hh" #include "tgba/tgbaexplicit.hh" #include "tgbaalgos/dotty.hh" -#include "ltlast/allnodes.hh" -#include "ltlast/visitor.hh" +#include "ltlast/formula.hh" int main() diff --git a/src/tgbatest/explprod.cc b/src/tgbatest/explprod.cc index 94648919a..1d2c661bf 100644 --- a/src/tgbatest/explprod.cc +++ b/src/tgbatest/explprod.cc @@ -26,7 +26,7 @@ #include "tgba/tgbaproduct.hh" #include "tgbaparse/public.hh" #include "tgbaalgos/save.hh" -#include "ltlast/allnodes.hh" +#include "ltlast/formula.hh" void syntax(char* prog) diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 02a5213ec..c0d2d5039 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -29,7 +29,6 @@ #include "ltlvisit/contain.hh" #include "ltlvisit/tostring.hh" #include "ltlvisit/apcollect.hh" -#include "ltlast/allnodes.hh" #include "ltlparse/public.hh" #include "tgbaalgos/ltl2tgba_lacim.hh" #include "tgbaalgos/ltl2tgba_fm.hh" diff --git a/src/tgbatest/ltlprod.cc b/src/tgbatest/ltlprod.cc index 2bc0e4a49..7c5e68d6d 100644 --- a/src/tgbatest/ltlprod.cc +++ b/src/tgbatest/ltlprod.cc @@ -23,7 +23,6 @@ #include #include #include "ltlvisit/destroy.hh" -#include "ltlast/allnodes.hh" #include "ltlparse/public.hh" #include "tgbaalgos/ltl2tgba_lacim.hh" #include "tgba/tgbaproduct.hh" diff --git a/src/tgbatest/mixprod.cc b/src/tgbatest/mixprod.cc index dc246c2e2..dcce01fcf 100644 --- a/src/tgbatest/mixprod.cc +++ b/src/tgbatest/mixprod.cc @@ -23,7 +23,6 @@ #include #include #include "ltlvisit/destroy.hh" -#include "ltlast/allnodes.hh" #include "ltlparse/public.hh" #include "tgbaalgos/ltl2tgba_lacim.hh" #include "tgba/tgbaproduct.hh" diff --git a/src/tgbatest/powerset.cc b/src/tgbatest/powerset.cc index 6bfebd85e..7780b82be 100644 --- a/src/tgbatest/powerset.cc +++ b/src/tgbatest/powerset.cc @@ -26,7 +26,6 @@ #include "tgbaalgos/powerset.hh" #include "tgbaparse/public.hh" #include "tgbaalgos/save.hh" -#include "ltlast/allnodes.hh" #include "tgbaalgos/dotty.hh" void diff --git a/src/tgbatest/randtgba.cc b/src/tgbatest/randtgba.cc index 5204484af..48e59499b 100644 --- a/src/tgbatest/randtgba.cc +++ b/src/tgbatest/randtgba.cc @@ -41,7 +41,6 @@ #include "tgbaalgos/save.hh" #include "tgbaalgos/stats.hh" #include "ltlenv/defaultenv.hh" -#include "ltlast/atomic_prop.hh" #include "tgbaalgos/dotty.hh" #include "tgbaparse/public.hh" #include "misc/random.hh" diff --git a/src/tgbatest/readsave.cc b/src/tgbatest/readsave.cc index 6783ed265..4d998b08f 100644 --- a/src/tgbatest/readsave.cc +++ b/src/tgbatest/readsave.cc @@ -26,7 +26,6 @@ #include "tgbaparse/public.hh" #include "tgba/tgbaexplicit.hh" #include "tgbaalgos/save.hh" -#include "ltlast/allnodes.hh" void syntax(char* prog) diff --git a/src/tgbatest/reductgba.cc b/src/tgbatest/reductgba.cc index 26e92266f..0d0c7ac24 100644 --- a/src/tgbatest/reductgba.cc +++ b/src/tgbatest/reductgba.cc @@ -27,7 +27,6 @@ #include "ltlvisit/destroy.hh" #include "ltlvisit/reduce.hh" -#include "ltlast/allnodes.hh" #include "ltlparse/public.hh" #include "tgbaalgos/ltl2tgba_lacim.hh" #include "tgbaalgos/ltl2tgba_fm.hh" diff --git a/src/tgbatest/tgbaread.cc b/src/tgbatest/tgbaread.cc index d05e6cf78..50a375462 100644 --- a/src/tgbatest/tgbaread.cc +++ b/src/tgbatest/tgbaread.cc @@ -26,7 +26,6 @@ #include "tgbaparse/public.hh" #include "tgba/tgbaexplicit.hh" #include "tgbaalgos/dotty.hh" -#include "ltlast/allnodes.hh" void syntax(char* prog) diff --git a/src/tgbatest/tripprod.cc b/src/tgbatest/tripprod.cc index 0a33f2e6b..84e849fe1 100644 --- a/src/tgbatest/tripprod.cc +++ b/src/tgbatest/tripprod.cc @@ -26,7 +26,6 @@ #include "tgba/tgbaproduct.hh" #include "tgbaparse/public.hh" #include "tgbaalgos/save.hh" -#include "ltlast/allnodes.hh" void syntax(char* prog)