Revert "Add never claim parser."
Such changes should not be pushed to master before they are finished
(this doesn't pass distcheck).
This reverts commit 9aaa638b27.
This commit is contained in:
Alexandre Duret-Lutz
parent
9aaa638b27
commit
498b44f742
13 changed files with 41 additions and 743 deletions
24
ChangeLog
24
ChangeLog
|
|
@ -1,27 +1,3 @@
|
||||||
2010-05-25 Felix Abecassis <abecassis@lrde.epita.fr>
|
|
||||||
|
|
||||||
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 <adl@lrde.epita.fr>
|
2010-05-20 Alexandre Duret-Lutz <adl@lrde.epita.fr>
|
||||||
|
|
||||||
Fix the --enable-optimizations check.
|
Fix the --enable-optimizations check.
|
||||||
|
|
|
||||||
81
README
81
README
|
|
@ -105,47 +105,46 @@ Layout of the source tree
|
||||||
Core directories
|
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.
|
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
|
Third party software
|
||||||
--------------------
|
--------------------
|
||||||
|
|
|
||||||
|
|
@ -111,7 +111,6 @@ AC_CONFIG_FILES([
|
||||||
src/ltlvisit/Makefile
|
src/ltlvisit/Makefile
|
||||||
src/Makefile
|
src/Makefile
|
||||||
src/misc/Makefile
|
src/misc/Makefile
|
||||||
src/neverclaimparse/Makefile
|
|
||||||
src/sanity/Makefile
|
src/sanity/Makefile
|
||||||
src/saba/Makefile
|
src/saba/Makefile
|
||||||
src/sabaalgos/Makefile
|
src/sabaalgos/Makefile
|
||||||
|
|
|
||||||
|
|
@ -28,7 +28,7 @@ AUTOMAKE_OPTIONS = subdir-objects
|
||||||
# libspot.la needed by the tests).
|
# libspot.la needed by the tests).
|
||||||
SUBDIRS = misc ltlenv ltlast ltlvisit ltlparse eltlparse tgba \
|
SUBDIRS = misc ltlenv ltlast ltlvisit ltlparse eltlparse tgba \
|
||||||
tgbaalgos tgbaparse evtgba evtgbaalgos evtgbaparse kripke \
|
tgbaalgos tgbaparse evtgba evtgbaalgos evtgbaparse kripke \
|
||||||
neverclaimparse . ltltest eltltest tgbatest evtgbatest \
|
saba sabaalgos . ltltest eltltest tgbatest evtgbatest \
|
||||||
sabatest sanity
|
sabatest sanity
|
||||||
|
|
||||||
lib_LTLIBRARIES = libspot.la
|
lib_LTLIBRARIES = libspot.la
|
||||||
|
|
@ -44,7 +44,6 @@ libspot_la_LIBADD = \
|
||||||
tgba/libtgba.la \
|
tgba/libtgba.la \
|
||||||
tgbaalgos/libtgbaalgos.la \
|
tgbaalgos/libtgbaalgos.la \
|
||||||
tgbaparse/libtgbaparse.la \
|
tgbaparse/libtgbaparse.la \
|
||||||
neverclaimparse/libneverclaimparse.la \
|
|
||||||
evtgba/libevtgba.la \
|
evtgba/libevtgba.la \
|
||||||
evtgbaalgos/libevtgbaalgos.la \
|
evtgbaalgos/libevtgbaalgos.la \
|
||||||
evtgbaparse/libevtgbaparse.la \
|
evtgbaparse/libevtgbaparse.la \
|
||||||
|
|
|
||||||
|
|
@ -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
|
|
||||||
|
|
@ -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 <ostream>
|
|
||||||
#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;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
@ -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 <string>
|
|
||||||
#include "public.hh"
|
|
||||||
typedef std::pair<std::string*, std::string*> 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<pair>* 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 <str> FORMULA
|
|
||||||
%token <str> IDENT
|
|
||||||
%type <p> transition
|
|
||||||
%type <list> transitions
|
|
||||||
|
|
||||||
%destructor { delete $$; } <str>
|
|
||||||
%destructor { delete $$->first; delete $$->second; delete $$; } <p>
|
|
||||||
%destructor {
|
|
||||||
for (std::list<pair>::iterator i = $$->begin();
|
|
||||||
i != $$->end(); ++i)
|
|
||||||
{
|
|
||||||
delete i->first;
|
|
||||||
delete i->second;
|
|
||||||
}
|
|
||||||
delete $$;
|
|
||||||
} <list>
|
|
||||||
%printer { debug_stream() << *$$; } <str>
|
|
||||||
|
|
||||||
%%
|
|
||||||
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<pair>::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<pair>::iterator it = $4->begin();
|
|
||||||
it != $4->end(); ++it)
|
|
||||||
{
|
|
||||||
delete it->first;
|
|
||||||
delete it->second;
|
|
||||||
}
|
|
||||||
delete $4;
|
|
||||||
}
|
|
||||||
;
|
|
||||||
|
|
||||||
transitions:
|
|
||||||
/* empty */ { $$ = new std::list<pair>; }
|
|
||||||
| 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:
|
|
||||||
|
|
@ -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 <string>
|
|
||||||
#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);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
@ -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 <string>
|
|
||||||
#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
|
|
||||||
|
|
@ -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 <string>
|
|
||||||
# include <list>
|
|
||||||
# include <utility>
|
|
||||||
# include <iosfwd>
|
|
||||||
|
|
||||||
namespace spot
|
|
||||||
{
|
|
||||||
/// \addtogroup tgba_io
|
|
||||||
/// @{
|
|
||||||
|
|
||||||
/// \brief A parse diagnostic with its location.
|
|
||||||
typedef std::pair<neverclaimyy::location, std::string> neverclaim_parse_error;
|
|
||||||
/// \brief A list of parser diagnostics, as filled by parse.
|
|
||||||
typedef std::list<neverclaim_parse_error> 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
|
|
||||||
|
|
@ -39,7 +39,6 @@ check_PROGRAMS = \
|
||||||
explprod \
|
explprod \
|
||||||
ltlprod \
|
ltlprod \
|
||||||
mixprod \
|
mixprod \
|
||||||
neverclaimread \
|
|
||||||
powerset \
|
powerset \
|
||||||
readsave \
|
readsave \
|
||||||
reductgba \
|
reductgba \
|
||||||
|
|
@ -59,7 +58,6 @@ explprod_SOURCES = explprod.cc
|
||||||
ltl2tgba_SOURCES = ltl2tgba.cc
|
ltl2tgba_SOURCES = ltl2tgba.cc
|
||||||
ltlprod_SOURCES = ltlprod.cc
|
ltlprod_SOURCES = ltlprod.cc
|
||||||
mixprod_SOURCES = mixprod.cc
|
mixprod_SOURCES = mixprod.cc
|
||||||
neverclaimread_SOURCES = neverclaimread.cc
|
|
||||||
powerset_SOURCES = powerset.cc
|
powerset_SOURCES = powerset.cc
|
||||||
randtgba_SOURCES = randtgba.cc
|
randtgba_SOURCES = randtgba.cc
|
||||||
readsave_SOURCES = readsave.cc
|
readsave_SOURCES = readsave.cc
|
||||||
|
|
@ -77,7 +75,6 @@ TESTS = \
|
||||||
explicit.test \
|
explicit.test \
|
||||||
taatgba.test \
|
taatgba.test \
|
||||||
tgbaread.test \
|
tgbaread.test \
|
||||||
neverclaimread.test \
|
|
||||||
readsave.test \
|
readsave.test \
|
||||||
ltl2tgba.test \
|
ltl2tgba.test \
|
||||||
ltl2neverclaim.test \
|
ltl2neverclaim.test \
|
||||||
|
|
|
||||||
|
|
@ -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;
|
|
||||||
}
|
|
||||||
|
|
@ -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 <<EOF
|
|
||||||
never {
|
|
||||||
T2_init:
|
|
||||||
if
|
|
||||||
:: (1) -> 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 <<EOF
|
|
||||||
digraph G {
|
|
||||||
0 [label="", style=invis, height=0]
|
|
||||||
0 -> 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
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue