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.
This commit is contained in:
Felix Abecassis
Alexandre Duret-Lutz
parent
7da112344e
commit
ab6ec5cb63
13 changed files with 743 additions and 41 deletions
24
ChangeLog
24
ChangeLog
|
|
@ -1,3 +1,27 @@
|
||||||
|
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-11-06 Alexandre Duret-Lutz <adl@lrde.epita.fr>
|
2010-11-06 Alexandre Duret-Lutz <adl@lrde.epita.fr>
|
||||||
|
|
||||||
Remove `readsave' and fix line numbers in tgbaparse error messages.
|
Remove `readsave' and fix line numbers in tgbaparse error messages.
|
||||||
|
|
|
||||||
81
README
81
README
|
|
@ -105,46 +105,47 @@ 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/.
|
||||||
sanity/ Sanity tests for the whole project.
|
neverclaimparse/ Parser for SPIN never claim.
|
||||||
doc/ Documentation for libspot.
|
sanity/ Sanity tests for the whole project.
|
||||||
spot.html/ HTML reference manual.
|
doc/ Documentation for libspot.
|
||||||
spot.latex/ Sources for the PDF manual. (Not distributed, can be rebuilt.)
|
spot.html/ HTML reference manual.
|
||||||
spotref.pdf PDF reference manual.
|
spot.latex/ Sources for the PDF manual. (Not distributed, can be rebuilt.)
|
||||||
bench/ Benchmarks for ...
|
spotref.pdf PDF reference manual.
|
||||||
emptchk/ ... emptiness-check algorithms,
|
bench/ Benchmarks for ...
|
||||||
gspn-ssp/ ... various symmetry-based methods with GreatSPN,
|
emptchk/ ... emptiness-check algorithms,
|
||||||
ltl2tgba/ ... LTL-to-Büchi translation algorithms,
|
gspn-ssp/ ... various symmetry-based methods with GreatSPN,
|
||||||
ltlcounter/ ... translation of a class of LTL formulae,
|
ltl2tgba/ ... LTL-to-Büchi translation algorithms,
|
||||||
scc-stats/ ... SCC statistics after translation of LTL formulae,
|
ltlcounter/ ... translation of a class of LTL formulae,
|
||||||
split-product/ ... parallelizing gain after splitting LTL automata.
|
scc-stats/ ... SCC statistics after translation of LTL formulae,
|
||||||
wrap/ Wrappers for other languages.
|
split-product/ ... parallelizing gain after splitting LTL automata.
|
||||||
python/ Python bindings for Spot and BuDDy
|
wrap/ Wrappers for other languages.
|
||||||
tests/ Tests for these bindings
|
python/ Python bindings for Spot and BuDDy
|
||||||
cgi-bin/ Python-based CGI script (ltl-to-tgba translator)
|
tests/ Tests for these bindings
|
||||||
iface/ Interfaces to other libraries.
|
cgi-bin/ Python-based CGI script (ltl-to-tgba translator)
|
||||||
gspn/ GreatSPN interface.
|
iface/ Interfaces to other libraries.
|
||||||
examples/ Supporting models used by the test cases.
|
gspn/ GreatSPN interface.
|
||||||
nips/ NIPS interface (to use Promela models).
|
examples/ Supporting models used by the test cases.
|
||||||
nipstest/ Tests for NIPS.
|
nips/ NIPS interface (to use Promela models).
|
||||||
|
nipstest/ Tests for NIPS.
|
||||||
|
|
||||||
Third party software
|
Third party software
|
||||||
--------------------
|
--------------------
|
||||||
|
|
|
||||||
|
|
@ -113,6 +113,7 @@ 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 \
|
||||||
saba sabaalgos . ltltest eltltest tgbatest evtgbatest \
|
neverclaimparse . ltltest eltltest tgbatest evtgbatest \
|
||||||
sabatest sanity
|
sabatest sanity
|
||||||
|
|
||||||
lib_LTLIBRARIES = libspot.la
|
lib_LTLIBRARIES = libspot.la
|
||||||
|
|
@ -44,6 +44,7 @@ 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 \
|
||||||
|
|
|
||||||
66
src/neverclaimparse/Makefile.am
Normal file
66
src/neverclaimparse/Makefile.am
Normal file
|
|
@ -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
|
||||||
44
src/neverclaimparse/fmterror.cc
Normal file
44
src/neverclaimparse/fmterror.cc
Normal file
|
|
@ -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 <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;
|
||||||
|
}
|
||||||
|
}
|
||||||
181
src/neverclaimparse/neverclaimparse.yy
Normal file
181
src/neverclaimparse/neverclaimparse.yy
Normal file
|
|
@ -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 <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:
|
||||||
102
src/neverclaimparse/neverclaimscan.ll
Normal file
102
src/neverclaimparse/neverclaimscan.ll
Normal file
|
|
@ -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 <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);
|
||||||
|
}
|
||||||
|
}
|
||||||
40
src/neverclaimparse/parsedecl.hh
Normal file
40
src/neverclaimparse/parsedecl.hh
Normal file
|
|
@ -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 <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
|
||||||
84
src/neverclaimparse/public.hh
Normal file
84
src/neverclaimparse/public.hh
Normal file
|
|
@ -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 <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,6 +39,7 @@ check_PROGRAMS = \
|
||||||
explprod \
|
explprod \
|
||||||
ltlprod \
|
ltlprod \
|
||||||
mixprod \
|
mixprod \
|
||||||
|
neverclaimread \
|
||||||
powerset \
|
powerset \
|
||||||
reductgba \
|
reductgba \
|
||||||
reduccmp \
|
reduccmp \
|
||||||
|
|
@ -57,6 +58,7 @@ 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
|
||||||
reductgba_SOURCES = reductgba.cc
|
reductgba_SOURCES = reductgba.cc
|
||||||
|
|
@ -73,6 +75,7 @@ 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 \
|
||||||
|
|
|
||||||
85
src/tgbatest/neverclaimread.cc
Normal file
85
src/tgbatest/neverclaimread.cc
Normal file
|
|
@ -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 <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;
|
||||||
|
}
|
||||||
70
src/tgbatest/neverclaimread.test
Executable file
70
src/tgbatest/neverclaimread.test
Executable file
|
|
@ -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 <<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