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

Use -fvisibility=hidden in src/tgba/.

Browse source 
* src/tgba/Makefile.am: Use $(VISIBILITY_CXXFLAGS).
* src/tgba/bdddict.hh, src/tgba/bddprint.hh, src/tgba/formula2bdd.hh,
src/tgba/futurecondcol.hh, src/tgba/state.hh, src/tgba/statebdd.hh,
src/tgba/succiter.hh, src/tgba/succiterconcrete.hh, src/tgba/taatgba.hh,
src/tgba/tgba.hh, src/tgba/tgbabddconcrete.hh,
src/tgba/tgbabddconcretefactory.hh, src/tgba/tgbabddconcreteproduct.hh,
src/tgba/tgbabddcoredata.hh, src/tgba/tgbabddfactory.hh,
src/tgba/tgbaexplicit.hh, src/tgba/tgbakvcomplement.hh,
src/tgba/tgbaproduct.hh, src/tgba/tgbasafracomplement.hh,
src/tgba/tgbascc.hh, src/tgba/tgbasgba.hh, src/tgba/tgbatba.hh,
src/tgba/tgbaunion.hh, src/tgba/wdbacomp.hh: Mark exported symbols with
SPOT_API.
* src/tgba/public.hh: Mark the file as deprecated.
* src/tgbaalgos/cutscc.hh: Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2013-06-26 22:46:23 +02:00
parent 8ba3e64f0a
commit a12922b331
27 changed files with 152 additions and 109 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/tgba/Makefile.am
View file

@ -1,7 +1,8 @@
## Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et ## -*- coding: utf-8 -*-
## 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), ## 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. ## et Marie Curie.
## ##
## This file is part of Spot, a model checking library. ## This file is part of Spot, a model checking library.
@ -20,7 +21,7 @@
## along with this program. If not, see <http://www.gnu.org/licenses/>. ## along with this program. If not, see <http://www.gnu.org/licenses/>.
AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(BUDDY_CPPFLAGS) AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(BUDDY_CPPFLAGS)
AM_CXXFLAGS = $(WARNING_CXXFLAGS) AM_CXXFLAGS = $(WARNING_CXXFLAGS) $(VISIBILITY_CXXFLAGS)
tgbadir = $(pkgincludedir)/tgba tgbadir = $(pkgincludedir)/tgba

2
src/tgba/bdddict.hh
View file

