From 6ded5e75c469a93c05ad7e5e9150557a4ea57179 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 28 Sep 2015 15:15:55 +0200 Subject: [PATCH] merge ltlvisit/ ltlast/ ltlenv/ into a single tl/ directory The ltl prefix does not make a lot of sens anymore (since we support psl as well). ltlast/ and ltlenv/ were almost empty. And ltlvisit/ did not contain any visitor anymore. * src/ltlvisit/, src/ltlast/, src/ltlenv/: Merge into... * src/tl/: ...this. * NEWS: Mention the change. * README, bench/stutter/stutter_invariance_formulas.cc, bench/stutter/stutter_invariance_randomgraph.cc, configure.ac, doc/org/tut01.org, doc/org/tut02.org, doc/org/tut10.org, doc/tl/tl.tex, iface/ltsmin/ltsmin.hh, iface/ltsmin/modelcheck.cc, src/Makefile.am, src/bin/autfilt.cc, src/bin/common_output.cc, src/bin/common_output.hh, src/bin/common_r.hh, src/bin/common_trans.cc, src/bin/genltl.cc, src/bin/ltl2tgba.cc, src/bin/ltl2tgta.cc, src/bin/ltlcross.cc, src/bin/ltldo.cc, src/bin/ltlfilt.cc, src/bin/ltlgrind.cc, src/bin/randltl.cc, src/kripke/kripkeexplicit.hh, src/kripkeparse/public.hh, src/parseaut/public.hh, src/priv/accmap.hh, src/ta/taexplicit.hh, src/ta/tgtaexplicit.hh, src/tests/equalsf.cc, src/tests/ikwiad.cc, src/tests/length.cc, src/tests/ltlrel.cc, src/tests/randtgba.cc, src/tests/readltl.cc, src/tests/reduc.cc, src/tests/syntimpl.cc, src/tests/taatgba.cc, src/tests/tostring.cc, src/tests/twagraph.cc, src/twa/acc.hh, src/twa/bdddict.cc, src/twa/bdddict.hh, src/twa/bddprint.cc, src/twa/taatgba.cc, src/twa/taatgba.hh, src/twa/twa.hh, src/twa/twagraph.cc, src/twa/twagraph.hh, src/twa/twasafracomplement.cc, src/twaalgos/compsusp.cc, src/twaalgos/compsusp.hh, src/twaalgos/dtgbasat.cc, src/twaalgos/hoa.cc, src/twaalgos/isweakscc.cc, src/twaalgos/lbtt.cc, src/twaalgos/ltl2taa.cc, src/twaalgos/ltl2taa.hh, src/twaalgos/ltl2tgba_fm.cc, src/twaalgos/ltl2tgba_fm.hh, src/twaalgos/minimize.hh, src/twaalgos/neverclaim.cc, src/twaalgos/randomgraph.hh, src/twaalgos/relabel.hh, src/twaalgos/remprop.hh, src/twaalgos/stats.cc, src/twaalgos/stutter.cc, src/twaalgos/translate.hh, wrap/python/spot_impl.i, src/ltlparse/ltlparse.yy, src/ltlparse/public.hh: Adjust. --- NEWS | 5 ++ README | 4 +- bench/stutter/stutter_invariance_formulas.cc | 3 +- .../stutter/stutter_invariance_randomgraph.cc | 2 +- configure.ac | 18 +++-- doc/org/tut01.org | 16 ++--- doc/org/tut02.org | 4 +- doc/org/tut10.org | 2 +- doc/tl/tl.tex | 2 +- iface/ltsmin/ltsmin.hh | 2 +- iface/ltsmin/modelcheck.cc | 2 +- src/Makefile.am | 11 ++- src/bin/autfilt.cc | 2 +- src/bin/common_output.cc | 2 +- src/bin/common_output.hh | 2 +- src/bin/common_r.hh | 2 +- src/bin/common_trans.cc | 2 +- src/bin/genltl.cc | 4 +- src/bin/ltl2tgba.cc | 4 +- src/bin/ltl2tgta.cc | 4 +- src/bin/ltlcross.cc | 8 +-- src/bin/ltldo.cc | 2 +- src/bin/ltlfilt.cc | 16 ++--- src/bin/ltlgrind.cc | 2 +- src/bin/randltl.cc | 4 +- src/kripke/kripkeexplicit.hh | 2 +- src/kripkeparse/public.hh | 2 +- src/ltlast/Makefile.am | 32 --------- src/ltlenv/.gitignore | 7 -- src/ltlenv/Makefile.am | 36 ---------- src/ltlparse/ltlparse.yy | 4 +- src/ltlparse/public.hh | 4 +- src/ltlvisit/.gitignore | 6 -- src/ltlvisit/Makefile.am | 63 ----------------- src/parseaut/public.hh | 2 +- src/priv/accmap.hh | 2 +- src/ta/taexplicit.hh | 2 +- src/ta/tgtaexplicit.hh | 2 +- src/tests/equalsf.cc | 8 +-- src/tests/ikwiad.cc | 6 +- src/tests/length.cc | 2 +- src/tests/ltlrel.cc | 4 +- src/tests/randtgba.cc | 12 ++-- src/tests/readltl.cc | 2 +- src/tests/reduc.cc | 6 +- src/tests/syntimpl.cc | 6 +- src/tests/taatgba.cc | 2 +- src/tests/tostring.cc | 2 +- src/tests/twagraph.cc | 2 +- src/{ltlast => tl}/.gitignore | 1 + src/tl/Makefile.am | 67 +++++++++++++++++++ src/{ltlvisit => tl}/apcollect.cc | 0 src/{ltlvisit => tl}/apcollect.hh | 2 +- src/{ltlvisit => tl}/contain.cc | 2 +- src/{ltlvisit => tl}/contain.hh | 2 +- src/{ltlenv => tl}/declenv.cc | 0 src/{ltlenv => tl}/declenv.hh | 2 +- src/{ltlenv => tl}/defaultenv.cc | 0 src/{ltlenv => tl}/defaultenv.hh | 2 +- src/{ltlvisit => tl}/dot.cc | 2 +- src/{ltlvisit => tl}/dot.hh | 2 +- src/{ltlenv => tl}/environment.hh | 2 +- src/{ltlvisit => tl}/exclusive.cc | 0 src/{ltlvisit => tl}/exclusive.hh | 2 +- src/{ltlast => tl}/formula.cc | 5 ++ src/{ltlast => tl}/formula.hh | 2 +- src/{ltlvisit => tl}/length.cc | 2 +- src/{ltlvisit => tl}/length.hh | 2 +- src/{ltlvisit => tl}/mark.cc | 0 src/{ltlvisit => tl}/mark.hh | 2 +- src/{ltlvisit => tl}/mutation.cc | 6 +- src/{ltlvisit => tl}/mutation.hh | 2 +- src/{ltlvisit => tl}/nenoform.cc | 0 src/{ltlvisit => tl}/nenoform.hh | 2 +- src/{ltlvisit => tl}/print.cc | 0 src/{ltlvisit => tl}/print.hh | 2 +- src/{ltlvisit => tl}/randomltl.cc | 2 +- src/{ltlvisit => tl}/randomltl.hh | 0 src/{ltlvisit => tl}/relabel.cc | 0 src/{ltlvisit => tl}/relabel.hh | 2 +- src/{ltlvisit => tl}/remove_x.cc | 6 +- src/{ltlvisit => tl}/remove_x.hh | 2 +- src/{ltlvisit => tl}/simpfg.cc | 0 src/{ltlvisit => tl}/simpfg.hh | 2 +- src/{ltlvisit => tl}/simplify.cc | 6 +- src/{ltlvisit => tl}/simplify.hh | 2 +- src/{ltlvisit => tl}/snf.cc | 0 src/{ltlvisit => tl}/snf.hh | 2 +- src/{ltlvisit => tl}/unabbrev.cc | 0 src/{ltlvisit => tl}/unabbrev.hh | 2 +- src/twa/acc.hh | 2 +- src/twa/bdddict.cc | 6 +- src/twa/bdddict.hh | 2 +- src/twa/bddprint.cc | 2 +- src/twa/taatgba.cc | 2 +- src/twa/taatgba.hh | 2 +- src/twa/twa.hh | 2 +- src/twa/twagraph.cc | 2 +- src/twa/twagraph.hh | 2 +- src/twa/twasafracomplement.cc | 2 +- src/twaalgos/compsusp.cc | 4 +- src/twaalgos/compsusp.hh | 2 +- src/twaalgos/dtgbasat.cc | 2 +- src/twaalgos/hoa.cc | 2 +- src/twaalgos/isweakscc.cc | 2 +- src/twaalgos/lbtt.cc | 2 +- src/twaalgos/ltl2taa.cc | 6 +- src/twaalgos/ltl2taa.hh | 2 +- src/twaalgos/ltl2tgba_fm.cc | 10 +-- src/twaalgos/ltl2tgba_fm.hh | 6 +- src/twaalgos/minimize.hh | 2 +- src/twaalgos/neverclaim.cc | 2 +- src/twaalgos/randomgraph.hh | 4 +- src/twaalgos/relabel.hh | 2 +- src/twaalgos/remprop.hh | 2 +- src/twaalgos/stats.cc | 2 +- src/twaalgos/stutter.cc | 4 +- src/twaalgos/translate.hh | 2 +- wrap/python/spot_impl.i | 52 +++++++------- 119 files changed, 269 insertions(+), 343 deletions(-) delete mode 100644 src/ltlast/Makefile.am delete mode 100644 src/ltlenv/.gitignore delete mode 100644 src/ltlenv/Makefile.am delete mode 100644 src/ltlvisit/.gitignore delete mode 100644 src/ltlvisit/Makefile.am rename src/{ltlast => tl}/.gitignore (84%) create mode 100644 src/tl/Makefile.am rename src/{ltlvisit => tl}/apcollect.cc (100%) rename src/{ltlvisit => tl}/apcollect.hh (98%) rename src/{ltlvisit => tl}/contain.cc (99%) rename src/{ltlvisit => tl}/contain.hh (98%) rename src/{ltlenv => tl}/declenv.cc (100%) rename src/{ltlenv => tl}/declenv.hh (98%) rename src/{ltlenv => tl}/defaultenv.cc (100%) rename src/{ltlenv => tl}/defaultenv.hh (98%) rename src/{ltlvisit => tl}/dot.cc (99%) rename src/{ltlvisit => tl}/dot.hh (97%) rename src/{ltlenv => tl}/environment.hh (98%) rename src/{ltlvisit => tl}/exclusive.cc (100%) rename src/{ltlvisit => tl}/exclusive.hh (97%) rename src/{ltlast => tl}/formula.cc (99%) rename src/{ltlast => tl}/formula.hh (99%) rename src/{ltlvisit => tl}/length.cc (98%) rename src/{ltlvisit => tl}/length.hh (98%) rename src/{ltlvisit => tl}/mark.cc (100%) rename src/{ltlvisit => tl}/mark.hh (97%) rename src/{ltlvisit => tl}/mutation.cc (98%) rename src/{ltlvisit => tl}/mutation.hh (97%) rename src/{ltlvisit => tl}/nenoform.cc (100%) rename src/{ltlvisit => tl}/nenoform.hh (98%) rename src/{ltlvisit => tl}/print.cc (100%) rename src/{ltlvisit => tl}/print.hh (99%) rename src/{ltlvisit => tl}/randomltl.cc (99%) rename src/{ltlvisit => tl}/randomltl.hh (100%) rename src/{ltlvisit => tl}/relabel.cc (100%) rename src/{ltlvisit => tl}/relabel.hh (98%) rename src/{ltlvisit => tl}/remove_x.cc (96%) rename src/{ltlvisit => tl}/remove_x.hh (98%) rename src/{ltlvisit => tl}/simpfg.cc (100%) rename src/{ltlvisit => tl}/simpfg.hh (98%) rename src/{ltlvisit => tl}/simplify.cc (99%) rename src/{ltlvisit => tl}/simplify.hh (99%) rename src/{ltlvisit => tl}/snf.cc (100%) rename src/{ltlvisit => tl}/snf.hh (98%) rename src/{ltlvisit => tl}/unabbrev.cc (100%) rename src/{ltlvisit => tl}/unabbrev.hh (98%) diff --git a/NEWS b/NEWS index 86554f017..149b4a74b 100644 --- a/NEWS +++ b/NEWS @@ -41,6 +41,11 @@ New in spot 1.99.3a (not yet released) more friendly, and several algorithms that spanned a few pages have been reduced to a few lines. + * The source directories ltlast/, ltlenv/, and ltlvisit/, have been + merged into a single tl/ directory (for temporal logic). This is + motivated by the fact that these formulas are not restricted to + LTL, and by the fact that we no longuer use the "visitor" pattern. + New in spot 1.99.3 (2015-08-26) * The CGI script for LTL translation offers a HOA download link diff --git a/README b/README index 039943851..447469f7a 100644 --- a/README +++ b/README @@ -140,10 +140,8 @@ src/ Sources for libspot. graph/ Graph representations. kripke/ Kripke Structure interface. kripkeparse/ Parser for explicit Kripke. - ltlast/ LTL abstract syntax tree (including nodes for ELTL). - ltlenv/ LTL environments. + tl/ Temporal Logic formulas and algorithms. ltlparse/ Parser for LTL formulae. - ltlvisit/ Visitors of LTL formulae. misc/ Miscellaneous support files. parseaut/ Parser for automata in multiple formats. priv/ Private algorithms, used internally but not exported. diff --git a/bench/stutter/stutter_invariance_formulas.cc b/bench/stutter/stutter_invariance_formulas.cc index 46ec21125..c23190d5d 100644 --- a/bench/stutter/stutter_invariance_formulas.cc +++ b/bench/stutter/stutter_invariance_formulas.cc @@ -25,8 +25,7 @@ #include "twaalgos/stutter.hh" #include "twaalgos/dupexp.hh" #include "twaalgos/stats.hh" -#include "ltlvisit/apcollect.hh" -#include "ltlvisit/length.hh" +#include "tl/apcollect.hh" #include "misc/timer.hh" #include diff --git a/bench/stutter/stutter_invariance_randomgraph.cc b/bench/stutter/stutter_invariance_randomgraph.cc index 8c3d27750..5575bfce0 100644 --- a/bench/stutter/stutter_invariance_randomgraph.cc +++ b/bench/stutter/stutter_invariance_randomgraph.cc @@ -18,7 +18,7 @@ // along with this program. If not, see . #include "misc/timer.hh" -#include "ltlvisit/apcollect.hh" +#include "tl/apcollect.hh" #include "twaalgos/dtgbacomp.hh" #include "twaalgos/randomgraph.hh" #include "twaalgos/dot.hh" diff --git a/configure.ac b/configure.ac index 273a489f2..07f15f62f 100644 --- a/configure.ac +++ b/configure.ac @@ -200,28 +200,26 @@ AC_CONFIG_FILES([ lib/Makefile src/bin/Makefile src/bin/man/Makefile - src/kripke/Makefile src/graph/Makefile - src/parseaut/Makefile - src/ltlast/Makefile - src/ltlenv/Makefile - src/ltlparse/Makefile + src/kripke/Makefile src/kripkeparse/Makefile - src/ltlvisit/Makefile + src/ltlparse/Makefile src/Makefile src/misc/Makefile + src/parseaut/Makefile src/priv/Makefile src/sanity/Makefile - src/twaalgos/gtec/Makefile - src/twaalgos/Makefile - src/twa/Makefile src/taalgos/Makefile src/ta/Makefile src/tests/defs src/tests/Makefile + src/tl/Makefile + src/twaalgos/gtec/Makefile + src/twaalgos/Makefile + src/twa/Makefile wrap/Makefile - wrap/python/Makefile wrap/python/ajax/Makefile + wrap/python/Makefile wrap/python/tests/Makefile tools/x-to-1 ]) diff --git a/doc/org/tut01.org b/doc/org/tut01.org index d9d12d71d..2c91a597b 100644 --- a/doc/org/tut01.org +++ b/doc/org/tut01.org @@ -67,7 +67,7 @@ exceptions. #+BEGIN_SRC C++ :results verbatim :exports both #include #include "ltlparse/public.hh" - #include "ltlvisit/print.hh" + #include "tl/print.hh" int main() { @@ -105,7 +105,7 @@ Here is how to call the infix parser explicitly,: #include #include #include "ltlparse/public.hh" - #include "ltlvisit/print.hh" + #include "tl/print.hh" int main() { @@ -147,7 +147,7 @@ with the "fixed" formula if you wish. Here is an example: #include #include #include "ltlparse/public.hh" - #include "ltlvisit/print.hh" + #include "tl/print.hh" int main() { @@ -189,7 +189,7 @@ of =parse_infix_psl()=. #include #include #include "ltlparse/public.hh" - #include "ltlvisit/print.hh" + #include "tl/print.hh" int main() { @@ -231,7 +231,7 @@ For instance, let's see what happens if a PSL formulas is passed to #include #include #include "ltlparse/public.hh" - #include "ltlvisit/print.hh" + #include "tl/print.hh" int main() { @@ -261,7 +261,7 @@ The first is to simply diagnose non-LTL formulas. #include #include #include "ltlparse/public.hh" - #include "ltlvisit/print.hh" + #include "tl/print.hh" int main() { @@ -290,8 +290,8 @@ prepared to reject the formula any way. In our example, we are lucky #include #include #include "ltlparse/public.hh" - #include "ltlvisit/print.hh" - #include "ltlvisit/simplify.hh" + #include "tl/print.hh" + #include "tl/simplify.hh" int main() { diff --git a/doc/org/tut02.org b/doc/org/tut02.org index 138e68a28..3e6c032d2 100644 --- a/doc/org/tut02.org +++ b/doc/org/tut02.org @@ -81,8 +81,8 @@ destructor. #include #include #include "ltlparse/public.hh" - #include "ltlvisit/print.hh" - #include "ltlvisit/relabel.hh" + #include "tl/print.hh" + #include "tl/relabel.hh" int main() { diff --git a/doc/org/tut10.org b/doc/org/tut10.org index 9b269c621..e210bd14d 100644 --- a/doc/org/tut10.org +++ b/doc/org/tut10.org @@ -130,7 +130,7 @@ never claim is done via the =print_never_claim= function. #include #include #include "ltlparse/public.hh" - #include "ltlvisit/print.hh" + #include "tl/print.hh" #include "twaalgos/translate.hh" #include "twaalgos/neverclaim.hh" diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index e9e1ff8ec..0d7c92f36 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -1287,7 +1287,7 @@ you plan to abbreviate many formulas sharing identical subformulas. The LTL rewritings described in the next three sections are all implemented in the `\verb|ltl_simplifier|' class defined in -\texttt{spot/ltlvisit/simplify.hh}. This class implements several +\texttt{spot/tl/simplify.hh}. This class implements several caches in order to quickly rewrite formulas that have already been rewritten previously. For this reason, it is suggested that you reuse your instance of `\verb|ltl_simplifier|' as much as possible. If you diff --git a/iface/ltsmin/ltsmin.hh b/iface/ltsmin/ltsmin.hh index 7daa88de2..cdc6985dc 100644 --- a/iface/ltsmin/ltsmin.hh +++ b/iface/ltsmin/ltsmin.hh @@ -20,7 +20,7 @@ #pragma once #include "kripke/kripke.hh" -#include "ltlvisit/apcollect.hh" +#include "tl/apcollect.hh" namespace spot { diff --git a/iface/ltsmin/modelcheck.cc b/iface/ltsmin/modelcheck.cc index 71e66b2e9..3e1c19b7c 100644 --- a/iface/ltsmin/modelcheck.cc +++ b/iface/ltsmin/modelcheck.cc @@ -19,7 +19,7 @@ #include "ltsmin.hh" #include "twaalgos/dot.hh" -#include "ltlenv/defaultenv.hh" +#include "tl/defaultenv.hh" #include "ltlparse/public.hh" #include "twaalgos/translate.hh" #include "twaalgos/emptiness.hh" diff --git a/src/Makefile.am b/src/Makefile.am index 5a86005f6..8efd0d9c3 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -25,25 +25,22 @@ 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 priv ltlenv ltlast ltlvisit ltlparse graph twa \ - twaalgos ta taalgos kripke kripkeparse parseaut . bin tests \ - sanity +SUBDIRS = misc priv tl ltlparse graph twa twaalgos ta taalgos kripke \ + kripkeparse parseaut . bin tests sanity lib_LTLIBRARIES = libspot.la libspot_la_SOURCES = libspot_la_LDFLAGS = $(BUDDY_LDFLAGS) -no-undefined libspot_la_LIBADD = \ - parseaut/libparseaut.la \ kripke/libkripke.la \ kripkeparse/libkripkeparse.la \ - ltlast/libltlast.la \ - ltlenv/libltlenv.la \ ltlparse/libltlparse.la \ - ltlvisit/libltlvisit.la \ misc/libmisc.la \ + parseaut/libparseaut.la \ priv/libpriv.la \ taalgos/libtaalgos.la \ ta/libta.la \ + tl/libtl.la \ twaalgos/libtwaalgos.la \ twa/libtwa.la \ ../lib/libgnu.la diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index ab6842317..de42801ac 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -44,7 +44,7 @@ #include "misc/timer.hh" #include "misc/random.hh" #include "parseaut/public.hh" -#include "ltlvisit/exclusive.hh" +#include "tl/exclusive.hh" #include "twaalgos/remprop.hh" #include "twaalgos/randomize.hh" #include "twaalgos/are_isomorphic.hh" diff --git a/src/bin/common_output.cc b/src/bin/common_output.cc index adbdbb55f..9f2c70960 100644 --- a/src/bin/common_output.cc +++ b/src/bin/common_output.cc @@ -21,7 +21,7 @@ #include "common_output.hh" #include #include -#include "ltlvisit/print.hh" +#include "tl/print.hh" #include "misc/formater.hh" #include "misc/escape.hh" #include "common_cout.hh" diff --git a/src/bin/common_output.hh b/src/bin/common_output.hh index c9e00b9cc..09989320f 100644 --- a/src/bin/common_output.hh +++ b/src/bin/common_output.hh @@ -24,7 +24,7 @@ #include #include #include -#include "ltlast/formula.hh" +#include "tl/formula.hh" #include "twaalgos/stats.hh" #include "common_output.hh" #include "common_file.hh" diff --git a/src/bin/common_r.hh b/src/bin/common_r.hh index 9c247d636..e35da9591 100644 --- a/src/bin/common_r.hh +++ b/src/bin/common_r.hh @@ -20,7 +20,7 @@ #pragma once #include "common_sys.hh" -#include "ltlvisit/simplify.hh" +#include "tl/simplify.hh" #define OPT_R 'r' diff --git a/src/bin/common_trans.cc b/src/bin/common_trans.cc index 00d2e1565..fe06a55a6 100644 --- a/src/bin/common_trans.cc +++ b/src/bin/common_trans.cc @@ -28,7 +28,7 @@ #include "error.h" -#include "ltlvisit/print.hh" +#include "tl/print.hh" #include "common_conv.hh" // A set of tools for which we know the correct output diff --git a/src/bin/genltl.cc b/src/bin/genltl.cc index 254b928de..2590d11ed 100644 --- a/src/bin/genltl.cc +++ b/src/bin/genltl.cc @@ -86,8 +86,8 @@ #include #include #include -#include "ltlast/formula.hh" -#include "ltlvisit/relabel.hh" +#include "tl/formula.hh" +#include "tl/relabel.hh" using namespace spot; using namespace spot::ltl; diff --git a/src/bin/ltl2tgba.cc b/src/bin/ltl2tgba.cc index 2b8ab34a6..d26dd1025 100644 --- a/src/bin/ltl2tgba.cc +++ b/src/bin/ltl2tgba.cc @@ -33,8 +33,8 @@ #include "common_aoutput.hh" #include "common_post.hh" -#include "ltlast/formula.hh" -#include "ltlvisit/print.hh" +#include "tl/formula.hh" +#include "tl/print.hh" #include "twaalgos/translate.hh" #include "misc/optionmap.hh" #include "misc/timer.hh" diff --git a/src/bin/ltl2tgta.cc b/src/bin/ltl2tgta.cc index 338c70238..7dbc309c9 100644 --- a/src/bin/ltl2tgta.cc +++ b/src/bin/ltl2tgta.cc @@ -33,8 +33,8 @@ #include "common_post.hh" #include "ltlparse/public.hh" -#include "ltlvisit/print.hh" -#include "ltlvisit/simplify.hh" +#include "tl/print.hh" +#include "tl/simplify.hh" #include "twaalgos/dot.hh" #include "twaalgos/ltl2tgba_fm.hh" #include "twaalgos/translate.hh" diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index 3972d9b48..40740068b 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -39,10 +39,10 @@ #include "common_file.hh" #include "common_finput.hh" #include "parseaut/public.hh" -#include "ltlvisit/print.hh" -#include "ltlvisit/apcollect.hh" -#include "ltlvisit/mutation.hh" -#include "ltlvisit/relabel.hh" +#include "tl/print.hh" +#include "tl/apcollect.hh" +#include "tl/mutation.hh" +#include "tl/relabel.hh" #include "twaalgos/lbtt.hh" #include "twaalgos/hoa.hh" #include "twaalgos/product.hh" diff --git a/src/bin/ltldo.cc b/src/bin/ltldo.cc index b93a47c48..e07549766 100644 --- a/src/bin/ltldo.cc +++ b/src/bin/ltldo.cc @@ -35,7 +35,7 @@ #include "common_post.hh" #include "common_trans.hh" -#include "ltlvisit/relabel.hh" +#include "tl/relabel.hh" #include "misc/bareword.hh" #include "misc/timer.hh" #include "twaalgos/lbtt.hh" diff --git a/src/bin/ltlfilt.cc b/src/bin/ltlfilt.cc index e753f51d9..e179b27a5 100644 --- a/src/bin/ltlfilt.cc +++ b/src/bin/ltlfilt.cc @@ -35,14 +35,14 @@ #include "common_r.hh" #include "misc/hash.hh" -#include "ltlvisit/simplify.hh" -#include "ltlvisit/length.hh" -#include "ltlvisit/relabel.hh" -#include "ltlvisit/unabbrev.hh" -#include "ltlvisit/remove_x.hh" -#include "ltlvisit/apcollect.hh" -#include "ltlvisit/exclusive.hh" -#include "ltlvisit/print.hh" +#include "tl/simplify.hh" +#include "tl/length.hh" +#include "tl/relabel.hh" +#include "tl/unabbrev.hh" +#include "tl/remove_x.hh" +#include "tl/apcollect.hh" +#include "tl/exclusive.hh" +#include "tl/print.hh" #include "twaalgos/ltl2tgba_fm.hh" #include "twaalgos/minimize.hh" #include "twaalgos/safety.hh" diff --git a/src/bin/ltlgrind.cc b/src/bin/ltlgrind.cc index 946ec2a15..ff70ac21c 100644 --- a/src/bin/ltlgrind.cc +++ b/src/bin/ltlgrind.cc @@ -27,7 +27,7 @@ #include "common_output.hh" #include "common_conv.hh" -#include "ltlvisit/mutation.hh" +#include "tl/mutation.hh" enum { OPT_AP2CONST = 1, diff --git a/src/bin/randltl.cc b/src/bin/randltl.cc index d700f004b..54fdeeed9 100644 --- a/src/bin/randltl.cc +++ b/src/bin/randltl.cc @@ -33,8 +33,8 @@ #include "common_conv.hh" #include -#include "ltlvisit/randomltl.hh" -#include "ltlvisit/simplify.hh" +#include "tl/randomltl.hh" +#include "tl/simplify.hh" #include "misc/random.hh" #include "misc/optionmap.hh" diff --git a/src/kripke/kripkeexplicit.hh b/src/kripke/kripkeexplicit.hh index cdbf8336d..c432d8beb 100644 --- a/src/kripke/kripkeexplicit.hh +++ b/src/kripke/kripkeexplicit.hh @@ -21,7 +21,7 @@ #include #include "kripke.hh" -#include "ltlast/formula.hh" +#include "tl/formula.hh" #include "kripkeprint.hh" namespace spot diff --git a/src/kripkeparse/public.hh b/src/kripkeparse/public.hh index 798ae6a0e..9bea2491d 100644 --- a/src/kripkeparse/public.hh +++ b/src/kripkeparse/public.hh @@ -21,7 +21,7 @@ #include "kripke/kripkeexplicit.hh" #include "misc/location.hh" -#include "ltlenv/defaultenv.hh" +#include "tl/defaultenv.hh" #include #include #include diff --git a/src/ltlast/Makefile.am b/src/ltlast/Makefile.am deleted file mode 100644 index 5fc301805..000000000 --- a/src/ltlast/Makefile.am +++ /dev/null @@ -1,32 +0,0 @@ -## -*- coding: utf-8 -*- -## Copyright (C) 2009, 2010, 2011, 2013, 2014, 2015 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. -## -## 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.. \ - -I$(top_builddir)/lib -I$(top_srcdir)/lib -AM_CXXFLAGS = $(WARNING_CXXFLAGS) - -ltlastdir = $(pkgincludedir)/ltlast - -ltlast_HEADERS = formula.hh - -noinst_LTLIBRARIES = libltlast.la -libltlast_la_SOURCES = formula.cc diff --git a/src/ltlenv/.gitignore b/src/ltlenv/.gitignore deleted file mode 100644 index df884f89f..000000000 --- a/src/ltlenv/.gitignore +++ /dev/null @@ -1,7 +0,0 @@ -.deps -Makefile -Makefile.in -libltlenv.a -*.lo -*.la -.libs diff --git a/src/ltlenv/Makefile.am b/src/ltlenv/Makefile.am deleted file mode 100644 index cba6c5cfc..000000000 --- a/src/ltlenv/Makefile.am +++ /dev/null @@ -1,36 +0,0 @@ -## -*- coding: utf-8 -*- -## Copyright (C) 2013 Laboratoire de Recherche et Développement de -## l'Epita (LRDE). -## Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -## département Systèmes Répartis Coopératifs (SRC), Université Pierre -## et Marie Curie. -## -## This file is part of Spot, a model checking library. -## -## 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)/.. -AM_CXXFLAGS = $(WARNING_CXXFLAGS) - -ltlenvdir = $(pkgincludedir)/ltlenv - -ltlenv_HEADERS = \ - declenv.hh \ - defaultenv.hh \ - environment.hh - -noinst_LTLIBRARIES = libltlenv.la -libltlenv_la_SOURCES = \ - declenv.cc \ - defaultenv.cc diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy index 52c38990c..a5bbc81bc 100644 --- a/src/ltlparse/ltlparse.yy +++ b/src/ltlparse/ltlparse.yy @@ -35,8 +35,8 @@ #include #include #include "public.hh" -#include "ltlast/formula.hh" -#include "ltlvisit/print.hh" +#include "tl/formula.hh" +#include "tl/print.hh" struct minmax_t { unsigned min, max; }; } diff --git a/src/ltlparse/public.hh b/src/ltlparse/public.hh index 0a7705a5d..4f41ea695 100644 --- a/src/ltlparse/public.hh +++ b/src/ltlparse/public.hh @@ -22,9 +22,9 @@ #pragma once -#include "ltlast/formula.hh" +#include "tl/formula.hh" #include "misc/location.hh" -#include "ltlenv/defaultenv.hh" +#include "tl/defaultenv.hh" #include #include #include diff --git a/src/ltlvisit/.gitignore b/src/ltlvisit/.gitignore deleted file mode 100644 index 6fe665a04..000000000 --- a/src/ltlvisit/.gitignore +++ /dev/null @@ -1,6 +0,0 @@ -.deps -Makefile -Makefile.in -*.lo -*.la -.libs diff --git a/src/ltlvisit/Makefile.am b/src/ltlvisit/Makefile.am deleted file mode 100644 index abfd0d09e..000000000 --- a/src/ltlvisit/Makefile.am +++ /dev/null @@ -1,63 +0,0 @@ -## -*- coding: utf-8 -*- -## Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de -## Recherche et Developpement de l'Epita (LRDE). -## Copyright (C) 2004, 2005, 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. -## -## 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) - -ltlvisitdir = $(pkgincludedir)/ltlvisit - -ltlvisit_HEADERS = \ - apcollect.hh \ - contain.hh \ - dot.hh \ - exclusive.hh \ - length.hh \ - mutation.hh \ - nenoform.hh \ - print.hh \ - randomltl.hh \ - relabel.hh \ - remove_x.hh \ - simpfg.hh \ - simplify.hh \ - snf.hh \ - unabbrev.hh - -noinst_LTLIBRARIES = libltlvisit.la -libltlvisit_la_SOURCES = \ - apcollect.cc \ - contain.cc \ - dot.cc \ - exclusive.cc \ - length.cc \ - mark.cc \ - mark.hh \ - mutation.cc \ - nenoform.cc \ - print.cc \ - randomltl.cc \ - relabel.cc \ - remove_x.cc \ - simpfg.cc \ - simplify.cc \ - snf.cc \ - unabbrev.cc diff --git a/src/parseaut/public.hh b/src/parseaut/public.hh index a98a4e1b7..31cfbb4d6 100644 --- a/src/parseaut/public.hh +++ b/src/parseaut/public.hh @@ -21,7 +21,7 @@ #include "twa/twagraph.hh" #include "misc/location.hh" -#include "ltlenv/defaultenv.hh" +#include "tl/defaultenv.hh" #include #include #include diff --git a/src/priv/accmap.hh b/src/priv/accmap.hh index d7da5b3fa..a1c3bf5ba 100644 --- a/src/priv/accmap.hh +++ b/src/priv/accmap.hh @@ -21,7 +21,7 @@ #include #include "misc/hash.hh" -#include "ltlast/formula.hh" +#include "tl/formula.hh" #include "twa/twagraph.hh" namespace spot diff --git a/src/ta/taexplicit.hh b/src/ta/taexplicit.hh index db292f4ca..8bc9e4c6f 100644 --- a/src/ta/taexplicit.hh +++ b/src/ta/taexplicit.hh @@ -23,7 +23,7 @@ #include #include "twa/twa.hh" #include -#include "ltlast/formula.hh" +#include "tl/formula.hh" #include #include "misc/bddlt.hh" #include "ta.hh" diff --git a/src/ta/tgtaexplicit.hh b/src/ta/tgtaexplicit.hh index 644d5a7ab..d3f19d4e6 100644 --- a/src/ta/tgtaexplicit.hh +++ b/src/ta/tgtaexplicit.hh @@ -23,7 +23,7 @@ #include #include "twa/twa.hh" #include -#include "ltlast/formula.hh" +#include "tl/formula.hh" #include #include "misc/bddlt.hh" #include "taexplicit.hh" diff --git a/src/tests/equalsf.cc b/src/tests/equalsf.cc index 1b8d665d8..c46385423 100644 --- a/src/tests/equalsf.cc +++ b/src/tests/equalsf.cc @@ -27,10 +27,10 @@ #include #include #include "ltlparse/public.hh" -#include "ltlvisit/unabbrev.hh" -#include "ltlvisit/nenoform.hh" -#include "ltlvisit/simplify.hh" -#include "ltlvisit/print.hh" +#include "tl/unabbrev.hh" +#include "tl/nenoform.hh" +#include "tl/simplify.hh" +#include "tl/print.hh" void syntax(char* prog) diff --git a/src/tests/ikwiad.cc b/src/tests/ikwiad.cc index 428d9af51..309f2c4e2 100644 --- a/src/tests/ikwiad.cc +++ b/src/tests/ikwiad.cc @@ -26,9 +26,9 @@ #include #include #include -#include "ltlvisit/print.hh" -#include "ltlvisit/apcollect.hh" -#include "ltlast/formula.hh" +#include "tl/print.hh" +#include "tl/apcollect.hh" +#include "tl/formula.hh" #include "ltlparse/public.hh" #include "twaalgos/ltl2tgba_fm.hh" #include "twaalgos/ltl2taa.hh" diff --git a/src/tests/length.cc b/src/tests/length.cc index d58356acf..2646a8546 100644 --- a/src/tests/length.cc +++ b/src/tests/length.cc @@ -22,7 +22,7 @@ #include #include #include "ltlparse/public.hh" -#include "ltlvisit/length.hh" +#include "tl/length.hh" void syntax(char *prog) diff --git a/src/tests/ltlrel.cc b/src/tests/ltlrel.cc index 73f039e88..fa1f1cb47 100644 --- a/src/tests/ltlrel.cc +++ b/src/tests/ltlrel.cc @@ -21,8 +21,8 @@ #include #include #include "ltlparse/public.hh" -#include "ltlvisit/relabel.hh" -#include "ltlvisit/print.hh" +#include "tl/relabel.hh" +#include "tl/print.hh" void syntax(char *prog) diff --git a/src/tests/randtgba.cc b/src/tests/randtgba.cc index 89a0a6ee7..1c98fdb0e 100644 --- a/src/tests/randtgba.cc +++ b/src/tests/randtgba.cc @@ -31,15 +31,15 @@ #include #include #include "ltlparse/public.hh" -#include "ltlvisit/apcollect.hh" -#include "ltlvisit/randomltl.hh" -#include "ltlvisit/print.hh" -#include "ltlvisit/length.hh" -#include "ltlvisit/simplify.hh" +#include "tl/apcollect.hh" +#include "tl/randomltl.hh" +#include "tl/print.hh" +#include "tl/length.hh" +#include "tl/simplify.hh" #include "twaalgos/randomgraph.hh" #include "twaalgos/hoa.hh" #include "twaalgos/stats.hh" -#include "ltlenv/defaultenv.hh" +#include "tl/defaultenv.hh" #include "twaalgos/dot.hh" #include "misc/random.hh" #include "misc/optionmap.hh" diff --git a/src/tests/readltl.cc b/src/tests/readltl.cc index 3a5621472..b196c8cb1 100644 --- a/src/tests/readltl.cc +++ b/src/tests/readltl.cc @@ -25,7 +25,7 @@ #include #include #include "ltlparse/public.hh" -#include "ltlvisit/dot.hh" +#include "tl/dot.hh" void syntax(char* prog) diff --git a/src/tests/reduc.cc b/src/tests/reduc.cc index 880ed6030..c960916a9 100644 --- a/src/tests/reduc.cc +++ b/src/tests/reduc.cc @@ -27,9 +27,9 @@ #include #include #include "ltlparse/public.hh" -#include "ltlvisit/print.hh" -#include "ltlvisit/simplify.hh" -#include "ltlvisit/length.hh" +#include "tl/print.hh" +#include "tl/simplify.hh" +#include "tl/length.hh" void syntax(char* prog) diff --git a/src/tests/syntimpl.cc b/src/tests/syntimpl.cc index 1f98fa9cb..bee75f051 100644 --- a/src/tests/syntimpl.cc +++ b/src/tests/syntimpl.cc @@ -24,9 +24,9 @@ #include #include #include "ltlparse/public.hh" -#include "ltlvisit/print.hh" -#include "ltlvisit/simplify.hh" -#include "ltlvisit/nenoform.hh" +#include "tl/print.hh" +#include "tl/simplify.hh" +#include "tl/nenoform.hh" void syntax(char* prog) diff --git a/src/tests/taatgba.cc b/src/tests/taatgba.cc index f4d80d9d0..52e551429 100644 --- a/src/tests/taatgba.cc +++ b/src/tests/taatgba.cc @@ -20,7 +20,7 @@ #include #include #include "misc/hash.hh" -#include "ltlenv/defaultenv.hh" +#include "tl/defaultenv.hh" #include "twaalgos/dot.hh" #include "twa/taatgba.hh" diff --git a/src/tests/tostring.cc b/src/tests/tostring.cc index 6f57e620b..8585b6d11 100644 --- a/src/tests/tostring.cc +++ b/src/tests/tostring.cc @@ -24,7 +24,7 @@ #include #include #include "ltlparse/public.hh" -#include "ltlvisit/print.hh" +#include "tl/print.hh" void syntax(char *prog) diff --git a/src/tests/twagraph.cc b/src/tests/twagraph.cc index 4a1af2312..c4261faed 100644 --- a/src/tests/twagraph.cc +++ b/src/tests/twagraph.cc @@ -21,7 +21,7 @@ #include #include "twa/twagraph.hh" #include "twaalgos/dot.hh" -#include "ltlenv/defaultenv.hh" +#include "tl/defaultenv.hh" void f1() { diff --git a/src/ltlast/.gitignore b/src/tl/.gitignore similarity index 84% rename from src/ltlast/.gitignore rename to src/tl/.gitignore index 6fe665a04..842206c7a 100644 --- a/src/ltlast/.gitignore +++ b/src/tl/.gitignore @@ -1,6 +1,7 @@ .deps Makefile Makefile.in +libtl.a *.lo *.la .libs diff --git a/src/tl/Makefile.am b/src/tl/Makefile.am new file mode 100644 index 000000000..c7ae7adcc --- /dev/null +++ b/src/tl/Makefile.am @@ -0,0 +1,67 @@ +## -*- coding: utf-8 -*- +## Copyright (C) 2015 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) + +tldir = $(pkgincludedir)/tl + +tl_HEADERS = \ + apcollect.hh \ + contain.hh \ + declenv.hh \ + defaultenv.hh \ + dot.hh \ + environment.hh \ + exclusive.hh \ + formula.hh \ + length.hh \ + mutation.hh \ + nenoform.hh \ + print.hh \ + randomltl.hh \ + relabel.hh \ + remove_x.hh \ + simpfg.hh \ + simplify.hh \ + snf.hh \ + unabbrev.hh + +noinst_LTLIBRARIES = libtl.la +libtl_la_SOURCES = \ + apcollect.cc \ + contain.cc \ + declenv.cc \ + defaultenv.cc \ + dot.cc \ + exclusive.cc \ + formula.cc \ + length.cc \ + mark.cc \ + mark.hh \ + mutation.cc \ + nenoform.cc \ + print.cc \ + randomltl.cc \ + relabel.cc \ + remove_x.cc \ + simpfg.cc \ + simplify.cc \ + snf.cc \ + unabbrev.cc diff --git a/src/ltlvisit/apcollect.cc b/src/tl/apcollect.cc similarity index 100% rename from src/ltlvisit/apcollect.cc rename to src/tl/apcollect.cc diff --git a/src/ltlvisit/apcollect.hh b/src/tl/apcollect.hh similarity index 98% rename from src/ltlvisit/apcollect.hh rename to src/tl/apcollect.hh index 8c32e8dcc..70cc2cd84 100644 --- a/src/ltlvisit/apcollect.hh +++ b/src/tl/apcollect.hh @@ -22,7 +22,7 @@ #pragma once -#include "ltlast/formula.hh" +#include "formula.hh" #include #include #include "twa/fwd.hh" diff --git a/src/ltlvisit/contain.cc b/src/tl/contain.cc similarity index 99% rename from src/ltlvisit/contain.cc rename to src/tl/contain.cc index 48465fd01..6b87992ad 100644 --- a/src/ltlvisit/contain.cc +++ b/src/tl/contain.cc @@ -22,7 +22,7 @@ #include "contain.hh" #include "simplify.hh" -#include "ltlast/formula.hh" +#include "formula.hh" #include "twaalgos/product.hh" namespace spot diff --git a/src/ltlvisit/contain.hh b/src/tl/contain.hh similarity index 98% rename from src/ltlvisit/contain.hh rename to src/tl/contain.hh index f4803c95c..8ea6939b9 100644 --- a/src/ltlvisit/contain.hh +++ b/src/tl/contain.hh @@ -22,7 +22,7 @@ #pragma once -#include "ltlast/formula.hh" +#include "formula.hh" #include "twaalgos/ltl2tgba_fm.hh" #include "misc/hash.hh" #include diff --git a/src/ltlenv/declenv.cc b/src/tl/declenv.cc similarity index 100% rename from src/ltlenv/declenv.cc rename to src/tl/declenv.cc diff --git a/src/ltlenv/declenv.hh b/src/tl/declenv.hh similarity index 98% rename from src/ltlenv/declenv.hh rename to src/tl/declenv.hh index 3fd64d4b9..0fc706639 100644 --- a/src/ltlenv/declenv.hh +++ b/src/tl/declenv.hh @@ -25,7 +25,7 @@ #include "environment.hh" #include #include -#include "ltlast/formula.hh" +#include "formula.hh" namespace spot { diff --git a/src/ltlenv/defaultenv.cc b/src/tl/defaultenv.cc similarity index 100% rename from src/ltlenv/defaultenv.cc rename to src/tl/defaultenv.cc diff --git a/src/ltlenv/defaultenv.hh b/src/tl/defaultenv.hh similarity index 98% rename from src/ltlenv/defaultenv.hh rename to src/tl/defaultenv.hh index 6324683c9..e54bc0f59 100644 --- a/src/ltlenv/defaultenv.hh +++ b/src/tl/defaultenv.hh @@ -23,7 +23,7 @@ #pragma once #include "environment.hh" -#include "ltlast/formula.hh" +#include "formula.hh" namespace spot { diff --git a/src/ltlvisit/dot.cc b/src/tl/dot.cc similarity index 99% rename from src/ltlvisit/dot.cc rename to src/tl/dot.cc index 66531d916..de7da2b6a 100644 --- a/src/ltlvisit/dot.cc +++ b/src/tl/dot.cc @@ -21,7 +21,7 @@ // along with this program. If not, see . #include "dot.hh" -#include "ltlast/formula.hh" +#include "formula.hh" #include #include #include diff --git a/src/ltlvisit/dot.hh b/src/tl/dot.hh similarity index 97% rename from src/ltlvisit/dot.hh rename to src/tl/dot.hh index 0e52d1807..13438ebbd 100644 --- a/src/ltlvisit/dot.hh +++ b/src/tl/dot.hh @@ -22,7 +22,7 @@ #pragma once -#include +#include "formula.hh" namespace spot { diff --git a/src/ltlenv/environment.hh b/src/tl/environment.hh similarity index 98% rename from src/ltlenv/environment.hh rename to src/tl/environment.hh index 1692543a1..f6551c29d 100644 --- a/src/ltlenv/environment.hh +++ b/src/tl/environment.hh @@ -22,7 +22,7 @@ #pragma once -#include "ltlast/formula.hh" +#include "formula.hh" #include namespace spot diff --git a/src/ltlvisit/exclusive.cc b/src/tl/exclusive.cc similarity index 100% rename from src/ltlvisit/exclusive.cc rename to src/tl/exclusive.cc diff --git a/src/ltlvisit/exclusive.hh b/src/tl/exclusive.hh similarity index 97% rename from src/ltlvisit/exclusive.hh rename to src/tl/exclusive.hh index bb6ca06da..c420c076e 100644 --- a/src/ltlvisit/exclusive.hh +++ b/src/tl/exclusive.hh @@ -20,7 +20,7 @@ #pragma once #include -#include "ltlast/formula.hh" +#include "formula.hh" #include "twa/twagraph.hh" namespace spot diff --git a/src/ltlast/formula.cc b/src/tl/formula.cc similarity index 99% rename from src/ltlast/formula.cc rename to src/tl/formula.cc index 4b73c62e4..de16f1732 100644 --- a/src/ltlast/formula.cc +++ b/src/tl/formula.cc @@ -28,6 +28,11 @@ #include #include "misc/bareword.hh" +#ifndef HAVE_STRVERSCMP +// If the libc does not have this, a version is compiled in lib/. +extern "C" int strverscmp(const char *s1, const char *s2); +#endif + namespace spot { namespace diff --git a/src/ltlast/formula.hh b/src/tl/formula.hh similarity index 99% rename from src/ltlast/formula.hh rename to src/tl/formula.hh index dda416778..5a94fc0e9 100644 --- a/src/ltlast/formula.hh +++ b/src/tl/formula.hh @@ -17,7 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . -/// \file ltlast/formula.hh +/// \file tlformula.hh /// \brief LTL/PSL formula interface #pragma once diff --git a/src/ltlvisit/length.cc b/src/tl/length.cc similarity index 98% rename from src/ltlvisit/length.cc rename to src/tl/length.cc index ab769aa41..c345952db 100644 --- a/src/ltlvisit/length.cc +++ b/src/tl/length.cc @@ -21,7 +21,7 @@ // along with this program. If not, see . #include "length.hh" -#include "ltlast/formula.hh" +#include "formula.hh" namespace spot { diff --git a/src/ltlvisit/length.hh b/src/tl/length.hh similarity index 98% rename from src/ltlvisit/length.hh rename to src/tl/length.hh index cc194c740..5a42cdd84 100644 --- a/src/ltlvisit/length.hh +++ b/src/tl/length.hh @@ -22,7 +22,7 @@ #pragma once -#include "ltlast/formula.hh" +#include "formula.hh" namespace spot { diff --git a/src/ltlvisit/mark.cc b/src/tl/mark.cc similarity index 100% rename from src/ltlvisit/mark.cc rename to src/tl/mark.cc diff --git a/src/ltlvisit/mark.hh b/src/tl/mark.hh similarity index 97% rename from src/ltlvisit/mark.hh rename to src/tl/mark.hh index 0baf0eb3c..3431005d2 100644 --- a/src/ltlvisit/mark.hh +++ b/src/tl/mark.hh @@ -19,7 +19,7 @@ #pragma once -#include "ltlast/formula.hh" +#include "formula.hh" #include "misc/hash.hh" namespace spot diff --git a/src/ltlvisit/mutation.cc b/src/tl/mutation.cc similarity index 98% rename from src/ltlvisit/mutation.cc rename to src/tl/mutation.cc index 125406fda..42c7b907c 100644 --- a/src/ltlvisit/mutation.cc +++ b/src/tl/mutation.cc @@ -20,9 +20,9 @@ #include #include -#include "ltlvisit/apcollect.hh" -#include "ltlvisit/mutation.hh" -#include "ltlvisit/length.hh" +#include "apcollect.hh" +#include "mutation.hh" +#include "length.hh" #define And_(x, y) formula::And({(x), (y)}) #define AndRat_(x, y) formula::AndRat({(x), (y)}) diff --git a/src/ltlvisit/mutation.hh b/src/tl/mutation.hh similarity index 97% rename from src/ltlvisit/mutation.hh rename to src/tl/mutation.hh index aeb09d4f5..250ae2bd6 100644 --- a/src/ltlvisit/mutation.hh +++ b/src/tl/mutation.hh @@ -19,7 +19,7 @@ #pragma once -#include "ltlast/formula.hh" +#include "formula.hh" #include namespace spot diff --git a/src/ltlvisit/nenoform.cc b/src/tl/nenoform.cc similarity index 100% rename from src/ltlvisit/nenoform.cc rename to src/tl/nenoform.cc diff --git a/src/ltlvisit/nenoform.hh b/src/tl/nenoform.hh similarity index 98% rename from src/ltlvisit/nenoform.hh rename to src/tl/nenoform.hh index d57e1ae55..2eb6ce636 100644 --- a/src/ltlvisit/nenoform.hh +++ b/src/tl/nenoform.hh @@ -22,7 +22,7 @@ #pragma once -#include "ltlast/formula.hh" +#include "formula.hh" namespace spot { diff --git a/src/ltlvisit/print.cc b/src/tl/print.cc similarity index 100% rename from src/ltlvisit/print.cc rename to src/tl/print.cc diff --git a/src/ltlvisit/print.hh b/src/tl/print.hh similarity index 99% rename from src/ltlvisit/print.hh rename to src/tl/print.hh index e52d177fa..8491dc2de 100644 --- a/src/ltlvisit/print.hh +++ b/src/tl/print.hh @@ -22,7 +22,7 @@ #pragma once -#include +#include "formula.hh" #include namespace spot diff --git a/src/ltlvisit/randomltl.cc b/src/tl/randomltl.cc similarity index 99% rename from src/ltlvisit/randomltl.cc rename to src/tl/randomltl.cc index e39340057..3e1355e7b 100644 --- a/src/ltlvisit/randomltl.cc +++ b/src/tl/randomltl.cc @@ -27,7 +27,7 @@ #include #include #include "misc/optionmap.hh" -#include "ltlenv/defaultenv.hh" +#include "defaultenv.hh" #include namespace spot diff --git a/src/ltlvisit/randomltl.hh b/src/tl/randomltl.hh similarity index 100% rename from src/ltlvisit/randomltl.hh rename to src/tl/randomltl.hh diff --git a/src/ltlvisit/relabel.cc b/src/tl/relabel.cc similarity index 100% rename from src/ltlvisit/relabel.cc rename to src/tl/relabel.cc diff --git a/src/ltlvisit/relabel.hh b/src/tl/relabel.hh similarity index 98% rename from src/ltlvisit/relabel.hh rename to src/tl/relabel.hh index a8448be00..e26b1b234 100644 --- a/src/ltlvisit/relabel.hh +++ b/src/tl/relabel.hh @@ -19,7 +19,7 @@ #pragma once -#include "ltlast/formula.hh" +#include "formula.hh" #include "misc/hash.hh" #include diff --git a/src/ltlvisit/remove_x.cc b/src/tl/remove_x.cc similarity index 96% rename from src/ltlvisit/remove_x.cc rename to src/tl/remove_x.cc index 81491f894..f2700173d 100644 --- a/src/ltlvisit/remove_x.cc +++ b/src/tl/remove_x.cc @@ -17,9 +17,9 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . -#include "ltlvisit/simplify.hh" -#include "ltlvisit/apcollect.hh" -#include "ltlvisit/remove_x.hh" +#include "simplify.hh" +#include "apcollect.hh" +#include "remove_x.hh" namespace spot { diff --git a/src/ltlvisit/remove_x.hh b/src/tl/remove_x.hh similarity index 98% rename from src/ltlvisit/remove_x.hh rename to src/tl/remove_x.hh index e347f4466..dce03c90b 100644 --- a/src/ltlvisit/remove_x.hh +++ b/src/tl/remove_x.hh @@ -19,7 +19,7 @@ #pragma once -#include "ltlast/formula.hh" +#include "formula.hh" namespace spot { diff --git a/src/ltlvisit/simpfg.cc b/src/tl/simpfg.cc similarity index 100% rename from src/ltlvisit/simpfg.cc rename to src/tl/simpfg.cc diff --git a/src/ltlvisit/simpfg.hh b/src/tl/simpfg.hh similarity index 98% rename from src/ltlvisit/simpfg.hh rename to src/tl/simpfg.hh index e3094b140..d2480cdd4 100644 --- a/src/ltlvisit/simpfg.hh +++ b/src/tl/simpfg.hh @@ -22,7 +22,7 @@ #pragma once -#include "ltlast/formula.hh" +#include "formula.hh" namespace spot { diff --git a/src/ltlvisit/simplify.cc b/src/tl/simplify.cc similarity index 99% rename from src/ltlvisit/simplify.cc rename to src/tl/simplify.cc index 9fdce4e2f..7feec746b 100644 --- a/src/ltlvisit/simplify.cc +++ b/src/tl/simplify.cc @@ -27,9 +27,9 @@ #include "simplify.hh" #include -#include "ltlvisit/contain.hh" -#include "ltlvisit/print.hh" -#include "ltlvisit/snf.hh" +#include "contain.hh" +#include "print.hh" +#include "snf.hh" #include "twa/formula2bdd.hh" #include #include diff --git a/src/ltlvisit/simplify.hh b/src/tl/simplify.hh similarity index 99% rename from src/ltlvisit/simplify.hh rename to src/tl/simplify.hh index 7623fdb7a..7f865c898 100644 --- a/src/ltlvisit/simplify.hh +++ b/src/tl/simplify.hh @@ -19,7 +19,7 @@ #pragma once -#include "ltlast/formula.hh" +#include "formula.hh" #include #include "twa/bdddict.hh" #include diff --git a/src/ltlvisit/snf.cc b/src/tl/snf.cc similarity index 100% rename from src/ltlvisit/snf.cc rename to src/tl/snf.cc diff --git a/src/ltlvisit/snf.hh b/src/tl/snf.hh similarity index 98% rename from src/ltlvisit/snf.hh rename to src/tl/snf.hh index 74fccc528..bdb2b8d34 100644 --- a/src/ltlvisit/snf.hh +++ b/src/tl/snf.hh @@ -19,7 +19,7 @@ #pragma once -#include "ltlast/formula.hh" +#include "formula.hh" #include namespace spot diff --git a/src/ltlvisit/unabbrev.cc b/src/tl/unabbrev.cc similarity index 100% rename from src/ltlvisit/unabbrev.cc rename to src/tl/unabbrev.cc diff --git a/src/ltlvisit/unabbrev.hh b/src/tl/unabbrev.hh similarity index 98% rename from src/ltlvisit/unabbrev.hh rename to src/tl/unabbrev.hh index d0d5a35a7..635909e8a 100644 --- a/src/ltlvisit/unabbrev.hh +++ b/src/tl/unabbrev.hh @@ -19,7 +19,7 @@ #pragma once -#include "ltlast/formula.hh" +#include "formula.hh" #include namespace spot diff --git a/src/twa/acc.hh b/src/twa/acc.hh index dc5233862..81d0be41c 100644 --- a/src/twa/acc.hh +++ b/src/twa/acc.hh @@ -23,7 +23,7 @@ #include #include #include -#include "ltlenv/defaultenv.hh" +#include "tl/defaultenv.hh" #include namespace spot diff --git a/src/twa/bdddict.cc b/src/twa/bdddict.cc index d2aa2190d..9cb309a14 100644 --- a/src/twa/bdddict.cc +++ b/src/twa/bdddict.cc @@ -23,9 +23,9 @@ #include #include #include -#include -#include -#include +#include "tl/print.hh" +#include "tl/formula.hh" +#include "tl/defaultenv.hh" #include "priv/bddalloc.hh" #include "bdddict.hh" diff --git a/src/twa/bdddict.hh b/src/twa/bdddict.hh index a56ed0950..46608550a 100644 --- a/src/twa/bdddict.hh +++ b/src/twa/bdddict.hh @@ -29,7 +29,7 @@ #include #include #include -#include "ltlast/formula.hh" +#include "tl/formula.hh" namespace spot { diff --git a/src/twa/bddprint.cc b/src/twa/bddprint.cc index 2c74a5dc5..1b32736ec 100644 --- a/src/twa/bddprint.cc +++ b/src/twa/bddprint.cc @@ -24,7 +24,7 @@ #include #include #include "bddprint.hh" -#include "ltlvisit/print.hh" +#include "tl/print.hh" #include "formula2bdd.hh" #include "misc/minato.hh" diff --git a/src/twa/taatgba.cc b/src/twa/taatgba.cc index e1ddf306b..817af1660 100644 --- a/src/twa/taatgba.cc +++ b/src/twa/taatgba.cc @@ -22,7 +22,7 @@ #include #include #include "twa/formula2bdd.hh" -#include "ltlvisit/print.hh" +#include "tl/print.hh" #include "taatgba.hh" namespace spot diff --git a/src/twa/taatgba.hh b/src/twa/taatgba.hh index 4345fdb8c..dd04effd8 100644 --- a/src/twa/taatgba.hh +++ b/src/twa/taatgba.hh @@ -24,7 +24,7 @@ #include #include #include "misc/hash.hh" -#include "ltlast/formula.hh" +#include "tl/formula.hh" #include "bdddict.hh" #include "twa.hh" diff --git a/src/twa/twa.hh b/src/twa/twa.hh index fc3b7af71..8b48fcce6 100644 --- a/src/twa/twa.hh +++ b/src/twa/twa.hh @@ -33,7 +33,7 @@ #include #include "misc/casts.hh" #include "misc/hash.hh" -#include "ltlast/formula.hh" +#include "tl/formula.hh" namespace spot { diff --git a/src/twa/twagraph.cc b/src/twa/twagraph.cc index 7acb18fa0..47b4d2420 100644 --- a/src/twa/twagraph.cc +++ b/src/twa/twagraph.cc @@ -18,7 +18,7 @@ // along with this program. If not, see . #include "twagraph.hh" -#include "ltlvisit/print.hh" +#include "tl/print.hh" namespace spot { diff --git a/src/twa/twagraph.hh b/src/twa/twagraph.hh index 93fa2bf38..513416cf4 100644 --- a/src/twa/twagraph.hh +++ b/src/twa/twagraph.hh @@ -25,7 +25,7 @@ #include "twa/bdddict.hh" #include "twa/twa.hh" #include "twaalgos/dupexp.hh" -#include "ltlast/formula.hh" +#include "tl/formula.hh" #include namespace spot diff --git a/src/twa/twasafracomplement.cc b/src/twa/twasafracomplement.cc index 4907f91c6..a566a8776 100644 --- a/src/twa/twasafracomplement.cc +++ b/src/twa/twasafracomplement.cc @@ -30,7 +30,7 @@ #include "twa/bdddict.hh" #include "twa/twa.hh" #include "misc/hashfunc.hh" -#include "ltlast/formula.hh" +#include "tl/formula.hh" #include "twaalgos/dot.hh" #include "twa/twasafracomplement.hh" #include "twaalgos/degen.hh" diff --git a/src/twaalgos/compsusp.cc b/src/twaalgos/compsusp.cc index e0a8c24cb..aabdd5711 100644 --- a/src/twaalgos/compsusp.cc +++ b/src/twaalgos/compsusp.cc @@ -25,10 +25,10 @@ #include "minimize.hh" #include "simulation.hh" #include "safety.hh" -#include "ltlvisit/print.hh" +#include "tl/print.hh" #include #include -#include "ltlenv/environment.hh" +#include "tl/environment.hh" namespace spot { diff --git a/src/twaalgos/compsusp.hh b/src/twaalgos/compsusp.hh index f50f649ef..670b34f5a 100644 --- a/src/twaalgos/compsusp.hh +++ b/src/twaalgos/compsusp.hh @@ -19,7 +19,7 @@ #pragma once -#include "ltlast/formula.hh" +#include "tl/formula.hh" #include "twa/twagraph.hh" namespace spot diff --git a/src/twaalgos/dtgbasat.cc b/src/twaalgos/dtgbasat.cc index 6ee15f21e..6548abeba 100644 --- a/src/twaalgos/dtgbasat.cc +++ b/src/twaalgos/dtgbasat.cc @@ -27,7 +27,7 @@ #include "sccinfo.hh" #include "twa/bddprint.hh" #include "stats.hh" -#include "ltlenv/defaultenv.hh" +#include "tl/defaultenv.hh" #include "misc/satsolver.hh" #include "misc/timer.hh" #include "isweakscc.hh" diff --git a/src/twaalgos/hoa.cc b/src/twaalgos/hoa.cc index 0e266ca0b..64384f039 100644 --- a/src/twaalgos/hoa.cc +++ b/src/twaalgos/hoa.cc @@ -32,7 +32,7 @@ #include "misc/bddlt.hh" #include "misc/minato.hh" #include "twa/formula2bdd.hh" -#include "ltlast/formula.hh" +#include "tl/formula.hh" namespace spot { diff --git a/src/twaalgos/isweakscc.cc b/src/twaalgos/isweakscc.cc index c79e0d371..b1d960432 100644 --- a/src/twaalgos/isweakscc.cc +++ b/src/twaalgos/isweakscc.cc @@ -18,7 +18,7 @@ // along with this program. If not, see . #include "cycles.hh" -#include "ltlast/formula.hh" +#include "tl/formula.hh" #include "isweakscc.hh" namespace spot diff --git a/src/twaalgos/lbtt.cc b/src/twaalgos/lbtt.cc index e494c45b3..d07dc2290 100644 --- a/src/twaalgos/lbtt.cc +++ b/src/twaalgos/lbtt.cc @@ -28,7 +28,7 @@ #include "reachiter.hh" #include "misc/bddlt.hh" #include "priv/accmap.hh" -#include "ltlvisit/print.hh" +#include "tl/print.hh" #include "ltlparse/public.hh" namespace spot diff --git a/src/twaalgos/ltl2taa.cc b/src/twaalgos/ltl2taa.cc index 5d1a9980c..bba9306ea 100644 --- a/src/twaalgos/ltl2taa.cc +++ b/src/twaalgos/ltl2taa.cc @@ -19,9 +19,9 @@ #include #include -#include "ltlvisit/unabbrev.hh" -#include "ltlvisit/nenoform.hh" -#include "ltlvisit/contain.hh" +#include "tl/unabbrev.hh" +#include "tl/nenoform.hh" +#include "tl/contain.hh" #include "ltl2taa.hh" namespace spot diff --git a/src/twaalgos/ltl2taa.hh b/src/twaalgos/ltl2taa.hh index 90dd8067e..891e69b8a 100644 --- a/src/twaalgos/ltl2taa.hh +++ b/src/twaalgos/ltl2taa.hh @@ -19,7 +19,7 @@ #pragma once -#include "ltlast/formula.hh" +#include "tl/formula.hh" #include "twa/taatgba.hh" namespace spot diff --git a/src/twaalgos/ltl2tgba_fm.cc b/src/twaalgos/ltl2tgba_fm.cc index 1a4130cbf..1b71184fa 100644 --- a/src/twaalgos/ltl2tgba_fm.cc +++ b/src/twaalgos/ltl2tgba_fm.cc @@ -23,11 +23,11 @@ #include "misc/hash.hh" #include "misc/bddlt.hh" #include "misc/minato.hh" -#include "ltlvisit/nenoform.hh" -#include "ltlvisit/print.hh" -#include "ltlvisit/apcollect.hh" -#include "ltlvisit/mark.hh" -#include "ltlvisit/print.hh" +#include "tl/nenoform.hh" +#include "tl/print.hh" +#include "tl/apcollect.hh" +#include "tl/mark.hh" +#include "tl/print.hh" #include #include #include diff --git a/src/twaalgos/ltl2tgba_fm.hh b/src/twaalgos/ltl2tgba_fm.hh index f3f6e3885..18ad7ecb8 100644 --- a/src/twaalgos/ltl2tgba_fm.hh +++ b/src/twaalgos/ltl2tgba_fm.hh @@ -22,10 +22,10 @@ #pragma once -#include "ltlast/formula.hh" +#include "tl/formula.hh" #include "twa/twagraph.hh" -#include "ltlvisit/apcollect.hh" -#include "ltlvisit/simplify.hh" +#include "tl/apcollect.hh" +#include "tl/simplify.hh" namespace spot { diff --git a/src/twaalgos/minimize.hh b/src/twaalgos/minimize.hh index b25d6d791..87251556c 100644 --- a/src/twaalgos/minimize.hh +++ b/src/twaalgos/minimize.hh @@ -20,7 +20,7 @@ #pragma once #include "twa/twagraph.hh" -#include "ltlast/formula.hh" +#include "tl/formula.hh" namespace spot { diff --git a/src/twaalgos/neverclaim.cc b/src/twaalgos/neverclaim.cc index 014632070..4bc85c0d3 100644 --- a/src/twaalgos/neverclaim.cc +++ b/src/twaalgos/neverclaim.cc @@ -26,7 +26,7 @@ #include "twa/bddprint.hh" #include "twa/twagraph.hh" #include "reachiter.hh" -#include "ltlvisit/print.hh" +#include "tl/print.hh" #include "twa/formula2bdd.hh" namespace spot diff --git a/src/twaalgos/randomgraph.hh b/src/twaalgos/randomgraph.hh index 1b89f7787..ee034025c 100644 --- a/src/twaalgos/randomgraph.hh +++ b/src/twaalgos/randomgraph.hh @@ -22,8 +22,8 @@ #pragma once -#include "ltlvisit/apcollect.hh" -#include "ltlenv/defaultenv.hh" +#include "tl/apcollect.hh" +#include "tl/defaultenv.hh" #include "twa/bdddict.hh" #include "twa/acc.hh" diff --git a/src/twaalgos/relabel.hh b/src/twaalgos/relabel.hh index 45c1df9e9..be11d9b10 100644 --- a/src/twaalgos/relabel.hh +++ b/src/twaalgos/relabel.hh @@ -19,7 +19,7 @@ #pragma once -#include "ltlvisit/relabel.hh" +#include "tl/relabel.hh" #include "twa/twagraph.hh" namespace spot diff --git a/src/twaalgos/remprop.hh b/src/twaalgos/remprop.hh index 85d187bbb..98c8f8f6a 100644 --- a/src/twaalgos/remprop.hh +++ b/src/twaalgos/remprop.hh @@ -20,7 +20,7 @@ #pragma once #include -#include "ltlast/formula.hh" +#include "tl/formula.hh" #include "twa/twagraph.hh" namespace spot diff --git a/src/twaalgos/stats.cc b/src/twaalgos/stats.cc index a74d2e360..bde1d9ab5 100644 --- a/src/twaalgos/stats.cc +++ b/src/twaalgos/stats.cc @@ -25,7 +25,7 @@ #include "twa/twa.hh" #include "stats.hh" #include "reachiter.hh" -#include "ltlvisit/print.hh" +#include "tl/print.hh" #include "twaalgos/isdet.hh" #include "twaalgos/sccinfo.hh" diff --git a/src/twaalgos/stutter.cc b/src/twaalgos/stutter.cc index 7bc01b600..4f711dff7 100644 --- a/src/twaalgos/stutter.cc +++ b/src/twaalgos/stutter.cc @@ -22,9 +22,9 @@ #include "dupexp.hh" #include "misc/hash.hh" #include "misc/hashfunc.hh" -#include "ltlvisit/apcollect.hh" +#include "tl/apcollect.hh" #include "translate.hh" -#include "ltlvisit/remove_x.hh" +#include "tl/remove_x.hh" #include "twaalgos/product.hh" #include "twaalgos/ltl2tgba_fm.hh" #include "twaalgos/isdet.hh" diff --git a/src/twaalgos/translate.hh b/src/twaalgos/translate.hh index 3049ef074..728e75f20 100644 --- a/src/twaalgos/translate.hh +++ b/src/twaalgos/translate.hh @@ -20,7 +20,7 @@ #pragma once #include "postproc.hh" -#include "ltlvisit/simplify.hh" +#include "tl/simplify.hh" namespace spot { diff --git a/wrap/python/spot_impl.i b/wrap/python/spot_impl.i index ec47c9499..ddd73946e 100644 --- a/wrap/python/spot_impl.i +++ b/wrap/python/spot_impl.i @@ -80,25 +80,25 @@ #include "misc/optionmap.hh" #include "misc/random.hh" -#include "ltlast/formula.hh" +#include "tl/formula.hh" -#include "ltlenv/environment.hh" -#include "ltlenv/defaultenv.hh" +#include "tl/environment.hh" +#include "tl/defaultenv.hh" #include "ltlparse/public.hh" #include "twa/bdddict.hh" -#include "ltlvisit/apcollect.hh" -#include "ltlvisit/dot.hh" -#include "ltlvisit/nenoform.hh" -#include "ltlvisit/print.hh" -#include "ltlvisit/simplify.hh" -#include "ltlvisit/unabbrev.hh" -#include "ltlvisit/randomltl.hh" -#include "ltlvisit/length.hh" -#include "ltlvisit/remove_x.hh" -#include "ltlvisit/relabel.hh" +#include "tl/apcollect.hh" +#include "tl/dot.hh" +#include "tl/nenoform.hh" +#include "tl/print.hh" +#include "tl/simplify.hh" +#include "tl/unabbrev.hh" +#include "tl/randomltl.hh" +#include "tl/length.hh" +#include "tl/remove_x.hh" +#include "tl/relabel.hh" #include "twa/bddprint.hh" #include "twa/fwd.hh" @@ -211,7 +211,7 @@ using namespace spot; %implicitconv std::vector; -%include "ltlast/formula.hh" +%include "tl/formula.hh" namespace std { %template(liststr) list; @@ -220,8 +220,8 @@ namespace std { %template(relabeling_map) map; } -%include "ltlenv/environment.hh" -%include "ltlenv/defaultenv.hh" +%include "tl/environment.hh" +%include "tl/defaultenv.hh" %include "ltlparse/public.hh" @@ -235,16 +235,16 @@ namespace std { %include "twa/acc.hh" %include "twa/twa.hh" -%include "ltlvisit/apcollect.hh" -%include "ltlvisit/dot.hh" -%include "ltlvisit/nenoform.hh" -%include "ltlvisit/print.hh" -%include "ltlvisit/simplify.hh" -%include "ltlvisit/unabbrev.hh" -%include "ltlvisit/randomltl.hh" -%include "ltlvisit/length.hh" -%include "ltlvisit/remove_x.hh" -%include "ltlvisit/relabel.hh" +%include "tl/apcollect.hh" +%include "tl/dot.hh" +%include "tl/nenoform.hh" +%include "tl/print.hh" +%include "tl/simplify.hh" +%include "tl/unabbrev.hh" +%include "tl/randomltl.hh" +%include "tl/length.hh" +%include "tl/remove_x.hh" +%include "tl/relabel.hh" // Help SWIG with namespace lookups. #define ltl spot::ltl