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

* src/ltlparse/ltlscan.ll: Pass yyleng to the std::string constructor,

Browse source 
so it doesn't have to compute it.
* src/tgbaparse/tgbascan.ll: Likewise.
(YY_USER_INIT, current_file): Remove, it is too costly to use
yy::Location::filename in the current implementation
of yy::Location (this attribute is duplicated for each token).
Leaving it empty divides the parsing time by 3.
* src/tgbaparse/fmterror.cc, src/tgbaparse/public.hh
(format_tgba_parse_errors): Take the filename as argument.
* src/tgbatest/explprod.cc, src/tgbatest/ltl2tgba.cc,
src/tgbatest/mixprod.cc, src/tgbatest/powerset.cc,
src/tgbatest/readsave.cc, src/tgbatest/reductgba.cc,
src/tgbatest/tgbaread.cc, src/tgbatest/tripprod.cc,
iface/gspn/dottyssp.cc, iface/gspn/ltlgspn.cc: Adjust calls
to format_tgba_parse_errors.
This commit is contained in:
Alexandre Duret-Lutz 2004-12-16 12:33:37 +00:00
parent 704f237a22
commit 0efca0f644
15 changed files with 44 additions and 31 deletions
Download patch file Download diff file Expand all files Collapse all files

18
ChangeLog
View file

@ -1,3 +1,21 @@
2004-12-16 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/ltlparse/ltlscan.ll: Pass yyleng to the std::string constructor,
so it doesn't have to compute it.
* src/tgbaparse/tgbascan.ll: Likewise.
(YY_USER_INIT, current_file): Remove, it is too costly to use
yy::Location::filename in the current implementation
of yy::Location (this attribute is duplicated for each token).
Leaving it empty divides the parsing time by 3.
* src/tgbaparse/fmterror.cc, src/tgbaparse/public.hh
(format_tgba_parse_errors): Take the filename as argument.
* src/tgbatest/explprod.cc, src/tgbatest/ltl2tgba.cc,
src/tgbatest/mixprod.cc, src/tgbatest/powerset.cc,
src/tgbatest/readsave.cc, src/tgbatest/reductgba.cc,
src/tgbatest/tgbaread.cc, src/tgbatest/tripprod.cc,
iface/gspn/dottyssp.cc, iface/gspn/ltlgspn.cc: Adjust calls
to format_tgba_parse_errors.
2004-12-15 Alexandre Duret-Lutz <adl@src.lip6.fr> 2004-12-15 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaparse/tgbaparse.yy: Cache parsed formulae to speedup * src/tgbaparse/tgbaparse.yy: Cache parsed formulae to speedup

2
iface/gspn/dottyssp.cc
View file

@ -46,7 +46,7 @@ main(int argc, char **argv)
spot::tgba_parse_error_list pel1; spot::tgba_parse_error_list pel1;
spot::tgba_explicit* control = spot::tgba_parse(argv[--argc], pel1, spot::tgba_explicit* control = spot::tgba_parse(argv[--argc], pel1,
dict, env); dict, env);
if (spot::format_tgba_parse_errors(std::cerr, pel1)) if (spot::format_tgba_parse_errors(std::cerr, argv[argc], pel1))
return 2; return 2;
spot::tgba* a = gspn.automaton(control); spot::tgba* a = gspn.automaton(control);

3
iface/gspn/ltlgspn.cc
View file

@ -182,7 +182,8 @@ main(int argc, char **argv)
spot::tgba_parse_error_list pel1; spot::tgba_parse_error_list pel1;
spot::tgba_explicit* control = spot::tgba_parse(argv[formula_index + 2], spot::tgba_explicit* control = spot::tgba_parse(argv[formula_index + 2],
pel1, dict, env); pel1, dict, env);
if (spot::format_tgba_parse_errors(std::cerr, pel1)) if (spot::format_tgba_parse_errors(std::cerr, argv[formula_index + 2],
pel1))
return 2; return 2;
#else #else
spot::gspn_interface gspn(2, argv, dict, env, dead); spot::gspn_interface gspn(2, argv, dict, env, dead);

2
src/ltlparse/ltlscan.ll
View file

@ -116,7 +116,7 @@ flex_set_buffer(const char* buf)
*/ */
<not_prop>[a-zA-EH-QSTWYZ_][a-zA-EH-WYZ0-9_]* | <not_prop>[a-zA-EH-QSTWYZ_][a-zA-EH-WYZ0-9_]* |
<not_prop>[a-zA-EH-QSTWYZ_][a-zA-EH-WYZ0-9_][a-zA-Z0-9_]* { <not_prop>[a-zA-EH-QSTWYZ_][a-zA-EH-WYZ0-9_][a-zA-Z0-9_]* {
yylval->str = new std::string(yytext); yylval->str = new std::string(yytext, yyleng);
BEGIN(not_prop); BEGIN(not_prop);
return ATOMIC_PROP; return ATOMIC_PROP;
} }

