diff --git a/ChangeLog b/ChangeLog index 27f4d79fc..23e43a8d9 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,13 @@ +2010-11-06 Alexandre Duret-Lutz + + Remove `readsave' and fix line numbers in tgbaparse error messages. + + * src/tgbaparse/tgbaparse.yy (line): Fix computation of line number + for error messages when parsing conditions. + * src/tgbatest/readsave.test: Check the syntax position of syntax errors + in the diagnostics. Use ltl2tgba instead of readsave. + * src/tgbatest/Makefile.am (check_PROGRAMS): Remove readsave. + 2010-11-06 Alexandre Duret-Lutz * bench/emptchk/pml2tgba.pl: Adjust to work with Spin 5.2.5. diff --git a/src/tgbaparse/tgbaparse.yy b/src/tgbaparse/tgbaparse.yy index 351d80622..93a3bca23 100644 --- a/src/tgbaparse/tgbaparse.yy +++ b/src/tgbaparse/tgbaparse.yy @@ -118,13 +118,12 @@ line: strident ',' strident ',' condition ',' acc_list ';' i != pel.end(); ++i) { // Adjust the diagnostic to the current position. - location here = @1; - here.begin.line += i->first.begin.line; + location here = @5; + here.end.line = here.begin.line + i->first.end.line - 1; + here.end.column = + here.begin.column + i->first.end.column; + here.begin.line += i->first.begin.line - 1; here.begin.column += i->first.begin.column; - here.end.line = - here.begin.line + i->first.begin.line; - here.end.column = - here.begin.column + i->first.begin.column; error_list.push_back(spot::tgba_parse_error(here, i->second)); } diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 9338091b8..bea274f50 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -40,7 +40,6 @@ check_PROGRAMS = \ ltlprod \ mixprod \ powerset \ - readsave \ reductgba \ reduccmp \ taatgba \ @@ -60,7 +59,6 @@ ltlprod_SOURCES = ltlprod.cc mixprod_SOURCES = mixprod.cc powerset_SOURCES = powerset.cc randtgba_SOURCES = randtgba.cc -readsave_SOURCES = readsave.cc reductgba_SOURCES = reductgba.cc reduccmp_SOURCES = reductgba.cc reduccmp_CXXFLAGS = -DREDUCCMP diff --git a/src/tgbatest/readsave.cc b/src/tgbatest/readsave.cc deleted file mode 100644 index 241387805..000000000 --- a/src/tgbatest/readsave.cc +++ /dev/null @@ -1,86 +0,0 @@ -// Copyright (C) 2008 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 et Marie Curie. -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 2 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with Spot; see the file COPYING. If not, write to the Free -// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA -// 02111-1307, USA. - -#include -#include -#include -#include -#include "tgbaparse/public.hh" -#include "tgba/tgbaexplicit.hh" -#include "tgbaalgos/save.hh" -#include "ltlast/allnodes.hh" - -void -syntax(char* prog) -{ - std::cerr << prog << " [-d] filename" << std::endl; - exit(2); -} - -int -main(int argc, char** argv) -{ - int exit_code = 0; - - if (argc < 2) - syntax(argv[0]); - - bool debug = false; - int filename_index = 1; - - if (!strcmp(argv[1], "-d")) - { - debug = true; - if (argc < 3) - syntax(argv[0]); - filename_index = 2; - } - - spot::bdd_dict* dict = new spot::bdd_dict(); - - spot::ltl::environment& env(spot::ltl::default_environment::instance()); - spot::tgba_parse_error_list pel; - spot::tgba_explicit* a = spot::tgba_parse(argv[filename_index], - pel, dict, env, env, debug); - - exit_code = - spot::format_tgba_parse_errors(std::cerr, argv[filename_index], pel); - - if (a) - { - spot::tgba_save_reachable(std::cout, a); - delete a; - } - else - { - exit_code = 1; - } - - delete dict; - assert(spot::ltl::atomic_prop::instance_count() == 0); - assert(spot::ltl::unop::instance_count() == 0); - assert(spot::ltl::binop::instance_count() == 0); - assert(spot::ltl::multop::instance_count() == 0); - - return exit_code; -} diff --git a/src/tgbatest/readsave.test b/src/tgbatest/readsave.test index 54a69be36..46592e434 100755 --- a/src/tgbatest/readsave.test +++ b/src/tgbatest/readsave.test @@ -1,5 +1,5 @@ #!/bin/sh -# 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 @@ -34,7 +34,7 @@ s1, "s2", "a&!b", c d; "state 3", s1,,; EOF -../readsave input > stdout +../ltl2tgba -b -X input > stdout cat >expected <<\EOF acc = "c" "d"; @@ -50,7 +50,7 @@ sed 's/"d" "c"/"c" "d"/g;s/!b & a/a \& !b/g' stdout > tmp_ && mv tmp_ stdout diff stdout expected mv stdout input -run 0 ../readsave input > stdout +run 0 ../ltl2tgba -b -X input > stdout # Sort out some possible inversions in the output. # (The order is not guaranteed by SPOT.) @@ -66,10 +66,32 @@ run 0 ../randtgba -t 1 -n 20 -d 0.2 a b -a 2 0.1 >input sed 's/"b & a"/"a \& b"/g;s/"a1" "a0"/"a0" "a1"/g' input > tmp_ && mv tmp_ input cat input -run 0 ../readsave input > stdout +run 0 ../ltl2tgba -b -X input > stdout sed 's/"b & a"/"a \& b"/g;s/"a1" "a0"/"a0" "a1"/g' stdout > tmp_ && mv tmp_ stdout diff input stdout rm -f input stdout + + +# Check the position of syntax errors in the diagnostics: +cat >input <<\EOF +acc = "c" "d"; +"s1", "s2", "a & !b", "c" "d"; +"s2", "state 3", "a &&", "c"; +"state 3", "s1", "1)",; +EOF + +run 2 ../ltl2tgba -b -X input > stdout 2>stderr +cat stderr +grep input: stderr > stderrfilt + +cat >expected <