Commit ae6cd921 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

ltlparse: move in parsetl/, and declare in tl/parse.hh

* src/ltlparse/public.hh: Rename as...
* src/tl/parse.hh: ... this.
* src/ltlparse/: Rename as...
* src/parsetl/: ... this.
* NEWS: Mention the change.
* README, configure.ac, doc/org/tut01.org, doc/org/tut02.org,
doc/org/tut03.org, doc/org/tut10.org, src/Makefile.am,
src/bin/common_finput.cc, src/bin/common_finput.hh, src/bin/ltl2tgta.cc,
src/kripkeparse/kripkeparse.yy, src/parseaut/parseaut.yy,
src/tests/checkpsl.cc, src/tests/checkta.cc,
src/tests/complementation.cc, src/tests/consterm.cc,
src/tests/emptchk.cc, src/tests/equalsf.cc, src/tests/ikwiad.cc,
src/tests/kind.cc, src/tests/length.cc, src/tests/ltlprod.cc,
src/tests/ltlrel.cc, src/tests/randtgba.cc, src/tests/readltl.cc,
src/tests/reduc.cc, src/tests/syntimpl.cc, src/tests/tostring.cc,
src/tl/Makefile.am, src/twaalgos/lbtt.cc, wrap/python/spot_impl.i,
iface/ltsmin/modelcheck.cc: Adjust.
parent 25b01536
......@@ -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.
......
......@@ -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
......@@ -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
......
......@@ -69,7 +69,7 @@ exceptions.
#+BEGIN_SRC C++ :results verbatim :exports both
#include <iostream>
#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 <string>
#include <iostream>
#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 <string>
#include <iostream>
#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 <string>
#include <iostream>
#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 <string>
#include <iostream>
#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 <string>
#include <iostream>
#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 <string>
#include <iostream>
#include "ltlparse/public.hh"
#include "tl/parse.hh"
#include "tl/print.hh"
#include "tl/simplify.hh"
......
......@@ -80,7 +80,7 @@ destructor.
#+BEGIN_SRC C++ :results verbatim :exports both
#include <string>
#include <iostream>
#include "ltlparse/public.hh"
#include "tl/parse.hh"
#include "tl/print.hh"
#include "tl/relabel.hh"
......
......@@ -201,7 +201,7 @@ save time by not exploring further).
#include <iostream>
#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 <iostream>
#include "tl/formula.hh"
#include "tl/print.hh"
#include "ltlparse/public.hh"
#include "tl/parse.hh"
spot::formula xchg_fg(spot::formula in)
{
......
......@@ -129,7 +129,7 @@ never claim is done via the =print_never_claim= function.
#+BEGIN_SRC C++ :results verbatim :exports both
#include <string>
#include <iostream>
#include "ltlparse/public.hh"
#include "tl/parse.hh"
#include "tl/print.hh"
#include "twaalgos/translate.hh"
#include "twaalgos/neverclaim.hh"
......
......@@ -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"
......
......@@ -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 \
......
......@@ -19,7 +19,6 @@
#include "common_finput.hh"
#include "error.h"
#include "ltlparse/public.hh"
#include <fstream>
#include <cstring>
......
......@@ -23,7 +23,7 @@
#include <argp.h>
#include <vector>
#include "ltlparse/public.hh"
#include "tl/parse.hh"
struct job
{
......
......@@ -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"
......
......@@ -54,7 +54,7 @@ typedef std::map<std::string, bdd> formula_cache;
%code
{
#include "kripke/kripkeexplicit.hh"
#include "ltlparse/public.hh"
#include "tl/parse.hh"
#include <map>
/* twaparse.hh and parsedecl.hh include each other recursively.
......
......@@ -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 <sstream>
#include "ltlparse/public.hh"
/* parseaut.hh and parsedecl.hh include each other recursively.
We must ensure that YYSTYPE is declared (by the above %union)
......
## -*- 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
......@@ -20,7 +20,7 @@
// You should have received a copy of the GNU General Public License
// along with this program. If not, see <http://www.gnu.org/licenses/>.
#include "public.hh"
#include "tl/parse.hh"
#include <ostream>
#include <iterator>
#include <vector>
......
// -*- 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);
......
......@@ -23,7 +23,7 @@
%language "C++"
%locations
%defines
%name-prefix "ltlyy"
%name-prefix "tlyy"
%debug
%error-verbose
%expect 0
......@@ -34,7 +34,7 @@
{
#include <string>
#include <sstream>
#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();
......
......@@ -21,7 +21,7 @@
** along with this program. If not, see <http://www.gnu.org/licenses/>.
*/
%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 <cstdlib>
#include <string>
#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;
%}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment