Cleanup neverclaim support.

* src/neverclaimparse/: Shorthen as ...
* src/neverparse/:... this.
* src/Makefile.am: Adjust, and add back the directories mistakenly
removed by previous patch.
* README: Adjust, and keep the file's width under 80 columns.
* configure.ac: Adjust.
* src/neverparse/Makefile.am, src/neverparse/fmterror.cc,
src/neverparse/neverclaimparse.yy,
src/neverparse/neverclaimscan.ll, src/neverparse/public.hh:
Fix copyright.
* src/tgbatest/Makefile.am (check_PROGRAMS): Remove neverclaimread.
* src/tgbatest/ltl2tgba.cc: Add option -XN to read a neverclaim.
* src/tgbatest/readneverclaim.cc: Delete.
* src/tgbatest/neverclaimread.test: Use ltl2tgba instead of
neverclaimread.

ChangeLog

@@ -1,3 +1,23 @@
+2010-11-06  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Cleanup neverclaim support.
+
+	* src/neverclaimparse/: Shorthen as ...
+	* src/neverparse/:... this.
+	* src/Makefile.am: Adjust, and add back the directories mistakenly
+	removed by previous patch.
+	* README: Adjust, and keep the file's width under 80 columns.
+	* configure.ac: Adjust.
+	* src/neverparse/Makefile.am, src/neverparse/fmterror.cc, 
+	src/neverparse/neverclaimparse.yy, 
+	src/neverparse/neverclaimscan.ll, src/neverparse/public.hh: 
+	Fix copyright.
+	* src/tgbatest/Makefile.am (check_PROGRAMS): Remove neverclaimread.
+	* src/tgbatest/ltl2tgba.cc: Add option -XN to read a neverclaim.
+	* src/tgbatest/readneverclaim.cc: Delete.
+	* src/tgbatest/neverclaimread.test: Use ltl2tgba instead of
+	neverclaimread.
+
 2010-05-25  Felix Abecassis  <abecassis@lrde.epita.fr>
 
 	Add never claim parser.

README

@@ -105,47 +105,47 @@ Layout of the source tree
 Core directories
 ----------------
 
