diff --git a/doc/org/tut.org b/doc/org/tut.org
index d799d0cdc..2cb7354d3 100644
--- a/doc/org/tut.org
+++ b/doc/org/tut.org
@@ -68,7 +68,7 @@ real notebooks instead.
- [[https://spot.lrde.epita.fr/ipynb/product.html][=product.ipynb=]] shows how to re-implement the product of two automata
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/decompose.html][=decompose.ipynb=]] illustrates the =decompose_strength()=, =decompose_acc_scc()= and =decompose_scc()= functions
- [[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-dve.html][=ltsmin-dve.ipynb=]] loading a DiVinE model using the LTSmin interface.
diff --git a/tests/python/decompose.ipynb b/tests/python/decompose.ipynb
index 9f21cc2e2..8740d8c03 100644
--- a/tests/python/decompose.ipynb
+++ b/tests/python/decompose.ipynb
@@ -43,7 +43,7 @@
"source": [
"This notebook demonstrates how to use the `decompose_strength()` function to split an automaton in up to three automata capturing different behaviors. This is based on the paper [Strength-based decomposition of the property B\u00fcchi automaton for faster model checking](https://www.lrde.epita.fr/~adl/dl/adl/renault.13.tacas.pdf) (TACAS'13).\n",
"\n",
- "This page uses the Python bindings, but the same decompositions can be performed from the shell using [`autfilt`](https://spot.lrde.epita.fr/autfilt.html) and its `--decompose-strength` option.\n",
+ "This page uses the Python bindings, but the same decompositions can be performed from the shell using [`autfilt`](https://spot.lrde.epita.fr/autfilt.html) and its `--decompose-strength` and `--decompose-scc` option.\n",
"\n",
"# Basics\n",
"\n",
@@ -4993,14 +4993,264 @@
],
"prompt_number": 20
},
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "collapsed": false
+ },
+ "source": [
+ "# `decompose_acc_scc()`\n",
+ "\n",
+ "Similarly to `decompose_strength()`, the `decompose_acc_scc()` function takes an automaton and the index of an accepting SCC, and preserves only this SCC and its upstream SCCs:"
+ ]
+ },
{
"cell_type": "code",
"collapsed": false,
- "input": [],
+ "input": [
+ "aut = spot.translate('(Ga -> Gb) W c')\n",
+ "spot.decompose_acc_scc(aut, 1)"
+ ],
"language": "python",
"metadata": {},
- "outputs": [],
- "prompt_number": null
+ "outputs": [
+ {
+ "metadata": {},
+ "output_type": "pyout",
+ "prompt_number": 21,
+ "svg": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text": [
+ " *' at 0x7ff37c13b1b0> >"
+ ]
+ }
+ ],
+ "prompt_number": 21
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {
+ "collapsed": true
+ },
+ "source": [
+ "# `decompose_scc()`\n",
+ "\n",
+ "You can also, like in the C++ interface, use a `scc_info` to extract a particular SCC and its parents, even non accepting."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "si = spot.scc_info(aut)\n",
+ "spot.decompose_scc(si, 2)"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [
+ {
+ "metadata": {},
+ "output_type": "pyout",
+ "prompt_number": 30,
+ "svg": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text": [
+ " *' at 0x7f6aa02181e0> >"
+ ]
+ }
+ ],
+ "prompt_number": 30
},
{
"cell_type": "code",