diff --git a/README b/README index 556ae764f..2123f2a71 100644 --- a/README +++ b/README @@ -156,10 +156,9 @@ src/ Sources for libspot. tgba/ TGBA objects and cousins. tgbaalgos/ Algorithms on TGBA. gtec/ Couvreur's Emptiness-Check. - tgbaparse/ Parser for explicit TGBA. ta/ TA objects and cousins (TGTA). taalgos/ Algorithms on TA/TGTA. - tgbatest/ Tests for tgba/, tgbaalgos/, tgbaparse/, ta/ and taalgos/. + tgbatest/ Tests for tgba/, tgbaalgos/, ta/ and taalgos/. sanity/ Sanity tests for the whole project. doc/ Documentation for libspot. org/ Source of userdoc/ as org-mode files. @@ -204,7 +203,7 @@ End: LocalWords: Python's BuDDy LBTT LTL Büchi lbtt gspn DIR GreatSPN Soheib Yann LocalWords: Baarir Thierry Mieg CVS Università di Torino devel src libspot ac LocalWords: ltlast ltlenv ltlparse ltlvisit ltltest misc tgba TGBA tgbaalgos - LocalWords: gtec Tarjan tgbaparse tgbatest doc html PDF spotref pdf cgi ELTL + LocalWords: gtec Tarjan tgbatest doc html PDF spotref pdf cgi ELTL LocalWords: CGI ltl iface BDD Couvreur's emptchk kripke Kripke saba vm LocalWords: eltlparse eltltest SABA sabaalgos sabatest ssp ltlcouter scc SCC LocalWords: formulae optimizations kripkeparse kripketest Automata diff --git a/configure.ac b/configure.ac index eb6bfa0a3..28975a9b6 100644 --- a/configure.ac +++ b/configure.ac @@ -1,5 +1,5 @@ # -*- coding: utf-8 -*- -# Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire +# Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire # de Recherche et Développement de l'Epita (LRDE). # Copyright (C) 2003, 2004, 2005, 2006, 2007 Laboratoire # d'Informatique de Paris 6 (LIP6), département Systèmes Répartis @@ -199,7 +199,6 @@ AC_CONFIG_FILES([ src/tgba/Makefile src/taalgos/Makefile src/ta/Makefile - src/tgbaparse/Makefile src/tgbatest/defs src/tgbatest/Makefile wrap/Makefile diff --git a/src/Makefile.am b/src/Makefile.am index e2da5094e..30f47e9e7 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -1,5 +1,5 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2009, 2010, 2012, 2013, 2014 Laboratoire de Recherche +## Copyright (C) 2009, 2010, 2012, 2013, 2014, 2015 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 @@ -25,10 +25,9 @@ AUTOMAKE_OPTIONS = subdir-objects # List directories in the order they must be built. Keep tests at the # end, after building '.' (since the current directory contains # libspot.la needed by the tests) -SUBDIRS = misc priv ltlenv ltlast ltlvisit ltlparse graph tgba \ - tgbaalgos tgbaparse ta taalgos kripke kripkeparse \ - dstarparse hoaparse . bin ltltest graphtest tgbatest \ - kripketest sanity +SUBDIRS = misc priv ltlenv ltlast ltlvisit ltlparse graph tgba \ + tgbaalgos ta taalgos kripke kripkeparse dstarparse hoaparse \ + . bin ltltest graphtest tgbatest kripketest sanity lib_LTLIBRARIES = libspot.la libspot_la_SOURCES = @@ -48,7 +47,6 @@ libspot_la_LIBADD = \ ta/libta.la \ tgbaalgos/libtgbaalgos.la \ tgba/libtgba.la \ - tgbaparse/libtgbaparse.la \ ../lib/libgnu.la # Dummy C++ source to cause C++ linking. diff --git a/src/tgbaparse/.cvsignore b/src/tgbaparse/.cvsignore deleted file mode 100644 index 0b2891e85..000000000 --- a/src/tgbaparse/.cvsignore +++ /dev/null @@ -1,13 +0,0 @@ -.deps -Makefile -Makefile.in -location.hh -tgbaparse.cc -tgbaparse.hh -tgbaparse.output -tgbascan.cc -position.hh -stack.hh -*.lo -*.la -.libs diff --git a/src/tgbaparse/.gitignore b/src/tgbaparse/.gitignore deleted file mode 100644 index 0b2891e85..000000000 --- a/src/tgbaparse/.gitignore +++ /dev/null @@ -1,13 +0,0 @@ -.deps -Makefile -Makefile.in -location.hh -tgbaparse.cc -tgbaparse.hh -tgbaparse.output -tgbascan.cc -position.hh -stack.hh -*.lo -*.la -.libs diff --git a/src/tgbaparse/Makefile.am b/src/tgbaparse/Makefile.am deleted file mode 100644 index 754a0552e..000000000 --- a/src/tgbaparse/Makefile.am +++ /dev/null @@ -1,60 +0,0 @@ -## -*- coding: utf-8 -*- -## Copyright (C) 2008, 2009, 2011, 2013 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 3 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 this program. If not, see . - -AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(BUDDY_CPPFLAGS) -DYY_NO_INPUT -# Disable -Werror because too many versions of flex yield warnings. -AM_CXXFLAGS = $(WARNING_CXXFLAGS:-Werror=) - -tgbaparsedir = $(pkgincludedir)/tgbaparse - -tgbaparse_HEADERS = public.hh - -noinst_LTLIBRARIES = libtgbaparse.la - -TGBAPARSE_YY = tgbaparse.yy -FROM_TGBAPARSE_YY_MAIN = tgbaparse.cc -FROM_TGBAPARSE_YY_OTHERS = \ - stack.hh \ - tgbaparse.hh - -FROM_TGBAPARSE_YY = $(FROM_TGBAPARSE_YY_MAIN) $(FROM_TGBAPARSE_YY_OTHERS) - -BUILT_SOURCES = $(FROM_TGBAPARSE_YY) -MAINTAINERCLEANFILES = $(FROM_TGBAPARSE_YY) - -$(FROM_TGBAPARSE_YY_MAIN): $(srcdir)/$(TGBAPARSE_YY) -## We must cd into $(srcdir) first because if we tell bison to read -## $(srcdir)/$(TGBAPARSE_YY), it will also use the value of $(srcdir)/ -## in the generated include statements. - cd $(srcdir) && \ - $(BISON) -Wall -Werror --report=all $(BISON_EXTRA_FLAGS) \ - $(TGBAPARSE_YY) -o $(FROM_TGBAPARSE_YY_MAIN) -$(FROM_TGBAPARSE_YY_OTHERS): $(TGBAPARSE_YY) - @test -f $@ || $(MAKE) $(AM_MAKEFLAGS) $(FROM_TGBAPARSE_YY_MAIN) - -EXTRA_DIST = $(TGBAPARSE_YY) - -libtgbaparse_la_SOURCES = \ - fmterror.cc \ - $(FROM_TGBAPARSE_YY) \ - tgbascan.ll \ - parsedecl.hh diff --git a/src/tgbaparse/fmterror.cc b/src/tgbaparse/fmterror.cc deleted file mode 100644 index a9493053d..000000000 --- a/src/tgbaparse/fmterror.cc +++ /dev/null @@ -1,45 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2014 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 3 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 this program. If not, see . - -#include -#include "public.hh" - -namespace spot -{ - bool - format_tgba_parse_errors(std::ostream& os, - const std::string& filename, - tgba_parse_error_list& error_list) - { - bool printed = false; - spot::tgba_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/tgbaparse/parsedecl.hh b/src/tgbaparse/parsedecl.hh deleted file mode 100644 index 52c7b4357..000000000 --- a/src/tgbaparse/parsedecl.hh +++ /dev/null @@ -1,42 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014 Laboratoire de Recherche et -// Développement de l'Epita. -// 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 3 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 this program. If not, see . - -#ifndef SPOT_TGBAPARSE_PARSEDECL_HH -# define SPOT_TGBAPARSE_PARSEDECL_HH - -#include -#include "tgbaparse.hh" -#include "misc/location.hh" - -# define YY_DECL \ - int tgbayylex (tgbayy::parser::semantic_type *yylval, \ - spot::location *yylloc) -YY_DECL; - -namespace spot -{ - int tgbayyopen(const std::string& name); - void tgbayyclose(); -} - - -#endif // SPOT_TGBAPARSE_PARSEDECL_HH diff --git a/src/tgbaparse/public.hh b/src/tgbaparse/public.hh deleted file mode 100644 index 4861e408b..000000000 --- a/src/tgbaparse/public.hh +++ /dev/null @@ -1,88 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2009, 2012, 2013, 2014 Laboratoire de Recherche et -// Développement de l'Epita. -// 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 3 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 this program. If not, see . - -#ifndef SPOT_TGBAPARSE_PUBLIC_HH -# define SPOT_TGBAPARSE_PUBLIC_HH - -# include "tgba/tgbagraph.hh" -# include "misc/location.hh" -# include "ltlenv/defaultenv.hh" -# include -# include -# include -# include - -namespace spot -{ - /// \addtogroup tgba_io - /// @{ - -#ifndef SWIG - /// \brief A parse diagnostic with its location. - typedef std::pair tgba_parse_error; - /// \brief A list of parser diagnostics, as filled by parse. - typedef std::list tgba_parse_error_list; -#else - // Turn parse_error_list into an opaque type for Swig. - struct tgba_parse_error_list {}; -#endif - - /// \brief Build a spot::tgba_digraph from a text 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. - SPOT_API - tgba_digraph_ptr tgba_parse(const std::string& filename, - tgba_parse_error_list& error_list, - bdd_dict_ptr dict, - ltl::environment& env - = ltl::default_environment::instance(), - bool debug = false); - - /// \brief Format diagnostics produced by spot::tgba_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. - SPOT_API - bool format_tgba_parse_errors(std::ostream& os, - const std::string& filename, - tgba_parse_error_list& error_list); - - /// @} -} - -#endif // SPOT_TGBAPARSE_PUBLIC_HH diff --git a/src/tgbaparse/tgbaparse.yy b/src/tgbaparse/tgbaparse.yy deleted file mode 100644 index 4ed3c90dd..000000000 --- a/src/tgbaparse/tgbaparse.yy +++ /dev/null @@ -1,245 +0,0 @@ -/* -*- coding: utf-8 -*- -** Copyright (C) 2009, 2010, 2012, 2013, 2014 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 3 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 this program. If not, see . -*/ -%language "C++" -%locations -%defines -%name-prefix "tgbayy" -%debug -%error-verbose -%define api.location.type "spot::location" - -%code requires -{ -#include -#include "public.hh" -#include "priv/accmap.hh" -#include "tgba/formula2bdd.hh" - -/* Cache parsed formulae. Labels on arcs are frequently identical and - it would be a waste of time to parse them to formula* over and - over, and to register all their atomic_propositions in the - bdd_dict. Keep the bdd result around so we can reuse it. */ - typedef std::map formula_cache; - typedef typename spot::tgba_digraph::namer::type named_tgba_t; -} - -%parse-param {spot::tgba_parse_error_list& error_list} -%parse-param {spot::ltl::environment& parse_environment} -%parse-param {spot::acc_mapper_string& acc_map} -%parse-param {spot::tgba_digraph_ptr& result} -%parse-param {named_tgba_t*& namer} -%parse-param {formula_cache& fcache} -%union -{ - int token; - std::string* str; - const spot::ltl::formula* f; - spot::acc_cond::mark_t acc; -} - -%code -{ -#include "ltlast/constant.hh" -#include "ltlparse/public.hh" -#include - -/* tgbaparse.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; - -typedef std::pair pair; -} - -%token STRING UNTERMINATED_STRING -%token IDENT -%type strident string -%type condition -%type acc_list -%token ACC_DEF - -%destructor { delete $$; } - -%printer { debug_stream() << *$$; } -%printer { debug_stream() << $$; } - -%% -tgba: acceptance_decl lines - | acceptance_decl - { namer->new_state("0"); } - | lines - | - { namer->new_state("0"); }; - -acceptance_decl: ACC_DEF acc_decl ';' - { - } - -/* At least one line. */ -lines: line - | lines line - ; - -line: strident ',' strident ',' condition ',' acc_list ';' - { - bdd cond = bddtrue; - if ($5) - { - formula_cache::const_iterator i = fcache.find(*$5); - if (i == fcache.end()) - { - parse_error_list pel; - const formula* f = - spot::ltl::parse_boolean(*$5, pel, parse_environment, - debug_level()); - for (auto& j: pel) - { - // Adjust the diagnostic to the current position. - spot::location here = @5; - here.end.line = here.begin.line + j.first.end.line - 1; - here.end.column = here.begin.column + j.first.end.column; - here.begin.line += j.first.begin.line - 1; - here.begin.column += j.first.begin.column; - error_list.emplace_back(here, j.second); - } - if (f) - { - cond = formula_to_bdd(f, result->get_dict(), result); - f->destroy(); - } - fcache[*$5] = cond; - } - else - { - cond = i->second; - } - } - unsigned s = namer->new_state(*$1); - unsigned d = namer->new_state(*$3); - namer->graph().new_transition(s, d, cond, $7); - delete $1; - delete $3; - delete $5; - } - ; - -string: STRING - | UNTERMINATED_STRING - { - $$ = $1; - error_list.emplace_back(@1, "unterminated string"); - } - -strident: string | IDENT - -condition: - { - $$ = 0; - } - | string - { - $$ = $1; - } - ; - -acc_list: - { - $$ = 0U; - } - | acc_list strident - { - if (*$2 != "" && *$2 != "false") - { - auto p = acc_map.lookup(*$2); - if (! p.first) - { - error_list.emplace_back(@2, - "undeclared acceptance condition `" + *$2 + "'"); - // $2 will be destroyed on error recovery. - YYERROR; - } - $1 |= p.second; - } - delete $2; - $$ = $1; - } - ; - - -acc_decl: - | acc_decl strident - { - acc_map.declare(*$2); - delete $2; - } - ; - -%% - -void -tgbayy::parser::error(const location_type& location, - const std::string& message) -{ - error_list.emplace_back(location, message); -} - -namespace spot -{ - tgba_digraph_ptr - tgba_parse(const std::string& name, - tgba_parse_error_list& error_list, - bdd_dict_ptr dict, - environment& env, - bool debug) - { - if (tgbayyopen(name)) - { - error_list.emplace_back(spot::location(), - std::string("Cannot open file ") + name); - return 0; - } - formula_cache fcache; - auto result = make_tgba_digraph(dict); - auto namer = result->create_namer(); - spot::acc_mapper_string acc_map(result); - tgbayy::parser parser(error_list, env, acc_map, result, namer, fcache); - parser.set_debug_level(debug); - parser.parse(); - tgbayyclose(); - - if (namer) // No fatal error - { - delete namer; - return result; - } - else // Fatal error - { - return nullptr; - } - } -} - -// Local Variables: -// mode: c++ -// End: diff --git a/src/tgbaparse/tgbascan.ll b/src/tgbaparse/tgbascan.ll deleted file mode 100644 index edc613b14..000000000 --- a/src/tgbaparse/tgbascan.ll +++ /dev/null @@ -1,113 +0,0 @@ -/* -*- coding: utf-8 -*- -** Copyright (C) 2011, 2014, 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 3 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 this program. If not, see . -*/ -%option noyywrap -%option prefix="tgbayy" -%option outfile="lex.yy.c" -%x STATE_STRING - -%{ -#include -#include "tgbaparse/parsedecl.hh" - -#define YY_USER_ACTION \ - yylloc->columns(yyleng); - -#define YY_NEVER_INTERACTIVE 1 - -typedef tgbayy::parser::token token; - -%} - -eol \n+|\r+ -eol2 (\n\r)+|(\r\n)+ - -%% - -%{ - yylloc->step (); -%} - -acc[ \t]*= return token::ACC_DEF; - -[a-zA-Z_.][a-zA-Z0-9_.]* { - yylval->str = new std::string(yytext, yyleng); - return token::IDENT; - } - - /* discard whitespace */ -{eol} yylloc->lines(yyleng); yylloc->step(); -{eol2} yylloc->lines(yyleng / 2); yylloc->step(); -[ \t]+ yylloc->step(); - -\" { - yylval->str = new std::string; - BEGIN(STATE_STRING); - } - -. return *yytext; - - /* Handle \" and \\ in strings. */ -{ - \" { - BEGIN(INITIAL); - return token::STRING; - } - \\["\\] yylval->str->append(1, yytext[1]); - [^"\\]+ yylval->str->append(yytext, yyleng); - <> { - BEGIN(INITIAL); - return token::UNTERMINATED_STRING; - } -} - -%{ - /* Dummy use of yyunput to shut up a gcc warning. */ - (void) &yyunput; -%} - -%% - -namespace spot -{ - int - tgbayyopen(const std::string &name) - { - if (name == "-") - { - yyin = stdin; - } - else - { - yyin = fopen(name.c_str(), "r"); - if (!yyin) - return 1; - } - return 0; - } - - void - tgbayyclose() - { - fclose(yyin); - } -} diff --git a/src/tgbatest/randtgba.cc b/src/tgbatest/randtgba.cc index bfbd91765..7766e605f 100644 --- a/src/tgbatest/randtgba.cc +++ b/src/tgbatest/randtgba.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014 Laboratoire de -// Recherche et Développement de l'Epita (LRDE). +// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014, 2015 Laboratoire +// de Recherche et Développement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. @@ -41,7 +41,6 @@ #include "tgbaalgos/stats.hh" #include "ltlenv/defaultenv.hh" #include "tgbaalgos/dotty.hh" -#include "tgbaparse/public.hh" #include "misc/random.hh" #include "misc/optionmap.hh" #include "tgbaalgos/degen.hh"