Commit 8ba3e64f authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

Use -fvisibility=hidden in src/ltlast/, src/ltlvisit/, and src/ltlenv/.

* src/ltlast/Makefile.am, src/ltlenv/Makefile.am,
src/ltlvisit/Makefile.am: Use $(VISIBILITY_CXXFLAGS).
* src/misc/common.hh (SPOT_DEPRECATED): New macro.
* src/ltlast/atomic_prop.hh, src/ltlast/automatop.hh,
src/ltlast/binop.hh, src/ltlast/bunop.hh, src/ltlast/constant.hh,
src/ltlast/formula.hh, src/ltlast/formula_tree.hh,
src/ltlast/multop.hh, src/ltlast/nfa.hh, src/ltlast/refformula.hh,
src/ltlast/unop.hh, src/ltlast/visitor.hh, src/ltlenv/declenv.hh,
src/ltlenv/defaultenv.hh, src/ltlvisit/apcollect.hh,
src/ltlvisit/clone.hh, src/ltlvisit/contain.hh,
src/ltlvisit/destroy.hh, src/ltlvisit/dotty.hh, src/ltlvisit/dump.hh,
src/ltlvisit/lbt.hh, src/ltlvisit/length.hh,
src/ltlvisit/lunabbrev.hh, src/ltlvisit/nenoform.hh,
src/ltlvisit/postfix.hh, src/ltlvisit/randomltl.hh,
src/ltlvisit/reduce.hh, src/ltlvisit/relabel.hh,
src/ltlvisit/remove_x.hh, src/ltlvisit/simpfg.hh,
src/ltlvisit/simplify.hh, src/ltlvisit/snf.hh,
src/ltlvisit/tostring.hh, src/ltlvisit/tunabbrev.hh,
src/ltlvisit/wmunabbrev.hh: Add SPOT_API in fron of
exported symbols.
* src/ltlvisit/nenoform.cc, src/ltlvisit/remove_x.cc: Add missing
include of the corresponding header file.
parent cbfbf142
## Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et
## Dveloppement de l'Epita (LRDE).
## -*- coding: utf-8 -*-
## Copyright (C) 2009, 2010, 2011, 2013 Laboratoire de Recherche et
## Développement de l'Epita (LRDE).
## Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
## dpartement Systmes Rpartis Coopratifs (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 <http://www.gnu.org/licenses/>.
AM_CPPFLAGS = -I$(srcdir)/.. -I..
AM_CXXFLAGS = $(WARNING_CXXFLAGS)
AM_CXXFLAGS = $(WARNING_CXXFLAGS) $(VISIBILITY_CXXFLAGS)
ltlastdir = $(pkgincludedir)/ltlast
......
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2012 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2009, 2012, 2013 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
......@@ -25,10 +25,10 @@
#ifndef SPOT_LTLAST_ATOMIC_PROP_HH
# define SPOT_LTLAST_ATOMIC_PROP_HH
#include "refformula.hh"
#include <string>
#include <iosfwd>
#include <map>
#include "refformula.hh"
#include "ltlenv/environment.hh"
namespace spot
......@@ -38,7 +38,7 @@ namespace spot
/// \ingroup ltl_ast
/// \brief Atomic propositions.
class atomic_prop : public ref_formula
class SPOT_API atomic_prop : public ref_formula
{
public:
/// Build an atomic proposition with name \a name in
......
// -*- coding: utf-8 -*-
// Copyright (C) 2008, 2009, 2012 Laboratoire de Recherche et
// Copyright (C) 2008, 2009, 2012, 2013 Laboratoire de Recherche et
// Développement de l'Epita (LRDE)
//
// This file is part of Spot, a model checking library.
......@@ -22,11 +22,11 @@
#ifndef SPOT_LTLAST_AUTOMATOP_HH
# define SPOT_LTLAST_AUTOMATOP_HH
# include "refformula.hh"
# include <vector>
# include <iosfwd>
# include <map>
# include "nfa.hh"
# include "refformula.hh"
namespace spot
{
......@@ -35,7 +35,7 @@ namespace spot
/// \ingroup eltl_ast
/// \brief Automaton operators.
///
class automatop : public ref_formula
class SPOT_API automatop : public ref_formula
{
public:
/// List of formulae.
......
......@@ -28,9 +28,9 @@
#ifndef SPOT_LTLAST_BINOP_HH
# define SPOT_LTLAST_BINOP_HH
#include "refformula.hh"
#include <map>
#include <iosfwd>
#include "refformula.hh"
namespace spot
{
......@@ -39,7 +39,7 @@ namespace spot
/// \ingroup ltl_ast
/// \brief Binary operator.
class binop : public ref_formula
class SPOT_API binop : public ref_formula
{
public:
/// Different kinds of binary opertaors
......
// Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// -*- coding: utf-8 -*-
// Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
......@@ -21,9 +22,9 @@
#ifndef SPOT_LTLAST_BUNOP_HH
# define SPOT_LTLAST_BUNOP_HH
#include "refformula.hh"
#include <map>
#include <iosfwd>
#include "refformula.hh"
#include "constant.hh"
namespace spot
......@@ -33,7 +34,7 @@ namespace spot
/// \ingroup ltl_ast
/// \brief Bounded unary operator.
class bunop : public ref_formula
class SPOT_API bunop : public ref_formula
{
public:
enum type { Star };
......
// Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2012, 2013 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
//
......@@ -31,7 +32,7 @@ namespace spot
/// \ingroup ltl_ast
/// \brief A constant (True or False)
class constant : public formula
class SPOT_API constant : public formula
{
public:
enum type { False, True, EmptyWord };
......
// -*- coding: utf-8 -*-
// Copyright (C) 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013 Laboratoire de
// Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de
//
// This file is part of Spot, a model checking library.
......@@ -23,6 +23,7 @@
#ifndef SPOT_LTLAST_FORMULA_HH
# define SPOT_LTLAST_FORMULA_HH
#include "misc/common.hh"
#include <string>
#include <cassert>
#include "predecl.hh"
......@@ -68,7 +69,7 @@ namespace spot
///
/// The only way you can work with a formula is to
/// build a spot::ltl::visitor or spot::ltl::const_visitor.
class formula
class SPOT_API formula
{
public:
/// Kind of a sub-formula
......@@ -420,11 +421,13 @@ namespace spot
};
/// Print the properties of formula \a f on stream \a out.
SPOT_API
std::ostream& print_formula_props(std::ostream& out,
const formula* f,
bool abbreviated = false);
/// List the properties of formula \a f.
SPOT_API
std::list<std::string> list_formula_props(const formula* f);
}
}
......
// Copyright (C) 2009, 2012 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2012, 2013 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
......@@ -21,9 +22,9 @@
#ifndef SPOT_LTLAST_FORMULA_TREE_HH
# define SPOT_LTLAST_FORMULA_TREE_HH
# include "formula.hh"
# include <vector>
# include <boost/shared_ptr.hpp>
# include "formula.hh"
# include "multop.hh"
# include "binop.hh"
# include "unop.hh"
......
// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
......@@ -24,10 +25,10 @@
#ifndef SPOT_LTLAST_MULTOP_HH
# define SPOT_LTLAST_MULTOP_HH
#include "refformula.hh"
#include <vector>
#include <map>
#include <iosfwd>
#include "refformula.hh"
namespace spot
{
......@@ -36,7 +37,7 @@ namespace spot
/// \ingroup ltl_ast
/// \brief Multi-operand operators.
class multop : public ref_formula
class SPOT_API multop : public ref_formula
{
public:
enum type { Or, OrRat, And, AndRat, AndNLM, Concat, Fusion };
......
// Copyright (C) 2008, 2010 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// -*- coding: utf-8 -*-
// Copyright (C) 2008, 2010, 2013 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
......@@ -21,6 +22,7 @@
#ifndef SPOT_LTLAST_NFA_HH
# define SPOT_LTLAST_NFA_HH
# include "misc/common.hh"
# include "misc/hash.hh"
# include <boost/shared_ptr.hpp>
# include <list>
......@@ -32,7 +34,7 @@ namespace spot
namespace ltl
{
/// Forward declaration. See below.
class succ_iterator;
class SPOT_API succ_iterator;
/// Forward declaration. NFA's labels are reprensented by nodes
/// which are defined in formula_tree.hh, included in nfa.cc.
namespace formula_tree
......@@ -45,7 +47,7 @@ namespace spot
/// States are represented by integers.
/// Labels are represented by formula_tree's nodes.
/// Currently, only one initial state is possible.
class nfa
class SPOT_API nfa
{
public:
struct transition;
......@@ -118,7 +120,7 @@ namespace spot
nfa& operator=(const nfa& other);
};
class succ_iterator
class SPOT_API succ_iterator
{
public:
succ_iterator(const nfa::state::const_iterator s)
......
// -*- coding: utf-8 -*-
// Copyright (C) 2010, 2012 Laboratoire de Recherche de Developpement
// de l'EPITA (LRDE).
// Copyright (C) 2010, 2012, 2013 Laboratoire de Recherche de
// Développement de l'EPITA (LRDE).
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
......@@ -34,7 +34,7 @@ namespace spot
/// \ingroup ltl_ast
/// \brief A reference-counted LTL formula.
class ref_formula : public formula
class SPOT_API ref_formula : public formula
{
protected:
virtual ~ref_formula();
......
// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
//
// This file is part of Spot, a model checking library.
//
......@@ -36,7 +37,7 @@ namespace spot
/// \ingroup ltl_ast
/// \brief Unary operators.
class unop : public ref_formula
class SPOT_API unop : public ref_formula
{
public:
enum type {
......
// Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et Dveloppement
// de l'Epita (LRDE).
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2012, 2013 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// This file is part of Spot, a model checking library.
......@@ -24,7 +25,8 @@
#ifndef SPOT_LTLAST_VISITOR_HH
# define SPOT_LTLAST_VISITOR_HH
#include "predecl.hh"
# include "misc/common.hh"
# include "predecl.hh"
namespace spot
{
......@@ -36,7 +38,7 @@ namespace spot
/// Implementing visitors is the prefered way
/// to traverse a formula, since it does not
/// involve any cast.
struct visitor
struct SPOT_API visitor
{
virtual ~visitor() {}
virtual void visit(const atomic_prop* node) = 0;
......
## Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
## Copyright (C) 2003, 2004, 2013 Laboratoire d'Informatique de Paris 6 (LIP6),
## dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre
## et Marie Curie.
##
......@@ -18,7 +18,7 @@
## along with this program. If not, see <http://www.gnu.org/licenses/>.
AM_CPPFLAGS = -I$(srcdir)/..
AM_CXXFLAGS = $(WARNING_CXXFLAGS)
AM_CXXFLAGS = $(WARNING_CXXFLAGS) $(VISIBILITY_CXXFLAGS)
ltlenvdir = $(pkgincludedir)/ltlenv
......
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2012 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2009, 2012, 2013 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
......@@ -38,7 +38,7 @@ namespace spot
///
/// This environment recognizes all atomic propositions
/// that have been previously declared. It will reject other.
class declarative_environment : public environment
class SPOT_API declarative_environment : public environment
{
public:
declarative_environment();
......
// -*- coding: utf-8 -*-
// Copyright (C) 2012 Laboratoire de Recherche et Développement
// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
......@@ -37,7 +37,7 @@ namespace spot
///
/// This is a singleton. Use default_environment::instance()
/// to obtain the instance.
class default_environment : public environment
class SPOT_API default_environment : public environment
{
public:
virtual ~default_environment();
......
......@@ -21,7 +21,7 @@
## along with this program. If not, see <http://www.gnu.org/licenses/>.
AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(BUDDY_CPPFLAGS)
AM_CXXFLAGS = $(WARNING_CXXFLAGS)
AM_CXXFLAGS = $(WARNING_CXXFLAGS) $(VISIBILITY_CXXFLAGS)
ltlvisitdir = $(pkgincludedir)/ltlvisit
......
// -*- coding: utf-8 -*-
// Copyright (C) 2012 Laboratoire de Recherche et Développement
// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
......@@ -23,8 +23,8 @@
#ifndef SPOT_LTLVISIT_APCOLLECT_HH
# define SPOT_LTLVISIT_APCOLLECT_HH
#include <set>
#include "ltlast/atomic_prop.hh"
#include <set>
#include "bdd.h"
namespace spot
......@@ -50,7 +50,7 @@ namespace spot
/// set containing all these atomic propositions if \c s is 0.
/// The atomic propositions inserted into \a s are not cloned, so
/// they are only valid as long as \a f is.
atomic_prop_set*
SPOT_API atomic_prop_set*
atomic_prop_collect(const formula* f, atomic_prop_set* s = 0);
/// \brief Return the set of atomic propositions occurring in a
......@@ -59,7 +59,7 @@ namespace spot
/// \param f the formula to inspect
/// \param a that automaton that should register the BDD variables used.
/// \return A conjunction the atomic propositions.
bdd
SPOT_API bdd
atomic_prop_collect_as_bdd(const formula* f, const tgba* a);
/// @}
......
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et
// Copyright (C) 2009, 2010, 2012, 2013 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
......@@ -37,7 +37,7 @@ namespace spot
/// to derive from it and override part of its methods.
/// But if you just want the functionality, consider using
/// spot::ltl::formula::clone instead, it is way faster.
class clone_visitor : public visitor
class SPOT_API clone_visitor : public visitor
{
public:
clone_visitor();
......@@ -59,17 +59,11 @@ namespace spot
const formula* result_;
};
#if __GNUC__
/// \ingroup ltl_essential
/// \brief Clone a formula.
/// \deprecated Use f->clone() instead.
SPOT_API SPOT_DEPRECATED
const formula* clone(const formula* f) __attribute__ ((deprecated));
#else
/// \ingroup ltl_essential
/// \brief Clone a formula.
/// \deprecated Use f->clone() instead.
const formula* clone(const formula* f);
#endif
}
}
......
// Copyright (C) 2011, 2012 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE).
// -*- coding: utf-8 -*-
// Copyright (C) 2011, 2012, 2013 Laboratoire de Recherche et
// Developpement de l'Epita (LRDE).
// Copyright (C) 2006 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// This file is part of Spot, a model checking library.
......@@ -31,8 +32,8 @@ namespace spot
{
namespace ltl
{
// Check containment of language represented by LTL formulae.
class language_containment_checker
/// Check containment between LTL formulae.
class SPOT_API language_containment_checker
{
struct record_
{
......@@ -44,7 +45,7 @@ namespace spot
record_, formula_ptr_hash> trans_map;
public:
/// This class uses spot::ltl_to_tgba_fm to translate LTL
/// formulae. See that class for the meaning of these options.
/// formulae. See that function for the meaning of these options.
language_containment_checker(bdd_dict* dict, bool exprop,
bool symb_merge,
bool branching_postponement,
......@@ -106,13 +107,9 @@ namespace spot
/// reduce some U, R, and X usages.
///
/// \deprecated Use spot::ltl::ltl_simplifier instead.
#if __GNUC__
SPOT_API SPOT_DEPRECATED
const formula* reduce_tau03(const formula* f,
bool stronger = true)
__attribute__ ((deprecated));
#else
const formula* reduce_tau03(const formula* f, bool stronger = true);
#endif
bool stronger = true);
}
}
......
// Copyright (C) 2009 Laboratoire de Recherche et Développement
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2013 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// This file is part of Spot, a model checking library.
......@@ -22,23 +23,18 @@
#ifndef SPOT_LTLVISIT_DESTROY_HH
# define SPOT_LTLVISIT_DESTROY_HH
#include "ltlvisit/postfix.hh"
# include "misc/common.hh"
# include "ltlvisit/postfix.hh"
namespace spot
{
namespace ltl
{
#if __GNUC__
/// \ingroup ltl_essential
/// \brief Destroys a formula
/// \deprecated Use f->destroy() instead.
void destroy(const formula *f) __attribute__ ((deprecated));
#else
/// \ingroup ltl_essential
/// \brief Destroys a formula
/// \deprecated Use f->destroy() instead.
SPOT_API SPOT_DEPRECATED
void destroy(const formula *f);
#endif
}
}
......
// -*- coding: utf-8 -*-
// Copyright (C) 2013 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// This file is part of Spot, a model checking library.
......@@ -34,6 +37,7 @@ namespace spot
///
/// \c dot is part of the GraphViz package
/// http://www.research.att.com/sw/tools/graphviz/
SPOT_API
std::ostream& dotty(std::ostream& os, const formula* f);
}
}
......
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre
// -*- coding: utf-8 -*-
// Copyright (C) 2013 Laboratoire de Recherche et Développement de
// l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// This file is part of Spot, a model checking library.
......@@ -33,6 +36,7 @@ namespace spot
/// \param f The formula to dump.
///
/// This is useful to display a formula when debugging.
SPOT_API
std::ostream& dump(std::ostream& os, const formula* f);
}
}
......
// -*- coding: utf-8 -*-
// Copyright (C) 2012 Laboratoire de Recherche et
// Copyright (C) 2012, 2013 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
......@@ -41,7 +41,7 @@ namespace spot
///
/// \param f The formula to translate.
/// \param os The stream where it should be output.
std::ostream&
SPOT_API std::ostream&
to_lbt_string(const formula* f, std::ostream& os);
/// \brief Output an LTL formula as a string in LBT's format.
......@@ -53,7 +53,7 @@ namespace spot
/// rewrite these two operators using unabbreviate_wm().
///
/// \param f The formula to translate.
std::string
SPOT_API std::string
to_lbt_string(const formula* f);
/// @}
}
......
// Copyright (C) 2012 Laboratoire de Recherche et Developement de
// -*- coding: utf-8 -*-
// Copyright (C) 2012, 2013 Laboratoire de Recherche et Developement de
// l'Epita (LRDE).
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// This file is part of Spot, a model checking library.
......@@ -40,6 +41,7 @@ namespace spot
///
/// If squash_boolean is set, all Boolean formulae are assumed
/// to have length one.
SPOT_API
int length(const formula* f);
/// \ingroup ltl_misc
......@@ -47,6 +49,7 @@ namespace spot
///
/// This is similar to spot::ltl::length(), except all Boolean
/// formulae are assumed to have length one.
SPOT_API