From 5a5f83f468915343240cb45a86d9a08de4b09b99 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 31 Jan 2016 21:05:44 +0100 Subject: [PATCH] python: add missing bindings for twa_word and twa_run Fixes #133. * python/spot/impl.i: Add bindings for twa_word. Add a __repr__ for twa_run, and instantiate templates for twa_run's members. * tests/python/word.ipynb: New file with examples. * tests/Makefile.am, doc/org/tut.org: Add it. --- doc/org/tut.org | 1 + python/spot/impl.i | 30 ++++ tests/Makefile.am | 3 +- tests/python/word.ipynb | 302 ++++++++++++++++++++++++++++++++++++++++ 4 files changed, 335 insertions(+), 1 deletion(-) create mode 100644 tests/python/word.ipynb diff --git a/doc/org/tut.org b/doc/org/tut.org index b3f395133..7e04511e3 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -63,3 +63,4 @@ real notebooks instead. automaton - [[https://spot.lrde.epita.fr/ipynb/ltsmin.html][=ltsmin.ipynb=]] minimal test for loading a DiVinE model using the LTSmin interface. +- [[https://spot.lrde.epita.fr/ipynb/ltsmin.html][=word.ipynb=]] example for the =twa_run= and =twa_word= classes. diff --git a/python/spot/impl.i b/python/spot/impl.i index 4181d0891..81053ec42 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -63,6 +63,7 @@ %shared_ptr(spot::taa_tgba_formula) %shared_ptr(spot::twa_safra_complement) %shared_ptr(spot::twa_run) +%shared_ptr(spot::twa_word) %shared_ptr(spot::emptiness_check_result) %shared_ptr(spot::emptiness_check) %shared_ptr(spot::emptiness_check_instantiator) @@ -140,6 +141,7 @@ #include #include #include +#include #include @@ -411,7 +413,9 @@ namespace std { %include %include %include +%feature("flatnested") spot::twa_run::step; %include +%template(list_step) std::list; %include %include %include @@ -434,6 +438,9 @@ namespace std { %include %include %include +%include +%template(list_bdd) std::list; + %include @@ -605,6 +612,29 @@ namespace std { } %extend spot::twa_run { + std::string __repr__() + { + std::ostringstream os; + os << *self; + return os.str(); + } + + std::string __str__() + { + std::ostringstream os; + os << *self; + return os.str(); + } +} + +%extend spot::twa_word { + std::string __repr__() + { + std::ostringstream os; + os << *self; + return os.str(); + } + std::string __str__() { std::ostringstream os; diff --git a/tests/Makefile.am b/tests/Makefile.am index 1e22ade06..2a8a99a20 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -313,7 +313,8 @@ TESTS_python = \ python/satmin.py \ python/setxor.py \ python/testingaut.ipynb \ - python/trival.py + python/trival.py \ + python/word.ipynb endif CLEANFILES = python/test1.dve python/test1.dve2C python/test1.dve.cpp diff --git a/tests/python/word.ipynb b/tests/python/word.ipynb new file mode 100644 index 000000000..1e95f4e6f --- /dev/null +++ b/tests/python/word.ipynb @@ -0,0 +1,302 @@ +{ + "metadata": { + "name": "", + "signature": "sha256:e975b9a64657f38248c434a89f29b28f0bf90f9c40b7e8afdd7459734cbdcd38" + }, + "nbformat": 3, + "nbformat_minor": 0, + "worksheets": [ + { + "cells": [ + { + "cell_type": "code", + "collapsed": false, + "input": [ + "import spot\n", + "spot.setup()" + ], + "language": "python", + "metadata": {}, + "outputs": [], + "prompt_number": 1 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Let's build a small automaton to use as example." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "aut = spot.translate('G(Fa <-> Xb)'); aut" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 2, + "svg": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & b\n", + "\u24ff\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & b\n", + "\u24ff\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!a & !b\n", + "\u24ff\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7f4f0c2e0810> >" + ] + } + ], + "prompt_number": 2 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "The call to `couvreur99()` just instanciate the emptiness check, but does not run the check. Calling `check()` will return `None` if no accepting run was found. Otherwise the presence of the accepting run is established, but an accepting run hasn't necessarily been calculated: calling `accepting_run()` on the result will cause this computation to happen.\n", + "\n", + "\n", + "In the example below, we do not check the result of `check()` because we know that the input formula is satisfiable, so the automaton has an accepting run." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "run = spot.couvreur99(aut).check().accepting_run(); run" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 3, + "text": [ + "Prefix:\n", + " 0\n", + " | !a\n", + "Cycle:\n", + " 1\n", + " | a & b\t{0}\n", + " 2\n", + " | !a & b" + ] + } + ], + "prompt_number": 3 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Accessing the contents of the run can be done via the `prefix` and `cycle` lists." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "print(spot.bdd_format_formula(aut.get_dict(), run.prefix[0].label))\n", + "print(run.cycle[0].acc)" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "!a\n", + "{0}\n" + ] + } + ], + "prompt_number": 4 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "To convert the run into a word, using `spot.twa_word()`. Note that our runs are labeled by Boolean formulas that are not necessarily a conjunction of all involved litterals. The word is just the projection of the run on its labels." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "word = spot.twa_word(run); word" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 5, + "text": [ + "!a; cycle{a & b; !a & b}" + ] + } + ], + "prompt_number": 5 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Accessing the different formulas (stored as BDDs) can be done again via the `prefix` and `cycle` lists." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "print(spot.bdd_format_formula(aut.get_dict(), word.prefix[0]))\n", + "print(spot.bdd_format_formula(aut.get_dict(), word.cycle[0]))\n", + "print(spot.bdd_format_formula(aut.get_dict(), word.cycle[1]))" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "!a\n", + "a & b\n", + "!a & b\n" + ] + } + ], + "prompt_number": 6 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Calling `simplifify()` will produce a shorter word that is compatible with the original word. For instance in the above word, the initial `!a` is compatible with both `a & b` and `!a & b`. The word obtained by restricting `!a` to `!a & b` is therefore still accepted, but it allows removing the prefix by rotating the cycle:" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "word.simplify()\n", + "word" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 7, + "text": [ + "cycle{!a & b; a & b}" + ] + } + ], + "prompt_number": 7 + } + ], + "metadata": {} + } + ] +} \ No newline at end of file