diff --git a/doc/org/tut.org b/doc/org/tut.org
index 639b8af51..6233324bc 100644
--- a/doc/org/tut.org
+++ b/doc/org/tut.org
@@ -68,3 +68,5 @@ real notebooks instead.
- [[https://spot.lrde.epita.fr/ipynb/word.html][=word.ipynb=]] example for the =twa_run= and =twa_word= classes.
- [[https://spot.lrde.epita.fr/ipynb/highlighting.html][=highlighting.ipynb=]] shows how to highlight states or edges in
automata.
+- [[https://spot.lrde.epita.fr/ipynb/atva16-fig2a.html][=atva16-fig2a.ipynb=]] first example from our [[https://www.lrde.epita.fr/~adl/dl/adl/duret.16.atva2.pdf][ATVA'16 tool paper]].
+- [[https://spot.lrde.epita.fr/ipynb/atva16-fig2b.html][=atva16-fig2b.ipynb=]] second example from our [[https://www.lrde.epita.fr/~adl/dl/adl/duret.16.atva2.pdf][ATVA'16 tool paper]].
diff --git a/tests/Makefile.am b/tests/Makefile.am
index 3c585789a..858106b57 100644
--- a/tests/Makefile.am
+++ b/tests/Makefile.am
@@ -291,6 +291,8 @@ if USE_PYTHON
TESTS_ipython = \
python/acc_cond.ipynb \
python/accparse.ipynb \
+ python/atva16-fig2a.ipynb \
+ python/atva16-fig2b.ipynb \
python/automata-io.ipynb \
python/automata.ipynb \
python/decompose.ipynb \
diff --git a/tests/python/atva16-fig2a.ipynb b/tests/python/atva16-fig2a.ipynb
new file mode 100644
index 000000000..8e2b789aa
--- /dev/null
+++ b/tests/python/atva16-fig2a.ipynb
@@ -0,0 +1,261 @@
+{
+ "metadata": {
+ "kernelspec": {
+ "display_name": "Python 3",
+ "language": "python",
+ "name": "python3"
+ },
+ "language_info": {
+ "codemirror_mode": {
+ "name": "ipython",
+ "version": 3
+ },
+ "file_extension": ".py",
+ "mimetype": "text/x-python",
+ "name": "python",
+ "nbconvert_exporter": "python",
+ "pygments_lexer": "ipython3",
+ "version": "3.5.2rc1"
+ },
+ "name": ""
+ },
+ "nbformat": 3,
+ "nbformat_minor": 0,
+ "worksheets": [
+ {
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "This example is the left part of Fig.2 in our ATVA'16 paper titled \"*Spot 2.0 \u2014 a framework for LTL and \u03c9-automata manipulation*\"."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "collapsed": true,
+ "input": [
+ "import spot\n",
+ "spot.setup(show_default='.abr')"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [],
+ "prompt_number": 1
+ },
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "f = spot.formula('GFa <-> GFb'); f"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [
+ {
+ "latex": [
+ "$\\mathsf{G} \\mathsf{F} a \\leftrightarrow \\mathsf{G} \\mathsf{F} b$"
+ ],
+ "metadata": {},
+ "output_type": "pyout",
+ "prompt_number": 2,
+ "text": [
+ "GFa <-> GFb"
+ ]
+ }
+ ],
+ "prompt_number": 2
+ },
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "f.translate()"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [
+ {
+ "metadata": {},
+ "output_type": "pyout",
+ "prompt_number": 3,
+ "svg": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text": [
+ " *' at 0x7f77f87ba300> >"
+ ]
+ }
+ ],
+ "prompt_number": 3
+ },
+ {
+ "cell_type": "code",
+ "collapsed": true,
+ "input": [
+ "def implies(f, g):\n",
+ " f = spot.formula(f)\n",
+ " g = spot.formula_Not(spot.formula(g))\n",
+ " return spot.product(f.translate(), g.translate()).is_empty()\n",
+ "def equiv(f, g):\n",
+ " return implies(f, g) and implies(g, f)"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [],
+ "prompt_number": 4
+ },
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "equiv('a U (b U a)', 'b U a')"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [
+ {
+ "metadata": {},
+ "output_type": "pyout",
+ "prompt_number": 5,
+ "text": [
+ "True"
+ ]
+ }
+ ],
+ "prompt_number": 5
+ },
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "equiv('!(a U b)', '!a U !b')"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [
+ {
+ "metadata": {},
+ "output_type": "pyout",
+ "prompt_number": 6,
+ "text": [
+ "False"
+ ]
+ }
+ ],
+ "prompt_number": 6
+ }
+ ],
+ "metadata": {}
+ }
+ ]
+}
diff --git a/tests/python/atva16-fig2b.ipynb b/tests/python/atva16-fig2b.ipynb
new file mode 100644
index 000000000..59023578d
--- /dev/null
+++ b/tests/python/atva16-fig2b.ipynb
@@ -0,0 +1,340 @@
+{
+ "metadata": {
+ "kernelspec": {
+ "display_name": "Python 3",
+ "language": "python",
+ "name": "python3"
+ },
+ "language_info": {
+ "codemirror_mode": {
+ "name": "ipython",
+ "version": 3
+ },
+ "file_extension": ".py",
+ "mimetype": "text/x-python",
+ "name": "python",
+ "nbconvert_exporter": "python",
+ "pygments_lexer": "ipython3",
+ "version": "3.5.2rc1"
+ },
+ "name": ""
+ },
+ "nbformat": 3,
+ "nbformat_minor": 0,
+ "worksheets": [
+ {
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "This example is the right part of Fig.2 in our ATVA'16 paper titled \"*Spot 2.0 \u2014 a framework for LTL and \u03c9-automata manipulation*\"."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "collapsed": true,
+ "input": [
+ "import spot\n",
+ "import spot.ltsmin\n",
+ "spot.setup(show_default='.abr', max_states=10)\n",
+ "# This extra line ensures that our test-suite skips this test if divine is not installed.\n",
+ "spot.ltsmin.require('divine')"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [],
+ "prompt_number": 1
+ },
+ {
+ "cell_type": "code",
+ "collapsed": true,
+ "input": [
+ "%%dve adding\n",
+ "int c=1, x1, x2;\n",
+ "process a1 {\n",
+ " state Q, R, S; init Q;\n",
+ " trans Q -> R { guard c<20; effect x1 = c; },\n",
+ " R -> S { effect x1 = x1 + c; },\n",
+ " S -> Q { effect c = x1; };\n",
+ "}\n",
+ "process a2 {\n",
+ " state Q, R, S; init Q;\n",
+ " trans Q -> R { guard c<20; effect x2 = c; },\n",
+ " R -> S { effect x2 = x2 + c; },\n",
+ " S -> Q { effect c = x2; };\n",
+ "}\n",
+ "system async;"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [],
+ "prompt_number": 2
+ },
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "adding"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [
+ {
+ "metadata": {},
+ "output_type": "pyout",
+ "prompt_number": 3,
+ "text": [
+ "ltsmin model with the following variables:\n",
+ " c: int\n",
+ " x1: int\n",
+ " x2: int\n",
+ " a1: ['Q', 'R', 'S']\n",
+ " a2: ['Q', 'R', 'S']"
+ ]
+ }
+ ],
+ "prompt_number": 3
+ },
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "adding.kripke(['a1.Q', 'c==17'])"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [
+ {
+ "metadata": {},
+ "output_type": "pyout",
+ "prompt_number": 4,
+ "svg": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text": [
+ " *' at 0x7f3406f6f5d0> >"
+ ]
+ }
+ ],
+ "prompt_number": 4
+ },
+ {
+ "cell_type": "code",
+ "collapsed": true,
+ "input": [
+ "def model_check(model, f):\n",
+ " f = spot.formula(f)\n",
+ " ss = model.kripke(spot.atomic_prop_collect(f))\n",
+ " nf = spot.formula_Not(f).translate()\n",
+ " return spot.otf_product(ss, nf).is_empty()"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [],
+ "prompt_number": 5
+ },
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "model_check(adding, 'F(\"c==2\")')"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [
+ {
+ "metadata": {},
+ "output_type": "pyout",
+ "prompt_number": 6,
+ "text": [
+ "True"
+ ]
+ }
+ ],
+ "prompt_number": 6
+ }
+ ],
+ "metadata": {}
+ }
+ ]
+}