From a0f5d53ea4a26baa1be067a2febba822ee9194d0 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 28 Jun 2013 17:34:20 +0200 Subject: [PATCH] Use -fvisibility=hidden in src/tgbaalgos/. * src/tgbaalgos/Makefile.am, src/tgbaalgos/gtec/Makefile.am: Add $(VISIBILITY_CXXFLAGS). * src/tgbaalgos/bfssteps.hh, src/tgbaalgos/compsusp.hh, src/tgbaalgos/cutscc.hh, src/tgbaalgos/cycles.hh, src/tgbaalgos/degen.hh, src/tgbaalgos/dotty.hh, src/tgbaalgos/dottydec.hh, src/tgbaalgos/dupexp.hh, src/tgbaalgos/eltl2tgba_lacim.hh, src/tgbaalgos/emptiness.hh, src/tgbaalgos/gtec/ce.hh, src/tgbaalgos/gtec/explscc.hh, src/tgbaalgos/gtec/gtec.hh, src/tgbaalgos/gtec/nsheap.hh, src/tgbaalgos/gtec/sccstack.hh, src/tgbaalgos/gtec/status.hh, src/tgbaalgos/gv04.hh, src/tgbaalgos/isdet.hh, src/tgbaalgos/isweakscc.cc, src/tgbaalgos/isweakscc.hh, src/tgbaalgos/lbtt.hh, src/tgbaalgos/ltl2taa.hh, src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_lacim.hh, src/tgbaalgos/magic.hh, src/tgbaalgos/minimize.hh, src/tgbaalgos/neverclaim.hh, src/tgbaalgos/postproc.hh, src/tgbaalgos/powerset.hh, src/tgbaalgos/projrun.hh, src/tgbaalgos/randomgraph.hh, src/tgbaalgos/reachiter.hh, src/tgbaalgos/reducerun.hh, src/tgbaalgos/reductgba_sim.cc, src/tgbaalgos/reductgba_sim.hh, src/tgbaalgos/replayrun.hh, src/tgbaalgos/rundotdec.hh, src/tgbaalgos/safety.hh, src/tgbaalgos/save.hh, src/tgbaalgos/scc.hh, src/tgbaalgos/sccfilter.hh, src/tgbaalgos/se05.hh, src/tgbaalgos/simulation.hh, src/tgbaalgos/stats.hh, src/tgbaalgos/stripacc.hh, src/tgbaalgos/tau03.hh, src/tgbaalgos/tau03opt.hh, src/tgbaalgos/translate.hh: Mark public symbol with SPOT_API. --- src/tgbaalgos/Makefile.am | 2 +- src/tgbaalgos/bfssteps.hh | 7 ++++--- src/tgbaalgos/compsusp.hh | 9 ++++---- src/tgbaalgos/cutscc.hh | 14 ++++++++----- src/tgbaalgos/cycles.hh | 2 +- src/tgbaalgos/degen.hh | 10 ++++++--- src/tgbaalgos/dotty.hh | 13 ++++++------ src/tgbaalgos/dottydec.hh | 12 +++++++---- src/tgbaalgos/dupexp.hh | 14 +++++++------ src/tgbaalgos/eltl2tgba_lacim.hh | 8 +++++--- src/tgbaalgos/emptiness.hh | 23 +++++++++++---------- src/tgbaalgos/gtec/Makefile.am | 9 ++++---- src/tgbaalgos/gtec/ce.hh | 7 +++++-- src/tgbaalgos/gtec/explscc.hh | 13 +++++++----- src/tgbaalgos/gtec/gtec.hh | 15 +++++++------- src/tgbaalgos/gtec/nsheap.hh | 19 +++++++++-------- src/tgbaalgos/gtec/sccstack.hh | 7 +++++-- src/tgbaalgos/gtec/status.hh | 7 +++++-- src/tgbaalgos/gv04.hh | 9 +++++--- src/tgbaalgos/isdet.hh | 8 +++++--- src/tgbaalgos/isweakscc.cc | 1 + src/tgbaalgos/isweakscc.hh | 21 ++++++++++++------- src/tgbaalgos/lbtt.hh | 15 +++++++------- src/tgbaalgos/ltl2taa.hh | 8 +++++--- src/tgbaalgos/ltl2tgba_fm.hh | 9 ++++---- src/tgbaalgos/ltl2tgba_lacim.hh | 12 +++++++---- src/tgbaalgos/magic.hh | 22 ++++++++++++-------- src/tgbaalgos/minimize.hh | 12 +++++------ src/tgbaalgos/neverclaim.hh | 16 ++++++++------- src/tgbaalgos/postproc.hh | 2 +- src/tgbaalgos/powerset.hh | 15 ++++++++------ src/tgbaalgos/projrun.hh | 15 +++++++++----- src/tgbaalgos/randomgraph.hh | 7 ++++--- src/tgbaalgos/reachiter.hh | 15 ++++++++------ src/tgbaalgos/reducerun.hh | 6 +++++- src/tgbaalgos/reductgba_sim.cc | 10 +++++---- src/tgbaalgos/reductgba_sim.hh | 35 ++++++++++++++------------------ src/tgbaalgos/replayrun.hh | 13 ++++++++---- src/tgbaalgos/rundotdec.hh | 9 ++++---- src/tgbaalgos/safety.hh | 12 ++++++----- src/tgbaalgos/save.hh | 12 +++++++---- src/tgbaalgos/scc.hh | 22 +++++++++++--------- src/tgbaalgos/sccfilter.hh | 11 ++++++---- src/tgbaalgos/se05.hh | 26 +++++++++++++++--------- src/tgbaalgos/simulation.hh | 19 +++++++++-------- src/tgbaalgos/stats.hh | 19 +++++++++-------- src/tgbaalgos/stripacc.hh | 5 +++-- src/tgbaalgos/tau03.hh | 13 +++++++----- src/tgbaalgos/tau03opt.hh | 13 +++++++----- src/tgbaalgos/translate.hh | 2 +- 50 files changed, 358 insertions(+), 247 deletions(-) diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index 8a9174ad5..ffcd917e3 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -23,7 +23,7 @@ SUBDIRS = gtec AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(BUDDY_CPPFLAGS) -AM_CXXFLAGS = $(WARNING_CXXFLAGS) +AM_CXXFLAGS = $(WARNING_CXXFLAGS) $(VISIBILITY_CXXFLAGS) tgbaalgosdir = $(pkgincludedir)/tgbaalgos diff --git a/src/tgbaalgos/bfssteps.hh b/src/tgbaalgos/bfssteps.hh index 7dde4dfa0..134865583 100644 --- a/src/tgbaalgos/bfssteps.hh +++ b/src/tgbaalgos/bfssteps.hh @@ -1,7 +1,8 @@ -// Copyright (C) 2011 Laboratoire de Recherche et Developpement de +// -*- coding: utf-8 -*- +// Copyright (C) 2011, 2013 Laboratoire de Recherche et Developpement 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. @@ -38,7 +39,7 @@ namespace spot /// These conditions should be specified by defining bfs_steps::match() /// in a subclass. Also the search can be restricted to some set of /// states with a proper definition of bfs_steps::filter(). - class bfs_steps + class SPOT_API bfs_steps { public: bfs_steps(const tgba* a); diff --git a/src/tgbaalgos/compsusp.hh b/src/tgbaalgos/compsusp.hh index 8aef32a73..10fe47afb 100644 --- a/src/tgbaalgos/compsusp.hh +++ b/src/tgbaalgos/compsusp.hh @@ -49,10 +49,11 @@ namespace spot /// This interface is subject to change, and clients aiming for /// long-term stability should better use the services of the /// spot::translator class instead. - tgba* compsusp(const ltl::formula* f, bdd_dict* dict, - bool no_wdba = false, bool no_simulation = false, - bool early_susp = false, bool no_susp_product = false, - bool wdba_smaller = false, bool oblig = false); + SPOT_API tgba* + compsusp(const ltl::formula* f, bdd_dict* dict, + bool no_wdba = false, bool no_simulation = false, + bool early_susp = false, bool no_susp_product = false, + bool wdba_smaller = false, bool oblig = false); } #endif // SPOT_TGBAALGOS_COMPSUSP_HH diff --git a/src/tgbaalgos/cutscc.hh b/src/tgbaalgos/cutscc.hh index 8ce4fd4bb..c12e60a6a 100644 --- a/src/tgbaalgos/cutscc.hh +++ b/src/tgbaalgos/cutscc.hh @@ -1,3 +1,4 @@ +// -*- coding: utf-8 -*- // Copyright (C) 2009, 2013 Laboratoire de Recherche et Developpement de // l'Epita (LRDE). // @@ -20,7 +21,6 @@ #ifndef SPOT_TGBAALGOS_CUTSCC_HH # define SPOT_TGBAALGOS_CUTSCC_HH -#include #include #include #include "tgba/tgba.hh" @@ -34,10 +34,14 @@ namespace spot unsigned size; }; - std::vector >* find_paths(tgba* a, const scc_map& m); - unsigned max_spanning_paths(std::vector* paths, scc_map& m); - std::list split_tgba(tgba* a, const scc_map& m, - unsigned split_number); + SPOT_API std::vector >* + find_paths(tgba* a, const scc_map& m); + + SPOT_API unsigned + max_spanning_paths(std::vector* paths, scc_map& m); + + SPOT_API std::list + split_tgba(tgba* a, const scc_map& m, unsigned split_number); } diff --git a/src/tgbaalgos/cycles.hh b/src/tgbaalgos/cycles.hh index 423ce88b9..b7800ccc2 100644 --- a/src/tgbaalgos/cycles.hh +++ b/src/tgbaalgos/cycles.hh @@ -76,7 +76,7 @@ namespace spot /// run() method will terminate. If it returns true, the run() /// method will search for the next elementary cycle and call /// cycle_found() again if it finds another cycle. - class enumerate_cycles + class SPOT_API enumerate_cycles { protected: typedef Sgi::hash_set +# include +# include "misc/common.hh" namespace spot { @@ -41,7 +42,7 @@ namespace spot /// decorators. If no decorator is specified, the dotty_decorator /// is used. /// labels the transitions are encoded in UTF-8. - std::ostream& + SPOT_API std::ostream& dotty_reachable(std::ostream& os, const tgba* g, bool assume_sba = false, diff --git a/src/tgbaalgos/dottydec.hh b/src/tgbaalgos/dottydec.hh index e2f8b51c2..71b34f00e 100644 --- a/src/tgbaalgos/dottydec.hh +++ b/src/tgbaalgos/dottydec.hh @@ -1,5 +1,8 @@ -// Copyright (C) 2004, 2011 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// -*- coding: utf-8 -*- +// Copyright (C) 2011, 2013 Laboratoire de Recherche et +// Developpement 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. @@ -20,7 +23,8 @@ #ifndef SPOT_TGBAALGOS_DOTTYDEC_HH # define SPOT_TGBAALGOS_DOTTYDEC_HH -#include +# include "misc/common.hh" +# include namespace spot { @@ -33,7 +37,7 @@ namespace spot /// \ingroup tgba_dotty /// \brief Choose state and link styles for spot::dotty_reachable. - class dotty_decorator + class SPOT_API dotty_decorator { public: virtual ~dotty_decorator(); diff --git a/src/tgbaalgos/dupexp.hh b/src/tgbaalgos/dupexp.hh index 3d9aff070..f189413b9 100644 --- a/src/tgbaalgos/dupexp.hh +++ b/src/tgbaalgos/dupexp.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// 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 et Marie Curie. @@ -30,23 +30,25 @@ namespace spot /// \ingroup tgba_misc /// \brief Build an explicit automata from all states of \a aut, /// numbering states in bread first order as they are processed. - tgba_explicit_number* tgba_dupexp_bfs(const tgba* aut); + SPOT_API tgba_explicit_number* + tgba_dupexp_bfs(const tgba* aut); /// \ingroup tgba_misc /// \brief Build an explicit automata from all states of \a aut, /// numbering states in depth first order as they are processed. - tgba_explicit_number* tgba_dupexp_dfs(const tgba* aut); + SPOT_API tgba_explicit_number* + tgba_dupexp_dfs(const tgba* aut); /// \ingroup tgba_misc /// \brief Build an explicit automata from all states of \a aut, /// numbering states in bread first order as they are processed. - tgba_explicit_number* + SPOT_API tgba_explicit_number* tgba_dupexp_bfs(const tgba* aut, std::map& relation); /// \ingroup tgba_misc /// \brief Build an explicit automata from all states of \a aut, /// numbering states in depth first order as they are processed. - tgba_explicit_number* + SPOT_API tgba_explicit_number* tgba_dupexp_dfs(const tgba* aut, std::map& relation); diff --git a/src/tgbaalgos/eltl2tgba_lacim.hh b/src/tgbaalgos/eltl2tgba_lacim.hh index 727febce2..c45b3accc 100644 --- a/src/tgbaalgos/eltl2tgba_lacim.hh +++ b/src/tgbaalgos/eltl2tgba_lacim.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. // @@ -46,7 +47,8 @@ namespace spot /// \param f The formula to translate into an automaton. /// \param dict The spot::bdd_dict the constructed automata should use. /// \return A spot::tgba_bdd_concrete that recognizes the language of \a f. - tgba_bdd_concrete* eltl_to_tgba_lacim(const ltl::formula* f, bdd_dict* dict); + SPOT_API tgba_bdd_concrete* + eltl_to_tgba_lacim(const ltl::formula* f, bdd_dict* dict); } #endif // SPOT_TGBAALGOS_LTL2TGBA_LACIM_HH diff --git a/src/tgbaalgos/emptiness.hh b/src/tgbaalgos/emptiness.hh index 04a9538c0..97d86b0e6 100644 --- a/src/tgbaalgos/emptiness.hh +++ b/src/tgbaalgos/emptiness.hh @@ -1,7 +1,8 @@ -// Copyright (C) 2011 Laboratoire de Recherche et Developpement de -// l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2011, 2013 Laboratoire de Recherche et Developpement +// 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. @@ -73,7 +74,7 @@ namespace spot /// Instances of these class should not last longer than the /// instances of emptiness_check that produced them as they /// may reference data internal to the check. - class emptiness_check_result + class SPOT_API emptiness_check_result { public: emptiness_check_result(const tgba* a, option_map o = option_map()) @@ -129,7 +130,7 @@ namespace spot }; /// Common interface to emptiness check algorithms. - class emptiness_check + class SPOT_API emptiness_check { public: emptiness_check(const tgba* a, option_map o = option_map()) @@ -190,7 +191,7 @@ namespace spot // Dynamically create emptiness checks. Given their name and options. - class emptiness_check_instantiator + class SPOT_API emptiness_check_instantiator { public: /// \brief Create an emptiness-check instantiator, given the name @@ -250,7 +251,7 @@ namespace spot /// @{ /// An accepted run, for a tgba. - struct tgba_run + struct SPOT_API tgba_run { struct step { const state* s; @@ -285,15 +286,15 @@ namespace spot /// This is unlike replay_tgba_run(), which will ensure the run /// actually exists in the automaton (and will also display any /// transition annotation). - std::ostream& print_tgba_run(std::ostream& os, - const tgba* a, - const tgba_run* run); + SPOT_API std::ostream& + print_tgba_run(std::ostream& os, const tgba* a, const tgba_run* run); /// \brief Return an explicit_tgba corresponding to \a run (i.e. comparable /// states are merged). /// /// \pre \a run must correspond to an actual run of the automaton \a a. - tgba* tgba_run_to_tgba(const tgba* a, const tgba_run* run); + SPOT_API tgba* + tgba_run_to_tgba(const tgba* a, const tgba_run* run); /// @} diff --git a/src/tgbaalgos/gtec/Makefile.am b/src/tgbaalgos/gtec/Makefile.am index 2c33afb5a..f8f108da7 100644 --- a/src/tgbaalgos/gtec/Makefile.am +++ b/src/tgbaalgos/gtec/Makefile.am @@ -1,7 +1,8 @@ -## Copyright (C) 2011 Laboratoire de Recherche et Developpement de -## l'Epita (LRDE). +## -*- coding: utf-8 -*- +## Copyright (C) 2011, 2013 Laboratoire de Recherche et Developpement +## 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 +## 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../.. $(BUDDY_CPPFLAGS) -AM_CXXFLAGS = $(WARNING_CXXFLAGS) +AM_CXXFLAGS = $(WARNING_CXXFLAGS) $(VISIBILITY_CXXFLAGS) gtecdir = $(pkgincludedir)/tgbaalgos/gtec diff --git a/src/tgbaalgos/gtec/ce.hh b/src/tgbaalgos/gtec/ce.hh index 171f91e07..9a6c7fce9 100644 --- a/src/tgbaalgos/gtec/ce.hh +++ b/src/tgbaalgos/gtec/ce.hh @@ -1,5 +1,8 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 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 +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -27,7 +30,7 @@ namespace spot { /// Compute a counter example from a spot::couvreur99_check_status - class couvreur99_check_result: + class SPOT_API couvreur99_check_result: public emptiness_check_result, public acss_statistics { diff --git a/src/tgbaalgos/gtec/explscc.hh b/src/tgbaalgos/gtec/explscc.hh index 57b17cdd0..992d4fa69 100644 --- a/src/tgbaalgos/gtec/explscc.hh +++ b/src/tgbaalgos/gtec/explscc.hh @@ -1,7 +1,8 @@ -// Copyright (C) 2011 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// -*- 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 +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -29,7 +30,8 @@ namespace spot { /// An SCC storing all its states explicitly. - class explicit_connected_component: public scc_stack::connected_component + class SPOT_API explicit_connected_component: + public scc_stack::connected_component { public: virtual ~explicit_connected_component() {} @@ -46,7 +48,8 @@ namespace spot /// A straightforward implementation of explicit_connected_component /// using a hash. - class connected_component_hash_set: public explicit_connected_component + class SPOT_API connected_component_hash_set: + public explicit_connected_component { public: virtual ~connected_component_hash_set() {} diff --git a/src/tgbaalgos/gtec/gtec.hh b/src/tgbaalgos/gtec/gtec.hh index d3727902d..44d33f23c 100644 --- a/src/tgbaalgos/gtec/gtec.hh +++ b/src/tgbaalgos/gtec/gtec.hh @@ -1,8 +1,9 @@ -// Copyright (C) 2008 Laboratoire de Recherche et Development de -// l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2008, 2013 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de -// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), -// Université Pierre et Marie Curie. +// 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. // @@ -135,7 +136,7 @@ namespace spot /// states that belong to the same SCC will be considered when /// choosing a successor. Otherwise, only the successor of the /// topmost state on the DFS stack are considered. - emptiness_check* + SPOT_API emptiness_check* couvreur99(const tgba* a, option_map options = option_map(), const numbered_state_heap_factory* nshf @@ -145,7 +146,7 @@ namespace spot /// \brief An implementation of the Couvreur99 emptiness-check algorithm. /// /// See the documentation for spot::couvreur99. - class couvreur99_check: public emptiness_check, public ec_statistics + class SPOT_API couvreur99_check: public emptiness_check, public ec_statistics { public: couvreur99_check(const tgba* a, @@ -190,7 +191,7 @@ namespace spot /// known states first. /// /// See the documentation for spot::couvreur99. - class couvreur99_check_shy : public couvreur99_check + class SPOT_API couvreur99_check_shy : public couvreur99_check { public: couvreur99_check_shy(const tgba* a, diff --git a/src/tgbaalgos/gtec/nsheap.hh b/src/tgbaalgos/gtec/nsheap.hh index fa640cae6..9ce345e89 100644 --- a/src/tgbaalgos/gtec/nsheap.hh +++ b/src/tgbaalgos/gtec/nsheap.hh @@ -1,5 +1,8 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2013 Laboratoire de Recherche et Development 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é 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,13 +23,13 @@ #ifndef SPOT_TGBAALGOS_GTEC_NSHEAP_HH # define SPOT_TGBAALGOS_GTEC_NSHEAP_HH -#include "tgba/state.hh" -#include "misc/hash.hh" +# include "tgba/state.hh" +# include "misc/hash.hh" namespace spot { /// Iterator on numbered_state_heap objects. - class numbered_state_heap_const_iterator + class SPOT_API numbered_state_heap_const_iterator { public: virtual ~numbered_state_heap_const_iterator() {} @@ -46,7 +49,7 @@ namespace spot }; /// Keep track of a large quantity of indexed states. - class numbered_state_heap + class SPOT_API numbered_state_heap { public: typedef std::pair state_index_p; @@ -95,7 +98,7 @@ namespace spot }; /// Abstract factory for numbered_state_heap - class numbered_state_heap_factory + class SPOT_API numbered_state_heap_factory { public: virtual ~numbered_state_heap_factory() {} @@ -103,7 +106,7 @@ namespace spot }; /// A straightforward implementation of numbered_state_heap with a hash map. - class numbered_state_heap_hash_map : public numbered_state_heap + class SPOT_API numbered_state_heap_hash_map : public numbered_state_heap { public: virtual ~numbered_state_heap_hash_map(); @@ -127,7 +130,7 @@ namespace spot /// \brief Factory for numbered_state_heap_hash_map. /// /// This class is a singleton. Retrieve the instance using instance(). - class numbered_state_heap_hash_map_factory: + class SPOT_API numbered_state_heap_hash_map_factory: public numbered_state_heap_factory { public: diff --git a/src/tgbaalgos/gtec/sccstack.hh b/src/tgbaalgos/gtec/sccstack.hh index 04520acc9..f1ad5f6f6 100644 --- a/src/tgbaalgos/gtec/sccstack.hh +++ b/src/tgbaalgos/gtec/sccstack.hh @@ -1,5 +1,8 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 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 +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -28,7 +31,7 @@ namespace spot { // A stack of Strongly-Connected Components, as needed by the // Tarjan-Couvreur algorithm. - class scc_stack + class SPOT_API scc_stack { public: struct connected_component diff --git a/src/tgbaalgos/gtec/status.hh b/src/tgbaalgos/gtec/status.hh index 69f4ce583..77f294f9f 100644 --- a/src/tgbaalgos/gtec/status.hh +++ b/src/tgbaalgos/gtec/status.hh @@ -1,5 +1,8 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 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 +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -32,7 +35,7 @@ namespace spot /// This contains everything needed to construct a counter-example: /// the automata, the stack of SCCs traversed by the counter-example, /// and the heap of visited states with their indexes. - class couvreur99_check_status + class SPOT_API couvreur99_check_status { public: couvreur99_check_status(const tgba* aut, diff --git a/src/tgbaalgos/gv04.hh b/src/tgbaalgos/gv04.hh index b5b65aeec..21a42a102 100644 --- a/src/tgbaalgos/gv04.hh +++ b/src/tgbaalgos/gv04.hh @@ -1,5 +1,8 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2013 Laboratoire de Recherche et Developpement +// 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. @@ -51,8 +54,8 @@ namespace spot isbn = {3-540-21299-X} } \endverbatim */ - emptiness_check* explicit_gv04_check(const tgba* a, - option_map o = option_map()); + SPOT_API emptiness_check* + explicit_gv04_check(const tgba* a, option_map o = option_map()); } #endif // SPOT_TGBAALGOS_GV04_HH diff --git a/src/tgbaalgos/isdet.hh b/src/tgbaalgos/isdet.hh index 8f9c7b79f..19e3b4f36 100644 --- a/src/tgbaalgos/isdet.hh +++ b/src/tgbaalgos/isdet.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. @@ -32,14 +32,16 @@ namespace spot /// The automaton is deterministic if it has 0 nondeterministic states, /// but it is more efficient to call is_deterministic() if you do not /// care about the number of nondeterministic states. - unsigned count_nondet_states(const tgba* aut); + SPOT_API unsigned + count_nondet_states(const tgba* aut); /// \brief Return true iff \a aut is deterministic. /// /// This function is more efficient than count_nondet_states() when /// the automaton is nondeterministic, because it can return before /// the entire automaton has been explored. - bool is_deterministic(const tgba* aut); + SPOT_API bool + is_deterministic(const tgba* aut); /// @} } diff --git a/src/tgbaalgos/isweakscc.cc b/src/tgbaalgos/isweakscc.cc index 1f217f67e..7c1b09c1e 100644 --- a/src/tgbaalgos/isweakscc.cc +++ b/src/tgbaalgos/isweakscc.cc @@ -19,6 +19,7 @@ #include "cycles.hh" #include "tgba/tgbaexplicit.hh" #include "ltlast/formula.hh" +#include "isweakscc.hh" namespace spot { diff --git a/src/tgbaalgos/isweakscc.hh b/src/tgbaalgos/isweakscc.hh index 85aa6d424..74b8dd659 100644 --- a/src/tgbaalgos/isweakscc.hh +++ b/src/tgbaalgos/isweakscc.hh @@ -1,4 +1,5 @@ -// Copyright (C) 2012, 2013 Laboratoire de Recherche et Developpement de +// -*- coding: utf-8 -*- +// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement de // l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -42,7 +43,8 @@ namespace spot /// necessarily weak. /// For other accepting SCCs, this function enumerates all cycles in /// the given SCC (it stops if it find a non-accepting cycle). - bool is_inherently_weak_scc(scc_map& map, unsigned scc); + SPOT_API bool + is_inherently_weak_scc(scc_map& map, unsigned scc); /// \brief Whether the SCC number \a scc in \a map is weak. /// @@ -52,7 +54,8 @@ namespace spot /// Note that terminal SCCs are also weak with that definition. /// /// The scc_map \a map should have been built already. - bool is_weak_scc(scc_map& map, unsigned scc); + SPOT_API bool + is_weak_scc(scc_map& map, unsigned scc); /// \brief Whether the SCC number \a scc in \a map is complete. /// @@ -60,7 +63,8 @@ namespace spot /// a transition that stays into this SCC. /// /// The scc_map \a map should have been built already. - bool is_complete_scc(scc_map& map, unsigned scc); + SPOT_API bool + is_complete_scc(scc_map& map, unsigned scc); /// \brief Whether the SCC number \a scc in \a map is syntactically /// weak. @@ -70,7 +74,8 @@ namespace spot /// syntactic-persistence formula. /// /// The scc_map \a map should have been built already. - bool is_syntactic_weak_scc(scc_map& map, unsigned scc); + SPOT_API bool + is_syntactic_weak_scc(scc_map& map, unsigned scc); /// \brief Whether the SCC number \a scc in \a map is syntactically /// terminal. @@ -80,14 +85,16 @@ namespace spot /// syntactic-guarantee formula. /// /// The scc_map \a map should have been built already. - bool is_syntactic_terminal_scc(scc_map& map, unsigned scc); + SPOT_API bool + is_syntactic_terminal_scc(scc_map& map, unsigned scc); /// \brief Whether the SCC number \a scc in \a map is terminal. /// /// An SCC is terminal if it is weak, complete, and accepting. /// /// The scc_map \a map should have been built already. - bool is_terminal_scc(scc_map& map, unsigned scc); + SPOT_API bool + is_terminal_scc(scc_map& map, unsigned scc); /// @} } diff --git a/src/tgbaalgos/lbtt.hh b/src/tgbaalgos/lbtt.hh index a6df4bcfb..af5dd0b7e 100644 --- a/src/tgbaalgos/lbtt.hh +++ b/src/tgbaalgos/lbtt.hh @@ -36,8 +36,8 @@ namespace spot /// \param os Where to print. /// \param sba Assume \a g is an SBA and use LBTT's state-based /// acceptance format (similar to LBT's format). - std::ostream& lbtt_reachable(std::ostream& os, const tgba* g, - bool sba = false); + SPOT_API std::ostream& + lbtt_reachable(std::ostream& os, const tgba* g, bool sba = false); /// \ingroup tgba_io /// \brief Read an automaton in LBTT's format @@ -51,12 +51,11 @@ namespace spot /// \param envacc The environment of acceptance conditions into which parsing /// should take place. /// \return the read tgba or 0 on error. - const tgba* lbtt_parse(std::istream& is, std::string& error, - bdd_dict* dict, - ltl::environment& env - = ltl::default_environment::instance(), - ltl::environment& envacc - = ltl::default_environment::instance()); + SPOT_API const tgba* + lbtt_parse(std::istream& is, std::string& error, + bdd_dict* dict, + ltl::environment& env = ltl::default_environment::instance(), + ltl::environment& envacc = ltl::default_environment::instance()); } #endif // SPOT_TGBAALGOS_LBTT_HH diff --git a/src/tgbaalgos/ltl2taa.hh b/src/tgbaalgos/ltl2taa.hh index d53264e9e..40f4e1f57 100644 --- a/src/tgbaalgos/ltl2taa.hh +++ b/src/tgbaalgos/ltl2taa.hh @@ -1,4 +1,5 @@ -// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2010, 2013 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -47,8 +48,9 @@ namespace spot /// \param dict The spot::bdd_dict the constructed automata should use. /// \param refined_rules If this parameter is set, refined rules are used. /// \return A spot::taa that recognizes the language of \a f. - taa_tgba* ltl_to_taa(const ltl::formula* f, bdd_dict* dict, - bool refined_rules = false); + SPOT_API taa_tgba* + ltl_to_taa(const ltl::formula* f, bdd_dict* dict, + bool refined_rules = false); } #endif // SPOT_TGBAALGOS_LTL2TAA_HH diff --git a/src/tgbaalgos/ltl2tgba_fm.hh b/src/tgbaalgos/ltl2tgba_fm.hh index 8d0fc5f83..a9af771a6 100644 --- a/src/tgbaalgos/ltl2tgba_fm.hh +++ b/src/tgbaalgos/ltl2tgba_fm.hh @@ -1,8 +1,9 @@ +// -*- coding: utf-8 -*- // Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de -// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), -// Université Pierre et Marie Curie. +// 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. // @@ -121,7 +122,7 @@ namespace spot \endverbatim */ /// /// \return A spot::tgba_explicit that recognizes the language of \a f. - tgba_explicit_formula* + SPOT_API tgba_explicit_formula* ltl_to_tgba_fm(const ltl::formula* f, bdd_dict* dict, bool exprop = false, bool symb_merge = true, bool branching_postponement = false, diff --git a/src/tgbaalgos/ltl2tgba_lacim.hh b/src/tgbaalgos/ltl2tgba_lacim.hh index 8e65e5a9c..d3316cbf5 100644 --- a/src/tgbaalgos/ltl2tgba_lacim.hh +++ b/src/tgbaalgos/ltl2tgba_lacim.hh @@ -1,6 +1,9 @@ -// 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. +// -*- 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), département Systèmes Répartis Coopératifs (SRC), +// Université Pierre et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -47,7 +50,8 @@ namespace spot /// \param f The formula to translate into an automaton. /// \param dict The spot::bdd_dict the constructed automata should use. /// \return A spot::tgba_bdd_concrete that recognizes the language of \a f. - tgba_bdd_concrete* ltl_to_tgba_lacim(const ltl::formula* f, bdd_dict* dict); + SPOT_API tgba_bdd_concrete* + ltl_to_tgba_lacim(const ltl::formula* f, bdd_dict* dict); } #endif // SPOT_TGBAALGOS_LTL2TGBA_LACIM_HH diff --git a/src/tgbaalgos/magic.hh b/src/tgbaalgos/magic.hh index db4e43812..08dee4ce2 100644 --- a/src/tgbaalgos/magic.hh +++ b/src/tgbaalgos/magic.hh @@ -1,5 +1,8 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2013 Laboratoire de Recherche et Developpement +// 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. @@ -47,7 +50,7 @@ namespace spot begin call dfs_blue(s0); end; - + procedure dfs_blue (s) begin s.color = blue; @@ -61,7 +64,7 @@ namespace spot end if; end for; end; - + procedure dfs_red(s) begin s.color = red; @@ -94,8 +97,9 @@ namespace spot /// /// \bug The name is misleading. Magic-search is the algorithm /// from \c godefroid.93.pstv, not \c courcoubetis.92.fmsd. - emptiness_check* explicit_magic_search(const tgba *a, - option_map o = option_map()); + SPOT_API emptiness_check* + explicit_magic_search(const tgba *a, + option_map o = option_map()); /// \brief Returns an emptiness checker on the spot::tgba automaton \a a. /// @@ -124,8 +128,9 @@ namespace spot /// /// \sa spot::explicit_magic_search /// - emptiness_check* bit_state_hashing_magic_search(const tgba *a, size_t size, - option_map o = option_map()); + SPOT_API emptiness_check* + bit_state_hashing_magic_search(const tgba *a, size_t size, + option_map o = option_map()); /// \brief Wrapper for the two magic_search implementations. /// @@ -133,7 +138,8 @@ namespace spot /// bit_state_hashing_magic_search() according to the \c "bsh" option /// in the \c option_map. If \c "bsh" is set and non null, its value /// is used as the size of the hash map. - emptiness_check* magic_search(const tgba *a, option_map o = option_map()); + SPOT_API emptiness_check* + magic_search(const tgba *a, option_map o = option_map()); /// @} } diff --git a/src/tgbaalgos/minimize.hh b/src/tgbaalgos/minimize.hh index e47951b05..fb91fb296 100644 --- a/src/tgbaalgos/minimize.hh +++ b/src/tgbaalgos/minimize.hh @@ -57,7 +57,7 @@ namespace spot /// \param a the automaton to convert into a minimal deterministic monitor /// \pre Dead SCCs should have been removed from \a a before /// calling this function. - sba_explicit_number* minimize_monitor(const tgba* a); + SPOT_API sba_explicit_number* minimize_monitor(const tgba* a); /// \brief Minimize a Büchi automaton in the WDBA class. /// @@ -93,7 +93,7 @@ namespace spot month = oct } \endverbatim */ - sba_explicit_number* minimize_wdba(const tgba* a); + SPOT_API sba_explicit_number* minimize_wdba(const tgba* a); /// \brief Minimize an automaton if it represents an obligation property. /// @@ -150,10 +150,10 @@ namespace spot /// determinization step during minimize_wdba().) Note that /// checking the size of the minimized WDBA occurs before ensuring /// that the minimized WDBA is correct. - tgba* minimize_obligation(const tgba* aut_f, - const ltl::formula* f = 0, - const tgba* aut_neg_f = 0, - bool reject_bigger = false); + SPOT_API tgba* minimize_obligation(const tgba* aut_f, + const ltl::formula* f = 0, + const tgba* aut_neg_f = 0, + bool reject_bigger = false); /// @} } diff --git a/src/tgbaalgos/neverclaim.hh b/src/tgbaalgos/neverclaim.hh index dfb597fa5..4c3d1ab57 100644 --- a/src/tgbaalgos/neverclaim.hh +++ b/src/tgbaalgos/neverclaim.hh @@ -1,7 +1,8 @@ -// Copyright (C) 2009, 2011, 2012 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2011, 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 +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -41,10 +42,11 @@ namespace spot /// it will be output as a comment. /// \param comments Whether to comment each state of the never clause /// with the label of the \a g automaton. - std::ostream& never_claim_reachable(std::ostream& os, - const tgba* g, - const ltl::formula* f = 0, - bool comments = false); + SPOT_API std::ostream& + never_claim_reachable(std::ostream& os, + const tgba* g, + const ltl::formula* f = 0, + bool comments = false); } #endif // SPOT_TGBAALGOS_NEVERCLAIM_HH diff --git a/src/tgbaalgos/postproc.hh b/src/tgbaalgos/postproc.hh index a3bbd3c40..fee1a684e 100644 --- a/src/tgbaalgos/postproc.hh +++ b/src/tgbaalgos/postproc.hh @@ -56,7 +56,7 @@ namespace spot /// when minimized_obligation failed to produce an automaton smaller /// than its input. pref=Small,level=Low will only run /// simulation(). - class postprocessor + class SPOT_API postprocessor { public: /// \brief Construct a postprocessor. diff --git a/src/tgbaalgos/powerset.hh b/src/tgbaalgos/powerset.hh index 8c55ab292..354d23409 100644 --- a/src/tgbaalgos/powerset.hh +++ b/src/tgbaalgos/powerset.hh @@ -1,7 +1,8 @@ -// Copyright (C) 2011 Laboratoire de Recherche et Développement de -// l'Epita. +// -*- coding: utf-8 -*- +// Copyright (C) 2011, 2013 Laboratoire de Recherche et Développement +// de l'Epita. // Copyright (C) 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. @@ -29,7 +30,7 @@ namespace spot { - struct power_map + struct SPOT_API power_map { typedef std::set power_state; typedef std::map power_map_data; @@ -86,8 +87,10 @@ namespace spot /// If \a pm is supplied it will be filled with the set of original states /// associated to each state of the deterministic automaton. //@{ - tgba_explicit_number* tgba_powerset(const tgba* aut, power_map& pm); - tgba_explicit_number* tgba_powerset(const tgba* aut); + SPOT_API tgba_explicit_number* + tgba_powerset(const tgba* aut, power_map& pm); + SPOT_API tgba_explicit_number* + tgba_powerset(const tgba* aut); //@} } diff --git a/src/tgbaalgos/projrun.hh b/src/tgbaalgos/projrun.hh index 058923ec0..0fe26c763 100644 --- a/src/tgbaalgos/projrun.hh +++ b/src/tgbaalgos/projrun.hh @@ -1,5 +1,8 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2013 Laboratoire de Recherche et Developpement +// 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 +// 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 +23,8 @@ #ifndef SPOT_TGBAALGOS_PROJRUN_HH # define SPOT_TGBAALGOS_PROJRUN_HH -#include +# include "misc/common.hh" +# include namespace spot { @@ -37,9 +41,10 @@ namespace spot /// \param a_run the automata on which the run was generated /// \param a_proj the automata on which to project the run /// \return true iff the run could be completed - tgba_run* project_tgba_run(const tgba* a_run, - const tgba* a_proj, - const tgba_run* run); + SPOT_API tgba_run* + project_tgba_run(const tgba* a_run, const tgba* a_proj, + +const tgba_run* run); } #endif // SPOT_TGBAALGOS_PROJRUN_HH diff --git a/src/tgbaalgos/randomgraph.hh b/src/tgbaalgos/randomgraph.hh index f61853876..c3d83f7e6 100644 --- a/src/tgbaalgos/randomgraph.hh +++ b/src/tgbaalgos/randomgraph.hh @@ -1,7 +1,8 @@ -// Copyright (C) 2011 Laboratoire de Recherche et Developpement de +// -*- coding: utf-8 -*- +// Copyright (C) 2011, 2013 Laboratoire de Recherche et Developpement 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. @@ -77,7 +78,7 @@ namespace spot /// \f$1+(n-1)d\f$ and variance \f$(n-1)d(1-d)\f$. (This is less /// accurate, but faster than considering all possible \a n /// successors one by one.) - tgba* + SPOT_API tgba* random_graph(int n, float d, const ltl::atomic_prop_set* ap, bdd_dict* dict, int n_acc = 0, float a = 0.1, float t = 0.5, diff --git a/src/tgbaalgos/reachiter.hh b/src/tgbaalgos/reachiter.hh index 8ef744501..599e3e59f 100644 --- a/src/tgbaalgos/reachiter.hh +++ b/src/tgbaalgos/reachiter.hh @@ -1,7 +1,8 @@ -// Copyright (C) 2008, 2009, 2011 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2008, 2009, 2011, 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é +// (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 +32,7 @@ namespace spot { /// \ingroup tgba_generic /// \brief Iterate over all reachable states of a spot::tgba. - class tgba_reachable_iterator + class SPOT_API tgba_reachable_iterator { public: tgba_reachable_iterator(const tgba* a); @@ -98,7 +99,8 @@ namespace spot /// \ingroup tgba_generic /// \brief An implementation of spot::tgba_reachable_iterator that browses /// states depth first. - class tgba_reachable_iterator_depth_first : public tgba_reachable_iterator + class SPOT_API tgba_reachable_iterator_depth_first : + public tgba_reachable_iterator { public: tgba_reachable_iterator_depth_first(const tgba* a); @@ -113,7 +115,8 @@ namespace spot /// \ingroup tgba_generic /// \brief An implementation of spot::tgba_reachable_iterator that browses /// states breadth first. - class tgba_reachable_iterator_breadth_first : public tgba_reachable_iterator + class SPOT_API tgba_reachable_iterator_breadth_first : + public tgba_reachable_iterator { public: tgba_reachable_iterator_breadth_first(const tgba* a); diff --git a/src/tgbaalgos/reducerun.hh b/src/tgbaalgos/reducerun.hh index e47a9a1b9..e0fb605d9 100644 --- a/src/tgbaalgos/reducerun.hh +++ b/src/tgbaalgos/reducerun.hh @@ -1,3 +1,4 @@ +// -*- coding: utf-8 -*- // Copyright (C) 2010, 2013 Laboratoire de Recherche et Développement de // l'Epita. // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), @@ -22,6 +23,8 @@ #ifndef SPOT_TGBAALGOS_REDUCERUN_HH # define SPOT_TGBAALGOS_REDUCERUN_HH +# include "misc/common.hh" + namespace spot { class tgba; @@ -32,7 +35,8 @@ namespace spot /// /// Return a run which is accepting for \a a and that is no longer /// than \a org. - tgba_run* reduce_run(const tgba* a, const tgba_run* org); + SPOT_API tgba_run* + reduce_run(const tgba* a, const tgba_run* org); } #endif // SPOT_TGBAALGOS_REDUCERUN_HH diff --git a/src/tgbaalgos/reductgba_sim.cc b/src/tgbaalgos/reductgba_sim.cc index 84279c786..4a3af77c6 100644 --- a/src/tgbaalgos/reductgba_sim.cc +++ b/src/tgbaalgos/reductgba_sim.cc @@ -1,8 +1,9 @@ -// Copyright (C) 2009, 2011, 2012 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2011, 2012, 2013 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2004, 2005, 2007 Laboratoire d'Informatique de -// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), -// Université Pierre et Marie Curie. +// 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. // @@ -19,6 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#define SKIP_DEPRECATED_WARNING #include "reductgba_sim.hh" #include "sccfilter.hh" #include "simulation.hh" diff --git a/src/tgbaalgos/reductgba_sim.hh b/src/tgbaalgos/reductgba_sim.hh index bac013ae9..dff51bef8 100644 --- a/src/tgbaalgos/reductgba_sim.hh +++ b/src/tgbaalgos/reductgba_sim.hh @@ -1,7 +1,8 @@ -// 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) 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. @@ -23,6 +24,14 @@ #ifndef SPOT_TGBAALGOS_REDUCTGBA_SIM_HH #define SPOT_TGBAALGOS_REDUCTGBA_SIM_HH +#if __GNUC__ +#ifndef SKIP_DEPRECATED_WARNING +#warning This file is deprecated. Use postproc.hh instead. +#endif +#endif + +#include "misc/common.hh" + namespace spot { class tgba; @@ -55,7 +64,6 @@ namespace spot #endif }; -#if __GNUC__ /// \brief Simplify the automaton using a simulation relation. /// /// Do not use this obsolete function. @@ -66,23 +74,10 @@ namespace spot /// simulation-related flag will cause direct simulation /// to be applied. /// \return the reduced automaton - /// \deprecated Use scc_filter(), minimize_wdba(), or simulation(). - const tgba* reduc_tgba_sim(const tgba* a, int opt = Reduce_All) - __attribute__ ((deprecated)); -#else - /// \brief Simplify the automaton using a simulation relation. - /// - /// Do not use this obsolete function. - /// - /// \param a the automata to reduce - /// \param opt a conjonction of spot::reduce_tgba_options specifying - /// which optimizations to apply. Actually any - /// simulation-related flag will cause direct simulation - /// to be applied. - /// \return the reduced automaton - /// \deprecated Use scc_filter(), minimize_wdba(), or simulation(). + /// \deprecated Use scc_filter(), minimize_wdba(), simulation(), + /// or postprocessor. + SPOT_API SPOT_DEPRECATED const tgba* reduc_tgba_sim(const tgba* a, int opt = Reduce_All); -#endif /// @} } diff --git a/src/tgbaalgos/replayrun.hh b/src/tgbaalgos/replayrun.hh index e352af4cb..46da88dbc 100644 --- a/src/tgbaalgos/replayrun.hh +++ b/src/tgbaalgos/replayrun.hh @@ -1,5 +1,8 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2013 Laboratoire de Recherche et Developpement +// 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 +// 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 +23,8 @@ #ifndef SPOT_TGBAALGOS_REPLAYRUN_HH # define SPOT_TGBAALGOS_REPLAYRUN_HH -#include +# include "misc/common.hh" +# include namespace spot { @@ -42,8 +46,9 @@ namespace spot /// \param debug if set the output will be more verbose and extra /// debugging informations will be output on failure /// \return true iff the run could be completed - bool replay_tgba_run(std::ostream& os, const tgba* a, const tgba_run* run, - bool debug = false); + SPOT_API bool + replay_tgba_run(std::ostream& os, const tgba* a, const tgba_run* run, + bool debug = false); } #endif // SPOT_TGBAALGOS_REPLAYRUN_HH diff --git a/src/tgbaalgos/rundotdec.hh b/src/tgbaalgos/rundotdec.hh index 539a91ce8..eb888e20e 100644 --- a/src/tgbaalgos/rundotdec.hh +++ b/src/tgbaalgos/rundotdec.hh @@ -1,7 +1,8 @@ -// Copyright (C) 2011 Laboratoire de Recherche et Developpement de -// l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2011, 2013 Laboratoire de Recherche et Developpement +// 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 +// 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,7 +35,7 @@ namespace spot /// \brief Highlight a spot::tgba_run on a spot::tgba. /// /// An instance of this class can be passed to spot::dotty_reachable. - class tgba_run_dotty_decorator: public dotty_decorator + class SPOT_API tgba_run_dotty_decorator: public dotty_decorator { public: tgba_run_dotty_decorator(const tgba_run* run); diff --git a/src/tgbaalgos/safety.hh b/src/tgbaalgos/safety.hh index a66fd6aa1..2369ecc9a 100644 --- a/src/tgbaalgos/safety.hh +++ b/src/tgbaalgos/safety.hh @@ -1,5 +1,6 @@ -// Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement de -// l'Epita (LRDE) +// -*- coding: utf-8 -*- +// Copyright (C) 2010, 2011, 2013 Laboratoire de Recherche et +// Développement de l'Epita (LRDE) // // This file is part of Spot, a model checking library. // @@ -45,7 +46,8 @@ namespace spot /// \param sm an scc_map of the automaton if available (it will be /// built otherwise. If you supply an scc_map you should call /// build_map() before passing it to this function. - bool is_guarantee_automaton(const tgba* aut, const scc_map* sm = 0); + SPOT_API bool + is_guarantee_automaton(const tgba* aut, const scc_map* sm = 0); /// \brief Whether a minimized WDBA represents a safety property. /// @@ -54,8 +56,8 @@ namespace spot /// only accepting transitions. /// /// \param aut the automaton to check - bool is_safety_mwdba(const tgba* aut); - + SPOT_API bool + is_safety_mwdba(const tgba* aut); } diff --git a/src/tgbaalgos/save.hh b/src/tgbaalgos/save.hh index c61b854ce..73a47b2b7 100644 --- a/src/tgbaalgos/save.hh +++ b/src/tgbaalgos/save.hh @@ -1,6 +1,9 @@ -// 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. +// -*- coding: utf-8 -*- +// Copyright (C) 2013 Laboratoire de Recherche et Developpement +// 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. // @@ -27,7 +30,8 @@ namespace spot { /// \ingroup tgba_io /// \brief Save reachable states in text format. - std::ostream& tgba_save_reachable(std::ostream& os, const tgba* g); + SPOT_API std::ostream& + tgba_save_reachable(std::ostream& os, const tgba* g); } #endif // SPOT_TGBAALGOS_SAVE_HH diff --git a/src/tgbaalgos/scc.hh b/src/tgbaalgos/scc.hh index 976c2d6c3..e1cd52f07 100644 --- a/src/tgbaalgos/scc.hh +++ b/src/tgbaalgos/scc.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche -// et Développement de l'Epita. +// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013 Laboratoire de +// Recherche et Développement de l'Epita. // // This file is part of Spot, a model checking library. // @@ -31,7 +31,7 @@ namespace spot { - struct scc_stats + struct SPOT_API scc_stats { /// Total number of SCCs. unsigned scc_total; @@ -67,7 +67,7 @@ namespace spot }; /// Build a map of Strongly Connected components in in a TGBA. - class scc_map + class SPOT_API scc_map { public: typedef std::map succ_type; @@ -247,13 +247,15 @@ namespace spot unsigned self_loops_; // Self loops count. }; - scc_stats build_scc_stats(const tgba* a); - scc_stats build_scc_stats(const scc_map& m); + SPOT_API scc_stats + build_scc_stats(const tgba* a); + SPOT_API scc_stats + build_scc_stats(const scc_map& m); - std::ostream& dump_scc_dot(const tgba* a, std::ostream& out, - bool verbose = false); - std::ostream& dump_scc_dot(const scc_map& m, std::ostream& out, - bool verbose = false); + SPOT_API std::ostream& + dump_scc_dot(const tgba* a, std::ostream& out, bool verbose = false); + SPOT_API std::ostream& + dump_scc_dot(const scc_map& m, std::ostream& out, bool verbose = false); } #endif // SPOT_TGBAALGOS_SCC_HH diff --git a/src/tgbaalgos/sccfilter.hh b/src/tgbaalgos/sccfilter.hh index 04f2167b9..60910642d 100644 --- a/src/tgbaalgos/sccfilter.hh +++ b/src/tgbaalgos/sccfilter.hh @@ -1,3 +1,4 @@ +// -*- coding: utf-8 -*- // Copyright (C) 2009, 2010, 2012, 2013 Laboratoire de Recherche et // Developpement de l'Epita (LRDE). // @@ -61,9 +62,10 @@ namespace spot /// (i.e., transitions leaving accepting states are all marked as /// accepting) may destroy this property. Use scc_filter_states() /// instead. - tgba* scc_filter(const tgba* aut, bool remove_all_useless = false, - scc_map* given_sm = 0, bdd susp = bddtrue, - bool early_susp = false, bdd ignored = bddtrue); + SPOT_API tgba* + scc_filter(const tgba* aut, bool remove_all_useless = false, + scc_map* given_sm = 0, bdd susp = bddtrue, + bool early_susp = false, bdd ignored = bddtrue); /// \brief Prune unaccepting SCCs. /// @@ -73,7 +75,8 @@ namespace spot /// Especially, if the input TGBA has the SBA property, (i.e., /// transitions leaving accepting states are all marked as /// accepting), then the output TGBA will also have that property. - tgba* scc_filter_states(const tgba* aut, scc_map* given_sm = 0); + SPOT_API tgba* + scc_filter_states(const tgba* aut, scc_map* given_sm = 0); } #endif // SPOT_TGBAALGOS_SCC_HH diff --git a/src/tgbaalgos/se05.hh b/src/tgbaalgos/se05.hh index 45ffc70ac..6df3fcb62 100644 --- a/src/tgbaalgos/se05.hh +++ b/src/tgbaalgos/se05.hh @@ -1,6 +1,9 @@ -// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. +// -*- coding: utf-8 -*- +// Copyright (C) 2013 Laboratoire de Recherche et Developpement +// 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 et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -48,7 +51,7 @@ namespace spot begin call dfs_blue(s0); end; - + procedure dfs_blue (s) begin s.color = cyan; @@ -67,7 +70,7 @@ namespace spot end for; s.color = blue; end; - + procedure dfs_red(s) begin if s.color == cyan then @@ -99,8 +102,9 @@ namespace spot /// /// \sa spot::explicit_magic_search /// - emptiness_check* explicit_se05_search(const tgba *a, - option_map o = option_map()); + SPOT_API emptiness_check* + explicit_se05_search(const tgba *a, option_map o = option_map()); + /// \brief Returns an emptiness checker on the spot::tgba automaton \a a. /// /// \pre The automaton \a a must have at most one acceptance condition (i.e. @@ -128,8 +132,9 @@ namespace spot /// /// \sa spot::explicit_se05_search /// - emptiness_check* bit_state_hashing_se05_search(const tgba *a, size_t size, - option_map o = option_map()); + SPOT_API emptiness_check* + bit_state_hashing_se05_search(const tgba *a, size_t size, + option_map o = option_map()); /// \brief Wrapper for the two se05 implementations. @@ -138,7 +143,8 @@ namespace spot /// bit_state_hashing_se05_search() according to the \c "bsh" option /// in the \c option_map. If \c "bsh" is set and non null, its value /// is used as the size of the hash map. - emptiness_check* se05(const tgba *a, option_map o); + SPOT_API emptiness_check* + se05(const tgba *a, option_map o); /// @} } diff --git a/src/tgbaalgos/simulation.hh b/src/tgbaalgos/simulation.hh index 7c453441d..70fe017b6 100644 --- a/src/tgbaalgos/simulation.hh +++ b/src/tgbaalgos/simulation.hh @@ -20,6 +20,8 @@ #ifndef SPOT_TGBAALGOS_SIMULATION_HH # define SPOT_TGBAALGOS_SIMULATION_HH +# include "misc/common.hh" + namespace spot { class tgba; @@ -67,8 +69,8 @@ namespace spot /// \param automaton the automaton to simulate. /// \return a new automaton which is at worst a copy of the received /// one - tgba* simulation(const tgba* automaton); - tgba* simulation_sba(const tgba* automaton); + SPOT_API tgba* simulation(const tgba* automaton); + SPOT_API tgba* simulation_sba(const tgba* automaton); /// @} /// @{ @@ -118,8 +120,8 @@ namespace spot /// \param automaton the automaton to simulate. /// \return a new automaton which is at worst a copy of the received /// one - tgba* cosimulation(const tgba* automaton); - tgba* cosimulation_sba(const tgba* automaton); + SPOT_API tgba* cosimulation(const tgba* automaton); + SPOT_API tgba* cosimulation_sba(const tgba* automaton); /// @} /// @{ @@ -137,14 +139,15 @@ namespace spot /// \param automaton the automaton to simulate. /// \return a new automaton which is at worst a copy of the received /// one - tgba* iterated_simulations(const tgba* automaton); - tgba* iterated_simulations_sba(const tgba* automaton); + SPOT_API tgba* iterated_simulations(const tgba* automaton); + SPOT_API tgba* iterated_simulations_sba(const tgba* automaton); /// @} - tgba* dont_care_simulation(const tgba* t, int limit = -1); + SPOT_API tgba* + dont_care_simulation(const tgba* t, int limit = -1); - tgba* + SPOT_API tgba* dont_care_iterated_simulations(const tgba* t, int limit = -1); diff --git a/src/tgbaalgos/stats.hh b/src/tgbaalgos/stats.hh index 1882d67d4..1b7140d7c 100644 --- a/src/tgbaalgos/stats.hh +++ b/src/tgbaalgos/stats.hh @@ -1,7 +1,8 @@ -// Copyright (C) 2008, 2011, 2012 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2008, 2011, 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 +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -32,7 +33,7 @@ namespace spot /// \addtogroup tgba_misc /// @{ - struct tgba_statistics + struct SPOT_API tgba_statistics { unsigned transitions; unsigned states; @@ -41,7 +42,7 @@ namespace spot std::ostream& dump(std::ostream& out) const; }; - struct tgba_sub_statistics: public tgba_statistics + struct SPOT_API tgba_sub_statistics: public tgba_statistics { unsigned sub_transitions; @@ -50,12 +51,12 @@ namespace spot }; /// \brief Compute statistics for an automaton. - tgba_statistics stats_reachable(const tgba* g); + SPOT_API tgba_statistics stats_reachable(const tgba* g); /// \brief Compute subended statistics for an automaton. - tgba_sub_statistics sub_stats_reachable(const tgba* g); + SPOT_API tgba_sub_statistics sub_stats_reachable(const tgba* g); - class printable_formula: public printable_value + class SPOT_API printable_formula: public printable_value { public: printable_formula& @@ -74,7 +75,7 @@ namespace spot /// This object can be configured to display various statistics /// about a TGBA. Some %-sequence of characters are interpreted in /// the format string, and replaced by the corresponding statistics. - class stat_printer: protected formater + class SPOT_API stat_printer: protected formater { public: stat_printer(std::ostream& os, const char* format); diff --git a/src/tgbaalgos/stripacc.hh b/src/tgbaalgos/stripacc.hh index 0557e944c..2f92d2668 100644 --- a/src/tgbaalgos/stripacc.hh +++ b/src/tgbaalgos/stripacc.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012 Laboratoire de Recherche et Développement de +// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement de // l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -28,7 +28,8 @@ namespace spot /// \brief Duplicate automaton \a a, removing all acceptance sets. /// /// This is equivalent to marking all states/transitions as accepting. - sba_explicit_number* strip_acceptance(const tgba* a); + SPOT_API sba_explicit_number* + strip_acceptance(const tgba* a); } #endif // SPOT_TGBAALGOS_STRIPACC_HH diff --git a/src/tgbaalgos/tau03.hh b/src/tgbaalgos/tau03.hh index 5c3ae40fa..0c0b2bc41 100644 --- a/src/tgbaalgos/tau03.hh +++ b/src/tgbaalgos/tau03.hh @@ -1,5 +1,8 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 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 +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -42,7 +45,7 @@ namespace spot begin call dfs_blue(s0); end; - + procedure dfs_blue (s) begin s.color = blue; @@ -62,7 +65,7 @@ namespace spot report a cycle; end if; end; - + procedure dfs_red(s, A) begin s.acc = s.acc U A; @@ -93,8 +96,8 @@ namespace spot } \endverbatim */ /// - emptiness_check* explicit_tau03_search(const tgba *a, - option_map o = option_map()); + SPOT_API emptiness_check* + explicit_tau03_search(const tgba *a, option_map o = option_map()); /// @} } diff --git a/src/tgbaalgos/tau03opt.hh b/src/tgbaalgos/tau03opt.hh index 6656450a1..1ea721e36 100644 --- a/src/tgbaalgos/tau03opt.hh +++ b/src/tgbaalgos/tau03opt.hh @@ -1,5 +1,8 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 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 +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -43,7 +46,7 @@ namespace spot weight = 0; // the null vector call dfs_blue(s0); end; - + procedure dfs_blue (s) begin s.color = cyan; @@ -71,7 +74,7 @@ namespace spot end for; s.color = blue; end; - + procedure dfs_red(s, Acc) begin for all t in post(s) do @@ -95,8 +98,8 @@ namespace spot /// the path stored in the blue stack. Such a vector is associated to each /// state of this stack. /// - emptiness_check* explicit_tau03_opt_search(const tgba *a, - option_map o = option_map()); + SPOT_API emptiness_check* + explicit_tau03_opt_search(const tgba *a, option_map o = option_map()); /// @} } diff --git a/src/tgbaalgos/translate.hh b/src/tgbaalgos/translate.hh index 32dc554d4..ab626df6f 100644 --- a/src/tgbaalgos/translate.hh +++ b/src/tgbaalgos/translate.hh @@ -45,7 +45,7 @@ namespace spot /// The semantic of these three methods is inherited from the /// spot::postprocessor class, but the optimization level is /// additionally used to select which LTL simplifications to enable. - class translator: protected postprocessor + class SPOT_API translator: protected postprocessor { public: translator(ltl::ltl_simplifier* simpl, const option_map* opt = 0)