From 104a372c41de1492b07ecaff67b1a8f7069bc6dc Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 8 Nov 2015 21:37:47 +0100 Subject: [PATCH] Add a notebook illustrating decompose_strength() * wrap/python/tests/decompose.ipynb: New file. * wrap/python/tests/Makefile.am: Add it. * src/twaalgos/strength.cc: Fix corner cases. * src/tests/strength.test: Adjust corner case. * NEWS, doc/org/tut.org: Mention the notebook. --- NEWS | 2 + doc/org/tut.org | 1 + src/tests/strength.test | 10 +- src/twaalgos/strength.cc | 46 +- wrap/python/tests/Makefile.am | 1 + wrap/python/tests/decompose.ipynb | 4800 +++++++++++++++++++++++++++++ 6 files changed, 4839 insertions(+), 21 deletions(-) create mode 100644 wrap/python/tests/decompose.ipynb diff --git a/NEWS b/NEWS index c3e32a2e8..ed07a01af 100644 --- a/NEWS +++ b/NEWS @@ -6,6 +6,8 @@ New in spot 1.99.5a (not yet released) * autfilt has a new transformation: --decompose-strength, implementing the decomposition of our TACAS'13 paper. + A demonstration of this feature via the Python bindings + can be found at https://spot.lrde.epita.fr/ipynb/decompose.html * All tools that output HOA files accept a --check=strength option to request automata to be marked as "weak" or "terminal" as diff --git a/doc/org/tut.org b/doc/org/tut.org index 2fb7d1517..9e5ae92be 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -54,5 +54,6 @@ real notebooks instead. after acceptance simplification - [[https://spot.lrde.epita.fr/ipynb/accparse.html][accparse.ipynb]] exercises the acceptance condition parser - [[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/testingaut.html][testingaut.ipynb]] shows the step necessary to build a testing automaton diff --git a/src/tests/strength.test b/src/tests/strength.test index 5417f3932..96ecd885f 100755 --- a/src/tests/strength.test +++ b/src/tests/strength.test @@ -535,14 +535,14 @@ HOA: v1 States: 2 Start: 0 AP: 0 -acc-name: all -Acceptance: 0 t -properties: trans-labels explicit-labels state-acc complete +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc colored complete properties: deterministic weak --BODY-- -State: 0 +State: 0 {0} [t] 1 -State: 1 +State: 1 {0} [t] 0 --END-- HOA: v1 diff --git a/src/twaalgos/strength.cc b/src/twaalgos/strength.cc index 2dca4be34..1aa581bf9 100644 --- a/src/twaalgos/strength.cc +++ b/src/twaalgos/strength.cc @@ -148,6 +148,33 @@ namespace spot (std::string("unknown option for decompose_strength(): ") + c); } + acc_cond::mark_t wacc = 0U; // Acceptance for weak SCCs + acc_cond::mark_t uacc = 0U; // Acceptance for "needed" SCCs, that + // we only want to traverse. + + // If the acceptance condition is always satisfiable, we will + // consider the automaton has weak (even if that is not the + // case syntactically) and not output any strong part. + bool all_accepting = false; + if (aut->acc().is_tt()) + { + all_accepting = true; + } + else if (aut->acc().uses_fin_acceptance()) + { + auto p = aut->get_acceptance().unsat_mark(); + if (p.first) + uacc = p.second; + else + all_accepting = true; + } + if (all_accepting) + { + keep &= ~Strong; + if (keep == Ignore) + return nullptr; + } + scc_info si(aut); si.determine_unknown_acceptance(); @@ -160,7 +187,7 @@ namespace spot { if (si.is_accepting_scc(i)) { - if (is_weak_scc(si, i)) + if (all_accepting | is_weak_scc(si, i)) { if (keep & Weak) { @@ -194,23 +221,10 @@ namespace spot res->copy_ap_of(aut); res->prop_copy(aut, { true, false, true, false }); - acc_cond::mark_t wacc = 0U; // Acceptance for weak SCCs - acc_cond::mark_t uacc = 0U; // Acceptance for "needed" SCCs, that - // we only want to traverse. if (keep & Strong) - { - res->copy_acceptance_of(aut); - auto& ac = res->acc(); - if (ac.uses_fin_acceptance()) - // Note that we ignore the cases where the acceptance - // condition is always satisfiable. In that case - // uacc will be set to 0U, which will be satisfiable - uacc = ac.get_acceptance().unsat_mark().second; - } + res->copy_acceptance_of(aut); else - { - wacc = res->set_buchi(); - } + wacc = res->set_buchi(); auto fun = [&si, &want, uacc, wacc, keep] (unsigned src, bdd& cond, acc_cond::mark_t& acc, unsigned dst) diff --git a/wrap/python/tests/Makefile.am b/wrap/python/tests/Makefile.am index 905b639d3..41c22c097 100644 --- a/wrap/python/tests/Makefile.am +++ b/wrap/python/tests/Makefile.am @@ -37,6 +37,7 @@ TESTS = \ automata.ipynb \ automata-io.ipynb \ bddnqueen.py \ + decompose.ipynb \ formulas.ipynb \ implies.py \ interdep.py \ diff --git a/wrap/python/tests/decompose.ipynb b/wrap/python/tests/decompose.ipynb new file mode 100644 index 000000000..682685fe5 --- /dev/null +++ b/wrap/python/tests/decompose.ipynb @@ -0,0 +1,4800 @@ +{ + "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.4.3+" + }, + "name": "" + }, + "nbformat": 3, + "nbformat_minor": 0, + "worksheets": [ + { + "cells": [ + { + "cell_type": "code", + "collapsed": true, + "input": [ + "from IPython.display import display\n", + "import spot\n", + "spot.setup()" + ], + "language": "python", + "metadata": {}, + "outputs": [], + "prompt_number": 1 + }, + { + "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", + "\n", + "# Basics\n", + "\n", + "Let's define the following strengths of SCCs:\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", + "- an accepting SCC is **strong** if it is not weak.\n", + "\n", + "The strengths **strong**, **stricly weak**, and **terminal** define a partition of all accepting SCCs. The following B\u00fcchi automaton has 4 SCCs, and its 3 accepting SCCs show an example of each strength." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "aut = spot.translate('(Ga -> Gb) W c')\n", + "aut.show('.sa')" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 2, + "svg": [ + "\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", + "cluster_3\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "I->1\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!a & !c\n", + "\u24ff\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "b\n", + "\u24ff\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "1\n", + "\u24ff\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!a & !c\n", + "\u24ff\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "a & c\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + } + ], + "prompt_number": 2 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "The `strength_decompose()` function takes an automaton, and a string specifying which strength to preserve. \n", + "\n", + "The letters used for this specification are as follows:\n", + "- `t`: terminal\n", + "- `w`: strictly weak\n", + "- `s`: strong\n", + "\n", + "For instance if we want to preserve only the **strictly weak** part of this automaton, we should get only the SCC with the self-loop on $b$, and the SCC above it so that we can reach it. However the SCC above is not stricly weak, so it should not accept any word in the new automaton." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "sweak = spot.decompose_strength(aut, 'w')\n", + "sweak.show('.sa')" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 3, + "svg": [ + "\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 & b & !c\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "b\n", + "\u24ff\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + } + ], + "prompt_number": 3 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Similarly, we can extract all the behaviors captured by the **terminal** part of the automaton:" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "term = spot.decompose_strength(aut, 't')\n", + "term.show('.sa')" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 4, + "svg": [ + "\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", + "" + ], + "text": [ + "" + ] + } + ], + "prompt_number": 4 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Here is the strong part:" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "strong = spot.decompose_strength(aut, 's')\n", + "strong.show('.sa')" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 5, + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "cluster_0\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", + "\u24ff\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a & !c\n", + "\u24ff\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + } + ], + "prompt_number": 5 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "The union of these three automata recognize the same language as the original automaton.\n", + "\n", + "\n", + "The application proposed in the aforementioned TACAS'13 paper is for parallelizing model checking. Instead of testing the emptiness of the product between `aut` and a system, one could test the emptiness **3** products in parallel: each with a sub-automaton of different strength. Model checking using weak and terminal automata can be done with much more simpler emptiness check procedures than needed for the general case. So in effect, we have isolated the \"hard\" (i.e. strong) part of the original automaton in a smaller automaton, and we only need to use a full-fledged emptiness check for this case.\n", + "\n", + "An additional bonus is that it is possible that the simplification algorithms will do a better job at simplifying the sub-automata than at simplifying the original `aut`. For instance here the `strong` automaton can be further simplified:" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "strong.postprocess('small')" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 6, + "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", + "0->0\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a & !c\n", + "\u24ff\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7fe318ffbf00> >" + ] + } + ], + "prompt_number": 6 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "# Multi-strength extraction\n", + "\n", + "The string passed to `decompose_strength()` can include multiple letters to extract multiple strengths at once." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "for opt in ('sw', 'st', 'wt'):\n", + " a = spot.decompose_strength(aut, opt)\n", + " a.set_name(\"option: \" + opt)\n", + " display(a.show('.asn'))" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "option: sw\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", + "\u24ff\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "b\n", + "\u24ff\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "!a & !c\n", + "\u24ff\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + }, + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "option: st\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", + "\u24ff\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", + "\u24ff\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", + "" + ], + "text": [ + "" + ] + }, + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "option: wt\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "cluster_0\n", + "\n", + "\n", + "cluster_1\n", + "\n", + "\n", + "cluster_2\n", + "\n", + "\n", + "cluster_3\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 & b & !c\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "b\n", + "\u24ff\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "1\n", + "\u24ff\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "a & c\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + } + ], + "prompt_number": 7 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "# Generalized acceptance\n", + "\n", + "There is (almost, see below) nothing that prevents the above decomposition to work with other types of acceptance.\n", + "\n", + "## Rabin\n", + "\n", + "The following Rabin automaton was generated with\n", + "\n", + " ltldo -f '(Ga -> Gb) W c' 'ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds' -H | autfilt -H --merge-transitions\n", + " \n", + "(The `autfilt -H --merge-transitions` pass is just here to reduce the size of the file and make the automaton more readable.)" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "aut = spot.automaton(\"\"\"\n", + "HOA: v1\n", + "States: 9\n", + "Start: 2\n", + "AP: 3 \"a\" \"b\" \"c\"\n", + "acc-name: Rabin 2\n", + "Acceptance: 4 (Fin(0) & Inf(1)) | (Fin(2) & Inf(3))\n", + "properties: trans-labels explicit-labels state-acc complete\n", + "properties: deterministic\n", + "--BODY--\n", + "State: 0 {2}\n", + "[0&!2] 0\n", + "[0&2] 1\n", + "[!0&!2] 5\n", + "[!0&2] 6\n", + "State: 1 {2}\n", + "[0] 1\n", + "[!0] 6\n", + "State: 2 {2}\n", + "[0&!1&!2] 3\n", + "[0&1&!2] 4\n", + "[!0&!2] 5\n", + "[2] 6\n", + "State: 3 {1 2}\n", + "[0&!2] 0\n", + "[0&2] 1\n", + "[!0&!2] 5\n", + "[!0&2] 6\n", + "State: 4 {1 2}\n", + "[0&!1&!2] 0\n", + "[0&!1&2] 1\n", + "[!0&!2] 5\n", + "[!0&2] 6\n", + "[0&1&!2] 7\n", + "[0&1&2] 8\n", + "State: 5 {1 2}\n", + "[0&!1&!2] 0\n", + "[!0&!2] 5\n", + "[2] 6\n", + "[0&1&!2] 7\n", + "State: 6 {1 2}\n", + "[t] 6\n", + "State: 7 {3}\n", + "[0&!1&!2] 0\n", + "[0&!1&2] 1\n", + "[!0&!2] 5\n", + "[!0&2] 6\n", + "[0&1&!2] 7\n", + "[0&1&2] 8\n", + "State: 8 {3}\n", + "[0&!1] 1\n", + "[!0] 6\n", + "[0&1] 8\n", + "--END--\n", + "\"\"\")\n", + "aut.show(\".as\")" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 8, + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "(Fin(\n", + "\u24ff\n", + ") & Inf(\n", + "\u2776\n", + ")) | (Fin(\n", + "\u2777\n", + ") & Inf(\n", + "\u2778\n", + "))\n", + "cluster_0\n", + "\n", + "\n", + "cluster_1\n", + "\n", + "\n", + "cluster_2\n", + "\n", + "\n", + "cluster_3\n", + "\n", + "\n", + "cluster_4\n", + "\n", + "\n", + "cluster_5\n", + "\n", + "\n", + "cluster_6\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\u2777\n", + "\n", + "\n", + "I->2\n", + "\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "6\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "2->6\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "2->5\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "6->6\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\u2777\n", + "\n", + "\n", + "1->6\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "8\n", + "\n", + "8\n", + "\u2778\n", + "\n", + "\n", + "8->6\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "8->1\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "8->8\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\u2777\n", + "\n", + "\n", + "0->6\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & c\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "0->5\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "5->6\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "5->0\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "5->5\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "7\n", + "\n", + "7\n", + "\u2778\n", + "\n", + "\n", + "5->7\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "7->6\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "7->1\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "7->8\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "7->0\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "7->5\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "7->7\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "3->6\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "a & c\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "3->5\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "4->6\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "4->1\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "4->8\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "4->0\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "4->5\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "4->7\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + } + ], + "prompt_number": 8 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Let's decompose it into three strengths:" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "for (name, opt) in (('terminal', 't'), ('strictly weak', 'w'), ('strong', 's')):\n", + " a = spot.decompose_strength(aut, opt)\n", + " a.set_name(name)\n", + " display(a.show('.asn'))" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "terminal\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "cluster_0\n", + "\n", + "\n", + "cluster_1\n", + "\n", + "\n", + "cluster_2\n", + "\n", + "\n", + "cluster_3\n", + "\n", + "\n", + "cluster_4\n", + "\n", + "\n", + "cluster_5\n", + "\n", + "\n", + "cluster_6\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "7\n", + "\n", + "7\n", + "\n", + "\n", + "7->4\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "7->7\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "8\n", + "\n", + "8\n", + "\n", + "\n", + "8->4\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "8->7\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "8->8\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "5->4\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "5->7\n", + "\n", + "\n", + "a & c\n", + "\n", + "\n", + "5->5\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "5->3\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "3->5\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "6\n", + "\n", + "6\n", + "\n", + "\n", + "3->6\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "6->4\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "6->7\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "6->8\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "6->5\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "6->3\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "6->6\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "1->7\n", + "\n", + "\n", + "a & c\n", + "\n", + "\n", + "1->5\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "2->7\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "2->8\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "2->5\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "2->6\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + }, + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "strictly weak\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "cluster_0\n", + "\n", + "\n", + "cluster_1\n", + "\n", + "\n", + "cluster_2\n", + "\n", + "\n", + "cluster_3\n", + "\n", + "\n", + "cluster_4\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "6->6\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "3->5\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "5->6\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "5->4\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "5->3\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "5->5\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "2->6\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "2->5\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + }, + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "strong\n", + "(Fin(\n", + "\u24ff\n", + ") & Inf(\n", + "\u2776\n", + ")) | (Fin(\n", + "\u2777\n", + ") & Inf(\n", + "\u2778\n", + "))\n", + "cluster_0\n", + "\n", + "\n", + "cluster_1\n", + "\n", + "\n", + "cluster_2\n", + "\n", + "\n", + "cluster_3\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\u2777\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\u2778\n", + "\n", + "\n", + "3->5\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "5->4\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "5->3\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "5->5\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "2->5\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + } + ], + "prompt_number": 9 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Note how the two weak automata (i.e., stricly weak and terminal) are now using a B\u00fcchi acceptance condition (because that is sufficient for weak automata) while the strong automaton inherited the original acceptance condition.\n", + "\n", + "When extracting multiple strengths and one of the strength is **strong**, we preserve the original acceptance. For instance extracting **strong** and **terminal** gives the following automaton, where only **stricly weak** SCCs have become rejecting." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "spot.decompose_strength(aut, \"st\").show(\".as\")" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 10, + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "(Fin(\n", + "\u24ff\n", + ") & Inf(\n", + "\u2776\n", + ")) | (Fin(\n", + "\u2777\n", + ") & Inf(\n", + "\u2778\n", + "))\n", + "cluster_0\n", + "\n", + "\n", + "cluster_1\n", + "\n", + "\n", + "cluster_2\n", + "\n", + "\n", + "cluster_3\n", + "\n", + "\n", + "cluster_4\n", + "\n", + "\n", + "cluster_5\n", + "\n", + "\n", + "cluster_6\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "7\n", + "\n", + "7\n", + "\n", + "\n", + "7->4\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "7->7\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "8\n", + "\n", + "8\n", + "\n", + "\n", + "8->4\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "8->7\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "8->8\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\u2777\n", + "\n", + "\n", + "5->4\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "5->7\n", + "\n", + "\n", + "a & c\n", + "\n", + "\n", + "5->5\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "5->3\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "3->5\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "6\n", + "\n", + "6\n", + "\u2778\n", + "\n", + "\n", + "3->6\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "6->4\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "6->7\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "6->8\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "6->5\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "6->3\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "6->6\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "1->7\n", + "\n", + "\n", + "a & c\n", + "\n", + "\n", + "1->5\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "2->7\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "2->8\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "2->5\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "2->6\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + } + ], + "prompt_number": 10 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "The weak automata seem to be good candidates for further simplification. Let's add a call to `postprocess()` to out decomposition loop, trying to preserve the determinism and state-based acceptance of the original automaton." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "for (name, opt) in (('terminal', 't'), ('strictly weak', 'w'), ('strong', 's')):\n", + " a = spot.decompose_strength(aut, opt).postprocess('deterministic', 'SBAcc')\n", + " a.set_name(name)\n", + " display(a.show('.asn'))" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "terminal\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "cluster_0\n", + "\n", + "\n", + "cluster_1\n", + "\n", + "\n", + "cluster_2\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "I->2\n", + "\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "a & c\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + }, + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "strictly weak\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "cluster_0\n", + "\n", + "\n", + "cluster_1\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "I->2\n", + "\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + }, + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "strong\n", + "(Fin(\n", + "\u24ff\n", + ") & Inf(\n", + "\u2776\n", + ")) | (Fin(\n", + "\u2777\n", + ") & Inf(\n", + "\u2778\n", + "))\n", + "cluster_0\n", + "\n", + "\n", + "cluster_1\n", + "\n", + "\n", + "cluster_2\n", + "\n", + "\n", + "cluster_3\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\u2777\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\u2778\n", + "\n", + "\n", + "3->5\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "5->3\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "5->4\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "5->5\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "2->5\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + } + ], + "prompt_number": 11 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "## Streett\n", + "\n", + "Since this notebook also serves as a test suite, let's try a Streett automaton. This one was generated with\n", + "\n", + " ltldo -f '(Ga -> Gb) W c' 'ltl2dstar --automata=streett --ltl2nba=spin:ltl2tgba@-Ds' -H | \n", + " autfilt -H --merge-transitions" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "aut = spot.automaton(\"\"\"\n", + "HOA: v1\n", + "States: 8\n", + "Start: 7\n", + "AP: 3 \"a\" \"b\" \"c\"\n", + "acc-name: Streett 2\n", + "Acceptance: 4 (Fin(0) | Inf(1)) & (Fin(2) | Inf(3))\n", + "properties: trans-labels explicit-labels state-acc complete\n", + "properties: deterministic\n", + "--BODY--\n", + "State: 0 {2}\n", + "[0&1] 0\n", + "[0&!1] 3\n", + "[!0] 4\n", + "State: 1 {2}\n", + "[0&1&2] 0\n", + "[0&1&!2] 1\n", + "[0&!1&!2] 2\n", + "[0&!1&2] 3\n", + "[!0&2] 4\n", + "[!0&!2] 7\n", + "State: 2 {2}\n", + "[0&1&!2] 1\n", + "[0&!1&!2] 2\n", + "[0&2] 3\n", + "[!0&2] 4\n", + "[!0&!2] 7\n", + "State: 3 {0 3}\n", + "[0] 3\n", + "[!0] 4\n", + "State: 4 {1 3}\n", + "[t] 4\n", + "State: 5 {3}\n", + "[0&!1] 3\n", + "[!0] 4\n", + "[0&1] 5\n", + "State: 6 {3}\n", + "[0&!1&!2] 2\n", + "[0&!1&2] 3\n", + "[!0&2] 4\n", + "[0&1&2] 5\n", + "[0&1&!2] 6\n", + "[!0&!2] 7\n", + "State: 7 {3}\n", + "[0&!1&!2] 2\n", + "[2] 4\n", + "[0&1&!2] 6\n", + "[!0&!2] 7\n", + "--END--\n", + "\"\"\")\n", + "aut.show(\".as\")" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 12, + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "(Fin(\n", + "\u24ff\n", + ") | Inf(\n", + "\u2776\n", + ")) & (Fin(\n", + "\u2777\n", + ") | Inf(\n", + "\u2778\n", + "))\n", + "cluster_0\n", + "\n", + "\n", + "cluster_1\n", + "\n", + "\n", + "cluster_2\n", + "\n", + "\n", + "cluster_3\n", + "\n", + "\n", + "cluster_4\n", + "\n", + "\n", + "\n", + "\n", + "7\n", + "\n", + "7\n", + "\u2778\n", + "\n", + "\n", + "I->7\n", + "\n", + "\n", + "\n", + "\n", + "7->7\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\u2776\n", + "\u2778\n", + "\n", + "\n", + "7->4\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\u2777\n", + "\n", + "\n", + "7->2\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "6\n", + "\n", + "6\n", + "\u2778\n", + "\n", + "\n", + "7->6\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\u24ff\n", + "\u2778\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\u2777\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\u2778\n", + "\n", + "\n", + "5->4\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "5->3\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "5->5\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "2->7\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "a & c\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\u2777\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "1->7\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "6->7\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "6->4\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "6->3\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "6->5\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "6->2\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "6->6\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + } + ], + "prompt_number": 12 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "for (name, opt) in (('terminal', 't'), ('strictly weak', 'w'), ('strong', 's')):\n", + " a = spot.decompose_strength(aut, opt)\n", + " a.set_name(name)\n", + " display(a.show('.asn'))" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "terminal\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "cluster_0\n", + "\n", + "\n", + "cluster_1\n", + "\n", + "\n", + "cluster_2\n", + "\n", + "\n", + "cluster_3\n", + "\n", + "\n", + "cluster_4\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\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", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "7->2\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "7->4\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "7->7\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "5->2\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "5->4\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "5->5\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "a & c\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "1->6\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "6->0\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "6->2\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "6->4\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "6->7\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "6->1\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "6->6\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "3->5\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + }, + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "strictly weak\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "cluster_0\n", + "\n", + "\n", + "cluster_1\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\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", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "4->0\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "4->1\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + }, + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "strong\n", + "(Fin(\n", + "\u24ff\n", + ") | Inf(\n", + "\u2776\n", + ")) & (Fin(\n", + "\u2777\n", + ") | Inf(\n", + "\u2778\n", + "))\n", + "cluster_0\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\u2778\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", + "\u2777\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\u2778\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\u2777\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + } + ], + "prompt_number": 13 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "The subtlety of Streett acceptance is that if a path that does not visit any accepting set infinitely often *is* accepting. So when disabling SCCs, we must be careful to label them with a combination of rejecting acceptance sets.\n", + "\n", + "This is easy to understand using an example. In the following extraction of the **strong** and **terminal** parts, the rejecting SCCs (that were either rejecting or strictly weak originally) have been labeled by the same acceptance sets, to ensure that they are rejected." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "spot.decompose_strength(aut, 'st').show('.as')" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 14, + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "(Fin(\n", + "\u24ff\n", + ") | Inf(\n", + "\u2776\n", + ")) & (Fin(\n", + "\u2777\n", + ") | Inf(\n", + "\u2778\n", + "))\n", + "cluster_0\n", + "\n", + "\n", + "cluster_1\n", + "\n", + "\n", + "cluster_2\n", + "\n", + "\n", + "cluster_3\n", + "\n", + "\n", + "cluster_4\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\u2778\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", + "\u2776\n", + "\u2778\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\u2777\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\u2778\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\u2777\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "7\n", + "\n", + "7\n", + "\u2777\n", + "\n", + "\n", + "7->2\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "7->4\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "7->7\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\u2777\n", + "\n", + "\n", + "5->2\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "5->4\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "5->5\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "a & c\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "6\n", + "\n", + "6\n", + "\u2777\n", + "\n", + "\n", + "1->6\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "6->0\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "6->2\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "6->4\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "6->7\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "6->1\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "6->6\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "3->5\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + } + ], + "prompt_number": 14 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "## Corner cases\n", + "\n", + "Here is the reason we said there is almost nothing preventing the decomposition to work for any acceptance condition.\n", + "To disable SCCs like above, the `decompose_strength()` must be able to find a set of acceptance sets to put those SCCs\n", + "in such that they will be rejected. This is impossible if the acceptance condition is always satisifiable.\n", + "\n", + "This include acceptances like `Acceptance: 0 t`, but also trickier ones like `Acceptance: 1 Inf(0) | Fin(0)` that you can make as complex as you fancy.\n", + "\n", + "### `Acceptance: 0 t`\n", + "\n", + "This is the least problematic case. Because automata with this acceptance are necessary weak, there is reason to extract the **strong** strength, and extracting the other two strengths will work as expected:" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "aut = spot.translate('(Gb|c) R a', 'any'); aut.show('.as')" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 15, + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "t\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", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & c\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + } + ], + "prompt_number": 15 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "# There is no strong part for this automaton\n", + "assert spot.decompose_strength(aut, 's') is None" + ], + "language": "python", + "metadata": {}, + "outputs": [], + "prompt_number": 16 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "for opt in ('w', 't'):\n", + " display(spot.decompose_strength(aut, opt).show('.as'))" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\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", + "\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", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + }, + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\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", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & c\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + } + ], + "prompt_number": 17 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "If we try to extract multiple strengths and include the (empty) strong part, this request will simply be ignored:" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "spot.decompose_strength(aut, 'st').show('.as')" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 18, + "svg": [ + "\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", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & c\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + } + ], + "prompt_number": 18 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Note that the above is exactly the output of `decompose_strength(aut, 't')`. The `'s'` flag was actively ignored. If `'s'` had not been ignored an the automaton processed as if its strong part had to be preserved, the original acceptance conditions would have been used, and this would have prevented the disabling of the initial SCC." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "### `Acceptance: 1 Inf(0) | Fin(0)`\n", + "\n", + "This acceptance could be replaced by `Acceptance: 0 t` without altering the language of the automaton. However its use of acceptance sets allows us to define some automata with strong SCCs." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "aut = spot.automaton(\"\"\"\n", + "HOA: v1\n", + "States: 4\n", + "Start: 0\n", + "AP: 1 \"a\"\n", + "Acceptance: 1 Inf(0) | Fin(0)\n", + "--BODY--\n", + "State: 0\n", + "[0] 0 \n", + "[!0] 1\n", + "State: 1\n", + "[0] 1 \n", + "[!0] 2 {0}\n", + "State: 2\n", + "[0] 1\n", + "[!0] 3\n", + "State: 3\n", + "[t] 3 {0}\n", + "--END--\n", + "\"\"\")\n", + "aut.show('.as')" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 19, + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u24ff\n", + ") | Fin(\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\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "1\n", + "\u24ff\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!a\n", + "\u24ff\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + } + ], + "prompt_number": 19 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "By our definitions, SCC $\\{0\\}$ is stricly weak, SCC $\\{1,2\\}$ is strong, and SCC $\\{3\\}$ is terminal.\n", + "\n", + "However with this acceptance condition, we would be unable to extract only the strong behaviors: because that would require a way to disable the SCC $\\{0\\}$, and we cannot do that with this acceptance condition. This could be solved by adding a new acceptance set, but if we are about the modify the accepance condition, it seems wiser to simply it.\n", + "Our solution to this problem is that whenever an acceptance condition is always satisfiable, we consider the entire automaton as weak, and ignore all requests to extract the strong part. As a consequence, the output will always use B\u00fcchi acceptance." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "for (name, opt) in (('terminal', 't'), ('strictly weak', 'w'), ('strong', 's'), ('all strengths', 'swt')):\n", + " a = spot.decompose_strength(aut, opt)\n", + " if a:\n", + " a.set_name(name)\n", + " display(a.show('.asn'))\n", + " else:\n", + " print(\"no output for \" + name)" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "terminal\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\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "1\n", + "\u24ff\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + }, + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "strictly weak\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\n", + "\u24ff\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!a\n", + "\u24ff\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a\n", + "\u24ff\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!a\n", + "\u24ff\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "a\n", + "\u24ff\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + }, + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "no output for strong\n" + ] + }, + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "all strengths\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\n", + "\u24ff\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!a\n", + "\u24ff\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "1\n", + "\u24ff\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a\n", + "\u24ff\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!a\n", + "\u24ff\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a\n", + "\u24ff\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "a\n", + "\u24ff\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + } + ], + "prompt_number": 20 + } + ], + "metadata": {} + } + ] +} \ No newline at end of file