From 58d9a12495697b9ce7edd7de6273fd3483e8b2b3 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 4 May 2018 15:27:51 +0200 Subject: [PATCH] python: introduce spot.jupyter.display_inline() * python/spot/jupyter.py: New file. * python/Makefile.am: Add it. * tests/python/product.ipynb: Use it. * NEWS: Mention it. --- NEWS | 5 + python/Makefile.am | 3 +- python/spot/jupyter.py | 51 + tests/python/product.ipynb | 2065 +++++++++++++++++++----------------- 4 files changed, 1131 insertions(+), 993 deletions(-) create mode 100644 python/spot/jupyter.py diff --git a/NEWS b/NEWS index 27b15d026..aba708710 100644 --- a/NEWS +++ b/NEWS @@ -60,6 +60,11 @@ New in spot 2.5.3.dev (not yet released) options; there are demonstrated on the new https://spot.lrde.epita.fr/ipynb/satmin.html page. + Python: + + - New spot.jupyter package. This currently contains a function for + displaying several argument side by side in a Jupyter notebook. + Bugs fixed: - print_dot() will correctly escape strings containing \n in HTML diff --git a/python/Makefile.am b/python/Makefile.am index 234701e9b..afd174655 100644 --- a/python/Makefile.am +++ b/python/Makefile.am @@ -1,5 +1,5 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2010, 2011, 2013-2017 Laboratoire de Recherche +## Copyright (C) 2010, 2011, 2013-2018 Laboratoire de Recherche ## et Development de l'Epita (LRDE). ## Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), ## département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -41,6 +41,7 @@ nobase_python_PYTHON = \ spot/impl.py \ spot/ltsmin.py \ spot/gen.py \ + spot/jupyter.py \ buddy.py nobase_pyexec_LTLIBRARIES = _buddy.la spot/_impl.la \ spot/_ltsmin.la spot/_gen.la diff --git a/python/spot/jupyter.py b/python/spot/jupyter.py new file mode 100644 index 000000000..0c4dc5a76 --- /dev/null +++ b/python/spot/jupyter.py @@ -0,0 +1,51 @@ +# -*- coding: utf-8 -*- +# Copyright (C) 2018 Laboratoire de Recherche et Développement de l'Epita +# (LRDE). +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +""" +Auxiliary functions for Spot's Python bindings. +""" + +from IPython.display import display, HTML + +def display_inline(*args, per_row=None): + """ + This is a wrapper around IPython's `display()` to display multiple + elements in a row, without forced line break between them. + + If the `per_row` argument is given, at most `per_row` arguments are + displayed on each row, each one taking 1/per_row of the line width. + """ + width = res = '' + if per_row: + width = 'width:{}%;'.format(100//per_row) + for arg in args: + dpy = 'inline-block' + if hasattr(arg, '_repr_svg_'): + rep = arg._repr_svg_() + elif hasattr(arg, '_repr_html_'): + rep = arg._repr_html_() + elif hasattr(arg, '_repr_latex_'): + rep = arg._repr_latex_() + if not per_row: + dpy = 'inline' + else: + rep = str(arg) + res += ("
{}
" + .format(dpy, width, rep)) + display(HTML(res)) diff --git a/tests/python/product.ipynb b/tests/python/product.ipynb index bd23df504..cfdd6e714 100644 --- a/tests/python/product.ipynb +++ b/tests/python/product.ipynb @@ -8,15 +8,9 @@ "source": [ "from IPython.display import display, HTML\n", "import spot\n", + "from spot.jupyter import display_inline # display multiple arguments side-by-side\n", "import buddy\n", - "spot.setup(show_default='.tavb')\n", - "\n", - "def horiz(*args):\n", - " \"\"\"Display multiple arguments side by side in a table.\"\"\"\n", - " s = ''\n", - " for arg in args:\n", - " s += ''\n", - " return HTML(s + '
' + arg.data + '
')" + "spot.setup(show_default='.tvb')" ] }, { @@ -39,370 +33,393 @@ { "data": { "text/html": [ - "
\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", "\n", - "\n", + "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", - "\n", - "I->1\n", - "\n", - "\n", + "\n", + "I->1\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", - "\n", - "1->0\n", - "\n", - "\n", - "1\n", + "\n", + "1->0\n", + "\n", + "\n", + "1\n", "\n", "\n", - "\n", - "0->0\n", - "\n", - "\n", - "a & !b\n", - "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b\n", + "\n", "\n", "\n", - "\n", + "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", - "\n", - "0->2\n", - "\n", - "\n", - "b\n", - "\n", + "\n", + "0->2\n", + "\n", + "\n", + "b\n", + "\n", "\n", "\n", - "\n", - "2->2\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", - "
\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", - "[gen. Büchi 2]\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")\n", + "[gen. Büchi 2]\n", "\n", "\n", - "\n", + "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", - "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!b & c\n", - "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & c\n", + "\n", "\n", "\n", - "\n", - "0->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", + "\n", + "0->0\n", + "\n", + "\n", + "b\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", - "\n", - "0->1\n", - "\n", - "\n", - "!b & !c\n", + "\n", + "0->1\n", + "\n", + "\n", + "!b & !c\n", "\n", "\n", - "\n", - "1->0\n", - "\n", - "\n", - "!b & c\n", - "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!b & c\n", + "\n", "\n", "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", "\n", "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b & !c\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & !c\n", "\n", "\n", - "\n", - "1->1\n", - "\n", - "\n", - "b & !c\n", - "\n", + "\n", + "1->1\n", + "\n", + "\n", + "b & !c\n", + "\n", "\n", "\n", - "
\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", - "[gen. Büchi 3]\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")\n", + "[gen. Büchi 3]\n", "\n", "\n", - "\n", + "\n", "0\n", - "\n", - "1,0\n", + "\n", + "1,0\n", "\n", "\n", - "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "1\n", - "\n", - "0,0\n", + "\n", + "0,0\n", "\n", "\n", - "\n", - "0->1\n", - "\n", - "\n", - "!b & c\n", - "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!b & c\n", + "\n", "\n", "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b\n", - "\n", - "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "2\n", - "\n", - "0,1\n", + "\n", + "0,1\n", "\n", "\n", - "\n", - "0->2\n", - "\n", - "\n", - "!b & !c\n", + "\n", + "0->2\n", + "\n", + "\n", + "!b & !c\n", "\n", "\n", - "\n", - "1->1\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", "\n", "\n", - "\n", - "1->2\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", "\n", "\n", - "\n", + "\n", "3\n", - "\n", - "2,0\n", + "\n", + "2,0\n", "\n", "\n", - "\n", - "1->3\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", + "\n", + "1->3\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", "\n", "\n", - "\n", - "2->1\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", + "\n", + "2->1\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", "\n", "\n", - "\n", - "2->2\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", "\n", "\n", - "\n", - "2->3\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", - "\n", + "\n", + "2->3\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "4\n", - "\n", - "2,1\n", + "\n", + "2,1\n", "\n", "\n", - "\n", - "2->4\n", - "\n", - "\n", - "b & !c\n", - "\n", - "\n", + "\n", + "2->4\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", "\n", "\n", - "\n", - "3->3\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", "\n", "\n", - "\n", - "3->3\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", + "\n", + "3->3\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", "\n", "\n", - "\n", - "3->4\n", - "\n", - "\n", - "!b & !c\n", - "\n", + "\n", + "3->4\n", + "\n", + "\n", + "!b & !c\n", + "\n", "\n", "\n", - "\n", - "4->3\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", + "\n", + "4->3\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", "\n", "\n", - "\n", - "4->3\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", - "\n", + "\n", + "4->3\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", "\n", "\n", - "\n", - "4->4\n", - "\n", - "\n", - "!b & !c\n", - "\n", + "\n", + "4->4\n", + "\n", + "\n", + "!b & !c\n", + "\n", "\n", "\n", - "\n", - "4->4\n", - "\n", - "\n", - "b & !c\n", - "\n", - "\n", + "\n", + "4->4\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", "\n", "\n", - "
" + "\n", + "" ], "text/plain": [ "" ] }, - "execution_count": 2, "metadata": {}, - "output_type": "execute_result" + "output_type": "display_data" } ], "source": [ "a1 = spot.translate('X(a W b)')\n", "a2 = spot.translate('G(Fc U b)')\n", "prod = spot.product(a1, a2)\n", - "horiz(a1.show(), a2.show(), prod.show())" + "display_inline(a1, a2, prod)" ] }, { @@ -424,71 +441,79 @@ { "data": { "text/html": [ - "
\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", "\n", - "\n", + "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", - "\n", - "I->1\n", - "\n", - "\n", + "\n", + "I->1\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", - "\n", - "1->0\n", - "\n", - "\n", - "1\n", + "\n", + "1->0\n", + "\n", + "\n", + "1\n", "\n", "\n", - "\n", - "0->0\n", - "\n", - "\n", - "a & !b\n", - "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b\n", + "\n", "\n", "\n", - "\n", + "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", - "\n", - "0->2\n", - "\n", - "\n", - "b\n", - "\n", + "\n", + "0->2\n", + "\n", + "\n", + "b\n", + "\n", "\n", "\n", - "\n", - "2->2\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", - "
\n", + "\n", + "
\n", "\n", "\n", "Inf(\n", @@ -573,206 +598,214 @@ "\n", "\n", "\n", - "
\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", - "[gen. Büchi 3]\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")\n", + "[gen. Büchi 3]\n", "\n", "\n", - "\n", + "\n", "0\n", - "\n", - "1,0\n", + "\n", + "1,0\n", "\n", "\n", - "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "1\n", - "\n", - "0,0\n", + "\n", + "0,0\n", "\n", "\n", - "\n", - "0->1\n", - "\n", - "\n", - "!b & c\n", - "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!b & c\n", + "\n", "\n", "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b\n", - "\n", - "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "2\n", - "\n", - "0,1\n", + "\n", + "0,1\n", "\n", "\n", - "\n", - "0->2\n", - "\n", - "\n", - "!b & !c\n", + "\n", + "0->2\n", + "\n", + "\n", + "!b & !c\n", "\n", "\n", - "\n", - "1->1\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", "\n", "\n", - "\n", - "1->2\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", "\n", "\n", - "\n", + "\n", "3\n", - "\n", - "2,0\n", + "\n", + "2,0\n", "\n", "\n", - "\n", - "1->3\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", + "\n", + "1->3\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", "\n", "\n", - "\n", - "2->1\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", + "\n", + "2->1\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", "\n", "\n", - "\n", - "2->2\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", "\n", "\n", - "\n", - "2->3\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", - "\n", + "\n", + "2->3\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "4\n", - "\n", - "2,1\n", + "\n", + "2,1\n", "\n", "\n", - "\n", - "2->4\n", - "\n", - "\n", - "b & !c\n", - "\n", - "\n", + "\n", + "2->4\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", "\n", "\n", - "\n", - "3->3\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", "\n", "\n", - "\n", - "3->3\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", + "\n", + "3->3\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", "\n", "\n", - "\n", - "3->4\n", - "\n", - "\n", - "!b & !c\n", - "\n", + "\n", + "3->4\n", + "\n", + "\n", + "!b & !c\n", + "\n", "\n", "\n", - "\n", - "4->3\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", + "\n", + "4->3\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", "\n", "\n", - "\n", - "4->3\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", - "\n", + "\n", + "4->3\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", "\n", "\n", - "\n", - "4->4\n", - "\n", - "\n", - "!b & !c\n", - "\n", + "\n", + "4->4\n", + "\n", + "\n", + "!b & !c\n", + "\n", "\n", "\n", - "\n", - "4->4\n", - "\n", - "\n", - "b & !c\n", - "\n", - "\n", + "\n", + "4->4\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", "\n", "\n", - "
" + "\n", + "" ], "text/plain": [ "" @@ -785,7 +818,7 @@ "source": [ "def show_prod(a1, a2, res):\n", " s1 = a1.num_sets()\n", - " display(horiz(a1.show(), a2.show('.tavb+{}'.format(s1)), res.show()))\n", + " display_inline(a1, a2.show('.tvb+{}'.format(s1)), res)\n", "\n", "show_prod(a1, a2, prod)" ] @@ -816,71 +849,79 @@ { "data": { "text/html": [ - "
\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", "\n", - "\n", + "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", - "\n", - "I->1\n", - "\n", - "\n", + "\n", + "I->1\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", - "\n", - "1->0\n", - "\n", - "\n", - "1\n", + "\n", + "1->0\n", + "\n", + "\n", + "1\n", "\n", "\n", - "\n", - "0->0\n", - "\n", - "\n", - "a & !b\n", - "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b\n", + "\n", "\n", "\n", - "\n", + "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", - "\n", - "0->2\n", - "\n", - "\n", - "b\n", - "\n", + "\n", + "0->2\n", + "\n", + "\n", + "b\n", + "\n", "\n", "\n", - "\n", - "2->2\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", - "
\n", + "\n", + "
\n", "\n", "\n", "Inf(\n", @@ -965,169 +1006,177 @@ "\n", "\n", "\n", - "
\n", - "\n", - "\n", - "t\n", - "[all]\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", - "\n", + "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", - "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", - "\n", - "0->1\n", - "\n", - "\n", - "!b & c\n", + "\n", + "0->1\n", + "\n", + "\n", + "!b & c\n", "\n", "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b\n", + "\n", + "0->1\n", + "\n", + "\n", + "b\n", "\n", "\n", - "\n", + "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", - "\n", - "0->2\n", - "\n", - "\n", - "!b & !c\n", + "\n", + "0->2\n", + "\n", + "\n", + "!b & !c\n", "\n", "\n", - "\n", - "1->1\n", - "\n", - "\n", - "a & !b & c\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !b & c\n", "\n", "\n", - "\n", - "1->2\n", - "\n", - "\n", - "a & !b & !c\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "\n", + "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", - "\n", - "1->3\n", - "\n", - "\n", - "b\n", + "\n", + "1->3\n", + "\n", + "\n", + "b\n", "\n", "\n", - "\n", - "2->1\n", - "\n", - "\n", - "a & !b & c\n", + "\n", + "2->1\n", + "\n", + "\n", + "a & !b & c\n", "\n", "\n", - "\n", - "2->2\n", - "\n", - "\n", - "a & !b & !c\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "\n", - "2->3\n", - "\n", - "\n", - "b & c\n", + "\n", + "2->3\n", + "\n", + "\n", + "b & c\n", "\n", "\n", - "\n", + "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", - "\n", - "2->4\n", - "\n", - "\n", - "b & !c\n", + "\n", + "2->4\n", + "\n", + "\n", + "b & !c\n", "\n", "\n", - "\n", - "3->3\n", - "\n", - "\n", - "!b & c\n", + "\n", + "3->3\n", + "\n", + "\n", + "!b & c\n", "\n", "\n", - "\n", - "3->3\n", - "\n", - "\n", - "b\n", + "\n", + "3->3\n", + "\n", + "\n", + "b\n", "\n", "\n", - "\n", - "3->4\n", - "\n", - "\n", - "!b & !c\n", + "\n", + "3->4\n", + "\n", + "\n", + "!b & !c\n", "\n", "\n", - "\n", - "4->3\n", - "\n", - "\n", - "!b & c\n", + "\n", + "4->3\n", + "\n", + "\n", + "!b & c\n", "\n", "\n", - "\n", - "4->3\n", - "\n", - "\n", - "b & c\n", + "\n", + "4->3\n", + "\n", + "\n", + "b & c\n", "\n", "\n", - "\n", - "4->4\n", - "\n", - "\n", - "!b & !c\n", + "\n", + "4->4\n", + "\n", + "\n", + "!b & !c\n", "\n", "\n", - "\n", - "4->4\n", - "\n", - "\n", - "b & !c\n", + "\n", + "4->4\n", + "\n", + "\n", + "b & !c\n", "\n", "\n", - "
" + "\n", + "" ], "text/plain": [ "" @@ -1242,71 +1291,79 @@ { "data": { "text/html": [ - "
\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", "\n", - "\n", + "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", - "\n", - "I->1\n", - "\n", - "\n", + "\n", + "I->1\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", - "\n", - "1->0\n", - "\n", - "\n", - "1\n", + "\n", + "1->0\n", + "\n", + "\n", + "1\n", "\n", "\n", - "\n", - "0->0\n", - "\n", - "\n", - "a & !b\n", - "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b\n", + "\n", "\n", "\n", - "\n", + "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", - "\n", - "0->2\n", - "\n", - "\n", - "b\n", - "\n", + "\n", + "0->2\n", + "\n", + "\n", + "b\n", + "\n", "\n", "\n", - "\n", - "2->2\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", - "
\n", + "\n", + "
\n", "\n", "\n", "Inf(\n", @@ -1391,206 +1448,214 @@ "\n", "\n", "\n", - "
\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", - "[gen. Büchi 3]\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")\n", + "[gen. Büchi 3]\n", "\n", "\n", - "\n", + "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", - "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", - "\n", - "0->1\n", - "\n", - "\n", - "!b & c\n", - "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!b & c\n", + "\n", "\n", "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b\n", - "\n", - "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", - "\n", - "0->2\n", - "\n", - "\n", - "!b & !c\n", + "\n", + "0->2\n", + "\n", + "\n", + "!b & !c\n", "\n", "\n", - "\n", - "1->1\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", "\n", "\n", - "\n", - "1->2\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", "\n", "\n", - "\n", + "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", - "\n", - "1->3\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", + "\n", + "1->3\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", "\n", "\n", - "\n", - "2->1\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", + "\n", + "2->1\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", "\n", "\n", - "\n", - "2->2\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", "\n", "\n", - "\n", - "2->3\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", - "\n", + "\n", + "2->3\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", - "\n", - "2->4\n", - "\n", - "\n", - "b & !c\n", - "\n", - "\n", + "\n", + "2->4\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", "\n", "\n", - "\n", - "3->3\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", "\n", "\n", - "\n", - "3->3\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", + "\n", + "3->3\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", "\n", "\n", - "\n", - "3->4\n", - "\n", - "\n", - "!b & !c\n", - "\n", + "\n", + "3->4\n", + "\n", + "\n", + "!b & !c\n", + "\n", "\n", "\n", - "\n", - "4->3\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", + "\n", + "4->3\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", "\n", "\n", - "\n", - "4->3\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", - "\n", + "\n", + "4->3\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", "\n", "\n", - "\n", - "4->4\n", - "\n", - "\n", - "!b & !c\n", - "\n", + "\n", + "4->4\n", + "\n", + "\n", + "!b & !c\n", + "\n", "\n", "\n", - "\n", - "4->4\n", - "\n", - "\n", - "b & !c\n", - "\n", - "\n", + "\n", + "4->4\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", "\n", "\n", - "
" + "\n", + "" ], "text/plain": [ "" @@ -1773,71 +1838,79 @@ { "data": { "text/html": [ - "
\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", "\n", - "\n", + "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", - "\n", - "I->1\n", - "\n", - "\n", + "\n", + "I->1\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", - "\n", - "1->0\n", - "\n", - "\n", - "1\n", + "\n", + "1->0\n", + "\n", + "\n", + "1\n", "\n", "\n", - "\n", - "0->0\n", - "\n", - "\n", - "a & !b\n", - "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b\n", + "\n", "\n", "\n", - "\n", + "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", - "\n", - "0->2\n", - "\n", - "\n", - "b\n", - "\n", + "\n", + "0->2\n", + "\n", + "\n", + "b\n", + "\n", "\n", "\n", - "\n", - "2->2\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", - "
\n", + "\n", + "
\n", "\n", "\n", "Inf(\n", @@ -1922,206 +1995,214 @@ "\n", "\n", "\n", - "
\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", - "[gen. Büchi 3]\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")\n", + "[gen. Büchi 3]\n", "\n", "\n", - "\n", + "\n", "0\n", - "\n", - "1,0\n", + "\n", + "1,0\n", "\n", "\n", - "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "1\n", - "\n", - "0,0\n", + "\n", + "0,0\n", "\n", "\n", - "\n", - "0->1\n", - "\n", - "\n", - "!b & c\n", - "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!b & c\n", + "\n", "\n", "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b\n", - "\n", - "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "2\n", - "\n", - "0,1\n", + "\n", + "0,1\n", "\n", "\n", - "\n", - "0->2\n", - "\n", - "\n", - "!b & !c\n", + "\n", + "0->2\n", + "\n", + "\n", + "!b & !c\n", "\n", "\n", - "\n", - "1->1\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", "\n", "\n", - "\n", - "1->2\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", "\n", "\n", - "\n", + "\n", "3\n", - "\n", - "2,0\n", + "\n", + "2,0\n", "\n", "\n", - "\n", - "1->3\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", + "\n", + "1->3\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", "\n", "\n", - "\n", - "2->1\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", + "\n", + "2->1\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", "\n", "\n", - "\n", - "2->2\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", "\n", "\n", - "\n", - "2->3\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", - "\n", + "\n", + "2->3\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "4\n", - "\n", - "2,1\n", + "\n", + "2,1\n", "\n", "\n", - "\n", - "2->4\n", - "\n", - "\n", - "b & !c\n", - "\n", - "\n", + "\n", + "2->4\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", "\n", "\n", - "\n", - "3->3\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", "\n", "\n", - "\n", - "3->3\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", + "\n", + "3->3\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", "\n", "\n", - "\n", - "3->4\n", - "\n", - "\n", - "!b & !c\n", - "\n", + "\n", + "3->4\n", + "\n", + "\n", + "!b & !c\n", + "\n", "\n", "\n", - "\n", - "4->3\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", + "\n", + "4->3\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", "\n", "\n", - "\n", - "4->3\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", - "\n", + "\n", + "4->3\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", "\n", "\n", - "\n", - "4->4\n", - "\n", - "\n", - "!b & !c\n", - "\n", + "\n", + "4->4\n", + "\n", + "\n", + "!b & !c\n", + "\n", "\n", "\n", - "\n", - "4->4\n", - "\n", - "\n", - "b & !c\n", - "\n", - "\n", + "\n", + "4->4\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", "\n", "\n", - "
" + "\n", + "" ], "text/plain": [ "" @@ -2470,7 +2551,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "254 µs ± 11.3 µs per loop (mean ± std. dev. of 7 runs, 1000 loops each)\n" + "409 µs ± 6.68 µs per loop (mean ± std. dev. of 7 runs, 1000 loops each)\n" ] } ], @@ -2487,7 +2568,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "3.35 µs ± 149 ns per loop (mean ± std. dev. of 7 runs, 100000 loops each)\n" + "7.02 µs ± 98.5 ns per loop (mean ± std. dev. of 7 runs, 100000 loops each)\n" ] } ],