-src/			Sources for libspot.
+src/              Sources for libspot.
-   kripke/	  	Kripke Structure interface.
+   kripke/        Kripke Structure interface.
-   ltlast/        	LTL abstract syntax tree (including nodes for ELTL).
+   ltlast/        LTL abstract syntax tree (including nodes for ELTL).
-   ltlenv/        	LTL environments.
+   ltlenv/        LTL environments.
-   ltlparse/      	Parser for LTL formulae.
+   ltlparse/      Parser for LTL formulae.
-   ltlvisit/      	Visitors of LTL formulae.
+   ltlvisit/      Visitors of LTL formulae.
-   ltltest/       	Tests for ltlast/, ltlenv/, ltlparse/, and ltlvisit/.
+   ltltest/       Tests for ltlast/, ltlenv/, ltlparse/, and ltlvisit/.
-   misc/          	Miscellaneous support files.
+   misc/          Miscellaneous support files.
-   tgba/          	TGBA objects and cousins.
+   tgba/          TGBA objects and cousins.
-   tgbaalgos/     	Algorithms on TGBA.
+   tgbaalgos/     Algorithms on TGBA.
-      gtec/       	Couvreur's Emptiness-Check.
+      gtec/       Couvreur's Emptiness-Check.
-   tgbaparse/     	Parser for explicit TGBA.
+   tgbaparse/     Parser for explicit TGBA.
-   tgbatest/      	Tests for tgba/, tgbaalgos/, and tgbaparse/.
+   tgbatest/      Tests for tgba/, tgbaalgos/, and tgbaparse/.
-   evtgba*/       	Ignore these for now.
+   evtgba*/       Ignore these for now.
-   eltlparse/	  	Parser for ELTL formulae.
+   eltlparse/     Parser for ELTL formulae.
-   eltltest/      	Tests for ELTL nodes in ltlast/ and eltlparse/.
+   eltltest/      Tests for ELTL nodes in ltlast/ and eltlparse/.
-   saba/          	SABA (State-labeled Alternating Büchi Automata) objects.
+   saba/          SABA (State-labeled Alternating Büchi Automata) objects.
-   sabaalgos/     	Algorithms on SABA.
+   sabaalgos/     Algorithms on SABA.
-   sabatest/      	Tests for saba/, sabaalgos/.
+   sabatest/      Tests for saba/, sabaalgos/.
-   neverclaimparse/	Parser for SPIN never claim.
+   neverparse/    Parser for SPIN never claims.
-   sanity/		Sanity tests for the whole project.
+   sanity/        Sanity tests for the whole project.
-doc/	          	Documentation for libspot.
+doc/              Documentation for libspot.
-   spot.html/     	HTML reference manual.
+   spot.html/     HTML reference manual.
-   spot.latex/    	Sources for the PDF manual. (Not distributed, can be rebuilt.)
+   spot.latex/    Sources for the PDF manual. (Not distributed, can be rebuilt.)
-   spotref.pdf    	PDF reference manual.
+   spotref.pdf    PDF reference manual.
-bench/            	Benchmarks for ...
+bench/            Benchmarks for ...
-   emptchk/       	... emptiness-check algorithms,
+   emptchk/       ... emptiness-check algorithms,
-   gspn-ssp/      	... various symmetry-based methods with GreatSPN,
+   gspn-ssp/      ... various symmetry-based methods with GreatSPN,
-   ltl2tgba/      	... LTL-to-Büchi translation algorithms,
+   ltl2tgba/      ... LTL-to-Büchi translation algorithms,
-   ltlcounter/    	... translation of a class of LTL formulae,
+   ltlcounter/    ... translation of a class of LTL formulae,
-   scc-stats/     	... SCC statistics after translation of LTL formulae,
+   scc-stats/     ... SCC statistics after translation of LTL formulae,
-   split-product/ 	... parallelizing gain after splitting LTL automata.
+   split-product/ ... parallelizing gain after splitting LTL automata.
-wrap/	          	Wrappers for other languages.
+wrap/             Wrappers for other languages.
-   python/        	Python bindings for Spot and BuDDy
+   python/        Python bindings for Spot and BuDDy
-      tests/      	Tests for these bindings
+      tests/      Tests for these bindings
-      cgi-bin/    	Python-based CGI script (ltl-to-tgba translator)
+      cgi-bin/    Python-based CGI script (ltl-to-tgba translator)
-iface/	          	Interfaces to other libraries.
+iface/            Interfaces to other libraries.
-   gspn/          	GreatSPN interface.
+   gspn/          GreatSPN interface.
-      examples/   	Supporting models used by the test cases.
+      examples/   Supporting models used by the test cases.
-   nips/          	NIPS interface (to use Promela models).
+   nips/          NIPS interface (to use Promela models).
-      nipstest/   	Tests for NIPS.
+      nipstest/   Tests for NIPS.
 
 Third party software
 --------------------

configure.ac

