diff --git a/src/ltlast/Makefile.am b/src/ltlast/Makefile.am index 8f3ebaa6d..a7ad7c36e 100644 --- a/src/ltlast/Makefile.am +++ b/src/ltlast/Makefile.am @@ -1,7 +1,8 @@ -## Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et -## Développement de l'Epita (LRDE). +## -*- coding: utf-8 -*- +## Copyright (C) 2009, 2010, 2011, 2013 Laboratoire de Recherche et +## Développement de l'Epita (LRDE). ## Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), -## département Systèmes Répartis Coopératifs (SRC), Université Pierre +## 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,7 +21,7 @@ ## along with this program. If not, see . AM_CPPFLAGS = -I$(srcdir)/.. -I.. -AM_CXXFLAGS = $(WARNING_CXXFLAGS) +AM_CXXFLAGS = $(WARNING_CXXFLAGS) $(VISIBILITY_CXXFLAGS) ltlastdir = $(pkgincludedir)/ltlast diff --git a/src/ltlast/atomic_prop.hh b/src/ltlast/atomic_prop.hh index f9be37f43..75ea65b12 100644 --- a/src/ltlast/atomic_prop.hh +++ b/src/ltlast/atomic_prop.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2012 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2009, 2012, 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. @@ -25,10 +25,10 @@ #ifndef SPOT_LTLAST_ATOMIC_PROP_HH # define SPOT_LTLAST_ATOMIC_PROP_HH +#include "refformula.hh" #include #include #include -#include "refformula.hh" #include "ltlenv/environment.hh" namespace spot @@ -38,7 +38,7 @@ namespace spot /// \ingroup ltl_ast /// \brief Atomic propositions. - class atomic_prop : public ref_formula + class SPOT_API atomic_prop : public ref_formula { public: /// Build an atomic proposition with name \a name in diff --git a/src/ltlast/automatop.hh b/src/ltlast/automatop.hh index 203d743c7..27c1c37eb 100644 --- a/src/ltlast/automatop.hh +++ b/src/ltlast/automatop.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2009, 2012 Laboratoire de Recherche et +// Copyright (C) 2008, 2009, 2012, 2013 Laboratoire de Recherche et // Développement de l'Epita (LRDE) // // This file is part of Spot, a model checking library. @@ -22,11 +22,11 @@ #ifndef SPOT_LTLAST_AUTOMATOP_HH # define SPOT_LTLAST_AUTOMATOP_HH +# include "refformula.hh" # include # include # include # include "nfa.hh" -# include "refformula.hh" namespace spot { @@ -35,7 +35,7 @@ namespace spot /// \ingroup eltl_ast /// \brief Automaton operators. /// - class automatop : public ref_formula + class SPOT_API automatop : public ref_formula { public: /// List of formulae. diff --git a/src/ltlast/binop.hh b/src/ltlast/binop.hh index c53759383..d47a6c181 100644 --- a/src/ltlast/binop.hh +++ b/src/ltlast/binop.hh @@ -28,9 +28,9 @@ #ifndef SPOT_LTLAST_BINOP_HH # define SPOT_LTLAST_BINOP_HH +#include "refformula.hh" #include #include -#include "refformula.hh" namespace spot { @@ -39,7 +39,7 @@ namespace spot /// \ingroup ltl_ast /// \brief Binary operator. - class binop : public ref_formula + class SPOT_API binop : public ref_formula { public: /// Different kinds of binary opertaors diff --git a/src/ltlast/bunop.hh b/src/ltlast/bunop.hh index b4a1de7bf..81e087bac 100644 --- a/src/ltlast/bunop.hh +++ b/src/ltlast/bunop.hh @@ -1,5 +1,6 @@ -// Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -21,9 +22,9 @@ #ifndef SPOT_LTLAST_BUNOP_HH # define SPOT_LTLAST_BUNOP_HH +#include "refformula.hh" #include #include -#include "refformula.hh" #include "constant.hh" namespace spot @@ -33,7 +34,7 @@ namespace spot /// \ingroup ltl_ast /// \brief Bounded unary operator. - class bunop : public ref_formula + class SPOT_API bunop : public ref_formula { public: enum type { Star }; diff --git a/src/ltlast/constant.hh b/src/ltlast/constant.hh index 2ebe83675..41ef4250c 100644 --- a/src/ltlast/constant.hh +++ b/src/ltlast/constant.hh @@ -1,4 +1,5 @@ -// Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2010, 2012, 2013 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // @@ -31,7 +32,7 @@ namespace spot /// \ingroup ltl_ast /// \brief A constant (True or False) - class constant : public formula + class SPOT_API constant : public formula { public: enum type { False, True, EmptyWord }; diff --git a/src/ltlast/formula.hh b/src/ltlast/formula.hh index ed31dc5ae..6b36f2fc3 100644 --- a/src/ltlast/formula.hh +++ b/src/ltlast/formula.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013 Laboratoire de +// Recherche et Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de // // This file is part of Spot, a model checking library. @@ -23,6 +23,7 @@ #ifndef SPOT_LTLAST_FORMULA_HH # define SPOT_LTLAST_FORMULA_HH +#include "misc/common.hh" #include #include #include "predecl.hh" @@ -68,7 +69,7 @@ namespace spot /// /// The only way you can work with a formula is to /// build a spot::ltl::visitor or spot::ltl::const_visitor. - class formula + class SPOT_API formula { public: /// Kind of a sub-formula @@ -420,11 +421,13 @@ namespace spot }; /// Print the properties of formula \a f on stream \a out. + SPOT_API std::ostream& print_formula_props(std::ostream& out, const formula* f, bool abbreviated = false); /// List the properties of formula \a f. + SPOT_API std::list list_formula_props(const formula* f); } } diff --git a/src/ltlast/formula_tree.hh b/src/ltlast/formula_tree.hh index c70daa44c..4cf946f32 100644 --- a/src/ltlast/formula_tree.hh +++ b/src/ltlast/formula_tree.hh @@ -1,5 +1,6 @@ -// Copyright (C) 2009, 2012 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2012, 2013 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -21,9 +22,9 @@ #ifndef SPOT_LTLAST_FORMULA_TREE_HH # define SPOT_LTLAST_FORMULA_TREE_HH +# include "formula.hh" # include # include -# include "formula.hh" # include "multop.hh" # include "binop.hh" # include "unop.hh" diff --git a/src/ltlast/multop.hh b/src/ltlast/multop.hh index b2ddf779c..4750e3e65 100644 --- a/src/ltlast/multop.hh +++ b/src/ltlast/multop.hh @@ -1,5 +1,6 @@ -// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2010, 2011, 2012, 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. @@ -24,10 +25,10 @@ #ifndef SPOT_LTLAST_MULTOP_HH # define SPOT_LTLAST_MULTOP_HH +#include "refformula.hh" #include #include #include -#include "refformula.hh" namespace spot { @@ -36,7 +37,7 @@ namespace spot /// \ingroup ltl_ast /// \brief Multi-operand operators. - class multop : public ref_formula + class SPOT_API multop : public ref_formula { public: enum type { Or, OrRat, And, AndRat, AndNLM, Concat, Fusion }; diff --git a/src/ltlast/nfa.hh b/src/ltlast/nfa.hh index abc58df61..34b969674 100644 --- a/src/ltlast/nfa.hh +++ b/src/ltlast/nfa.hh @@ -1,5 +1,6 @@ -// Copyright (C) 2008, 2010 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2008, 2010, 2013 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -21,6 +22,7 @@ #ifndef SPOT_LTLAST_NFA_HH # define SPOT_LTLAST_NFA_HH +# include "misc/common.hh" # include "misc/hash.hh" # include # include @@ -32,7 +34,7 @@ namespace spot namespace ltl { /// Forward declaration. See below. - class succ_iterator; + class SPOT_API succ_iterator; /// Forward declaration. NFA's labels are reprensented by nodes /// which are defined in formula_tree.hh, included in nfa.cc. namespace formula_tree @@ -45,7 +47,7 @@ namespace spot /// States are represented by integers. /// Labels are represented by formula_tree's nodes. /// Currently, only one initial state is possible. - class nfa + class SPOT_API nfa { public: struct transition; @@ -118,7 +120,7 @@ namespace spot nfa& operator=(const nfa& other); }; - class succ_iterator + class SPOT_API succ_iterator { public: succ_iterator(const nfa::state::const_iterator s) diff --git a/src/ltlast/refformula.hh b/src/ltlast/refformula.hh index c7eed062c..3755d1ee5 100644 --- a/src/ltlast/refformula.hh +++ b/src/ltlast/refformula.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2012 Laboratoire de Recherche de Developpement -// de l'EPITA (LRDE). +// Copyright (C) 2010, 2012, 2013 Laboratoire de Recherche de +// Développement de l'EPITA (LRDE). // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. @@ -34,7 +34,7 @@ namespace spot /// \ingroup ltl_ast /// \brief A reference-counted LTL formula. - class ref_formula : public formula + class SPOT_API ref_formula : public formula { protected: virtual ~ref_formula(); diff --git a/src/ltlast/unop.hh b/src/ltlast/unop.hh index 2eff2dbe3..4f2843571 100644 --- a/src/ltlast/unop.hh +++ b/src/ltlast/unop.hh @@ -1,8 +1,9 @@ -// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2010, 2011, 2012, 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. +// 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. // @@ -36,7 +37,7 @@ namespace spot /// \ingroup ltl_ast /// \brief Unary operators. - class unop : public ref_formula + class SPOT_API unop : public ref_formula { public: enum type { diff --git a/src/ltlast/visitor.hh b/src/ltlast/visitor.hh index ed8bf1d53..91ac6462e 100644 --- a/src/ltlast/visitor.hh +++ b/src/ltlast/visitor.hh @@ -1,7 +1,8 @@ -// Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2010, 2012, 2013 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -24,7 +25,8 @@ #ifndef SPOT_LTLAST_VISITOR_HH # define SPOT_LTLAST_VISITOR_HH -#include "predecl.hh" +# include "misc/common.hh" +# include "predecl.hh" namespace spot { @@ -36,7 +38,7 @@ namespace spot /// Implementing visitors is the prefered way /// to traverse a formula, since it does not /// involve any cast. - struct visitor + struct SPOT_API visitor { virtual ~visitor() {} virtual void visit(const atomic_prop* node) = 0; diff --git a/src/ltlenv/Makefile.am b/src/ltlenv/Makefile.am index 99e9570d4..000484cc5 100644 --- a/src/ltlenv/Makefile.am +++ b/src/ltlenv/Makefile.am @@ -1,4 +1,4 @@ -## Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +## Copyright (C) 2003, 2004, 2013 Laboratoire d'Informatique de Paris 6 (LIP6), ## département Systèmes Répartis Coopératifs (SRC), Université Pierre ## et Marie Curie. ## @@ -18,7 +18,7 @@ ## along with this program. If not, see . AM_CPPFLAGS = -I$(srcdir)/.. -AM_CXXFLAGS = $(WARNING_CXXFLAGS) +AM_CXXFLAGS = $(WARNING_CXXFLAGS) $(VISIBILITY_CXXFLAGS) ltlenvdir = $(pkgincludedir)/ltlenv diff --git a/src/ltlenv/declenv.hh b/src/ltlenv/declenv.hh index 45076e8fe..f8d2eeae7 100644 --- a/src/ltlenv/declenv.hh +++ b/src/ltlenv/declenv.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2012 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2009, 2012, 2013 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -38,7 +38,7 @@ namespace spot /// /// This environment recognizes all atomic propositions /// that have been previously declared. It will reject other. - class declarative_environment : public environment + class SPOT_API declarative_environment : public environment { public: declarative_environment(); diff --git a/src/ltlenv/defaultenv.hh b/src/ltlenv/defaultenv.hh index c73594a08..5ad6163eb 100644 --- a/src/ltlenv/defaultenv.hh +++ b/src/ltlenv/defaultenv.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012 Laboratoire de Recherche et Développement +// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -37,7 +37,7 @@ namespace spot /// /// This is a singleton. Use default_environment::instance() /// to obtain the instance. - class default_environment : public environment + class SPOT_API default_environment : public environment { public: virtual ~default_environment(); diff --git a/src/ltlvisit/Makefile.am b/src/ltlvisit/Makefile.am index d8cfdf34f..16ea5d75d 100644 --- a/src/ltlvisit/Makefile.am +++ b/src/ltlvisit/Makefile.am @@ -21,7 +21,7 @@ ## along with this program. If not, see . AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(BUDDY_CPPFLAGS) -AM_CXXFLAGS = $(WARNING_CXXFLAGS) +AM_CXXFLAGS = $(WARNING_CXXFLAGS) $(VISIBILITY_CXXFLAGS) ltlvisitdir = $(pkgincludedir)/ltlvisit diff --git a/src/ltlvisit/apcollect.hh b/src/ltlvisit/apcollect.hh index f42869c4c..480480b0e 100644 --- a/src/ltlvisit/apcollect.hh +++ b/src/ltlvisit/apcollect.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012 Laboratoire de Recherche et Développement +// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -23,8 +23,8 @@ #ifndef SPOT_LTLVISIT_APCOLLECT_HH # define SPOT_LTLVISIT_APCOLLECT_HH -#include #include "ltlast/atomic_prop.hh" +#include #include "bdd.h" namespace spot @@ -50,7 +50,7 @@ namespace spot /// set containing all these atomic propositions if \c s is 0. /// The atomic propositions inserted into \a s are not cloned, so /// they are only valid as long as \a f is. - atomic_prop_set* + SPOT_API atomic_prop_set* atomic_prop_collect(const formula* f, atomic_prop_set* s = 0); /// \brief Return the set of atomic propositions occurring in a @@ -59,7 +59,7 @@ namespace spot /// \param f the formula to inspect /// \param a that automaton that should register the BDD variables used. /// \return A conjunction the atomic propositions. - bdd + SPOT_API bdd atomic_prop_collect_as_bdd(const formula* f, const tgba* a); /// @} diff --git a/src/ltlvisit/clone.hh b/src/ltlvisit/clone.hh index cab13d08a..5efca2671 100644 --- a/src/ltlvisit/clone.hh +++ b/src/ltlvisit/clone.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et +// Copyright (C) 2009, 2010, 2012, 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 @@ -37,7 +37,7 @@ namespace spot /// to derive from it and override part of its methods. /// But if you just want the functionality, consider using /// spot::ltl::formula::clone instead, it is way faster. - class clone_visitor : public visitor + class SPOT_API clone_visitor : public visitor { public: clone_visitor(); @@ -59,17 +59,11 @@ namespace spot const formula* result_; }; -#if __GNUC__ /// \ingroup ltl_essential /// \brief Clone a formula. /// \deprecated Use f->clone() instead. + SPOT_API SPOT_DEPRECATED const formula* clone(const formula* f) __attribute__ ((deprecated)); -#else - /// \ingroup ltl_essential - /// \brief Clone a formula. - /// \deprecated Use f->clone() instead. - const formula* clone(const formula* f); -#endif } } diff --git a/src/ltlvisit/contain.hh b/src/ltlvisit/contain.hh index 0c95ec393..03d5c6205 100644 --- a/src/ltlvisit/contain.hh +++ b/src/ltlvisit/contain.hh @@ -1,7 +1,8 @@ -// Copyright (C) 2011, 2012 Laboratoire de Recherche et Developpement de -// l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2011, 2012, 2013 Laboratoire de Recherche et +// Developpement de l'Epita (LRDE). // Copyright (C) 2006 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -31,8 +32,8 @@ namespace spot { namespace ltl { - // Check containment of language represented by LTL formulae. - class language_containment_checker + /// Check containment between LTL formulae. + class SPOT_API language_containment_checker { struct record_ { @@ -44,7 +45,7 @@ namespace spot record_, formula_ptr_hash> trans_map; public: /// This class uses spot::ltl_to_tgba_fm to translate LTL - /// formulae. See that class for the meaning of these options. + /// formulae. See that function for the meaning of these options. language_containment_checker(bdd_dict* dict, bool exprop, bool symb_merge, bool branching_postponement, @@ -106,13 +107,9 @@ namespace spot /// reduce some U, R, and X usages. /// /// \deprecated Use spot::ltl::ltl_simplifier instead. -#if __GNUC__ + SPOT_API SPOT_DEPRECATED const formula* reduce_tau03(const formula* f, - bool stronger = true) - __attribute__ ((deprecated)); -#else - const formula* reduce_tau03(const formula* f, bool stronger = true); -#endif + bool stronger = true); } } diff --git a/src/ltlvisit/destroy.hh b/src/ltlvisit/destroy.hh index 81218f612..caf688d4c 100644 --- a/src/ltlvisit/destroy.hh +++ b/src/ltlvisit/destroy.hh @@ -1,7 +1,8 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement +// -*- 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 +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -22,23 +23,18 @@ #ifndef SPOT_LTLVISIT_DESTROY_HH # define SPOT_LTLVISIT_DESTROY_HH -#include "ltlvisit/postfix.hh" +# include "misc/common.hh" +# include "ltlvisit/postfix.hh" namespace spot { namespace ltl { -#if __GNUC__ - /// \ingroup ltl_essential - /// \brief Destroys a formula - /// \deprecated Use f->destroy() instead. - void destroy(const formula *f) __attribute__ ((deprecated)); -#else /// \ingroup ltl_essential /// \brief Destroys a formula /// \deprecated Use f->destroy() instead. + SPOT_API SPOT_DEPRECATED void destroy(const formula *f); -#endif } } diff --git a/src/ltlvisit/dotty.hh b/src/ltlvisit/dotty.hh index b88950d3c..a35eb79d7 100644 --- a/src/ltlvisit/dotty.hh +++ b/src/ltlvisit/dotty.hh @@ -1,5 +1,8 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 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 +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -34,6 +37,7 @@ namespace spot /// /// \c dot is part of the GraphViz package /// http://www.research.att.com/sw/tools/graphviz/ + SPOT_API std::ostream& dotty(std::ostream& os, const formula* f); } } diff --git a/src/ltlvisit/dump.hh b/src/ltlvisit/dump.hh index 483d8ba47..c6cdf20c1 100644 --- a/src/ltlvisit/dump.hh +++ b/src/ltlvisit/dump.hh @@ -1,5 +1,8 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// -*- coding: utf-8 -*- +// Copyright (C) 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. @@ -33,6 +36,7 @@ namespace spot /// \param f The formula to dump. /// /// This is useful to display a formula when debugging. + SPOT_API std::ostream& dump(std::ostream& os, const formula* f); } } diff --git a/src/ltlvisit/lbt.hh b/src/ltlvisit/lbt.hh index 3313325a0..8dfd39b33 100644 --- a/src/ltlvisit/lbt.hh +++ b/src/ltlvisit/lbt.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012 Laboratoire de Recherche et +// Copyright (C) 2012, 2013 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -41,7 +41,7 @@ namespace spot /// /// \param f The formula to translate. /// \param os The stream where it should be output. - std::ostream& + SPOT_API std::ostream& to_lbt_string(const formula* f, std::ostream& os); /// \brief Output an LTL formula as a string in LBT's format. @@ -53,7 +53,7 @@ namespace spot /// rewrite these two operators using unabbreviate_wm(). /// /// \param f The formula to translate. - std::string + SPOT_API std::string to_lbt_string(const formula* f); /// @} } diff --git a/src/ltlvisit/length.hh b/src/ltlvisit/length.hh index 5ab222e35..fdb08e945 100644 --- a/src/ltlvisit/length.hh +++ b/src/ltlvisit/length.hh @@ -1,7 +1,8 @@ -// Copyright (C) 2012 Laboratoire de Recherche et Developement de +// -*- coding: utf-8 -*- +// Copyright (C) 2012, 2013 Laboratoire de Recherche et Developement de // l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -40,6 +41,7 @@ namespace spot /// /// If squash_boolean is set, all Boolean formulae are assumed /// to have length one. + SPOT_API int length(const formula* f); /// \ingroup ltl_misc @@ -47,6 +49,7 @@ namespace spot /// /// This is similar to spot::ltl::length(), except all Boolean /// formulae are assumed to have length one. + SPOT_API int length_boolone(const formula* f); } } diff --git a/src/ltlvisit/lunabbrev.hh b/src/ltlvisit/lunabbrev.hh index 9f41bf476..f56631685 100644 --- a/src/ltlvisit/lunabbrev.hh +++ b/src/ltlvisit/lunabbrev.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012 Laboratoire de Recherche et Développement +// Copyright (C) 2012, 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 @@ -41,7 +41,7 @@ namespace spot /// to derive from it and override some of its methods. /// But if you just want the functionality, consider using /// spot::ltl::unabbreviate_logic instead. - class unabbreviate_logic_visitor : public clone_visitor + class SPOT_API unabbreviate_logic_visitor : public clone_visitor { typedef clone_visitor super; public: @@ -61,7 +61,7 @@ namespace spot /// This will rewrite binary operators such as binop::Implies, /// binop::Equals, and binop::Xor, using only unop::Not, multop::Or, /// and multop::And. - const formula* unabbreviate_logic(const formula* f); + SPOT_API const formula* unabbreviate_logic(const formula* f); } } diff --git a/src/ltlvisit/nenoform.cc b/src/ltlvisit/nenoform.cc index 5e40172ae..bf1bcc7fb 100644 --- a/src/ltlvisit/nenoform.cc +++ b/src/ltlvisit/nenoform.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2011, 2012, 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. @@ -20,6 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "nenoform.hh" #include "simplify.hh" namespace spot diff --git a/src/ltlvisit/nenoform.hh b/src/ltlvisit/nenoform.hh index b49801a41..5a13cde8d 100644 --- a/src/ltlvisit/nenoform.hh +++ b/src/ltlvisit/nenoform.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// Copyright (C) 2011, 2012, 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. @@ -44,7 +44,7 @@ namespace spot /// or spot::ltl::unabbreviate_ltl first. (Calling these functions /// after spot::ltl::negative_normal_form would likely produce a /// formula which is not in negative normal form.) - const formula* + SPOT_API const formula* negative_normal_form(const formula* f, bool negated = false); } } diff --git a/src/ltlvisit/postfix.hh b/src/ltlvisit/postfix.hh index c0141f8fb..860aceccb 100644 --- a/src/ltlvisit/postfix.hh +++ b/src/ltlvisit/postfix.hh @@ -1,7 +1,8 @@ -// Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2010, 2012, 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 +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -35,7 +36,7 @@ namespace spot /// /// Override one or more of the postifix_visitor::doit methods /// with the algorithm to apply. - class postfix_visitor : public visitor + class SPOT_API postfix_visitor : public visitor { public: postfix_visitor(); diff --git a/src/ltlvisit/randomltl.hh b/src/ltlvisit/randomltl.hh index 77602c63a..77457866a 100644 --- a/src/ltlvisit/randomltl.hh +++ b/src/ltlvisit/randomltl.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et +// Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -33,7 +33,7 @@ namespace spot /// \ingroup ltl_io /// \brief Base class for random formula generators - class random_formula + class SPOT_API random_formula { public: random_formula(unsigned proba_size, @@ -110,7 +110,7 @@ namespace spot /// Also, each atomic proposition has as much chance as each /// constant (i.e., true and false) to be picked. This can be /// tuned using parse_options(). - class random_ltl: public random_formula + class SPOT_API random_ltl: public random_formula { public: /// Create a random LTL generator using atomic propositions from \a ap. @@ -160,7 +160,7 @@ namespace spot /// constant and all Boolean operators supported by Spot. /// /// By default each operator has equal chance to be selected. - class random_boolean: public random_formula + class SPOT_API random_boolean: public random_formula { public: /// Create a random Boolean formula generator using atomic @@ -200,7 +200,7 @@ namespace spot /// constant and all SERE operators supported by Spot. /// /// By default each operator has equal chance to be selected. - class random_sere: public random_formula + class SPOT_API random_sere: public random_formula { public: /// Create a random SERE genere using atomic propositions from \a ap. @@ -241,7 +241,7 @@ namespace spot /// The formulae will use the use atomic propositions from the /// set of propositions passed to the constructor, in addition to the /// constant and all PSL operators supported by Spot. - class random_psl: public random_ltl + class SPOT_API random_psl: public random_ltl { public: /// Create a random PSL generator using atomic propositions from \a ap. diff --git a/src/ltlvisit/reduce.hh b/src/ltlvisit/reduce.hh index f8333044c..4093178be 100644 --- a/src/ltlvisit/reduce.hh +++ b/src/ltlvisit/reduce.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et +// 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é @@ -68,12 +68,8 @@ namespace spot /// \return the reduced formula /// /// \deprecated Use spot::ltl::ltl_simplifier instead. -#if __GNUC__ - const formula* - reduce(const formula* f, int opt = Reduce_All) __attribute__ ((deprecated)); -#else - const formula* reduce(const formula* f, int opt = Reduce_All); -#endif + SPOT_API SPOT_DEPRECATED const formula* + reduce(const formula* f, int opt = Reduce_All); /// @} /// \ingroup ltl_misc @@ -99,11 +95,8 @@ namespace spot /// anything and still satisfies the formula. /// /// \deprecated Use f->is_eventual() instead. -#if __GNUC__ - bool is_eventual(const formula* f) __attribute__ ((deprecated)); -#else + SPOT_API SPOT_DEPRECATED bool is_eventual(const formula* f); -#endif /// \ingroup ltl_misc /// \brief Check whether a formula is purely universal. @@ -128,11 +121,8 @@ namespace spot /// universal formula also satisfies the formula. /// /// \deprecated Use f->is_universal() instead. -#if __GNUC__ - bool is_universal(const formula* f) __attribute__ ((deprecated)); -#else + SPOT_API SPOT_DEPRECATED bool is_universal(const formula* f); -#endif } } diff --git a/src/ltlvisit/relabel.hh b/src/ltlvisit/relabel.hh index d52df66a2..34030c105 100644 --- a/src/ltlvisit/relabel.hh +++ b/src/ltlvisit/relabel.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012 Laboratoire de Recherche et +// Copyright (C) 2012, 2013 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -29,8 +29,8 @@ namespace spot enum relabeling_style { Abc, Pnn }; /// \ingroup ltl_rewriting - /// \brief Relabel the atomic proposition in a formula. - /// + /// \brief Relabel the atomic propositions in a formula. + SPOT_API const formula* relabel(const formula* f, relabeling_style style); } } diff --git a/src/ltlvisit/remove_x.cc b/src/ltlvisit/remove_x.cc index aa79eadcf..4b44aa2d0 100644 --- a/src/ltlvisit/remove_x.cc +++ b/src/ltlvisit/remove_x.cc @@ -20,6 +20,7 @@ #include "ltlvisit/simplify.hh" #include "ltlvisit/clone.hh" #include "ltlvisit/apcollect.hh" +#include "ltlvisit/remove_x.hh" namespace spot { diff --git a/src/ltlvisit/remove_x.hh b/src/ltlvisit/remove_x.hh index 5a1385817..a7d1039af 100644 --- a/src/ltlvisit/remove_x.hh +++ b/src/ltlvisit/remove_x.hh @@ -1,3 +1,4 @@ +// -*- coding: utf-8 -*- // Copyright (C) 2013 Laboratoire de Recherche et Developpement de // l'Epita (LRDE). // @@ -19,6 +20,8 @@ #ifndef SPOT_LTLVISIT_REMOVE_X_HH # define SPOT_LTLVISIT_REMOVE_X_HH +# include "misc/common.hh" + namespace spot { namespace ltl @@ -43,6 +46,7 @@ namespace spot pages = {261--263} } \endverbatim */ + SPOT_API const formula* remove_x(const formula* f); /// \brief Whether an LTL formula \a f is stutter-insensitive. @@ -63,6 +67,7 @@ namespace spot pages = {261--263} } \endverbatim */ + SPOT_API bool is_stutter_insensitive(const formula* f); } } diff --git a/src/ltlvisit/simpfg.hh b/src/ltlvisit/simpfg.hh index 6d6f4bfc8..ea6685702 100644 --- a/src/ltlvisit/simpfg.hh +++ b/src/ltlvisit/simpfg.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2012 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2010, 2012, 2013 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -40,7 +40,7 @@ namespace spot /// - false R a = G a /// - a W false = G a /// - class simplify_f_g_visitor : public clone_visitor + class SPOT_API simplify_f_g_visitor : public clone_visitor { typedef clone_visitor super; public: @@ -64,7 +64,7 @@ namespace spot /// - false R a = G a /// - a W false = G a /// - const formula* simplify_f_g(const formula* f); + SPOT_API const formula* simplify_f_g(const formula* f); } } diff --git a/src/ltlvisit/simplify.hh b/src/ltlvisit/simplify.hh index 63ee7526e..170e32479 100644 --- a/src/ltlvisit/simplify.hh +++ b/src/ltlvisit/simplify.hh @@ -75,7 +75,7 @@ namespace spot /// \ingroup ltl_rewriting /// \brief Rewrite or simplify \a f in various ways. - class ltl_simplifier + class SPOT_API ltl_simplifier { public: ltl_simplifier(bdd_dict* dict = 0); diff --git a/src/ltlvisit/snf.hh b/src/ltlvisit/snf.hh index 39f49a055..391f40309 100644 --- a/src/ltlvisit/snf.hh +++ b/src/ltlvisit/snf.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012 Laboratoire de Recherche et Developpement +// Copyright (C) 2012, 2013 Laboratoire de Recherche et Developpement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -50,8 +50,8 @@ namespace spot /// /// \param sere the SERE to rewrite /// \param cache an optional cache - const formula* star_normal_form(const formula* sere, - snf_cache* cache = 0); + SPOT_API const formula* + star_normal_form(const formula* sere, snf_cache* cache = 0); } } diff --git a/src/ltlvisit/tostring.hh b/src/ltlvisit/tostring.hh index 70189678f..db35b89af 100644 --- a/src/ltlvisit/tostring.hh +++ b/src/ltlvisit/tostring.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et +// Copyright (C) 2010, 2011, 2012, 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 @@ -40,7 +40,7 @@ namespace spot /// \param full_parent Whether or not the string should by fully /// parenthesized. /// \param ratexp Whether we are printing a SERE. - std::ostream& + SPOT_API std::ostream& to_string(const formula* f, std::ostream& os, bool full_parent = false, bool ratexp = false); @@ -50,7 +50,7 @@ namespace spot /// \param full_parent Whether or not the string should by fully /// parenthesized. /// \param ratexp Whether we are printing a SERE. - std::string + SPOT_API std::string to_string(const formula* f, bool full_parent = false, bool ratexp = false); /// \brief Output a formula as an utf8 string which is parsable unless @@ -60,7 +60,7 @@ namespace spot /// \param full_parent Whether or not the string should by fully /// parenthesized. /// \param ratexp Whether we are printing a SERE. - std::ostream& + SPOT_API std::ostream& to_utf8_string(const formula* f, std::ostream& os, bool full_parent = false, bool ratexp = false); @@ -70,7 +70,7 @@ namespace spot /// \param full_parent Whether or not the string should by fully /// parenthesized. /// \param ratexp Whether we are printing a SERE. - std::string + SPOT_API std::string to_utf8_string(const formula* f, bool full_parent = false, bool ratexp = false); @@ -79,23 +79,27 @@ namespace spot /// \param os The stream where it should be output. /// \param full_parent Whether or not the string should by fully /// parenthesized. - std::ostream& to_spin_string(const formula* f, std::ostream& os, - bool full_parent = false); + SPOT_API std::ostream& + to_spin_string(const formula* f, std::ostream& os, + bool full_parent = false); /// \brief Convert a formula into a string parsable by Spin. /// \param f The formula to translate. /// \param full_parent Whether or not the string should by fully /// parenthesized. - std::string to_spin_string(const formula* f, bool full_parent = false); + SPOT_API std::string + to_spin_string(const formula* f, bool full_parent = false); /// \brief Output a formula as a string parsable by Wring. /// \param f The formula to translate. /// \param os The stream where it should be output. - std::ostream& to_wring_string(const formula* f, std::ostream& os); + SPOT_API std::ostream& + to_wring_string(const formula* f, std::ostream& os); /// \brief Convert a formula into a string parsable by Wring /// \param f The formula to translate. - std::string to_wring_string(const formula* f); + SPOT_API std::string + to_wring_string(const formula* f); /// @} } diff --git a/src/ltlvisit/tunabbrev.hh b/src/ltlvisit/tunabbrev.hh index 358df0970..a3b739033 100644 --- a/src/ltlvisit/tunabbrev.hh +++ b/src/ltlvisit/tunabbrev.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement de +// Copyright (C) 2011, 2012, 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 @@ -44,7 +44,7 @@ namespace spot /// to derive from it and override some of its methods. /// But if you just want the functionality, consider using /// spot::ltl::unabbreviate_ltl instead. - class unabbreviate_ltl_visitor : public unabbreviate_logic_visitor + class SPOT_API unabbreviate_ltl_visitor : public unabbreviate_logic_visitor { typedef unabbreviate_logic_visitor super; public: @@ -65,7 +65,7 @@ namespace spot /// /// This will also rewrite unary operators such as unop::F, /// and unop::G, using only binop::U, and binop::R. - const formula* unabbreviate_ltl(const formula* f); + SPOT_API const formula* unabbreviate_ltl(const formula* f); } } diff --git a/src/ltlvisit/wmunabbrev.hh b/src/ltlvisit/wmunabbrev.hh index 710a75556..49fd737b5 100644 --- a/src/ltlvisit/wmunabbrev.hh +++ b/src/ltlvisit/wmunabbrev.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012 Laboratoire de Recherche et Développement +// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -20,6 +20,8 @@ #ifndef SPOT_LTLVISIT_WMUNABBREV_HH # define SPOT_LTLVISIT_WMUNABBREV_HH +# include "misc/common.hh" + namespace spot { namespace ltl @@ -35,7 +37,7 @@ namespace spot /// a W b is replaced by b R (b | a), /// and a M b is replaced by b U (b & a). /// - const formula* unabbreviate_wm(const formula* f); + SPOT_API const formula* unabbreviate_wm(const formula* f); } } diff --git a/src/misc/common.hh b/src/misc/common.hh index 50a929507..989e9962c 100644 --- a/src/misc/common.hh +++ b/src/misc/common.hh @@ -20,6 +20,14 @@ #ifndef SPOT_MISC_COMMON_HH # define SPOT_MISC_COMMON_HH +#ifdef __GNUC__ +#define SPOT_DEPRECATED __attribute__ ((deprecated)) +#elif defined(_MSC_VER) +#define SPOT_DEPRECATED __declspec(deprecated) +#else +#define SPOT_DEPRECATED func +#endif + #if defined _WIN32 || defined __CYGWIN__ #define SPOT_HELPER_DLL_IMPORT __declspec(dllimport) #define SPOT_HELPER_DLL_EXPORT __declspec(dllexport)