alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

tgbaparse: remove this parser

Browse source 
For issue #1 (nearly done).

* src/tgbaparse/: Delete.
* configure.ac, src/Makefile.am, README: Adjust.
* src/tgbatest/randtgba.cc: Remove useless #include.
This commit is contained in:
Alexandre Duret-Lutz 2015-01-31 20:44:33 +01:00
parent d0f0be234d
commit a246c3b8ba
12 changed files with 9 additions and 633 deletions
Download patch file Download diff file Expand all files Collapse all files

5
README
View file

@ -156,10 +156,9 @@ src/ Sources for libspot.
tgba/ TGBA objects and cousins.
tgbaalgos/ Algorithms on TGBA.
gtec/ Couvreur's Emptiness-Check.
tgbaparse/ Parser for explicit TGBA.
ta/ TA objects and cousins (TGTA).
taalgos/ Algorithms on TA/TGTA.
tgbatest/ Tests for tgba/, tgbaalgos/, tgbaparse/, ta/ and taalgos/.
tgbatest/ Tests for tgba/, tgbaalgos/, ta/ and taalgos/.
sanity/ Sanity tests for the whole project.
doc/ Documentation for libspot.
org/ Source of userdoc/ as org-mode files.
@ -204,7 +203,7 @@ End:
LocalWords: Python's BuDDy LBTT LTL Büchi lbtt gspn DIR GreatSPN Soheib Yann
LocalWords: Baarir Thierry Mieg CVS Università di Torino devel src libspot ac
LocalWords: ltlast ltlenv ltlparse ltlvisit ltltest misc tgba TGBA tgbaalgos
LocalWords: gtec Tarjan tgbaparse tgbatest doc html PDF spotref pdf cgi ELTL
LocalWords: gtec Tarjan tgbatest 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 kripketest Automata

3
configure.ac
View file

