{ "cells": [ { "cell_type": "markdown", "metadata": {}, "source": [ "Test the optimization of `product()` for weak arguments." ] }, { "cell_type": "code", "execution_count": 1, "metadata": {}, "outputs": [], "source": [ "import spot\n", "spot.setup()\n", "from spot.jupyter import display_inline" ] }, { "cell_type": "code", "execution_count": 2, "metadata": {}, "outputs": [], "source": [ "auts = list(spot.automata(\"\"\"\n", "HOA: v1\n", "name: \"a\"\n", "States: 2\n", "Start: 1\n", "AP: 1 \"a\"\n", "acc-name: all\n", "Acceptance: 0 t\n", "properties: trans-labels explicit-labels state-acc deterministic\n", "properties: stutter-invariant terminal\n", "--BODY--\n", "State: 0\n", "[t] 0\n", "State: 1\n", "[0] 0\n", "--END--\n", "HOA: v1\n", "name: \"Fb\"\n", "States: 2\n", "Start: 1\n", "AP: 1 \"b\"\n", "acc-name: Buchi\n", "Acceptance: 1 Inf(0)\n", "properties: trans-labels explicit-labels state-acc complete\n", "properties: deterministic stutter-invariant terminal\n", "--BODY--\n", "State: 0 {0}\n", "[t] 0\n", "State: 1\n", "[0] 0\n", "[!0] 1\n", "--END--\n", "HOA: v1\n", "name: \"Fb\"\n", "States: 2\n", "Start: 1\n", "AP: 1 \"b\"\n", "acc-name: co-Buchi\n", "Acceptance: 1 Fin(0)\n", "properties: trans-labels explicit-labels state-acc complete\n", "properties: deterministic stutter-invariant terminal\n", "--BODY--\n", "State: 0 \n", "[t] 0\n", "State: 1 {0}\n", "[0] 0\n", "[!0] 1\n", "--END--\n", "HOA: v1\n", "name: \"GFc\"\n", "States: 1\n", "Start: 0\n", "AP: 1 \"c\"\n", "acc-name: Buchi\n", "Acceptance: 1 Inf(0)\n", "properties: trans-labels explicit-labels trans-acc complete\n", "properties: deterministic stutter-invariant\n", "--BODY--\n", "State: 0\n", "[!0] 0\n", "[0] 0 {0}\n", "--END--\n", "HOA: v1\n", "States: 1\n", "Start: 0\n", "AP: 1 \"d\"\n", "Acceptance: 1 Inf(0)&Fin(0)\n", "--BODY--\n", "State: 0\n", "[!0] 0 {0}\n", "[0] 0\n", "--END--\n", "HOA: v1\n", "States: 1\n", "Start: 0\n", "AP: 1 \"d\"\n", "Acceptance: 1 Inf(0)|Fin(0)\n", "--BODY--\n", "State: 0 \n", "[!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": { "image/svg+xml": [ "\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" ], "text/plain": [ " *' at 0x7fa5b04de690> >" ] }, "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", "t\n", "[all]\n", "\n", "\n", "\n", "0\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\n", "\n", "\n", "\n", "1->1\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", "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", "1\n", "\n", "\n", "0,0\n", "\n", "\n", "\n", "0->1\n", "\n", "\n", "a & b\n", "\n", "\n", "\n", "2\n", "\n", "0,1\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", "\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", "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", "1\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", "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", "\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", "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", "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", "\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", "1\n", "\n", "0,0\n", "\n", "\n", "\n", "0->1\n", "\n", "\n", "a & !c\n", "⓿\n", "\n", "\n", "\n", "0->1\n", "\n", "\n", "a & c\n", "⓿\n", "\n", "\n", "\n", "2\n", "\n", "2,0\n", "\n", "\n", "\n", "0->2\n", "\n", "\n", "!a & !c\n", "⓿\n", "\n", "\n", "\n", "0->2\n", "\n", "\n", "!a & c\n", "⓿\n", "\n", "\n", "\n", "1->1\n", "\n", "\n", "!c\n", "⓿\n", "\n", "\n", "\n", "1->1\n", "\n", "\n", "c\n", "⓿\n", "\n", "\n", "\n", "2->2\n", "\n", "\n", "!c\n", "\n", "\n", "\n", "2->2\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", "\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", "
\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", "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", "\n", "2\n", "\n", "2,0\n", "\n", "\n", "\n", "0->2\n", "\n", "\n", "!a & !d\n", "⓿\n", "\n", "\n", "\n", "0->2\n", "\n", "\n", "!a & d\n", "⓿\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", "2->2\n", "\n", "\n", "!d\n", "\n", "\n", "\n", "2->2\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", "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", "\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", "0->1\n", "\n", "\n", "a & d\n", "\n", "\n", "\n", "2\n", "\n", "2,0\n", "\n", "\n", "\n", "0->2\n", "\n", "\n", "!a & !d\n", "\n", "\n", "\n", "0->2\n", "\n", "\n", "!a & d\n", "\n", "\n", "\n", "1->1\n", "\n", "\n", "!d\n", "\n", "\n", "\n", "1->1\n", "\n", "\n", "d\n", "\n", "\n", "\n", "2->2\n", "\n", "\n", "!d\n", "⓿\n", "\n", "\n", "\n", "2->2\n", "\n", "\n", "d\n", "\n", "\n", "\n", "
" ], "text/plain": [ "" ] }, "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": { "image/svg+xml": [ "\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" ], "text/plain": [ " *' at 0x7fa5b04de600> >" ] }, "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", "[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", "\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,2\n", "\n", "\n", "\n", "0->2\n", "\n", "\n", "!a & b\n", "\n", "\n", "\n", "3\n", "\n", "\n", "1,0\n", "\n", "\n", "\n", "0->3\n", "\n", "\n", "a & !b\n", "\n", "\n", "\n", "4\n", "\n", "1,2\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->2\n", "\n", "\n", "1\n", "\n", "\n", "\n", "3->1\n", "\n", "\n", "b\n", "\n", "\n", "\n", "3->3\n", "\n", "\n", "!b\n", "\n", "\n", "\n", "4->2\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", "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", "
\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", "\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", "
\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", "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", "
\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", "\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", "\n", "1->1\n", "\n", "\n", "!c\n", "⓿\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", "\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", "
\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", "\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", "
\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", "0->0\n", "\n", "\n", "!b & !d\n", "⓿\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", "\n", "0->1\n", "\n", "\n", "b & d\n", "\n", "\n", "\n", "1->1\n", "\n", "\n", "!d\n", "\n", "\n", "\n", "1->1\n", "\n", "\n", "d\n", "\n", "\n", "\n", "
" ], "text/plain": [ "" ] }, "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": { "image/svg+xml": [ "\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" ], "text/plain": [ " *' at 0x7fa5b04de6c0> >" ] }, "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", "[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", "\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,2\n", "\n", "\n", "\n", "0->2\n", "\n", "\n", "!a & b\n", "\n", "\n", "\n", "3\n", "\n", "\n", "1,0\n", "\n", "\n", "\n", "0->3\n", "\n", "\n", "a & !b\n", "\n", "\n", "\n", "4\n", "\n", "1,2\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->2\n", "\n", "\n", "1\n", "\n", "\n", "\n", "3->1\n", "\n", "\n", "b\n", "\n", "\n", "\n", "3->3\n", "\n", "\n", "!b\n", "\n", "\n", "\n", "4->2\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", "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", "
\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", "\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", "\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", "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", "
\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", "\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", "\n", "1->1\n", "\n", "\n", "!c\n", "⓿\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", "\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", "
\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", "\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", "
\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", "0->0\n", "\n", "\n", "!b & !d\n", "⓿\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", "\n", "0->1\n", "\n", "\n", "b & d\n", "\n", "\n", "\n", "1->1\n", "\n", "\n", "!d\n", "\n", "\n", "\n", "1->1\n", "\n", "\n", "d\n", "\n", "\n", "\n", "
" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "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": 7, "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ "\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" ], "text/plain": [ " *' at 0x7fa5b04de720> >" ] }, "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", ")\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", "\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", "\n", "0->1\n", "\n", "\n", "a & c\n", "⓿\n", "\n", "\n", "\n", "2\n", "\n", "0,2\n", "\n", "\n", "\n", "0->2\n", "\n", "\n", "!a & !c\n", "⓿\n", "\n", "\n", "\n", "0->2\n", "\n", "\n", "!a & c\n", "⓿\n", "\n", "\n", "\n", "1->1\n", "\n", "\n", "!c\n", "⓿\n", "\n", "\n", "\n", "1->1\n", "\n", "\n", "c\n", "⓿\n", "\n", "\n", "\n", "2->2\n", "\n", "\n", "!c\n", "\n", "\n", "\n", "2->2\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", ")\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", "\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", "\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", "\n", "1->1\n", "\n", "\n", "!c\n", "⓿\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", ")\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", "\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", "\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", "\n", "1->1\n", "\n", "\n", "!c\n", "⓿\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", "\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", "
\n", "\n", "\n", "\n", "\n", "\n", "\n", "Inf(\n", "⓿\n", ") | Inf(\n", "❶\n", ")\n", "[Fin-less 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", "\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", "
\n", "\n", "\n", "\n", "\n", "\n", "\n", "Inf(\n", "⓿\n", ") | (Inf(\n", "❶\n", ") & Fin(\n", "❶\n", "))\n", "[Rabin-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", "[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", "
\n", "\n", "\n", "\n", "\n", "\n", "\n", "Inf(\n", "⓿\n", ") | Inf(\n", "❶\n", ") | Fin(\n", "❶\n", ")\n", "[Rabin-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" } ], "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": { "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\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" ], "text/plain": [ " *' at 0x7fa5b04de780> >" ] }, "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,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", "\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 & !d\n", "⓿\n", "\n", "\n", "\n", "0->1\n", "\n", "\n", "a & d\n", "⓿\n", "\n", "\n", "\n", "2\n", "\n", "0,2\n", "\n", "\n", "\n", "0->2\n", "\n", "\n", "!a & !d\n", "⓿\n", "\n", "\n", "\n", "0->2\n", "\n", "\n", "!a & d\n", "⓿\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", "2->2\n", "\n", "\n", "!d\n", "\n", "\n", "\n", "2->2\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", "[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", "\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", "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", "
\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", "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", "
\n", "\n", "\n", "\n", "\n", "\n", "\n", "(Inf(\n", "⓿\n", ") & Fin(\n", "⓿\n", ")) | Inf(\n", "❶\n", ")\n", "[Rabin-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", "[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", "
\n", "\n", "\n", "\n", "\n", "\n", "\n", "(Inf(\n", "⓿\n", ") & Fin(\n", "⓿\n", ")) | (Inf(\n", "❶\n", ") & Fin(\n", "❶\n", "))\n", "[Rabin-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" }, { "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", ") & (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", "\n", "(Inf(\n", "⓿\n", ") & Fin(\n", "⓿\n", ")) | Inf(\n", "❶\n", ") | Fin(\n", "❶\n", ")\n", "[Rabin-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" } ], "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": { "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\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" ], "text/plain": [ " *' at 0x7fa5b04de7e0> >" ] }, "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,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", "\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", "0->1\n", "\n", "\n", "a & d\n", "\n", "\n", "\n", "2\n", "\n", "0,2\n", "\n", "\n", "\n", "0->2\n", "\n", "\n", "!a & !d\n", "\n", "\n", "\n", "0->2\n", "\n", "\n", "!a & d\n", "\n", "\n", "\n", "1->1\n", "\n", "\n", "!d\n", "\n", "\n", "\n", "1->1\n", "\n", "\n", "d\n", "\n", "\n", "\n", "2->2\n", "\n", "\n", "!d\n", "⓿\n", "\n", "\n", "\n", "2->2\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", ")\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", "\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", "0->0\n", "\n", "\n", "!b & !d\n", "⓿\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", "\n", "0->1\n", "\n", "\n", "b & d\n", "\n", "\n", "\n", "1->1\n", "\n", "\n", "!d\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", ")\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", "\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", "0->0\n", "\n", "\n", "!b & !d\n", "⓿\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", "\n", "0->1\n", "\n", "\n", "b & d\n", "\n", "\n", "\n", "1->1\n", "\n", "\n", "!d\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", "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", "
\n", "\n", "\n", "\n", "\n", "\n", "\n", "Inf(\n", "⓿\n", ") | Fin(\n", "⓿\n", ") | Inf(\n", "❶\n", ")\n", "[Rabin-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", ")) & 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", "\n", "Inf(\n", "⓿\n", ") | Fin(\n", "⓿\n", ") | (Inf(\n", "❶\n", ") & Fin(\n", "❶\n", "))\n", "[Rabin-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", ")) & (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", "
\n", "\n", "\n", "\n", "\n", "\n", "\n", "Inf(\n", "⓿\n", ") | (Fin(\n", "⓿\n", ")|Fin(\n", "❶\n", ")) | Inf(\n", "❶\n", ")\n", "[Rabin-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" } ], "source": [ "left = auts[5]\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": null, "metadata": {}, "outputs": [], "source": [] } ], "metadata": { "kernelspec": { "display_name": "Python 3", "language": "python", "name": "python3" }, "language_info": { "codemirror_mode": { "name": "ipython", "version": 3 }, "file_extension": ".py", "mimetype": "text/x-python", "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", "version": "3.7.4+" } }, "nbformat": 4, "nbformat_minor": 2 }