diff --git a/NEWS b/NEWS index 8572a9030..873782594 100644 --- a/NEWS +++ b/NEWS @@ -49,6 +49,9 @@ New in spot 1.99.3a (not yet released) * For similar reasons, the spot::ltl namespace has been merged with the spot namespace. + * The LTL/PSL parser is now declared in tl/parse.hh (instead of + ltlparse/public.hh). + * The dupexp_dfs() function has been renamed to copy(), and as learn to preserve named states if required. diff --git a/README b/README index 447469f7a..2d73b1e22 100644 --- a/README +++ b/README @@ -141,9 +141,9 @@ src/ Sources for libspot. kripke/ Kripke Structure interface. kripkeparse/ Parser for explicit Kripke. tl/ Temporal Logic formulas and algorithms. - ltlparse/ Parser for LTL formulae. misc/ Miscellaneous support files. parseaut/ Parser for automata in multiple formats. + parsetl/ Parser for LTL/PSL formulas. priv/ Private algorithms, used internally but not exported. ta/ TA objects and cousins (TGTA). taalgos/ Algorithms on TA/TGTA. @@ -161,8 +161,8 @@ bench/ Benchmarks for ... dtgbasat/ ... SAT-based minimization of DTGBA, emptchk/ ... emptiness-check algorithms, ltl2tgba/ ... LTL-to-Büchi translation algorithms, - ltlcounter/ ... translation of a class of LTL formulae, - ltlclasses/ ... translation of more classes of LTL formulae, + ltlcounter/ ... translation of a class of LTL formulas, + ltlclasses/ ... translation of more classes of LTL formulas, spin13/ ... compositional suspension and other improvements, wdba/ ... WDBA minimization (for obligation properties). stutter/ ... stutter-invariance checking algorithms @@ -200,6 +200,6 @@ End: LocalWords: gtec Tarjan doc html PDF spotref pdf cgi ELTL LocalWords: CGI ltl iface BDD Couvreur's emptchk kripke Kripke saba vm LocalWords: eltlparse eltltest SABA sabaalgos sabatest ssp ltlcouter scc SCC -LocalWords: formulae optimizations kripkeparse Automata +LocalWords: optimizations kripkeparse Automata LocalWords: neverparse ltlcounter ltlclasses parallelizing automata LocalWords: wdba WDBA ajax dve DiVinE ltdl Libtool's dlopen diff --git a/configure.ac b/configure.ac index 07f15f62f..3ed3b09f9 100644 --- a/configure.ac +++ b/configure.ac @@ -203,10 +203,10 @@ AC_CONFIG_FILES([ src/graph/Makefile src/kripke/Makefile src/kripkeparse/Makefile - src/ltlparse/Makefile src/Makefile src/misc/Makefile src/parseaut/Makefile + src/parsetl/Makefile src/priv/Makefile src/sanity/Makefile src/taalgos/Makefile diff --git a/doc/org/tut01.org b/doc/org/tut01.org index 91c3f849f..8548e16d3 100644 --- a/doc/org/tut01.org +++ b/doc/org/tut01.org @@ -69,7 +69,7 @@ exceptions. #+BEGIN_SRC C++ :results verbatim :exports both #include - #include "ltlparse/public.hh" + #include "tl/parse.hh" #include "tl/print.hh" int main() @@ -110,7 +110,7 @@ Here is how to call the infix parser explicitly: #+BEGIN_SRC C++ :results verbatim :exports both #include #include - #include "ltlparse/public.hh" + #include "tl/parse.hh" #include "tl/print.hh" int main() @@ -152,7 +152,7 @@ with the "fixed" formula if you wish. Here is an example: #+BEGIN_SRC C++ :results verbatim :exports both #include #include - #include "ltlparse/public.hh" + #include "tl/parse.hh" #include "tl/print.hh" int main() @@ -193,7 +193,7 @@ of =parse_infix_psl()=. #+BEGIN_SRC C++ :results verbatim :exports both #include #include - #include "ltlparse/public.hh" + #include "tl/parse.hh" #include "tl/print.hh" int main() @@ -237,7 +237,7 @@ For instance, let's see what happens if a PSL formulas is passed to #+BEGIN_SRC C++ :results verbatim :exports both #include #include - #include "ltlparse/public.hh" + #include "tl/parse.hh" #include "tl/print.hh" int main() @@ -267,7 +267,7 @@ The first is to simply diagnose non-LTL formulas. #+BEGIN_SRC C++ :results verbatim :exports code #include #include - #include "ltlparse/public.hh" + #include "tl/parse.hh" #include "tl/print.hh" int main() @@ -296,7 +296,7 @@ prepared to reject the formula any way. In our example, we are lucky #+BEGIN_SRC C++ :results verbatim :exports both #include #include - #include "ltlparse/public.hh" + #include "tl/parse.hh" #include "tl/print.hh" #include "tl/simplify.hh" diff --git a/doc/org/tut02.org b/doc/org/tut02.org index e87e72c4f..7d280d204 100644 --- a/doc/org/tut02.org +++ b/doc/org/tut02.org @@ -80,7 +80,7 @@ destructor. #+BEGIN_SRC C++ :results verbatim :exports both #include #include - #include "ltlparse/public.hh" + #include "tl/parse.hh" #include "tl/print.hh" #include "tl/relabel.hh" diff --git a/doc/org/tut03.org b/doc/org/tut03.org index f5a385be9..86a23ce60 100644 --- a/doc/org/tut03.org +++ b/doc/org/tut03.org @@ -201,7 +201,7 @@ save time by not exploring further). #include #include "tl/formula.hh" #include "tl/print.hh" - #include "ltlparse/public.hh" + #include "tl/parse.hh" int main() { @@ -249,7 +249,7 @@ in a formula: #include #include "tl/formula.hh" #include "tl/print.hh" - #include "ltlparse/public.hh" + #include "tl/parse.hh" spot::formula xchg_fg(spot::formula in) { diff --git a/doc/org/tut10.org b/doc/org/tut10.org index d01ae5e23..91373ca2e 100644 --- a/doc/org/tut10.org +++ b/doc/org/tut10.org @@ -129,7 +129,7 @@ never claim is done via the =print_never_claim= function. #+BEGIN_SRC C++ :results verbatim :exports both #include #include - #include "ltlparse/public.hh" + #include "tl/parse.hh" #include "tl/print.hh" #include "twaalgos/translate.hh" #include "twaalgos/neverclaim.hh" diff --git a/iface/ltsmin/modelcheck.cc b/iface/ltsmin/modelcheck.cc index 3f6f61946..19e7683fa 100644 --- a/iface/ltsmin/modelcheck.cc +++ b/iface/ltsmin/modelcheck.cc @@ -20,7 +20,7 @@ #include "ltsmin.hh" #include "twaalgos/dot.hh" #include "tl/defaultenv.hh" -#include "ltlparse/public.hh" +#include "tl/parse.hh" #include "twaalgos/translate.hh" #include "twaalgos/emptiness.hh" #include "twaalgos/reducerun.hh" diff --git a/src/Makefile.am b/src/Makefile.am index 8efd0d9c3..18c2ae452 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -25,8 +25,8 @@ 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 tl ltlparse graph twa twaalgos ta taalgos kripke \ - kripkeparse parseaut . bin tests sanity +SUBDIRS = misc priv tl graph twa twaalgos ta taalgos kripke \ + kripkeparse parseaut parsetl . bin tests sanity lib_LTLIBRARIES = libspot.la libspot_la_SOURCES = @@ -34,9 +34,9 @@ libspot_la_LDFLAGS = $(BUDDY_LDFLAGS) -no-undefined libspot_la_LIBADD = \ kripke/libkripke.la \ kripkeparse/libkripkeparse.la \ - ltlparse/libltlparse.la \ misc/libmisc.la \ parseaut/libparseaut.la \ + parsetl/libparsetl.la \ priv/libpriv.la \ taalgos/libtaalgos.la \ ta/libta.la \ diff --git a/src/bin/common_finput.cc b/src/bin/common_finput.cc index 7c602412f..1b328848a 100644 --- a/src/bin/common_finput.cc +++ b/src/bin/common_finput.cc @@ -19,7 +19,6 @@ #include "common_finput.hh" #include "error.h" -#include "ltlparse/public.hh" #include #include diff --git a/src/bin/common_finput.hh b/src/bin/common_finput.hh index 015307384..9ee5f855b 100644 --- a/src/bin/common_finput.hh +++ b/src/bin/common_finput.hh @@ -23,7 +23,7 @@ #include #include -#include "ltlparse/public.hh" +#include "tl/parse.hh" struct job { diff --git a/src/bin/ltl2tgta.cc b/src/bin/ltl2tgta.cc index 6edb9d821..83b5d2f1b 100644 --- a/src/bin/ltl2tgta.cc +++ b/src/bin/ltl2tgta.cc @@ -32,7 +32,7 @@ #include "common_finput.hh" #include "common_post.hh" -#include "ltlparse/public.hh" +#include "tl/parse.hh" #include "tl/print.hh" #include "tl/simplify.hh" #include "twaalgos/dot.hh" diff --git a/src/kripkeparse/kripkeparse.yy b/src/kripkeparse/kripkeparse.yy index 27683befa..53ec57634 100644 --- a/src/kripkeparse/kripkeparse.yy +++ b/src/kripkeparse/kripkeparse.yy @@ -54,7 +54,7 @@ typedef std::map formula_cache; %code { #include "kripke/kripkeexplicit.hh" -#include "ltlparse/public.hh" +#include "tl/parse.hh" #include /* twaparse.hh and parsedecl.hh include each other recursively. diff --git a/src/parseaut/parseaut.yy b/src/parseaut/parseaut.yy index 76bda205e..f8627301f 100644 --- a/src/parseaut/parseaut.yy +++ b/src/parseaut/parseaut.yy @@ -37,7 +37,7 @@ #include "twa/formula2bdd.hh" #include "public.hh" #include "priv/accmap.hh" -#include "ltlparse/public.hh" +#include "tl/parse.hh" inline namespace hoayy_support { @@ -152,7 +152,6 @@ %code { #include -#include "ltlparse/public.hh" /* parseaut.hh and parsedecl.hh include each other recursively. We must ensure that YYSTYPE is declared (by the above %union) diff --git a/src/ltlparse/.gitignore b/src/parsetl/.gitignore similarity index 100% rename from src/ltlparse/.gitignore rename to src/parsetl/.gitignore diff --git a/src/ltlparse/Makefile.am b/src/parsetl/Makefile.am similarity index 60% rename from src/ltlparse/Makefile.am rename to src/parsetl/Makefile.am index c754ed045..4aaeeb97b 100644 --- a/src/ltlparse/Makefile.am +++ b/src/parsetl/Makefile.am @@ -1,6 +1,6 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire -## de Recherche et Développement de l'Epita (LRDE). +## Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015 +## Laboratoire de Recherche et Développement de l'Epita (LRDE). ## Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris ## 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), ## Université Pierre et Marie Curie. @@ -24,37 +24,32 @@ AM_CPPFLAGS = -I$(top_srcdir) -I$(srcdir)/.. -I.. -DYY_NO_INPUT # Disable -Werror because too many versions of flex yield warnings. AM_CXXFLAGS = $(WARNING_CXXFLAGS:-Werror=) -ltlparsedir = $(pkgincludedir)/ltlparse +noinst_LTLIBRARIES = libparsetl.la -noinst_LTLIBRARIES = libltlparse.la - -LTLPARSE_YY = ltlparse.yy -FROM_LTLPARSE_YY_MAIN = ltlparse.cc -FROM_LTLPARSE_YY_OTHERS = \ +PARSETL_YY = parsetl.yy +FROM_PARSETL_YY_MAIN = parsetl.cc +FROM_PARSETL_YY_OTHERS = \ stack.hh \ - ltlparse.hh -FROM_LTLPARSE_YY = $(FROM_LTLPARSE_YY_MAIN) $(FROM_LTLPARSE_YY_OTHERS) + parsetl.hh +FROM_PARSETL_YY = $(FROM_PARSETL_YY_MAIN) $(FROM_PARSETL_YY_OTHERS) -BUILT_SOURCES = $(FROM_LTLPARSE_YY) -MAINTAINERCLEANFILES = $(FROM_LTLPARSE_YY) +BUILT_SOURCES = $(FROM_PARSETL_YY) +MAINTAINERCLEANFILES = $(FROM_PARSETL_YY) -$(FROM_LTLPARSE_YY_MAIN): $(srcdir)/$(LTLPARSE_YY) +$(FROM_PARSETL_YY_MAIN): $(srcdir)/$(PARSETL_YY) ## We must cd into $(srcdir) first because if we tell bison to read -## $(srcdir)/$(LTLPARSE_YY), it will also use the value of $(srcdir)/ +## $(srcdir)/$(PARSETL_YY), it will also use the value of $(srcdir)/ ## in the generated include statements. cd $(srcdir) && \ $(BISON) -Wall -Werror --report=all $(BISON_EXTRA_FLAGS) \ - $(LTLPARSE_YY) -o $(FROM_LTLPARSE_YY_MAIN) -$(FROM_LTLPARSE_YY_OTHERS): $(LTLPARSE_YY) - @test -f $@ || $(MAKE) $(AM_MAKEFLAGS) $(FROM_LTLPARSE_YY_MAIN) + $(PARSETL_YY) -o $(FROM_PARSETL_YY_MAIN) +$(FROM_PARSETL_YY_OTHERS): $(PARSETL_YY) + @test -f $@ || $(MAKE) $(AM_MAKEFLAGS) $(FROM_PARSETL_YY_MAIN) -EXTRA_DIST = $(LTLPARSE_YY) +EXTRA_DIST = $(PARSETL_YY) -libltlparse_la_SOURCES = \ +libparsetl_la_SOURCES = \ fmterror.cc \ - $(FROM_LTLPARSE_YY) \ - ltlscan.ll \ + $(FROM_PARSETL_YY) \ + scantl.ll \ parsedecl.hh - -ltlparse_HEADERS = \ - public.hh diff --git a/src/ltlparse/fmterror.cc b/src/parsetl/fmterror.cc similarity index 99% rename from src/ltlparse/fmterror.cc rename to src/parsetl/fmterror.cc index 6c1c3de9c..874000be9 100644 --- a/src/ltlparse/fmterror.cc +++ b/src/parsetl/fmterror.cc @@ -20,7 +20,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . -#include "public.hh" +#include "tl/parse.hh" #include #include #include diff --git a/src/ltlparse/parsedecl.hh b/src/parsetl/parsedecl.hh similarity index 82% rename from src/ltlparse/parsedecl.hh rename to src/parsetl/parsedecl.hh index 46345ad9d..be3e4ee6a 100644 --- a/src/ltlparse/parsedecl.hh +++ b/src/parsetl/parsedecl.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2012, 2013, 2014 Laboratoire de Recherche et +// Copyright (C) 2010, 2012, 2013, 2014, 2015 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 @@ -22,13 +22,13 @@ #pragma once -#include "ltlparse.hh" +#include "parsetl.hh" #include "misc/location.hh" # define YY_DECL \ - int ltlyylex (ltlyy::parser::semantic_type *yylval, \ - spot::location *yylloc, \ - spot::parse_error_list& error_list) + int tlyylex (tlyy::parser::semantic_type *yylval, \ + spot::location *yylloc, \ + spot::parse_error_list& error_list) YY_DECL; void flex_set_buffer(const std::string& buf, int start_tok, bool lenient); diff --git a/src/ltlparse/ltlparse.yy b/src/parsetl/parsetl.yy similarity index 98% rename from src/ltlparse/ltlparse.yy rename to src/parsetl/parsetl.yy index e54af8351..fdf29bf8d 100644 --- a/src/ltlparse/ltlparse.yy +++ b/src/parsetl/parsetl.yy @@ -23,7 +23,7 @@ %language "C++" %locations %defines -%name-prefix "ltlyy" +%name-prefix "tlyy" %debug %error-verbose %expect 0 @@ -34,7 +34,7 @@ { #include #include -#include "public.hh" +#include "tl/parse.hh" #include "tl/formula.hh" #include "tl/print.hh" @@ -53,7 +53,7 @@ } %code { -/* ltlparse.hh and parsedecl.hh include each other recursively. +/* parsetl.hh and parsedecl.hh include each other recursively. We mut ensure that YYSTYPE is declared (by the above %union) before parsedecl.hh uses it. */ #include "parsedecl.hh" @@ -986,7 +986,7 @@ lbtformula: ATOMIC_PROP %% void -ltlyy::parser::error(const location_type& location, const std::string& message) +tlyy::parser::error(const location_type& location, const std::string& message) { error_list.emplace_back(location, message); } @@ -1001,9 +1001,9 @@ namespace spot { formula result = nullptr; flex_set_buffer(ltl_string, - ltlyy::parser::token::START_LTL, + tlyy::parser::token::START_LTL, lenient); - ltlyy::parser parser(error_list, env, result); + tlyy::parser parser(error_list, env, result); parser.set_debug_level(debug); parser.parse(); flex_unset_buffer(); @@ -1018,9 +1018,9 @@ namespace spot { formula result = nullptr; flex_set_buffer(ltl_string, - ltlyy::parser::token::START_BOOL, + tlyy::parser::token::START_BOOL, lenient); - ltlyy::parser parser(error_list, env, result); + tlyy::parser parser(error_list, env, result); parser.set_debug_level(debug); parser.parse(); flex_unset_buffer(); @@ -1035,9 +1035,9 @@ namespace spot { formula result = nullptr; flex_set_buffer(ltl_string, - ltlyy::parser::token::START_LBT, + tlyy::parser::token::START_LBT, false); - ltlyy::parser parser(error_list, env, result); + tlyy::parser parser(error_list, env, result); parser.set_debug_level(debug); parser.parse(); flex_unset_buffer(); @@ -1053,9 +1053,9 @@ namespace spot { formula result = nullptr; flex_set_buffer(sere_string, - ltlyy::parser::token::START_SERE, + tlyy::parser::token::START_SERE, lenient); - ltlyy::parser parser(error_list, env, result); + tlyy::parser parser(error_list, env, result); parser.set_debug_level(debug); parser.parse(); flex_unset_buffer(); diff --git a/src/ltlparse/ltlscan.ll b/src/parsetl/scantl.ll similarity index 99% rename from src/ltlparse/ltlscan.ll rename to src/parsetl/scantl.ll index f207009f7..c762162ad 100644 --- a/src/ltlparse/ltlscan.ll +++ b/src/parsetl/scantl.ll @@ -21,7 +21,7 @@ ** along with this program. If not, see . */ %option noyywrap warn 8bit batch -%option prefix="ltlyy" +%option prefix="tlyy" %option outfile="lex.yy.c" %option stack %option never-interactive @@ -30,7 +30,7 @@ #include #include -#include "ltlparse/parsedecl.hh" +#include "parsedecl.hh" #include "misc/escape.hh" #define YY_USER_ACTION \ @@ -43,7 +43,7 @@ static bool lenient_mode = false; static int orig_cond = 0; static unsigned comment_level = 0; -typedef ltlyy::parser::token token; +typedef tlyy::parser::token token; %} diff --git a/src/tests/checkpsl.cc b/src/tests/checkpsl.cc index bdbd5195b..ac4350a16 100644 --- a/src/tests/checkpsl.cc +++ b/src/tests/checkpsl.cc @@ -22,7 +22,7 @@ #include #include #include -#include "ltlparse/public.hh" +#include "tl/parse.hh" #include "twaalgos/ltl2tgba_fm.hh" #include "twaalgos/ltl2taa.hh" #include "twaalgos/sccfilter.hh" diff --git a/src/tests/checkta.cc b/src/tests/checkta.cc index 8e3eabe73..cf912bf6d 100644 --- a/src/tests/checkta.cc +++ b/src/tests/checkta.cc @@ -23,7 +23,7 @@ #include #include #include -#include "ltlparse/public.hh" +#include "tl/parse.hh" #include "twaalgos/ltl2tgba_fm.hh" #include "twaalgos/sccfilter.hh" #include "twaalgos/degen.hh" diff --git a/src/tests/complementation.cc b/src/tests/complementation.cc index 63a3e0e5c..ef051dea0 100644 --- a/src/tests/complementation.cc +++ b/src/tests/complementation.cc @@ -25,7 +25,7 @@ #include "twa/twaproduct.hh" #include "twaalgos/gtec/gtec.hh" #include "twaalgos/ltl2tgba_fm.hh" -#include "ltlparse/public.hh" +#include "tl/parse.hh" #include "twaalgos/stats.hh" #include "twaalgos/emptiness.hh" #include "twaalgos/stats.hh" diff --git a/src/tests/consterm.cc b/src/tests/consterm.cc index 6ffb3ff3e..fdc666657 100644 --- a/src/tests/consterm.cc +++ b/src/tests/consterm.cc @@ -22,7 +22,7 @@ #include #include #include -#include "ltlparse/public.hh" +#include "tl/parse.hh" void syntax(char *prog) diff --git a/src/tests/emptchk.cc b/src/tests/emptchk.cc index c39aa9893..8d55c843a 100644 --- a/src/tests/emptchk.cc +++ b/src/tests/emptchk.cc @@ -22,7 +22,7 @@ #include #include #include -#include "ltlparse/public.hh" +#include "tl/parse.hh" #include "twaalgos/ltl2tgba_fm.hh" #include "twaalgos/ltl2taa.hh" #include "twaalgos/sccfilter.hh" diff --git a/src/tests/equalsf.cc b/src/tests/equalsf.cc index 5eefee0d7..e5878de3f 100644 --- a/src/tests/equalsf.cc +++ b/src/tests/equalsf.cc @@ -26,7 +26,7 @@ #include #include #include -#include "ltlparse/public.hh" +#include "tl/parse.hh" #include "tl/unabbrev.hh" #include "tl/nenoform.hh" #include "tl/simplify.hh" diff --git a/src/tests/ikwiad.cc b/src/tests/ikwiad.cc index 4a85b44ed..982992f7b 100644 --- a/src/tests/ikwiad.cc +++ b/src/tests/ikwiad.cc @@ -29,7 +29,7 @@ #include "tl/print.hh" #include "tl/apcollect.hh" #include "tl/formula.hh" -#include "ltlparse/public.hh" +#include "tl/parse.hh" #include "twaalgos/ltl2tgba_fm.hh" #include "twaalgos/ltl2taa.hh" #include "twa/bddprint.hh" diff --git a/src/tests/kind.cc b/src/tests/kind.cc index 16f411284..d0eef6ab2 100644 --- a/src/tests/kind.cc +++ b/src/tests/kind.cc @@ -22,7 +22,7 @@ #include #include #include -#include "ltlparse/public.hh" +#include "tl/parse.hh" void syntax(char *prog) diff --git a/src/tests/length.cc b/src/tests/length.cc index a752d9e8b..28d438eb0 100644 --- a/src/tests/length.cc +++ b/src/tests/length.cc @@ -21,7 +21,7 @@ #include #include #include -#include "ltlparse/public.hh" +#include "tl/parse.hh" #include "tl/length.hh" void diff --git a/src/tests/ltlprod.cc b/src/tests/ltlprod.cc index 830bbef7f..bdeaaf60d 100644 --- a/src/tests/ltlprod.cc +++ b/src/tests/ltlprod.cc @@ -23,7 +23,7 @@ #include #include #include -#include "ltlparse/public.hh" +#include "tl/parse.hh" #include "twaalgos/product.hh" #include "twaalgos/ltl2tgba_fm.hh" #include "twaalgos/dot.hh" diff --git a/src/tests/ltlrel.cc b/src/tests/ltlrel.cc index 3f8e732c5..dc5c8a1b5 100644 --- a/src/tests/ltlrel.cc +++ b/src/tests/ltlrel.cc @@ -20,7 +20,7 @@ #include #include #include -#include "ltlparse/public.hh" +#include "tl/parse.hh" #include "tl/relabel.hh" #include "tl/print.hh" diff --git a/src/tests/randtgba.cc b/src/tests/randtgba.cc index d8406e1da..613d96fe9 100644 --- a/src/tests/randtgba.cc +++ b/src/tests/randtgba.cc @@ -30,7 +30,7 @@ #include #include #include -#include "ltlparse/public.hh" +#include "tl/parse.hh" #include "tl/apcollect.hh" #include "tl/randomltl.hh" #include "tl/print.hh" diff --git a/src/tests/readltl.cc b/src/tests/readltl.cc index f65599ce8..cfabb0bea 100644 --- a/src/tests/readltl.cc +++ b/src/tests/readltl.cc @@ -24,7 +24,7 @@ #include #include #include -#include "ltlparse/public.hh" +#include "tl/parse.hh" #include "tl/dot.hh" void diff --git a/src/tests/reduc.cc b/src/tests/reduc.cc index 2de7cdd9f..be847d674 100644 --- a/src/tests/reduc.cc +++ b/src/tests/reduc.cc @@ -26,7 +26,7 @@ #include #include #include -#include "ltlparse/public.hh" +#include "tl/parse.hh" #include "tl/print.hh" #include "tl/simplify.hh" #include "tl/length.hh" diff --git a/src/tests/syntimpl.cc b/src/tests/syntimpl.cc index 328883740..52d49cac7 100644 --- a/src/tests/syntimpl.cc +++ b/src/tests/syntimpl.cc @@ -23,7 +23,7 @@ #include #include #include -#include "ltlparse/public.hh" +#include "tl/parse.hh" #include "tl/print.hh" #include "tl/simplify.hh" #include "tl/nenoform.hh" diff --git a/src/tests/tostring.cc b/src/tests/tostring.cc index 60193473e..2c56dadb6 100644 --- a/src/tests/tostring.cc +++ b/src/tests/tostring.cc @@ -23,7 +23,7 @@ #include #include #include -#include "ltlparse/public.hh" +#include "tl/parse.hh" #include "tl/print.hh" void diff --git a/src/tl/Makefile.am b/src/tl/Makefile.am index c7ae7adcc..f1c6da577 100644 --- a/src/tl/Makefile.am +++ b/src/tl/Makefile.am @@ -34,6 +34,7 @@ tl_HEADERS = \ length.hh \ mutation.hh \ nenoform.hh \ + parse.hh \ print.hh \ randomltl.hh \ relabel.hh \ diff --git a/src/ltlparse/public.hh b/src/tl/parse.hh similarity index 100% rename from src/ltlparse/public.hh rename to src/tl/parse.hh diff --git a/src/twaalgos/lbtt.cc b/src/twaalgos/lbtt.cc index d07dc2290..8f1f7904e 100644 --- a/src/twaalgos/lbtt.cc +++ b/src/twaalgos/lbtt.cc @@ -29,7 +29,6 @@ #include "misc/bddlt.hh" #include "priv/accmap.hh" #include "tl/print.hh" -#include "ltlparse/public.hh" namespace spot { diff --git a/wrap/python/spot_impl.i b/wrap/python/spot_impl.i index 890aee1d8..459de7b1c 100644 --- a/wrap/python/spot_impl.i +++ b/wrap/python/spot_impl.i @@ -85,7 +85,7 @@ #include "tl/environment.hh" #include "tl/defaultenv.hh" -#include "ltlparse/public.hh" +#include "tl/parse.hh" #include "twa/bdddict.hh" @@ -222,7 +222,7 @@ namespace std { %include "tl/environment.hh" %include "tl/defaultenv.hh" -%include "ltlparse/public.hh" +%include "tl/parse.hh" /* these must come before apcollect.hh */ %include "twa/bdddict.hh"