diff --git a/src/ta/Makefile.am b/src/ta/Makefile.am
index b22efcb86..ab2a121a3 100644
--- a/src/ta/Makefile.am
+++ b/src/ta/Makefile.am
@@ -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).
##
## This file is part of Spot, a model checking library.
##
@@ -18,7 +18,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)
tadir = $(pkgincludedir)/ta
diff --git a/src/ta/ta.hh b/src/ta/ta.hh
index 3a1066baa..eebf71e84 100644
--- a/src/ta/ta.hh
+++ b/src/ta/ta.hh
@@ -1,5 +1,6 @@
-// Copyright (C) 2010, 2012 Laboratoire de Recherche et Developpement
-// de l Epita (LRDE).
+// -*- coding: utf-8 -*-
+// Copyright (C) 2010, 2012, 2013 Laboratoire de Recherche et
+// Developpement de l Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@@ -50,7 +51,7 @@ namespace spot
/// The Testing Automata (TA) were introduced by
/// Henri Hansen, Wojciech Penczek and Antti Valmari
/// in "Stuttering-insensitive automata for on-the-fly detection of livelock
- /// properties" In Proc. of FMICSÕ02, vol. 66(2) of Electronic Notes in
+ /// properties" In Proc. of FMICSÕ02, vol. 66(2) of Electronic Notes in
/// Theoretical Computer Science.Elsevier.
///
/// While a TGBA automaton observes the value of the atomic propositions, the
@@ -74,7 +75,7 @@ namespace spot
/// obtained by querying the iterator over the successors of
/// a state.
- class ta
+ class SPOT_API ta
{
public:
diff --git a/src/ta/taexplicit.hh b/src/ta/taexplicit.hh
index a6516b987..6b45a778f 100644
--- a/src/ta/taexplicit.hh
+++ b/src/ta/taexplicit.hh
@@ -38,7 +38,7 @@ namespace spot
/// Explicit representation of a spot::ta.
/// \ingroup ta_representation
- class ta_explicit : public ta
+ class SPOT_API ta_explicit : public ta
{
public:
ta_explicit(const tgba* tgba, bdd all_acceptance_conditions,
@@ -146,7 +146,7 @@ namespace spot
/// states used by spot::ta_explicit.
/// \ingroup ta_representation
- class state_ta_explicit : public spot::state
+ class SPOT_API state_ta_explicit : public spot::state
{
#ifndef SWIG
public:
@@ -241,7 +241,7 @@ namespace spot
};
/// Successor iterators used by spot::ta_explicit.
- class ta_explicit_succ_iterator : public ta_succ_iterator
+ class SPOT_API ta_explicit_succ_iterator : public ta_succ_iterator
{
public:
ta_explicit_succ_iterator(const state_ta_explicit* s);
diff --git a/src/ta/taproduct.hh b/src/ta/taproduct.hh
index b1352a84b..311e804e4 100644
--- a/src/ta/taproduct.hh
+++ b/src/ta/taproduct.hh
@@ -31,7 +31,7 @@ namespace spot
///
/// This state is in fact a pair of state: the state from the TA
/// automaton and that of Kripke structure.
- class state_ta_product : public state
+ class SPOT_API state_ta_product : public state
{
public:
/// \brief Constructor
@@ -73,7 +73,7 @@ namespace spot
};
/// \brief Iterate over the successors of a product computed on the fly.
- class ta_succ_iterator_product : public ta_succ_iterator
+ class SPOT_API ta_succ_iterator_product : public ta_succ_iterator
{
public:
ta_succ_iterator_product(const state_ta_product* s, const ta* t,
@@ -135,7 +135,7 @@ namespace spot
/// \ingroup ta_emptiness_check
/// \brief A lazy product between a Testing automaton and a Kripke structure.
/// (States are computed on the fly.)
- class ta_product : public ta
+ class SPOT_API ta_product: public ta
{
public:
/// \brief Constructor.
@@ -208,21 +208,17 @@ namespace spot
};
- class ta_succ_iterator_product_by_changeset : public ta_succ_iterator_product
+ class SPOT_API ta_succ_iterator_product_by_changeset :
+ public ta_succ_iterator_product
{
public:
ta_succ_iterator_product_by_changeset(const state_ta_product* s,
- const ta* t, const kripke* k, bdd changeset);
-
-
-
- /// \brief Move to the next successor in the kripke structure
- void
- next_kripke_dest();
-
-
- };
+ const ta* t, const kripke* k,
+ bdd changeset);
+ /// \brief Move to the next successor in the Kripke structure
+ void next_kripke_dest();
+ };
}
diff --git a/src/ta/tgta.hh b/src/ta/tgta.hh
index 5114f62b6..20446a28d 100644
--- a/src/ta/tgta.hh
+++ b/src/ta/tgta.hh
@@ -1,3 +1,4 @@
+// -*- coding: utf-8 -*-
// Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
@@ -57,7 +58,7 @@ namespace spot
/// a state.
- class tgta : public tgba
+ class SPOT_API tgta : public tgba
{
protected:
diff --git a/src/ta/tgtaexplicit.hh b/src/ta/tgtaexplicit.hh
index a9374e5f6..34a66b7b3 100644
--- a/src/ta/tgtaexplicit.hh
+++ b/src/ta/tgtaexplicit.hh
@@ -1,4 +1,5 @@
-// Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et
+// -*- 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.
@@ -34,7 +35,7 @@ namespace spot
/// Explicit representation of a spot::tgta.
/// \ingroup ta_representation
- class tgta_explicit : public tgta
+ class SPOT_API tgta_explicit : public tgta
{
public:
tgta_explicit(const tgba* tgba, bdd all_acceptance_conditions,
diff --git a/src/ta/tgtaproduct.hh b/src/ta/tgtaproduct.hh
index 33860213c..58aa364af 100644
--- a/src/ta/tgtaproduct.hh
+++ b/src/ta/tgtaproduct.hh
@@ -1,9 +1,6 @@
// -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement
+// Copyright (C) 2011, 2012, 2013 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
-// Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris
-// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
-// Université Pierre et Marie Curie.
//
// This file is part of Spot, a model checking library.
//
@@ -33,7 +30,7 @@ namespace spot
{
/// \brief A lazy product. (States are computed on the fly.)
- class tgta_product : public tgba_product
+ class SPOT_API tgta_product : public tgba_product
{
public:
tgta_product(const kripke* left, const tgta* right);
@@ -47,7 +44,7 @@ namespace spot
};
/// \brief Iterate over the successors of a product computed on the fly.
- class tgta_succ_iterator_product : public tgba_succ_iterator
+ class SPOT_API tgta_succ_iterator_product : public tgba_succ_iterator
{
public:
tgta_succ_iterator_product(const state_product* s, const kripke* k,
diff --git a/src/taalgos/Makefile.am b/src/taalgos/Makefile.am
index 465ecff90..750bcbc25 100644
--- a/src/taalgos/Makefile.am
+++ b/src/taalgos/Makefile.am
@@ -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).
##
## This file is part of Spot, a model checking library.et Marie Curie.
##
@@ -19,7 +19,7 @@
AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(BUDDY_CPPFLAGS)
-AM_CXXFLAGS = $(WARNING_CXXFLAGS)
+AM_CXXFLAGS = $(WARNING_CXXFLAGS) $(VISIBILITY_CXXFLAGS)
taalgosdir = $(pkgincludedir)/taalgos
diff --git a/src/taalgos/dotty.hh b/src/taalgos/dotty.hh
index 33726bc36..8629239e8 100644
--- a/src/taalgos/dotty.hh
+++ b/src/taalgos/dotty.hh
@@ -1,5 +1,6 @@
-// Copyright (C) 2010 Laboratoire de Recherche et Developpement
-// de l Epita (LRDE).
+// -*- coding: utf-8 -*-
+// Copyright (C) 2010, 2013 Laboratoire de Recherche et Développement
+// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@@ -26,7 +27,7 @@ namespace spot
{
class ta;
- std::ostream&
+ SPOT_API std::ostream&
dotty_reachable(std::ostream& os, const ta* a);
}
diff --git a/src/taalgos/emptinessta.hh b/src/taalgos/emptinessta.hh
index 6c754b5bb..733b93da8 100644
--- a/src/taalgos/emptinessta.hh
+++ b/src/taalgos/emptinessta.hh
@@ -85,7 +85,7 @@ namespace spot
/// between a TA and a Kripke structure
///
/// See the paper cited above.
- class ta_check : public ec_statistics
+ class SPOT_API ta_check : public ec_statistics
{
public:
ta_check(const ta_product* a, option_map o = option_map());
diff --git a/src/taalgos/minimize.hh b/src/taalgos/minimize.hh
index 14e59fe03..2d9a81814 100644
--- a/src/taalgos/minimize.hh
+++ b/src/taalgos/minimize.hh
@@ -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).
//
// This file is part of Spot, a model checking library.
//
@@ -56,7 +56,7 @@ namespace spot
\endverbatim */
///
/// \param ta_ the TA automaton to convert into a simplified TA
- ta*
+ SPOT_API ta*
minimize_ta(const ta* ta_);
@@ -70,7 +70,7 @@ namespace spot
/// the acceptance conditions of the outgoing transitions.
///
/// \param tgta_ the TGTA automaton to convert into a simplified TGTA
- tgta_explicit*
+ SPOT_API tgta_explicit*
minimize_tgta(const tgta_explicit* tgta_);
/// @}
diff --git a/src/taalgos/reachiter.hh b/src/taalgos/reachiter.hh
index e8d77b486..f1a428056 100644
--- a/src/taalgos/reachiter.hh
+++ b/src/taalgos/reachiter.hh
@@ -29,7 +29,7 @@ namespace spot
{
/// \ingroup ta_generic
/// \brief Iterate over all reachable states of a spot::ta.
- class ta_reachable_iterator
+ class SPOT_API ta_reachable_iterator
{
public:
ta_reachable_iterator(const ta* a);
@@ -97,7 +97,8 @@ namespace spot
/// \ingroup ta_generic
/// \brief An implementation of spot::ta_reachable_iterator that browses
/// states depth first.
- class ta_reachable_iterator_depth_first : public ta_reachable_iterator
+ class SPOT_API ta_reachable_iterator_depth_first
+ : public ta_reachable_iterator
{
public:
ta_reachable_iterator_depth_first(const ta* a);
@@ -114,7 +115,8 @@ namespace spot
/// \ingroup ta_generic
/// \brief An implementation of spot::ta_reachable_iterator that browses
/// states breadth first.
- class ta_reachable_iterator_breadth_first : public ta_reachable_iterator
+ class SPOT_API ta_reachable_iterator_breadth_first
+ : public ta_reachable_iterator
{
public:
ta_reachable_iterator_breadth_first(const ta* a);
diff --git a/src/taalgos/statessetbuilder.hh b/src/taalgos/statessetbuilder.hh
index aebd7e2d4..2bdd215e6 100644
--- a/src/taalgos/statessetbuilder.hh
+++ b/src/taalgos/statessetbuilder.hh
@@ -1,4 +1,5 @@
-// Copyright (C) 2010 Laboratoire de Recherche et Développement
+// -*- coding: utf-8 -*-
+// Copyright (C) 2010, 2013 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@@ -25,7 +26,7 @@ namespace spot
{
/// \brief Compute states set for an automaton.
- std::set get_states_set(const ta* t);
+ SPOT_API std::set get_states_set(const ta* t);
/// @}
}
diff --git a/src/taalgos/stats.hh b/src/taalgos/stats.hh
index d3fd305d6..3c19ca3f5 100644
--- a/src/taalgos/stats.hh
+++ b/src/taalgos/stats.hh
@@ -1,8 +1,6 @@
-// Copyright (C) 2008 Laboratoire de Recherche et Développement
+// -*- coding: utf-8 -*-
+// Copyright (C) 2011, 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.
//
// This file is part of Spot, a model checking library.
//
@@ -31,7 +29,7 @@ namespace spot
/// \addtogroup ta_misc
/// @{
- struct ta_statistics
+ struct SPOT_API ta_statistics
{
unsigned transitions;
unsigned states;
@@ -41,7 +39,7 @@ namespace spot
};
/// \brief Compute statistics for an automaton.
- ta_statistics stats_reachable(const ta* t);
+ SPOT_API ta_statistics stats_reachable(const ta* t);
/// @}
}
diff --git a/src/taalgos/tgba2ta.hh b/src/taalgos/tgba2ta.hh
index 8ad468034..babc69e2b 100644
--- a/src/taalgos/tgba2ta.hh
+++ b/src/taalgos/tgba2ta.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).
//
// This file is part of Spot, a model checking library.
//
@@ -79,7 +79,7 @@ namespace spot
///
/// \return A spot::ta_explicit that recognizes the same language as the
/// TGBA \a tgba_to_convert.
- ta_explicit*
+ SPOT_API ta_explicit*
tgba_to_ta(const tgba* tgba_to_convert, bdd atomic_propositions_set,
bool degeneralized = true, bool artificial_initial_state_mode = true,
bool single_pass_emptiness_check = false,
@@ -94,7 +94,7 @@ namespace spot
///
/// \return A spot::tgta_explicit (spot::tgta) that recognizes the same
/// language as the TGBA \a tgba_to_convert.
- tgta_explicit*
+ SPOT_API tgta_explicit*
tgba_to_tgta(const tgba* tgba_to_convert, bdd atomic_propositions_set);
}