diff --git a/README b/README
index 37344b5f5..0f9f965b4 100644
--- a/README
+++ b/README
@@ -155,6 +155,10 @@ Core directories
----------------
src/ Sources for libspot.
+ bin/ User tools built using the Spot library.
+ man/ Man pages for the above tools.
+ eltlparse/ Parser for ELTL formulae.
+ eltltest/ Tests for ELTL nodes in ltlast/ and eltlparse/.
kripke/ Kripke Structure interface.
kripkeparse/ Parser for explicit Kripke.
kripketest/ Tests for kripke explicit.
@@ -164,6 +168,8 @@ src/ Sources for libspot.
ltlvisit/ Visitors of LTL formulae.
ltltest/ Tests for ltlast/, ltlenv/, ltlparse/, and ltlvisit/.
misc/ Miscellaneous support files.
+ neverparse/ Parser for SPIN never claims.
+ priv/ Private algorithms, used internally but not exported.
tgba/ TGBA objects and cousins.
tgbaalgos/ Algorithms on TGBA.
gtec/ Couvreur's Emptiness-Check.
@@ -171,14 +177,9 @@ src/ Sources for libspot.
ta/ TA objects and cousins (TGTA).
taalgos/ Algorithms on TA/TGTA.
tgbatest/ Tests for tgba/, tgbaalgos/, tgbaparse/, ta/ and taalgos/.
- eltlparse/ Parser for ELTL formulae.
- eltltest/ Tests for ELTL nodes in ltlast/ and eltlparse/.
saba/ SABA (State-labeled Alternating Büchi Automata) objects.
sabaalgos/ Algorithms on SABA.
sabatest/ Tests for saba/, sabaalgos/.
- neverparse/ Parser for SPIN never claims.
- bin/ User tools built using the Spot library.
- man/ Man pages for the above tools.
sanity/ Sanity tests for the whole project.
doc/ Documentation for libspot.
org/ Source of userdoc/ as org-mode files.
diff --git a/configure.ac b/configure.ac
index dd45ef26e..a4c800039 100644
--- a/configure.ac
+++ b/configure.ac
@@ -161,6 +161,7 @@ AC_CONFIG_FILES([
src/Makefile
src/misc/Makefile
src/neverparse/Makefile
+ src/priv/Makefile
src/sanity/Makefile
src/saba/Makefile
src/sabaalgos/Makefile
diff --git a/src/Makefile.am b/src/Makefile.am
index 78de8ff2c..48cfc396d 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -25,7 +25,7 @@ AUTOMAKE_OPTIONS = subdir-objects
# List directories in the order they must be built. Keep tests at the
# end, after building '.' (since the current directory contains
# libspot.la needed by the tests)
-SUBDIRS = misc ltlenv ltlast ltlvisit ltlparse eltlparse tgba \
+SUBDIRS = misc priv ltlenv ltlast ltlvisit ltlparse eltlparse tgba \
tgbaalgos tgbaparse ta taalgos kripke saba sabaalgos \
neverparse kripkeparse . bin ltltest eltltest tgbatest \
sabatest sanity kripketest
@@ -34,22 +34,23 @@ lib_LTLIBRARIES = libspot.la
libspot_la_SOURCES =
libspot_la_LDFLAGS = $(BUDDY_LDFLAGS) -no-undefined
libspot_la_LIBADD = \
- misc/libmisc.la \
+ eltlparse/libeltlparse.la \
+ kripke/libkripke.la \
+ kripkeparse/libkripkeparse.la \
+ ltlast/libltlast.la \
ltlenv/libltlenv.la \
ltlparse/libltlparse.la \
ltlvisit/libltlvisit.la \
- ltlast/libltlast.la \
- eltlparse/libeltlparse.la \
- tgba/libtgba.la \
- tgbaalgos/libtgbaalgos.la \
- ta/libta.la \
- taalgos/libtaalgos.la \
- tgbaparse/libtgbaparse.la \
+ misc/libmisc.la \
neverparse/libneverparse.la \
- saba/libsaba.la \
+ priv/libpriv.la \
sabaalgos/libsabaalgos.la \
- kripke/libkripke.la \
- kripkeparse/libkripkeparse.la
+ saba/libsaba.la \
+ taalgos/libtaalgos.la \
+ ta/libta.la \
+ tgbaalgos/libtgbaalgos.la \
+ tgba/libtgba.la \
+ tgbaparse/libtgbaparse.la
# Dummy C++ source to cause C++ linking.
nodist_EXTRA_libspot_la_SOURCES = _.cc
diff --git a/src/misc/Makefile.am b/src/misc/Makefile.am
index 5271ccad5..bf27c91ca 100644
--- a/src/misc/Makefile.am
+++ b/src/misc/Makefile.am
@@ -29,8 +29,6 @@ nodist_misc_HEADERS = _config.h
DISTCLEANFILES = _config.h
misc_HEADERS = \
- acccompl.hh \
- accconv.hh \
bareword.hh \
bddalloc.hh \
bddlt.hh \
@@ -58,8 +56,6 @@ misc_HEADERS = \
noinst_LTLIBRARIES = libmisc.la
libmisc_la_SOURCES = \
- acccompl.cc \
- accconv.cc \
bareword.cc \
bddalloc.cc \
bddop.cc \
diff --git a/src/priv/Makefile.am b/src/priv/Makefile.am
new file mode 100644
index 000000000..2d5c7d56f
--- /dev/null
+++ b/src/priv/Makefile.am
@@ -0,0 +1,31 @@
+## -*- coding: utf-8 -*-
+## Copyright (C) 2013 Laboratoire de Recherche et
+## Développement de l'Epita (LRDE).
+##
+## This file is part of Spot, a model checking library.
+##
+## Spot is free software; you can redistribute it and/or modify it
+## under the terms of the GNU General Public License as published by
+## the Free Software Foundation; either version 3 of the License, or
+## (at your option) any later version.
+##
+## Spot is distributed in the hope that it will be useful, but WITHOUT
+## ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+## or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
+## License for more details.
+##
+## You should have received a copy of the GNU General Public License
+## along with this program. If not, see .
+
+AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(BUDDY_CPPFLAGS)
+AM_CXXFLAGS = $(WARNING_CXXFLAGS) $(VISIBILITY_CXXFLAGS)
+
+noinst_HEADERS = \
+ acccompl.hh \
+ accconv.hh
+
+noinst_LTLIBRARIES = libpriv.la
+libpriv_la_SOURCES = \
+ acccompl.cc \
+ accconv.cc
+
diff --git a/src/misc/acccompl.cc b/src/priv/acccompl.cc
similarity index 100%
rename from src/misc/acccompl.cc
rename to src/priv/acccompl.cc
diff --git a/src/misc/acccompl.hh b/src/priv/acccompl.hh
similarity index 100%
rename from src/misc/acccompl.hh
rename to src/priv/acccompl.hh
diff --git a/src/misc/accconv.cc b/src/priv/accconv.cc
similarity index 100%
rename from src/misc/accconv.cc
rename to src/priv/accconv.cc
diff --git a/src/misc/accconv.hh b/src/priv/accconv.hh
similarity index 100%
rename from src/misc/accconv.hh
rename to src/priv/accconv.hh
diff --git a/src/sanity/style.test b/src/sanity/style.test
index 18c61709c..3a2057bea 100755
--- a/src/sanity/style.test
+++ b/src/sanity/style.test
@@ -242,6 +242,12 @@ for dir in "${INCDIR-..}" "${INCDIR-..}"/../iface; do
grep '#.*include.*' $tmp &&
diag 'Avoid in headers, better use .'
fi
+ # Headers from src/priv/ are not installed, so may only be
+ # included from *.cc files or from other src/priv/ headers
+ # (in the latter case they do not have to specify the priv/
+ # directory, so they will not match this regex).
+ grep '#.*include.*priv/' $tmp &&
+ diag 'Do not include private headers in public headers.'
;;
*.cc)
if grep 'namespace$' $tmp >/dev/null; then
diff --git a/src/tgbaalgos/scc.cc b/src/tgbaalgos/scc.cc
index 5c4963f43..3ec480ead 100644
--- a/src/tgbaalgos/scc.cc
+++ b/src/tgbaalgos/scc.cc
@@ -24,7 +24,7 @@
#include "scc.hh"
#include "tgba/bddprint.hh"
#include "misc/escape.hh"
-#include "misc/accconv.hh"
+#include "priv/accconv.hh"
namespace spot
{
diff --git a/src/tgbaalgos/simulation.cc b/src/tgbaalgos/simulation.cc
index 953ce79e7..a938300a7 100644
--- a/src/tgbaalgos/simulation.cc
+++ b/src/tgbaalgos/simulation.cc
@@ -24,7 +24,7 @@
#include
#include "tgba/tgbaexplicit.hh"
#include "simulation.hh"
-#include "misc/acccompl.hh"
+#include "priv/acccompl.hh"
#include "misc/minato.hh"
#include "misc/unique_ptr.hh"
#include "tgba/bddprint.hh"