* src/evtgbaparse/evtgbaparse.yy, src/evtgbaparse/evtgbascan.ll,

src/evtgbaparse/fmterror.cc, src/evtgbaparse/parsedecl.hh,
src/evtgbaparse/public.hh, src/evtgbatest/product.cc,
src/evtgbatest/readsave.cc, src/ltlparse/fmterror.cc,
src/ltlparse/ltlparse.yy, src/ltlparse/parsedecl.hh,
src/ltlparse/public.hh, src/tgbaparse/parsedecl.hh,
src/tgbaparse/public.hh, src/tgbaparse/tgbaparse.yy: Update
to Bison 2.0.
This commit is contained in:
Alexandre Duret-Lutz 2005-02-01 18:03:00 +00:00
parent 461fcd3732
commit 5cd58f9aaf
16 changed files with 64 additions and 66 deletions

View file

@ -1,5 +1,14 @@
2005-02-01 Alexandre Duret-Lutz <adl@src.lip6.fr> 2005-02-01 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/evtgbaparse/evtgbaparse.yy, src/evtgbaparse/evtgbascan.ll,
src/evtgbaparse/fmterror.cc, src/evtgbaparse/parsedecl.hh,
src/evtgbaparse/public.hh, src/evtgbatest/product.cc,
src/evtgbatest/readsave.cc, src/ltlparse/fmterror.cc,
src/ltlparse/ltlparse.yy, src/ltlparse/parsedecl.hh,
src/ltlparse/public.hh, src/tgbaparse/parsedecl.hh,
src/tgbaparse/public.hh, src/tgbaparse/tgbaparse.yy: Update
to Bison 2.0.
* bench/emptchk/pml2tgba.pl (usage): Correct description. From Denis. * bench/emptchk/pml2tgba.pl (usage): Correct description. From Denis.
* bench/emptchk/README: Timing info from Denis. * bench/emptchk/README: Timing info from Denis.

View file

@ -13,7 +13,7 @@ generally if you plan to regenerate some of the generated files.
GNU Automake >= 1.9 GNU Automake >= 1.9
GNU Libtool >= 1.4 GNU Libtool >= 1.4
GNU Flex (the version probably doesn't matter much, we used 2.5.31) GNU Flex (the version probably doesn't matter much, we used 2.5.31)
The CVS version of GNU Bison (called 1.875c at the time of writing) GNU Bison >= 2.0
SWIG >= 1.3.23 SWIG >= 1.3.23
Doxygen >= 1.4.0 Doxygen >= 1.4.0

View file

