diff --git a/ChangeLog b/ChangeLog index c168cdc72..ad5ecfb2b 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,24 @@ +2010-11-06 Alexandre Duret-Lutz + + Make sure the neverclaim parser works on the output of spin and + ltl2ba. + + * src/neverparse/neverclaimparse.yy: Accept multiple labels + for the same state. Honor accepting states. Forward parse + error from the parser used for guards. Accept "false" as a + single instruction for a state. + * src/neverparse/neverclaimscan.ll: Recognize "false" specifically, + and remove the ";" hack. + * src/tgba/tgbaexplicit.cc + (tgba_explicit_string::~tgba_explicit_string): Adjust not to + destroy a state twice. + * src/tgba/tgbaexplicit.hh + (tgba_explicit_string::add_state_alias): New function. + * src/tgbatest/defs.in (SPIN, LTL2BA): New variables. + * src/tgbatest/neverclaimread.test: Check error messages for + syntax errors in guards. Make sure we can read the output + of `spin -f' and `ltl2ba -f' on a few test formulae. + 2010-11-06 Alexandre Duret-Lutz Cleanup neverclaim support. diff --git a/src/neverparse/neverclaimparse.yy b/src/neverparse/neverclaimparse.yy index e753ad69c..e08758cbe 100644 --- a/src/neverparse/neverclaimparse.yy +++ b/src/neverparse/neverclaimparse.yy @@ -30,8 +30,11 @@ %code requires { #include +#include +#include "ltlast/constant.hh" #include "public.hh" -typedef std::pair pair; + + typedef std::pair pair; } %parse-param {spot::neverclaim_parse_error_list& error_list} @@ -65,18 +68,22 @@ using namespace spot::ltl; %token FI "fi" %token ARROW "->" %token GOTO "goto" -%token FORMULA -%token IDENT +%token FALSE "false" +%token FORMULA "boolean formula" +%token IDENT "identifier" +%type formula %type

transition %type transitions +%type ident_list + %destructor { delete $$; } -%destructor { delete $$->first; delete $$->second; delete $$; }

+%destructor { $$->first->destroy(); delete $$->second; delete $$; }

