diff --git a/ChangeLog b/ChangeLog index 7173a79c7..aaeb8f84d 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,27 @@ +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 e00bd2430..0358ecc21 100644 --- a/README +++ b/README @@ -105,46 +105,47 @@ 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/. - 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/. + 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. Third party software -------------------- diff --git a/configure.ac b/configure.ac index 226b955af..a544c3668 100644 --- a/configure.ac +++ b/configure.ac @@ -111,6 +111,7 @@ 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 c506fe51c..317399510 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 \ - saba sabaalgos . ltltest eltltest tgbatest evtgbatest \ + neverclaimparse . ltltest eltltest tgbatest evtgbatest \ sabatest sanity lib_LTLIBRARIES = libspot.la @@ -44,6 +44,7 @@ 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 new file mode 100644 index 000000000..9839e5bf0 --- /dev/null +++ b/src/neverclaimparse/Makefile.am @@ -0,0 +1,66 @@ +## 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 new file mode 100644 index 000000000..7070dd539 --- /dev/null +++ b/src/neverclaimparse/fmterror.cc @@ -0,0 +1,44 @@ +// 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 new file mode 100644 index 000000000..e5a9f7782 --- /dev/null +++ b/src/neverclaimparse/neverclaimparse.yy @@ -0,0 +1,181 @@ +/* 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 new file mode 100644 index 000000000..64deea7c1 --- /dev/null +++ b/src/neverclaimparse/neverclaimscan.ll @@ -0,0 +1,102 @@ +/* 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 new file mode 100644 index 000000000..49df9bcf3 --- /dev/null +++ b/src/neverclaimparse/parsedecl.hh @@ -0,0 +1,40 @@ +// 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 new file mode 100644 index 000000000..4acd73dcc --- /dev/null +++ b/src/neverclaimparse/public.hh @@ -0,0 +1,84 @@ +// 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 9338091b8..2eed02211 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -39,6 +39,7 @@ check_PROGRAMS = \ explprod \ ltlprod \ mixprod \ + neverclaimread \ powerset \ readsave \ reductgba \ @@ -58,6 +59,7 @@ 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 @@ -75,6 +77,7 @@ 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 new file mode 100644 index 000000000..62c65d40c --- /dev/null +++ b/src/tgbatest/neverclaimread.cc @@ -0,0 +1,85 @@ +// 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 new file mode 100755 index 000000000..e2bb8e23d --- /dev/null +++ b/src/tgbatest/neverclaimread.test @@ -0,0 +1,70 @@ +#!/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