diff --git a/ChangeLog b/ChangeLog index 5cfaad691..550e7a87e 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,15 @@ +2011-01-06 Alexandre Duret-Lutz + + The neverclaim output by spin -f '([]a && XXXX!a)' was not + understood by Spot. + + * src/neverparse/neverclaimparse.yy: Support "if :: false fi;" + instructions. Spin sometimes output these on dead states. + Also rewrite the "transitions" rule as a left recursion. + * src/tgbatest/neverclaimread.test: Adjust output because + of the right->left recursion change, and add two more formula + to submit to Spin to test its output. + 2011-01-06 Alexandre Duret-Lutz Speed up computation of non_final states for minimize_wdba. diff --git a/src/neverparse/neverclaimparse.yy b/src/neverparse/neverclaimparse.yy index e08758cbe..a849cdb1a 100644 --- a/src/neverparse/neverclaimparse.yy +++ b/src/neverparse/neverclaimparse.yy @@ -1,4 +1,4 @@ -/* Copyright (C) 2010 Laboratoire de Recherche et Développement +/* Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement ** de l'Epita (LRDE). ** ** This file is part of Spot, a model checking library. @@ -71,7 +71,7 @@ using namespace spot::ltl; %token FALSE "false" %token FORMULA "boolean formula" %token IDENT "identifier" -%type formula +%type formula opt_dest %type

transition %type transitions %type ident_list @@ -88,7 +88,11 @@ using namespace spot::ltl; } delete $$; } -%printer { debug_stream() << *$$; } + %printer { + if ($$) + debug_stream() << *$$; + else + debug_stream() << "\"\""; } %% neverclaim: @@ -101,7 +105,7 @@ states: | states ';' state | states ';' -ident_list: +ident_list: IDENT ':' { $$ = $1; @@ -119,7 +123,7 @@ state: 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, + result->add_acceptance_condition(t, spot::ltl::constant::true_instance()); delete $1; } @@ -133,7 +137,7 @@ state: { spot::tgba_explicit::transition* t = result->create_transition(*$1,*it->second); - + result->add_condition(t, it->first); if (acc) result @@ -150,35 +154,60 @@ state: transitions: /* empty */ { $$ = new std::list; } - | transition transitions + | transitions transition { - $2->push_back(*$1); - delete $1; - $$ = $2; + if ($2) + { + $1->push_back(*$2); + delete $2; + } + $$ = $1; } formula: FORMULA | "false" { $$ = new std::string("0"); } - -transition: - ':' ':' formula "->" "goto" IDENT - { - 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); +opt_dest: + /* empty */ + { + $$ = 0; + } + | "->" "goto" IDENT + { + $$ = $3; + } + +transition: + ':' ':' formula opt_dest + { + // If there is no destination, do ignore the transition. + // This happens for instance with + // if + // :: false + // fi + if (!$4) + { + delete $3; + $$ = 0; + } + else + { + 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, $4); + } } %% diff --git a/src/tgbatest/neverclaimread.test b/src/tgbatest/neverclaimread.test index 28ec275a2..3aac302be 100755 --- a/src/tgbatest/neverclaimread.test +++ b/src/tgbatest/neverclaimread.test @@ -1,5 +1,5 @@ #!/bin/sh -# Copyright (C) 2010 Laboratoire de Recherche et Développement +# Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -48,11 +48,11 @@ digraph G { 0 [label="", style=invis, height=0] 0 -> 1 1 [label="T2_init"] - 1 -> 2 [label="p0 & p1\n"] 1 -> 1 [label="1\n"] + 1 -> 2 [label="p0 & p1\n"] 2 [label="T1"] - 2 -> 2 [label="p1\n"] 2 -> 3 [label="p1 & !p0\n"] + 2 -> 2 [label="p1\n"] 3 [label="accept_all"] 3 -> 3 [label="1\n{Acc[1]}"] } @@ -101,6 +101,8 @@ a X false ([] a) U X b (a U b) U (c U d) +true +([]a && XXXX!a) EOF while read f do