alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Merge all ltlast/ files into formula.hh. The forward declaration of visitor was causing error messages too cryptic for users.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2008-06-12 16:31:59 +02:00
parent 9afbaf6342
commit 25a3114287
60 changed files with 132 additions and 475 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/ltlast/Makefile.am
View file

@ -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

35
src/ltlast/allnodes.hh
View file

@ -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

42
src/ltlast/atomic_prop.hh
View file

@ -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<ltl_t> atomic_prop;
}
}
#endif // SPOT_LTLAST_ATOMICPROP_HH

45
src/ltlast/binop.hh
View file

@ -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<ltl_t> binop;
}
}
#endif // SPOT_LTLAST_BINOP_HH

42
src/ltlast/constant.hh
View file

@ -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<ltl_t> constant;
}
}
#endif // SPOT_LTLAST_CONSTANT_HH

69
src/ltlast/formula.hh
View file

@ -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<ltl_t> formula_ptr_less_than;
typedef spot::internal::formula_ptr_hash<ltl_t> formula_ptr_hash;
/// \brief Atomic propositions.
/// \ingroup ltl_ast
typedef spot::internal::atomic_prop<ltl_t> atomic_prop;
/// \brief A constant (True or False)
/// \ingroup ltl_ast
typedef spot::internal::constant<ltl_t> constant;
/// \brief Unary operators.
/// \ingroup ltl_ast
typedef spot::internal::unop<ltl_t> unop;
/// \brief Binary operator.
/// \ingroup ltl_ast
typedef spot::internal::binop<ltl_t> binop;
/// \brief Multi-operand operators.
/// \ingroup ltl_ast
///
/// These operators are considered commutative and associative.
typedef spot::internal::multop<ltl_t> 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;
};
}
}

44
src/ltlast/multop.hh
View file

@ -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<ltl_t> multop;
}
}
#endif // SPOT_LTLAST_MULTOP_HH

42
src/ltlast/refformula.hh
View file

@ -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<ltl_t> ref_formula;
}
}
#endif // SPOT_LTLAST_REFFORMULA_HH

42
src/ltlast/unop.hh
View file

@ -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<ltl_t> unop;
}
}
#endif // SPOT_LTLAST_UNOP_HH

77
src/ltlast/visitor.hh
View file

@ -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

3
src/ltlparse/ltlparse.yy
View file

@ -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 <string>
#include "public.hh"
#include "ltlast/allnodes.hh"
#include "ltlvisit/destroy.hh"
%}

1
src/ltlparse/public.hh
View file

@ -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

1
src/ltltest/equals.cc
View file

@ -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"

1
src/ltltest/randltl.cc
View file

@ -25,7 +25,6 @@
#include <string>
#include <cstdlib>
#include <cstring>
#include "ltlast/atomic_prop.hh"
#include "ltlvisit/randomltl.hh"
#include "ltlvisit/tostring.hh"
#include "ltlvisit/destroy.hh"

1
src/ltltest/readltl.cc
View file

@ -27,7 +27,6 @@
#include "ltlvisit/dump.hh"
#include "ltlvisit/dotty.hh"
#include "ltlvisit/destroy.hh"
#include "ltlast/allnodes.hh"
void
syntax(char* prog)

1
src/ltltest/reduc.cc
View file

@ -32,7 +32,6 @@
#include "ltlvisit/reduce.hh"
#include "ltlvisit/length.hh"
#include "ltlvisit/contain.hh"
#include "ltlast/allnodes.hh"
void
syntax(char* prog)

1
src/ltltest/syntimpl.cc
View file

@ -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

1
src/ltltest/tostring.cc
View file

@ -25,7 +25,6 @@
#include "ltlparse/public.hh"
#include "ltlvisit/tostring.hh"
#include "ltlvisit/destroy.hh"
#include "ltlast/allnodes.hh"
void
syntax(char *prog)

4
src/ltlvisit/apcollect.hh
View file

