diff --git a/README b/README
index 73e549914..abf4c3466 100644
--- a/README
+++ b/README
@@ -146,8 +146,6 @@ src/ Sources for libspot.
bin/ User tools built using the Spot library.
man/ Man pages for the above tools.
dstarparse/ Parser for the output of ltl2dstar.
- eltlparse/ Parser for ELTL formulae.
- eltltest/ Tests for ELTL nodes in ltlast/ and eltlparse/.
graph/ Graph representations.
graphtest/ Graph representations.
kripke/ Kripke Structure interface.
diff --git a/configure.ac b/configure.ac
index 9410b3fac..ab45c12be 100644
--- a/configure.ac
+++ b/configure.ac
@@ -177,9 +177,6 @@ AC_CONFIG_FILES([
src/bin/Makefile
src/bin/man/Makefile
src/dstarparse/Makefile
- src/eltlparse/Makefile
- src/eltltest/defs
- src/eltltest/Makefile
src/kripke/Makefile
src/graph/Makefile
src/graphtest/Makefile
diff --git a/src/Makefile.am b/src/Makefile.am
index 5a2302b22..8b19c1a5d 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -25,17 +25,16 @@ 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 eltlparse graph \
- tgba tgbaalgos tgbaparse ta taalgos kripke saba sabaalgos \
- neverparse kripkeparse dstarparse . bin ltltest eltltest \
- graphtest tgbatest sabatest kripketest sanity
+SUBDIRS = misc priv ltlenv ltlast ltlvisit ltlparse graph tgba \
+ tgbaalgos tgbaparse ta taalgos kripke saba sabaalgos \
+ neverparse kripkeparse dstarparse . bin ltltest graphtest \
+ tgbatest sabatest kripketest sanity
lib_LTLIBRARIES = libspot.la
libspot_la_SOURCES =
libspot_la_LDFLAGS = $(BUDDY_LDFLAGS) -no-undefined
libspot_la_LIBADD = \
dstarparse/libdstarparse.la \
- eltlparse/libeltlparse.la \
kripke/libkripke.la \
kripkeparse/libkripkeparse.la \
ltlast/libltlast.la \
diff --git a/src/eltlparse/.gitignore b/src/eltlparse/.gitignore
deleted file mode 100644
index 9f03c8c07..000000000
--- a/src/eltlparse/.gitignore
+++ /dev/null
@@ -1,7 +0,0 @@
-eltlparse.cc
-eltlparse.hh
-*.output
-eltlscan.cc
-location.hh
-position.hh
-stack.hh
diff --git a/src/eltlparse/Makefile.am b/src/eltlparse/Makefile.am
deleted file mode 100644
index 0d0fb0d4a..000000000
--- a/src/eltlparse/Makefile.am
+++ /dev/null
@@ -1,57 +0,0 @@
-## -*- coding: utf-8 -*-
-## Copyright (C) 2008, 2011, 2013 Laboratoire de Recherche et
-## Développement de l'Epita (LRDE).
-##
-## This file is part of Spot, a model checking library.
-##
-## Spot is free software; you can redistribute it and/or modify it
-## under the terms of the GNU General Public License as published by
-## the Free Software Foundation; either version 3 of the License, or
-## (at your option) any later version.
-##
-## Spot is distributed in the hope that it will be useful, but WITHOUT
-## ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
-## or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
-## License for more details.
-##
-## You should have received a copy of the GNU General Public License
-## along with this program. If not, see .
-
-AM_CPPFLAGS = -I$(srcdir)/.. -I.. -DYY_NO_INPUT
-# Disable -Werror because too many versions of flex yield warnings.
-AM_CXXFLAGS = $(WARNING_CXXFLAGS:-Werror=)
-
-eltlparsedir = $(pkgincludedir)/eltlparse
-
-noinst_LTLIBRARIES = libeltlparse.la
-
-ELTLPARSE_YY = eltlparse.yy
-FROM_ELTLPARSE_YY_MAIN = eltlparse.cc
-FROM_ELTLPARSE_YY_OTHERS = \
- stack.hh \
- eltlparse.hh
-FROM_ELTLPARSE_YY = $(FROM_ELTLPARSE_YY_MAIN) $(FROM_ELTLPARSE_YY_OTHERS)
-
-BUILT_SOURCES = $(FROM_ELTLPARSE_YY)
-MAINTAINERCLEANFILES = $(FROM_ELTLPARSE_YY)
-
-$(FROM_ELTLPARSE_YY_MAIN): $(srcdir)/$(ELTLPARSE_YY)
-## We must cd into $(srcdir) first because if we tell bison to read
-## $(srcdir)/$(ELTLPARSE_YY), it will also use the value of $(srcdir)/
-## in the generated include statements.
- cd $(srcdir) && \
- $(BISON) -Wall -Werror --report=all $(BISON_EXTRA_FLAGS) \
- $(ELTLPARSE_YY) -o $(FROM_ELTLPARSE_YY_MAIN)
-$(FROM_ELTLPARSE_YY_OTHERS): $(ELTLPARSE_YY)
- @test -f $@ || $(MAKE) $(AM_MAKEFLAGS) $(FROM_ELTLPARSE_YY_MAIN)
-
-EXTRA_DIST = $(ELTLPARSE_YY)
-
-libeltlparse_la_SOURCES = \
- fmterror.cc \
- $(FROM_ELTLPARSE_YY) \
- eltlscan.ll \
- parsedecl.hh
-
-eltlparse_HEADERS = public.hh
-
diff --git a/src/eltlparse/eltlparse.yy b/src/eltlparse/eltlparse.yy
deleted file mode 100644
index 3ebde0e33..000000000
--- a/src/eltlparse/eltlparse.yy
+++ /dev/null
@@ -1,568 +0,0 @@
-/* -*- coding: utf-8 -*-
-** Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014 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 .
-*/
-%language "C++"
-%locations
-%defines
-%name-prefix "eltlyy"
-%debug
-%error-verbose
-%define api.location.type "spot::location"
-
-%code requires
-{
-#include
-#include
-#include
-#include
-#include
-#include "public.hh"
-#include "ltlast/allnodes.hh"
-#include "ltlast/formula_tree.hh"
-
-namespace spot
-{
- namespace eltl
- {
- typedef std::map nfamap;
-
- /// The following parser allows one to define aliases of automaton
- /// operators such as: F=U(true,$0). Internally it's handled by
- /// creating a small AST associated with each alias in order to
- /// instanciate the right automatop after: U(constant(1), AP(f))
- /// for the formula F(f).
- typedef std::map aliasmap;
-
- /// Implementation details for error handling.
- struct parse_error_list_t
- {
- parse_error_list list_;
- std::string file_;
- };
- }
-}
-}
-
-%parse-param {spot::eltl::nfamap& nmap}
-%parse-param {spot::eltl::aliasmap& amap}
-%parse-param {spot::eltl::parse_error_list_t &pe}
-%parse-param {spot::ltl::environment &parse_environment}
-%parse-param {const spot::ltl::formula* &result}
-%lex-param {spot::eltl::parse_error_list_t &pe}
-%expect 0
-
-%union
-{
- int ival;
- std::string* sval;
- spot::ltl::nfa* nval;
- spot::ltl::automatop::vec* aval;
- const spot::ltl::formula* fval;
-
- /// To handle aliases.
- spot::ltl::formula_tree::node* pval;
- spot::ltl::formula_tree::node_nfa* bval;
-}
-
-%code {
-/* ltlparse.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"
-using namespace spot::eltl;
-using namespace spot::ltl;
-
-namespace spot
-{
- namespace eltl
- {
- using namespace spot::ltl::formula_tree;
-
- /// Alias an existing alias, as in Strong=G(F($0))->G(F($1)),
- /// where F is an alias.
- ///
- /// \param ap The original alias.
- /// \param v The arguments of the new alias.
- static node_ptr
- realias(const node_ptr ap, std::vector v)
- {
- if (node_atomic* a = dynamic_cast(ap.get())) // Do it.
- return a->i < 0 ? ap : v.at(a->i);
-
- // Traverse the tree.
- if (node_unop* a = dynamic_cast(ap.get()))
- {
- node_unop* res = new node_unop;
- res->op = a->op;
- res->child = realias(a->child, v);
- return node_ptr(res);
- }
- if (node_nfa* a = dynamic_cast(ap.get()))
- {
- node_nfa* res = new node_nfa;
- std::vector::const_iterator i = a->children.begin();
- while (i != a->children.end())
- res->children.push_back(realias(*i++, v));
- res->nfa = a->nfa;
- return node_ptr(res);
- }
- if (node_binop* a = dynamic_cast(ap.get()))
- {
- node_binop* res = new node_binop;
- res->op = a->op;
- res->lhs = realias(a->lhs, v);
- res->rhs = realias(a->rhs, v);
- return node_ptr(res);
- }
- if (node_multop* a = dynamic_cast(ap.get()))
- {
- node_multop* res = new node_multop;
- res->op = a->op;
- res->lhs = realias(a->lhs, v);
- res->rhs = realias(a->rhs, v);
- return node_ptr(res);
- }
- SPOT_UNREACHABLE();
- }
- }
-}
-
-#define PARSE_ERROR(Loc, Msg) \
- pe.list_.push_back \
- (parse_error(Loc, spair(pe.file_, Msg)))
-
-#define CHECK_EXISTING_NMAP(Loc, Ident) \
- { \
- nfamap::const_iterator i = nmap.find(*Ident); \
- if (i == nmap.end()) \
- { \
- std::string s = "unknown automaton operator `"; \
- s += *Ident; \
- s += "'"; \
- PARSE_ERROR(Loc, s); \
- delete Ident; \
- YYERROR; \
- } \
- }
-
-#define CHECK_ARITY(Loc, Ident, A1, A2) \
- { \
- if (A1 != A2) \
- { \
- std::ostringstream oss1; \
- oss1 << A1; \
- std::ostringstream oss2; \
- oss2 << A2; \
- \
- std::string s(*Ident); \
- s += " is used with "; \
- s += oss1.str(); \
- s += " arguments, but has an arity of "; \
- s += oss2.str(); \
- PARSE_ERROR(Loc, s); \
- delete Ident; \
- YYERROR; \
- } \
- }
-
-#define INSTANCIATE_OP(Name, TypeNode, TypeOp, L, R) \
- { \
- TypeNode* res = new TypeNode; \
- res->op = TypeOp; \
- res->lhs = formula_tree::node_ptr(L); \
- res->rhs = formula_tree::node_ptr(R); \
- Name = res; \
- }
-
-}
-
-/* All tokens. */
-
-%token ATOMIC_PROP "atomic proposition"
- IDENT "identifier"
-
-%token ARG "argument"
- STATE "state"
- OP_OR "or operator"
- OP_XOR "xor operator"
- OP_AND "and operator"
- OP_IMPLIES "implication operator"
- OP_EQUIV "equivalent operator"
- OP_NOT "not operator"
-
-%token ACC "accept"
- EQ "="
- FIN "finish"
- LPAREN "("
- RPAREN ")"
- COMMA ","
- END_OF_FILE "end of file"
- CONST_TRUE "constant true"
- CONST_FALSE "constant false"
-
-/* Priorities. */
-
-%left OP_OR
-%left OP_XOR
-%left OP_AND
-%left OP_IMPLIES OP_EQUIV
-
-%left ATOMIC_PROP
-
-%nonassoc OP_NOT
-
-%type nfa_def
-%type subformula
-%type arg_list
-%type nfa_arg
-%type nfa_arg_list
-
-%destructor { delete $$; }
-%destructor { $$->destroy(); }
-
-%printer { debug_stream() << *$$; }
-
-%%
-
-result: nfa_list subformula
- {
- result = $2;
- YYACCEPT;
- }
-;
-
-/* NFA definitions. */
-
-nfa_list: /* empty */
- | nfa_list nfa
-;
-
-nfa: IDENT "=" "(" nfa_def ")"
- {
- $4->set_name(*$1);
- nmap[*$1] = nfa::ptr($4);
- delete $1;
- }
- | IDENT "=" nfa_arg
- {
- /// Recursivity issues of aliases are handled by a parse error.
- aliasmap::iterator i = amap.find(*$1);
- if (i != amap.end())
- {
- std::string s = "`";
- s += *$1;
- s += "' is already aliased";
- PARSE_ERROR(@1, s);
- delete $1;
- YYERROR;
- }
- amap.insert(make_pair(*$1, formula_tree::node_ptr($3)));
- delete $1;
- }
-;
-
-nfa_def: /* empty */
- {
- $$ = new nfa;
- }
- | nfa_def STATE STATE nfa_arg
- {
- $1->add_transition($2, $3, formula_tree::node_ptr($4));
- $$ = $1;
- }
- | nfa_def ACC STATE
- {
- $1->set_final($3);
- $$ = $1;
- }
-;
-
-nfa_arg_list: nfa_arg
- {
- $$ = new formula_tree::node_nfa;
- $$->children.push_back(formula_tree::node_ptr($1));
- }
- | nfa_arg_list "," nfa_arg
- {
- $1->children.push_back(formula_tree::node_ptr($3));
- $$ = $1;
- }
-;
-
-nfa_arg: ARG
- {
- if ($1 == -1)
- {
- std::string s = "out of range integer";
- PARSE_ERROR(@1, s);
- YYERROR;
- }
- formula_tree::node_atomic* res = new formula_tree::node_atomic;
- res->i = $1;
- $$ = res;
- }
- | CONST_TRUE
- {
- formula_tree::node_atomic* res = new formula_tree::node_atomic;
- res->i = formula_tree::True;
- $$ = res;
- }
- | CONST_FALSE
- {
- formula_tree::node_atomic* res = new formula_tree::node_atomic;
- res->i = formula_tree::False;
- $$ = res;
- }
- | OP_NOT nfa_arg
- {
- formula_tree::node_unop* res = new formula_tree::node_unop;
- res->op = unop::Not;
- res->child = formula_tree::node_ptr($2);
- $$ = res;
- }
- | FIN "(" nfa_arg ")"
- {
- formula_tree::node_unop* res = new formula_tree::node_unop;
- res->op = unop::Finish;
- res->child = formula_tree::node_ptr($3);
- $$ = res;
- }
- | nfa_arg OP_AND nfa_arg
- {
- INSTANCIATE_OP($$, formula_tree::node_multop, multop::And, $1, $3);
- }
- | nfa_arg OP_OR nfa_arg
- {
- INSTANCIATE_OP($$, formula_tree::node_multop, multop::Or, $1, $3);
- }
- | nfa_arg OP_XOR nfa_arg
- {
- INSTANCIATE_OP($$, formula_tree::node_binop, binop::Xor, $1, $3);
- }
- | nfa_arg OP_IMPLIES nfa_arg
- {
- INSTANCIATE_OP($$, formula_tree::node_binop, binop::Implies, $1, $3);
- }
- | nfa_arg OP_EQUIV nfa_arg
- {
- INSTANCIATE_OP($$, formula_tree::node_binop, binop::Equiv, $1, $3);
- }
- | IDENT "(" nfa_arg_list ")"
- {
- aliasmap::const_iterator i = amap.find(*$1);
- if (i != amap.end())
- {
- unsigned arity = formula_tree::arity(i->second);
- CHECK_ARITY(@1, $1, $3->children.size(), arity);
-
- // Hack to return the right type without screwing with the
- // std::shared_ptr memory handling by using get for
- // example. FIXME: modify the %union to handle
- // formula_tree::node_ptr.
- formula_tree::node_unop* tmp1 = new formula_tree::node_unop;
- tmp1->op = unop::Not;
- tmp1->child = realias(i->second, $3->children);
- formula_tree::node_unop* tmp2 = new formula_tree::node_unop;
- tmp2->op = unop::Not;
- tmp2->child = formula_tree::node_ptr(tmp1);
- $$ = tmp2;
- delete $3;
- }
- else
- {
- CHECK_EXISTING_NMAP(@1, $1);
- nfa::ptr np = nmap[*$1];
-
- CHECK_ARITY(@1, $1, $3->children.size(), np->arity());
- $3->nfa = np;
- $$ = $3;
- }
- delete $1;
- }
-
-/* Formulae. */
-
-subformula: ATOMIC_PROP
- {
- $$ = parse_environment.require(*$1);
- if (!$$)
- {
- std::string s = "unknown atomic proposition `";
- s += *$1;
- s += "' in environment `";
- s += parse_environment.name();
- s += "'";
- PARSE_ERROR(@1, s);
- delete $1;
- YYERROR;
- }
- else
- delete $1;
- }
- | subformula ATOMIC_PROP subformula
- {
- aliasmap::iterator i = amap.find(*$2);
- if (i != amap.end())
- {
- CHECK_ARITY(@1, $2, 2, formula_tree::arity(i->second));
- automatop::vec v;
- v.push_back($1);
- v.push_back($3);
- $$ = instanciate(i->second, v);
- $1->destroy();
- $3->destroy();
- }
- else
- {
- CHECK_EXISTING_NMAP(@1, $2);
- nfa::ptr np = nmap[*$2];
- CHECK_ARITY(@1, $2, 2, np->arity());
- automatop::vec* v = new automatop::vec;
- v->push_back($1);
- v->push_back($3);
- $$ = automatop::instance(np, v, false);
- }
- delete $2;
- }
- | ATOMIC_PROP "(" arg_list ")"
- {
- aliasmap::iterator i = amap.find(*$1);
- if (i != amap.end())
- {
- CHECK_ARITY(@1, $1, $3->size(), formula_tree::arity(i->second));
- $$ = instanciate(i->second, *$3);
- automatop::vec::iterator it = $3->begin();
- while (it != $3->end())
- (*it++)->destroy();
- delete $3;
- }
- else
- {
- CHECK_EXISTING_NMAP(@1, $1);
- nfa::ptr np = nmap[*$1];
-
- /// Easily handle deletion of $3 when CHECK_ARITY fails.
- unsigned i = $3->size();
- if ($3->size() != np->arity())
- {
- automatop::vec::iterator it = $3->begin();
- while (it != $3->end())
- (*it++)->destroy();
- delete $3;
- }
-
- CHECK_ARITY(@1, $1, i, np->arity());
- $$ = automatop::instance(np, $3, false);
- }
- delete $1;
- }
- | CONST_TRUE
- { $$ = constant::true_instance(); }
- | CONST_FALSE
- { $$ = constant::false_instance(); }
- | "(" subformula ")"
- { $$ = $2; }
- | subformula OP_AND subformula
- { $$ = multop::instance(multop::And, $1, $3); }
- | subformula OP_OR subformula
- { $$ = multop::instance(multop::Or, $1, $3); }
- | subformula OP_XOR subformula
- { $$ = binop::instance(binop::Xor, $1, $3); }
- | subformula OP_IMPLIES subformula
- { $$ = binop::instance(binop::Implies, $1, $3); }
- | subformula OP_EQUIV subformula
- { $$ = binop::instance(binop::Equiv, $1, $3); }
- | OP_NOT subformula
- { $$ = unop::instance(unop::Not, $2); }
-;
-
-arg_list: subformula
- {
- $$ = new automatop::vec;
- $$->push_back($1);
- }
- | arg_list "," subformula
- {
- $1->push_back($3);
- $$ = $1;
- }
-;
-
-%%
-
-void
-eltlyy::parser::error(const location_type& loc, const std::string& s)
-{
- PARSE_ERROR(loc, s);
-}
-
-namespace spot
-{
- namespace eltl
- {
- const formula*
- parse_file(const std::string& name,
- parse_error_list& error_list,
- environment& env,
- bool debug)
- {
- if (flex_open(name))
- {
- error_list.push_back
- (parse_error(spot::location(),
- spair("-", std::string("Cannot open file ") + name)));
- return 0;
- }
- const formula* result = 0;
- nfamap nmap;
- aliasmap amap;
- parse_error_list_t pe;
- pe.file_ = name;
- eltlyy::parser parser(nmap, amap, pe, env, result);
- parser.set_debug_level(debug);
- parser.parse();
- error_list = pe.list_;
- flex_close();
- return result;
- }
-
- const formula*
- parse_string(const std::string& eltl_string,
- parse_error_list& error_list,
- environment& env,
- bool debug)
- {
- flex_set_buffer(eltl_string);
- const formula* result = 0;
- nfamap nmap;
- aliasmap amap;
- parse_error_list_t pe;
- eltlyy::parser parser(nmap, amap, pe, env, result);
- parser.set_debug_level(debug);
- parser.parse();
- error_list = pe.list_;
- flex_unset_buffer();
- return result;
- }
- }
-}
-
-// Local Variables:
-// mode: c++
-// End:
diff --git a/src/eltlparse/eltlscan.ll b/src/eltlparse/eltlscan.ll
deleted file mode 100644
index 97c0fba2a..000000000
--- a/src/eltlparse/eltlscan.ll
+++ /dev/null
@@ -1,221 +0,0 @@
-/* -*- coding: utf-8 -*-
-** Copyright (C) 2008, 2014 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 .
-*/
-%option noyywrap
-%option prefix="eltlyy"
-%option outfile="lex.yy.c"
-%option stack
-
-%{
-#include
-#include
-#include "eltlparse/parsedecl.hh"
-
-static int _atoi (char* yytext, int base);
-
-#define YY_USER_ACTION \
- yylloc->columns(yyleng);
-
-// Flex uses `0' for end of file. 0 is not a token_type.
-#define yyterminate() return token::END_OF_FILE
-
-// Stack for handling include files.
-typedef std::pair state;
-std::stack include;
-
-#define ERROR(Msg) \
- pe.list_.push_back \
- (spot::eltl::parse_error(*yylloc, spot::eltl::spair(pe.file_, Msg)))
-
-typedef eltlyy::parser::token token;
-
-%}
-
-eol \n|\r|\n\r|\r\n
-%s formula
-%x incl
-
-%%
-
-%{
- yylloc->step();
-%}
-
- /* Rules for the include part. */
-
-[ \t]*
-[^ \t\n]+ {
- FILE* tmp = fopen(yytext, "r");
- if (!tmp)
- ERROR(std::string("cannot open file ") + yytext);
- else
- {
- include.push(make_pair(YY_CURRENT_BUFFER, pe.file_));
- pe.file_ = std::string(yytext);
- yy_switch_to_buffer(yy_create_buffer(tmp, YY_BUF_SIZE));
- }
- BEGIN(INITIAL);
- }
-
- /* Global rules (1). */
-
-"(" return token::LPAREN;
-"," return token::COMMA;
-")" return token::RPAREN;
-"!" return token::OP_NOT;
-
- /* & and | come from Spin. && and || from LTL2BA.
- /\, \/, and xor are from LBTT.
- */
-"||"|"|"|"+"|"\\/" {
- return token::OP_OR;
- }
-"&&"|"&"|"."|"*"|"/\\" {
- return token::OP_AND;
- }
-"^"|"xor" return token::OP_XOR;
-"=>"|"->" return token::OP_IMPLIES;
-"<=>"|"<->" return token::OP_EQUIV;
-
- /* Rules for the automaton definitions part. */
-
-"include" BEGIN(incl);
-"%" BEGIN(formula);
-
-"=" return token::EQ;
-"accept" return token::ACC;
-"finish" return token::FIN;
-
-[tT][rR][uU][eE] {
- return token::CONST_TRUE;
- }
-[fF][aA][lL][sS][eE] {
- return token::CONST_FALSE;
- }
-
-[a-zA-Z][a-zA-Z0-9_]* {
- yylval->sval = new std::string(yytext, yyleng);
- return token::IDENT;
- }
-
-[0-9]+ {
- // Out of range is checked in the parser.
- yylval->ival = _atoi(yytext, 10);
- return token::STATE;
- }
-
-$[0-9]+ {
- // Out of range is checked in the parser.
- yylval->ival = _atoi(++yytext, 10);
- return token::ARG;
- }
-
-<> {
- if (include.empty())
- yyterminate();
-
- state s = include.top();
- include.pop();
- pe.file_ = s.second;
- yy_delete_buffer(YY_CURRENT_BUFFER);
- yy_switch_to_buffer(s.first);
- }
-
- /* Rules for the formula part. */
-
-"1"|[tT][rR][uU][eE] {
- return token::CONST_TRUE;
- }
-"0"|[fF][aA][lL][sS][eE] {
- return token::CONST_FALSE;
- }
-
-[a-zA-Z][a-zA-Z0-9_]* {
- yylval->sval = new std::string(yytext, yyleng);
- return token::ATOMIC_PROP;
- }
-
- /* Global rules (2). */
-
- /* discard whitespace */
-{eol} yylloc->lines(yyleng); yylloc->step();
-[ \t]+ yylloc->step();
-
-. return *yytext;
-
-
-%{
- /* Dummy use of yyunput to shut up a gcc warning. */
- (void) &yyunput;
-%}
-
-%%
-
-namespace spot
-{
- namespace eltl
- {
- int
- flex_open(const std::string &name)
- {
- if (name == "-")
- yyin = stdin;
- else
- {
- yyin = fopen(name.c_str(), "r");
- if (!yyin)
- return 1;
- }
- return 0;
- }
-
- void
- flex_close()
- {
- fclose(yyin);
- }
-
- void
- flex_set_buffer(const std::string& buf)
- {
- yypush_buffer_state(YY_CURRENT_BUFFER);
- (void) yy_scan_bytes(buf.c_str(), buf.size());
- yy_push_state(0);
- }
-
- void
- flex_unset_buffer()
- {
- (void)&yy_top_state; // shut up a g++ warning.
- yy_pop_state();
- yypop_buffer_state();
- }
- }
-}
-
-static int
-_atoi(char* yytext, int base)
-{
- errno = 0;
- long i = strtol(yytext, 0, base);
- if (i > std::numeric_limits::max() ||
- i < std::numeric_limits::min() || errno == ERANGE)
- return -1;
- return i;
-}
diff --git a/src/eltlparse/fmterror.cc b/src/eltlparse/fmterror.cc
deleted file mode 100644
index 814b8db5a..000000000
--- a/src/eltlparse/fmterror.cc
+++ /dev/null
@@ -1,45 +0,0 @@
-// Copyright (C) 2008 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 .
-
-#include
-#include "public.hh"
-
-namespace spot
-{
- namespace eltl
- {
- bool
- format_parse_errors(std::ostream& os,
- parse_error_list& error_list)
- {
- bool printed = false;
- spot::eltl::parse_error_list::iterator it;
- for (it = error_list.begin(); it != error_list.end(); ++it)
- {
- if (it->second.first != "-")
- {
- os << it->second.first << ": ";
- os << it->first << ": ";
- }
- os << it->second.second << std::endl;
- printed = true;
- }
- return printed;
- }
- }
-}
diff --git a/src/eltlparse/parsedecl.hh b/src/eltlparse/parsedecl.hh
deleted file mode 100644
index e55fee06f..000000000
--- a/src/eltlparse/parsedecl.hh
+++ /dev/null
@@ -1,43 +0,0 @@
-// -*- coding: utf-8 -*-
-// Copyright (C) 2008, 2013, 2014 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 .
-
-#ifndef SPOT_ELTLPARSE_PARSEDECL_HH
-# define SPOT_ELTLPARSE_PARSEDECL_HH
-
-#include "eltlparse.hh"
-#include "misc/location.hh"
-
-# define YY_DECL \
- int eltlyylex (eltlyy::parser::semantic_type *yylval, \
- spot::location *yylloc, \
- spot::eltl::parse_error_list_t &pe)
-YY_DECL;
-
-namespace spot
-{
- namespace eltl
- {
- int flex_open(const std::string& name);
- void flex_close();
- void flex_set_buffer(const std::string& buf);
- void flex_unset_buffer();
- }
-}
-
-#endif // SPOT_ELTLPARSE_PARSEDECL_HH
diff --git a/src/eltlparse/public.hh b/src/eltlparse/public.hh
deleted file mode 100644
index 939d974fa..000000000
--- a/src/eltlparse/public.hh
+++ /dev/null
@@ -1,96 +0,0 @@
-// -*- coding: utf-8 -*-
-// Copyright (C) 2008, 2010, 2012, 2013 Laboratoire de Recherche et
-// Développement de l'Epita (LRDE).
-//
-// This file is part of Spot, a model checking library.
-//
-// Spot is free software; you can redistribute it and/or modify it
-// under the terms of the GNU General Public License as published by
-// the Free Software Foundation; either version 3 of the License, or
-// (at your option) any later version.
-//
-// Spot is distributed in the hope that it will be useful, but WITHOUT
-// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
-// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
-// License for more details.
-//
-// You should have received a copy of the GNU General Public License
-// along with this program. If not, see .
-
-#ifndef SPOT_ELTLPARSE_PUBLIC_HH
-# define SPOT_ELTLPARSE_PUBLIC_HH
-
-# include "ltlast/formula.hh"
-# include "ltlenv/defaultenv.hh"
-# include "ltlast/nfa.hh"
-# include "misc/location.hh"
-# include
-# include
-# include