@ -54,7 +54,7 @@ namespace spot
/// unregister_all_my_variables(), giving the same pointer. /// unregister_all_my_variables(), giving the same pointer.
/// Variables can also by unregistered one by one using /// Variables can also by unregistered one by one using
/// unregister_variable(). /// unregister_variable().
class bdd_dict class SPOT_API bdd_dict
{ {
bdd_dict_priv* priv_; bdd_dict_priv* priv_;
public: public:

48
src/tgba/bddprint.hh
View file

@ -37,8 +37,8 @@ namespace spot
/// \param os The output stream. /// \param os The output stream.
/// \param dict The dictionary to use, to lookup variables. /// \param dict The dictionary to use, to lookup variables.
/// \param b The BDD to print. /// \param b The BDD to print.
std::ostream& bdd_print_sat(std::ostream& os, SPOT_API std::ostream&
const bdd_dict* dict, bdd b); bdd_print_sat(std::ostream& os, const bdd_dict* dict, bdd b);
/// \brief Format a BDD as a list of literals. /// \brief Format a BDD as a list of literals.
/// ///
@ -46,7 +46,8 @@ namespace spot
/// \param dict The dictionary to use, to lookup variables. /// \param dict The dictionary to use, to lookup variables.
/// \param b The BDD to print. /// \param b The BDD to print.
/// \return The BDD formated as a string. /// \return The BDD formated as a string.
std::string bdd_format_sat(const bdd_dict* dict, bdd b); SPOT_API std::string
bdd_format_sat(const bdd_dict* dict, bdd b);
/// \brief Print a BDD as a list of acceptance conditions. /// \brief Print a BDD as a list of acceptance conditions.
/// ///
@ -55,8 +56,8 @@ namespace spot
/// \param dict The dictionary to use, to lookup variables. /// \param dict The dictionary to use, to lookup variables.
/// \param b The BDD to print. /// \param b The BDD to print.
/// \return The BDD formated as a string. /// \return The BDD formated as a string.
std::ostream& bdd_print_acc(std::ostream& os, SPOT_API std::ostream&
const bdd_dict* dict, bdd b); bdd_print_acc(std::ostream& os, const bdd_dict* dict, bdd b);
/// \brief Print a BDD as a set of acceptance conditions. /// \brief Print a BDD as a set of acceptance conditions.
/// ///
@ -65,8 +66,8 @@ namespace spot
/// \param dict The dictionary to use, to lookup variables. /// \param dict The dictionary to use, to lookup variables.
/// \param b The BDD to print. /// \param b The BDD to print.
/// \return The BDD formated as a string. /// \return The BDD formated as a string.
std::ostream& bdd_print_accset(std::ostream& os, SPOT_API std::ostream&
const bdd_dict* dict, bdd b); bdd_print_accset(std::ostream& os, const bdd_dict* dict, bdd b);
/// \brief Format a BDD as a set of acceptance conditions. /// \brief Format a BDD as a set of acceptance conditions.
/// ///
@ -74,55 +75,60 @@ namespace spot
/// \param dict The dictionary to use, to lookup variables. /// \param dict The dictionary to use, to lookup variables.
/// \param b The BDD to print. /// \param b The BDD to print.
/// \return The BDD formated as a string. /// \return The BDD formated as a string.
std::string bdd_format_accset(const bdd_dict* dict, bdd b); SPOT_API std::string
bdd_format_accset(const bdd_dict* dict, bdd b);
/// \brief Print a BDD as a set. /// \brief Print a BDD as a set.
/// \param os The output stream. /// \param os The output stream.
/// \param dict The dictionary to use, to lookup variables. /// \param dict The dictionary to use, to lookup variables.
/// \param b The BDD to print. /// \param b The BDD to print.
std::ostream& bdd_print_set(std::ostream& os, SPOT_API std::ostream&
const bdd_dict* dict, bdd b); bdd_print_set(std::ostream& os, const bdd_dict* dict, bdd b);
/// \brief Format a BDD as a set. /// \brief Format a BDD as a set.
/// \param dict The dictionary to use, to lookup variables. /// \param dict The dictionary to use, to lookup variables.
/// \param b The BDD to print. /// \param b The BDD to print.
/// \return The BDD formated as a string. /// \return The BDD formated as a string.
std::string bdd_format_set(const bdd_dict* dict, bdd b); SPOT_API std::string
bdd_format_set(const bdd_dict* dict, bdd b);
/// \brief Print a BDD as a formula. /// \brief Print a BDD as a formula.
/// \param os The output stream. /// \param os The output stream.
/// \param dict The dictionary to use, to lookup variables. /// \param dict The dictionary to use, to lookup variables.
/// \param b The BDD to print. /// \param b The BDD to print.
std::ostream& bdd_print_formula(std::ostream& os, SPOT_API std::ostream&
const bdd_dict* dict, bdd b); bdd_print_formula(std::ostream& os, const bdd_dict* dict, bdd b);
/// \brief Format a BDD as a formula. /// \brief Format a BDD as a formula.
/// \param dict The dictionary to use, to lookup variables. /// \param dict The dictionary to use, to lookup variables.
/// \param b The BDD to print. /// \param b The BDD to print.
/// \return The BDD formated as a string. /// \return The BDD formated as a string.
std::string bdd_format_formula(const bdd_dict* dict, bdd b); SPOT_API std::string
bdd_format_formula(const bdd_dict* dict, bdd b);
/// \brief Print a BDD as a diagram in dotty format. /// \brief Print a BDD as a diagram in dotty format.
/// \param os The output stream. /// \param os The output stream.
/// \param dict The dictionary to use, to lookup variables. /// \param dict The dictionary to use, to lookup variables.
/// \param b The BDD to print. /// \param b The BDD to print.
std::ostream& bdd_print_dot(std::ostream& os, SPOT_API std::ostream&
const bdd_dict* dict, bdd b); bdd_print_dot(std::ostream& os, const bdd_dict* dict, bdd b);
/// \brief Print a BDD as a table. /// \brief Print a BDD as a table.
/// \param os The output stream. /// \param os The output stream.
/// \param dict The dictionary to use, to lookup variables. /// \param dict The dictionary to use, to lookup variables.
/// \param b The BDD to print. /// \param b The BDD to print.
std::ostream& bdd_print_table(std::ostream& os, SPOT_API std::ostream&
const bdd_dict* dict, bdd b); bdd_print_table(std::ostream& os, const bdd_dict* dict, bdd b);
/// \brief Enable UTF-8 output for bdd printers. /// \brief Enable UTF-8 output for bdd printers.
void enable_utf8(); SPOT_API void enable_utf8();
/// \brief Format a BDD as an irredundant sum of product. /// \brief Format a BDD as an irredundant sum of product.
/// \param dict The dictionary to use, to lookup variables. /// \param dict The dictionary to use, to lookup variables.
/// \param b The BDD to print. /// \param b The BDD to print.
/// \return The BDD formated as a string. /// \return The BDD formated as a string.
std::string SPOT_API std::string
bdd_format_isop(const bdd_dict* dict, bdd b); bdd_format_isop(const bdd_dict* dict, bdd b);
@ -130,7 +136,7 @@ namespace spot
/// \param os The output stream. /// \param os The output stream.
/// \param dict The dictionary to use, to lookup variables. /// \param dict The dictionary to use, to lookup variables.
/// \param b The BDD to print. /// \param b The BDD to print.
std::ostream& SPOT_API std::ostream&
bdd_print_isop(std::ostream& os, const bdd_dict* dict, bdd b); bdd_print_isop(std::ostream& os, const bdd_dict* dict, bdd b);
} }

