diff --git a/src/neverparse/neverclaimparse.yy b/src/neverparse/neverclaimparse.yy index 73d4337c0..1532a425d 100644 --- a/src/neverparse/neverclaimparse.yy +++ b/src/neverparse/neverclaimparse.yy @@ -1,5 +1,5 @@ /* -*- coding: utf-8 -*- -** Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et +** Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et ** DĂ©veloppement de l'Epita (LRDE). ** ** This file is part of Spot, a model checking library. @@ -25,6 +25,7 @@ %name-prefix "neverclaimyy" %debug %error-verbose +%lex-param { spot::neverclaim_parse_error_list& error_list } %code requires { @@ -59,20 +60,26 @@ before parsedecl.hh uses it. */ #include "parsedecl.hh" using namespace spot::ltl; +static bool accept_all_needed = false; +static bool accept_all_seen = false; } %token NEVER "never" %token SKIP "skip" %token IF "if" %token FI "fi" +%token DO "do" +%token OD "od" %token ARROW "->" %token GOTO "goto" %token FALSE "false" +%token ATOMIC "atomic" +%token ASSERT "assert" %token FORMULA "boolean formula" %token IDENT "identifier" %type formula opt_dest -%type

transition -%type transitions +%type

transition src_dest +%type transitions transition_block %type ident_list @@ -112,7 +119,7 @@ ident_list: | ident_list IDENT ':' { result->add_state_alias(*$2, *$1); - // Keep any identifier that start with accept. + // Keep any identifier that starts with accept. if (strncmp("accept", $1->c_str(), 6)) { delete $1; @@ -125,9 +132,23 @@ ident_list: } } + +transition_block: + "if" transitions "fi" + { + $$ = $2; + } + | "do" transitions "od" + { + $$ = $2; + } + state: ident_list "skip" { + if (*$1 == "accept_all") + accept_all_seen = true; + spot::state_explicit_string::transition* t = result->create_transition(*$1, *$1); bool acc = !strncmp("accept", $1->c_str(), 6); if (acc) @@ -137,11 +158,11 @@ state: } | ident_list { delete $1; } | ident_list "false" { delete $1; } - | ident_list "if" transitions "fi" + | ident_list transition_block { std::list::iterator it; bool acc = !strncmp("accept", $1->c_str(), 6); - for (it = $3->begin(); it != $3->end(); ++it) + for (it = $2->begin(); it != $2->end(); ++it) { spot::state_explicit_string::transition* t = result->create_transition(*$1, *it->second); @@ -153,10 +174,10 @@ state: } // Free the list delete $1; - for (std::list::iterator it = $3->begin(); - it != $3->end(); ++it) + for (std::list::iterator it = $2->begin(); + it != $2->end(); ++it) delete it->second; - delete $3; + delete $2; } @@ -184,41 +205,57 @@ opt_dest: { $$ = $3; } + | "->" "assert" FORMULA + { + delete $3; + $$ = new std::string("accept_all"); + accept_all_needed = true; + } -transition: - ':' ':' formula opt_dest +src_dest: formula opt_dest { // If there is no destination, do ignore the transition. // This happens for instance with // if // :: false // fi - if (!$4) + if (!$2) { - delete $3; + delete $1; $$ = 0; } else { spot::ltl::parse_error_list pel; const spot::ltl::formula* f = - spot::ltl::parse_boolean(*$3, pel, parse_environment, + spot::ltl::parse_boolean(*$1, pel, parse_environment, debug_level(), true); - delete $3; + delete $1; for(spot::ltl::parse_error_list::const_iterator i = pel.begin(); i != pel.end(); ++i) { // Adjust the diagnostic to the current position. - location here = @3; + location here = @1; here.end.line = here.begin.line + i->first.end.line - 1; here.end.column = here.begin.column + i->first.end.column -1; here.begin.line += i->first.begin.line - 1; here.begin.column += i->first.begin.column - 1; error(here, i->second); } - $$ = new pair(f, $4); + $$ = new pair(f, $2); } } + + +transition: + ':' ':' "atomic" '{' src_dest '}' + { + $$ = $5; + } + | ':' ':' src_dest + { + $$ = $3; + } %% void @@ -250,6 +287,17 @@ namespace spot parser.set_debug_level(debug); parser.parse(); neverclaimyyclose(); + + if (accept_all_needed && !accept_all_seen) + { + spot::state_explicit_string::transition* t = + result->create_transition("accept_all", "accept_all"); + result->add_acceptance_condition + (t, spot::ltl::constant::true_instance()); + } + accept_all_needed = false; + accept_all_seen = false; + return result; } } diff --git a/src/neverparse/neverclaimscan.ll b/src/neverparse/neverclaimscan.ll index 71a971dcd..77656137d 100644 --- a/src/neverparse/neverclaimscan.ll +++ b/src/neverparse/neverclaimscan.ll @@ -1,5 +1,5 @@ -/* Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement de -** l'Epita (LRDE). +/* Copyright (C) 2010, 2011, 2013 Laboratoire de Recherche et +** Développement de l'Epita (LRDE). ** ** This file is part of Spot, a model checking library. ** @@ -23,6 +23,7 @@ %{ #include #include "neverparse/parsedecl.hh" +#include "misc/escape.hh" #define YY_USER_ACTION \ yylloc->columns(yyleng); @@ -30,9 +31,13 @@ #define YY_NEVER_INTERACTIVE 1 typedef neverclaimyy::parser::token token; +static int parent_level = 0; +static bool missing_parent = false; %} +%x in_par + eol \n|\r|\n\r|\r\n %% @@ -50,11 +55,46 @@ eol \n|\r|\n\r|\r\n "skip" return token::SKIP; "if" return token::IF; "fi" return token::FI; +"do" return token::DO; +"od" return token::OD; "->" return token::ARROW; "goto" return token::GOTO; "false"|"0" return token::FALSE; +"atomic" return token::ATOMIC; +"assert" return token::ASSERT; -("!"[ \t]*)?"(".*")"|"true"|"1" { +("!"[ \t]*)?"(" { + parent_level = 1; + BEGIN(in_par); + yylval->str = new std::string(yytext,yyleng); + } + +{ + "(" { + ++parent_level; + yylval->str->append(yytext, yyleng); + } + ")" { + yylval->str->append(yytext, yyleng); + if (!--parent_level) + { + BEGIN(0); + spot::trim(*yylval->str); + return token::FORMULA; + } + } + [^()]+ yylval->str->append(yytext, yyleng); + <> { + unput(')'); + if (!missing_parent) + error_list.push_back( + spot::neverclaim_parse_error(*yylloc, + "missing closing parenthese")); + missing_parent = true; + } +} + +"true"|"1" { yylval->str = new std::string(yytext, yyleng); return token::FORMULA; } @@ -95,5 +135,6 @@ namespace spot neverclaimyyclose() { fclose(yyin); + missing_parent = false; } } diff --git a/src/neverparse/parsedecl.hh b/src/neverparse/parsedecl.hh index ea53b8dfe..f701c2dac 100644 --- a/src/neverparse/parsedecl.hh +++ b/src/neverparse/parsedecl.hh @@ -1,5 +1,5 @@ -// Copyright (C) 2010 Laboratoire de Recherche et Développement de -// l'EPITA. +// Copyright (C) 2010, 2013 Laboratoire de Recherche et Développement +// de l'EPITA. // // This file is part of Spot, a model checking library. // @@ -24,8 +24,9 @@ #include "location.hh" # define YY_DECL \ - int neverclaimyylex (neverclaimyy::parser::semantic_type *yylval, \ - neverclaimyy::location *yylloc) + int neverclaimyylex(neverclaimyy::parser::semantic_type *yylval, \ + neverclaimyy::location *yylloc, \ + spot::neverclaim_parse_error_list& error_list) YY_DECL; namespace spot diff --git a/src/tgbatest/neverclaimread.test b/src/tgbatest/neverclaimread.test index e643587d5..5407fce59 100755 --- a/src/tgbatest/neverclaimread.test +++ b/src/tgbatest/neverclaimread.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et +# Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et # DĂ©veloppement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -68,6 +68,51 @@ diff stdout expected rm input stdout expected +# Same test, but with the newer syntax output since Spin 6.24 +cat >input < goto T2_init +:: (p1 && p0) -> goto T1 +od; +T1: +do +:: atomic { (p1 && (! p0)) -> assert(!(p1 && (! p0))) } +:: !(p1) -> goto T1 +:: ! (p1) -> goto T2_init +od; +} +EOF + +run 0 ../ltl2tgba -XN input > stdout + +cat >expected < 1 + 1 [label="T2_init"] + 1 -> 1 [label="1\n"] + 1 -> 2 [label="p0 & p1\n"] + 2 [label="T1"] + 2 -> 3 [label="p1 & !p0\n"] + 2 -> 2 [label="!p1\n"] + 2 -> 1 [label="!p1\n"] + 3 [label="accept_all", peripheries=2] + 3 -> 3 [label="1\n{Acc[1]}"] +} +EOF + +# Sort out some possible inversions in the output. +# (The order is not guaranteed by SPOT.) +sed -e 's/!p0 & p1/p1 \& !p0/g' -e 's/p1 & p0/p0 \& p1/g' stdout \ + > tmp_ && mv tmp_ stdout +diff stdout expected + +rm input stdout expected + + + # Test broken guards in input cat >input < stdout 2>stderr -cat >expected <expected <<\EOF +input:9.16: syntax error, unexpected $undefined, expecting fi or ':' EOF grep input: stderr >> stderrfilt diff stderrfilt expected