@ -1,5 +1,5 @@
# -*- coding: utf-8 -*-
# Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire
# Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire
# de Recherche et Développement de l'Epita (LRDE).
# Copyright (C) 2003, 2004, 2005, 2006, 2007 Laboratoire
# d'Informatique de Paris 6 (LIP6), département Systèmes Répartis
@ -199,7 +199,6 @@ AC_CONFIG_FILES([
src/tgba/Makefile
src/taalgos/Makefile
src/ta/Makefile
src/tgbaparse/Makefile
src/tgbatest/defs
src/tgbatest/Makefile
wrap/Makefile

8
src/Makefile.am
View file

@ -1,5 +1,5 @@
## -*- coding: utf-8 -*-
## Copyright (C) 2009, 2010, 2012, 2013, 2014 Laboratoire de Recherche
## Copyright (C) 2009, 2010, 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
@ -26,9 +26,8 @@ AUTOMAKE_OPTIONS = subdir-objects
# end, after building '.' (since the current directory contains
# libspot.la needed by the tests)
SUBDIRS = misc priv ltlenv ltlast ltlvisit ltlparse graph tgba \
tgbaalgos tgbaparse ta taalgos kripke kripkeparse \
dstarparse hoaparse . bin ltltest graphtest tgbatest \
kripketest sanity
tgbaalgos ta taalgos kripke kripkeparse dstarparse hoaparse \
. bin ltltest graphtest tgbatest kripketest sanity
lib_LTLIBRARIES = libspot.la
libspot_la_SOURCES =
@ -48,7 +47,6 @@ libspot_la_LIBADD = \
ta/libta.la \
tgbaalgos/libtgbaalgos.la \
tgba/libtgba.la \
tgbaparse/libtgbaparse.la \
../lib/libgnu.la
# Dummy C++ source to cause C++ linking.

13
src/tgbaparse/.cvsignore
View file

@ -1,13 +0,0 @@
.deps
Makefile
Makefile.in
location.hh
tgbaparse.cc
tgbaparse.hh
tgbaparse.output
tgbascan.cc
position.hh
stack.hh
*.lo
*.la
.libs

13
src/tgbaparse/.gitignore vendored
View file

@ -1,13 +0,0 @@
.deps
Makefile
Makefile.in
location.hh
tgbaparse.cc
tgbaparse.hh
tgbaparse.output
tgbascan.cc
position.hh
stack.hh
*.lo
*.la
.libs

60
src/tgbaparse/Makefile.am
View file

@ -1,60 +0,0 @@
## -*- coding: utf-8 -*-
## Copyright (C) 2008, 2009, 2011, 2013 Laboratoire de Recherche et
## Développement de l'Epita (LRDE).
## Copyright (C) 2003, 2004, 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 <http://www.gnu.org/licenses/>.
AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(BUDDY_CPPFLAGS) -DYY_NO_INPUT
# Disable -Werror because too many versions of flex yield warnings.
AM_CXXFLAGS = $(WARNING_CXXFLAGS:-Werror=)
tgbaparsedir = $(pkgincludedir)/tgbaparse
tgbaparse_HEADERS = public.hh
noinst_LTLIBRARIES = libtgbaparse.la
TGBAPARSE_YY = tgbaparse.yy
FROM_TGBAPARSE_YY_MAIN = tgbaparse.cc
FROM_TGBAPARSE_YY_OTHERS = \
stack.hh \
tgbaparse.hh
FROM_TGBAPARSE_YY = $(FROM_TGBAPARSE_YY_MAIN) $(FROM_TGBAPARSE_YY_OTHERS)
BUILT_SOURCES = $(FROM_TGBAPARSE_YY)
MAINTAINERCLEANFILES = $(FROM_TGBAPARSE_YY)
$(FROM_TGBAPARSE_YY_MAIN): $(srcdir)/$(TGBAPARSE_YY)
## We must cd into $(srcdir) first because if we tell bison to read
## $(srcdir)/$(TGBAPARSE_YY), it will also use the value of $(srcdir)/
## in the generated include statements.
cd $(srcdir) && \
$(BISON) -Wall -Werror --report=all $(BISON_EXTRA_FLAGS) \
$(TGBAPARSE_YY) -o $(FROM_TGBAPARSE_YY_MAIN)
$(FROM_TGBAPARSE_YY_OTHERS): $(TGBAPARSE_YY)
@test -f $@ || $(MAKE) $(AM_MAKEFLAGS) $(FROM_TGBAPARSE_YY_MAIN)
EXTRA_DIST = $(TGBAPARSE_YY)
libtgbaparse_la_SOURCES = \
fmterror.cc \
$(FROM_TGBAPARSE_YY) \
tgbascan.ll \
parsedecl.hh

45
src/tgbaparse/fmterror.cc
View file

@ -1,45 +0,0 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2014 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 <http://www.gnu.org/licenses/>.
#include <ostream>
#include "public.hh"
namespace spot
{
bool
format_tgba_parse_errors(std::ostream& os,
const std::string& filename,
tgba_parse_error_list& error_list)
{
bool printed = false;
spot::tgba_parse_error_list::iterator it;
for (it = error_list.begin(); it != error_list.end(); ++it)
{
if (filename != "-")
os << filename << ':';
os << it->first << ": ";
os << it->second << std::endl;
printed = true;
}
return printed;
}
}

42
src/tgbaparse/parsedecl.hh
View file

@ -1,42 +0,0 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2013, 2014 Laboratoire de Recherche et
// Développement de l'Epita.
// Copyright (C) 2003, 2005 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 <http://www.gnu.org/licenses/>.
#ifndef SPOT_TGBAPARSE_PARSEDECL_HH
# define SPOT_TGBAPARSE_PARSEDECL_HH
#include <string>
#include "tgbaparse.hh"
#include "misc/location.hh"
# define YY_DECL \
int tgbayylex (tgbayy::parser::semantic_type *yylval, \
spot::location *yylloc)
YY_DECL;
namespace spot
{
int tgbayyopen(const std::string& name);
void tgbayyclose();
}
#endif // SPOT_TGBAPARSE_PARSEDECL_HH

88
src/tgbaparse/public.hh
View file

@ -1,88 +0,0 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2012, 2013, 2014 Laboratoire de Recherche et
// Développement de l'Epita.
// Copyright (C) 2003, 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 <http://www.gnu.org/licenses/>.
#ifndef SPOT_TGBAPARSE_PUBLIC_HH
# define SPOT_TGBAPARSE_PUBLIC_HH
# include "tgba/tgbagraph.hh"
# include "misc/location.hh"
# include "ltlenv/defaultenv.hh"
# include <string>
# include <list>
# include <utility>
# include <iosfwd>
namespace spot
{
/// \addtogroup tgba_io
/// @{
#ifndef SWIG
/// \brief A parse diagnostic with its location.
typedef std::pair<spot::location, std::string> tgba_parse_error;
/// \brief A list of parser diagnostics, as filled by parse.
typedef std::list<tgba_parse_error> tgba_parse_error_list;
#else
// Turn parse_error_list into an opaque type for Swig.
struct tgba_parse_error_list {};
#endif
/// \brief Build a spot::tgba_digraph from a text file.
/// \param filename The name of the file to parse.
/// \param error_list A list that will be filled with
/// parse errors that occured during parsing.
/// \param dict The BDD dictionary where to use.
/// \param env The environment of atomic proposition into which parsing
/// should take place.
/// \param debug When true, causes the parser to trace its execution.
/// \return A pointer to the tgba built from \a filename, or
/// 0 if the file could not be opened.
///
/// Note that the parser usually tries to recover from errors. It can
/// return an non zero value even if it encountered error during the
/// parsing of \a filename. If you want to make sure \a filename
/// was parsed succesfully, check \a error_list for emptiness.
///
/// \warning This function is not reentrant.
SPOT_API
tgba_digraph_ptr tgba_parse(const std::string& filename,
tgba_parse_error_list& error_list,
bdd_dict_ptr dict,
ltl::environment& env
= ltl::default_environment::instance(),
bool debug = false);
/// \brief Format diagnostics produced by spot::tgba_parse.
/// \param os Where diagnostics should be output.
/// \param filename The filename that should appear in the diagnostics.
/// \param error_list The error list filled by spot::ltl::parse while
/// parsing \a ltl_string.
/// \return \c true iff any diagnostic was output.
SPOT_API
bool format_tgba_parse_errors(std::ostream& os,
const std::string& filename,
tgba_parse_error_list& error_list);
/// @}
}
#endif // SPOT_TGBAPARSE_PUBLIC_HH

245
src/tgbaparse/tgbaparse.yy
View file

@ -1,245 +0,0 @@
/* -*- coding: utf-8 -*-
** Copyright (C) 2009, 2010, 2012, 2013, 2014 Laboratoire de Recherche
** et Développement de l'Epita (LRDE).
** Copyright (C) 2003, 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 <http://www.gnu.org/licenses/>.
*/
%language "C++"
%locations
%defines
%name-prefix "tgbayy"
%debug
%error-verbose
%define api.location.type "spot::location"
%code requires
{
#include <string>
#include "public.hh"
#include "priv/accmap.hh"
#include "tgba/formula2bdd.hh"
/* Cache parsed formulae. Labels on arcs are frequently identical and
it would be a waste of time to parse them to formula* over and
over, and to register all their atomic_propositions in the
bdd_dict. Keep the bdd result around so we can reuse it. */
typedef std::map<std::string, bdd> formula_cache;
typedef typename spot::tgba_digraph::namer<std::string>::type named_tgba_t;
}
%parse-param {spot::tgba_parse_error_list& error_list}
%parse-param {spot::ltl::environment& parse_environment}
%parse-param {spot::acc_mapper_string& acc_map}
%parse-param {spot::tgba_digraph_ptr& result}
%parse-param {named_tgba_t*& namer}
%parse-param {formula_cache& fcache}
%union
{
int token;
std::string* str;
const spot::ltl::formula* f;
spot::acc_cond::mark_t acc;
}
%code
{
#include "ltlast/constant.hh"
#include "ltlparse/public.hh"
#include <map>
/* tgbaparse.hh and parsedecl.hh include each other recursively.
We must ensure that YYSTYPE is declared (by the above %union)
before parsedecl.hh uses it. */
#include "parsedecl.hh"
using namespace spot::ltl;
typedef std::pair<bool, spot::ltl::formula*> pair;
}
%token <str> STRING UNTERMINATED_STRING
%token <str> IDENT
%type <str> strident string
%type <str> condition
%type <acc> acc_list
%token ACC_DEF
%destructor { delete $$; } <str>
%printer { debug_stream() << *$$; } <str>
%printer { debug_stream() << $$; } <acc>
%%
tgba: acceptance_decl lines
| acceptance_decl
{ namer->new_state("0"); }
| lines
|
{ namer->new_state("0"); };
acceptance_decl: ACC_DEF acc_decl ';'
{
}
/* At least one line. */
lines: line
| lines line
;
line: strident ',' strident ',' condition ',' acc_list ';'
{
bdd cond = bddtrue;
if ($5)
{
formula_cache::const_iterator i = fcache.find(*$5);
if (i == fcache.end())
{
parse_error_list pel;
const formula* f =
spot::ltl::parse_boolean(*$5, pel, parse_environment,
debug_level());
for (auto& j: pel)
{
// Adjust the diagnostic to the current position.
spot::location here = @5;
here.end.line = here.begin.line + j.first.end.line - 1;
here.end.column = here.begin.column + j.first.end.column;
here.begin.line += j.first.begin.line - 1;
here.begin.column += j.first.begin.column;
error_list.emplace_back(here, j.second);
}
if (f)
{
cond = formula_to_bdd(f, result->get_dict(), result);
f->destroy();
}
fcache[*$5] = cond;
}
else
{
cond = i->second;
}
}
unsigned s = namer->new_state(*$1);
unsigned d = namer->new_state(*$3);
namer->graph().new_transition(s, d, cond, $7);
delete $1;
delete $3;
delete $5;
}
;
string: STRING
| UNTERMINATED_STRING
{
$$ = $1;
error_list.emplace_back(@1, "unterminated string");
}
strident: string | IDENT
condition:
{
$$ = 0;
}
| string
{
$$ = $1;
}
;
acc_list:
{
$$ = 0U;
}
| acc_list strident
{
if (*$2 != "" && *$2 != "false")
{
auto p = acc_map.lookup(*$2);
if (! p.first)
{
error_list.emplace_back(@2,
"undeclared acceptance condition `" + *$2 + "'");
// $2 will be destroyed on error recovery.
YYERROR;
}
$1 |= p.second;
}
delete $2;
$$ = $1;
}
;
acc_decl:
| acc_decl strident
{
acc_map.declare(*$2);
delete $2;
}
;
%%
void
tgbayy::parser::error(const location_type& location,
const std::string& message)
{
error_list.emplace_back(location, message);
}
namespace spot
{
tgba_digraph_ptr
tgba_parse(const std::string& name,
tgba_parse_error_list& error_list,
bdd_dict_ptr dict,
environment& env,
bool debug)
{
if (tgbayyopen(name))
{
error_list.emplace_back(spot::location(),
std::string("Cannot open file ") + name);
return 0;
}
formula_cache fcache;
auto result = make_tgba_digraph(dict);
auto namer = result->create_namer<std::string>();
spot::acc_mapper_string acc_map(result);
tgbayy::parser parser(error_list, env, acc_map, result, namer, fcache);
parser.set_debug_level(debug);
parser.parse();
tgbayyclose();
if (namer) // No fatal error
{
delete namer;
return result;
}
else // Fatal error
{
return nullptr;
}
}
}
// Local Variables:
// mode: c++
// End:

113
src/tgbaparse/tgbascan.ll
View file

@ -1,113 +0,0 @@
/* -*- coding: utf-8 -*-
** Copyright (C) 2011, 2014, 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 <http://www.gnu.org/licenses/>.
*/
%option noyywrap
%option prefix="tgbayy"
%option outfile="lex.yy.c"
%x STATE_STRING
%{
#include <string>
#include "tgbaparse/parsedecl.hh"
#define YY_USER_ACTION \
yylloc->columns(yyleng);
#define YY_NEVER_INTERACTIVE 1
typedef tgbayy::parser::token token;
%}
eol \n+|\r+
eol2 (\n\r)+|(\r\n)+
%%
%{
yylloc->step ();
%}
acc[ \t]*= return token::ACC_DEF;
[a-zA-Z_.][a-zA-Z0-9_.]* {
yylval->str = new std::string(yytext, yyleng);
return token::IDENT;
}
/* discard whitespace */
{eol} yylloc->lines(yyleng); yylloc->step();
{eol2} yylloc->lines(yyleng / 2); yylloc->step();
[ \t]+ yylloc->step();
\" {
yylval->str = new std::string;
BEGIN(STATE_STRING);
}
. return *yytext;
/* Handle \" and \\ in strings. */
<STATE_STRING>{
\" {
BEGIN(INITIAL);
return token::STRING;
}
\\["\\] yylval->str->append(1, yytext[1]);
[^"\\]+ yylval->str->append(yytext, yyleng);
<<EOF>> {
BEGIN(INITIAL);
return token::UNTERMINATED_STRING;
}
}
%{
/* Dummy use of yyunput to shut up a gcc warning. */
(void) &yyunput;
%}
%%
namespace spot
{
int
tgbayyopen(const std::string &name)
{
if (name == "-")
{
yyin = stdin;
}
else
{
yyin = fopen(name.c_str(), "r");
if (!yyin)
return 1;
}
return 0;
}
void
tgbayyclose()
{
fclose(yyin);
}
}

5
src/tgbatest/randtgba.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014 Laboratoire de
// Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014, 2015 Laboratoire
// de Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
@ -41,7 +41,6 @@
#include "tgbaalgos/stats.hh"
#include "ltlenv/defaultenv.hh"
#include "tgbaalgos/dotty.hh"
#include "tgbaparse/public.hh"
#include "misc/random.hh"
#include "misc/optionmap.hh"
#include "tgbaalgos/degen.hh"