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.

ChangeLog

@@ -1,3 +1,13 @@
+2010-11-06  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	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  <adl@lrde.epita.fr>
 
 	* bench/emptchk/pml2tgba.pl: Adjust to work with Spin 5.2.5.

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;
+		     location here = @5;
-		     here.begin.line += i->first.begin.line;
+		     here.end.line = here.begin.line + i->first.end.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;
+		       here.begin.column + i->first.end.column;
+		     here.begin.line += i->first.begin.line - 1;
+		     here.begin.column += i->first.begin.column;
 		     error_list.push_back(spot::tgba_parse_error(here,
 								 i->second));
 		   }

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

src/tgbatest/readsave.cc

@@ -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 <iostream>
-#include <cassert>
-#include <cstdlib>
-#include <cstring>
-#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;
-}

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 <<EOF
+input:3.23-22: syntax error, unexpected end of formula
+input:3.21-22: missing right operand for "and operator"
+input:4.20: syntax error, unexpected closing parenthesis
+input:4.20: ignoring trailing garbage
+EOF
+
+diff stderrfilt expected