diff --git a/wrap/python/tests/decompose.ipynb b/wrap/python/tests/decompose.ipynb index 682685fe5..80d4b12e9 100644 --- a/wrap/python/tests/decompose.ipynb +++ b/wrap/python/tests/decompose.ipynb @@ -17,7 +17,8 @@ "pygments_lexer": "ipython3", "version": "3.4.3+" }, - "name": "" + "name": "", + "signature": "sha256:80d55ee45e6262dfcb29a53e9df5940e6a49ea8584e10e97963faeee4ace738a" }, "nbformat": 3, "nbformat_minor": 0, @@ -41,11 +42,14 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "This notebook demonstrates how to use the `strength_decompose()` 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", + "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", "\n", "# Basics\n", "\n", "Let's define the following strengths of SCCs:\n", + "\n", "- an accepting SCC is **weak** if all its transitions belong to the same acceptance sets\n", "- an accepting SCC is **terminal** if it is *weak* and complete (i.e. from any state, you can stay in the SCC by reading any word)\n", "- an accepting SCC is **strictly weak** if it is *weak* and not complete (in other words: *weak* but not *terminal*)\n", @@ -199,7 +203,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -209,9 +213,10 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "The `strength_decompose()` function takes an automaton, and a string specifying which strength to preserve. \n", + "The `decompose_strength()` function takes an automaton, and a string specifying which strength to preserve. \n", "\n", "The letters used for this specification are as follows:\n", + "\n", "- `t`: terminal\n", "- `w`: strictly weak\n", "- `s`: strong\n", @@ -309,7 +314,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -444,7 +449,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -528,7 +533,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -599,7 +604,7 @@ "\n" ], "text": [ - " *' at 0x7fe318ffbf00> >" + " *' at 0x7fd4fcbe7720> >" ] } ], @@ -708,7 +713,7 @@ "" ], "text": [ - "" + "" ] }, { @@ -825,7 +830,7 @@ "" ], "text": [ - "" + "" ] }, { @@ -961,7 +966,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -1359,7 +1364,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -1677,7 +1682,7 @@ "" ], "text": [ - "" + "" ] }, { @@ -1867,7 +1872,7 @@ "" ], "text": [ - "" + "" ] }, { @@ -2040,7 +2045,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -2368,7 +2373,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -2505,7 +2510,7 @@ "" ], "text": [ - "" + "" ] }, { @@ -2617,7 +2622,7 @@ "" ], "text": [ - "" + "" ] }, { @@ -2790,7 +2795,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -3140,7 +3145,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -3423,7 +3428,7 @@ "" ], "text": [ - "" + "" ] }, { @@ -3568,7 +3573,7 @@ "" ], "text": [ - "" + "" ] }, { @@ -3698,7 +3703,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -3994,7 +3999,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -4100,7 +4105,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -4185,7 +4190,7 @@ "" ], "text": [ - "" + "" ] }, { @@ -4244,7 +4249,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -4323,7 +4328,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -4471,7 +4476,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -4596,7 +4601,7 @@ "" ], "text": [ - "" + "" ] }, { @@ -4677,7 +4682,7 @@ "" ], "text": [ - "" + "" ] }, { @@ -4787,7 +4792,7 @@ "" ], "text": [ - "" + "" ] } ],