diff --git a/NEWS b/NEWS index 0b5a961ed716f18439fba2e2abd5deb62420c3ab..a1b7bf5f4ea3616b3f4e216399886be5e6d1ba58 100644 --- a/NEWS +++ b/NEWS @@ -16,6 +16,8 @@ New in spot 0.9a: - Promises generated for formula of the form P(a U (b U c)) are reduced into P(c), avoiding the introduction of many promises that imply each other. + * The tgba_parse() function is now available via the Python + bindings. * Bug fixes: - The random SERE generator was using the wrong operators for "and" and "or", mistaking And/Or with AndRat/OrRat. diff --git a/src/tgbaparse/public.hh b/src/tgbaparse/public.hh index 80c061c2ecbab390842a6eb82236d0dce182205e..c15595c4f6f9aca5c1f175d4128648b77c21f39b 100644 --- a/src/tgbaparse/public.hh +++ b/src/tgbaparse/public.hh @@ -1,6 +1,9 @@ -// 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. +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2012 Laboratoire de Recherche et Développement +// de l'Epita. +// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire +// d'Informatique de Paris 6 (LIP6), département Systèmes Répartis +// Coopératifs (SRC), Université Pierre et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -38,10 +41,15 @@ namespace spot /// \addtogroup tgba_io /// @{ +#ifndef SWIG /// \brief A parse diagnostic with its location. typedef std::pair tgba_parse_error; /// \brief A list of parser diagnostics, as filled by parse. typedef std::list tgba_parse_error_list; +#else + // Turn parse_error_list into an opaque type for Swig. + struct tgba_parse_error_list {}; +#endif /// \brief Build a spot::tgba_explicit from a text file. /// \param filename The name of the file to parse. diff --git a/wrap/python/spot.i b/wrap/python/spot.i index 05f566b485f5a361a4b41847186bbe741dc83d04..472d6055609fb86fa657ef6a681d1b1c0f248397 100644 --- a/wrap/python/spot.i +++ b/wrap/python/spot.i @@ -107,6 +107,8 @@ namespace std { #include "tgbaalgos/stats.hh" #include "tgbaalgos/simulation.hh" +#include "tgbaparse/public.hh" + using namespace spot::ltl; using namespace spot; %} @@ -191,6 +193,8 @@ using namespace spot; %feature("new") spot::tgba::succ_iter; %feature("new") spot::tgba_succ_iterator::current_state; %feature("new") spot::simulation; +%feature("new") spot::tgba_parse; + // Help SWIG with namespace lookups. #define ltl spot::ltl %include "tgba/bdddict.hh" @@ -215,11 +219,11 @@ using namespace spot; spot::explicit_graph; %template(explicit_string_tgba) - spot::explicit_graph; -%template(explicit_number_tgba) - spot::tgba_explicit; + spot::tgba_explicit; %template(explicit__number_tgba) spot::tgba_explicit; +%template(explicit_formula_tgba) + spot::tgba_explicit; %template(explicit_string__tgba) spot::explicit_conf, @@ -249,6 +253,9 @@ using namespace spot; %include "tgbaalgos/sccfilter.hh" %include "tgbaalgos/stats.hh" %include "tgbaalgos/simulation.hh" + +%include "tgbaparse/public.hh" + #undef ltl %extend spot::ltl::formula { @@ -331,6 +338,13 @@ empty_parse_error_list() return l; } +spot::tgba_parse_error_list +empty_tgba_parse_error_list() +{ + tgba_parse_error_list l; + return l; +} + std::ostream& get_cout() { @@ -381,3 +395,13 @@ __nonzero__() } } + +%extend spot::tgba_parse_error_list { + +bool +__nonzero__() +{ + return !self->empty(); +} + +} diff --git a/wrap/python/tests/Makefile.am b/wrap/python/tests/Makefile.am index d694e4984cc52c65e42e88b63de1d004aa32713c..c1dddb471ef63525147ed6ca6b3f05d0226bb9a0 100644 --- a/wrap/python/tests/Makefile.am +++ b/wrap/python/tests/Makefile.am @@ -1,4 +1,4 @@ -## Copyright (C) 2010 Labortatoire de Recherche et Développement de +## Copyright (C) 2010, 2012 Labortatoire de Recherche et Développement de ## l'EPITA. ## Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), ## département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -38,4 +38,5 @@ TESTS = \ minato.py \ modgray.py \ optionmap.py \ + parsetgba.py \ setxor.py diff --git a/wrap/python/tests/parsetgba.py b/wrap/python/tests/parsetgba.py new file mode 100755 index 0000000000000000000000000000000000000000..9b6199a6382a934f04116dffa8c42217a4126710 --- /dev/null +++ b/wrap/python/tests/parsetgba.py @@ -0,0 +1,46 @@ +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2012 Laboratoire de Recherche et Développement +# de l'Epita (LRDE). +# +# 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. + +import os +import spot + +contents = ''' +acc = "b"; +"a U b", "1", "b", "b"; +"a U b", "a U b", "a & !b",; +"1", "1", "1", "b"; +''' + +filename = 'parsetgba.out' + +out = open(filename, 'w+') +out.write(contents) +out.close() + +d = spot.bdd_dict() +p = spot.empty_tgba_parse_error_list() +a = spot.tgba_parse(filename, p, d) + +assert not p + +spot.dotty_reachable(spot.get_cout(), a) + +os.unlink(filename)