7
src/tgba/formula2bdd.hh
View file

@ -24,7 +24,6 @@
# define SPOT_TGBA_FORMULA2BDD_HH # define SPOT_TGBA_FORMULA2BDD_HH
# include "bdddict.hh" # include "bdddict.hh"
# include "ltlast/formula.hh"
namespace spot namespace spot
{ {
@ -39,7 +38,8 @@ namespace spot
/// passing it right away to bdd_to_formula(), you should not forget /// passing it right away to bdd_to_formula(), you should not forget
/// to unregister the variables that have been registered for \a /// to unregister the variables that have been registered for \a
/// for_me. See bdd_dict::unregister_all_my_variables(). /// for_me. See bdd_dict::unregister_all_my_variables().
bdd formula_to_bdd(const ltl::formula* f, bdd_dict* d, void* for_me); SPOT_API bdd
formula_to_bdd(const ltl::formula* f, bdd_dict* d, void* for_me);
/// \brief Convert a BDD into a formula. /// \brief Convert a BDD into a formula.
/// ///
@ -49,7 +49,8 @@ namespace spot
/// formulas, and all the BDD variables used in \a f should have /// formulas, and all the BDD variables used in \a f should have
/// been registered in \a d. Although the result has type /// been registered in \a d. Although the result has type
/// ltl::formula*, it obviously does not use any temporal operator. /// ltl::formula*, it obviously does not use any temporal operator.
const ltl::formula* bdd_to_formula(bdd f, const bdd_dict* d); SPOT_API const
ltl::formula* bdd_to_formula(bdd f, const bdd_dict* d);
} }
#endif // SPOT_TGBA_FORMULA2BDD_HH #endif // SPOT_TGBA_FORMULA2BDD_HH

6
src/tgba/futurecondcol.hh
View file

