From ac6b0c9432a75ac627ff2f391efd8f22ec7eda20 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 20 Feb 2018 21:42:59 +0100 Subject: [PATCH] include config.h in all *.cc files This helps working around missing C functions like strcasecmp that do not exist everywhere (e.g. on Cygwin), and for which lib/ supplies a replacement. Unfortunately we do not have such build in our current continuous integration suite, so we cannot easily detect files where such config.h inclusion would be useful. Therefore this patch simply makes it mandatory to include config.h in *.cc files. Including this in public *.hh file is currently forbidden. * spot/gen/automata.cc, spot/gen/formulas.cc, spot/kripke/fairkripke.cc, spot/kripke/kripke.cc, spot/ltsmin/ltsmin.cc, spot/misc/game.cc, spot/parseaut/fmterror.cc, spot/parsetl/fmterror.cc, spot/parsetl/parsetl.yy, spot/priv/bddalloc.cc, spot/priv/freelist.cc, spot/priv/satcommon.cc, spot/priv/trim.cc, spot/priv/weight.cc, spot/ta/ta.cc, spot/ta/taexplicit.cc, spot/ta/taproduct.cc, spot/ta/tgtaexplicit.cc, spot/ta/tgtaproduct.cc, spot/taalgos/dot.cc, spot/taalgos/emptinessta.cc, spot/taalgos/minimize.cc, spot/taalgos/reachiter.cc, spot/taalgos/statessetbuilder.cc, spot/taalgos/stats.cc, spot/taalgos/tgba2ta.cc, spot/tl/apcollect.cc, spot/tl/contain.cc, spot/tl/declenv.cc, spot/tl/defaultenv.cc, spot/tl/dot.cc, spot/tl/exclusive.cc, spot/tl/hierarchy.cc, spot/tl/length.cc, spot/tl/ltlf.cc, spot/tl/mark.cc, spot/tl/mutation.cc, spot/tl/nenoform.cc, spot/tl/print.cc, spot/tl/randomltl.cc, spot/tl/relabel.cc, spot/tl/remove_x.cc, spot/tl/simplify.cc, spot/tl/snf.cc, spot/tl/unabbrev.cc, spot/twa/acc.cc, spot/twa/bdddict.cc, spot/twa/bddprint.cc, spot/twa/formula2bdd.cc, spot/twa/taatgba.cc, spot/twa/twa.cc, spot/twa/twagraph.cc, spot/twa/twaproduct.cc, spot/twaalgos/aiger.cc, spot/twaalgos/alternation.cc, spot/twaalgos/are_isomorphic.cc, spot/twaalgos/bfssteps.cc, spot/twaalgos/canonicalize.cc, spot/twaalgos/cleanacc.cc, spot/twaalgos/cobuchi.cc, spot/twaalgos/complement.cc, spot/twaalgos/complete.cc, spot/twaalgos/compsusp.cc, spot/twaalgos/couvreurnew.cc, spot/twaalgos/cycles.cc, spot/twaalgos/degen.cc, spot/twaalgos/determinize.cc, spot/twaalgos/dot.cc, spot/twaalgos/dtbasat.cc, spot/twaalgos/dtwasat.cc, spot/twaalgos/dualize.cc, spot/twaalgos/emptiness.cc, spot/twaalgos/gtec/ce.cc, spot/twaalgos/gtec/gtec.cc, spot/twaalgos/gtec/sccstack.cc, spot/twaalgos/gtec/status.cc, spot/twaalgos/gv04.cc, spot/twaalgos/hoa.cc, spot/twaalgos/iscolored.cc, spot/twaalgos/isdet.cc, spot/twaalgos/isunamb.cc, spot/twaalgos/isweakscc.cc, spot/twaalgos/langmap.cc, spot/twaalgos/lbtt.cc, spot/twaalgos/ltl2taa.cc, spot/twaalgos/ltl2tgba_fm.cc, spot/twaalgos/magic.cc, spot/twaalgos/mask.cc, spot/twaalgos/minimize.cc, spot/twaalgos/neverclaim.cc, spot/twaalgos/parity.cc, spot/twaalgos/postproc.cc, spot/twaalgos/powerset.cc, spot/twaalgos/product.cc, spot/twaalgos/rabin2parity.cc, spot/twaalgos/randomgraph.cc, spot/twaalgos/randomize.cc, spot/twaalgos/reachiter.cc, spot/twaalgos/relabel.cc, spot/twaalgos/remfin.cc, spot/twaalgos/remprop.cc, spot/twaalgos/sbacc.cc, spot/twaalgos/sccfilter.cc, spot/twaalgos/sccinfo.cc, spot/twaalgos/se05.cc, spot/twaalgos/sepsets.cc, spot/twaalgos/simulation.cc, spot/twaalgos/split.cc, spot/twaalgos/stats.cc, spot/twaalgos/strength.cc, spot/twaalgos/stripacc.cc, spot/twaalgos/stutter.cc, spot/twaalgos/sum.cc, spot/twaalgos/tau03.cc, spot/twaalgos/tau03opt.cc, spot/twaalgos/totgba.cc, spot/twaalgos/toweak.cc, spot/twaalgos/translate.cc, spot/twaalgos/word.cc, tests/core/acc.cc, tests/core/bitvect.cc, tests/core/checkpsl.cc, tests/core/checkta.cc, tests/core/consterm.cc, tests/core/emptchk.cc, tests/core/equalsf.cc, tests/core/graph.cc, tests/core/ikwiad.cc, tests/core/intvcmp2.cc, tests/core/intvcomp.cc, tests/core/kind.cc, tests/core/kripkecat.cc, tests/core/length.cc, tests/core/ltlrel.cc, tests/core/ngraph.cc, tests/core/parity.cc, tests/core/randtgba.cc, tests/core/readltl.cc, tests/core/reduc.cc, tests/core/safra.cc, tests/core/sccif.cc, tests/core/syntimpl.cc, tests/core/taatgba.cc, tests/core/tostring.cc, tests/core/trival.cc, tests/core/twagraph.cc, tests/ltsmin/modelcheck.cc, spot/parseaut/scanaut.ll, spot/parsetl/scantl.ll: Include config.h. * spot/gen/Makefile.am, spot/graph/Makefile.am, spot/kripke/Makefile.am, spot/ltsmin/Makefile.am, spot/parseaut/Makefile.am, spot/parsetl/Makefile.am, spot/priv/Makefile.am, spot/ta/Makefile.am, spot/taalgos/Makefile.am, spot/tl/Makefile.am, spot/twa/Makefile.am, spot/twaalgos/Makefile.am, spot/twaalgos/gtec/Makefile.am, tests/Makefile.am: Add the -I lib/ flags. * tests/sanity/includes.test: Catch missing config.h in *.cc, and diagnose config.h in *.hh. * tests/sanity/style.test: Better diagnostics. --- spot/gen/Makefile.am | 7 +++--- spot/gen/automata.cc | 5 ++-- spot/gen/formulas.cc | 1 + spot/graph/Makefile.am | 5 ++-- spot/kripke/Makefile.am | 5 ++-- spot/kripke/fairkripke.cc | 5 ++-- spot/kripke/kripke.cc | 5 ++-- spot/ltsmin/Makefile.am | 7 ++++-- spot/ltsmin/ltsmin.cc | 1 + spot/misc/game.cc | 6 ++--- spot/parseaut/Makefile.am | 7 +++--- spot/parseaut/fmterror.cc | 3 ++- spot/parseaut/scanaut.ll | 6 +++-- spot/parsetl/Makefile.am | 7 +++--- spot/parsetl/fmterror.cc | 5 ++-- spot/parsetl/parsetl.yy | 3 ++- spot/parsetl/scantl.ll | 5 +++- spot/priv/Makefile.am | 7 +++--- spot/priv/bddalloc.cc | 5 ++-- spot/priv/freelist.cc | 3 ++- spot/priv/satcommon.cc | 3 ++- spot/priv/trim.cc | 5 ++-- spot/priv/weight.cc | 5 ++-- spot/ta/Makefile.am | 7 +++--- spot/ta/ta.cc | 3 ++- spot/ta/taexplicit.cc | 3 ++- spot/ta/taproduct.cc | 3 ++- spot/ta/tgtaexplicit.cc | 3 ++- spot/ta/tgtaproduct.cc | 3 ++- spot/taalgos/Makefile.am | 7 +++--- spot/taalgos/dot.cc | 3 ++- spot/taalgos/emptinessta.cc | 5 ++-- spot/taalgos/minimize.cc | 5 ++-- spot/taalgos/reachiter.cc | 3 ++- spot/taalgos/statessetbuilder.cc | 5 ++-- spot/taalgos/stats.cc | 5 ++-- spot/taalgos/tgba2ta.cc | 3 ++- spot/tl/Makefile.am | 5 ++-- spot/tl/apcollect.cc | 5 ++-- spot/tl/contain.cc | 5 ++-- spot/tl/declenv.cc | 5 ++-- spot/tl/defaultenv.cc | 3 ++- spot/tl/dot.cc | 5 ++-- spot/tl/exclusive.cc | 13 +++++----- spot/tl/hierarchy.cc | 3 ++- spot/tl/length.cc | 3 ++- spot/tl/ltlf.cc | 5 ++-- spot/tl/mark.cc | 5 ++-- spot/tl/mutation.cc | 3 ++- spot/tl/nenoform.cc | 3 ++- spot/tl/print.cc | 3 ++- spot/tl/randomltl.cc | 5 ++-- spot/tl/relabel.cc | 5 ++-- spot/tl/remove_x.cc | 3 ++- spot/tl/simplify.cc | 3 ++- spot/tl/snf.cc | 5 ++-- spot/tl/unabbrev.cc | 3 ++- spot/twa/Makefile.am | 7 +++--- spot/twa/acc.cc | 5 ++-- spot/twa/bdddict.cc | 9 +++---- spot/twa/bddprint.cc | 5 ++-- spot/twa/formula2bdd.cc | 3 ++- spot/twa/taatgba.cc | 3 ++- spot/twa/twa.cc | 3 ++- spot/twa/twagraph.cc | 1 + spot/twa/twaproduct.cc | 5 ++-- spot/twaalgos/Makefile.am | 5 ++-- spot/twaalgos/aiger.cc | 3 ++- spot/twaalgos/alternation.cc | 3 ++- spot/twaalgos/are_isomorphic.cc | 3 ++- spot/twaalgos/bfssteps.cc | 5 ++-- spot/twaalgos/canonicalize.cc | 3 ++- spot/twaalgos/cleanacc.cc | 1 + spot/twaalgos/cobuchi.cc | 41 ++++++++++++++++---------------- spot/twaalgos/complement.cc | 3 ++- spot/twaalgos/complete.cc | 3 ++- spot/twaalgos/compsusp.cc | 3 ++- spot/twaalgos/couvreurnew.cc | 3 ++- spot/twaalgos/cycles.cc | 3 ++- spot/twaalgos/degen.cc | 2 +- spot/twaalgos/determinize.cc | 1 + spot/twaalgos/dot.cc | 3 ++- spot/twaalgos/dtbasat.cc | 33 ++++++++++++------------- spot/twaalgos/dtwasat.cc | 33 ++++++++++++------------- spot/twaalgos/dualize.cc | 11 +++++---- spot/twaalgos/emptiness.cc | 3 ++- spot/twaalgos/gtec/Makefile.am | 7 +++--- spot/twaalgos/gtec/ce.cc | 3 ++- spot/twaalgos/gtec/gtec.cc | 3 ++- spot/twaalgos/gtec/sccstack.cc | 3 ++- spot/twaalgos/gtec/status.cc | 5 ++-- spot/twaalgos/gv04.cc | 3 ++- spot/twaalgos/hoa.cc | 6 ++--- spot/twaalgos/iscolored.cc | 5 ++-- spot/twaalgos/isdet.cc | 3 ++- spot/twaalgos/isunamb.cc | 3 ++- spot/twaalgos/isweakscc.cc | 3 ++- spot/twaalgos/langmap.cc | 3 ++- spot/twaalgos/lbtt.cc | 11 +++++---- spot/twaalgos/ltl2taa.cc | 5 ++-- spot/twaalgos/ltl2tgba_fm.cc | 3 ++- spot/twaalgos/magic.cc | 3 ++- spot/twaalgos/mask.cc | 3 ++- spot/twaalgos/minimize.cc | 4 ++-- spot/twaalgos/neverclaim.cc | 5 ++-- spot/twaalgos/parity.cc | 1 + spot/twaalgos/postproc.cc | 1 + spot/twaalgos/powerset.cc | 1 + spot/twaalgos/product.cc | 1 + spot/twaalgos/rabin2parity.cc | 6 ++--- spot/twaalgos/randomgraph.cc | 3 ++- spot/twaalgos/randomize.cc | 3 ++- spot/twaalgos/reachiter.cc | 3 ++- spot/twaalgos/relabel.cc | 3 ++- spot/twaalgos/remfin.cc | 1 + spot/twaalgos/remprop.cc | 11 +++++---- spot/twaalgos/sbacc.cc | 3 ++- spot/twaalgos/sccfilter.cc | 3 ++- spot/twaalgos/sccinfo.cc | 3 ++- spot/twaalgos/se05.cc | 3 ++- spot/twaalgos/sepsets.cc | 3 ++- spot/twaalgos/simulation.cc | 3 ++- spot/twaalgos/split.cc | 3 ++- spot/twaalgos/stats.cc | 5 ++-- spot/twaalgos/strength.cc | 5 ++-- spot/twaalgos/stripacc.cc | 5 ++-- spot/twaalgos/stutter.cc | 1 + spot/twaalgos/sum.cc | 5 ++-- spot/twaalgos/tau03.cc | 3 ++- spot/twaalgos/tau03opt.cc | 3 ++- spot/twaalgos/totgba.cc | 37 ++++++++++++++-------------- spot/twaalgos/toweak.cc | 1 + spot/twaalgos/translate.cc | 3 ++- spot/twaalgos/word.cc | 3 ++- tests/Makefile.am | 3 ++- tests/core/acc.cc | 3 ++- tests/core/bitvect.cc | 3 ++- tests/core/checkpsl.cc | 5 ++-- tests/core/checkta.cc | 3 ++- tests/core/consterm.cc | 3 ++- tests/core/emptchk.cc | 3 ++- tests/core/equalsf.cc | 3 ++- tests/core/graph.cc | 4 ++-- tests/core/ikwiad.cc | 1 + tests/core/intvcmp2.cc | 5 ++-- tests/core/intvcomp.cc | 3 ++- tests/core/kind.cc | 5 ++-- tests/core/kripkecat.cc | 4 ++-- tests/core/length.cc | 3 ++- tests/core/ltlrel.cc | 5 ++-- tests/core/ngraph.cc | 2 +- tests/core/parity.cc | 3 ++- tests/core/randtgba.cc | 3 ++- tests/core/readltl.cc | 5 ++-- tests/core/reduc.cc | 3 ++- tests/core/safra.cc | 5 ++-- tests/core/sccif.cc | 3 ++- tests/core/syntimpl.cc | 5 ++-- tests/core/taatgba.cc | 5 ++-- tests/core/tostring.cc | 5 ++-- tests/core/trival.cc | 5 ++-- tests/core/twagraph.cc | 4 ++-- tests/ltsmin/modelcheck.cc | 5 ++-- tests/sanity/includes.test | 13 +++++----- tests/sanity/style.test | 23 ++++++++++++++---- 165 files changed, 493 insertions(+), 324 deletions(-) diff --git a/spot/gen/Makefile.am b/spot/gen/Makefile.am index ed668cfd4..b8249f1e5 100644 --- a/spot/gen/Makefile.am +++ b/spot/gen/Makefile.am @@ -1,6 +1,6 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2017 Laboratoire de Recherche et Développement de l'Epita -## (LRDE). +## Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement +## de l'Epita (LRDE). ## ## This file is part of Spot, a model checking library. ## @@ -17,7 +17,8 @@ ## You should have received a copy of the GNU General Public License ## along with this program. If not, see . -AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) +AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) \ + -I$(top_builddir)/lib -I$(top_srcdir)/lib AM_CXXFLAGS = $(WARNING_CXXFLAGS) spotgendir = $(pkgincludedir)/gen diff --git a/spot/gen/automata.cc b/spot/gen/automata.cc index e634d4e8a..bf1785dd3 100644 --- a/spot/gen/automata.cc +++ b/spot/gen/automata.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017 Laboratoire de Recherche et Developpement de -// l'EPITA (LRDE). +// Copyright (C) 2017-2018 Laboratoire de Recherche et Developpement +// de l'EPITA (LRDE). // // This file is part of Spot, a model checking library. // @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/gen/formulas.cc b/spot/gen/formulas.cc index d9dd5eab9..b50062252 100644 --- a/spot/gen/formulas.cc +++ b/spot/gen/formulas.cc @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include diff --git a/spot/graph/Makefile.am b/spot/graph/Makefile.am index 9af6d639c..87723057a 100644 --- a/spot/graph/Makefile.am +++ b/spot/graph/Makefile.am @@ -1,5 +1,5 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2014 Laboratoire de Recherche et Développement de +## Copyright (C) 2014, 2018 Laboratoire de Recherche et Développement de ## l'Epita (LRDE). ## ## This file is part of Spot, a model checking library. @@ -18,7 +18,8 @@ ## along with this program. If not, see . -AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) +AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) \ + -I$(top_builddir)/lib -I$(top_srcdir)/lib AM_CXXFLAGS = $(WARNING_CXXFLAGS) graphdir = $(pkgincludedir)/graph diff --git a/spot/kripke/Makefile.am b/spot/kripke/Makefile.am index 2b8d80a8f..90161378e 100644 --- a/spot/kripke/Makefile.am +++ b/spot/kripke/Makefile.am @@ -1,5 +1,5 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2009, 2011, 2013, 2014, 2015 Laboratoire de Recherche +## Copyright (C) 2009, 2011, 2013-2015, 2018 Laboratoire de Recherche ## et Developpement de l'Epita (LRDE). ## ## This file is part of Spot, a model checking library. @@ -17,7 +17,8 @@ ## You should have received a copy of the GNU General Public License ## along with this program. If not, see . -AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) +AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) \ + -I$(top_builddir)/lib -I$(top_srcdir)/lib AM_CXXFLAGS = $(WARNING_CXXFLAGS) kripkedir = $(pkgincludedir)/kripke diff --git a/spot/kripke/fairkripke.cc b/spot/kripke/fairkripke.cc index 5d8c059cc..70d44a2b4 100644 --- a/spot/kripke/fairkripke.cc +++ b/spot/kripke/fairkripke.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2014, 2016 Laboratoire de Recherche et -// Developpement de l'Epita +// Copyright (C) 2009, 2010, 2014, 2016, 2018 Laboratoire de Recherche +// et Developpement de l'Epita // // This file is part of Spot, a model checking library. // @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include namespace spot diff --git a/spot/kripke/kripke.cc b/spot/kripke/kripke.cc index cbec796fa..07beb6b10 100644 --- a/spot/kripke/kripke.cc +++ b/spot/kripke/kripke.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2014, 2016 Laboratoire de Recherche et -// Developpement de l'Epita +// Copyright (C) 2009, 2010, 2014, 2016, 2018 Laboratoire de Recherche +// et Developpement de l'Epita // // This file is part of Spot, a model checking library. // @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include namespace spot diff --git a/spot/ltsmin/Makefile.am b/spot/ltsmin/Makefile.am index 3204ba4c9..6f3b6ae3d 100644 --- a/spot/ltsmin/Makefile.am +++ b/spot/ltsmin/Makefile.am @@ -1,5 +1,5 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2011, 2013, 2014, 2015, 2016, 2017 Laboratoire de +## Copyright (C) 2011, 2013, 2014, 2015, 2016, 2017, 2018 Laboratoire de ## Recherche et Developpement de l'Epita (LRDE). ## ## This file is part of Spot, a model checking library. @@ -18,7 +18,8 @@ ## along with this program. If not, see . AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) \ - $(BUDDY_CPPFLAGS) $(LTDLINCL) + $(BUDDY_CPPFLAGS) $(LTDLINCL) \ + -I$(top_builddir)/lib -I$(top_srcdir)/lib AM_CXXFLAGS = $(WARNING_CXXFLAGS) ltsmindir = $(pkgincludedir)/ltsmin @@ -29,10 +30,12 @@ lib_LTLIBRARIES = libspotltsmin.la libspotltsmin_la_DEPENDENCIES = \ $(top_builddir)/spot/libspot.la \ $(top_builddir)/buddy/src/libbddx.la \ + $(top_builddir)/lib/libgnu.la \ $(LTDLDEPS) libspotltsmin_la_LIBADD = \ $(top_builddir)/spot/libspot.la \ $(top_builddir)/buddy/src/libbddx.la \ + $(top_builddir)/lib/libgnu.la \ $(LIBLTDL) -lpthread libspotltsmin_la_LDFLAGS = -no-undefined $(SYMBOLIC_LDFLAGS) libspotltsmin_la_SOURCES = ltsmin.cc diff --git a/spot/ltsmin/ltsmin.cc b/spot/ltsmin/ltsmin.cc index 7757f554a..c893793b7 100644 --- a/spot/ltsmin/ltsmin.cc +++ b/spot/ltsmin/ltsmin.cc @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/misc/game.cc b/spot/misc/game.cc index b8c51587c..ea897d5e5 100644 --- a/spot/misc/game.cc +++ b/spot/misc/game.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017 Laboratoire de Recherche et Développement +// Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -17,10 +17,10 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . -#include +#include "config.h" #include -#include "spot/misc/game.hh" +#include namespace spot { diff --git a/spot/parseaut/Makefile.am b/spot/parseaut/Makefile.am index 56d56fa4b..8d34c5605 100644 --- a/spot/parseaut/Makefile.am +++ b/spot/parseaut/Makefile.am @@ -1,6 +1,6 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement de -## l'Epita (LRDE). +## Copyright (C) 2013, 2014, 2018 Laboratoire de Recherche et +## Développement de l'Epita (LRDE). ## ## This file is part of Spot, a model checking library. ## @@ -17,7 +17,8 @@ ## You should have received a copy of the GNU General Public License ## along with this program. If not, see . -AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) -DYY_NO_INPUT +AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) \ + -DYY_NO_INPUT -I$(top_builddir)/lib -I$(top_srcdir)/lib # Disable -Werror because too many versions of flex yield warnings. AM_CXXFLAGS = $(WARNING_CXXFLAGS:-Werror=) diff --git a/spot/parseaut/fmterror.cc b/spot/parseaut/fmterror.cc index 9175a263e..49db70b41 100644 --- a/spot/parseaut/fmterror.cc +++ b/spot/parseaut/fmterror.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et +// Copyright (C) 2013-2015, 2018 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include diff --git a/spot/parseaut/scanaut.ll b/spot/parseaut/scanaut.ll index aef870ae5..728404c3d 100644 --- a/spot/parseaut/scanaut.ll +++ b/spot/parseaut/scanaut.ll @@ -1,5 +1,5 @@ /* -*- coding: utf-8 -*- -** Copyright (C) 2014-2017 Laboratoire de Recherche et Développement +** Copyright (C) 2014-2018 Laboratoire de Recherche et Développement ** de l'Epita (LRDE). ** ** This file is part of Spot, a model checking library. @@ -24,7 +24,9 @@ %option extra-type="struct extra_data*" /* %option debug */ - +%top{ +#include "config.h" +} %{ #include #include diff --git a/spot/parsetl/Makefile.am b/spot/parsetl/Makefile.am index 3a8edf31e..d98c9ebab 100644 --- a/spot/parsetl/Makefile.am +++ b/spot/parsetl/Makefile.am @@ -1,6 +1,6 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015 -## Laboratoire de Recherche et Développement de l'Epita (LRDE). +## Copyright (C) 2008-2015, 2018 Laboratoire de Recherche et +## Développement de l'Epita (LRDE). ## Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris ## 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), ## Université Pierre et Marie Curie. @@ -20,7 +20,8 @@ ## You should have received a copy of the GNU General Public License ## along with this program. If not, see . -AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) -DYY_NO_INPUT +AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) -DYY_NO_INPUT \ + -I$(top_builddir)/lib -I$(top_srcdir)/lib # Disable -Werror because too many versions of flex yield warnings. AM_CXXFLAGS = $(WARNING_CXXFLAGS:-Werror=) diff --git a/spot/parsetl/fmterror.cc b/spot/parsetl/fmterror.cc index a8b262874..eb13c9459 100644 --- a/spot/parsetl/fmterror.cc +++ b/spot/parsetl/fmterror.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2012, 2013, 2015, 2016 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2010, 2012-2013, 2015-2016, 2018 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. @@ -20,6 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/parsetl/parsetl.yy b/spot/parsetl/parsetl.yy index 69b619252..369204f18 100644 --- a/spot/parsetl/parsetl.yy +++ b/spot/parsetl/parsetl.yy @@ -1,6 +1,6 @@ /* -*- coding: utf-8 -*- -** Copyright (C) 2009-2017 Laboratoire de Recherche et Développement +** Copyright (C) 2009-2018 Laboratoire de Recherche et Développement ** de l'Epita (LRDE). ** Copyright (C) 2003-2006 Laboratoire d'Informatique de Paris 6 ** (LIP6), département Systèmes Répartis Coopératifs (SRC), Université @@ -33,6 +33,7 @@ %code requires { +#include "config.h" #include #include #include diff --git a/spot/parsetl/scantl.ll b/spot/parsetl/scantl.ll index 256543726..4f2c53512 100644 --- a/spot/parsetl/scantl.ll +++ b/spot/parsetl/scantl.ll @@ -1,5 +1,5 @@ /* -*- coding: utf-8 -*- -** Copyright (C) 2010-2015, 2017, Laboratoire de Recherche et +** Copyright (C) 2010-2015, 2017, 2018, 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 @@ -26,6 +26,9 @@ %option stack %option never-interactive +%top{ +#include "config.h" +} %{ #include #include diff --git a/spot/priv/Makefile.am b/spot/priv/Makefile.am index 09c35cb1c..13317e41d 100644 --- a/spot/priv/Makefile.am +++ b/spot/priv/Makefile.am @@ -1,6 +1,6 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2013, 2014, 2015, 2016, 2017 Laboratoire de Recherche -## et Développement de l'Epita (LRDE). +## Copyright (C) 2013-2018 Laboratoire de Recherche et Développement +## de l'Epita (LRDE). ## ## This file is part of Spot, a model checking library. ## @@ -17,7 +17,8 @@ ## You should have received a copy of the GNU General Public License ## along with this program. If not, see . -AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) +AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) \ + -I$(top_builddir)/lib -I$(top_srcdir)/lib AM_CXXFLAGS = $(WARNING_CXXFLAGS) noinst_LTLIBRARIES = libpriv.la diff --git a/spot/priv/bddalloc.cc b/spot/priv/bddalloc.cc index 7ee299714..3ce691c0f 100644 --- a/spot/priv/bddalloc.cc +++ b/spot/priv/bddalloc.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2007, 2011, 2014, 2015, 2017 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2007, 2011, 2014, 2015, 2017, 2018 Laboratoire de +// Recherche et Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2006, 2007 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. @@ -20,6 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/priv/freelist.cc b/spot/priv/freelist.cc index 4b806afc9..f93c9428f 100644 --- a/spot/priv/freelist.cc +++ b/spot/priv/freelist.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014 Laboratoire de Recherche et Développement de +// Copyright (C) 2014, 2018 Laboratoire de Recherche et Développement de // l'Epita. // Copyright (C) 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -20,6 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include "spot/priv/freelist.hh" #include #include diff --git a/spot/priv/satcommon.cc b/spot/priv/satcommon.cc index 999086616..6d9e0a675 100644 --- a/spot/priv/satcommon.cc +++ b/spot/priv/satcommon.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013-2017 Laboratoire de Recherche et Développement +// Copyright (C) 2013-2018 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -18,6 +18,7 @@ // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/priv/trim.cc b/spot/priv/trim.cc index 12b3c95e6..ad8dbbf64 100644 --- a/spot/priv/trim.cc +++ b/spot/priv/trim.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015 Laboratoire de Recherche et Developpement de -// l'Epita (LRDE). +// Copyright (C) 2015, 2018 Laboratoire de Recherche et Developpement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/priv/weight.cc b/spot/priv/weight.cc index 18f0009d5..ec3e02baf 100644 --- a/spot/priv/weight.cc +++ b/spot/priv/weight.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2014, 2016, 2017 Laboratoire de Recherche et -// Developpement de l'Epita. +// Copyright (C) 2011, 2014, 2016, 2017, 2018 Laboratoire de Recherche +// et Developpement de l'Epita. // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -20,6 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/ta/Makefile.am b/spot/ta/Makefile.am index 3498fc64f..12f7196b1 100644 --- a/spot/ta/Makefile.am +++ b/spot/ta/Makefile.am @@ -1,6 +1,6 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2010, 2012, 2013, 2015 Laboratoire de Recherche et -## Développement de l'Epita (LRDE). +## Copyright (C) 2010, 2012, 2013, 2015, 2018 Laboratoire de Recherche +## et Développement de l'Epita (LRDE). ## ## This file is part of Spot, a model checking library. ## @@ -17,7 +17,8 @@ ## You should have received a copy of the GNU General Public License ## along with this program. If not, see . -AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) +AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) \ + -I$(top_builddir)/lib -I$(top_srcdir)/lib AM_CXXFLAGS = $(WARNING_CXXFLAGS) tadir = $(pkgincludedir)/ta diff --git a/spot/ta/ta.cc b/spot/ta/ta.cc index f371beca9..84d3db390 100644 --- a/spot/ta/ta.cc +++ b/spot/ta/ta.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2014 Laboratoire de Recherche et +// Copyright (C) 2010, 2011, 2014, 2018 Laboratoire de Recherche et // Developpement de l Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -18,6 +18,7 @@ // along with this program. If not, see . +#include "config.h" #include namespace spot diff --git a/spot/ta/taexplicit.cc b/spot/ta/taexplicit.cc index 075f725ed..457bf0ff8 100644 --- a/spot/ta/taexplicit.cc +++ b/spot/ta/taexplicit.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010-2017 Laboratoire de Recherche et Développement de +// Copyright (C) 2010-2018 Laboratoire de Recherche et Développement de // l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -19,6 +19,7 @@ //#define TRACE +#include "config.h" #include #ifdef TRACE #define trace std::clog diff --git a/spot/ta/taproduct.cc b/spot/ta/taproduct.cc index d6975d293..f5728560d 100644 --- a/spot/ta/taproduct.cc +++ b/spot/ta/taproduct.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012, 2014-2017 Laboratoire de Recherche et +// Copyright (C) 2011, 2012, 2014-2018 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // @@ -18,6 +18,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/ta/tgtaexplicit.cc b/spot/ta/tgtaexplicit.cc index 40af1632e..694636583 100644 --- a/spot/ta/tgtaexplicit.cc +++ b/spot/ta/tgtaexplicit.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2012, 2014, 2015, 2016 Laboratoire de +// Copyright (C) 2010-2012, 2014-2016, 2018 Laboratoire de // Recherche et Developpement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/ta/tgtaproduct.cc b/spot/ta/tgtaproduct.cc index e49c6d629..f073fbdbd 100644 --- a/spot/ta/tgtaproduct.cc +++ b/spot/ta/tgtaproduct.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2014-2017 Laboratoire de Recherche et Développement de +// Copyright (C) 2012, 2014-2018 Laboratoire de Recherche et Développement de // l Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -20,6 +20,7 @@ //#define TRACE +#include "config.h" #include #ifdef TRACE #define trace std::clog diff --git a/spot/taalgos/Makefile.am b/spot/taalgos/Makefile.am index 29d15f4a8..958900947 100644 --- a/spot/taalgos/Makefile.am +++ b/spot/taalgos/Makefile.am @@ -1,6 +1,6 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2010, 2012, 2013, 2015 Laboratoire de Recherche et -## Développement de l'Epita (LRDE). +## Copyright (C) 2010, 2012, 2013, 2015, 2018 Laboratoire de Recherche +## et Développement de l'Epita (LRDE). ## ## This file is part of Spot, a model checking library. ## @@ -18,7 +18,8 @@ ## along with this program. If not, see . -AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) -I.. $(BUDDY_CPPFLAGS) +AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) -I.. $(BUDDY_CPPFLAGS) \ + -I$(top_builddir)/lib -I$(top_srcdir)/lib AM_CXXFLAGS = $(WARNING_CXXFLAGS) taalgosdir = $(pkgincludedir)/taalgos diff --git a/spot/taalgos/dot.cc b/spot/taalgos/dot.cc index c6a612218..39e69e683 100644 --- a/spot/taalgos/dot.cc +++ b/spot/taalgos/dot.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2012, 2014, 2015, 2016 Laboratoire de Recherche +// Copyright (C) 2010, 2012, 2014-2016, 2018 Laboratoire de Recherche // et Developpement de l Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/taalgos/emptinessta.cc b/spot/taalgos/emptinessta.cc index 952e54073..152afc110 100644 --- a/spot/taalgos/emptinessta.cc +++ b/spot/taalgos/emptinessta.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire -// de Recherche et Développement de l'Epita (LRDE). +// Copyright (C) 2010-2016, 2018 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -19,6 +19,7 @@ //#define TRACE +#include "config.h" #include #ifdef TRACE #define trace std::clog diff --git a/spot/taalgos/minimize.cc b/spot/taalgos/minimize.cc index bea3fd2e6..b2b12cb12 100644 --- a/spot/taalgos/minimize.cc +++ b/spot/taalgos/minimize.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire -// de Recherche et Développement de l'Epita (LRDE). +// Copyright (C) 2010-2016, 2018 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -20,6 +20,7 @@ //#define TRACE +#include "config.h" #ifdef TRACE # define trace std::cerr #else diff --git a/spot/taalgos/reachiter.cc b/spot/taalgos/reachiter.cc index f60e504dd..44f52e4d0 100644 --- a/spot/taalgos/reachiter.cc +++ b/spot/taalgos/reachiter.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2012, 2014, 2015, 2016 Laboratoire de Recherche +// Copyright (C) 2010, 2012, 2014-2016, 2018 Laboratoire de Recherche // et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include diff --git a/spot/taalgos/statessetbuilder.cc b/spot/taalgos/statessetbuilder.cc index 7e1a611d2..68c4046fa 100644 --- a/spot/taalgos/statessetbuilder.cc +++ b/spot/taalgos/statessetbuilder.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2014, 2016 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2010, 2014, 2016, 2018 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/taalgos/stats.cc b/spot/taalgos/stats.cc index f7851834c..1787f6a27 100644 --- a/spot/taalgos/stats.cc +++ b/spot/taalgos/stats.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2014, 2015, 2016 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2008, 2014, 2015, 2016, 2018 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. @@ -20,6 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/taalgos/tgba2ta.cc b/spot/taalgos/tgba2ta.cc index 434d47a46..e088ffa18 100644 --- a/spot/taalgos/tgba2ta.cc +++ b/spot/taalgos/tgba2ta.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010-2017 Laboratoire de Recherche et Développement de +// Copyright (C) 2010-2018 Laboratoire de Recherche et Développement de // l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -19,6 +19,7 @@ //#define TRACE +#include "config.h" #include #ifdef TRACE #define trace std::clog diff --git a/spot/tl/Makefile.am b/spot/tl/Makefile.am index e997811b5..b7362ae99 100644 --- a/spot/tl/Makefile.am +++ b/spot/tl/Makefile.am @@ -1,5 +1,5 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et +## Copyright (C) 2015-2018 Laboratoire de Recherche et ## Développement de l'Epita (LRDE). ## ## This file is part of Spot, a model checking library. @@ -17,7 +17,8 @@ ## You should have received a copy of the GNU General Public License ## along with this program. If not, see . -AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) +AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) \ + -I$(top_builddir)/lib -I$(top_srcdir)/lib AM_CXXFLAGS = $(WARNING_CXXFLAGS) tldir = $(pkgincludedir)/tl diff --git a/spot/tl/apcollect.cc b/spot/tl/apcollect.cc index 65b092470..e1f11372d 100644 --- a/spot/tl/apcollect.cc +++ b/spot/tl/apcollect.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2014, 2015 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2012, 2014, 2015, 2018 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 // et Marie Curie. @@ -20,6 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/tl/contain.cc b/spot/tl/contain.cc index a60a7ac3b..19c3b7158 100644 --- a/spot/tl/contain.cc +++ b/spot/tl/contain.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012, 2014, 2015, 2016 Laboratoire de -// Recherche et Développement de l'Epita (LRDE). +// Copyright (C) 2009-2012, 2014-2016, 2018 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // Copyright (C) 2006, 2007 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -20,6 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/tl/declenv.cc b/spot/tl/declenv.cc index b044bc522..cad6466cd 100644 --- a/spot/tl/declenv.cc +++ b/spot/tl/declenv.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2012, 2014, 2015 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2012, 2014, 2015, 2018 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. @@ -20,6 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include namespace spot diff --git a/spot/tl/defaultenv.cc b/spot/tl/defaultenv.cc index cbf817283..ae3c22643 100644 --- a/spot/tl/defaultenv.cc +++ b/spot/tl/defaultenv.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2014, 2015 Laboratoire de Recherche et +// Copyright (C) 2012, 2014, 2015, 2018 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -20,6 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include namespace spot diff --git a/spot/tl/dot.cc b/spot/tl/dot.cc index 1f8dbf157..be6e2ac6b 100644 --- a/spot/tl/dot.cc +++ b/spot/tl/dot.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire -// de Recherche et Développement de l'Epita (LRDE). +// Copyright (C) 2009-2015, 2018 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université // Pierre et Marie Curie. @@ -20,6 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/tl/exclusive.cc b/spot/tl/exclusive.cc index 35e70c020..979b8fe94 100644 --- a/spot/tl/exclusive.cc +++ b/spot/tl/exclusive.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015-2017 Laboratoire de Recherche et Développement +// Copyright (C) 2015-2018 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include @@ -154,7 +155,7 @@ namespace spot support &= bdd_support(t.cond); } - bdd restrict = bddtrue; + bdd restrict_ = bddtrue; auto d = aut->get_dict(); std::vector group; @@ -172,7 +173,7 @@ namespace spot unsigned s = group.size(); for (unsigned j = 0; j < s; ++j) for (unsigned k = j + 1; k < s; ++k) - restrict &= group[j] | group[k]; + restrict_ &= group[j] | group[k]; } twa_graph_ptr res = make_twa_graph(aut->get_dict()); @@ -184,8 +185,8 @@ namespace spot transform_accessible(aut, res, [&](unsigned, bdd& cond, acc_cond::mark_t&, unsigned) { - minato_isop isop(cond & restrict, - cond | !restrict, + minato_isop isop(cond & restrict_, + cond | !restrict_, true); bdd res = bddfalse; bdd cube = bddfalse; @@ -200,7 +201,7 @@ namespace spot transform_accessible(aut, res, [&](unsigned, bdd& cond, acc_cond::mark_t&, unsigned) { - cond &= restrict; + cond &= restrict_; }); } return res; diff --git a/spot/tl/hierarchy.cc b/spot/tl/hierarchy.cc index 4f042799a..7b9716f5a 100644 --- a/spot/tl/hierarchy.cc +++ b/spot/tl/hierarchy.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017 Laboratoire de Recherche et Développement de +// Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement de // l'Epita (LRDE) // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/tl/length.cc b/spot/tl/length.cc index 789df65b2..2793a6af5 100644 --- a/spot/tl/length.cc +++ b/spot/tl/length.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2012, 2014, 2015 Laboratoire de Recherche et +// Copyright (C) 2010, 2012, 2014, 2015, 2018 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 @@ -20,6 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include diff --git a/spot/tl/ltlf.cc b/spot/tl/ltlf.cc index 74532eabb..a6a61fe96 100644 --- a/spot/tl/ltlf.cc +++ b/spot/tl/ltlf.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2016 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// Copyright (C) 2016, 2018 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include namespace spot diff --git a/spot/tl/mark.cc b/spot/tl/mark.cc index b6e83ccca..ec17d78d3 100644 --- a/spot/tl/mark.cc +++ b/spot/tl/mark.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2012, 2014, 2015 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2010, 2012, 2014, 2015, 2018 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/tl/mutation.cc b/spot/tl/mutation.cc index 6bee8e1e8..7c704dba5 100644 --- a/spot/tl/mutation.cc +++ b/spot/tl/mutation.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et +// Copyright (C) 2014-2016, 2018 Laboratoire de Recherche et // Developpement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include diff --git a/spot/tl/nenoform.cc b/spot/tl/nenoform.cc index 7283080c8..8705960df 100644 --- a/spot/tl/nenoform.cc +++ b/spot/tl/nenoform.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2015 Laboratoire de +// Copyright (C) 2009-2013, 2015, 2018 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 @@ -20,6 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include diff --git a/spot/tl/print.cc b/spot/tl/print.cc index f46dc4976..5bbb0cf98 100644 --- a/spot/tl/print.cc +++ b/spot/tl/print.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2010, 2012, 2013, 2014, 2015, 2016 Laboratoire de +// Copyright (C) 2008, 2010, 2012-2016, 2018 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 @@ -20,6 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/tl/randomltl.cc b/spot/tl/randomltl.cc index f7ff25162..a284b0690 100644 --- a/spot/tl/randomltl.cc +++ b/spot/tl/randomltl.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014, 2015, 2016 -// Laboratoire de Recherche et Développement de l'Epita (LRDE). +// Copyright (C) 2008-2012, 2014-2016, 2018 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université // Pierre et Marie Curie. @@ -20,6 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/tl/relabel.cc b/spot/tl/relabel.cc index 838fe19c5..383f559c1 100644 --- a/spot/tl/relabel.cc +++ b/spot/tl/relabel.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2012-2016, 2018 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/tl/remove_x.cc b/spot/tl/remove_x.cc index 582036103..4ab27d1d7 100644 --- a/spot/tl/remove_x.cc +++ b/spot/tl/remove_x.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et +// Copyright (C) 2013, 2014, 2015, 2018 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/tl/simplify.cc b/spot/tl/simplify.cc index 8c4e82bb9..1332d24dc 100644 --- a/spot/tl/simplify.cc +++ b/spot/tl/simplify.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011-2017 Laboratoire de Recherche et Developpement +// Copyright (C) 2011-2018 Laboratoire de Recherche et Developpement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include //#define TRACE #ifdef TRACE diff --git a/spot/tl/snf.cc b/spot/tl/snf.cc index e234a44d2..e525fe6df 100644 --- a/spot/tl/snf.cc +++ b/spot/tl/snf.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2014, 2015, 2016 Laboratoire de Recherche et -// Developpement de l'Epita (LRDE). +// Copyright (C) 2012, 2014, 2015, 2016, 2018 Laboratoire de Recherche +// et Developpement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #if defined __clang__ diff --git a/spot/tl/unabbrev.cc b/spot/tl/unabbrev.cc index b5daa5d7c..e0164a5ce 100644 --- a/spot/tl/unabbrev.cc +++ b/spot/tl/unabbrev.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015 Laboratoire de Recherche et Développement +// Copyright (C) 2015, 2018 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -18,6 +18,7 @@ // along with this program. If not, see . +#include "config.h" #include namespace spot diff --git a/spot/twa/Makefile.am b/spot/twa/Makefile.am index f0dde7983..f99598a8f 100644 --- a/spot/twa/Makefile.am +++ b/spot/twa/Makefile.am @@ -1,6 +1,6 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire -## de Recherche et Développement de l'Epita (LRDE). +## Copyright (C) 2009-2016, 2018 Laboratoire de Recherche et +## Développement de l'Epita (LRDE). ## Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), ## département Systèmes Répartis Coopératifs (SRC), Université Pierre ## et Marie Curie. @@ -20,7 +20,8 @@ ## You should have received a copy of the GNU General Public License ## along with this program. If not, see . -AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) +AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) \ + -I$(top_builddir)/lib -I$(top_srcdir)/lib AM_CXXFLAGS = $(WARNING_CXXFLAGS) twadir = $(pkgincludedir)/twa diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc index 0c36625b5..c6df13210 100644 --- a/spot/twa/acc.cc +++ b/spot/twa/acc.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et -// Développement de l'Epita. +// Copyright (C) 2015-2018 Laboratoire de Recherche et Développement +// de l'Epita. // // This file is part of Spot, a model checking library. // @@ -18,6 +18,7 @@ // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/twa/bdddict.cc b/spot/twa/bdddict.cc index 58d7185c3..1d83e37d5 100644 --- a/spot/twa/bdddict.cc +++ b/spot/twa/bdddict.cc @@ -1,9 +1,9 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2012-2017 Laboratoire de Recherche et +// Copyright (C) 2009, 2012-2018 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. +// Copyright (C) 2003-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. // @@ -20,6 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/twa/bddprint.cc b/spot/twa/bddprint.cc index 79c89d1f2..a0d4b3625 100644 --- a/spot/twa/bddprint.cc +++ b/spot/twa/bddprint.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2012, 2014, 2015 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2012, 2014, 2015, 2018 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université // Pierre et Marie Curie. @@ -20,6 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/twa/formula2bdd.cc b/spot/twa/formula2bdd.cc index f10f53ad4..d93e1ecf6 100644 --- a/spot/twa/formula2bdd.cc +++ b/spot/twa/formula2bdd.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009-2017 Laboratoire de Recherche et Développement +// Copyright (C) 2009-2018 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), @@ -20,6 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/twa/taatgba.cc b/spot/twa/taatgba.cc index 5cdab01d3..27f15edcc 100644 --- a/spot/twa/taatgba.cc +++ b/spot/twa/taatgba.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009-2017 Laboratoire de Recherche et Développement de +// Copyright (C) 2009-2018 Laboratoire de Recherche et Développement de // l'Epita (LRDE) // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/twa/twa.cc b/spot/twa/twa.cc index cdbb033d1..19fd494a0 100644 --- a/spot/twa/twa.cc +++ b/spot/twa/twa.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2014-2017 Laboratoire de Recherche et Developpement de +// Copyright (C) 2011, 2014-2018 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 @@ -20,6 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index f43b1b48d..c3d2671d7 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/twa/twaproduct.cc b/spot/twa/twaproduct.cc index 29328355c..d1ff07b17 100644 --- a/spot/twa/twaproduct.cc +++ b/spot/twa/twaproduct.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2011, 2012, 2014, 2015, 2016, 2017 Laboratoire -// de Recherche et Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2011-2012, 2014-2018 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. @@ -20,6 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/twaalgos/Makefile.am b/spot/twaalgos/Makefile.am index 5d1d7fa3b..500115a51 100644 --- a/spot/twaalgos/Makefile.am +++ b/spot/twaalgos/Makefile.am @@ -1,5 +1,5 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2008-2017 Laboratoire de Recherche et Développement +## Copyright (C) 2008-2018 Laboratoire de Recherche et Développement ## de l'Epita (LRDE). ## Copyright (C) 2003-2005 Laboratoire d'Informatique de Paris 6 ## (LIP6), département Systèmes Répartis Coopératifs (SRC), Université @@ -22,7 +22,8 @@ SUBDIRS = gtec -AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) +AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) \ + -I$(top_builddir)/lib -I$(top_srcdir)/lib AM_CXXFLAGS = $(WARNING_CXXFLAGS) twaalgosdir = $(pkgincludedir)/twaalgos diff --git a/spot/twaalgos/aiger.cc b/spot/twaalgos/aiger.cc index 26344ce68..8cf2f1c82 100644 --- a/spot/twaalgos/aiger.cc +++ b/spot/twaalgos/aiger.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017 Laboratoire de Recherche et Développement +// Copyright (C) 2017-2018 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include diff --git a/spot/twaalgos/alternation.cc b/spot/twaalgos/alternation.cc index eed14cedd..0ebbb1667 100644 --- a/spot/twaalgos/alternation.cc +++ b/spot/twaalgos/alternation.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2016, 2017 Laboratoire de Recherche et Développement +// Copyright (C) 2016-2018 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/twaalgos/are_isomorphic.cc b/spot/twaalgos/are_isomorphic.cc index 773e640d3..77fb95741 100644 --- a/spot/twaalgos/are_isomorphic.cc +++ b/spot/twaalgos/are_isomorphic.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014-2017 Laboratoire de Recherche et Développement +// Copyright (C) 2014-2018 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 @@ -20,6 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/twaalgos/bfssteps.cc b/spot/twaalgos/bfssteps.cc index 082c815fd..131596117 100644 --- a/spot/twaalgos/bfssteps.cc +++ b/spot/twaalgos/bfssteps.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement -// de l'Epita (LRDE) +// Copyright (C) 2014, 2015, 2018 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. @@ -20,6 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/twaalgos/canonicalize.cc b/spot/twaalgos/canonicalize.cc index 9b3cbaa39..1feca0113 100644 --- a/spot/twaalgos/canonicalize.cc +++ b/spot/twaalgos/canonicalize.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014-2017 Laboratoire de Recherche et Développement +// Copyright (C) 2014-2018 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/twaalgos/cleanacc.cc b/spot/twaalgos/cleanacc.cc index 74d4c5692..a672f1cb5 100644 --- a/spot/twaalgos/cleanacc.cc +++ b/spot/twaalgos/cleanacc.cc @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include namespace spot diff --git a/spot/twaalgos/cobuchi.cc b/spot/twaalgos/cobuchi.cc index 73d0f5661..32129a196 100644 --- a/spot/twaalgos/cobuchi.cc +++ b/spot/twaalgos/cobuchi.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement +// Copyright (C) 2017-2018 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include @@ -35,11 +36,11 @@ #include #include -#define DEBUG 0 -#if DEBUG -#define debug std::cerr +#define TRACE 0 +#if TRACE +#define trace std::cerr #else -#define debug while (0) std::cout +#define trace while (0) std::cout #endif namespace spot @@ -461,7 +462,7 @@ namespace spot } } } - debug << "All_states:\n" << *bv_aut_trans_ << '\n'; + trace << "All_states:\n" << *bv_aut_trans_ << '\n'; twa_graph_ptr res = make_twa_graph(aut_->get_dict()); res->copy_ap_of(aut_); @@ -548,14 +549,14 @@ namespace spot bv_trans_mark->at(l) |= bv_aut_trans_->at(s * nc + l); toclean_.push_back(bv_trans_mark); - debug << "src:" << top.second; + trace << "src:" << top.second; if (named_states) - debug << ' ' << (*state_name)[top.second]; - debug << '\n'; + trace << ' ' << (*state_name)[top.second]; + trace << '\n'; for (unsigned l = 0; l < nc; ++l) { - debug << "l: " + trace << "l: " << bdd_format_formula(aut_->get_dict(), num2bdd_[l]) << '\n'; @@ -582,12 +583,12 @@ namespace spot (top.first.first + 1) % (nb_copy_ + 1) : top.first.first; - debug << "dest\n" << *bv_res << "i: " << i << '\n'; + trace << "dest\n" << *bv_res << "i: " << i << '\n'; res->new_edge(top.second, new_state(std::make_pair(i, bv_res)), num2bdd_[l]); } - debug << '\n'; + trace << '\n'; } // Set rejecting states. @@ -617,7 +618,7 @@ namespace spot twa_graph_ptr nsa_to_dca(const_twa_graph_ptr aut, bool named_states) { - debug << "NSA_to_dca\n"; + trace << "NSA_to_dca\n"; std::vector pairs; if (!aut->acc().is_streett_like(pairs) && !aut->acc().is_parity()) throw std::runtime_error("nsa_to_dca() only works with Streett-like or " @@ -632,10 +633,10 @@ namespace spot vect_nca_info nca_info; nsa_to_nca(aut, named_states, &nca_info); -#if DEBUG - debug << "PRINTING INFO\n"; +#if TRACE + trace << "PRINTING INFO\n"; for (unsigned i = 0; i < nca_info.size(); ++i) - debug << '<' << nca_info[i]->clause_num << ',' << nca_info[i]->state_num + trace << '<' << nca_info[i]->clause_num << ',' << nca_info[i]->state_num << ',' << *nca_info[i]->all_dst << ">\n"; #endif @@ -647,7 +648,7 @@ namespace spot twa_graph_ptr dnf_to_dca(const_twa_graph_ptr aut, bool named_states) { - debug << "DNF_to_dca\n"; + trace << "DNF_to_dca\n"; const acc_cond::acc_code& code = aut->get_acceptance(); if (!code.is_dnf()) throw std::runtime_error("dnf_to_dca() only works with DNF (Rabin-like " @@ -662,10 +663,10 @@ namespace spot vect_nca_info nca_info; dnf_to_nca(aut, false, &nca_info); -#if DEBUG - debug << "PRINTING INFO\n"; +#if TRACE + trace << "PRINTING INFO\n"; for (unsigned i = 0; i < nca_info.size(); ++i) - debug << '<' << nca_info[i]->clause_num << ',' << nca_info[i]->state_num + trace << '<' << nca_info[i]->clause_num << ',' << nca_info[i]->state_num << ',' << *nca_info[i]->all_dst << ">\n"; #endif diff --git a/spot/twaalgos/complement.cc b/spot/twaalgos/complement.cc index 2ac33d058..446052b44 100644 --- a/spot/twaalgos/complement.cc +++ b/spot/twaalgos/complement.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013-2015, 2017 Laboratoire de Recherche et +// Copyright (C) 2013-2015, 2017-2018 Laboratoire de Recherche et // Développement de l'Epita. // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/twaalgos/complete.cc b/spot/twaalgos/complete.cc index 71426c795..78ac48b7b 100644 --- a/spot/twaalgos/complete.cc +++ b/spot/twaalgos/complete.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013-2017 Laboratoire de Recherche et Développement +// Copyright (C) 2013-2018 Laboratoire de Recherche et Développement // de l'Epita. // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include namespace spot diff --git a/spot/twaalgos/compsusp.cc b/spot/twaalgos/compsusp.cc index ae9b6a68f..36dbeb008 100644 --- a/spot/twaalgos/compsusp.cc +++ b/spot/twaalgos/compsusp.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et +// Copyright (C) 2012-2015, 2018 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/twaalgos/couvreurnew.cc b/spot/twaalgos/couvreurnew.cc index 3f9fcc780..103431ec9 100644 --- a/spot/twaalgos/couvreurnew.cc +++ b/spot/twaalgos/couvreurnew.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2016-2017 Laboratoire de Recherche et Développement +// Copyright (C) 2016-2018 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include diff --git a/spot/twaalgos/cycles.cc b/spot/twaalgos/cycles.cc index 90deed5b3..51b528584 100644 --- a/spot/twaalgos/cycles.cc +++ b/spot/twaalgos/cycles.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2014-2017 Laboratoire de Recherche et +// Copyright (C) 2012, 2014-2018 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include diff --git a/spot/twaalgos/degen.cc b/spot/twaalgos/degen.cc index 77ff75a2d..d1dbdc633 100644 --- a/spot/twaalgos/degen.cc +++ b/spot/twaalgos/degen.cc @@ -17,7 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . - +#include "config.h" #include #include #include diff --git a/spot/twaalgos/determinize.cc b/spot/twaalgos/determinize.cc index bfb2bc9e3..323a5ad0d 100644 --- a/spot/twaalgos/determinize.cc +++ b/spot/twaalgos/determinize.cc @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/twaalgos/dot.cc b/spot/twaalgos/dot.cc index cb8efa123..39fbc87d5 100644 --- a/spot/twaalgos/dot.cc +++ b/spot/twaalgos/dot.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012, 2014-2017 Laboratoire de Recherche +// Copyright (C) 2011, 2012, 2014-2018 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 @@ -20,6 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/twaalgos/dtbasat.cc b/spot/twaalgos/dtbasat.cc index f945bd2ef..e765fae3d 100644 --- a/spot/twaalgos/dtbasat.cc +++ b/spot/twaalgos/dtbasat.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015, 2016, 2017 Laboratoire de Recherche +// Copyright (C) 2013-2018 Laboratoire de Recherche // et Développement de l'Epita. // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include @@ -33,14 +34,14 @@ // file used to communicate with the sat solver will be left in // the current directory. // -// Additionally, if the following DEBUG macro is set to 1, the CNF +// Additionally, if the following TRACE macro is set to 1, the CNF // file will be output with a comment before each clause, and an // additional output file (dtba-sat.dbg) will be created with a list // of all positive variables in the result and their meaning. -#define DEBUG 0 +#define TRACE 0 -#if DEBUG +#if TRACE #define dout out << "c " #define cnf_comment(...) solver.comment(__VA_ARGS__) #define trace std::cerr @@ -105,7 +106,7 @@ namespace spot int transid(unsigned src, bdd& cond, unsigned dst) { -#if DEBUG +#if TRACE try { return helper.get_t(src, alpha_map.at(cond), dst); @@ -130,7 +131,7 @@ namespace spot int transacc(unsigned src, bdd& cond, unsigned dst) { -#if DEBUG +#if TRACE try { return helper.get_ta(src, alpha_map.at(cond), dst); @@ -150,7 +151,7 @@ namespace spot pathid_ref(unsigned src_cand, unsigned src_ref, unsigned dst_cand, unsigned dst_ref) { -#if DEBUG +#if TRACE try { return helper.get_prc( @@ -169,7 +170,7 @@ namespace spot #endif } -#if DEBUG +#if TRACE int pathid_ref(unsigned path, unsigned src_cand, unsigned dst_cand) { @@ -187,7 +188,7 @@ namespace spot pathid_cand(unsigned src_cand, unsigned src_ref, unsigned dst_cand, unsigned dst_ref) { -#if DEBUG +#if TRACE try { return helper.get_prc( @@ -330,7 +331,7 @@ namespace spot // Empty automaton is impossible. assert(d.cand_size > 0); -#if DEBUG +#if TRACE debug_dict = ref->get_dict(); solver.comment("d.ref_size", d.ref_size, '\n'); solver.comment("d.cand_size", d.cand_size, '\n'); @@ -353,7 +354,7 @@ namespace spot for (unsigned q1 = 0; q1 < d.cand_size; ++q1) for (unsigned l = 0; l < alpha_size; ++l) { -#if DEBUG +#if TRACE solver.comment(""); for (unsigned q2 = 0; q2 < d.cand_size; q2++) { @@ -457,7 +458,7 @@ namespace spot { bdd s = bdd_satoneset(all, ap, bddfalse); all -= s; -#if DEBUG +#if TRACE std::string f_t = d.fmt_t(q2, s, q1); cnf_comment(f_p, "R ∧", f_t, "δ → ¬", f_t, "F\n"); @@ -544,7 +545,7 @@ namespace spot { bdd s = bdd_satoneset(all, ap, bddfalse); all -= s; -#if DEBUG +#if TRACE std::string f_t = d.fmt_t(q2, s, q1); cnf_comment(f_p, "C ∧", f_t, "δ →", f_t, "F\n"); @@ -566,7 +567,7 @@ namespace spot { bdd s = bdd_satoneset(all, ap, bddfalse); all -= s; -#if DEBUG +#if TRACE std::string f_t = d.fmt_t(q2, s, q3); cnf_comment(f_p, "C ∧", f_t, "δ ∧ ¬", f_t, "F →", d.fmt_p(q1, q1p, q3, dp), @@ -602,7 +603,7 @@ namespace spot a->prop_universal(true); a->new_states(satdict.cand_size); -#if DEBUG +#if TRACE std::fstream out("dtba-sat.dbg", std::ios_base::trunc | std::ios_base::out); out.exceptions(std::ifstream::failbit | std::ifstream::badbit); @@ -638,7 +639,7 @@ namespace spot } } } -#if DEBUG +#if TRACE dout << "--- transition variables ---\n"; for (unsigned i = 0; i < cand_size; ++i) for (unsigned j = 0; j < alpha_size; ++j) diff --git a/spot/twaalgos/dtwasat.cc b/spot/twaalgos/dtwasat.cc index a66197ecc..b1fd22b4b 100644 --- a/spot/twaalgos/dtwasat.cc +++ b/spot/twaalgos/dtwasat.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015, 2016, 2017 Laboratoire de Recherche +// Copyright (C) 2013-2018 Laboratoire de Recherche // et Développement de l'Epita. // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include @@ -41,14 +42,14 @@ // file used to communicate with the sat solver will be left in // the current directory. // -// Additionally, if the following DEBUG macro is set to 1, the CNF +// Additionally, if the following TRACE macro is set to 1, the CNF // file will be output with a comment before each clause, and an // additional output file (dtwa-sat.dbg) will be created with a list // of all positive variables in the result and their meaning. -#define DEBUG 0 +#define TRACE 0 -#if DEBUG +#if TRACE #define dout out << "c " #define cnf_comment(...) solver.comment(__VA_ARGS__) #define trace std::cerr @@ -247,7 +248,7 @@ namespace spot int transid(unsigned src, bdd& cond, unsigned dst) { -#if DEBUG +#if TRACE try { return helper.get_t(src, alpha_map.at(cond), dst); @@ -272,7 +273,7 @@ namespace spot int transacc(unsigned src, bdd& cond, unsigned dst, unsigned nacc) { -#if DEBUG +#if TRACE try { return helper.get_ta(src, alpha_map.at(cond), dst, nacc); @@ -293,7 +294,7 @@ namespace spot unsigned dst_ref, acc_cond::mark_t acc_cand = 0U, acc_cond::mark_t acc_ref = 0U) { -#if DEBUG +#if TRACE try { return helper.get_p( @@ -315,7 +316,7 @@ namespace spot #endif } -#if DEBUG +#if TRACE int pathid(unsigned path, unsigned src_cand, unsigned dst_cand) { @@ -539,7 +540,7 @@ namespace spot bool state_based, bool colored) { -#if DEBUG +#if TRACE debug_dict = ref->get_dict(); #endif // Compute the AP used. @@ -572,7 +573,7 @@ namespace spot // Empty automaton is impossible. assert(d.cand_size > 0); -#if DEBUG +#if TRACE debug_ref_acc = &ref->acc(); debug_cand_acc = &d.cacc; solver.comment("d.ref_size:", d.ref_size, '\n'); @@ -597,7 +598,7 @@ namespace spot for (unsigned q1 = 0; q1 < d.cand_size; ++q1) for (unsigned l = 0; l < alpha_size; ++l) { -#if DEBUG +#if TRACE solver.comment(""); for (unsigned q2 = 0; q2 < d.cand_size; ++q2) { @@ -768,7 +769,7 @@ namespace spot for (auto& v: missing) { -#if DEBUG +#if TRACE solver.comment((rejloop ? "(11) " : "(12) "), f_p, " ∧ ", d.fmt_t(q2, l, q3), @@ -787,7 +788,7 @@ namespace spot orsep = " ∨ "; } solver.comment_rec(")\n"); -#endif // DEBUG +#endif // TRACE solver.add({-pid, -ti}); for (int s: v) if (s < 0) @@ -825,7 +826,7 @@ namespace spot q1, q1p, q3, dp, f2, f2p); if (pid == p2id) continue; -#if DEBUG +#if TRACE solver.comment("(13) ", f_p, " ∧ ", d.fmt_t(q1, l, q3), "δ "); @@ -883,7 +884,7 @@ namespace spot a->set_acceptance(satdict.cand_nacc, satdict.cand_acc); a->new_states(satdict.cand_size); -#if DEBUG +#if TRACE std::fstream out("dtwa-sat.dbg", std::ios_base::trunc | std::ios_base::out); out.exceptions(std::ifstream::failbit | std::ifstream::badbit); @@ -922,7 +923,7 @@ namespace spot } } -#if DEBUG +#if TRACE dout << "--- transition variables ---\n"; for (unsigned i = 0; i < satdict.cand_size; ++i) for (unsigned j = 0; j < alpha_size; ++j) diff --git a/spot/twaalgos/dualize.cc b/spot/twaalgos/dualize.cc index 73d762728..1f8a436cf 100644 --- a/spot/twaalgos/dualize.cc +++ b/spot/twaalgos/dualize.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017 Laboratoire de Recherche et Développement +// Copyright (C) 2017-2018 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include @@ -180,8 +181,8 @@ namespace spot } // Handles the dualization of a universal initial transition. - // In theory the transition would be split into several existential - // initial transitions, but since spot does not allow multiple initial + // In theory the transition would be split into several existential + // initial transitions, but since spot does not allow multiple initial // states, we rather use a trick: We add a new initial state, and then // copy all exiting transitions from each of the state of the universal // initial transition. @@ -251,9 +252,9 @@ namespace spot } // Given the bdd representation b of a transition, adds destination states - // to s, and returns the marks on the transition. s being empty means the + // to s, and returns the marks on the transition. s being empty means the // transition goes toward a "forever true" state. s with size one - // represents an existential transition, while size over one represents + // represents an existential transition, while size over one represents // a universal transition. acc_cond::mark_t bdd_to_state(bdd b, std::vector& s) { diff --git a/spot/twaalgos/emptiness.cc b/spot/twaalgos/emptiness.cc index 606c6d3ab..f9b91f1a7 100644 --- a/spot/twaalgos/emptiness.cc +++ b/spot/twaalgos/emptiness.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2011-2017 Laboratoire de Recherche et +// Copyright (C) 2009, 2011-2018 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 @@ -20,6 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/twaalgos/gtec/Makefile.am b/spot/twaalgos/gtec/Makefile.am index 14f6dc92f..98198e6ef 100644 --- a/spot/twaalgos/gtec/Makefile.am +++ b/spot/twaalgos/gtec/Makefile.am @@ -1,6 +1,6 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2011, 2013, 2014, 2016 Laboratoire de Recherche et -## Developpement de l'Epita (LRDE). +## Copyright (C) 2011, 2013, 2014, 2016, 2018 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. @@ -20,7 +20,8 @@ ## You should have received a copy of the GNU General Public License ## along with this program. If not, see . -AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) +AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) \ + -I$(top_builddir)/lib -I$(top_srcdir)/lib AM_CXXFLAGS = $(WARNING_CXXFLAGS) gtecdir = $(pkgincludedir)/twaalgos/gtec diff --git a/spot/twaalgos/gtec/ce.cc b/spot/twaalgos/gtec/ce.cc index 66aae9b9d..c44bb3ebe 100644 --- a/spot/twaalgos/gtec/ce.cc +++ b/spot/twaalgos/gtec/ce.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2013, 2014, 2015, 2016 Laboratoire de +// Copyright (C) 2010-2011, 2013-2016, 2018 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 @@ -20,6 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/twaalgos/gtec/gtec.cc b/spot/twaalgos/gtec/gtec.cc index 8aece6ad5..243ad8c91 100644 --- a/spot/twaalgos/gtec/gtec.cc +++ b/spot/twaalgos/gtec/gtec.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2011, 2014, 2015, 2016 Laboratoire de Recherche +// Copyright (C) 2008, 2011, 2014-2016, 2018 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), @@ -22,6 +22,7 @@ // #define TRACE +#include "config.h" #include #ifdef TRACE #define trace std::cerr diff --git a/spot/twaalgos/gtec/sccstack.cc b/spot/twaalgos/gtec/sccstack.cc index d953fff45..34ec7493b 100644 --- a/spot/twaalgos/gtec/sccstack.cc +++ b/spot/twaalgos/gtec/sccstack.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014 Laboratoire de Recherche et Developpement de +// Copyright (C) 2014, 2018 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 @@ -20,6 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include namespace spot diff --git a/spot/twaalgos/gtec/status.cc b/spot/twaalgos/gtec/status.cc index 0c5862408..d9b6d8fc8 100644 --- a/spot/twaalgos/gtec/status.cc +++ b/spot/twaalgos/gtec/status.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014, 2016 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2014, 2016, 2018 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. @@ -20,6 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include diff --git a/spot/twaalgos/gv04.cc b/spot/twaalgos/gv04.cc index 45e496954..a6e7e6b64 100644 --- a/spot/twaalgos/gv04.cc +++ b/spot/twaalgos/gv04.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2010, 2011, 2013-2017 Laboratoire de +// Copyright (C) 2008, 2010, 2011, 2013-2018 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é @@ -22,6 +22,7 @@ //#define TRACE +#include "config.h" #include #ifdef TRACE #define trace std::cerr diff --git a/spot/twaalgos/hoa.cc b/spot/twaalgos/hoa.cc index 51d45e6a7..e70bf4d18 100644 --- a/spot/twaalgos/hoa.cc +++ b/spot/twaalgos/hoa.cc @@ -1,9 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012, 2014, 2015, 2016, 2017 Laboratoire de Recherche et +// Copyright (C) 2014-2018 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. // @@ -20,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/twaalgos/iscolored.cc b/spot/twaalgos/iscolored.cc index 871ab6bc4..d38a36ee8 100644 --- a/spot/twaalgos/iscolored.cc +++ b/spot/twaalgos/iscolored.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017 Laboratoire de Recherche et Développement de l'Epita -// (LRDE). +// Copyright (C) 2017-2018 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include namespace spot diff --git a/spot/twaalgos/isdet.cc b/spot/twaalgos/isdet.cc index 50cdcde2b..51a43661c 100644 --- a/spot/twaalgos/isdet.cc +++ b/spot/twaalgos/isdet.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2017 Laboratoire de Recherche et Développement +// Copyright (C) 2012-2018 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include diff --git a/spot/twaalgos/isunamb.cc b/spot/twaalgos/isunamb.cc index e0f8af6a0..3adb787bd 100644 --- a/spot/twaalgos/isunamb.cc +++ b/spot/twaalgos/isunamb.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2015-2017 Laboratoire de Recherche et +// Copyright (C) 2013, 2015-2018 Laboratoire de Recherche et // Developpement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/twaalgos/isweakscc.cc b/spot/twaalgos/isweakscc.cc index 5bd292e5e..04a9f07db 100644 --- a/spot/twaalgos/isweakscc.cc +++ b/spot/twaalgos/isweakscc.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2017 Laboratoire de Recherche et Développement +// Copyright (C) 2012-2018 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/twaalgos/langmap.cc b/spot/twaalgos/langmap.cc index a49386717..3ba6b3b23 100644 --- a/spot/twaalgos/langmap.cc +++ b/spot/twaalgos/langmap.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2016, 2017 Laboratoire de Recherche et Développement +// Copyright (C) 2016-2018 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/twaalgos/lbtt.cc b/spot/twaalgos/lbtt.cc index c96c599c7..c56f4a0f9 100644 --- a/spot/twaalgos/lbtt.cc +++ b/spot/twaalgos/lbtt.cc @@ -1,9 +1,9 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012, 2013, 2014, 2015, 2016 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. +// Copyright (C) 2011-2016, 2018 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). +// Copyright (C) 2003-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. // @@ -20,6 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/twaalgos/ltl2taa.cc b/spot/twaalgos/ltl2taa.cc index 2a06fcd02..8b02d7c9e 100644 --- a/spot/twaalgos/ltl2taa.cc +++ b/spot/twaalgos/ltl2taa.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2012, 2013, 2014, 2015, 2016 Laboratoire -// de Recherche et Développement de l'Epita (LRDE). +// Copyright (C) 2009-2010, 2012-2016, 2018 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/twaalgos/ltl2tgba_fm.cc b/spot/twaalgos/ltl2tgba_fm.cc index 62d039748..648c03b08 100644 --- a/spot/twaalgos/ltl2tgba_fm.cc +++ b/spot/twaalgos/ltl2tgba_fm.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008-2017 Laboratoire de Recherche et Développement +// Copyright (C) 2008-2018 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2003-2006 Laboratoire d'Informatique de Paris 6 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université @@ -20,6 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/twaalgos/magic.cc b/spot/twaalgos/magic.cc index 24820aac4..ac3a5bd37 100644 --- a/spot/twaalgos/magic.cc +++ b/spot/twaalgos/magic.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013-2017 Laboratoire de recherche et +// Copyright (C) 2011, 2013-2018 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 @@ -22,6 +22,7 @@ //#define TRACE +#include "config.h" #include #ifdef TRACE #define trace std::cerr diff --git a/spot/twaalgos/mask.cc b/spot/twaalgos/mask.cc index 70fbb22e5..5a6e6a6aa 100644 --- a/spot/twaalgos/mask.cc +++ b/spot/twaalgos/mask.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et Développement +// Copyright (C) 2015-2018 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include namespace spot diff --git a/spot/twaalgos/minimize.cc b/spot/twaalgos/minimize.cc index fcab083f7..db5ad9c63 100644 --- a/spot/twaalgos/minimize.cc +++ b/spot/twaalgos/minimize.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010-2017 Laboratoire de Recherche et Développement +// Copyright (C) 2010-2018 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -19,13 +19,13 @@ //#define TRACE - #ifdef TRACE # define trace std::cerr #else # define trace while (0) std::cerr #endif +#include "config.h" #include #include #include diff --git a/spot/twaalgos/neverclaim.cc b/spot/twaalgos/neverclaim.cc index 296f02344..c24fc8948 100644 --- a/spot/twaalgos/neverclaim.cc +++ b/spot/twaalgos/neverclaim.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2011, 2012, 2014, 2015, 2016 Laboratoire de -// Recherche et Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2011, 2012, 2014-2016, 2018 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. @@ -20,6 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/twaalgos/parity.cc b/spot/twaalgos/parity.cc index 5908baf10..81b67024b 100644 --- a/spot/twaalgos/parity.cc +++ b/spot/twaalgos/parity.cc @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc index 4203e5b57..b443481df 100644 --- a/spot/twaalgos/postproc.cc +++ b/spot/twaalgos/postproc.cc @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/twaalgos/powerset.cc b/spot/twaalgos/powerset.cc index 516945841..8ed37fbc1 100644 --- a/spot/twaalgos/powerset.cc +++ b/spot/twaalgos/powerset.cc @@ -20,6 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/twaalgos/product.cc b/spot/twaalgos/product.cc index ab0aa13df..df32d2c8b 100644 --- a/spot/twaalgos/product.cc +++ b/spot/twaalgos/product.cc @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/twaalgos/rabin2parity.cc b/spot/twaalgos/rabin2parity.cc index c41638c63..178981cad 100644 --- a/spot/twaalgos/rabin2parity.cc +++ b/spot/twaalgos/rabin2parity.cc @@ -1,5 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017-2018 Laboratoire de Recherche et Développement de l'Epita. +// Copyright (C) 2017-2018 Laboratoire de Recherche et Développement +// de l'Epita. // // This file is part of Spot, a model checking library. // @@ -16,10 +17,9 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include - #include - #include namespace spot diff --git a/spot/twaalgos/randomgraph.cc b/spot/twaalgos/randomgraph.cc index 1452ffd7c..59e1c6bdf 100644 --- a/spot/twaalgos/randomgraph.cc +++ b/spot/twaalgos/randomgraph.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008-2010, 2012-2017 Laboratoire de Recherche et +// Copyright (C) 2008-2010, 2012-2018 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), @@ -20,6 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/twaalgos/randomize.cc b/spot/twaalgos/randomize.cc index a38435ba9..c3b09a004 100644 --- a/spot/twaalgos/randomize.cc +++ b/spot/twaalgos/randomize.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014-2017 Laboratoire de Recherche et Développement +// Copyright (C) 2014-2018 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/twaalgos/reachiter.cc b/spot/twaalgos/reachiter.cc index 33ece2d65..a85c20005 100644 --- a/spot/twaalgos/reachiter.cc +++ b/spot/twaalgos/reachiter.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2011, 2013, 2014, 2015, 2016 Laboratoire de Recherche +// Copyright (C) 2009, 2011, 2013-2016, 2018 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 @@ -20,6 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include diff --git a/spot/twaalgos/relabel.cc b/spot/twaalgos/relabel.cc index 72884400d..3d09136bc 100644 --- a/spot/twaalgos/relabel.cc +++ b/spot/twaalgos/relabel.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et Développement +// Copyright (C) 2015-2018 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include diff --git a/spot/twaalgos/remfin.cc b/spot/twaalgos/remfin.cc index 682bddc40..07b496dfe 100644 --- a/spot/twaalgos/remfin.cc +++ b/spot/twaalgos/remfin.cc @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/twaalgos/remprop.cc b/spot/twaalgos/remprop.cc index 32e32bfdb..bdd5a842c 100644 --- a/spot/twaalgos/remprop.cc +++ b/spot/twaalgos/remprop.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015-2017 Laboratoire de Recherche et Développement +// Copyright (C) 2015-2018 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include @@ -124,7 +125,7 @@ namespace spot twa_graph_ptr remove_ap::strip(const_twa_graph_ptr aut) const { - bdd restrict = bddtrue; + bdd restrict_ = bddtrue; bdd exist = bddtrue; auto d = aut->get_dict(); @@ -147,7 +148,7 @@ namespace spot int v = d->has_registered_proposition(ap, aut); if (v >= 0) { - restrict &= bdd_ithvar(v); + restrict_ &= bdd_ithvar(v); res->unregister_ap(v); } } @@ -156,7 +157,7 @@ namespace spot int v = d->has_registered_proposition(ap, aut); if (v >= 0) { - restrict &= bdd_nithvar(v); + restrict_ &= bdd_nithvar(v); res->unregister_ap(v); } } @@ -165,7 +166,7 @@ namespace spot acc_cond::mark_t&, unsigned) { cond = bdd_restrict(bdd_exist(cond, exist), - restrict); + restrict_); }); return res; } diff --git a/spot/twaalgos/sbacc.cc b/spot/twaalgos/sbacc.cc index 3cff71f1a..fe55d5fb8 100644 --- a/spot/twaalgos/sbacc.cc +++ b/spot/twaalgos/sbacc.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015-2017 Laboratoire de Recherche et Développement +// Copyright (C) 2015-2018 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/twaalgos/sccfilter.cc b/spot/twaalgos/sccfilter.cc index 34bbd92ca..d73e67b26 100644 --- a/spot/twaalgos/sccfilter.cc +++ b/spot/twaalgos/sccfilter.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009-2017 Laboratoire de Recherche et Développement +// Copyright (C) 2009-2018 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/twaalgos/sccinfo.cc b/spot/twaalgos/sccinfo.cc index 567b9f1bd..9f77bb313 100644 --- a/spot/twaalgos/sccinfo.cc +++ b/spot/twaalgos/sccinfo.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014-2017 Laboratoire de Recherche et Développement +// Copyright (C) 2014-2018 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/twaalgos/se05.cc b/spot/twaalgos/se05.cc index ec24263b7..89032f289 100644 --- a/spot/twaalgos/se05.cc +++ b/spot/twaalgos/se05.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013-2017 Laboratoire de Recherche et +// Copyright (C) 2011, 2013-2018 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 @@ -22,6 +22,7 @@ //#define TRACE +#include "config.h" #include #ifdef TRACE #define trace std::cerr diff --git a/spot/twaalgos/sepsets.cc b/spot/twaalgos/sepsets.cc index 2e9f95f42..2b246a06d 100644 --- a/spot/twaalgos/sepsets.cc +++ b/spot/twaalgos/sepsets.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et +// Copyright (C) 2015-2018 Laboratoire de Recherche et // Développement de l'Epita. // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include diff --git a/spot/twaalgos/simulation.cc b/spot/twaalgos/simulation.cc index e7b8979ed..724510d84 100644 --- a/spot/twaalgos/simulation.cc +++ b/spot/twaalgos/simulation.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2017 Laboratoire de Recherche et Développement +// Copyright (C) 2012-2018 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/twaalgos/split.cc b/spot/twaalgos/split.cc index 70d63f405..f2d1bae92 100644 --- a/spot/twaalgos/split.cc +++ b/spot/twaalgos/split.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017 Laboratoire de Recherche et Développement +// Copyright (C) 2017-2018 Laboratoire de Recherche et Développement // de l'Epita. // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include namespace spot diff --git a/spot/twaalgos/stats.cc b/spot/twaalgos/stats.cc index cfcdd51c5..2d0a7a849 100644 --- a/spot/twaalgos/stats.cc +++ b/spot/twaalgos/stats.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2011, 2012, 2013, 2014, 2015, 2016, 2017 -// Laboratoire de Recherche et Développement de l'Epita (LRDE). +// Copyright (C) 2008, 2011-2018 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. @@ -20,6 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/twaalgos/strength.cc b/spot/twaalgos/strength.cc index 24578f268..36821c91e 100644 --- a/spot/twaalgos/strength.cc +++ b/spot/twaalgos/strength.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2013, 2014, 2015, 2016, 2017 Laboratoire -// de Recherche et Développement de l'Epita (LRDE) +// Copyright (C) 2010-2011, 2013-2018 Laboratoire de Recherche et +// Développement de l'Epita (LRDE) // // This file is part of Spot, a model checking library. // @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/twaalgos/stripacc.cc b/spot/twaalgos/stripacc.cc index a4018035a..41634b409 100644 --- a/spot/twaalgos/stripacc.cc +++ b/spot/twaalgos/stripacc.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2014, 2015, 2017 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2012, 2014-2015, 2017-2018 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include diff --git a/spot/twaalgos/stutter.cc b/spot/twaalgos/stutter.cc index 8fd9cbd48..b2f2cbedb 100644 --- a/spot/twaalgos/stutter.cc +++ b/spot/twaalgos/stutter.cc @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/twaalgos/sum.cc b/spot/twaalgos/sum.cc index f175d7de5..85e579471 100644 --- a/spot/twaalgos/sum.cc +++ b/spot/twaalgos/sum.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017 Laboratoire de Recherche et Développement +// Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include @@ -76,7 +77,7 @@ namespace spot } } - // Helper function that perform the sum of the automaton in left and the + // Helper function that perform the sum of the automaton in left and the // automaton in right, using is_sum true for sum_or and is_sum false // as sum_and static diff --git a/spot/twaalgos/tau03.cc b/spot/twaalgos/tau03.cc index 8e07a2fac..ec7396949 100644 --- a/spot/twaalgos/tau03.cc +++ b/spot/twaalgos/tau03.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013-2017 Laboratoire de Recherche et +// Copyright (C) 2011, 2013-2018 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 @@ -25,6 +25,7 @@ //#define TRACE +#include "config.h" #include #ifdef TRACE #define trace std::cerr diff --git a/spot/twaalgos/tau03opt.cc b/spot/twaalgos/tau03opt.cc index 9b9907605..51f988854 100644 --- a/spot/twaalgos/tau03opt.cc +++ b/spot/twaalgos/tau03opt.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013-2017 Laboratoire de Recherche et +// Copyright (C) 2011, 2013-2018 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 @@ -34,6 +34,7 @@ //#define TRACE +#include "config.h" #include #ifdef TRACE #define trace std::cerr diff --git a/spot/twaalgos/totgba.cc b/spot/twaalgos/totgba.cc index bac6fad04..e9440f22e 100644 --- a/spot/twaalgos/totgba.cc +++ b/spot/twaalgos/totgba.cc @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include @@ -25,11 +26,11 @@ #include #include -#define DEBUG 0 -#if DEBUG -#define debug std::cerr +#define TRACE 0 +#if TRACE +#define trace std::cerr #else -#define debug while (0) std::cerr +#define trace while (0) std::cerr #endif namespace spot @@ -121,11 +122,11 @@ namespace spot SPOT_UNREACHABLE(); } } -#if DEBUG - debug << "\nPrinting all clauses\n"; +#if TRACE + trace << "\nPrinting all clauses\n"; for (unsigned i = 0; i < all_clauses_.size(); ++i) { - debug << i << " Fin:" << all_clauses_[i].first << " Inf:" + trace << i << " Fin:" << all_clauses_[i].first << " Inf:" << all_clauses_[i].second << '\n'; } #endif @@ -238,16 +239,16 @@ namespace spot res[scc].push_back(clause); } } -#if DEBUG - debug << "accepting clauses\n"; +#if TRACE + trace << "accepting clauses\n"; for (unsigned i = 0; i < res.size(); ++i) { - debug << "scc(" << i << ") --> "; + trace << "scc(" << i << ") --> "; for (auto elt : res[i]) - debug << elt << ','; - debug << '\n' + trace << elt << ','; + trace << '\n' } - debug << '\n'; + trace << '\n'; #endif } @@ -257,7 +258,7 @@ namespace spot void add_state(unsigned st) { - debug << "add_state(" << st << ")\n"; + trace << "add_state(" << st << ")\n"; if (st_repr_[st].empty()) { unsigned st_scc = si_.scc_of(st); @@ -270,7 +271,7 @@ namespace spot else st_repr_[st].emplace_back(-1U, res_->new_state()); - debug << "added\n"; + trace << "added\n"; } } @@ -317,7 +318,7 @@ namespace spot init_st_in_(in->get_init_state_number()), init_reachable_(is_init_reachable()) { - debug << "State based ? " << state_based_ << '\n'; + trace << "State based ? " << state_based_ << '\n'; std::tie(all_inf_, all_fin_) = code.used_inf_fin_sets(); split_dnf_clauses(code); find_set_to_add(); @@ -346,7 +347,7 @@ namespace spot add_state(st); for (const auto& e : in_->out(st)) { - debug << "working_on_edge(" << st << ',' << e.dst << ")\n"; + trace << "working_on_edge(" << st << ',' << e.dst << ")\n"; unsigned dst_scc = si_.scc_of(e.dst); if (!si_.is_useful_scc(dst_scc)) @@ -366,7 +367,7 @@ namespace spot for (const auto& p_src : st_repr_[st]) for (const auto& p_dst : st_repr_[e.dst]) { - debug << "repr(" << p_src.second << ',' + trace << "repr(" << p_src.second << ',' << p_dst.second << ")\n"; if (same_scc && p_src.first == p_dst.first) diff --git a/spot/twaalgos/toweak.cc b/spot/twaalgos/toweak.cc index efebee736..f734ecfc2 100644 --- a/spot/twaalgos/toweak.cc +++ b/spot/twaalgos/toweak.cc @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/twaalgos/translate.cc b/spot/twaalgos/translate.cc index c7de29be9..d8fb14f3e 100644 --- a/spot/twaalgos/translate.cc +++ b/spot/twaalgos/translate.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013-2017 Laboratoire de Recherche et Développement +// Copyright (C) 2013-2018 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/spot/twaalgos/word.cc b/spot/twaalgos/word.cc index a5bad2812..cd117d898 100644 --- a/spot/twaalgos/word.cc +++ b/spot/twaalgos/word.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013-2017 Laboratoire de Recherche et Développement +// Copyright (C) 2013-2018 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/tests/Makefile.am b/tests/Makefile.am index 5c4f4b1ba..4e25ec2a1 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -22,7 +22,8 @@ ## along with this program. If not, see . AUTOMAKE_OPTIONS = subdir-objects -AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) +AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) \ + -I$(top_builddir)/lib -I$(top_srcdir)/lib AM_CXXFLAGS = $(WARNING_CXXFLAGS) LDADD = $(top_builddir)/spot/libspot.la $(top_builddir)/buddy/src/libbddx.la diff --git a/tests/core/acc.cc b/tests/core/acc.cc index 6c534c751..40059d8c2 100644 --- a/tests/core/acc.cc +++ b/tests/core/acc.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*-x -// Copyright (C) 2014, 2015, 2017 Laboratoire de Recherche et +// Copyright (C) 2014, 2015, 2017, 2018 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/tests/core/bitvect.cc b/tests/core/bitvect.cc index 32a2f6d52..d8b0750d5 100644 --- a/tests/core/bitvect.cc +++ b/tests/core/bitvect.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et +// Copyright (C) 2013-2016, 2018 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include diff --git a/tests/core/checkpsl.cc b/tests/core/checkpsl.cc index 09a473f88..b9cb6e746 100644 --- a/tests/core/checkpsl.cc +++ b/tests/core/checkpsl.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2014-2016, 2018 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/tests/core/checkta.cc b/tests/core/checkta.cc index f8482c09e..5750d5516 100644 --- a/tests/core/checkta.cc +++ b/tests/core/checkta.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et +// Copyright (C) 2014-2016, 2018 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/tests/core/consterm.cc b/tests/core/consterm.cc index 75904b31b..dedb2479a 100644 --- a/tests/core/consterm.cc +++ b/tests/core/consterm.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2012, 2015, 2016 Laboratoire de Recherche +// Copyright (C) 2010-2012, 2015-2016, 2018 Laboratoire de Recherche // et Dévelopement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/tests/core/emptchk.cc b/tests/core/emptchk.cc index 12c573652..171036d55 100644 --- a/tests/core/emptchk.cc +++ b/tests/core/emptchk.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et +// Copyright (C) 2014-2016, 2018 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/tests/core/equalsf.cc b/tests/core/equalsf.cc index 3761d25ab..692ddc167 100644 --- a/tests/core/equalsf.cc +++ b/tests/core/equalsf.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014, 2015, 2016 Laboratoire de +// Copyright (C) 2008-2012, 2014-2016, 2018 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), @@ -20,6 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/tests/core/graph.cc b/tests/core/graph.cc index 3de1d51f0..caaf073c0 100644 --- a/tests/core/graph.cc +++ b/tests/core/graph.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014, 2015, 2016, 2017 Laboratoire de Recherche et +// Copyright (C) 2014-2018 Laboratoire de Recherche et // Développement de l'Epita. // // This file is part of Spot, a model checking library. @@ -17,7 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . - +#include "config.h" #include #include diff --git a/tests/core/ikwiad.cc b/tests/core/ikwiad.cc index b60aa72f9..c85d44f80 100644 --- a/tests/core/ikwiad.cc +++ b/tests/core/ikwiad.cc @@ -20,6 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/tests/core/intvcmp2.cc b/tests/core/intvcmp2.cc index ad4d07dc5..8024673af 100644 --- a/tests/core/intvcmp2.cc +++ b/tests/core/intvcmp2.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2014, 2015 Laboratoire de Recherche et Developpement -// de l'Epita (LRDE). +// Copyright (C) 2011, 2014, 2015, 2018 Laboratoire de Recherche et +// Developpement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/tests/core/intvcomp.cc b/tests/core/intvcomp.cc index c5b709678..b4d61de76 100644 --- a/tests/core/intvcomp.cc +++ b/tests/core/intvcomp.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2014, 2015 Laboratoire de Recherche et +// Copyright (C) 2011, 2014, 2015, 2018 Laboratoire de Recherche et // Developpement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/tests/core/kind.cc b/tests/core/kind.cc index 37e9499a0..35c69c48e 100644 --- a/tests/core/kind.cc +++ b/tests/core/kind.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2012, 2015, 2016 Laboratoire de Recherche et -// Developement de l'Epita (LRDE). +// Copyright (C) 2010, 2012, 2015, 2016, 2018 Laboratoire de Recherche +// et Developement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/tests/core/kripkecat.cc b/tests/core/kripkecat.cc index b780c2f8e..d3ea0fd86 100644 --- a/tests/core/kripkecat.cc +++ b/tests/core/kripkecat.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2014, 2015 Laboratoire de Recherche et +// Copyright (C) 2011, 2014, 2015, 2018 Laboratoire de Recherche et // Developpement de l'Epita (LRDE) // // This file is part of Spot, a model checking library. @@ -17,7 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . - +#include "config.h" #include #include diff --git a/tests/core/length.cc b/tests/core/length.cc index 2df3ed530..7d99186e4 100644 --- a/tests/core/length.cc +++ b/tests/core/length.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2015, 2016 Laboratoire de Recherche et +// Copyright (C) 2012, 2015, 2016, 2018 Laboratoire de Recherche et // Developement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/tests/core/ltlrel.cc b/tests/core/ltlrel.cc index 3beb53d38..82e001464 100644 --- a/tests/core/ltlrel.cc +++ b/tests/core/ltlrel.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et Developement -// de l'Epita (LRDE). +// Copyright (C) 2013-2016, 2018 Laboratoire de Recherche et +// Developement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/tests/core/ngraph.cc b/tests/core/ngraph.cc index 6de093314..0c0db715e 100644 --- a/tests/core/ngraph.cc +++ b/tests/core/ngraph.cc @@ -17,7 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . - +#include "config.h" #include #include #include diff --git a/tests/core/parity.cc b/tests/core/parity.cc index 61983f8e4..64b5f18a2 100644 --- a/tests/core/parity.cc +++ b/tests/core/parity.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2016 Laboratoire de Recherche et Développement +// Copyright (C) 2016, 2018 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/tests/core/randtgba.cc b/tests/core/randtgba.cc index 3bc655f78..15039c1ba 100644 --- a/tests/core/randtgba.cc +++ b/tests/core/randtgba.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008-2012, 2014-2017 Laboratoire de Recherche et +// Copyright (C) 2008-2012, 2014-2018 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), @@ -20,6 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/tests/core/readltl.cc b/tests/core/readltl.cc index 747c68fe6..6e445bd1a 100644 --- a/tests/core/readltl.cc +++ b/tests/core/readltl.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2009, 2012, 2015, 2016 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2008, 2009, 2012, 2015, 2016, 2018 Laboratoire de +// Recherche et Développement de l'Epita (LRDE). // Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université // Pierre et Marie Curie. @@ -20,6 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/tests/core/reduc.cc b/tests/core/reduc.cc index 5e6be26be..d6b5a9067 100644 --- a/tests/core/reduc.cc +++ b/tests/core/reduc.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*_ -// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014, 2015, 2016 Laboratoire +// Copyright (C) 2008-2012, 2014-2016, 2018 Laboratoire // de Recherche et Développement de l'Epita (LRDE). // Copyright (C) 2004, 2006, 2007 Laboratoire d'Informatique de Paris // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -20,6 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/tests/core/safra.cc b/tests/core/safra.cc index 53f91642d..ca4591559 100644 --- a/tests/core/safra.cc +++ b/tests/core/safra.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2015, 2016, 2018 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include diff --git a/tests/core/sccif.cc b/tests/core/sccif.cc index 4947e9da9..96f289936 100644 --- a/tests/core/sccif.cc +++ b/tests/core/sccif.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017 Laboratoire de Recherche et Développement +// Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -18,6 +18,7 @@ // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/tests/core/syntimpl.cc b/tests/core/syntimpl.cc index 2c08a248d..d5037c183 100644 --- a/tests/core/syntimpl.cc +++ b/tests/core/syntimpl.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014, 2015, 2016 -// Laboratoire de Recherche et Développement de l'Epita (LRDE). +// Copyright (C) 2008-2012, 2014-2016, 2018 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. @@ -20,6 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/tests/core/taatgba.cc b/tests/core/taatgba.cc index 8ebf4f1f6..beba2d3de 100644 --- a/tests/core/taatgba.cc +++ b/tests/core/taatgba.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2014, 2015 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2009, 2014, 2015, 2018 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/tests/core/tostring.cc b/tests/core/tostring.cc index 411c1271c..895c1a490 100644 --- a/tests/core/tostring.cc +++ b/tests/core/tostring.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2009, 2012, 2015, 2016 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2008, 2009, 2012, 2015, 2016, 2018 Laboratoire de +// Recherche et Développement de l'Epita (LRDE). // Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -20,6 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/tests/core/trival.cc b/tests/core/trival.cc index 74a643d0e..203bf8177 100644 --- a/tests/core/trival.cc +++ b/tests/core/trival.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2016 Laboratoire de Recherche et Developpement de -// l'Epita (LRDE). +// Copyright (C) 2016, 2018 Laboratoire de Recherche et Developpement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -18,6 +18,7 @@ // along with this program. If not, see . #undef NDEBUG +#include "config.h" #include #include diff --git a/tests/core/twagraph.cc b/tests/core/twagraph.cc index c3cf98b20..4a34535f0 100644 --- a/tests/core/twagraph.cc +++ b/tests/core/twagraph.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014-2017 Laboratoire de Recherche et Développement +// Copyright (C) 2014-2018 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -17,7 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . - +#include "config.h" #include #include #include diff --git a/tests/ltsmin/modelcheck.cc b/tests/ltsmin/modelcheck.cc index 7a5cc9f7e..8c3770c0a 100644 --- a/tests/ltsmin/modelcheck.cc +++ b/tests/ltsmin/modelcheck.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012, 2013, 2014, 2015, 2016, 2017 Laboratoire de -// Recherche et Developpement de l'Epita (LRDE) +// Copyright (C) 2011-2018 Laboratoire de Recherche et Developpement +// de l'Epita (LRDE) // // This file is part of Spot, a model checking library. // @@ -17,6 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include "config.h" #include #include #include diff --git a/tests/sanity/includes.test b/tests/sanity/includes.test index bbcf29b89..32732bc63 100755 --- a/tests/sanity/includes.test +++ b/tests/sanity/includes.test @@ -1,6 +1,6 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2008, 2011, 2012, 2016 Laboratoire de Recherche et +# Copyright (C) 2008, 2011, 2012, 2016, 2018 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é @@ -24,6 +24,7 @@ # Check that each header is self contained and generates no warning. set -e +set +x rm -f failures.inc @@ -39,21 +40,19 @@ for file in `find "$INCDIR" \( -name "${1-*}.hh" \ # Those are not public headers, so we do not care continue else - echo "Missing, or incorrect include guard." >&2 - echo "FAIL: $file" - echo " $file" >> failures.inc + echo "FAIL: $file (missing #pragma once)" + echo " $file (missing #pragma once)" >> failures.inc continue fi echo "#include " >incltest.cc - if $CXX $CPPFLAGS -DSKIP_DEPRECATED_WARNING $CXXFLAGS \ -I$top_builddir -I$top_srcdir -I$top_srcdir/buddy/src \ -c incltest.cc; then echo "PASS: $file" else - echo "FAIL: $file" - echo " $file" >> failures.inc + echo "FAIL: $file (not self-contained)" + echo " $file (not self-contained)" >> failures.inc fi done diff --git a/tests/sanity/style.test b/tests/sanity/style.test index bcf29fea8..131d049bb 100755 --- a/tests/sanity/style.test +++ b/tests/sanity/style.test @@ -1,6 +1,6 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2009-2017 Laboratoire de Recherche et Développement de +# Copyright (C) 2009-2018 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é @@ -306,11 +306,16 @@ for dir in "$TOP/spot" "$TOP/bin" "$TOP/tests"; do *) $GREP '#.*include.*priv/' $tmp && diag 'Do not include private headers in public headers.' - $GREP '^[^#]*[^#_]assert[ ]*(.*)' $tmp && - diag 'Use SPOT_ASSERT() instead of assert() in public headers.' + $GREP '^[^#]*[^#_]assert[ ]*(.*)' $tmp && + diag 'Use SPOT_ASSERT() instead of assert() in public headers.' ;; - esac + case $file in + */bin/*);; + *.hh) + $GREP '#.*include.*[<"]config.h[">]' $tmp && + diag 'Do not include config.h in header files.' + esac ;; *.cc) if $GREP 'namespace$' $tmp >/dev/null; then @@ -322,7 +327,15 @@ for dir in "$TOP/spot" "$TOP/bin" "$TOP/tests"; do fi e$GREP ' ' $tmp && diag 'Use spaces instead of tabs.' - ;; + case $file in + */bin/*) ;; + *) + if $GREP -q '#.*include.*"config.h"' $tmp; then + : + else + diag "*.cc files should include "'"config.h"' + fi;; + esac;; esac case $file in */bin/*|*.cc);;