6
src/tgbaparse/fmterror.cc
View file

@ -26,14 +26,16 @@ namespace spot
{ {
bool bool
format_tgba_parse_errors(std::ostream& os, format_tgba_parse_errors(std::ostream& os,
const std::string& filename,
tgba_parse_error_list& error_list) tgba_parse_error_list& error_list)
{ {
bool printed = false; bool printed = false;
spot::tgba_parse_error_list::iterator it; spot::tgba_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 << it->first << ": "; os << filename << ":";
os << it->first << ": ";
os << it->second << std::endl; os << it->second << std::endl;
printed = true; printed = true;
} }

1
src/tgbaparse/public.hh
View file

@ -69,6 +69,7 @@ namespace spot
/// 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_tgba_parse_errors(std::ostream& os, bool format_tgba_parse_errors(std::ostream& os,
const std::string& filename,
tgba_parse_error_list& error_list); tgba_parse_error_list& error_list);
/// @} /// @}

18
src/tgbaparse/tgbascan.ll
View file

@ -1,4 +1,4 @@
/* Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), /* Copyright (C) 2003, 2004 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
@ -54,7 +46,7 @@ eol \n|\r|\n\r|\r\n
acc[ \t]*= return ACC_DEF; acc[ \t]*= return ACC_DEF;
[a-zA-Z][a-zA-Z0-9_]* { [a-zA-Z][a-zA-Z0-9_]* {
yylval->str = new std::string(yytext); yylval->str = new std::string(yytext, yyleng);
return IDENT; return IDENT;
} }
@ -76,7 +68,7 @@ acc[ \t]*= return ACC_DEF;
return STRING; return STRING;
} }
\\["\\] yylval->str->append(1, yytext[1]); \\["\\] yylval->str->append(1, yytext[1]);
[^"\\]+ yylval->str->append (yytext, yyleng); [^"\\]+ yylval->str->append(yytext, yyleng);
<<EOF>> { <<EOF>> {
BEGIN(INITIAL); BEGIN(INITIAL);
return UNTERMINATED_STRING; return UNTERMINATED_STRING;
@ -98,12 +90,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;
} }

4
src/tgbatest/explprod.cc
View file

@ -47,11 +47,11 @@ main(int argc, char** argv)
spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::ltl::environment& env(spot::ltl::default_environment::instance());
spot::tgba_parse_error_list pel1; spot::tgba_parse_error_list pel1;
spot::tgba_explicit* a1 = spot::tgba_parse(argv[1], pel1, dict, env); spot::tgba_explicit* a1 = spot::tgba_parse(argv[1], pel1, dict, env);
if (spot::format_tgba_parse_errors(std::cerr, pel1)) if (spot::format_tgba_parse_errors(std::cerr, argv[1], pel1))
return 2; return 2;
spot::tgba_parse_error_list pel2; spot::tgba_parse_error_list pel2;
spot::tgba_explicit* a2 = spot::tgba_parse(argv[2], pel2, dict, env); spot::tgba_explicit* a2 = spot::tgba_parse(argv[2], pel2, dict, env);
if (spot::format_tgba_parse_errors(std::cerr, pel2)) if (spot::format_tgba_parse_errors(std::cerr, argv[2], pel2))
return 2; return 2;
{ {

5
src/tgbatest/ltl2tgba.cc
View file

@ -280,7 +280,8 @@ main(int argc, char** argv)
spot::tgba_parse_error_list pel; spot::tgba_parse_error_list pel;
system = spot::tgba_parse(argv[formula_index] + 2, system = spot::tgba_parse(argv[formula_index] + 2,
pel, dict, env, debug_opt); pel, dict, env, debug_opt);
if (spot::format_tgba_parse_errors(std::cerr, pel)) if (spot::format_tgba_parse_errors(std::cerr,
argv[formula_index] + 2, pel))
return 2; return 2;
system->merge_transitions(); system->merge_transitions();
std::clog << argv[formula_index] + 2 << " read" << std::endl; std::clog << argv[formula_index] + 2 << " read" << std::endl;
@ -528,7 +529,7 @@ main(int argc, char** argv)
spot::tgba_parse_error_list pel; spot::tgba_parse_error_list pel;
spot::tgba_explicit* e; spot::tgba_explicit* e;
to_free = a = e = spot::tgba_parse(input, pel, dict, env, debug_opt); to_free = a = e = spot::tgba_parse(input, pel, dict, env, debug_opt);
if (spot::format_tgba_parse_errors(std::cerr, pel)) if (spot::format_tgba_parse_errors(std::cerr, input, pel))
{ {
delete to_free; delete to_free;
delete dict; delete dict;

2
src/tgbatest/mixprod.cc
View file

@ -56,7 +56,7 @@ main(int argc, char** argv)
spot::tgba_parse_error_list pel2; spot::tgba_parse_error_list pel2;
spot::tgba_explicit* a2 = spot::tgba_parse(argv[2], pel2, dict, env); spot::tgba_explicit* a2 = spot::tgba_parse(argv[2], pel2, dict, env);
if (spot::format_tgba_parse_errors(std::cerr, pel2)) if (spot::format_tgba_parse_errors(std::cerr, argv[2], pel2))
return 2; return 2;
{ {

2
src/tgbatest/powerset.cc
View file

@ -48,7 +48,7 @@ main(int argc, char** argv)
spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::ltl::environment& env(spot::ltl::default_environment::instance());
spot::tgba_parse_error_list pel; spot::tgba_parse_error_list pel;
spot::tgba_explicit* a = spot::tgba_parse(argv[1], pel, dict, env); spot::tgba_explicit* a = spot::tgba_parse(argv[1], pel, dict, env);
if (spot::format_tgba_parse_errors(std::cerr, pel)) if (spot::format_tgba_parse_errors(std::cerr, argv[1], pel))
return 2; return 2;

2
src/tgbatest/readsave.cc
View file

@ -60,7 +60,7 @@ main(int argc, char** argv)
pel, dict, env, debug); pel, dict, env, debug);
exit_code = exit_code =
spot::format_tgba_parse_errors(std::cerr, pel); spot::format_tgba_parse_errors(std::cerr, argv[filename_index], pel);
if (a) if (a)
{ {

2
src/tgbatest/reductgba.cc
View file

@ -106,7 +106,7 @@ main(int argc, char** argv)
#ifdef REDUCCMP #ifdef REDUCCMP
spot::tgba_parse_error_list pel; spot::tgba_parse_error_list pel;
automata = spot::tgba_parse(argv[2], pel, dict, env, false); automata = spot::tgba_parse(argv[2], pel, dict, env, false);
if (spot::format_tgba_parse_errors(std::cerr, pel)) if (spot::format_tgba_parse_errors(std::cerr, argv[2], pel))
return 2; return 2;
#else #else
spot::ltl::parse_error_list p1; spot::ltl::parse_error_list p1;

2
src/tgbatest/tgbaread.cc
View file

@ -57,7 +57,7 @@ main(int argc, char** argv)
spot::tgba_explicit* a = spot::tgba_parse(argv[filename_index], spot::tgba_explicit* a = spot::tgba_parse(argv[filename_index],
pel, dict, env, debug); pel, dict, env, debug);
if (spot::format_tgba_parse_errors(std::cerr, pel)) if (spot::format_tgba_parse_errors(std::cerr, argv[filename_index], pel))
return 2; return 2;
if (a) if (a)

6
src/tgbatest/tripprod.cc
View file

@ -47,15 +47,15 @@ main(int argc, char** argv)
spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::ltl::environment& env(spot::ltl::default_environment::instance());
spot::tgba_parse_error_list pel1; spot::tgba_parse_error_list pel1;
spot::tgba_explicit* a1 = spot::tgba_parse(argv[1], pel1, dict, env); spot::tgba_explicit* a1 = spot::tgba_parse(argv[1], pel1, dict, env);
if (spot::format_tgba_parse_errors(std::cerr, pel1)) if (spot::format_tgba_parse_errors(std::cerr, argv[1], pel1))
return 2; return 2;
spot::tgba_parse_error_list pel2; spot::tgba_parse_error_list pel2;
spot::tgba_explicit* a2 = spot::tgba_parse(argv[2], pel2, dict, env); spot::tgba_explicit* a2 = spot::tgba_parse(argv[2], pel2, dict, env);
if (spot::format_tgba_parse_errors(std::cerr, pel2)) if (spot::format_tgba_parse_errors(std::cerr, argv[2], pel2))
return 2; return 2;
spot::tgba_parse_error_list pel3; spot::tgba_parse_error_list pel3;
spot::tgba_explicit* a3 = spot::tgba_parse(argv[3], pel3, dict, env); spot::tgba_explicit* a3 = spot::tgba_parse(argv[3], pel3, dict, env);
if (spot::format_tgba_parse_errors(std::cerr, pel3)) if (spot::format_tgba_parse_errors(std::cerr, argv[3], pel3))
return 2; return 2;
{ {