@ -1,4 +1,4 @@
/* Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), /* Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
** département Systèmes Répartis Coopératifs (SRC), Université Pierre ** département Systèmes Répartis Coopératifs (SRC), Université Pierre
** et Marie Curie. ** et Marie Curie.
** **
@ -55,6 +55,12 @@
%token ACC_DEF %token ACC_DEF
%token INIT_DEF %token INIT_DEF
%destructor { delete $$; } STRING UNTERMINATED_STRING IDENT
strident string acc_list
%printer { debug_stream() << *$$; } STRING UNTERMINATED_STRING IDENT
strident string
%% %%
evtgba: lines evtgba: lines
@ -114,14 +120,7 @@ init_decl:
%% %%
void void
yy::Parser::print_() yy::parser::error(const location_type& location, const std::string& message)
{
if (looka_ == STRING || looka_ == IDENT)
YYCDEBUG << " '" << *value.str << "'";
}
void
yy::Parser::error_()
{ {
error_list.push_back(spot::evtgba_parse_error(location, message)); error_list.push_back(spot::evtgba_parse_error(location, message));
} }
@ -136,12 +135,13 @@ namespace spot
if (evtgbayyopen(name)) if (evtgbayyopen(name))
{ {
error_list.push_back error_list.push_back
(evtgba_parse_error(yy::Location(), (evtgba_parse_error(yy::location(),
std::string("Cannot open file ") + name)); std::string("Cannot open file ") + name));
return 0; return 0;
} }
evtgba_explicit* result = new evtgba_explicit(); evtgba_explicit* result = new evtgba_explicit();
evtgbayy::Parser parser(debug, yy::Location(), error_list, result); evtgbayy::parser parser(error_list, result);
parser.set_debug_level(debug);
parser.parse(); parser.parse();
evtgbayyclose(); evtgbayyclose();
return result; return result;

View file

@ -1,4 +1,4 @@
/* Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), /* Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
** département Systèmes Répartis Coopératifs (SRC), Université Pierre ** département Systèmes Répartis Coopératifs (SRC), Université Pierre
** et Marie Curie. ** et Marie Curie.
** **
@ -31,16 +31,8 @@
#define YY_USER_ACTION \ #define YY_USER_ACTION \
yylloc->columns(yyleng); yylloc->columns(yyleng);
#define YY_USER_INIT \
do { \
yylloc->begin.filename = current_file; \
yylloc->end.filename = current_file; \
} while (0)
#define YY_NEVER_INTERACTIVE 1 #define YY_NEVER_INTERACTIVE 1
static std::string current_file;
%} %}
eol \n|\r|\n\r|\r\n eol \n|\r|\n\r|\r\n
@ -99,12 +91,10 @@ namespace spot
if (name == "-") if (name == "-")
{ {
yyin = stdin; yyin = stdin;
current_file = "standard input";
} }
else else
{ {
yyin = fopen (name.c_str (), "r"); yyin = fopen (name.c_str (), "r");
current_file = name;
if (!yyin) if (!yyin)
return 1; return 1;
} }

View file

@ -1,4 +1,4 @@
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
@ -26,13 +26,15 @@ namespace spot
{ {
bool bool
format_evtgba_parse_errors(std::ostream& os, format_evtgba_parse_errors(std::ostream& os,
const std::string& filename,
evtgba_parse_error_list& error_list) evtgba_parse_error_list& error_list)
{ {
bool printed = false; bool printed = false;
spot::evtgba_parse_error_list::iterator it; spot::evtgba_parse_error_list::iterator it;
for (it = error_list.begin(); it != error_list.end(); ++it) for (it = error_list.begin(); it != error_list.end(); ++it)
{ {
if (it->first.begin.filename != "") if (filename != "-")
os << filename << ":";
os << it->first << ": "; os << it->first << ": ";
os << it->second << std::endl; os << it->second << std::endl;
printed = true; printed = true;

View file

@ -1,4 +1,4 @@
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
@ -27,7 +27,7 @@
#include "location.hh" #include "location.hh"
# define YY_DECL \ # define YY_DECL \
int evtgbayylex (yystype *yylval, yy::Location *yylloc) int evtgbayylex (yystype *yylval, yy::location *yylloc)
YY_DECL; YY_DECL;
namespace spot namespace spot

View file

@ -1,4 +1,4 @@
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
@ -32,7 +32,7 @@
namespace spot namespace spot
{ {
/// \brief A parse diagnostic with its location. /// \brief A parse diagnostic with its location.
typedef std::pair<yy::Location, std::string> evtgba_parse_error; typedef std::pair<yy::location, std::string> evtgba_parse_error;
/// \brief A list of parser diagnostics, as filled by parse. /// \brief A list of parser diagnostics, as filled by parse.
typedef std::list<evtgba_parse_error> evtgba_parse_error_list; typedef std::list<evtgba_parse_error> evtgba_parse_error_list;
@ -56,10 +56,12 @@ namespace spot
/// \brief Format diagnostics produced by spot::evtgba_parse. /// \brief Format diagnostics produced by spot::evtgba_parse.
/// \param os Where diagnostics should be output. /// \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 /// \param error_list The error list filled by spot::ltl::parse while
/// parsing \a ltl_string. /// parsing \a ltl_string.
/// \return \c true iff any diagnostic was output. /// \return \c true iff any diagnostic was output.
bool format_evtgba_parse_errors(std::ostream& os, bool format_evtgba_parse_errors(std::ostream& os,
const std::string& filename,
evtgba_parse_error_list& error_list); evtgba_parse_error_list& error_list);
} }

View file

@ -1,4 +1,4 @@
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
@ -67,7 +67,9 @@ main(int argc, char** argv)
spot::evtgba_explicit* a = spot::evtgba_parse(argv[filename_index], spot::evtgba_explicit* a = spot::evtgba_parse(argv[filename_index],
pel, debug); pel, debug);
exit_code = spot::format_evtgba_parse_errors(std::cerr, pel); exit_code = spot::format_evtgba_parse_errors(std::cerr,
argv[filename_index],
pel);
if (a) if (a)
{ {

View file

@ -1,4 +1,4 @@
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
@ -54,7 +54,8 @@ main(int argc, char** argv)
spot::evtgba_explicit* a = spot::evtgba_parse(argv[filename_index], spot::evtgba_explicit* a = spot::evtgba_parse(argv[filename_index],
pel, debug); pel, debug);
exit_code = spot::format_evtgba_parse_errors(std::cerr, pel); exit_code = spot::format_evtgba_parse_errors(std::cerr, argv[filename_index],
pel);
if (a) if (a)
{ {

View file

@ -1,4 +1,4 @@
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
@ -37,7 +37,7 @@ namespace spot
for (it = error_list.begin(); it != error_list.end(); ++it) for (it = error_list.begin(); it != error_list.end(); ++it)
{ {
os << ">>> " << ltl_string << std::endl; os << ">>> " << ltl_string << std::endl;
yy::Location& l = it->first; yy::location& l = it->first;
unsigned n = 0; unsigned n = 0;
for (; n < 4 + l.begin.column; ++n) for (; n < 4 + l.begin.column; ++n)

View file

@ -1,4 +1,4 @@
/* Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), /* Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
** département Systèmes Répartis Coopératifs (SRC), Université Pierre ** département Systèmes Répartis Coopératifs (SRC), Université Pierre
** et Marie Curie. ** et Marie Curie.
** **
@ -111,6 +111,8 @@ using namespace spot::ltl;
%destructor { delete $$; } "atomic proposition" %destructor { delete $$; } "atomic proposition"
%destructor { spot::ltl::destroy($$); } result subformula %destructor { spot::ltl::destroy($$); } result subformula
%printer { debug_stream() << *$$; } "atomic proposition"
%% %%
result: subformula END_OF_INPUT result: subformula END_OF_INPUT
{ result = $$ = $1; { result = $$ = $1;
@ -260,14 +262,7 @@ subformula: ATOMIC_PROP
%% %%
void void
yy::Parser::print_() yy::parser::error(const location_type& location, const std::string& message)
{
if (looka_ == ATOMIC_PROP)
YYCDEBUG << " '" << *value.str << "'";
}
void
yy::Parser::error_()
{ {
error_list.push_back(parse_error(location, message)); error_list.push_back(parse_error(location, message));
} }
@ -284,7 +279,8 @@ namespace spot
{ {
formula* result = 0; formula* result = 0;
flex_set_buffer(ltl_string.c_str()); flex_set_buffer(ltl_string.c_str());
yy::Parser parser(debug, yy::Location(), error_list, env, result); yy::parser parser(error_list, env, result);
parser.set_debug_level(debug);
parser.parse(); parser.parse();
return result; return result;
} }

View file

@ -1,4 +1,4 @@
// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
@ -26,7 +26,7 @@
#include "location.hh" #include "location.hh"
# define YY_DECL \ # define YY_DECL \
int ltlyylex (yystype *yylval, yy::Location *yylloc) int ltlyylex (yystype *yylval, yy::location *yylloc)
YY_DECL; YY_DECL;
void flex_set_buffer(const char *buf); void flex_set_buffer(const char *buf);

View file

@ -1,4 +1,4 @@
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
@ -38,7 +38,7 @@ namespace spot
/// @{ /// @{
/// \brief A parse diagnostic with its location. /// \brief A parse diagnostic with its location.
typedef std::pair<yy::Location, std::string> parse_error; typedef std::pair<yy::location, std::string> parse_error;
/// \brief A list of parser diagnostics, as filled by parse. /// \brief A list of parser diagnostics, as filled by parse.
typedef std::list<parse_error> parse_error_list; typedef std::list<parse_error> parse_error_list;

View file

@ -1,4 +1,4 @@
// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
@ -27,7 +27,7 @@
#include "location.hh" #include "location.hh"
# define YY_DECL \ # define YY_DECL \
int tgbayylex (yystype *yylval, yy::Location *yylloc) int tgbayylex (yystype *yylval, yy::location *yylloc)
YY_DECL; YY_DECL;
namespace spot namespace spot

View file

@ -36,7 +36,7 @@ namespace spot
/// @{ /// @{
/// \brief A parse diagnostic with its location. /// \brief A parse diagnostic with its location.
typedef std::pair<yy::Location, std::string> tgba_parse_error; typedef std::pair<yy::location, std::string> tgba_parse_error;
/// \brief A list of parser diagnostics, as filled by parse. /// \brief A list of parser diagnostics, as filled by parse.
typedef std::list<tgba_parse_error> tgba_parse_error_list; typedef std::list<tgba_parse_error> tgba_parse_error_list;

View file

@ -1,4 +1,4 @@
/* Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), /* Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
** département Systèmes Répartis Coopératifs (SRC), Université Pierre ** département Systèmes Répartis Coopératifs (SRC), Université Pierre
** et Marie Curie. ** et Marie Curie.
** **
@ -80,6 +80,9 @@ typedef std::map<std::string, bdd> formula_cache;
delete $$; delete $$;
} acc_list } acc_list
%printer { debug_stream() << *$$; } STRING UNTERMINATED_STRING IDENT
strident string condition
%% %%
tgba: acceptance_decl lines tgba: acceptance_decl lines
| acceptance_decl | acceptance_decl
@ -110,7 +113,7 @@ line: strident ',' strident ',' condition ',' acc_list ';'
i != pel.end(); ++i) i != pel.end(); ++i)
{ {
// Adjust the diagnostic to the current position. // Adjust the diagnostic to the current position.
Location here = @1; location here = @1;
here.begin.line += i->first.begin.line; here.begin.line += i->first.begin.line;
here.begin.column += i->first.begin.column; here.begin.column += i->first.begin.column;
here.end.line = here.end.line =
@ -201,14 +204,7 @@ acc_decl:
%% %%
void void
yy::Parser::print_() yy::parser::error(const location_type& location, const std::string& message)
{
if (looka_ == STRING || looka_ == IDENT)
YYCDEBUG << " '" << *value.str << "'";
}
void
yy::Parser::error_()
{ {
error_list.push_back(spot::tgba_parse_error(location, message)); error_list.push_back(spot::tgba_parse_error(location, message));
} }
@ -225,14 +221,14 @@ namespace spot
if (tgbayyopen(name)) if (tgbayyopen(name))
{ {
error_list.push_back error_list.push_back
(tgba_parse_error(yy::Location(), (tgba_parse_error(yy::location(),
std::string("Cannot open file ") + name)); std::string("Cannot open file ") + name));
return 0; return 0;
} }
formula_cache fcache; formula_cache fcache;
tgba_explicit* result = new tgba_explicit(dict); tgba_explicit* result = new tgba_explicit(dict);
tgbayy::Parser parser(debug, yy::Location(), error_list, tgbayy::parser parser(error_list, env, result, fcache);
env, result, fcache); parser.set_debug_level(debug);
parser.parse(); parser.parse();
tgbayyclose(); tgbayyclose();
return result; return result;