From da051e112d2ff13a4f7cd20eaf9848ed6968610e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Gillard?= Date: Tue, 7 Feb 2017 17:35:33 +0100 Subject: [PATCH] decompose_scc: Update 'decompose' notebook * tests/python/decompose.ipynb: Add about `decompose_scc`. * doc/org/tut.org: Update description. --- doc/org/tut.org | 2 +- tests/python/decompose.ipynb | 258 ++++++++++++++++++++++++++++++++++- 2 files changed, 255 insertions(+), 5 deletions(-) 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", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "cluster_0\n", + "\n", + "\n", + "cluster_1\n", + "\n", + "\n", + "cluster_2\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", + "\u24ff\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "a & c\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !c\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", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "cluster_0\n", + "\n", + "\n", + "cluster_1\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & c\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7f6aa02181e0> >" + ] + } + ], + "prompt_number": 30 }, { "cell_type": "code",