diff --git a/wrap/python/spot.py b/wrap/python/spot.py index 25855977d..417ac2383 100644 --- a/wrap/python/spot.py +++ b/wrap/python/spot.py @@ -46,6 +46,7 @@ def _extend(*classes): return classes[0] return wrap +_show_default = None def setup(**kwargs): """Configure Spot for fancy display. @@ -68,6 +69,8 @@ def setup(**kwargs): (default: '10.2,5') font : str the font to use in the GraphViz output (default: 'Lato') + show_default : str + default options for show() """ import os @@ -78,6 +81,8 @@ def setup(**kwargs): bullets = 'B' if kwargs.get('bullets', True) else '' d = 'rf({})'.format(kwargs.get('font', 'Lato')) + bullets + global _show_default + _show_default = kwargs.get('show_default', None) os.environ['SPOT_DOTDEFAULT'] = d @@ -122,11 +127,17 @@ class twa: def _repr_svg_(self, opt=None): """Output the automaton as SVG""" ostr = ostringstream() + if opt is None: + global _show_default + opt = _show_default print_dot(ostr, self, opt) return _ostream_to_svg(ostr) def show(self, opt=None): """Display the automaton as SVG, in the IPython/Jupyter notebook""" + if opt is None: + global _show_default + opt = _show_default # Load the SVG function only if we need it. This way the # bindings can still be used outside of IPython if IPython is # not installed. diff --git a/wrap/python/tests/decompose.ipynb b/wrap/python/tests/decompose.ipynb index a153db058..e073a50e4 100644 --- a/wrap/python/tests/decompose.ipynb +++ b/wrap/python/tests/decompose.ipynb @@ -18,7 +18,7 @@ "version": "3.4.3+" }, "name": "", - "signature": "sha256:3d73c80c329ce7b32e9edaa2470fce5e27744462f43431affbbb771deb92aff2" + "signature": "sha256:b3b36fe78a04d878ed9e49766fcef5febec464e5c25ad302dd1f446e45b2fd36" }, "nbformat": 3, "nbformat_minor": 0, @@ -31,7 +31,7 @@ "input": [ "from IPython.display import display\n", "import spot\n", - "spot.setup()" + "spot.setup(show_default='.bans')" ], "language": "python", "metadata": {}, @@ -63,7 +63,7 @@ "collapsed": false, "input": [ "aut = spot.translate('(Ga -> Gb) W c')\n", - "aut.show('.sa')" + "aut" ], "language": "python", "metadata": {}, @@ -73,137 +73,144 @@ "output_type": "pyout", "prompt_number": 2, "svg": [ - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", "G\n", - "\n", - "Inf(\n", - "\u24ff\n", - ")\n", - "cluster_0\n", - "\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "cluster_0\n", + "\n", "\n", - "cluster_1\n", - "\n", + "cluster_1\n", + "\n", "\n", - "cluster_2\n", - "\n", + "cluster_2\n", + "\n", "\n", - "cluster_3\n", - "\n", + "cluster_3\n", + "\n", "\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "I->1\n", - "\n", - "\n", + "I->1\n", + "\n", + "\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "!a & !c\n", - "\u24ff\n", + "1->1\n", + "\n", + "\n", + "!a & !c\n", + "\u24ff\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "a & b & !c\n", + "1->0\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "3\n", - "\n", - "3\n", + "3\n", + "\n", + "3\n", "\n", "\n", - "1->3\n", - "\n", - "\n", - "c\n", + "1->3\n", + "\n", + "\n", + "c\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "2\n", + "\n", + "2\n", "\n", "\n", - "1->2\n", - "\n", - "\n", - "a & !c\n", + "1->2\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "b\n", - "\u24ff\n", + "0->0\n", + "\n", + "\n", + "b\n", + "\u24ff\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "1\n", - "\u24ff\n", + "3->3\n", + "\n", + "\n", + "1\n", + "\u24ff\n", "\n", "\n", - "4\n", - "\n", - "4\n", + "4\n", + "\n", + "4\n", "\n", "\n", - "4->3\n", - "\n", - "\n", - "!a\n", + "4->3\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "4->4\n", - "\n", - "\n", - "a\n", + "4->4\n", + "\n", + "\n", + "a\n", "\n", "\n", - "2->1\n", - "\n", - "\n", - "!a & !c\n", - "\u24ff\n", + "2->1\n", + "\n", + "\n", + "!a & !c\n", + "\u24ff\n", "\n", "\n", - "2->3\n", - "\n", - "\n", - "!a & c\n", + "2->3\n", + "\n", + "\n", + "!a & c\n", "\n", "\n", - "2->4\n", - "\n", - "\n", - "a & c\n", + "2->4\n", + "\n", + "\n", + "a & c\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "a & !c\n", + "2->2\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", - "" + "\n" ], "text": [ - "" + " *' at 0x7f8dcc0f7a50> >" ] } ], @@ -228,8 +235,7 @@ "cell_type": "code", "collapsed": false, "input": [ - "sweak = spot.decompose_strength(aut, 'w')\n", - "sweak.show('.sa')" + "spot.decompose_strength(aut, 'w')" ], "language": "python", "metadata": {}, @@ -239,82 +245,89 @@ "output_type": "pyout", "prompt_number": 3, "svg": [ - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", "G\n", - "\n", - "Inf(\n", - "\u24ff\n", - ")\n", - "cluster_0\n", - "\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "cluster_0\n", + "\n", "\n", - "cluster_1\n", - "\n", + "cluster_1\n", + "\n", "\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "!a & !c\n", + "0->0\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a & b & !c\n", + "0->1\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "2\n", + "\n", + "2\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "a & !c\n", + "0->2\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "b\n", - "\u24ff\n", + "1->1\n", + "\n", + "\n", + "b\n", + "\u24ff\n", "\n", "\n", - "2->0\n", - "\n", - "\n", - "!a & !c\n", + "2->0\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "a & !c\n", + "2->2\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", - "" + "\n" ], "text": [ - "" + " *' at 0x7f8dcc0f79c0> >" ] } ], @@ -331,8 +344,7 @@ "cell_type": "code", "collapsed": false, "input": [ - "term = spot.decompose_strength(aut, 't')\n", - "term.show('.sa')" + "spot.decompose_strength(aut, 't')" ], "language": "python", "metadata": {}, @@ -342,114 +354,121 @@ "output_type": "pyout", "prompt_number": 4, "svg": [ - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", "G\n", - "\n", - "Inf(\n", - "\u24ff\n", - ")\n", - "cluster_0\n", - "\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "cluster_0\n", + "\n", "\n", - "cluster_1\n", - "\n", + "cluster_1\n", + "\n", "\n", - "cluster_2\n", - "\n", + "cluster_2\n", + "\n", "\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "!a & !c\n", + "0->0\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "2\n", + "\n", + "2\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "c\n", + "0->2\n", + "\n", + "\n", + "c\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a & !c\n", + "0->1\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "1\n", - "\u24ff\n", + "2->2\n", + "\n", + "\n", + "1\n", + "\u24ff\n", "\n", "\n", - "3\n", - "\n", - "3\n", + "3\n", + "\n", + "3\n", "\n", "\n", - "3->2\n", - "\n", - "\n", - "!a\n", + "3->2\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "a\n", + "3->3\n", + "\n", + "\n", + "a\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "!a & !c\n", + "1->0\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "1->2\n", - "\n", - "\n", - "!a & c\n", + "1->2\n", + "\n", + "\n", + "!a & c\n", "\n", "\n", - "1->3\n", - "\n", - "\n", - "a & c\n", + "1->3\n", + "\n", + "\n", + "a & c\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "a & !c\n", + "1->1\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", - "" + "\n" ], "text": [ - "" + " *' at 0x7f8dcc0f7990> >" ] } ], @@ -466,8 +485,7 @@ "cell_type": "code", "collapsed": false, "input": [ - "strong = spot.decompose_strength(aut, 's')\n", - "strong.show('.sa')" + "strong = spot.decompose_strength(aut, 's'); strong" ], "language": "python", "metadata": {}, @@ -477,63 +495,70 @@ "output_type": "pyout", "prompt_number": 5, "svg": [ - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", "G\n", - "\n", - "Inf(\n", - "\u24ff\n", - ")\n", - "cluster_0\n", - "\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "cluster_0\n", + "\n", "\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "!a & !c\n", - "\u24ff\n", + "0->0\n", + "\n", + "\n", + "!a & !c\n", + "\u24ff\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a & !c\n", + "0->1\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "!a & !c\n", - "\u24ff\n", + "1->0\n", + "\n", + "\n", + "!a & !c\n", + "\u24ff\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "a & !c\n", + "1->1\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", - "" + "\n" ], "text": [ - "" + " *' at 0x7f8dcc0f7a20> >" ] } ], @@ -571,40 +596,46 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "cluster_0\n", + "\n", + "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a & !c\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!a & !c\n", - "\u24ff\n", + "\n", + "\n", + "!a & !c\n", + "\u24ff\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7fe3f46e3f00> >" + " *' at 0x7f8dcc11a3f0> >" ] } ], @@ -626,7 +657,7 @@ "for opt in ('sw', 'st', 'wt'):\n", " a = spot.decompose_strength(aut, opt)\n", " a.set_name(\"option: \" + opt)\n", - " display(a.show('.asn'))" + " display(a)" ], "language": "python", "metadata": {}, @@ -635,338 +666,359 @@ "metadata": {}, "output_type": "display_data", "svg": [ - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", "G\n", - "\n", - "option: sw\n", - "Inf(\n", - "\u24ff\n", - ")\n", - "cluster_0\n", - "\n", + "\n", + "option: sw\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "cluster_0\n", + "\n", "\n", - "cluster_1\n", - "\n", + "cluster_1\n", + "\n", "\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "!a & !c\n", - "\u24ff\n", + "0->0\n", + "\n", + "\n", + "!a & !c\n", + "\u24ff\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a & b & !c\n", + "0->1\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "2\n", + "\n", + "2\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "a & !c\n", + "0->2\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "b\n", - "\u24ff\n", + "1->1\n", + "\n", + "\n", + "b\n", + "\u24ff\n", "\n", "\n", - "2->0\n", - "\n", - "\n", - "!a & !c\n", - "\u24ff\n", + "2->0\n", + "\n", + "\n", + "!a & !c\n", + "\u24ff\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "a & !c\n", + "2->2\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", - "" + "\n" ], "text": [ - "" + " *' at 0x7f8dcc11a0f0> >" ] }, { "metadata": {}, "output_type": "display_data", "svg": [ - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", "G\n", - "\n", - "option: st\n", - "Inf(\n", - "\u24ff\n", - ")\n", - "cluster_0\n", - "\n", + "\n", + "option: st\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "cluster_0\n", + "\n", "\n", - "cluster_1\n", - "\n", + "cluster_1\n", + "\n", "\n", - "cluster_2\n", - "\n", + "cluster_2\n", + "\n", "\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "!a & !c\n", - "\u24ff\n", + "0->0\n", + "\n", + "\n", + "!a & !c\n", + "\u24ff\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "2\n", + "\n", + "2\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "c\n", + "0->2\n", + "\n", + "\n", + "c\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a & !c\n", + "0->1\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "1\n", - "\u24ff\n", + "2->2\n", + "\n", + "\n", + "1\n", + "\u24ff\n", "\n", "\n", - "3\n", - "\n", - "3\n", + "3\n", + "\n", + "3\n", "\n", "\n", - "3->2\n", - "\n", - "\n", - "!a\n", + "3->2\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "a\n", + "3->3\n", + "\n", + "\n", + "a\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "!a & !c\n", - "\u24ff\n", + "1->0\n", + "\n", + "\n", + "!a & !c\n", + "\u24ff\n", "\n", "\n", - "1->2\n", - "\n", - "\n", - "!a & c\n", + "1->2\n", + "\n", + "\n", + "!a & c\n", "\n", "\n", - "1->3\n", - "\n", - "\n", - "a & c\n", + "1->3\n", + "\n", + "\n", + "a & c\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "a & !c\n", + "1->1\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", - "" + "\n" ], "text": [ - "" + " *' at 0x7f8dcc11a420> >" ] }, { "metadata": {}, "output_type": "display_data", "svg": [ - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", "G\n", - "\n", - "option: wt\n", - "Inf(\n", - "\u24ff\n", - ")\n", - "cluster_0\n", - "\n", + "\n", + "option: wt\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "cluster_0\n", + "\n", "\n", - "cluster_1\n", - "\n", + "cluster_1\n", + "\n", "\n", - "cluster_2\n", - "\n", + "cluster_2\n", + "\n", "\n", - "cluster_3\n", - "\n", + "cluster_3\n", + "\n", "\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "!a & !c\n", + "0->0\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a & b & !c\n", + "0->1\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "3\n", - "\n", - "3\n", + "3\n", + "\n", + "3\n", "\n", "\n", - "0->3\n", - "\n", - "\n", - "c\n", + "0->3\n", + "\n", + "\n", + "c\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "2\n", + "\n", + "2\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "a & !c\n", + "0->2\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "b\n", - "\u24ff\n", + "1->1\n", + "\n", + "\n", + "b\n", + "\u24ff\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "1\n", - "\u24ff\n", + "3->3\n", + "\n", + "\n", + "1\n", + "\u24ff\n", "\n", "\n", - "4\n", - "\n", - "4\n", + "4\n", + "\n", + "4\n", "\n", "\n", - "4->3\n", - "\n", - "\n", - "!a\n", + "4->3\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "4->4\n", - "\n", - "\n", - "a\n", + "4->4\n", + "\n", + "\n", + "a\n", "\n", "\n", - "2->0\n", - "\n", - "\n", - "!a & !c\n", + "2->0\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "2->3\n", - "\n", - "\n", - "!a & c\n", + "2->3\n", + "\n", + "\n", + "!a & c\n", "\n", "\n", - "2->4\n", - "\n", - "\n", - "a & c\n", + "2->4\n", + "\n", + "\n", + "a & c\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "a & !c\n", + "2->2\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", - "" + "\n" ], "text": [ - "" + " *' at 0x7f8dcc11a0f0> >" ] } ], @@ -1048,7 +1100,7 @@ "[0&1] 8\n", "--END--\n", "\"\"\")\n", - "aut.show(\".as\")" + "aut" ], "language": "python", "metadata": {}, @@ -1058,313 +1110,320 @@ "output_type": "pyout", "prompt_number": 8, "svg": [ - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\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", + "(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", + "cluster_1\n", + "\n", "\n", - "cluster_2\n", - "\n", + "cluster_2\n", + "\n", "\n", - "cluster_3\n", - "\n", + "cluster_3\n", + "\n", "\n", - "cluster_4\n", - "\n", + "cluster_4\n", + "\n", "\n", - "cluster_5\n", - "\n", + "cluster_5\n", + "\n", "\n", - "cluster_6\n", - "\n", + "cluster_6\n", + "\n", "\n", "\n", "\n", - "2\n", - "\n", - "2\n", - "\u2777\n", + "2\n", + "\n", + "2\n", + "\u2777\n", "\n", "\n", - "I->2\n", - "\n", - "\n", + "I->2\n", + "\n", + "\n", "\n", "\n", - "6\n", - "\n", - "6\n", - "\u2776\n", - "\u2777\n", + "6\n", + "\n", + "6\n", + "\u2776\n", + "\u2777\n", "\n", "\n", - "2->6\n", - "\n", - "\n", - "c\n", + "2->6\n", + "\n", + "\n", + "c\n", "\n", "\n", - "5\n", - "\n", - "5\n", - "\u2776\n", - "\u2777\n", + "5\n", + "\n", + "5\n", + "\u2776\n", + "\u2777\n", "\n", "\n", - "2->5\n", - "\n", - "\n", - "!a & !c\n", + "2->5\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "3\n", - "\n", - "3\n", - "\u2776\n", - "\u2777\n", + "3\n", + "\n", + "3\n", + "\u2776\n", + "\u2777\n", "\n", "\n", - "2->3\n", - "\n", - "\n", - "a & !b & !c\n", + "2->3\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "4\n", - "\n", - "4\n", - "\u2776\n", - "\u2777\n", + "4\n", + "\n", + "4\n", + "\u2776\n", + "\u2777\n", "\n", "\n", - "2->4\n", - "\n", - "\n", - "a & b & !c\n", + "2->4\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "6->6\n", - "\n", - "\n", - "1\n", + "6->6\n", + "\n", + "\n", + "1\n", "\n", "\n", - "1\n", - "\n", - "1\n", - "\u2777\n", + "1\n", + "\n", + "1\n", + "\u2777\n", "\n", "\n", - "1->6\n", - "\n", - "\n", - "!a\n", + "1->6\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "a\n", + "1->1\n", + "\n", + "\n", + "a\n", "\n", "\n", - "8\n", - "\n", - "8\n", - "\u2778\n", + "8\n", + "\n", + "8\n", + "\u2778\n", "\n", "\n", - "8->6\n", - "\n", - "\n", - "!a\n", + "8->6\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "8->1\n", - "\n", - "\n", - "a & !b\n", + "8->1\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", - "8->8\n", - "\n", - "\n", - "a & b\n", + "8->8\n", + "\n", + "\n", + "a & b\n", "\n", "\n", - "0\n", - "\n", - "0\n", - "\u2777\n", + "0\n", + "\n", + "0\n", + "\u2777\n", "\n", "\n", - "0->6\n", - "\n", - "\n", - "!a & c\n", + "0->6\n", + "\n", + "\n", + "!a & c\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a & c\n", + "0->1\n", + "\n", + "\n", + "a & c\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "a & !c\n", + "0->0\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", - "0->5\n", - "\n", - "\n", - "!a & !c\n", + "0->5\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "5->6\n", - "\n", - "\n", - "c\n", + "5->6\n", + "\n", + "\n", + "c\n", "\n", "\n", - "5->0\n", - "\n", - "\n", - "a & !b & !c\n", + "5->0\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "5->5\n", - "\n", - "\n", - "!a & !c\n", + "5->5\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "7\n", - "\n", - "7\n", - "\u2778\n", + "7\n", + "\n", + "7\n", + "\u2778\n", "\n", "\n", - "5->7\n", - "\n", - "\n", - "a & b & !c\n", + "5->7\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "7->6\n", - "\n", - "\n", - "!a & c\n", + "7->6\n", + "\n", + "\n", + "!a & c\n", "\n", "\n", - "7->1\n", - "\n", - "\n", - "a & !b & c\n", + "7->1\n", + "\n", + "\n", + "a & !b & c\n", "\n", "\n", - "7->8\n", - "\n", - "\n", - "a & b & c\n", + "7->8\n", + "\n", + "\n", + "a & b & c\n", "\n", "\n", - "7->0\n", - "\n", - "\n", - "a & !b & !c\n", + "7->0\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "7->5\n", - "\n", - "\n", - "!a & !c\n", + "7->5\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "7->7\n", - "\n", - "\n", - "a & b & !c\n", + "7->7\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "3->6\n", - "\n", - "\n", - "!a & c\n", + "3->6\n", + "\n", + "\n", + "!a & c\n", "\n", "\n", - "3->1\n", - "\n", - "\n", - "a & c\n", + "3->1\n", + "\n", + "\n", + "a & c\n", "\n", "\n", - "3->0\n", - "\n", - "\n", - "a & !c\n", + "3->0\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", - "3->5\n", - "\n", - "\n", - "!a & !c\n", + "3->5\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "4->6\n", - "\n", - "\n", - "!a & c\n", + "4->6\n", + "\n", + "\n", + "!a & c\n", "\n", "\n", - "4->1\n", - "\n", - "\n", - "a & !b & c\n", + "4->1\n", + "\n", + "\n", + "a & !b & c\n", "\n", "\n", - "4->8\n", - "\n", - "\n", - "a & b & c\n", + "4->8\n", + "\n", + "\n", + "a & b & c\n", "\n", "\n", - "4->0\n", - "\n", - "\n", - "a & !b & !c\n", + "4->0\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "4->5\n", - "\n", - "\n", - "!a & !c\n", + "4->5\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "4->7\n", - "\n", - "\n", - "a & b & !c\n", + "4->7\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "" + "\n" ], "text": [ - "" + " *' at 0x7f8dcf801c60> >" ] } ], @@ -1384,7 +1443,7 @@ "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('.basn'))" + " display(a)" ], "language": "python", "metadata": {}, @@ -1393,659 +1452,680 @@ "metadata": {}, "output_type": "display_data", "svg": [ - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", "G\n", - "\n", - "terminal\n", - "Inf(\n", - "\u24ff\n", - ")\n", - "cluster_0\n", - "\n", + "\n", + "terminal\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "cluster_0\n", + "\n", "\n", - "cluster_1\n", - "\n", + "cluster_1\n", + "\n", "\n", - "cluster_2\n", - "\n", + "cluster_2\n", + "\n", "\n", - "cluster_3\n", - "\n", + "cluster_3\n", + "\n", "\n", - "cluster_4\n", - "\n", + "cluster_4\n", + "\n", "\n", - "cluster_5\n", - "\n", + "cluster_5\n", + "\n", "\n", - "cluster_6\n", - "\n", + "cluster_6\n", + "\n", "\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "4\n", - "\n", - "4\n", - "\u24ff\n", + "4\n", + "\n", + "4\n", + "\u24ff\n", "\n", "\n", - "0->4\n", - "\n", - "\n", - "c\n", + "0->4\n", + "\n", + "\n", + "c\n", "\n", "\n", - "3\n", - "\n", - "3\n", + "3\n", + "\n", + "3\n", "\n", "\n", - "0->3\n", - "\n", - "\n", - "!a & !c\n", + "0->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a & !b & !c\n", + "0->1\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "2\n", + "\n", + "2\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "a & b & !c\n", + "0->2\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "4->4\n", - "\n", - "\n", - "1\n", + "4->4\n", + "\n", + "\n", + "1\n", "\n", "\n", - "7\n", - "\n", - "7\n", + "7\n", + "\n", + "7\n", "\n", "\n", - "7->4\n", - "\n", - "\n", - "!a\n", + "7->4\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "7->7\n", - "\n", - "\n", - "a\n", + "7->7\n", + "\n", + "\n", + "a\n", "\n", "\n", - "8\n", - "\n", - "8\n", + "8\n", + "\n", + "8\n", "\n", "\n", - "8->4\n", - "\n", - "\n", - "!a\n", + "8->4\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "8->7\n", - "\n", - "\n", - "a & !b\n", + "8->7\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", - "8->8\n", - "\n", - "\n", - "a & b\n", + "8->8\n", + "\n", + "\n", + "a & b\n", "\n", "\n", - "5\n", - "\n", - "5\n", + "5\n", + "\n", + "5\n", "\n", "\n", - "5->4\n", - "\n", - "\n", - "!a & c\n", + "5->4\n", + "\n", + "\n", + "!a & c\n", "\n", "\n", - "5->7\n", - "\n", - "\n", - "a & c\n", + "5->7\n", + "\n", + "\n", + "a & c\n", "\n", "\n", - "5->5\n", - "\n", - "\n", - "a & !c\n", + "5->5\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", - "5->3\n", - "\n", - "\n", - "!a & !c\n", + "5->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "3->4\n", - "\n", - "\n", - "c\n", + "3->4\n", + "\n", + "\n", + "c\n", "\n", "\n", - "3->5\n", - "\n", - "\n", - "a & !b & !c\n", + "3->5\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "!a & !c\n", + "3->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "6\n", - "\n", - "6\n", + "6\n", + "\n", + "6\n", "\n", "\n", - "3->6\n", - "\n", - "\n", - "a & b & !c\n", + "3->6\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "6->4\n", - "\n", - "\n", - "!a & c\n", + "6->4\n", + "\n", + "\n", + "!a & c\n", "\n", "\n", - "6->7\n", - "\n", - "\n", - "a & !b & c\n", + "6->7\n", + "\n", + "\n", + "a & !b & c\n", "\n", "\n", - "6->8\n", - "\n", - "\n", - "a & b & c\n", + "6->8\n", + "\n", + "\n", + "a & b & c\n", "\n", "\n", - "6->5\n", - "\n", - "\n", - "a & !b & !c\n", + "6->5\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "6->3\n", - "\n", - "\n", - "!a & !c\n", + "6->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "6->6\n", - "\n", - "\n", - "a & b & !c\n", + "6->6\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "1->4\n", - "\n", - "\n", - "!a & c\n", + "1->4\n", + "\n", + "\n", + "!a & c\n", "\n", "\n", - "1->7\n", - "\n", - "\n", - "a & c\n", + "1->7\n", + "\n", + "\n", + "a & c\n", "\n", "\n", - "1->5\n", - "\n", - "\n", - "a & !c\n", + "1->5\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", - "1->3\n", - "\n", - "\n", - "!a & !c\n", + "1->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "2->4\n", - "\n", - "\n", - "!a & c\n", + "2->4\n", + "\n", + "\n", + "!a & c\n", "\n", "\n", - "2->7\n", - "\n", - "\n", - "a & !b & c\n", + "2->7\n", + "\n", + "\n", + "a & !b & c\n", "\n", "\n", - "2->8\n", - "\n", - "\n", - "a & b & c\n", + "2->8\n", + "\n", + "\n", + "a & b & c\n", "\n", "\n", - "2->5\n", - "\n", - "\n", - "a & !b & !c\n", + "2->5\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "2->3\n", - "\n", - "\n", - "!a & !c\n", + "2->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "2->6\n", - "\n", - "\n", - "a & b & !c\n", + "2->6\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "" + "\n" ], "text": [ - "" + " *' at 0x7f8dcc11a0c0> >" ] }, { "metadata": {}, "output_type": "display_data", "svg": [ - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", "G\n", - "\n", - "strictly weak\n", - "Inf(\n", - "\u24ff\n", - ")\n", - "cluster_0\n", - "\n", + "\n", + "strictly weak\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "cluster_0\n", + "\n", "\n", - "cluster_1\n", - "\n", + "cluster_1\n", + "\n", "\n", - "cluster_2\n", - "\n", + "cluster_2\n", + "\n", "\n", - "cluster_3\n", - "\n", + "cluster_3\n", + "\n", "\n", - "cluster_4\n", - "\n", + "cluster_4\n", + "\n", "\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "3\n", - "\n", - "3\n", + "3\n", + "\n", + "3\n", "\n", "\n", - "0->3\n", - "\n", - "\n", - "!a & !c\n", + "0->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a & !b & !c\n", + "0->1\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "2\n", + "\n", + "2\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "a & b & !c\n", + "0->2\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "6\n", - "\n", - "6\n", - "\u24ff\n", + "6\n", + "\n", + "6\n", + "\u24ff\n", "\n", "\n", - "6->6\n", - "\n", - "\n", - "a & b\n", + "6->6\n", + "\n", + "\n", + "a & b\n", "\n", "\n", - "4\n", - "\n", - "4\n", + "4\n", + "\n", + "4\n", "\n", "\n", - "4->4\n", - "\n", - "\n", - "a & !c\n", + "4->4\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", - "4->3\n", - "\n", - "\n", - "!a & !c\n", + "4->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "3->4\n", - "\n", - "\n", - "a & !b & !c\n", + "3->4\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "!a & !c\n", + "3->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "5\n", - "\n", - "5\n", + "5\n", + "\n", + "5\n", "\n", "\n", - "3->5\n", - "\n", - "\n", - "a & b & !c\n", + "3->5\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "5->6\n", - "\n", - "\n", - "a & b & c\n", + "5->6\n", + "\n", + "\n", + "a & b & c\n", "\n", "\n", - "5->4\n", - "\n", - "\n", - "a & !b & !c\n", + "5->4\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "5->3\n", - "\n", - "\n", - "!a & !c\n", + "5->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "5->5\n", - "\n", - "\n", - "a & b & !c\n", + "5->5\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "1->4\n", - "\n", - "\n", - "a & !c\n", + "1->4\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", - "1->3\n", - "\n", - "\n", - "!a & !c\n", + "1->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "2->6\n", - "\n", - "\n", - "a & b & c\n", + "2->6\n", + "\n", + "\n", + "a & b & c\n", "\n", "\n", - "2->4\n", - "\n", - "\n", - "a & !b & !c\n", + "2->4\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "2->3\n", - "\n", - "\n", - "!a & !c\n", + "2->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "2->5\n", - "\n", - "\n", - "a & b & !c\n", + "2->5\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "" + "\n" ], "text": [ - "" + " *' at 0x7f8dcc11a0f0> >" ] }, { "metadata": {}, "output_type": "display_data", "svg": [ - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\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", + "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", + "cluster_1\n", + "\n", "\n", - "cluster_2\n", - "\n", + "cluster_2\n", + "\n", "\n", - "cluster_3\n", - "\n", + "cluster_3\n", + "\n", "\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "3\n", - "\n", - "3\n", - "\u2776\n", - "\u2777\n", + "3\n", + "\n", + "3\n", + "\u2776\n", + "\u2777\n", "\n", "\n", - "0->3\n", - "\n", - "\n", - "!a & !c\n", + "0->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a & !b & !c\n", + "0->1\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "2\n", + "\n", + "2\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "a & b & !c\n", + "0->2\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "4\n", - "\n", - "4\n", - "\u2777\n", + "4\n", + "\n", + "4\n", + "\u2777\n", "\n", "\n", - "4->4\n", - "\n", - "\n", - "a & !c\n", + "4->4\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", - "4->3\n", - "\n", - "\n", - "!a & !c\n", + "4->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "3->4\n", - "\n", - "\n", - "a & !b & !c\n", + "3->4\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "!a & !c\n", + "3->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "5\n", - "\n", - "5\n", - "\u2778\n", + "5\n", + "\n", + "5\n", + "\u2778\n", "\n", "\n", - "3->5\n", - "\n", - "\n", - "a & b & !c\n", + "3->5\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "5->4\n", - "\n", - "\n", - "a & !b & !c\n", + "5->4\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "5->3\n", - "\n", - "\n", - "!a & !c\n", + "5->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "5->5\n", - "\n", - "\n", - "a & b & !c\n", + "5->5\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "1->4\n", - "\n", - "\n", - "a & !c\n", + "1->4\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", - "1->3\n", - "\n", - "\n", - "!a & !c\n", + "1->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "2->4\n", - "\n", - "\n", - "a & !b & !c\n", + "2->4\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "2->3\n", - "\n", - "\n", - "!a & !c\n", + "2->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "2->5\n", - "\n", - "\n", - "a & b & !c\n", + "2->5\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "" + "\n" ], "text": [ - "" + " *' at 0x7f8dcc11a0c0> >" ] } ], @@ -2064,7 +2144,7 @@ "cell_type": "code", "collapsed": false, "input": [ - "spot.decompose_strength(aut, \"st\").show(\".as\")" + "spot.decompose_strength(aut, \"st\")" ], "language": "python", "metadata": {}, @@ -2074,306 +2154,313 @@ "output_type": "pyout", "prompt_number": 10, "svg": [ - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\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", + "(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", + "cluster_1\n", + "\n", "\n", - "cluster_2\n", - "\n", + "cluster_2\n", + "\n", "\n", - "cluster_3\n", - "\n", + "cluster_3\n", + "\n", "\n", - "cluster_4\n", - "\n", + "cluster_4\n", + "\n", "\n", - "cluster_5\n", - "\n", + "cluster_5\n", + "\n", "\n", - "cluster_6\n", - "\n", + "cluster_6\n", + "\n", "\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "4\n", - "\n", - "4\n", - "\u2776\n", - "\u2777\n", + "4\n", + "\n", + "4\n", + "\u2776\n", + "\u2777\n", "\n", "\n", - "0->4\n", - "\n", - "\n", - "c\n", + "0->4\n", + "\n", + "\n", + "c\n", "\n", "\n", - "3\n", - "\n", - "3\n", - "\u2776\n", - "\u2777\n", + "3\n", + "\n", + "3\n", + "\u2776\n", + "\u2777\n", "\n", "\n", - "0->3\n", - "\n", - "\n", - "!a & !c\n", + "0->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a & !b & !c\n", + "0->1\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "2\n", + "\n", + "2\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "a & b & !c\n", + "0->2\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "4->4\n", - "\n", - "\n", - "1\n", + "4->4\n", + "\n", + "\n", + "1\n", "\n", "\n", - "7\n", - "\n", - "7\n", + "7\n", + "\n", + "7\n", "\n", "\n", - "7->4\n", - "\n", - "\n", - "!a\n", + "7->4\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "7->7\n", - "\n", - "\n", - "a\n", + "7->7\n", + "\n", + "\n", + "a\n", "\n", "\n", - "8\n", - "\n", - "8\n", + "8\n", + "\n", + "8\n", "\n", "\n", - "8->4\n", - "\n", - "\n", - "!a\n", + "8->4\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "8->7\n", - "\n", - "\n", - "a & !b\n", + "8->7\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", - "8->8\n", - "\n", - "\n", - "a & b\n", + "8->8\n", + "\n", + "\n", + "a & b\n", "\n", "\n", - "5\n", - "\n", - "5\n", - "\u2777\n", + "5\n", + "\n", + "5\n", + "\u2777\n", "\n", "\n", - "5->4\n", - "\n", - "\n", - "!a & c\n", + "5->4\n", + "\n", + "\n", + "!a & c\n", "\n", "\n", - "5->7\n", - "\n", - "\n", - "a & c\n", + "5->7\n", + "\n", + "\n", + "a & c\n", "\n", "\n", - "5->5\n", - "\n", - "\n", - "a & !c\n", + "5->5\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", - "5->3\n", - "\n", - "\n", - "!a & !c\n", + "5->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "3->4\n", - "\n", - "\n", - "c\n", + "3->4\n", + "\n", + "\n", + "c\n", "\n", "\n", - "3->5\n", - "\n", - "\n", - "a & !b & !c\n", + "3->5\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "!a & !c\n", + "3->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "6\n", - "\n", - "6\n", - "\u2778\n", + "6\n", + "\n", + "6\n", + "\u2778\n", "\n", "\n", - "3->6\n", - "\n", - "\n", - "a & b & !c\n", + "3->6\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "6->4\n", - "\n", - "\n", - "!a & c\n", + "6->4\n", + "\n", + "\n", + "!a & c\n", "\n", "\n", - "6->7\n", - "\n", - "\n", - "a & !b & c\n", + "6->7\n", + "\n", + "\n", + "a & !b & c\n", "\n", "\n", - "6->8\n", - "\n", - "\n", - "a & b & c\n", + "6->8\n", + "\n", + "\n", + "a & b & c\n", "\n", "\n", - "6->5\n", - "\n", - "\n", - "a & !b & !c\n", + "6->5\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "6->3\n", - "\n", - "\n", - "!a & !c\n", + "6->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "6->6\n", - "\n", - "\n", - "a & b & !c\n", + "6->6\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "1->4\n", - "\n", - "\n", - "!a & c\n", + "1->4\n", + "\n", + "\n", + "!a & c\n", "\n", "\n", - "1->7\n", - "\n", - "\n", - "a & c\n", + "1->7\n", + "\n", + "\n", + "a & c\n", "\n", "\n", - "1->5\n", - "\n", - "\n", - "a & !c\n", + "1->5\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", - "1->3\n", - "\n", - "\n", - "!a & !c\n", + "1->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "2->4\n", - "\n", - "\n", - "!a & c\n", + "2->4\n", + "\n", + "\n", + "!a & c\n", "\n", "\n", - "2->7\n", - "\n", - "\n", - "a & !b & c\n", + "2->7\n", + "\n", + "\n", + "a & !b & c\n", "\n", "\n", - "2->8\n", - "\n", - "\n", - "a & b & c\n", + "2->8\n", + "\n", + "\n", + "a & b & c\n", "\n", "\n", - "2->5\n", - "\n", - "\n", - "a & !b & !c\n", + "2->5\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "2->3\n", - "\n", - "\n", - "!a & !c\n", + "2->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "2->6\n", - "\n", - "\n", - "a & b & !c\n", + "2->6\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "" + "\n" ], "text": [ - "" + " *' at 0x7f8dcc11ac00> >" ] } ], @@ -2393,7 +2480,7 @@ "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('.basn'))" + " display(a)" ], "language": "python", "metadata": {}, @@ -2402,400 +2489,421 @@ "metadata": {}, "output_type": "display_data", "svg": [ - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", "G\n", - "\n", - "terminal\n", - "Inf(\n", - "\u24ff\n", - ")\n", - "cluster_0\n", - "\n", + "\n", + "terminal\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "cluster_0\n", + "\n", "\n", - "cluster_1\n", - "\n", + "cluster_1\n", + "\n", "\n", - "cluster_2\n", - "\n", + "cluster_2\n", + "\n", "\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "2\n", + "\n", + "2\n", "\n", "\n", - "I->2\n", - "\n", - "\n", + "I->2\n", + "\n", + "\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "!a & !c\n", + "2->2\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "0\n", - "\n", - "0\n", - "\u24ff\n", + "0\n", + "\n", + "0\n", + "\u24ff\n", "\n", "\n", - "2->0\n", - "\n", - "\n", - "c\n", + "2->0\n", + "\n", + "\n", + "c\n", "\n", "\n", - "3\n", - "\n", - "3\n", + "3\n", + "\n", + "3\n", "\n", "\n", - "2->3\n", - "\n", - "\n", - "a & !c\n", + "2->3\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "1\n", + "0->0\n", + "\n", + "\n", + "1\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "!a\n", + "1->0\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "a\n", + "1->1\n", + "\n", + "\n", + "a\n", "\n", "\n", - "3->2\n", - "\n", - "\n", - "!a & !c\n", + "3->2\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "3->0\n", - "\n", - "\n", - "!a & c\n", + "3->0\n", + "\n", + "\n", + "!a & c\n", "\n", "\n", - "3->1\n", - "\n", - "\n", - "a & c\n", + "3->1\n", + "\n", + "\n", + "a & c\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "a & !c\n", + "3->3\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", - "" + "\n" ], "text": [ - "" + " *' at 0x7f8dcc11af90> >" ] }, { "metadata": {}, "output_type": "display_data", "svg": [ - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", "G\n", - "\n", - "strictly weak\n", - "Inf(\n", - "\u24ff\n", - ")\n", - "cluster_0\n", - "\n", + "\n", + "strictly weak\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "cluster_0\n", + "\n", "\n", - "cluster_1\n", - "\n", + "cluster_1\n", + "\n", "\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "2\n", + "\n", + "2\n", "\n", "\n", - "I->2\n", - "\n", - "\n", + "I->2\n", + "\n", + "\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "!a & !c\n", + "2->2\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "2->1\n", - "\n", - "\n", - "a & !b & !c\n", + "2->1\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "3\n", - "\n", - "3\n", + "3\n", + "\n", + "3\n", "\n", "\n", - "2->3\n", - "\n", - "\n", - "a & b & !c\n", + "2->3\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "0\n", - "\n", - "0\n", - "\u24ff\n", + "0\n", + "\n", + "0\n", + "\u24ff\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "a & b\n", + "0->0\n", + "\n", + "\n", + "a & b\n", "\n", "\n", - "1->2\n", - "\n", - "\n", - "!a & !c\n", + "1->2\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "a & !c\n", + "1->1\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", - "3->2\n", - "\n", - "\n", - "!a & !c\n", + "3->2\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "3->0\n", - "\n", - "\n", - "a & b & c\n", + "3->0\n", + "\n", + "\n", + "a & b & c\n", "\n", "\n", - "3->1\n", - "\n", - "\n", - "a & !b & !c\n", + "3->1\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "a & b & !c\n", + "3->3\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "" + "\n" ], "text": [ - "" + " *' at 0x7f8dcc11acf0> >" ] }, { "metadata": {}, "output_type": "display_data", "svg": [ - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\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", + "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", + "cluster_1\n", + "\n", "\n", - "cluster_2\n", - "\n", + "cluster_2\n", + "\n", "\n", - "cluster_3\n", - "\n", + "cluster_3\n", + "\n", "\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "3\n", - "\n", - "3\n", - "\u2776\n", - "\u2777\n", + "3\n", + "\n", + "3\n", + "\u2776\n", + "\u2777\n", "\n", "\n", - "0->3\n", - "\n", - "\n", - "!a & !c\n", + "0->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a & !b & !c\n", + "0->1\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "2\n", + "\n", + "2\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "a & b & !c\n", + "0->2\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "!a & !c\n", + "3->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "4\n", - "\n", - "4\n", - "\u2777\n", + "4\n", + "\n", + "4\n", + "\u2777\n", "\n", "\n", - "3->4\n", - "\n", - "\n", - "a & !b & !c\n", + "3->4\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "5\n", - "\n", - "5\n", - "\u2778\n", + "5\n", + "\n", + "5\n", + "\u2778\n", "\n", "\n", - "3->5\n", - "\n", - "\n", - "a & b & !c\n", + "3->5\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "4->3\n", - "\n", - "\n", - "!a & !c\n", + "4->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "4->4\n", - "\n", - "\n", - "a & !c\n", + "4->4\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", - "5->3\n", - "\n", - "\n", - "!a & !c\n", + "5->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "5->4\n", - "\n", - "\n", - "a & !b & !c\n", + "5->4\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "5->5\n", - "\n", - "\n", - "a & b & !c\n", + "5->5\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "1->3\n", - "\n", - "\n", - "!a & !c\n", + "1->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "1->4\n", - "\n", - "\n", - "a & !c\n", + "1->4\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", - "2->3\n", - "\n", - "\n", - "!a & !c\n", + "2->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "2->4\n", - "\n", - "\n", - "a & !b & !c\n", + "2->4\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "2->5\n", - "\n", - "\n", - "a & b & !c\n", + "2->5\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "" + "\n" ], "text": [ - "" + " *' at 0x7f8dcc11a450> >" ] } ], @@ -2867,7 +2975,7 @@ "[!0&!2] 7\n", "--END--\n", "\"\"\")\n", - "aut.show(\".as\")" + "aut" ], "language": "python", "metadata": {}, @@ -2877,275 +2985,282 @@ "output_type": "pyout", "prompt_number": 12, "svg": [ - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\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", + "(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", + "cluster_1\n", + "\n", "\n", - "cluster_2\n", - "\n", + "cluster_2\n", + "\n", "\n", - "cluster_3\n", - "\n", + "cluster_3\n", + "\n", "\n", - "cluster_4\n", - "\n", + "cluster_4\n", + "\n", "\n", "\n", "\n", - "7\n", - "\n", - "7\n", - "\u2778\n", + "7\n", + "\n", + "7\n", + "\u2778\n", "\n", "\n", - "I->7\n", - "\n", - "\n", + "I->7\n", + "\n", + "\n", "\n", "\n", - "7->7\n", - "\n", - "\n", - "!a & !c\n", + "7->7\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "4\n", - "\n", - "4\n", - "\u2776\n", - "\u2778\n", + "4\n", + "\n", + "4\n", + "\u2776\n", + "\u2778\n", "\n", "\n", - "7->4\n", - "\n", - "\n", - "c\n", + "7->4\n", + "\n", + "\n", + "c\n", "\n", "\n", - "2\n", - "\n", - "2\n", - "\u2777\n", + "2\n", + "\n", + "2\n", + "\u2777\n", "\n", "\n", - "7->2\n", - "\n", - "\n", - "a & !b & !c\n", + "7->2\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "6\n", - "\n", - "6\n", - "\u2778\n", + "6\n", + "\n", + "6\n", + "\u2778\n", "\n", "\n", - "7->6\n", - "\n", - "\n", - "a & b & !c\n", + "7->6\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "4->4\n", - "\n", - "\n", - "1\n", + "4->4\n", + "\n", + "\n", + "1\n", "\n", "\n", - "3\n", - "\n", - "3\n", - "\u24ff\n", - "\u2778\n", + "3\n", + "\n", + "3\n", + "\u24ff\n", + "\u2778\n", "\n", "\n", - "3->4\n", - "\n", - "\n", - "!a\n", + "3->4\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "a\n", + "3->3\n", + "\n", + "\n", + "a\n", "\n", "\n", - "0\n", - "\n", - "0\n", - "\u2777\n", + "0\n", + "\n", + "0\n", + "\u2777\n", "\n", "\n", - "0->4\n", - "\n", - "\n", - "!a\n", + "0->4\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "0->3\n", - "\n", - "\n", - "a & !b\n", + "0->3\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "a & b\n", + "0->0\n", + "\n", + "\n", + "a & b\n", "\n", "\n", - "5\n", - "\n", - "5\n", - "\u2778\n", + "5\n", + "\n", + "5\n", + "\u2778\n", "\n", "\n", - "5->4\n", - "\n", - "\n", - "!a\n", + "5->4\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "5->3\n", - "\n", - "\n", - "a & !b\n", + "5->3\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", - "5->5\n", - "\n", - "\n", - "a & b\n", + "5->5\n", + "\n", + "\n", + "a & b\n", "\n", "\n", - "2->7\n", - "\n", - "\n", - "!a & !c\n", + "2->7\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "2->4\n", - "\n", - "\n", - "!a & c\n", + "2->4\n", + "\n", + "\n", + "!a & c\n", "\n", "\n", - "2->3\n", - "\n", - "\n", - "a & c\n", + "2->3\n", + "\n", + "\n", + "a & c\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "a & !b & !c\n", + "2->2\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "1\n", - "\n", - "1\n", - "\u2777\n", + "1\n", + "\n", + "1\n", + "\u2777\n", "\n", "\n", - "2->1\n", - "\n", - "\n", - "a & b & !c\n", + "2->1\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "1->7\n", - "\n", - "\n", - "!a & !c\n", + "1->7\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "1->4\n", - "\n", - "\n", - "!a & c\n", + "1->4\n", + "\n", + "\n", + "!a & c\n", "\n", "\n", - "1->3\n", - "\n", - "\n", - "a & !b & c\n", + "1->3\n", + "\n", + "\n", + "a & !b & c\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "a & b & c\n", + "1->0\n", + "\n", + "\n", + "a & b & c\n", "\n", "\n", - "1->2\n", - "\n", - "\n", - "a & !b & !c\n", + "1->2\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "a & b & !c\n", + "1->1\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "6->7\n", - "\n", - "\n", - "!a & !c\n", + "6->7\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "6->4\n", - "\n", - "\n", - "!a & c\n", + "6->4\n", + "\n", + "\n", + "!a & c\n", "\n", "\n", - "6->3\n", - "\n", - "\n", - "a & !b & c\n", + "6->3\n", + "\n", + "\n", + "a & !b & c\n", "\n", "\n", - "6->5\n", - "\n", - "\n", - "a & b & c\n", + "6->5\n", + "\n", + "\n", + "a & b & c\n", "\n", "\n", - "6->2\n", - "\n", - "\n", - "a & !b & !c\n", + "6->2\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "6->6\n", - "\n", - "\n", - "a & b & !c\n", + "6->6\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "" + "\n" ], "text": [ - "" + " *' at 0x7f8dcc0c2120> >" ] } ], @@ -3158,7 +3273,7 @@ "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('.basn'))" + " display(a)" ], "language": "python", "metadata": {}, @@ -3167,543 +3282,564 @@ "metadata": {}, "output_type": "display_data", "svg": [ - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", "G\n", - "\n", - "terminal\n", - "Inf(\n", - "\u24ff\n", - ")\n", - "cluster_0\n", - "\n", + "\n", + "terminal\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "cluster_0\n", + "\n", "\n", - "cluster_1\n", - "\n", + "cluster_1\n", + "\n", "\n", - "cluster_2\n", - "\n", + "cluster_2\n", + "\n", "\n", - "cluster_3\n", - "\n", + "cluster_3\n", + "\n", "\n", - "cluster_4\n", - "\n", + "cluster_4\n", + "\n", "\n", "\n", "\n", - "0\n", - "\n", - "0\n", - "\u2777\n", + "0\n", + "\n", + "0\n", + "\u2777\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "!a & !c\n", + "0->0\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "2\n", - "\n", - "2\n", - "\u24ff\n", + "2\n", + "\n", + "2\n", + "\u24ff\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "c\n", + "0->2\n", + "\n", + "\n", + "c\n", "\n", "\n", - "1\n", - "\n", - "1\n", - "\u2777\n", + "1\n", + "\n", + "1\n", + "\u2777\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a & !b & !c\n", + "0->1\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "3\n", - "\n", - "3\n", - "\u2777\n", + "3\n", + "\n", + "3\n", + "\u2777\n", "\n", "\n", - "0->3\n", - "\n", - "\n", - "a & b & !c\n", + "0->3\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "1\n", + "2->2\n", + "\n", + "\n", + "1\n", "\n", "\n", - "4\n", - "\n", - "4\n", - "\u2777\n", + "4\n", + "\n", + "4\n", + "\u2777\n", "\n", "\n", - "4->2\n", - "\n", - "\n", - "!a\n", + "4->2\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "4->4\n", - "\n", - "\n", - "a\n", + "4->4\n", + "\n", + "\n", + "a\n", "\n", "\n", - "7\n", - "\n", - "7\n", - "\u2777\n", + "7\n", + "\n", + "7\n", + "\u2777\n", "\n", "\n", - "7->2\n", - "\n", - "\n", - "!a\n", + "7->2\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "7->4\n", - "\n", - "\n", - "a & !b\n", + "7->4\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", - "7->7\n", - "\n", - "\n", - "a & b\n", + "7->7\n", + "\n", + "\n", + "a & b\n", "\n", "\n", - "5\n", - "\n", - "5\n", - "\u2777\n", + "5\n", + "\n", + "5\n", + "\u2777\n", "\n", "\n", - "5->2\n", - "\n", - "\n", - "!a\n", + "5->2\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "5->4\n", - "\n", - "\n", - "a & !b\n", + "5->4\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", - "5->5\n", - "\n", - "\n", - "a & b\n", + "5->5\n", + "\n", + "\n", + "a & b\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "!a & !c\n", + "1->0\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "1->2\n", - "\n", - "\n", - "!a & c\n", + "1->2\n", + "\n", + "\n", + "!a & c\n", "\n", "\n", - "1->4\n", - "\n", - "\n", - "a & c\n", + "1->4\n", + "\n", + "\n", + "a & c\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "a & !b & !c\n", + "1->1\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "6\n", - "\n", - "6\n", - "\u2777\n", + "6\n", + "\n", + "6\n", + "\u2777\n", "\n", "\n", - "1->6\n", - "\n", - "\n", - "a & b & !c\n", + "1->6\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "6->0\n", - "\n", - "\n", - "!a & !c\n", + "6->0\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "6->2\n", - "\n", - "\n", - "!a & c\n", + "6->2\n", + "\n", + "\n", + "!a & c\n", "\n", "\n", - "6->4\n", - "\n", - "\n", - "a & !b & c\n", + "6->4\n", + "\n", + "\n", + "a & !b & c\n", "\n", "\n", - "6->7\n", - "\n", - "\n", - "a & b & c\n", + "6->7\n", + "\n", + "\n", + "a & b & c\n", "\n", "\n", - "6->1\n", - "\n", - "\n", - "a & !b & !c\n", + "6->1\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "6->6\n", - "\n", - "\n", - "a & b & !c\n", + "6->6\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "3->0\n", - "\n", - "\n", - "!a & !c\n", + "3->0\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "3->2\n", - "\n", - "\n", - "!a & c\n", + "3->2\n", + "\n", + "\n", + "!a & c\n", "\n", "\n", - "3->4\n", - "\n", - "\n", - "a & !b & c\n", + "3->4\n", + "\n", + "\n", + "a & !b & c\n", "\n", "\n", - "3->5\n", - "\n", - "\n", - "a & b & c\n", + "3->5\n", + "\n", + "\n", + "a & b & c\n", "\n", "\n", - "3->1\n", - "\n", - "\n", - "a & !b & !c\n", + "3->1\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "a & b & !c\n", + "3->3\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "" + "\n" ], "text": [ - "" + " *' at 0x7f8dcc0c20c0> >" ] }, { "metadata": {}, "output_type": "display_data", "svg": [ - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", "G\n", - "\n", - "strictly weak\n", - "Inf(\n", - "\u24ff\n", - ")\n", - "cluster_0\n", - "\n", + "\n", + "strictly weak\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "cluster_0\n", + "\n", "\n", - "cluster_1\n", - "\n", + "cluster_1\n", + "\n", "\n", "\n", "\n", - "0\n", - "\n", - "0\n", - "\u2777\n", + "0\n", + "\n", + "0\n", + "\u2777\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "!a & !c\n", + "0->0\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "1\n", - "\n", - "1\n", - "\u2777\n", + "1\n", + "\n", + "1\n", + "\u2777\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a & !b & !c\n", + "0->1\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "2\n", - "\n", - "2\n", - "\u2777\n", + "2\n", + "\n", + "2\n", + "\u2777\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "a & b & !c\n", + "0->2\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "3\n", - "\n", - "3\n", - "\u24ff\n", + "3\n", + "\n", + "3\n", + "\u24ff\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "a & b\n", + "3->3\n", + "\n", + "\n", + "a & b\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "!a & !c\n", + "1->0\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "a & !b & !c\n", + "1->1\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "4\n", - "\n", - "4\n", - "\u2777\n", + "4\n", + "\n", + "4\n", + "\u2777\n", "\n", "\n", - "1->4\n", - "\n", - "\n", - "a & b & !c\n", + "1->4\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "4->0\n", - "\n", - "\n", - "!a & !c\n", + "4->0\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "4->1\n", - "\n", - "\n", - "a & !b & !c\n", + "4->1\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "4->4\n", - "\n", - "\n", - "a & b & !c\n", + "4->4\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "2->0\n", - "\n", - "\n", - "!a & !c\n", + "2->0\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "2->3\n", - "\n", - "\n", - "a & b & c\n", + "2->3\n", + "\n", + "\n", + "a & b & c\n", "\n", "\n", - "2->1\n", - "\n", - "\n", - "a & !b & !c\n", + "2->1\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "a & b & !c\n", + "2->2\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "" + "\n" ], "text": [ - "" + " *' at 0x7f8dcc11a450> >" ] }, { "metadata": {}, "output_type": "display_data", "svg": [ - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\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", + "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", + "0\n", + "\n", + "0\n", + "\u2778\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "!a & !c\n", + "0->0\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "1\n", - "\n", - "1\n", - "\u2777\n", + "1\n", + "\n", + "1\n", + "\u2777\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a & !b & !c\n", + "0->1\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "2\n", - "\n", - "2\n", - "\u2778\n", + "2\n", + "\n", + "2\n", + "\u2778\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "a & b & !c\n", + "0->2\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "!a & !c\n", + "1->0\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "a & !b & !c\n", + "1->1\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "3\n", - "\n", - "3\n", - "\u2777\n", + "3\n", + "\n", + "3\n", + "\u2777\n", "\n", "\n", - "1->3\n", - "\n", - "\n", - "a & b & !c\n", + "1->3\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "3->0\n", - "\n", - "\n", - "!a & !c\n", + "3->0\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "3->1\n", - "\n", - "\n", - "a & !b & !c\n", + "3->1\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "a & b & !c\n", + "3->3\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "2->0\n", - "\n", - "\n", - "!a & !c\n", + "2->0\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "2->1\n", - "\n", - "\n", - "a & !b & !c\n", + "2->1\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "a & b & !c\n", + "2->2\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "" + "\n" ], "text": [ - "" + " *' at 0x7f8dcc0c20c0> >" ] } ], @@ -3722,7 +3858,7 @@ "cell_type": "code", "collapsed": false, "input": [ - "spot.decompose_strength(aut, 'st').show('.as')" + "spot.decompose_strength(aut, 'st')" ], "language": "python", "metadata": {}, @@ -3732,274 +3868,281 @@ "output_type": "pyout", "prompt_number": 14, "svg": [ - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\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", + "(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", + "cluster_1\n", + "\n", "\n", - "cluster_2\n", - "\n", + "cluster_2\n", + "\n", "\n", - "cluster_3\n", - "\n", + "cluster_3\n", + "\n", "\n", - "cluster_4\n", - "\n", + "cluster_4\n", + "\n", "\n", "\n", "\n", - "0\n", - "\n", - "0\n", - "\u2778\n", + "0\n", + "\n", + "0\n", + "\u2778\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "!a & !c\n", + "0->0\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "2\n", - "\n", - "2\n", - "\u2776\n", - "\u2778\n", + "2\n", + "\n", + "2\n", + "\u2776\n", + "\u2778\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "c\n", + "0->2\n", + "\n", + "\n", + "c\n", "\n", "\n", - "1\n", - "\n", - "1\n", - "\u2777\n", + "1\n", + "\n", + "1\n", + "\u2777\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a & !b & !c\n", + "0->1\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "3\n", - "\n", - "3\n", - "\u2778\n", + "3\n", + "\n", + "3\n", + "\u2778\n", "\n", "\n", - "0->3\n", - "\n", - "\n", - "a & b & !c\n", + "0->3\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "1\n", + "2->2\n", + "\n", + "\n", + "1\n", "\n", "\n", - "4\n", - "\n", - "4\n", - "\u2777\n", + "4\n", + "\n", + "4\n", + "\u2777\n", "\n", "\n", - "4->2\n", - "\n", - "\n", - "!a\n", + "4->2\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "4->4\n", - "\n", - "\n", - "a\n", + "4->4\n", + "\n", + "\n", + "a\n", "\n", "\n", - "7\n", - "\n", - "7\n", - "\u2777\n", + "7\n", + "\n", + "7\n", + "\u2777\n", "\n", "\n", - "7->2\n", - "\n", - "\n", - "!a\n", + "7->2\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "7->4\n", - "\n", - "\n", - "a & !b\n", + "7->4\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", - "7->7\n", - "\n", - "\n", - "a & b\n", + "7->7\n", + "\n", + "\n", + "a & b\n", "\n", "\n", - "5\n", - "\n", - "5\n", - "\u2777\n", + "5\n", + "\n", + "5\n", + "\u2777\n", "\n", "\n", - "5->2\n", - "\n", - "\n", - "!a\n", + "5->2\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "5->4\n", - "\n", - "\n", - "a & !b\n", + "5->4\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", - "5->5\n", - "\n", - "\n", - "a & b\n", + "5->5\n", + "\n", + "\n", + "a & b\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "!a & !c\n", + "1->0\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "1->2\n", - "\n", - "\n", - "!a & c\n", + "1->2\n", + "\n", + "\n", + "!a & c\n", "\n", "\n", - "1->4\n", - "\n", - "\n", - "a & c\n", + "1->4\n", + "\n", + "\n", + "a & c\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "a & !b & !c\n", + "1->1\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "6\n", - "\n", - "6\n", - "\u2777\n", + "6\n", + "\n", + "6\n", + "\u2777\n", "\n", "\n", - "1->6\n", - "\n", - "\n", - "a & b & !c\n", + "1->6\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "6->0\n", - "\n", - "\n", - "!a & !c\n", + "6->0\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "6->2\n", - "\n", - "\n", - "!a & c\n", + "6->2\n", + "\n", + "\n", + "!a & c\n", "\n", "\n", - "6->4\n", - "\n", - "\n", - "a & !b & c\n", + "6->4\n", + "\n", + "\n", + "a & !b & c\n", "\n", "\n", - "6->7\n", - "\n", - "\n", - "a & b & c\n", + "6->7\n", + "\n", + "\n", + "a & b & c\n", "\n", "\n", - "6->1\n", - "\n", - "\n", - "a & !b & !c\n", + "6->1\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "6->6\n", - "\n", - "\n", - "a & b & !c\n", + "6->6\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "3->0\n", - "\n", - "\n", - "!a & !c\n", + "3->0\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "3->2\n", - "\n", - "\n", - "!a & c\n", + "3->2\n", + "\n", + "\n", + "!a & c\n", "\n", "\n", - "3->4\n", - "\n", - "\n", - "a & !b & c\n", + "3->4\n", + "\n", + "\n", + "a & !b & c\n", "\n", "\n", - "3->5\n", - "\n", - "\n", - "a & b & c\n", + "3->5\n", + "\n", + "\n", + "a & b & c\n", "\n", "\n", - "3->1\n", - "\n", - "\n", - "a & !b & !c\n", + "3->1\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "a & b & !c\n", + "3->3\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "" + "\n" ], "text": [ - "" + " *' at 0x7f8dcc0c2210> >" ] } ], @@ -4026,7 +4169,7 @@ "cell_type": "code", "collapsed": false, "input": [ - "aut = spot.translate('(Gb|c) R a', 'any'); aut.show('.as')" + "aut = spot.translate('(Gb|c) R a', 'any'); aut" ], "language": "python", "metadata": {}, @@ -4036,76 +4179,83 @@ "output_type": "pyout", "prompt_number": 15, "svg": [ - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", "G\n", - "\n", - "t\n", - "cluster_0\n", - "\n", + "\n", + "t\n", + "cluster_0\n", + "\n", "\n", - "cluster_1\n", - "\n", + "cluster_1\n", + "\n", "\n", - "cluster_2\n", - "\n", + "cluster_2\n", + "\n", "\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "a & !c\n", + "0->0\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a & c\n", + "0->1\n", + "\n", + "\n", + "a & c\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "2\n", + "\n", + "2\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "a & b & !c\n", + "0->2\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "1\n", + "1->1\n", + "\n", + "\n", + "1\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "b\n", + "2->2\n", + "\n", + "\n", + "b\n", "\n", "\n", - "" + "\n" ], "text": [ - "" + " *' at 0x7f8dcc0c2390> >" ] } ], @@ -4128,7 +4278,7 @@ "collapsed": false, "input": [ "for opt in ('w', 't'):\n", - " display(spot.decompose_strength(aut, opt).show('.bas'))" + " display(spot.decompose_strength(aut, opt))" ], "language": "python", "metadata": {}, @@ -4137,119 +4287,133 @@ "metadata": {}, "output_type": "display_data", "svg": [ - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", "G\n", - "\n", - "Inf(\n", - "\u24ff\n", - ")\n", - "cluster_0\n", - "\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "cluster_0\n", + "\n", "\n", - "cluster_1\n", - "\n", + "cluster_1\n", + "\n", "\n", "\n", "\n", - "0\n", - "\n", - "0\n", - "\u24ff\n", + "0\n", + "\n", + "0\n", + "\u24ff\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "a & !c\n", + "0->0\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", - "1\n", - "\n", - "1\n", - "\u24ff\n", + "1\n", + "\n", + "1\n", + "\u24ff\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a & b & !c\n", + "0->1\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "b\n", + "1->1\n", + "\n", + "\n", + "b\n", "\n", "\n", - "" + "\n" ], "text": [ - "" + " *' at 0x7f8dcc0c23f0> >" ] }, { "metadata": {}, "output_type": "display_data", "svg": [ - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", "G\n", - "\n", - "Inf(\n", - "\u24ff\n", - ")\n", - "cluster_0\n", - "\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "cluster_0\n", + "\n", "\n", - "cluster_1\n", - "\n", + "cluster_1\n", + "\n", "\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "a & !c\n", + "0->0\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", - "1\n", - "\n", - "1\n", - "\u24ff\n", + "1\n", + "\n", + "1\n", + "\u24ff\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a & c\n", + "0->1\n", + "\n", + "\n", + "a & c\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "1\n", + "1->1\n", + "\n", + "\n", + "1\n", "\n", "\n", - "" + "\n" ], "text": [ - "" + " *' at 0x7f8dcc0c23f0> >" ] } ], @@ -4266,7 +4430,7 @@ "cell_type": "code", "collapsed": false, "input": [ - "spot.decompose_strength(aut, 'st').show('.bas')" + "spot.decompose_strength(aut, 'st')" ], "language": "python", "metadata": {}, @@ -4276,59 +4440,66 @@ "output_type": "pyout", "prompt_number": 18, "svg": [ - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", "G\n", - "\n", - "Inf(\n", - "\u24ff\n", - ")\n", - "cluster_0\n", - "\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "cluster_0\n", + "\n", "\n", - "cluster_1\n", - "\n", + "cluster_1\n", + "\n", "\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "a & !c\n", + "0->0\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", - "1\n", - "\n", - "1\n", - "\u24ff\n", + "1\n", + "\n", + "1\n", + "\u24ff\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a & c\n", + "0->1\n", + "\n", + "\n", + "a & c\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "1\n", + "1->1\n", + "\n", + "\n", + "1\n", "\n", "\n", - "" + "\n" ], "text": [ - "" + " *' at 0x7f8dcc0c2450> >" ] } ], @@ -4374,7 +4545,7 @@ "[t] 3 {0}\n", "--END--\n", "\"\"\")\n", - "aut.show('.as')" + "aut" ], "language": "python", "metadata": {}, @@ -4384,99 +4555,106 @@ "output_type": "pyout", "prompt_number": 19, "svg": [ - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", "G\n", - "\n", - "Inf(\n", - "\u24ff\n", - ") | Fin(\n", - "\u24ff\n", - ")\n", - "cluster_0\n", - "\n", + "\n", + "Inf(\n", + "\u24ff\n", + ") | Fin(\n", + "\u24ff\n", + ")\n", + "cluster_0\n", + "\n", "\n", - "cluster_1\n", - "\n", + "cluster_1\n", + "\n", "\n", - "cluster_2\n", - "\n", + "cluster_2\n", + "\n", "\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "a\n", + "0->0\n", + "\n", + "\n", + "a\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "!a\n", + "0->1\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "3\n", - "\n", - "3\n", + "3\n", + "\n", + "3\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "1\n", - "\u24ff\n", + "3->3\n", + "\n", + "\n", + "1\n", + "\u24ff\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "a\n", + "1->1\n", + "\n", + "\n", + "a\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "2\n", + "\n", + "2\n", "\n", "\n", - "1->2\n", - "\n", - "\n", - "!a\n", - "\u24ff\n", + "1->2\n", + "\n", + "\n", + "!a\n", + "\u24ff\n", "\n", "\n", - "2->3\n", - "\n", - "\n", - "!a\n", + "2->3\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "2->1\n", - "\n", - "\n", - "a\n", + "2->1\n", + "\n", + "\n", + "a\n", "\n", "\n", - "" + "\n" ], "text": [ - "" + " *' at 0x7f8dcc0c24e0> >" ] } ], @@ -4500,7 +4678,7 @@ " a = spot.decompose_strength(aut, opt)\n", " if a:\n", " a.set_name(name)\n", - " display(a.show('.asn'))\n", + " display(a)\n", " else:\n", " print(\"no output for \" + name)" ], @@ -4511,178 +4689,192 @@ "metadata": {}, "output_type": "display_data", "svg": [ - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", "G\n", - "\n", - "terminal\n", - "Inf(\n", - "\u24ff\n", - ")\n", - "cluster_0\n", - "\n", + "\n", + "terminal\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "cluster_0\n", + "\n", "\n", - "cluster_1\n", - "\n", + "cluster_1\n", + "\n", "\n", - "cluster_2\n", - "\n", + "cluster_2\n", + "\n", "\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "a\n", + "0->0\n", + "\n", + "\n", + "a\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "!a\n", + "0->1\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "3\n", - "\n", - "3\n", + "3\n", + "\n", + "3\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "1\n", - "\u24ff\n", + "3->3\n", + "\n", + "\n", + "1\n", + "\u24ff\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "a\n", + "1->1\n", + "\n", + "\n", + "a\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "2\n", + "\n", + "2\n", "\n", "\n", - "1->2\n", - "\n", - "\n", - "!a\n", + "1->2\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "2->3\n", - "\n", - "\n", - "!a\n", + "2->3\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "2->1\n", - "\n", - "\n", - "a\n", + "2->1\n", + "\n", + "\n", + "a\n", "\n", "\n", - "" + "\n" ], "text": [ - "" + " *' at 0x7f8dcc0c2d50> >" ] }, { "metadata": {}, "output_type": "display_data", "svg": [ - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", "G\n", - "\n", - "strictly weak\n", - "Inf(\n", - "\u24ff\n", - ")\n", - "cluster_0\n", - "\n", + "\n", + "strictly weak\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "cluster_0\n", + "\n", "\n", - "cluster_1\n", - "\n", + "cluster_1\n", + "\n", "\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "a\n", - "\u24ff\n", + "0->0\n", + "\n", + "\n", + "a\n", + "\u24ff\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "!a\n", - "\u24ff\n", + "0->1\n", + "\n", + "\n", + "!a\n", + "\u24ff\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "a\n", - "\u24ff\n", + "1->1\n", + "\n", + "\n", + "a\n", + "\u24ff\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "2\n", + "\n", + "2\n", "\n", "\n", - "1->2\n", - "\n", - "\n", - "!a\n", - "\u24ff\n", + "1->2\n", + "\n", + "\n", + "!a\n", + "\u24ff\n", "\n", "\n", - "2->1\n", - "\n", - "\n", - "a\n", - "\u24ff\n", + "2->1\n", + "\n", + "\n", + "a\n", + "\u24ff\n", "\n", "\n", - "" + "\n" ], "text": [ - "" + " *' at 0x7f8dcc11a450> >" ] }, { @@ -4696,107 +4888,123 @@ "metadata": {}, "output_type": "display_data", "svg": [ - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", "G\n", - "\n", - "all strengths\n", - "Inf(\n", - "\u24ff\n", - ")\n", - "cluster_0\n", - "\n", + "\n", + "all strengths\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "cluster_0\n", + "\n", "\n", - "cluster_1\n", - "\n", + "cluster_1\n", + "\n", "\n", - "cluster_2\n", - "\n", + "cluster_2\n", + "\n", "\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "a\n", - "\u24ff\n", + "0->0\n", + "\n", + "\n", + "a\n", + "\u24ff\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "!a\n", - "\u24ff\n", + "0->1\n", + "\n", + "\n", + "!a\n", + "\u24ff\n", "\n", "\n", - "3\n", - "\n", - "3\n", + "3\n", + "\n", + "3\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "1\n", - "\u24ff\n", + "3->3\n", + "\n", + "\n", + "1\n", + "\u24ff\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "a\n", - "\u24ff\n", + "1->1\n", + "\n", + "\n", + "a\n", + "\u24ff\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "2\n", + "\n", + "2\n", "\n", "\n", - "1->2\n", - "\n", - "\n", - "!a\n", - "\u24ff\n", + "1->2\n", + "\n", + "\n", + "!a\n", + "\u24ff\n", "\n", "\n", - "2->3\n", - "\n", - "\n", - "!a\n", - "\u24ff\n", + "2->3\n", + "\n", + "\n", + "!a\n", + "\u24ff\n", "\n", "\n", - "2->1\n", - "\n", - "\n", - "a\n", - "\u24ff\n", + "2->1\n", + "\n", + "\n", + "a\n", + "\u24ff\n", "\n", "\n", - "" + "\n" ], "text": [ - "" + " *' at 0x7f8dcc11a450> >" ] } ], "prompt_number": 20 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [], + "language": "python", + "metadata": {}, + "outputs": [], + "prompt_number": 20 } ], "metadata": {}