@ -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 <set>
#include "ltlast/atomic_prop.hh"
#include "ltlast/formula.hh"
namespace spot
{

2
src/ltlvisit/basicreduce.cc
View file

@ -20,8 +20,6 @@
// 02111-1307, USA.
#include "basicreduce.hh"
#include "ltlast/visitor.hh"
#include "ltlast/allnodes.hh"
#include <cassert>
#include "clone.hh"

3
src/ltlvisit/clone.cc
View file

@ -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

3
src/ltlvisit/clone.hh
View file

@ -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
{

6
src/ltlvisit/contain.cc
View file

@ -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"

4
src/ltlvisit/dotty.cc
View file

@ -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 <ostream>
namespace spot

8
src/ltlvisit/dump.cc
View file

@ -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 <ostream>
namespace spot

3
src/ltlvisit/lunabbrev.cc
View file

@ -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 <cassert>

5
src/ltlvisit/nenoform.cc
View file

@ -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 <cassert>
#include "nenoform.hh"
namespace spot
{

3
src/ltlvisit/nenoform.hh
View file

@ -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
{

3
src/ltlvisit/postfix.cc
View file

@ -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
{

3
src/ltlvisit/postfix.hh
View file

@ -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
{

2
src/ltlvisit/randomltl.cc
View file

@ -22,8 +22,6 @@
#include <cassert>
#include <algorithm>
#include "randomltl.hh"
#include "ltlast/allnodes.hh"
#include "ltlast/visitor.hh"
#include "misc/random.hh"
#include <iostream>
#include <cstring>

1
src/ltlvisit/reduce.cc
View file

@ -22,7 +22,6 @@
#include "reduce.hh"
#include "basicreduce.hh"
#include "syntimpl.hh"
#include "ltlast/allnodes.hh"
#include <cassert>
#include "lunabbrev.hh"

3
src/ltlvisit/reduce.hh
View file

@ -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
{

4
src/ltlvisit/simpfg.cc
View file

@ -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 <cassert>

3
src/ltlvisit/syntimpl.cc
View file

@ -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 <cassert>
#include "lunabbrev.hh"

3
src/ltlvisit/tostring.cc
View file

@ -25,9 +25,6 @@
#include <ostream>
#include <cstring>
#include "tostring.hh"
#include "ltlast/visitor.hh"
#include "ltlast/allnodes.hh"
namespace spot
{

3
src/ltlvisit/tunabbrev.cc
View file

@ -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

3
src/tgba/bdddict.cc
View file

@ -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 <ltlvisit/destroy.hh>
#include <ltlvisit/tostring.hh>
#include <ltlvisit/tostring.hh>
#include <ltlast/atomic_prop.hh>
#include <ltlenv/defaultenv.hh>
#include "bdddict.hh"

4
src/tgba/formula2bdd.cc
View file

@ -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 <cassert>
#include "formula2bdd.hh"
#include "ltlast/allnodes.hh"
#include "ltlast/visitor.hh"
#include "misc/minato.hh"
#include "ltlvisit/clone.hh"

4
src/tgba/tgbaexplicit.cc
View file

@ -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"

4
src/tgba/tgbatba.cc
View file

@ -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 <cassert>
#include "tgbatba.hh"
#include "bddprint.hh"
#include "ltlast/constant.hh"
#include "ltlast/visitor.hh"
#include "misc/hashfunc.hh"
namespace spot

2
src/tgbaalgos/ltl2tgba_fm.cc
View file

@ -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"

4
src/tgbaalgos/ltl2tgba_lacim.cc
View file

@ -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"

1
src/tgbaalgos/randomgraph.cc
View file

@ -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 <sstream>
#include <list>

1
src/tgbaalgos/randomgraph.hh
View file

@ -23,7 +23,6 @@
# define SPOT_TGBAALGOS_RANDOMGRAPH_HH
#include "ltlvisit/apcollect.hh"
#include "ltlast/visitor.hh"
#include "ltlenv/defaultenv.hh"
namespace spot

7
src/tgbaalgos/save.cc
View file

@ -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"

1
src/tgbaparse/public.hh
View file

@ -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 <string>
# include <list>

3
src/tgbaparse/tgbaparse.yy
View file

@ -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<std::string, bdd> 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

5
src/tgbatest/explicit.cc
View file

@ -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()

2
src/tgbatest/explprod.cc
View file

@ -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)

1
src/tgbatest/ltl2tgba.cc
View file

@ -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"

1
src/tgbatest/ltlprod.cc
View file

@ -23,7 +23,6 @@
#include <cassert>
#include <cstdlib>
#include "ltlvisit/destroy.hh"
#include "ltlast/allnodes.hh"
#include "ltlparse/public.hh"
#include "tgbaalgos/ltl2tgba_lacim.hh"
#include "tgba/tgbaproduct.hh"

1
src/tgbatest/mixprod.cc
View file

@ -23,7 +23,6 @@
#include <cassert>
#include <cstdlib>
#include "ltlvisit/destroy.hh"
#include "ltlast/allnodes.hh"
#include "ltlparse/public.hh"
#include "tgbaalgos/ltl2tgba_lacim.hh"
#include "tgba/tgbaproduct.hh"

1
src/tgbatest/powerset.cc
View file

@ -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

1
src/tgbatest/randtgba.cc
View file

@ -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"

1
src/tgbatest/readsave.cc
View file

@ -26,7 +26,6 @@
#include "tgbaparse/public.hh"
#include "tgba/tgbaexplicit.hh"
#include "tgbaalgos/save.hh"
#include "ltlast/allnodes.hh"
void
syntax(char* prog)

1
src/tgbatest/reductgba.cc
View file

@ -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"

1
src/tgbatest/tgbaread.cc
View file

@ -26,7 +26,6 @@
#include "tgbaparse/public.hh"
#include "tgba/tgbaexplicit.hh"
#include "tgbaalgos/dotty.hh"
#include "ltlast/allnodes.hh"
void
syntax(char* prog)

1
src/tgbatest/tripprod.cc
View file

@ -26,7 +26,6 @@
#include "tgba/tgbaproduct.hh"
#include "tgbaparse/public.hh"
#include "tgbaalgos/save.hh"
#include "ltlast/allnodes.hh"
void
syntax(char* prog)