diff --git a/ChangeLog b/ChangeLog index aaeb8f84d..7173a79c7 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,27 +1,3 @@ -2010-05-25 Felix Abecassis - - Add never claim parser. - - * src/neverclaimparse/: New directory. - * src/neverclaimparse/fmterror.cc: New file. Print a formatted parse - error on a output stream. - * src/neverclaimparse/neverclaimparse.yy: New file. Parser declaration - for Bison. - * src/neverclaimparse/neverclaimscan.ll: New file. Scanner declaration - for Flex. - * src/neverclaimparse/public.hh: New file. Public header for external - use. - * src/neverclaimparse/parsedecl.hh: New file. Header file for - Flex-Bison interaction. - * src/neverclaimparse/Makefile.am: New Makefile. - * src/tgbatest/neverclaimread.cc: New file. Test program for the - never claim parser. - * src/tgbatest/neverclaimread.test: New file. Test script for the - never claim parser. - * src/tgbatest/Makefile.am: Adjust. - * configure.ac : Adjust. - * README: Adjust. - 2010-05-20 Alexandre Duret-Lutz Fix the --enable-optimizations check. diff --git a/README b/README index 0358ecc21..e00bd2430 100644 --- a/README +++ b/README @@ -105,47 +105,46 @@ Layout of the source tree Core directories ---------------- -src/ Sources for libspot. - kripke/ Kripke Structure interface. - ltlast/ LTL abstract syntax tree (including nodes for ELTL). - ltlenv/ LTL environments. - ltlparse/ Parser for LTL formulae. - ltlvisit/ Visitors of LTL formulae. - ltltest/ Tests for ltlast/, ltlenv/, ltlparse/, and ltlvisit/. - misc/ Miscellaneous support files. - tgba/ TGBA objects and cousins. - tgbaalgos/ Algorithms on TGBA. - gtec/ Couvreur's Emptiness-Check. - tgbaparse/ Parser for explicit TGBA. - tgbatest/ Tests for tgba/, tgbaalgos/, and tgbaparse/. - evtgba*/ Ignore these for now. - eltlparse/ Parser for ELTL formulae. - eltltest/ Tests for ELTL nodes in ltlast/ and eltlparse/. - saba/ SABA (State-labeled Alternating Büchi Automata) objects. - sabaalgos/ Algorithms on SABA. - sabatest/ Tests for saba/, sabaalgos/. - neverclaimparse/ Parser for SPIN never claim. - sanity/ Sanity tests for the whole project. -doc/ Documentation for libspot. - spot.html/ HTML reference manual. - spot.latex/ Sources for the PDF manual. (Not distributed, can be rebuilt.) - spotref.pdf PDF reference manual. -bench/ Benchmarks for ... - emptchk/ ... emptiness-check algorithms, - gspn-ssp/ ... various symmetry-based methods with GreatSPN, - ltl2tgba/ ... LTL-to-Büchi translation algorithms, - ltlcounter/ ... translation of a class of LTL formulae, - scc-stats/ ... SCC statistics after translation of LTL formulae, - split-product/ ... parallelizing gain after splitting LTL automata. -wrap/ Wrappers for other languages. - python/ Python bindings for Spot and BuDDy - tests/ Tests for these bindings - cgi-bin/ Python-based CGI script (ltl-to-tgba translator) -iface/ Interfaces to other libraries. - gspn/ GreatSPN interface. - examples/ Supporting models used by the test cases. - nips/ NIPS interface (to use Promela models). - nipstest/ Tests for NIPS. +src/ Sources for libspot. + kripke/ Kripke Structure interface. + ltlast/ LTL abstract syntax tree (including nodes for ELTL). + ltlenv/ LTL environments. + ltlparse/ Parser for LTL formulae. + ltlvisit/ Visitors of LTL formulae. + ltltest/ Tests for ltlast/, ltlenv/, ltlparse/, and ltlvisit/. + misc/ Miscellaneous support files. + tgba/ TGBA objects and cousins. + tgbaalgos/ Algorithms on TGBA. + gtec/ Couvreur's Emptiness-Check. + tgbaparse/ Parser for explicit TGBA. + tgbatest/ Tests for tgba/, tgbaalgos/, and tgbaparse/. + evtgba*/ Ignore these for now. + eltlparse/ Parser for ELTL formulae. + eltltest/ Tests for ELTL nodes in ltlast/ and eltlparse/. + saba/ SABA (State-labeled Alternating Büchi Automata) objects. + sabaalgos/ Algorithms on SABA. + sabatest/ Tests for saba/, sabaalgos/. + sanity/ Sanity tests for the whole project. +doc/ Documentation for libspot. + spot.html/ HTML reference manual. + spot.latex/ Sources for the PDF manual. (Not distributed, can be rebuilt.) + spotref.pdf PDF reference manual. +bench/ Benchmarks for ... + emptchk/ ... emptiness-check algorithms, + gspn-ssp/ ... various symmetry-based methods with GreatSPN, + ltl2tgba/ ... LTL-to-Büchi translation algorithms, + ltlcounter/ ... translation of a class of LTL formulae, + scc-stats/ ... SCC statistics after translation of LTL formulae, + split-product/ ... parallelizing gain after splitting LTL automata. +wrap/ Wrappers for other languages. + python/ Python bindings for Spot and BuDDy + tests/ Tests for these bindings + cgi-bin/ Python-based CGI script (ltl-to-tgba translator) +iface/ Interfaces to other libraries. + gspn/ GreatSPN interface. + examples/ Supporting models used by the test cases. + nips/ NIPS interface (to use Promela models). + nipstest/ Tests for NIPS. Third party software -------------------- diff --git a/configure.ac b/configure.ac index a544c3668..226b955af 100644 --- a/configure.ac +++ b/configure.ac @@ -111,7 +111,6 @@ AC_CONFIG_FILES([ src/ltlvisit/Makefile src/Makefile src/misc/Makefile - src/neverclaimparse/Makefile src/sanity/Makefile src/saba/Makefile src/sabaalgos/Makefile diff --git a/src/Makefile.am b/src/Makefile.am index 317399510..c506fe51c 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -28,7 +28,7 @@ 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 . ltltest eltltest tgbatest evtgbatest \ sabatest sanity lib_LTLIBRARIES = libspot.la @@ -44,7 +44,6 @@ libspot_la_LIBADD = \ tgba/libtgba.la \ tgbaalgos/libtgbaalgos.la \ tgbaparse/libtgbaparse.la \ - neverclaimparse/libneverclaimparse.la \ evtgba/libevtgba.la \ evtgbaalgos/libevtgbaalgos.la \ evtgbaparse/libevtgbaparse.la \ diff --git a/src/neverclaimparse/Makefile.am b/src/neverclaimparse/Makefile.am deleted file mode 100644 index 9839e5bf0..000000000 --- a/src/neverclaimparse/Makefile.am +++ /dev/null @@ -1,66 +0,0 @@ -## Copyright (C) 2008, 2009 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. - -AM_CPPFLAGS = -I$(srcdir)/.. $(BUDDY_CPPFLAGS) -# Disable -Werror because too many versions of flex yield warnings. -AM_CXXFLAGS = $(WARNING_CXXFLAGS:-Werror=) - -neverclaimparsedir = $(pkgincludedir)/neverclaimparse - -neverclaimparse_HEADERS = \ - public.hh \ - location.hh \ - position.hh - -noinst_LTLIBRARIES = libneverclaimparse.la - -NEVERCLAIMPARSE_YY = neverclaimparse.yy -FROM_NEVERCLAIMPARSE_YY_MAIN = neverclaimparse.cc -FROM_NEVERCLAIMPARSE_YY_OTHERS = \ - stack.hh \ - position.hh \ - location.hh \ - neverclaimparse.hh - -FROM_NEVERCLAIMPARSE_YY = $(FROM_NEVERCLAIMPARSE_YY_MAIN) $(FROM_NEVERCLAIMPARSE_YY_OTHERS) - -BUILT_SOURCES = $(FROM_NEVERCLAIMPARSE_YY) -MAINTAINERCLEANFILES = $(FROM_NEVERCLAIMPARSE_YY) - -$(FROM_NEVERCLAIMPARSE_YY_MAIN): $(srcdir)/$(NEVERCLAIMPARSE_YY) -## We must cd into $(srcdir) first because if we tell bison to read -## $(srcdir)/$(NEVERCLAIMPARSE_YY), it will also use the value of $(srcdir)/ -## in the generated include statements. - cd $(srcdir) && \ - bison -Wall -Werror --report=all \ - $(NEVERCLAIMPARSE_YY) -o $(FROM_NEVERCLAIMPARSE_YY_MAIN) -$(FROM_NEVERCLAIMPARSE_YY_OTHERS): $(NEVERCLAIMPARSE_YY) - @test -f $@ || $(MAKE) $(AM_MAKEFLAGS) $(FROM_NEVERCLAIMPARSE_YY_MAIN) - -EXTRA_DIST = $(NEVERCLAIMPARSE_YY) - -libneverclaimparse_la_SOURCES = \ - fmterror.cc \ - $(FROM_NEVERCLAIMPARSE_YY) \ - neverclaimscan.ll \ - parsedecl.hh diff --git a/src/neverclaimparse/fmterror.cc b/src/neverclaimparse/fmterror.cc deleted file mode 100644 index 7070dd539..000000000 --- a/src/neverclaimparse/fmterror.cc +++ /dev/null @@ -1,44 +0,0 @@ -// 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. -// -// 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 "public.hh" - -namespace spot -{ - bool - format_neverclaim_parse_errors(std::ostream& os, - const std::string& filename, - neverclaim_parse_error_list& error_list) - { - bool printed = false; - spot::neverclaim_parse_error_list::iterator it; - for (it = error_list.begin(); it != error_list.end(); ++it) - { - if (filename != "-") - os << filename << ":"; - os << it->first << ": "; - os << it->second << std::endl; - printed = true; - } - return printed; - } -} diff --git a/src/neverclaimparse/neverclaimparse.yy b/src/neverclaimparse/neverclaimparse.yy deleted file mode 100644 index e5a9f7782..000000000 --- a/src/neverclaimparse/neverclaimparse.yy +++ /dev/null @@ -1,181 +0,0 @@ -/* Copyright (C) 2009, 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. -** -** 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. -*/ -%language "C++" -%locations -%defines -%expect 0 // No shift/reduce -%expect-rr 0 // No reduce/reduce -%name-prefix "neverclaimyy" -%debug -%error-verbose - -%code requires -{ -#include -#include "public.hh" -typedef std::pair pair; -} - -%parse-param {spot::neverclaim_parse_error_list& error_list} -%parse-param {spot::ltl::environment& parse_environment} -%parse-param {spot::tgba_explicit_string*& result} -%union -{ - std::string* str; - pair* p; - std::list* list; -} - -%code -{ -#include "ltlast/constant.hh" - /* Unfortunately Bison 2.3 uses the same guards in all parsers :( */ -#undef BISON_POSITION_HH -#undef BISON_LOCATION_HH -#include "ltlparse/public.hh" - -/* neverclaimparse.hh and parsedecl.hh include each other recursively. - We must ensure that YYSTYPE is declared (by the above %union) - before parsedecl.hh uses it. */ -#include "parsedecl.hh" -using namespace spot::ltl; -} - -%token NEVER "never" -%token SKIP "skip" -%token IF "if" -%token FI "fi" -%token ARROW "->" -%token GOTO "goto" -%token FORMULA -%token IDENT -%type

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

-%destructor { - for (std::list::iterator i = $$->begin(); - i != $$->end(); ++i) - { - delete i->first; - delete i->second; - } - delete $$; - } -%printer { debug_stream() << *$$; } - -%% -neverclaim: - "never" '{' states '}' -; - -states: - /* empty */ - | state states -; - -state: - IDENT ':' "skip" - { - result->create_transition(*$1, *$1); - delete $1; - } - | IDENT ':' { delete $1; } - | IDENT ':' "if" transitions "fi" - { - std::list::iterator it; - for (it = $4->begin(); it != $4->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); - } - // Free the list - delete $1; - for (std::list::iterator it = $4->begin(); - it != $4->end(); ++it) - { - delete it->first; - delete it->second; - } - delete $4; - } -; - -transitions: - /* empty */ { $$ = new std::list; } - | transition transitions - { - $2->push_back(*$1); - delete $1; - $$ = $2; - } -; - -transition: - ':' ':' FORMULA "->" "goto" IDENT - { - $$ = new pair($3, $6); - } -%% - -void -neverclaimyy::parser::error(const location_type& location, - const std::string& message) -{ - error_list.push_back(spot::neverclaim_parse_error(location, message)); -} - -namespace spot -{ - tgba_explicit_string* - neverclaim_parse(const std::string& name, - neverclaim_parse_error_list& error_list, - bdd_dict* dict, - environment& env, - bool debug) - { - if (neverclaimyyopen(name)) - { - error_list.push_back - (neverclaim_parse_error(neverclaimyy::location(), - std::string("Cannot open file ") + name)); - return 0; - } - tgba_explicit_string* result = new tgba_explicit_string(dict); - neverclaimyy::parser parser(error_list, env, result); - parser.set_debug_level(debug); - parser.parse(); - neverclaimyyclose(); - result->merge_transitions(); - return result; - } -} - -// Local Variables: -// mode: c++ -// End: diff --git a/src/neverclaimparse/neverclaimscan.ll b/src/neverclaimparse/neverclaimscan.ll deleted file mode 100644 index 64deea7c1..000000000 --- a/src/neverclaimparse/neverclaimscan.ll +++ /dev/null @@ -1,102 +0,0 @@ -/* 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. -** -** 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. -*/ -%option noyywrap -%option prefix="neverclaimyy" -%option outfile="lex.yy.c" - -%{ -#include -#include "neverclaimparse/parsedecl.hh" - -#define YY_USER_ACTION \ - yylloc->columns(yyleng); - -#define YY_NEVER_INTERACTIVE 1 - -typedef neverclaimyy::parser::token token; - -%} - -eol \n|\r|\n\r|\r\n - -%% - -%{ - yylloc->step(); -%} - - /* skip blanks */ -{eol} yylloc->lines(yyleng); yylloc->step(); -[ \t]+ yylloc->step(); -"/*".*"*/" yylloc->step(); - -"never" return token::NEVER; -"skip"|"skip;" return token::SKIP; -"if" return token::IF; -"fi"|"fi;" return token::FI; -"->" return token::ARROW; -"goto" return token::GOTO; - -"(".*")"|"true"|"1"|"false"|"0" { - yylval->str = - new std::string(yytext, yyleng); - return token::FORMULA; - } - -[a-zA-Z][a-zA-Z0-9_]* { - yylval->str = new std::string(yytext, yyleng); - return token::IDENT; - } - -. return *yytext; - -%{ - /* Dummy use of yyunput to shut up a gcc warning. */ - (void) &yyunput; -%} - -%% - -namespace spot -{ - int - neverclaimyyopen(const std::string &name) - { - if (name == "-") - { - yyin = stdin; - } - else - { - yyin = fopen(name.c_str(), "r"); - if (!yyin) - return 1; - } - return 0; - } - - void - neverclaimyyclose() - { - fclose(yyin); - } -} diff --git a/src/neverclaimparse/parsedecl.hh b/src/neverclaimparse/parsedecl.hh deleted file mode 100644 index 49df9bcf3..000000000 --- a/src/neverclaimparse/parsedecl.hh +++ /dev/null @@ -1,40 +0,0 @@ -// Copyright (C) 2003, 2005 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. - -#ifndef SPOT_NEVERCLAIMPARSE_PARSEDECL_HH -# define SPOT_NEVERCLAIMPARSE_PARSEDECL_HH - -#include -#include "neverclaimparse.hh" -#include "location.hh" - -# define YY_DECL \ - int neverclaimyylex (neverclaimyy::parser::semantic_type *yylval, \ - neverclaimyy::location *yylloc) -YY_DECL; - -namespace spot -{ - int neverclaimyyopen(const std::string& name); - void neverclaimyyclose(); -} - -#endif // SPOT_NEVERCLAIMPARSE_PARSEDECL_HH diff --git a/src/neverclaimparse/public.hh b/src/neverclaimparse/public.hh deleted file mode 100644 index 4acd73dcc..000000000 --- a/src/neverclaimparse/public.hh +++ /dev/null @@ -1,84 +0,0 @@ -// Copyright (C) 2003, 2004, 2005, 2006, 2009 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. - -#ifndef SPOT_NEVERCLAIMPARSE_PUBLIC_HH -# define SPOT_NEVERCLAIMPARSE_PUBLIC_HH - -# include "tgba/tgbaexplicit.hh" -// Unfortunately Bison 2.3 uses the same guards in all parsers :( -# undef BISON_LOCATION_HH -# undef BISON_POSITION_HH -# include "neverclaimparse/location.hh" -# include "ltlenv/defaultenv.hh" -# include -# include -# include -# include - -namespace spot -{ - /// \addtogroup tgba_io - /// @{ - - /// \brief A parse diagnostic with its location. - typedef std::pair neverclaim_parse_error; - /// \brief A list of parser diagnostics, as filled by parse. - typedef std::list neverclaim_parse_error_list; - - /// \brief Build a spot::tgba_explicit from a Spin never claim file. - /// \param filename The name of the file to parse. - /// \param error_list A list that will be filled with - /// parse errors that occured during parsing. - /// \param dict The BDD dictionary where to use. - /// \param env The environment of atomic proposition into which parsing - /// should take place. - /// \param debug When true, causes the parser to trace its execution. - /// \return A pointer to the tgba built from \a filename, or - /// 0 if the file could not be opened. - /// - /// Note that the parser usually tries to recover from errors. It can - /// return an non zero value even if it encountered error during the - /// parsing of \a filename. If you want to make sure \a filename - /// was parsed succesfully, check \a error_list for emptiness. - /// - /// \warning This function is not reentrant. - tgba_explicit_string* neverclaim_parse( - const std::string& filename, - neverclaim_parse_error_list& - error_list, - bdd_dict* dict, - ltl::environment& env - = ltl::default_environment::instance(), - bool debug = false); - - /// \brief Format diagnostics produced by spot::neverclaim_parse. - /// \param os Where diagnostics should be output. - /// \param filename The filename that should appear in the diagnostics. - /// \param error_list The error list filled by spot::ltl::parse while - /// parsing \a ltl_string. - /// \return \c true iff any diagnostic was output. - bool format_neverclaim_parse_errors(std::ostream& os, - const std::string& filename, - neverclaim_parse_error_list& error_list); - /// @} -} - -#endif // SPOT_NEVERCLAIMPARSE_PUBLIC_HH diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 2eed02211..9338091b8 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -39,7 +39,6 @@ check_PROGRAMS = \ explprod \ ltlprod \ mixprod \ - neverclaimread \ powerset \ readsave \ reductgba \ @@ -59,7 +58,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 readsave_SOURCES = readsave.cc @@ -77,7 +75,6 @@ TESTS = \ explicit.test \ taatgba.test \ tgbaread.test \ - neverclaimread.test \ readsave.test \ ltl2tgba.test \ ltl2neverclaim.test \ diff --git a/src/tgbatest/neverclaimread.cc b/src/tgbatest/neverclaimread.cc deleted file mode 100644 index 62c65d40c..000000000 --- a/src/tgbatest/neverclaimread.cc +++ /dev/null @@ -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 -#include -#include -#include -#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; -} diff --git a/src/tgbatest/neverclaimread.test b/src/tgbatest/neverclaimread.test deleted file mode 100755 index e2bb8e23d..000000000 --- a/src/tgbatest/neverclaimread.test +++ /dev/null @@ -1,70 +0,0 @@ -#!/bin/sh -# Copyright (C) 2009 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. -# -# 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. - - -. ./defs - -set -e - -cat >input < goto T2_init -:: (p1 && p0) -> goto T1 -fi; -T1: -if -:: (p1 && (! p0)) -> goto accept_all -:: (p1) -> goto T1 -fi; -accept_all: -skip -} -EOF - -run 0 ../neverclaimread input > stdout - -cat >expected < 1 - 1 [label="T2_init"] - 1 -> 2 [label="p0 & p1\n"] - 1 -> 1 [label="1\n"] - 2 [label="T1"] - 2 -> 2 [label="p1\n"] - 2 -> 3 [label="p1 & !p0\n"] - 3 [label="accept_all"] - 3 -> 3 [label="1\n"] -} -EOF - -# Sort out some possible inversions in the output. -# (The order is not guaranteed by SPOT.) -sed -e 's/!p0 & p1/p1 \& !p0/g' -e 's/p1 & p0/p0 \& p1/g' stdout \ - > tmp_ && mv tmp_ stdout -diff stdout expected - -rm input stdout expected