diff --git a/debian/control b/debian/control index ff0e4cc28e5008ddc282d597ee073025abce816b..ed327ea591a319ee34210d7705c37a3ec2f74b37 100644 --- a/debian/control +++ b/debian/control @@ -30,7 +30,7 @@ Package: libspot-dev Architecture: any Section: libdevel Suggests: spot-doc -Depends: libspot0 (>= ${source:Version}), libspot0 (<< ${source:Version}.1~), libspotltsmin0 (>= ${source:Version}) , libspotltsmin0 (<< ${source:Version}.1~), ${misc:Depends}, libbddx-dev +Depends: libspot0 (>= ${source:Version}), libspot0 (<< ${source:Version}.1~), libspotltsmin0 (>= ${source:Version}), libspotltsmin0 (<< ${source:Version}.1~), ${misc:Depends}, libbddx-dev Description: headers for the Spot model checking library C++ headers for the Spot library. @@ -70,7 +70,7 @@ Description: documentation for Spot Package: python3-spot Architecture: any Section: python -Depends: ${shlibs:Depends}, ${misc:Depends}, ${python3:Depends}, libspot0 (>= ${source:Version}), libspot0 (<< ${source:Version}.1~) +Depends: ${shlibs:Depends}, ${misc:Depends}, ${python3:Depends}, libspot0 (>= ${source:Version}), libspot0 (<< ${source:Version}.1~), libspotltsmin0 (>= ${source:Version}), libspotltsmin0 (<< ${source:Version}.1~) Suggests: ipython3 Description: python3 binding for spot Spot allows manipulation of omega-automata as well diff --git a/doc/org/tut.org b/doc/org/tut.org index ca08eac5b339ef13ac530ca15f3f96865e8cac80..b3f39513386db0a4cbdac77286dfdf35cc64af80 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -59,5 +59,7 @@ real notebooks instead. in Python - [[https://spot.lrde.epita.fr/ipynb/randltl.html][=randltl.ipynb=]] demonstrates a Python-version of [[file:randltl.org][=randltl=]] - [[https://spot.lrde.epita.fr/ipynb/decompose.html][=decompose.ipynb=]] illustrates the =decompose_strength()= function -- [[https://spot.lrde.epita.fr/ipynb/testingaut.html][=testingaut.ipynb=]] shows the step necessary to build a testing +- [[https://spot.lrde.epita.fr/ipynb/testingaut.html][=testingaut.ipynb=]] shows the steps necessary to build a testing automaton +- [[https://spot.lrde.epita.fr/ipynb/ltsmin.html][=ltsmin.ipynb=]] minimal test for loading a DiVinE model using + the LTSmin interface. diff --git a/python/Makefile.am b/python/Makefile.am index dd45717c05c8b5727e2e7bfbc6069e74eae0f9f6..e965d9a1f8aca73bfef52212ff85a8f91f208592 100644 --- a/python/Makefile.am +++ b/python/Makefile.am @@ -32,15 +32,17 @@ AM_CPPFLAGS = -I$(PYTHONINC) -I$(top_builddir) -I$(top_srcdir) \ # this. SWIGFLAGS = -c++ -python -py3 -O -nofastproxy -EXTRA_DIST = spot/impl.i buddy.i +EXTRA_DIST = buddy.i spot/impl.i spot/ltsmin.i python_PYTHON = \ $(srcdir)/spot/__init__.py \ $(srcdir)/spot/impl.py \ + $(srcdir)/spot/ltsmin.py \ $(srcdir)/buddy.py -pyexec_LTLIBRARIES = spot/_impl.la _buddy.la +pyexec_LTLIBRARIES = _buddy.la spot/_impl.la spot/_ltsmin.la MAINTAINERCLEANFILES = \ $(srcdir)/spot/impl_wrap.cxx $(srcdir)/spot/impl.py \ + $(srcdir)/spot/ltsmin_wrap.cxx $(srcdir)/spot/ltsmin.py \ $(srcdir)/buddy_wrap.cxx $(srcdir)/buddy.py ## spot @@ -56,6 +58,20 @@ $(srcdir)/spot/impl.py: $(srcdir)/spot/impl.i $(MAKE) $(AM_MAKEFLAGS) spot/impl_wrap.cxx +## spot-ltsmin + +spot__ltsmin_la_SOURCES = $(srcdir)/spot/ltsmin_wrap.cxx +spot__ltsmin_la_LDFLAGS = -avoid-version -module $(SYMBOLIC_LDFLAGS) +spot__ltsmin_la_LIBADD = $(top_builddir)/spot/libspot.la \ + $(top_builddir)/spot/ltsmin/libspotltsmin.la + +$(srcdir)/spot/ltsmin_wrap.cxx: $(srcdir)/spot/ltsmin.i + $(SWIG) $(SWIGFLAGS) -I$(srcdir) -I$(top_srcdir) $(srcdir)/spot/ltsmin.i + +$(srcdir)/spot/ltsmin.py: $(srcdir)/spot/ltsmin.i + $(MAKE) $(AM_MAKEFLAGS) spot/ltsmin_wrap.cxx + + ## buddy _buddy_la_SOURCES = $(srcdir)/buddy_wrap.cxx diff --git a/python/spot/__init__.py b/python/spot/__init__.py index ef2c6eb556e4f26a4cc10d686974f349b66c7d91..dbab62b50943d7b6a0515f029a4aca39d203082a 100644 --- a/python/spot/__init__.py +++ b/python/spot/__init__.py @@ -872,5 +872,5 @@ def sat_minimize(aut, acc=None, colored=False, args += ',max-states=' + str(max_states) if dichotomy: args += ',dichotomy'; - from spot_impl import sat_minimize as sm + from spot.impl import sat_minimize as sm return sm(aut, args, state_based) diff --git a/python/spot/impl.i b/python/spot/impl.i index 0593da1856d225b6ec7488e59828d5b6f7daa6bf..4181d0891cd5612a24ce424a964eb158bc822e89 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -143,6 +143,9 @@ #include +#include +#include + #include #include #include @@ -434,6 +437,9 @@ namespace std { %include +%include +%include + %include %include %include diff --git a/python/spot/ltsmin.i b/python/spot/ltsmin.i new file mode 100644 index 0000000000000000000000000000000000000000..13b18117c5136bfcb3f311fa05e7725b8acadaa2 --- /dev/null +++ b/python/spot/ltsmin.i @@ -0,0 +1,66 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2016 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") ltsmin + +%include "std_string.i" +%include "std_set.i" +%include "std_shared_ptr.i" + +%shared_ptr(spot::bdd_dict) +%shared_ptr(spot::twa) +%shared_ptr(spot::kripke) +%shared_ptr(spot::fair_kripke) + +%{ +#include +using namespace spot; +%} + +%import(module="spot.impl") +%import(module="spot.impl") +%import(module="spot.impl") +%import(module="spot.impl") +%import(module="spot.impl") +%import(module="spot.impl") +%import(module="spot.impl") + +namespace std { + %template(atomic_prop_set) set; +} + +%include + +%pythoncode %{ +import spot + +def load(filename, ap_set, dict=spot._bdd_dict, + dead=spot.formula_ap('dead'), + compress=2, debug=False): + s = spot.atomic_prop_set() + for ap in ap_set: + s.insert(spot.formula_ap(ap)) + return load_ltsmin(filename, dict, s, dead, compress, debug) +%} diff --git a/tests/Makefile.am b/tests/Makefile.am index 1e881dcb94cd33a6b14e820204d569328d5bb602..a69507cb4a3fda5c6c76d77c9ad0bfd210262e56 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -298,6 +298,7 @@ TESTS_python = \ python/ltl2tgba.test \ python/ltlparse.py \ python/ltlsimple.py \ + python/ltsmin.ipynb \ python/minato.py \ python/optionmap.py \ python/parsetgba.py \ @@ -315,6 +316,8 @@ TESTS_python = \ python/trival.py endif +CLEANFILES = python/finite.dve2C python/finite.dve.cpp + SUFFIXES = .ipynb .html .ipynb.html: $(IPYTHON) nbconvert $< --to html --stdout >$@ diff --git a/tests/python/ipnbdoctest.py b/tests/python/ipnbdoctest.py index 8069fe19ed3aee3848f989a0950aa6137be27dd7..f86ac5b82d6e3a7f8a124cbedfd4c1f74ccfde88 100755 --- a/tests/python/ipnbdoctest.py +++ b/tests/python/ipnbdoctest.py @@ -185,6 +185,10 @@ def run_cell(kc, cell): out.ename = content['ename'] out.evalue = content['evalue'] out.traceback = content['traceback'] + + # sys.exit(77) is used to Skip the test. + if out.ename == 'SystemExit' and out.evalue == '77': + sys.exit(77) else: print("unhandled iopub msg:", msg_type) diff --git a/tests/python/ltsmin.ipynb b/tests/python/ltsmin.ipynb new file mode 100644 index 0000000000000000000000000000000000000000..5346b61d9855f449e6f5c00d5ad5dc99940876f5 --- /dev/null +++ b/tests/python/ltsmin.ipynb @@ -0,0 +1,532 @@ +{ + "metadata": { + "name": "", + "signature": "sha256:d5994cc04991eaf218539c16319f17128cf42be5d813785fd977ee3d991a5c00" + }, + "nbformat": 3, + "nbformat_minor": 0, + "worksheets": [ + { + "cells": [ + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "This first chunk just makes sure the version of divine instaled accepts the `--LTSmin` option. If that is not the case, this notebook should be skipped by the test suite: `sys.exit(77)` does that." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "import os, sys\n", + "srcdir = os.environ.get('srcdir', '.')\n", + "# Make sure we have divine and that it is patched to accept the --LTSmin option.\n", + "import shutil\n", + "if shutil.which(\"divine\") == None:\n", + " sys.exit(77)\n", + "import subprocess\n", + "out = subprocess.check_output(['divine', 'compile', '--help'], stderr=subprocess.STDOUT)\n", + "if b'LTSmin' not in out:\n", + " sys.exit(77)" + ], + "language": "python", + "metadata": {}, + "outputs": [], + "prompt_number": 1 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "The real test case starts here." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "import spot\n", + "import spot.ltsmin\n", + "spot.setup()" + ], + "language": "python", + "metadata": {}, + "outputs": [], + "prompt_number": 2 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "m = spot.ltsmin.load(srcdir + '/../ltsmin/finite.dve', ['P.a<1', 'P.b>2'])\n", + "m" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 3, + "svg": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "P.a=0, P.b=0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "P.a=1, P.b=0\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + ""P.a<1" & !"P.b>2" & !dead\n", + "\n", + "\n", + "12\n", + "\n", + "P.a=0, P.b=1\n", + "\n", + "\n", + "0->12\n", + "\n", + "\n", + ""P.a<1" & !"P.b>2" & !dead\n", + "\n", + "\n", + "2\n", + "\n", + "P.a=2, P.b=0\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!"P.a<1" & !"P.b>2" & !dead\n", + "\n", + "\n", + "9\n", + "\n", + "P.a=1, P.b=1\n", + "\n", + "\n", + "1->9\n", + "\n", + "\n", + "!"P.a<1" & !"P.b>2" & !dead\n", + "\n", + "\n", + "12->9\n", + "\n", + "\n", + ""P.a<1" & !"P.b>2" & !dead\n", + "\n", + "\n", + "13\n", + "\n", + "P.a=0, P.b=2\n", + "\n", + "\n", + "12->13\n", + "\n", + "\n", + ""P.a<1" & !"P.b>2" & !dead\n", + "\n", + "\n", + "3\n", + "\n", + "P.a=3, P.b=0\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!"P.a<1" & !"P.b>2" & !dead\n", + "\n", + "\n", + "4\n", + "\n", + "P.a=2, P.b=1\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "!"P.a<1" & !"P.b>2" & !dead\n", + "\n", + "\n", + "9->4\n", + "\n", + "\n", + "!"P.a<1" & !"P.b>2" & !dead\n", + "\n", + "\n", + "10\n", + "\n", + "P.a=1, P.b=2\n", + "\n", + "\n", + "9->10\n", + "\n", + "\n", + "!"P.a<1" & !"P.b>2" & !dead\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!"P.a<1" & !"P.b>2" & dead\n", + "\n", + "\n", + "5\n", + "\n", + "P.a=3, P.b=1\n", + "\n", + "\n", + "4->5\n", + "\n", + "\n", + "!"P.a<1" & !"P.b>2" & !dead\n", + "\n", + "\n", + "6\n", + "\n", + "P.a=2, P.b=2\n", + "\n", + "\n", + "4->6\n", + "\n", + "\n", + "!"P.a<1" & !"P.b>2" & !dead\n", + "\n", + "\n", + "5->5\n", + "\n", + "\n", + "!"P.a<1" & !"P.b>2" & dead\n", + "\n", + "\n", + "7\n", + "\n", + "P.a=3, P.b=2\n", + "\n", + "\n", + "6->7\n", + "\n", + "\n", + "!"P.a<1" & !"P.b>2" & !dead\n", + "\n", + "\n", + "8\n", + "\n", + "P.a=2, P.b=3\n", + "\n", + "\n", + "6->8\n", + "\n", + "\n", + "!"P.a<1" & !"P.b>2" & !dead\n", + "\n", + "\n", + "7->7\n", + "\n", + "\n", + "!"P.a<1" & !"P.b>2" & dead\n", + "\n", + "\n", + "8->8\n", + "\n", + "\n", + "!"P.a<1" & "P.b>2" & dead\n", + "\n", + "\n", + "10->6\n", + "\n", + "\n", + "!"P.a<1" & !"P.b>2" & !dead\n", + "\n", + "\n", + "11\n", + "\n", + "P.a=1, P.b=3\n", + "\n", + "\n", + "10->11\n", + "\n", + "\n", + "!"P.a<1" & !"P.b>2" & !dead\n", + "\n", + "\n", + "11->11\n", + "\n", + "\n", + "!"P.a<1" & "P.b>2" & dead\n", + "\n", + "\n", + "13->10\n", + "\n", + "\n", + ""P.a<1" & !"P.b>2" & !dead\n", + "\n", + "\n", + "14\n", + "\n", + "P.a=0, P.b=3\n", + "\n", + "\n", + "13->14\n", + "\n", + "\n", + ""P.a<1" & !"P.b>2" & !dead\n", + "\n", + "\n", + "14->14\n", + "\n", + "\n", + ""P.a<1" & "P.b>2" & dead\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7f40740974e0> >" + ] + } + ], + "prompt_number": 3 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "a = spot.translate('\"P.a<1\" U \"P.b>2\"'); a" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 4, + "svg": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "I->1\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + ""P.a<1" & !"P.b>2"\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + ""P.b>2"\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7f40740977e0> >" + ] + } + ], + "prompt_number": 4 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "spot.otf_product(m, a)" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 5, + "svg": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "P.a=0, P.b=0 * 1\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "P.a=1, P.b=0 * 1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + ""P.a<1" & !"P.b>2" & !dead\n", + "\n", + "\n", + "2\n", + "\n", + "P.a=0, P.b=1 * 1\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + ""P.a<1" & !"P.b>2" & !dead\n", + "\n", + "\n", + "3\n", + "\n", + "P.a=1, P.b=1 * 1\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + ""P.a<1" & !"P.b>2" & !dead\n", + "\n", + "\n", + "4\n", + "\n", + "P.a=0, P.b=2 * 1\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + ""P.a<1" & !"P.b>2" & !dead\n", + "\n", + "\n", + "5\n", + "\n", + "P.a=1, P.b=2 * 1\n", + "\n", + "\n", + "4->5\n", + "\n", + "\n", + ""P.a<1" & !"P.b>2" & !dead\n", + "\n", + "\n", + "6\n", + "\n", + "P.a=0, P.b=3 * 1\n", + "\n", + "\n", + "4->6\n", + "\n", + "\n", + ""P.a<1" & !"P.b>2" & !dead\n", + "\n", + "\n", + "7\n", + "\n", + "P.a=0, P.b=3 * 0\n", + "\n", + "\n", + "6->7\n", + "\n", + "\n", + ""P.a<1" & "P.b>2" & dead\n", + "\n", + "\n", + "7->7\n", + "\n", + "\n", + ""P.a<1" & "P.b>2" & dead\n", + "\u24ff\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7f4074097720> >" + ] + } + ], + "prompt_number": 5 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [], + "language": "python", + "metadata": {}, + "outputs": [], + "prompt_number": 5 + } + ], + "metadata": {} + } + ] +} \ No newline at end of file