@ -1,4 +1,6 @@
// Copyright (C) 2009 Laboratoire de recherche et développement de l'Epita. // -*- coding: utf-8 -*-
// Copyright (C) 2009, 2013 Laboratoire de recherche et développement
// de l'Epita.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -32,7 +34,7 @@ namespace spot
/// This new method returns a set of conditions that can be /// This new method returns a set of conditions that can be
/// seen on a transitions accessible (maybe indirectly) from /// seen on a transitions accessible (maybe indirectly) from
/// the given state. /// the given state.
class future_conditions_collector : public tgba_scc class SPOT_API future_conditions_collector : public tgba_scc
{ {
public: public:
typedef scc_map::cond_set cond_set; typedef scc_map::cond_set cond_set;

12
src/tgba/public.hh
View file

@ -1,5 +1,8 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2013 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE).
// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), // 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. // et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -20,6 +23,13 @@
#ifndef SPOT_TGBA_PUBLIC_HH #ifndef SPOT_TGBA_PUBLIC_HH
# define SPOT_TGBA_PUBLIC_HH # define SPOT_TGBA_PUBLIC_HH
// This file should not exist.
#if __GNUC__
#ifndef SKIP_DEPRECATED_WARNING
#warning This file is deprecated. Include tgba.hh or what you need.
#endif
#endif
# include "tgba.hh" # include "tgba.hh"
# include "tgbabddconcrete.hh" # include "tgbabddconcrete.hh"
# include "tgbabddconcreteproduct.hh" # include "tgbabddconcreteproduct.hh"

3
src/tgba/state.hh
View file

@ -23,6 +23,7 @@
#ifndef SPOT_TGBA_STATE_HH #ifndef SPOT_TGBA_STATE_HH
# define SPOT_TGBA_STATE_HH # define SPOT_TGBA_STATE_HH
#include "misc/common.hh"
#include <cstddef> #include <cstddef>
#include <bdd.h> #include <bdd.h>
#include <cassert> #include <cassert>
@ -35,7 +36,7 @@ namespace spot
/// \ingroup tgba_essentials /// \ingroup tgba_essentials
/// \brief Abstract class for states. /// \brief Abstract class for states.
class state class SPOT_API state
{ {
public: public:
/// \brief Compares two states (that come from the same automaton). /// \brief Compares two states (that come from the same automaton).

7
src/tgba/statebdd.hh
View file

@ -1,5 +1,8 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2013 Laboratoire de Recherche et Développement de
// l'Epita.
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // 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. // et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -27,7 +30,7 @@ namespace spot
{ {
/// A state whose representation is a BDD. /// A state whose representation is a BDD.
/// \ingroup tgba_representation /// \ingroup tgba_representation
class state_bdd: public state class SPOT_API state_bdd: public state
{ {
public: public:
state_bdd(bdd s) state_bdd(bdd s)

5
src/tgba/succiter.hh
View file

@ -1,7 +1,8 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2011, 2013 Laboratoire de Recherche et Developpement de // Copyright (C) 2011, 2013 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE). // l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // 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. // et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -34,7 +35,7 @@ namespace spot
/// transition labels. Because transitions are never explicitely /// transition labels. Because transitions are never explicitely
/// encoded, labels (conditions and acceptance conditions) can only /// encoded, labels (conditions and acceptance conditions) can only
/// be queried while iterating over the successors. /// be queried while iterating over the successors.
class tgba_succ_iterator class SPOT_API tgba_succ_iterator
{ {
public: public:
virtual virtual

8
src/tgba/succiterconcrete.hh
View file

@ -1,5 +1,8 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2013 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // 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. // et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -28,7 +31,8 @@ namespace spot
{ {
/// A concrete iterator over successors of a TGBA state. /// A concrete iterator over successors of a TGBA state.
/// \ingroup tgba_representation /// \ingroup tgba_representation
class tgba_succ_iterator_concrete: public tgba_succ_iterator class SPOT_API tgba_succ_iterator_concrete:
public tgba_succ_iterator
{ {
public: public:
/// \brief Build a spot::tgba_succ_iterator_concrete. /// \brief Build a spot::tgba_succ_iterator_concrete.

14
src/tgba/taatgba.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2009, 2011, 2012 Laboratoire de Recherche et // Copyright (C) 2009, 2011, 2012, 2013 Laboratoire de Recherche et
// Développement de l'Epita (LRDE). // Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -32,7 +32,7 @@ namespace spot
{ {
/// \brief A self-loop Transition-based Alternating Automaton (TAA) /// \brief A self-loop Transition-based Alternating Automaton (TAA)
/// which is seen as a TGBA (abstract class, see below). /// which is seen as a TGBA (abstract class, see below).
class taa_tgba : public tgba class SPOT_API taa_tgba : public tgba
{ {
public: public:
taa_tgba(bdd_dict* dict); taa_tgba(bdd_dict* dict);
@ -83,7 +83,7 @@ namespace spot
}; };
/// Set of states deriving from spot::state. /// Set of states deriving from spot::state.
class state_set : public spot::state class SPOT_API state_set : public spot::state
{ {
public: public:
state_set(const taa_tgba::state_set* s, bool delete_me = false) state_set(const taa_tgba::state_set* s, bool delete_me = false)
@ -107,7 +107,7 @@ namespace spot
bool delete_me_; bool delete_me_;
}; };
class taa_succ_iterator : public tgba_succ_iterator class SPOT_API taa_succ_iterator : public tgba_succ_iterator
{ {
public: public:
taa_succ_iterator(const taa_tgba::state_set* s, bdd all_acc); taa_succ_iterator(const taa_tgba::state_set* s, bdd all_acc);
@ -152,7 +152,7 @@ namespace spot
/// A taa_tgba instance with states labeled by a given type. /// A taa_tgba instance with states labeled by a given type.
/// Still an abstract class, see below. /// Still an abstract class, see below.
template<typename label, typename label_hash> template<typename label, typename label_hash>
class taa_tgba_labelled : public taa_tgba class SPOT_API taa_tgba_labelled : public taa_tgba
{ {
public: public:
taa_tgba_labelled(bdd_dict* dict) : taa_tgba(dict) {}; taa_tgba_labelled(bdd_dict* dict) : taa_tgba(dict) {};
@ -324,7 +324,7 @@ namespace spot
} }
}; };
class taa_tgba_string : class SPOT_API taa_tgba_string :
public taa_tgba_labelled<std::string, string_hash> public taa_tgba_labelled<std::string, string_hash>
{ {
public: public:
@ -336,7 +336,7 @@ namespace spot
virtual std::string clone_if(const std::string& label) const; virtual std::string clone_if(const std::string& label) const;
}; };
class taa_tgba_formula : class SPOT_API taa_tgba_formula :
public taa_tgba_labelled<const ltl::formula*, ltl::formula_ptr_hash> public taa_tgba_labelled<const ltl::formula*, ltl::formula_ptr_hash>
{ {
public: public:

2
src/tgba/tgba.hh
View file

@ -64,7 +64,7 @@ namespace spot
/// we never represent transitions! Transition informations are /// we never represent transitions! Transition informations are
/// obtained by querying the iterator over the successors of /// obtained by querying the iterator over the successors of
/// a state. /// a state.
class tgba class SPOT_API tgba
{ {
protected: protected:
tgba(); tgba();

4
src/tgba/tgbabddconcrete.hh
View file

@ -1,4 +1,4 @@
// Copyright (C) 2011 Laboratoire de Recherche et Développement // Copyright (C) 2011, 2013 Laboratoire de Recherche et Développement
// de l'Epita (LRDE). // de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris // Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@ -31,7 +31,7 @@ namespace spot
{ {
/// \ingroup tgba_representation /// \ingroup tgba_representation
/// \brief A concrete spot::tgba implemented using BDDs. /// \brief A concrete spot::tgba implemented using BDDs.
class tgba_bdd_concrete: public tgba class SPOT_API tgba_bdd_concrete: public tgba
{ {
public: public:
/// \brief Construct a tgba_bdd_concrete with unknown initial state. /// \brief Construct a tgba_bdd_concrete with unknown initial state.

7
src/tgba/tgbabddconcretefactory.hh
View file

@ -1,7 +1,8 @@
// Copyright (C) 2008 Laboratoire de Recherche et Développement // -*- coding: utf-8 -*-
// Copyright (C) 2008, 2013 Laboratoire de Recherche et Développement
// de l'Epita (LRDE). // de l'Epita (LRDE).
// Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003, 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. // et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -29,7 +30,7 @@
namespace spot namespace spot
{ {
/// Helper class to build a spot::tgba_bdd_concrete object. /// Helper class to build a spot::tgba_bdd_concrete object.
class tgba_bdd_concrete_factory: public tgba_bdd_factory class SPOT_API tgba_bdd_concrete_factory: public tgba_bdd_factory
{ {
public: public:
tgba_bdd_concrete_factory(bdd_dict* dict); tgba_bdd_concrete_factory(bdd_dict* dict);

4
src/tgba/tgbabddconcreteproduct.hh
View file

@ -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 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
@ -29,7 +29,7 @@ namespace spot
/// ///
/// This function builds the resulting product as another /// This function builds the resulting product as another
/// spot::tgba_bdd_concrete automaton. /// spot::tgba_bdd_concrete automaton.
tgba_bdd_concrete* SPOT_API tgba_bdd_concrete*
product(const tgba_bdd_concrete* left, const tgba_bdd_concrete* right); product(const tgba_bdd_concrete* left, const tgba_bdd_concrete* right);
} }

11
src/tgba/tgbabddcoredata.hh
View file

@ -1,7 +1,8 @@
// Copyright (C) 2009, 2011, 2012 Laboratoire de Recherche et // -*- coding: utf-8 -*-
// Développement de l'Epita (LRDE). // Copyright (C) 2009, 2011, 2012, 2013 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003, 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. // et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -28,7 +29,7 @@
namespace spot namespace spot
{ {
/// Core data for a TGBA encoded using BDDs. /// Core data for a TGBA encoded using BDDs.
struct tgba_bdd_core_data struct SPOT_API tgba_bdd_core_data
{ {
/// \brief encodes the transition relation of the TGBA. /// \brief encodes the transition relation of the TGBA.
/// ///
@ -42,7 +43,7 @@ namespace spot
/// \brief encodes the acceptance conditions /// \brief encodes the acceptance conditions
/// ///
/// <tt>a U b</tt>, or <tt>F b</tt>, both imply that \c b should /// <tt>a U b</tt>, or <tt>F b</tt>, both imply that \c b should
/// be verified eventually. We encode this with generalized Büchi /// be verified eventually. We encode this with generalized Büchi
/// acceptating conditions. An acceptance set, called /// acceptating conditions. An acceptance set, called
/// <tt>Acc[b]</tt>, hold all the state that do not promise to /// <tt>Acc[b]</tt>, hold all the state that do not promise to
/// verify \c b eventually. (I.e., all the states that contain \c /// verify \c b eventually. (I.e., all the states that contain \c

7
src/tgba/tgbabddfactory.hh
View file

@ -1,5 +1,8 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2013 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE).
// Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003, 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. // et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -28,7 +31,7 @@ namespace spot
/// ///
/// A spot::tgba_bdd_concrete can be constructed from anything that /// A spot::tgba_bdd_concrete can be constructed from anything that
/// supplies core data and their associated dictionary. /// supplies core data and their associated dictionary.
class tgba_bdd_factory class SPOT_API tgba_bdd_factory
{ {
public: public:
virtual ~tgba_bdd_factory() {} virtual ~tgba_bdd_factory() {}

29
src/tgba/tgbaexplicit.hh
View file

@ -38,7 +38,7 @@ namespace spot
{ {
// How to destroy the label of a state. // How to destroy the label of a state.
template<typename T> template<typename T>
struct destroy_key struct SPOT_API destroy_key
{ {
void destroy(T t) void destroy(T t)
{ {
@ -47,7 +47,7 @@ namespace spot
}; };
template<> template<>
struct destroy_key<const ltl::formula*> struct SPOT_API destroy_key<const ltl::formula*>
{ {
void destroy(const ltl::formula* t) void destroy(const ltl::formula* t)
{ {
@ -58,7 +58,7 @@ namespace spot
/// States used by spot::explicit_graph implementation /// States used by spot::explicit_graph implementation
/// \ingroup tgba_representation /// \ingroup tgba_representation
template<typename Label, typename label_hash> template<typename Label, typename label_hash>
class state_explicit: public spot::state class SPOT_API state_explicit: public spot::state
{ {
public: public:
state_explicit() state_explicit()
@ -133,7 +133,7 @@ namespace spot
/// States labeled by an int /// States labeled by an int
/// \ingroup tgba_representation /// \ingroup tgba_representation
class state_explicit_number: class SPOT_API state_explicit_number:
public state_explicit<int, identity_hash<int> > public state_explicit<int, identity_hash<int> >
{ {
public: public:
@ -152,7 +152,7 @@ namespace spot
/// States labeled by a string /// States labeled by a string
/// \ingroup tgba_representation /// \ingroup tgba_representation
class state_explicit_string: class SPOT_API state_explicit_string:
public state_explicit<std::string, string_hash> public state_explicit<std::string, string_hash>
{ {
public: public:
@ -171,7 +171,7 @@ namespace spot
/// States labeled by a formula /// States labeled by a formula
/// \ingroup tgba_representation /// \ingroup tgba_representation
class state_explicit_formula: class SPOT_API state_explicit_formula:
public state_explicit<const ltl::formula*, ltl::formula_ptr_hash> public state_explicit<const ltl::formula*, ltl::formula_ptr_hash>
{ {
public: public:
@ -191,7 +191,8 @@ namespace spot
/// Successor iterators used by spot::tgba_explicit. /// Successor iterators used by spot::tgba_explicit.
/// \ingroup tgba_representation /// \ingroup tgba_representation
template<typename State> template<typename State>
class tgba_explicit_succ_iterator: public tgba_succ_iterator class SPOT_API tgba_explicit_succ_iterator:
public tgba_succ_iterator
{ {
public: public:
tgba_explicit_succ_iterator(const State* start, tgba_explicit_succ_iterator(const State* start,
@ -251,7 +252,7 @@ namespace spot
/// Graph implementation for explicit automaton /// Graph implementation for explicit automaton
/// \ingroup tgba_representation /// \ingroup tgba_representation
template<typename State, typename Type> template<typename State, typename Type>
class explicit_graph: public Type class SPOT_API explicit_graph: public Type
{ {
public: public:
typedef typename State::label_t label_t; typedef typename State::label_t label_t;
@ -694,7 +695,8 @@ namespace spot
}; };
template <typename State> template <typename State>
class tgba_explicit: public explicit_graph<State, tgba> class SPOT_API tgba_explicit:
public explicit_graph<State, tgba>
{ {
public: public:
tgba_explicit(bdd_dict* dict): explicit_graph<State, tgba>(dict) tgba_explicit(bdd_dict* dict): explicit_graph<State, tgba>(dict)
@ -712,7 +714,8 @@ namespace spot
}; };
template <typename State> template <typename State>
class sba_explicit: public explicit_graph<State, sba> class SPOT_API sba_explicit:
public explicit_graph<State, sba>
{ {
public: public:
sba_explicit(bdd_dict* dict): explicit_graph<State, sba>(dict) sba_explicit(bdd_dict* dict): explicit_graph<State, sba>(dict)
@ -752,7 +755,7 @@ namespace spot
/// Configuration of graph automata /// Configuration of graph automata
/// \ingroup tgba_representation /// \ingroup tgba_representation
template<class graph, typename Type> template<class graph, typename Type>
class explicit_conf: public graph class SPOT_API explicit_conf: public graph
{ {
public: public:
explicit_conf(bdd_dict* d): graph(d) explicit_conf(bdd_dict* d): graph(d)
@ -769,7 +772,7 @@ namespace spot
}; };
template<class graph> template<class graph>
class explicit_conf<graph, state_explicit_string>: public graph class SPOT_API explicit_conf<graph, state_explicit_string>: public graph
{ {
public: public:
explicit_conf(bdd_dict* d): graph(d) explicit_conf(bdd_dict* d): graph(d)
@ -784,7 +787,7 @@ namespace spot
}; };
template<class graph> template<class graph>
class explicit_conf<graph, state_explicit_formula>: public graph class SPOT_API explicit_conf<graph, state_explicit_formula>: public graph
{ {
public: public:
explicit_conf(bdd_dict* d): graph(d) explicit_conf(bdd_dict* d): graph(d)

6
src/tgba/tgbakvcomplement.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- 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). // Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -27,7 +27,7 @@
namespace spot namespace spot
{ {
class bdd_ordered class SPOT_API bdd_ordered
{ {
public: public:
bdd_ordered() bdd_ordered()
@ -83,7 +83,7 @@ namespace spot
/// The construction is done on-the-fly, by the /// The construction is done on-the-fly, by the
/// \c tgba_kv_complement_succ_iterator class. /// \c tgba_kv_complement_succ_iterator class.
/// \see tgba_kv_complement_succ_iterator /// \see tgba_kv_complement_succ_iterator
class tgba_kv_complement : public tgba class SPOT_API tgba_kv_complement : public tgba
{ {
public: public:
tgba_kv_complement(const tgba* a); tgba_kv_complement(const tgba* a);

13
src/tgba/tgbaproduct.hh
View file

@ -1,8 +1,9 @@
// Copyright (C) 2011 Laboratoire de Recherche et Développement // -*- coding: utf-8 -*-
// Copyright (C) 2011, 2013 Laboratoire de Recherche et Développement
// de l'Epita (LRDE). // de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris // Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie. // Université Pierre et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -33,7 +34,7 @@ namespace spot
/// ///
/// This state is in fact a pair of state: the state from the left /// This state is in fact a pair of state: the state from the left
/// automaton and that of the right. /// automaton and that of the right.
class state_product : public state class SPOT_API state_product : public state
{ {
public: public:
/// \brief Constructor /// \brief Constructor
@ -77,7 +78,7 @@ namespace spot
/// \brief A lazy product. (States are computed on the fly.) /// \brief A lazy product. (States are computed on the fly.)
class tgba_product: public tgba class SPOT_API tgba_product: public tgba
{ {
public: public:
/// \brief Constructor. /// \brief Constructor.
@ -130,7 +131,7 @@ namespace spot
}; };
/// \brief A lazy product with different initial states. /// \brief A lazy product with different initial states.
class tgba_product_init: public tgba_product class SPOT_API tgba_product_init: public tgba_product
{ {
public: public:
tgba_product_init(const tgba* left, const tgba* right, tgba_product_init(const tgba* left, const tgba* right,

16
src/tgba/tgbasafracomplement.hh
View file

@ -1,5 +1,6 @@
// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement // -*- coding: utf-8 -*-
// de l'Epita (LRDE). // Copyright (C) 2009, 2010, 2011, 2013 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -20,7 +21,7 @@
# define SPOT_TGBA_TGBASAFRACOMPLEMENT_HH # define SPOT_TGBA_TGBASAFRACOMPLEMENT_HH
# include <vector> # include <vector>
# include "tgba/tgba.hh" # include "tgba.hh"
#ifndef TRANSFORM_TO_TBA #ifndef TRANSFORM_TO_TBA
# define TRANSFORM_TO_TBA 0 # define TRANSFORM_TO_TBA 0
@ -40,13 +41,13 @@ namespace spot
/// 2. Interpreting this deterministic Rabin automaton as a /// 2. Interpreting this deterministic Rabin automaton as a
/// deterministic Streett will produce a complemented automaton. /// deterministic Streett will produce a complemented automaton.
/// 3. Then we use a transformation from deterministic Streett /// 3. Then we use a transformation from deterministic Streett
/// automaton to nondeterministic Büchi automaton. /// automaton to nondeterministic Büchi automaton.
/// ///
/// Safra construction is done in \a tgba_complement, the transformation /// Safra construction is done in \a tgba_complement, the transformation
/// is done on-the-fly when successors are called. /// is done on-the-fly when successors are called.
/// ///
/// \sa safra_determinisation, tgba_safra_complement::succ_iter. /// \sa safra_determinisation, tgba_safra_complement::succ_iter.
class tgba_safra_complement : public tgba class SPOT_API tgba_safra_complement : public tgba
{ {
public: public:
tgba_safra_complement(const tgba* a); tgba_safra_complement(const tgba* a);
@ -89,10 +90,9 @@ namespace spot
/// \brief Produce a dot output of the Safra automaton associated /// \brief Produce a dot output of the Safra automaton associated
/// to \a a. /// to \a a.
/// ///
/// @param a The \c tgba_safra_complement with an intermediate Safra /// \param a The \c tgba_safra_complement with an intermediate Safra
/// automaton to display /// automaton to display
/// void SPOT_API display_safra(const tgba_safra_complement* a);
void display_safra(const tgba_safra_complement* a);
} }
#endif // SPOT_TGBA_TGBASAFRACOMPLEMENT_HH #endif // SPOT_TGBA_TGBASAFRACOMPLEMENT_HH

6
src/tgba/tgbascc.hh
View file

@ -1,4 +1,6 @@
// Copyright (C) 2009 Laboratoire de recherche et développement de l'Epita. // -*- coding: utf-8 -*-
// Copyright (C) 2009, 2013 Laboratoire de recherche et développement
// de l'Epita.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -30,7 +32,7 @@ namespace spot
/// ///
/// This class is a spot::tgba wrapper that simply add a new method /// This class is a spot::tgba wrapper that simply add a new method
/// scc_of_state() to retrieve the number of a SCC a state belongs to. /// scc_of_state() to retrieve the number of a SCC a state belongs to.
class tgba_scc : public tgba class SPOT_API tgba_scc : public tgba
{ {
public: public:
/// \brief Create a tgba_scc wrapper for \a aut. /// \brief Create a tgba_scc wrapper for \a aut.

4
src/tgba/tgbasgba.hh
View file

@ -1,4 +1,4 @@
// Copyright (C) 2009 Laboratoire de Recherche et Développement // Copyright (C) 2009, 2013 Laboratoire de Recherche et Développement
// de l'Epita (LRDE). // de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -32,7 +32,7 @@ namespace spot
/// This class acts as a proxy in front of a spot::tgba, that should /// This class acts as a proxy in front of a spot::tgba, that should
/// label on states on-the-fly. The result is still a spot::tgba, /// label on states on-the-fly. The result is still a spot::tgba,
/// but acceptances conditions are also on states. /// but acceptances conditions are also on states.
class tgba_sgba_proxy : public tgba class SPOT_API tgba_sgba_proxy : public tgba
{ {
public: public:
tgba_sgba_proxy(const tgba* a, bool no_zero_acc = true); tgba_sgba_proxy(const tgba* a, bool no_zero_acc = true);

4
src/tgba/tgbatba.hh
View file

@ -49,7 +49,7 @@ namespace spot
/// transitions. /// transitions.
/// ///
/// \see tgba_sba_proxy /// \see tgba_sba_proxy
class tgba_tba_proxy : public tgba class SPOT_API tgba_tba_proxy : public tgba
{ {
public: public:
tgba_tba_proxy(const tgba* a); tgba_tba_proxy(const tgba* a);
@ -147,7 +147,7 @@ namespace spot
/// one. /// one.
/// ///
/// \see degeneralize /// \see degeneralize
class tgba_sba_proxy : public tgba_tba_proxy class SPOT_API tgba_sba_proxy : public tgba_tba_proxy
{ {
public: public:
tgba_sba_proxy(const tgba* a); tgba_sba_proxy(const tgba* a);

11
src/tgba/tgbaunion.hh
View file

@ -1,5 +1,6 @@
// Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement // -*- coding: utf-8 -*-
// de l'Epita (LRDE). // Copyright (C) 2009, 2011, 2013 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -32,7 +33,7 @@ namespace spot
/// If the first member is different from 0 and the second is 0, /// If the first member is different from 0 and the second is 0,
/// the state belongs to the right automaton. /// the state belongs to the right automaton.
/// If both members are 0, the state is the initial state. /// If both members are 0, the state is the initial state.
class state_union : public state class SPOT_API state_union : public state
{ {
public: public:
/// \brief Constructor /// \brief Constructor
@ -75,7 +76,7 @@ namespace spot
}; };
/// \brief Iterate over the successors of an union computed on the fly. /// \brief Iterate over the successors of an union computed on the fly.
class tgba_succ_iterator_union: public tgba_succ_iterator class SPOT_API tgba_succ_iterator_union: public tgba_succ_iterator
{ {
public: public:
tgba_succ_iterator_union(tgba_succ_iterator* left, tgba_succ_iterator_union(tgba_succ_iterator* left,
@ -107,7 +108,7 @@ namespace spot
}; };
/// \brief A lazy union. (States are computed on the fly.) /// \brief A lazy union. (States are computed on the fly.)
class tgba_union: public tgba class SPOT_API tgba_union: public tgba
{ {
public: public:
/// \brief Constructor. /// \brief Constructor.

12
src/tgba/wdbacomp.hh
View file

@ -1,5 +1,6 @@
// Copyright (C) 2011 Laboratoire de Recherche et Développement de // -*- coding: utf-8 -*-
// l'Epita. // Copyright (C) 2011, 2013 Laboratoire de Recherche et Développement
// de l'Epita.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -24,10 +25,11 @@
namespace spot namespace spot
{ {
/// \ingroup tgba_on_the_fly_algorithms /// \ingroup tgba_on_the_fly_algorithms
/// \brief Complement a weak deterministic Büchi automaton /// \brief Complement a weak deterministic Büchi automaton
/// \param aut a weak deterministic Büchi automaton to complement /// \param aut a weak deterministic Büchi automaton to complement
/// \return a new automaton that recognizes the complement language /// \return a new automaton that recognizes the complement language
tgba* wdba_complement(const tgba* aut); SPOT_API tgba*
wdba_complement(const tgba* aut);
} }
#endif #endif

4
src/tgbaalgos/cutscc.hh
View file

@ -1,4 +1,4 @@
// Copyright (C) 2009 Laboratoire de Recherche et Developpement de // Copyright (C) 2009, 2013 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE). // l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -23,7 +23,7 @@
#include <iosfwd> #include <iosfwd>
#include <set> #include <set>
#include <vector> #include <vector>
#include "tgba/public.hh" #include "tgba/tgba.hh"
#include "tgbaalgos/scc.hh" #include "tgbaalgos/scc.hh"
namespace spot namespace spot