%destructor { for (std::list::iterator i = $$->begin(); i != $$->end(); ++i) { - delete i->first; + i->first->destroy(); delete i->second; } delete $$; @@ -86,42 +93,60 @@ using namespace spot::ltl; %% neverclaim: "never" '{' states '}' -; + states: /* empty */ - | state states -; + | state + | states ';' state + | states ';' + +ident_list: + IDENT ':' + { + $$ = $1; + } + | ident_list IDENT ':' + { + result->add_state_alias(*$2, *$1); + delete $1; + $$ = $2; + } state: - IDENT ':' "skip" + ident_list "skip" { - result->create_transition(*$1, *$1); + spot::tgba_explicit::transition* t = result->create_transition(*$1, *$1); + bool acc = !strncmp("accept", $1->c_str(), 6); + if (acc) + result->add_acceptance_condition(t, + spot::ltl::constant::true_instance()); delete $1; } - | IDENT ':' { delete $1; } - | IDENT ':' "if" transitions "fi" + | ident_list { delete $1; } + | ident_list "false" { delete $1; } + | ident_list "if" transitions "fi" { std::list::iterator it; - for (it = $4->begin(); it != $4->end(); ++it) + bool acc = !strncmp("accept", $1->c_str(), 6); + for (it = $3->begin(); it != $3->end(); ++it) { spot::tgba_explicit::transition* t = result->create_transition(*$1,*it->second); - spot::ltl::parse_error_list pel; - spot::ltl::formula* f = spot::ltl::parse(*(it->first), pel); - result->add_condition(t, f); + + result->add_condition(t, it->first); + if (acc) + result + ->add_acceptance_condition(t, spot::ltl::constant::true_instance()); } // Free the list delete $1; - for (std::list::iterator it = $4->begin(); - it != $4->end(); ++it) - { - delete it->first; + for (std::list::iterator it = $3->begin(); + it != $3->end(); ++it) delete it->second; - } - delete $4; + delete $3; } -; + transitions: /* empty */ { $$ = new std::list; } @@ -131,12 +156,29 @@ transitions: delete $1; $$ = $2; } -; + +formula: FORMULA | "false" { $$ = new std::string("0"); } + transition: - ':' ':' FORMULA "->" "goto" IDENT + ':' ':' formula "->" "goto" IDENT { - $$ = new pair($3, $6); + spot::ltl::parse_error_list pel; + spot::ltl::formula* f = spot::ltl::parse(*$3, pel); + delete $3; + 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; + 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, $6); } %% @@ -164,11 +206,11 @@ namespace spot return 0; } tgba_explicit_string* result = new tgba_explicit_string(dict); + result->declare_acceptance_condition(spot::ltl::constant::true_instance()); neverclaimyy::parser parser(error_list, env, result); parser.set_debug_level(debug); parser.parse(); neverclaimyyclose(); - result->merge_transitions(); return result; } } diff --git a/src/neverparse/neverclaimscan.ll b/src/neverparse/neverclaimscan.ll index a7c128797..64b880aad 100644 --- a/src/neverparse/neverclaimscan.ll +++ b/src/neverparse/neverclaimscan.ll @@ -49,17 +49,17 @@ eol \n|\r|\n\r|\r\n "/*".*"*/" yylloc->step(); "never" return token::NEVER; -"skip"|"skip;" return token::SKIP; +"skip" return token::SKIP; "if" return token::IF; -"fi"|"fi;" return token::FI; +"fi" return token::FI; "->" return token::ARROW; "goto" return token::GOTO; +"false"|"0" return token::FALSE; -"(".*")"|"true"|"1"|"false"|"0" { - yylval->str = - new std::string(yytext, yyleng); - return token::FORMULA; - } +"(".*")"|"true"|"1" { + yylval->str = new std::string(yytext, yyleng); + return token::FORMULA; + } [a-zA-Z][a-zA-Z0-9_]* { yylval->str = new std::string(yytext, yyleng); diff --git a/src/tgba/tgbaexplicit.cc b/src/tgba/tgbaexplicit.cc index 0a225e2ad..2aeaa0991 100644 --- a/src/tgba/tgbaexplicit.cc +++ b/src/tgba/tgbaexplicit.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2010 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 @@ -291,10 +291,14 @@ namespace spot ns_map::iterator i; for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i) { - tgba_explicit::state::iterator i2; - for (i2 = i->second->begin(); i2 != i->second->end(); ++i2) - delete *i2; - delete i->second; + // Do not erase the same state twice. (Because of possible aliases.) + if (state_name_map_.erase(i->second)) + { + tgba_explicit::state::iterator i2; + for (i2 = i->second->begin(); i2 != i->second->end(); ++i2) + delete *i2; + delete i->second; + } } } diff --git a/src/tgba/tgbaexplicit.hh b/src/tgba/tgbaexplicit.hh index 4f38c4bdf..2b8519019 100644 --- a/src/tgba/tgbaexplicit.hh +++ b/src/tgba/tgbaexplicit.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2010 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), @@ -212,7 +212,7 @@ namespace spot } return i->second; } - + state* set_init_state(const label& state) { @@ -323,6 +323,15 @@ namespace spot virtual ~tgba_explicit_string(); virtual state* add_default_init(); virtual std::string format_state(const spot::state* s) const; + + /// Create an alias for a state. Any reference to \a alias_name + /// will act as a reference to \a real_name. + virtual + void add_state_alias(const std::string& alias_name, + const std::string& real_name) + { + name_state_map_[alias_name] = add_state(real_name); + } }; class tgba_explicit_formula: diff --git a/src/tgbatest/defs.in b/src/tgbatest/defs.in index 7923b14b6..fccf16cd0 100644 --- a/src/tgbatest/defs.in +++ b/src/tgbatest/defs.in @@ -1,5 +1,5 @@ # -*- shell-script -*- -# Copyright (C) 2009 Laboratoire de Recherche et Développement +# Copyright (C) 2009, 2010 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 @@ -65,6 +65,8 @@ top_builddir='../@top_builddir@' LBTT="@LBTT@" LBTT_TRANSLATE="@LBTT_TRANSLATE@" VALGRIND='@VALGRIND@' +SPIN='@SPIN@' +LTL2BA='@LTL2BA@' run() { diff --git a/src/tgbatest/neverclaimread.test b/src/tgbatest/neverclaimread.test index de6e11e28..28d72a7d8 100755 --- a/src/tgbatest/neverclaimread.test +++ b/src/tgbatest/neverclaimread.test @@ -54,7 +54,7 @@ digraph G { 2 -> 2 [label="p1\n"] 2 -> 3 [label="p1 & !p0\n"] 3 [label="accept_all"] - 3 -> 3 [label="1\n"] + 3 -> 3 [label="1\n{Acc[1]}"] } EOF @@ -65,3 +65,55 @@ sed -e 's/!p0 & p1/p1 \& !p0/g' -e 's/p1 & p0/p0 \& p1/g' stdout \ diff stdout expected rm input stdout expected + + +# Test broken guards in input +cat >input < goto T2_init +:: (p1 && ) -> goto T1 +fi; +T1: +if +:: (p1 && ! p0)) -> goto accept_all +:: (p1) -> goto T1 +fi; +accept_all: +skip +} +EOF + +run 2 ../ltl2tgba -XN input > stdout 2>stderr +cat >expected <> stderrfilt +diff stderrfilt expected + +# Skip the rest of this test if neither Spin nor ltl2ba are installed. +test -n "$SPIN$LTL2BA" || exit + +cat >formulae<[] a +X false +([] a) U X b +(a U b) U (c U d) +EOF +while read f +do + run 0 ../ltl2tgba -b -f "!($f)" > f.tgba + if test -n "$SPIN"; then + $SPIN -f "$f" > f.spin + run 0 ../ltl2tgba -E -Pf.tgba -XN f.spin + fi + if test -n "$LTL2BA"; then + $LTL2BA -f "$f" > f.ltl2ba + run 0 ../ltl2tgba -E -Pf.tgba -XN f.ltl2ba + fi +done