From f185aabf44747d41073eda2431b847b4bf31db10 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 23 Apr 2017 15:22:08 +0200 Subject: [PATCH] python: add wrapper for libspotgen For #254. * python/spot/gen.i, tests/python/gen.py: New files. * python/Makefile.am, tests/Makefile.am: Adjust. * NEWS: Mention the spot.gen python package. --- NEWS | 5 +++++ python/.gitignore | 1 + python/Makefile.am | 24 ++++++++++++++++++-- python/spot/gen.i | 53 +++++++++++++++++++++++++++++++++++++++++++++ tests/Makefile.am | 1 + tests/python/gen.py | 38 ++++++++++++++++++++++++++++++++ 6 files changed, 120 insertions(+), 2 deletions(-) create mode 100644 python/spot/gen.i create mode 100644 tests/python/gen.py diff --git a/NEWS b/NEWS index 463fbac28..c38c3ff53 100644 --- a/NEWS +++ b/NEWS @@ -61,6 +61,11 @@ New in spot 2.3.3.dev (not yet released) spot::acc_cond::rabin_like_pairs() are implemented for Rabin-like pairs. + Python: + + - The 'spot.gen' package is a wrapper around the functions from + the libspotgen library. + Bugs fixed: - the transformation to state-based acceptance (spot::sbacc()) was diff --git a/python/.gitignore b/python/.gitignore index 7e98f4b06..8175d2b40 100644 --- a/python/.gitignore +++ b/python/.gitignore @@ -12,3 +12,4 @@ buddy.py* ajax/*.py spot/impl.py spot/ltsmin.py +spot/gen.py diff --git a/python/Makefile.am b/python/Makefile.am index 4d6e6103e..234701e9b 100644 --- a/python/Makefile.am +++ b/python/Makefile.am @@ -34,18 +34,21 @@ AM_CPPFLAGS = -I$(PYTHONINC) -I$(top_builddir) -I$(top_srcdir) \ # this. SWIGFLAGS = -c++ -python -py3 -O -nofastproxy -MD -EXTRA_DIST = buddy.i spot/impl.i spot/ltsmin.i +EXTRA_DIST = buddy.i spot/impl.i spot/ltsmin.i spot/gen.i nobase_python_PYTHON = \ spot/__init__.py \ spot/aux.py \ spot/impl.py \ spot/ltsmin.py \ + spot/gen.py \ buddy.py -nobase_pyexec_LTLIBRARIES = _buddy.la spot/_impl.la spot/_ltsmin.la +nobase_pyexec_LTLIBRARIES = _buddy.la spot/_impl.la \ + spot/_ltsmin.la spot/_gen.la MAINTAINERCLEANFILES = \ $(srcdir)/spot/impl_wrap.cxx $(srcdir)/spot/impl.py \ $(srcdir)/spot/ltsmin_wrap.cxx $(srcdir)/spot/ltsmin.py \ + $(srcdir)/spot/gen_wrap.cxx $(srcdir)/spot/gen.py \ $(srcdir)/buddy_wrap.cxx $(srcdir)/buddy.py ## spot @@ -81,6 +84,23 @@ spot/ltsmin.py: spot/ltsmin.i $(MAKE) $(AM_MAKEFLAGS) spot/ltsmin_wrap.cxx +## spot-gen + +spot__gen_la_SOURCES = spot/gen_wrap.cxx +spot__gen_la_LDFLAGS = -avoid-version -module $(SYMBOLIC_LDFLAGS) +spot__gen_la_LIBADD = $(top_builddir)/spot/libspot.la \ + $(top_builddir)/spot/gen/libspotgen.la + +@AMDEP_TRUE@@am__include@ @am__quote@./spot/$(DEPDIR)/gen_wrap.Pcxx@am__quote@ + +${srcdir}/spot/gen_wrap.cxx: spot/gen.i + $(SWIG) $(SWIGFLAGS) -I$(srcdir) -I$(top_srcdir) -MF spot/$(DEPDIR)/gen_wrap.TPcxx $(srcdir)/spot/gen.i + mv spot/$(DEPDIR)/gen_wrap.TPcxx spot/$(DEPDIR)/gen_wrap.Pcxx + +spot/gen.py: spot/gen.i + $(MAKE) $(AM_MAKEFLAGS) spot/gen_wrap.cxx + + ## buddy _buddy_la_SOURCES = buddy_wrap.cxx diff --git a/python/spot/gen.i b/python/spot/gen.i new file mode 100644 index 000000000..487f2ead2 --- /dev/null +++ b/python/spot/gen.i @@ -0,0 +1,53 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2017 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 3 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with this program. If not, see . + +%{ + // Workaround for SWIG 2.0.2 using ptrdiff_t but not including cstddef. + // It matters with g++ 4.6. +#include +%} + +%module(package="spot", director="1") gen + +%include "std_string.i" +%include "exception.i" +%include "std_shared_ptr.i" + +%shared_ptr(spot::twa_graph) + +%{ +#include +using namespace spot; +%} + +%import(module="spot.impl") +%import(module="spot.impl") +%import(module="spot.impl") + +%exception { + try { + $action + } + catch (const std::runtime_error& e) + { + SWIG_exception(SWIG_RuntimeError, e.what()); + } +} + +%include diff --git a/tests/Makefile.am b/tests/Makefile.am index dac18ae83..e8eec9428 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -335,6 +335,7 @@ TESTS_python = \ python/declenv.py \ python/decompose_scc.py \ python/dualize.py \ + python/gen.py \ python/implies.py \ python/interdep.py \ python/ltl2tgba.test \ diff --git a/tests/python/gen.py b/tests/python/gen.py new file mode 100644 index 000000000..ec3843464 --- /dev/null +++ b/tests/python/gen.py @@ -0,0 +1,38 @@ +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2017 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 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +# Test that the spot.gen package works, in particular, we want +# to make sure that the objects created from spot.gen methods +# are usable with methods from the spot package. + +import spot.gen as gen +from sys import exit + +k2 = gen.ks_cobuchi(2) +assert k2.num_states() == 5 +# to_str is defined in the spot package, so this makes sure +# the type returned by spot.gen.ks_cobuchi() is the correct one. +assert 'to_str' in dir(k2) + +try: + gen.ks_cobuchi(0) +except RuntimeError as e: + assert 'positive argument' in str(e) +else: + exit(2)