@@ -113,7 +113,7 @@ AC_CONFIG_FILES([
   src/ltlvisit/Makefile
   src/Makefile
   src/misc/Makefile
-  src/neverclaimparse/Makefile
+  src/neverparse/Makefile
   src/sanity/Makefile
   src/saba/Makefile
   src/sabaalgos/Makefile

src/Makefile.am

@@ -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
@@ -28,8 +28,8 @@ AUTOMAKE_OPTIONS = subdir-objects
 # libspot.la needed by the tests).
 SUBDIRS = misc ltlenv ltlast ltlvisit ltlparse eltlparse tgba		\
           tgbaalgos tgbaparse evtgba evtgbaalgos evtgbaparse kripke	\
-          neverclaimparse . ltltest eltltest tgbatest evtgbatest	\
+          saba sabaalgos neverparse . ltltest eltltest tgbatest		\
-          sabatest sanity
+          evtgbatest sabatest sanity
 
 lib_LTLIBRARIES = libspot.la
 libspot_la_SOURCES =
@@ -44,7 +44,7 @@ libspot_la_LIBADD =  \
   tgba/libtgba.la \
   tgbaalgos/libtgbaalgos.la \
   tgbaparse/libtgbaparse.la \
-  neverclaimparse/libneverclaimparse.la \
+  neverparse/libneverclaimparse.la \
   evtgba/libevtgba.la \
   evtgbaalgos/libevtgbaalgos.la \
   evtgbaparse/libevtgbaparse.la \

src/neverparse/Makefile.am

@@ -1,8 +1,5 @@
-## Copyright (C) 2008, 2009 Laboratoire de Recherche et Développement
+## Copyright (C) 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 et Marie Curie.
 ##
 ## This file is part of Spot, a model checking library.
 ##

src/neverparse/fmterror.cc

@@ -1,6 +1,5 @@
-// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2010 Laboratoire de Recherche et Développement de
-// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// l'Epita (LRDE).
-// et Marie Curie.
 //
 // This file is part of Spot, a model checking library.
 //

src/neverparse/neverclaimparse.yy

@@ -1,8 +1,5 @@
-/* Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
+/* Copyright (C) 2010 Laboratoire de Recherche et Développement
 ** de l'Epita (LRDE).
-** Copyright (C) 2003, 2004, 2005, 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.
 **

src/neverparse/neverclaimscan.ll

@@ -1,6 +1,5 @@
-/* Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+/* Copyright (C) 2010 Laboratoire de Recherche et Développement de
-** département Systèmes Répartis Coopératifs (SRC), Université Pierre
+** l'Epita (LRDE).
-** et Marie Curie.
 **
 ** This file is part of Spot, a model checking library.
 **
@@ -25,7 +24,7 @@
 
 %{
 #include <string>
-#include "neverclaimparse/parsedecl.hh"
+#include "neverparse/parsedecl.hh"
 
 #define YY_USER_ACTION \
   yylloc->columns(yyleng);

src/neverparse/public.hh

@@ -1,6 +1,5 @@
-// Copyright (C) 2003, 2004, 2005, 2006, 2009 Laboratoire
+// Copyright (C) 2010 Laboratoire de Recherche et Développement de
-// d'Informatique de Paris 6 (LIP6), département Systèmes Répartis
+// l'Epita (LRDE).
-// Coopératifs (SRC), Université Pierre et Marie Curie.
 //
 // This file is part of Spot, a model checking library.
 //
@@ -26,7 +25,7 @@
 // Unfortunately Bison 2.3 uses the same guards in all parsers :(
 # undef BISON_LOCATION_HH
 # undef BISON_POSITION_HH
-# include "neverclaimparse/location.hh"
+# include "neverparse/location.hh"
 # include "ltlenv/defaultenv.hh"
 # include <string>
 # include <list>

src/tgbatest/Makefile.am

@@ -39,7 +39,6 @@ check_PROGRAMS = \
   explprod \
   ltlprod \
   mixprod \
-  neverclaimread \
   powerset \
   reductgba \
   reduccmp \
@@ -58,7 +57,6 @@ explprod_SOURCES = explprod.cc
 ltl2tgba_SOURCES = ltl2tgba.cc
 ltlprod_SOURCES  = ltlprod.cc
 mixprod_SOURCES  = mixprod.cc
-neverclaimread_SOURCES = neverclaimread.cc
 powerset_SOURCES = powerset.cc
 randtgba_SOURCES = randtgba.cc
 reductgba_SOURCES = reductgba.cc

src/tgbatest/ltl2tgba.cc

@@ -45,6 +45,7 @@
 #include "tgba/futurecondcol.hh"
 #include "tgbaalgos/reducerun.hh"
 #include "tgbaparse/public.hh"
+#include "neverparse/public.hh"
 #include "tgbaalgos/dupexp.hh"
 #include "tgbaalgos/neverclaim.hh"
 #include "tgbaalgos/reductgba_sim.hh"
@@ -105,6 +106,8 @@ syntax(char* prog)
 	    << std::endl
 	    << "  -X    do not compute an automaton, read it from a file"
 	    << std::endl
+	    << "  -XN   do not compute an automaton, read it from a"
+	    << " neverclaim file" << std::endl
 	    << "  -Pfile  multiply the formula automaton with the automaton"
 	    << " from `file'"
 	    << std::endl
@@ -285,6 +288,7 @@ main(int argc, char** argv)
   enum { NoneDup, BFS, DFS } dupexp = NoneDup;
   bool expect_counter_example = false;
   bool from_file = false;
+  bool read_neverclaim = false;
   int reduc_aut = spot::Reduce_None;
   int redopt = spot::ltl::Reduce_None;
   bool scc_filter_all = false;
@@ -635,6 +639,11 @@ main(int argc, char** argv)
 	{
 	  from_file = true;
 	}
+      else if (!strcmp(argv[formula_index], "-XN"))
+	{
+	  from_file = true;
+	  read_neverclaim = true;
+	}
       else if (!strcmp(argv[formula_index], "-y"))
 	{
 	  translation = TransFM;
@@ -738,17 +747,34 @@ main(int argc, char** argv)
 
       if (from_file)
 	{
-	  spot::tgba_parse_error_list pel;
 	  spot::tgba_explicit_string* e;
-	  tm.start("parsing automaton");
+	  if (!read_neverclaim)
-	  to_free = a = e = spot::tgba_parse(input, pel, dict,
-					     env, env, debug_opt);
-	  tm.stop("parsing automaton");
-	  if (spot::format_tgba_parse_errors(std::cerr, input, pel))
 	    {
-	      delete to_free;
+	      spot::tgba_parse_error_list pel;
-	      delete dict;
+	      tm.start("parsing automaton");
-	      return 2;
+	      to_free = a = e = spot::tgba_parse(input, pel, dict,
+						 env, env, debug_opt);
+	      tm.stop("parsing automaton");
+	      if (spot::format_tgba_parse_errors(std::cerr, input, pel))
+		{
+		  delete to_free;
+		  delete dict;
+		  return 2;
+		}
+	    }
+	  else
+	    {
+	      spot::neverclaim_parse_error_list pel;
+	      tm.start("parsing never claim");
+	      to_free = a = e = spot::neverclaim_parse(input, pel, dict, 
+						       env, debug_opt);	      
+	      tm.stop("parsing never claim");
+	      if (spot::format_neverclaim_parse_errors(std::cerr, input, pel))
+		{
+		  delete to_free;
+		  delete dict;
+		  return 2;
+		}	      
 	    }
 	  e->merge_transitions();
 	}

src/tgbatest/neverclaimread.cc

@@ -1,85 +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 "neverclaimparse/public.hh"
-#include "tgba/tgbaexplicit.hh"
-#include "tgbaalgos/dotty.hh"
-#include "ltlast/allnodes.hh"
-
-void
-syntax(char* prog)
-{
-  std::cerr << prog << " [-d] filename" << std::endl;
-  exit(2);
-}
-
-int
-main(int argc, char** argv)
-{
-  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::neverclaim_parse_error_list pel;
-  spot::tgba_explicit* a = spot::neverclaim_parse(argv[filename_index],
-						  pel, dict, env, debug);
-
-  if (spot::format_neverclaim_parse_errors(std::cerr, argv[filename_index],
-					   pel))
-    return 2;
-
-  if (a)
-  {
-    spot::dotty_reachable(std::cout, a);
-    delete a;
-  }
-  else
-  {
-    return 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 0;
-}

src/tgbatest/neverclaimread.test

@@ -1,9 +1,6 @@
 #!/bin/sh
-# Copyright (C) 2009 Laboratoire de Recherche et Développement
+# Copyright (C) 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
-# et Marie Curie.
 #
 # This file is part of Spot, a model checking library.
 #
@@ -44,7 +41,7 @@ skip
 }
 EOF
 
-run 0 ../neverclaimread input > stdout
+run 0 ../ltl2tgba -XN input > stdout
 
 cat >expected <<EOF
 digraph G {