diff --git a/tests/python/_product_weak.ipynb b/tests/python/_product_weak.ipynb index 5defa2ef4..7c31ec51a 100644 --- a/tests/python/_product_weak.ipynb +++ b/tests/python/_product_weak.ipynb @@ -24,7 +24,7 @@ "metadata": {}, "outputs": [], "source": [ - "auts = [a for a in spot.automata(\"\"\"\n", + "auts = list(spot.automata(\"\"\"\n", "HOA: v1\n", "name: \"a\"\n", "States: 2\n", @@ -106,20 +106,40 @@ "[!0] 0 {0}\n", "[0] 0\n", "--END--\n", - "\"\"\")]" + "\"\"\"))" ] }, { "cell_type": "code", "execution_count": 3, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "6" + ] + }, + "execution_count": 3, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "len(auts)" + ] + }, + { + "cell_type": "code", + "execution_count": 4, "metadata": { "scrolled": false }, "outputs": [ { "data": { - "text/html": [ - "
\n", + "image/svg+xml": [ + "\n", "\n", "\n", + "\n", + "\n", + "\n", + "\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1,1\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2,2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", "
" ], "text/plain": [ @@ -279,54 +378,6 @@ " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", "\n", - "\n", - "\n", - "\n", - "a\n", - "\n", - "t\n", - "[all]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", "\n", "\n", @@ -451,6 +502,130 @@ "\n", "\n", "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1,1\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "0,1\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "2,0\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "2,1\n", + "\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", "
" ], "text/plain": [ @@ -468,54 +643,6 @@ " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", "\n", - "\n", - "\n", - "\n", - "a\n", - "\n", - "t\n", - "[all]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", "\n", "\n", @@ -641,6 +768,130 @@ "\n", "\n", "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1,1\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "0,1\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "2,0\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "2,1\n", + "\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", "
" ], "text/plain": [ @@ -658,54 +909,6 @@ " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", "\n", - "\n", - "\n", - "\n", - "a\n", - "\n", - "t\n", - "[all]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", "\n", "\n", @@ -811,6478 +1014,6 @@ "\n", "\n", "\n", - "
" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/html": [ - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "a\n", - "\n", - "t\n", - "[all]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") & Fin(\n", - "\n", - ")\n", - "[Rabin-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") & Fin(\n", - "\n", - ")\n", - "[Rabin-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "1,0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "a & !d\n", - "\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "a & d\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/html": [ - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "a\n", - "\n", - "t\n", - "[all]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")\n", - "[Streett-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")\n", - "[Streett-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "1,0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "a & !d\n", - "\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "a & d\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/html": [ - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Fb\n", - "\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "a\n", - "\n", - "t\n", - "[all]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "1,1\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "\n", - "2\n", - "\n", - "1,0\n", - "\n", - "\n", - "\n", - "0->2\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "
" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/html": [ - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Fb\n", - "\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Fb\n", - "\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "1,1\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/html": [ - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Fb\n", - "\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Fb\n", - "\n", - "[co-Büchi]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "1,1\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/html": [ - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Fb\n", - "\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "GFc\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!c\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "c\n", - "\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "1,0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!b & !c\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b & !c\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!c\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "c\n", - "\n", - "\n", - "\n", - "\n", - "
" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/html": [ - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Fb\n", - "\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") & Fin(\n", - "\n", - ")\n", - "[Rabin-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") & Fin(\n", - "\n", - ")\n", - "[Rabin-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "1,0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!b & !d\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!b & d\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b & !d\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b & d\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/html": [ - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Fb\n", - "\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")\n", - "[Streett-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "1,0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!b & !d\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!b & d\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b & !d\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b & d\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "\n", - "
" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/html": [ - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Fb\n", - "\n", - "[co-Büchi]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "a\n", - "\n", - "t\n", - "[all]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "[co-Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1,1\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "1,0\n", - "\n", - "\n", - "\n", - "0->2\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "
" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/html": [ - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Fb\n", - "\n", - "[co-Büchi]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Fb\n", - "\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "1,1\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/html": [ - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Fb\n", - "\n", - "[co-Büchi]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Fb\n", - "\n", - "[co-Büchi]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "[co-Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1,1\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/html": [ - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Fb\n", - "\n", - "[co-Büchi]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "GFc\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!c\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "c\n", - "\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "1,0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!b & !c\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b & !c\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!c\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "c\n", - "\n", - "\n", - "\n", - "\n", - "
" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/html": [ - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Fb\n", - "\n", - "[co-Büchi]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") & Fin(\n", - "\n", - ")\n", - "[Rabin-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") & Fin(\n", - "\n", - ")\n", - "[Rabin-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "1,0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!b & !d\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!b & d\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b & !d\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b & d\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/html": [ - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Fb\n", - "\n", - "[co-Büchi]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")\n", - "[Streett-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "1,0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!b & !d\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!b & d\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b & !d\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b & d\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "\n", - "
" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - } - ], - "source": [ - "autslen = len(auts)\n", - "# We have trouble with Jupyter on i386, where running the full loop abort with some low-level \n", - "# exeptions from Jupyter client. \n", - "for left in auts[0:autslen//2]:\n", - " for right in auts:\n", - " display_inline(left, right, spot.product(left, right))" - ] - }, - { - "cell_type": "code", - "execution_count": 4, - "metadata": {}, - "outputs": [ - { - "data": { - "text/html": [ - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "GFc\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!c\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "c\n", - "\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "a\n", - "\n", - "t\n", - "[all]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0,1\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "a & !c\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "a & c\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!c\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "c\n", - "\n", - "\n", - "\n", - "\n", - "
" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/html": [ - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "GFc\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!c\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "c\n", - "\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Fb\n", - "\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0,1\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!b & !c\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b & !c\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!c\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "c\n", - "\n", - "\n", - "\n", - "\n", - "
" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/html": [ - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "GFc\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!c\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "c\n", - "\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Fb\n", - "\n", - "[co-Büchi]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0,1\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!b & !c\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b & !c\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!c\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "c\n", - "\n", - "\n", - "\n", - "\n", - "
" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/html": [ - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "GFc\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!c\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "c\n", - "\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "GFc\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!c\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "c\n", - "\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", - "[gen. Büchi 2]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!c\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "c\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "
" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/html": [ - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "GFc\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!c\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "c\n", - "\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") & Fin(\n", - "\n", - ")\n", - "[Rabin-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "(Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")) & Fin(\n", - "\n", - ")\n", - "[Streett-like 3]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!c & !d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!c & d\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "c & !d\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "c & d\n", - "\n", - "\n", - "\n", - "\n", - "
" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/html": [ - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "GFc\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!c\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "c\n", - "\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")\n", - "[Streett-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") & (Inf(\n", - "\n", - ") | Fin(\n", - "\n", - "))\n", - "[Streett-like 2]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!c & !d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!c & d\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "c & !d\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "c & d\n", - "\n", - "\n", - "\n", - "\n", - "
" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/html": [ - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") & Fin(\n", - "\n", - ")\n", - "[Rabin-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "a\n", - "\n", - "t\n", - "[all]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") & Fin(\n", - "\n", - ")\n", - "[Rabin-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0,1\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "a & !d\n", - "\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "a & d\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/html": [ - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") & Fin(\n", - "\n", - ")\n", - "[Rabin-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Fb\n", - "\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") & Fin(\n", - "\n", - ")\n", - "[Rabin-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0,1\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!b & !d\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!b & d\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b & !d\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b & d\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/html": [ - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") & Fin(\n", - "\n", - ")\n", - "[Rabin-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Fb\n", - "\n", - "[co-Büchi]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") & Fin(\n", - "\n", - ")\n", - "[Rabin-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0,1\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!b & !d\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!b & d\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b & !d\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b & d\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/html": [ - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") & Fin(\n", - "\n", - ")\n", - "[Rabin-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "GFc\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!c\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "c\n", - "\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "(Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")) & Fin(\n", - "\n", - ")\n", - "[Streett-like 3]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!c & !d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "c & !d\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!c & d\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "c & d\n", - "\n", - "\n", - "\n", - "\n", - "
" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/html": [ - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") & Fin(\n", - "\n", - ")\n", - "[Rabin-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") & Fin(\n", - "\n", - ")\n", - "[Rabin-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "(Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")) & Fin(\n", - "\n", - ") & Fin(\n", - "\n", - ")\n", - "[Streett-like 4]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/html": [ - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") & Fin(\n", - "\n", - ")\n", - "[Rabin-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")\n", - "[Streett-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") & Fin(\n", - "\n", - ") & (Inf(\n", - "\n", - ") | Fin(\n", - "\n", - "))\n", - "[Streett-like 3]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/html": [ - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")\n", - "[Streett-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "a\n", - "\n", - "t\n", - "[all]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")\n", - "[Streett-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0,1\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "a & !d\n", - "\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "a & d\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/html": [ - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")\n", - "[Streett-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Fb\n", - "\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0,1\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!b & !d\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!b & d\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b & !d\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b & d\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "\n", - "
" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/html": [ - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")\n", - "[Streett-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Fb\n", - "\n", - "[co-Büchi]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0,1\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!b & !d\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!b & d\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b & !d\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b & d\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "\n", - "
" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/html": [ - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")\n", - "[Streett-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "GFc\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!c\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "c\n", - "\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "(Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")) & Inf(\n", - "\n", - ")\n", - "[Streett-like 2]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!c & !d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "c & !d\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!c & d\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "c & d\n", - "\n", - "\n", - "\n", - "\n", - "
" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/html": [ - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")\n", - "[Streett-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") & Fin(\n", - "\n", - ")\n", - "[Rabin-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "(Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")) & Inf(\n", - "\n", - ") & Fin(\n", - "\n", - ")\n", - "[Streett-like 3]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/html": [ - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")\n", - "[Streett-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")\n", - "[Streett-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "(Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")) & (Inf(\n", - "\n", - ") | Fin(\n", - "\n", - "))\n", - "[Streett-like 2]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - } - ], - "source": [ - "for left in auts[autslen//2:]:\n", - " for right in auts:\n", - " display_inline(left, right, spot.product(left, right))" - ] - }, - { - "cell_type": "code", - "execution_count": 5, - "metadata": {}, - "outputs": [ - { - "data": { - "text/html": [ - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "a\n", - "\n", - "t\n", - "[all]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "a\n", - "\n", - "t\n", - "[all]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1,1\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "\n", - "2\n", - "\n", - "2,2\n", - "\n", - "\n", - "\n", - "0->2\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/html": [ - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "a\n", - "\n", - "t\n", - "[all]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Fb\n", - "\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1,1\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "0,1\n", - "\n", - "\n", - "\n", - "0->2\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "2,0\n", - "\n", - "\n", - "\n", - "0->3\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", - "\n", - "4\n", - "\n", - "2,1\n", - "\n", - "\n", - "\n", - "0->4\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "4->3\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "4->4\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "
" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/html": [ - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "a\n", - "\n", - "t\n", - "[all]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Fb\n", - "\n", - "[co-Büchi]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1,1\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0,0\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "0,1\n", - "\n", - "\n", - "\n", - "0->2\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "2,0\n", - "\n", - "\n", - "\n", - "0->3\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", - "\n", - "4\n", - "\n", - "2,1\n", - "\n", - "\n", - "\n", - "0->4\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "4->3\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "4->4\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "
" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/html": [ - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "a\n", - "\n", - "t\n", - "[all]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "GFc\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!c\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "c\n", - "\n", - "\n", - "\n", - "\n", "
\n", "\n", @@ -7404,54 +1135,6 @@ " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", "\n", - "\n", - "\n", - "\n", - "a\n", - "\n", - "t\n", - "[all]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", "\n", "\n", @@ -7499,6 +1182,73 @@ "\n", "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ") & Fin(\n", + "\n", + ")\n", + "[Rabin-like 1]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "1,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & !d\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & d\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "d\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", "\n", "\n", @@ -7613,54 +1363,6 @@ " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", "\n", - "\n", - "\n", - "\n", - "a\n", - "\n", - "t\n", - "[all]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", "\n", "\n", @@ -7708,6 +1410,73 @@ "\n", "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ") | Fin(\n", + "\n", + ")\n", + "[Streett-like 1]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "1,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & !d\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & d\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "d\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", "\n", "\n", @@ -7810,11 +1579,29 @@ }, "metadata": {}, "output_type": "display_data" - }, + } + ], + "source": [ + "autslen = len(auts)\n", + "# In a previous version we used to iterate over all possible left automata with \"for left in auts:\"\n", + "# however we had trouble with Jupyter on i386, where running the full loop abort with some low-level \n", + "# exeptions from Jupyter client. Halving the loop helped for some times, but then the timeout\n", + "# came back. So we do one left automaton at at time.\n", + "left = auts[0]\n", + "display(left)\n", + "for right in auts:\n", + " display_inline(right, spot.product(left, right), spot.product_or(left, right))" + ] + }, + { + "cell_type": "code", + "execution_count": 5, + "metadata": {}, + "outputs": [ { "data": { - "text/html": [ - "
\n", + "image/svg+xml": [ + "\n", "\n", "\n", "\n", + "\n", + "\n", + "\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "1,1\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "1,0\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", "\n", "\n", @@ -8113,53 +1985,52 @@ " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", "\n", - "\n", - "\n", + "\n", + "\n", "\n", - "Fb\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", - "\n", + "\n", "\n", - "1\n", - "\n", - "1\n", + "0\n", + "\n", + "1,1\n", "\n", - "\n", + "\n", "\n", - "I->1\n", - "\n", - "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", @@ -8240,61 +2111,6 @@ "\n", "Fb\n", "\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Fb\n", - "\n", "[co-Büchi]\n", "\n", "\n", @@ -8393,6 +2209,60 @@ "\n", "\n", "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "1,1\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", "
" ], "text/plain": [ @@ -8410,61 +2280,6 @@ " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", "\n", - "\n", - "\n", - "\n", - "Fb\n", - "\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", "\n", "\n", @@ -8511,6 +2326,84 @@ "\n", "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "1,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", "\n", "\n", @@ -8603,61 +2496,6 @@ " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", "\n", - "\n", - "\n", - "\n", - "Fb\n", - "\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", "\n", "\n", @@ -8705,6 +2543,86 @@ "\n", "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ") & Fin(\n", + "\n", + ")\n", + "[Rabin-like 1]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "1,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & !d\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & d\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & !d\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & d\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "d\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", "\n", "\n", @@ -8795,61 +2713,6 @@ " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", "\n", - "\n", - "\n", - "\n", - "Fb\n", - "\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", "\n", "\n", @@ -8897,6 +2760,85 @@ "\n", "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "1,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & !d\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & d\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & !d\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & d\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "d\n", + "\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", "\n", "\n", @@ -8980,11 +2922,24 @@ }, "metadata": {}, "output_type": "display_data" - }, + } + ], + "source": [ + "left = auts[1]\n", + "display(left)\n", + "for right in auts:\n", + " display_inline(right, spot.product(left, right), spot.product_or(left, right))" + ] + }, + { + "cell_type": "code", + "execution_count": 6, + "metadata": {}, + "outputs": [ { "data": { - "text/html": [ - "
\n", + "image/svg+xml": [ + "\n", "\n", "\n", "\n", + "\n", + "\n", + "\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1,1\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "1,0\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", "\n", "\n", @@ -9234,61 +3275,6 @@ "\n", "Fb\n", "\n", - "[co-Büchi]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Fb\n", - "\n", "[Büchi]\n", "\n", "\n", @@ -9387,6 +3373,60 @@ "\n", "\n", "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "1,1\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", "
" ], "text/plain": [ @@ -9459,61 +3499,60 @@ " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", "\n", - "\n", - "\n", - "\n", - "Fb\n", - "\n", - "[co-Büchi]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1,1\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", "\n", "\n", @@ -9580,61 +3619,6 @@ " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", "\n", - "\n", - "\n", - "\n", - "Fb\n", - "\n", - "[co-Büchi]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", "\n", "\n", @@ -9681,6 +3665,84 @@ "\n", "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "1,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", "\n", "\n", @@ -9773,61 +3835,6 @@ " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", "\n", - "\n", - "\n", - "\n", - "Fb\n", - "\n", - "[co-Büchi]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", "\n", "\n", @@ -9875,6 +3882,86 @@ "\n", "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ") & Fin(\n", + "\n", + ")\n", + "[Rabin-like 1]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "1,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & !d\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & d\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & !d\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & d\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "d\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", "\n", "\n", @@ -9965,61 +4052,6 @@ " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", "\n", - "\n", - "\n", - "\n", - "Fb\n", - "\n", - "[co-Büchi]\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", "\n", "\n", @@ -10067,6 +4099,85 @@ "\n", "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "1,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & !d\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & d\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & !d\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & d\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "d\n", + "\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", "\n", "\n", @@ -10153,22 +4264,21 @@ } ], "source": [ - "for left in auts[0:autslen//2]:\n", - " for right in auts:\n", - " display_inline(left, right, spot.product_or(left, right))" + "left = auts[2]\n", + "display(left)\n", + "for right in auts:\n", + " display_inline(right, spot.product(left, right), spot.product_or(left, right))" ] }, { "cell_type": "code", - "execution_count": 6, - "metadata": { - "scrolled": false - }, + "execution_count": 7, + "metadata": {}, "outputs": [ { "data": { - "text/html": [ - "
\n", + "image/svg+xml": [ + "\n", "\n", "\n", "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,1\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & c\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", "\n", "\n", @@ -10382,51 +4568,6 @@ " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", "\n", - "\n", - "\n", - "\n", - "GFc\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!c\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "c\n", - "\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", "\n", "\n", @@ -10483,6 +4624,84 @@ "\n", "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,1\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", "\n", "\n", @@ -10575,51 +4794,6 @@ " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", "\n", - "\n", - "\n", - "\n", - "GFc\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!c\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "c\n", - "\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", "\n", "\n", @@ -10676,6 +4850,84 @@ "\n", "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,1\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", "\n", "\n", @@ -10813,43 +5065,45 @@ " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", "\n", - "\n", - "\n", - "\n", - "GFc\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")\n", + "[gen. Büchi 2]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0,0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!c\n", + "\n", + "\n", + "!c\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "c\n", - "\n", + "\n", + "\n", + "c\n", + "\n", + "\n", "\n", "\n", "\n", @@ -10917,51 +5171,6 @@ " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", "\n", - "\n", - "\n", - "\n", - "GFc\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!c\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "c\n", - "\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", "\n", "\n", @@ -11009,6 +5218,71 @@ "\n", "\n", + "\n", + "\n", + "\n", + "(Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")) & Fin(\n", + "\n", + ")\n", + "[Streett-like 3]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c & !d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c & d\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c & !d\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c & d\n", + "\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", "\n", "\n", @@ -11085,51 +5359,6 @@ " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", "\n", - "\n", - "\n", - "\n", - "GFc\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!c\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "c\n", - "\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", "\n", "\n", @@ -11177,6 +5406,71 @@ "\n", "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ") & (Inf(\n", + "\n", + ") | Fin(\n", + "\n", + "))\n", + "[Streett-like 2]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c & !d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c & d\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c & !d\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c & d\n", + "\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", "\n", "\n", @@ -11244,11 +5538,24 @@ }, "metadata": {}, "output_type": "display_data" - }, + } + ], + "source": [ + "left = auts[3]\n", + "display(left)\n", + "for right in auts:\n", + " display_inline(right, spot.product(left, right), spot.product_or(left, right))" + ] + }, + { + "cell_type": "code", + "execution_count": 8, + "metadata": {}, + "outputs": [ { "data": { - "text/html": [ - "
\n", + "image/svg+xml": [ + "\n", "\n", "\n", "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ") & Fin(\n", + "\n", + ")\n", + "[Rabin-like 1]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,1\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & !d\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & d\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "d\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", "\n", "\n", @@ -11462,52 +5847,6 @@ " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") & Fin(\n", - "\n", - ")\n", - "[Rabin-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", "\n", "\n", @@ -11564,6 +5903,86 @@ "\n", "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ") & Fin(\n", + "\n", + ")\n", + "[Rabin-like 1]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,1\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & !d\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & d\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & !d\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & d\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "d\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", "\n", "\n", @@ -11654,52 +6073,6 @@ " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") & Fin(\n", - "\n", - ")\n", - "[Rabin-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", "\n", "\n", @@ -11756,6 +6129,86 @@ "\n", "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ") & Fin(\n", + "\n", + ")\n", + "[Rabin-like 1]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,1\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & !d\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & d\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & !d\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & d\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "d\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", "\n", "\n", @@ -11846,52 +6299,6 @@ " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") & Fin(\n", - "\n", - ")\n", - "[Rabin-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", "\n", "\n", @@ -11944,6 +6351,71 @@ "\n", "(Inf(\n", "\n", + ")&Inf(\n", + "\n", + ")) & Fin(\n", + "\n", + ")\n", + "[Streett-like 3]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c & !d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c & !d\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c & d\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c & d\n", + "\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "(Inf(\n", + "\n", ") & Fin(\n", "\n", ")) | Inf(\n", @@ -12061,43 +6533,48 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") & Fin(\n", - "\n", - ")\n", - "[Rabin-like 1]\n", + "\n", + "\n", + "\n", + "(Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")) & Fin(\n", + "\n", + ") & Fin(\n", + "\n", + ")\n", + "[Streett-like 4]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0,0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!d\n", - "\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "d\n", + "\n", + "\n", + "d\n", "\n", "\n", "\n", @@ -12170,52 +6647,6 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") & Fin(\n", - "\n", - ")\n", - "[Rabin-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", "\n", "\n", @@ -12262,6 +6693,57 @@ "\n", "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ") & Fin(\n", + "\n", + ") & (Inf(\n", + "\n", + ") | Fin(\n", + "\n", + "))\n", + "[Streett-like 3]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "d\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", "\n", "\n", @@ -12315,11 +6797,24 @@ }, "metadata": {}, "output_type": "display_data" - }, + } + ], + "source": [ + "left = auts[4]\n", + "display(left)\n", + "for right in auts:\n", + " display_inline(right, spot.product(left, right), spot.product_or(left, right))" + ] + }, + { + "cell_type": "code", + "execution_count": 9, + "metadata": {}, + "outputs": [ { "data": { - "text/html": [ - "
\n", + "image/svg+xml": [ + "\n", "\n", "\n", "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ") | Fin(\n", + "\n", + ")\n", + "[Streett-like 1]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,1\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & !d\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & d\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "d\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", "\n", "\n", @@ -12530,52 +7103,6 @@ " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")\n", - "[Streett-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", "\n", "\n", @@ -12632,6 +7159,85 @@ "\n", "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,1\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & !d\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & d\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & !d\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & d\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "d\n", + "\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", "\n", "\n", @@ -12724,52 +7330,6 @@ " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")\n", - "[Streett-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", "\n", "\n", @@ -12826,6 +7386,85 @@ "\n", "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,1\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & !d\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & d\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & !d\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & d\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "d\n", + "\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", "\n", "\n", @@ -12918,52 +7557,6 @@ " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", "\n", - "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")\n", - "[Streett-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", "\n", "\n", @@ -13010,6 +7603,71 @@ "\n", "\n", + "\n", + "\n", + "\n", + "(Inf(\n", + "\n", + ") | Fin(\n", + "\n", + ")) & Inf(\n", + "\n", + ")\n", + "[Streett-like 2]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c & !d\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c & !d\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!c & d\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "c & d\n", + "\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", "\n", "\n", @@ -13087,52 +7745,6 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")\n", - "[Streett-like 1]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!d\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "d\n", - "\n", - "\n", - "\n", - "
\n", - "\n", - "\n", - "\n", "\n", "\n", @@ -13179,6 +7791,57 @@ "\n", "\n", + "\n", + "\n", + "\n", + "(Inf(\n", + "\n", + ") | Fin(\n", + "\n", + ")) & Inf(\n", + "\n", + ") & Fin(\n", + "\n", + ")\n", + "[Streett-like 3]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "d\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", "\n", "\n", @@ -13288,43 +7951,48 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")\n", - "[Streett-like 1]\n", + "\n", + "\n", + "\n", + "(Inf(\n", + "\n", + ") | Fin(\n", + "\n", + ")) & (Inf(\n", + "\n", + ") | Fin(\n", + "\n", + "))\n", + "[Streett-like 2]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0,0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!d\n", - "\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "d\n", + "\n", + "\n", + "d\n", "\n", "\n", "\n", @@ -13390,9 +8058,10 @@ } ], "source": [ - "for left in auts[autslen//2:]:\n", - " for right in auts:\n", - " display_inline(left, right, spot.product_or(left, right))" + "left = auts[5]\n", + "display(left)\n", + "for right in auts:\n", + " display_inline(right, spot.product(left, right), spot.product_or(left, right))" ] }, { @@ -13419,7 +8088,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.6.7rc1" + "version": "3.7.4+" } }, "nbformat": 4,