{ "cells": [ { "cell_type": "code", "execution_count": 1, "id": "found-hurricane", "metadata": {}, "outputs": [], "source": [ "import spot\n", "spot.setup()" ] }, { "cell_type": "code", "execution_count": 2, "id": "colonial-testimony", "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n", "\n", "zielonka_tree\n", "\n", "\n", "\n", "0\n", "\n", "{0,1,2,3}\n", "\n", "\n", "\n", "1\n", "\n", "{1,2,3}\n", "\n", "\n", "\n", "0->1\n", "\n", "\n", "\n", "\n", "\n", "2\n", "\n", "{0,1,3}\n", "\n", "\n", "\n", "0->2\n", "\n", "\n", "\n", "\n", "\n", "3\n", "\n", "{2,3}\n", "\n", "\n", "\n", "1->3\n", "\n", "\n", "\n", "\n", "\n", "4\n", "\n", "{1,3}\n", "\n", "\n", "\n", "1->4\n", "\n", "\n", "\n", "\n", "\n", "5\n", "\n", "{1,3}\n", "\n", "\n", "\n", "2->5\n", "\n", "\n", "\n", "\n", "\n", "6\n", "\n", "{0,1}\n", "\n", "\n", "\n", "2->6\n", "\n", "\n", "\n", "\n", "\n", "7\n", "\n", "{3}\n", "<7>\n", "\n", "\n", "\n", "3->7\n", "\n", "\n", "\n", "\n", "\n", "8\n", "\n", "{3}\n", "<8>\n", "\n", "\n", "\n", "4->8\n", "\n", "\n", "\n", "\n", "\n", "9\n", "\n", "{1}\n", "<9>\n", "\n", "\n", "\n", "4->9\n", "\n", "\n", "\n", "\n", "\n", "10\n", "\n", "{3}\n", "<10>\n", "\n", "\n", "\n", "5->10\n", "\n", "\n", "\n", "\n", "\n", "11\n", "\n", "{1}\n", "<11>\n", "\n", "\n", "\n", "5->11\n", "\n", "\n", "\n", "\n", "\n", "12\n", "\n", "{1}\n", "<12>\n", "\n", "\n", "\n", "6->12\n", "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " >" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/plain": [ "(6, 7, False, False, False)" ] }, "execution_count": 2, "metadata": {}, "output_type": "execute_result" } ], "source": [ "c = spot.acc_cond('Fin(0)&Inf(1)&(Inf(2)|Fin(3)) | (Inf(0)|Fin(1))&Fin(2)&Inf(3)')\n", "t = spot.zielonka_tree(c); display(t)\n", "t.num_branches(), t.first_branch(), t.has_rabin_shape(), t.has_streett_shape(), t.has_parity_shape()" ] }, { "cell_type": "code", "execution_count": 3, "id": "incorrect-protection", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "(7, 3)" ] }, "execution_count": 3, "metadata": {}, "output_type": "execute_result" } ], "source": [ "t.step(7, [3])" ] }, { "cell_type": "code", "execution_count": 4, "id": "rolled-command", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "(7, 2)" ] }, "execution_count": 4, "metadata": {}, "output_type": "execute_result" } ], "source": [ "t.step(7, [2])" ] }, { "cell_type": "code", "execution_count": 5, "id": "affecting-border", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "(8, 1)" ] }, "execution_count": 5, "metadata": {}, "output_type": "execute_result" } ], "source": [ "t.step(7, [1])" ] }, { "cell_type": "code", "execution_count": 6, "id": "accepting-clerk", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "(9, 2)" ] }, "execution_count": 6, "metadata": {}, "output_type": "execute_result" } ], "source": [ "t.step(8, [1])" ] }, { "cell_type": "code", "execution_count": 7, "id": "flexible-country", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "(9, 3)" ] }, "execution_count": 7, "metadata": {}, "output_type": "execute_result" } ], "source": [ "t.step(9, [1])" ] }, { "cell_type": "code", "execution_count": 8, "id": "continental-sessions", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "(8, 3)" ] }, "execution_count": 8, "metadata": {}, "output_type": "execute_result" } ], "source": [ "t.step(8, [3])" ] }, { "cell_type": "code", "execution_count": 9, "id": "expired-asian", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "(10, 0)" ] }, "execution_count": 9, "metadata": {}, "output_type": "execute_result" } ], "source": [ "t.step(8, [0])" ] }, { "cell_type": "code", "execution_count": 10, "id": "binary-republic", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "(7, 0)" ] }, "execution_count": 10, "metadata": {}, "output_type": "execute_result" } ], "source": [ "t.step(10, [0,2])" ] }, { "cell_type": "code", "execution_count": 11, "id": "starting-liechtenstein", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "(10, 0)" ] }, "execution_count": 11, "metadata": {}, "output_type": "execute_result" } ], "source": [ "t.step(7, [0,2])" ] }, { "cell_type": "code", "execution_count": 12, "id": "forced-canyon", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "(7, 4)" ] }, "execution_count": 12, "metadata": {}, "output_type": "execute_result" } ], "source": [ "t.step(7, [])" ] }, { "cell_type": "code", "execution_count": 13, "id": "floppy-chassis", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "(6, (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)) | (Fin(4) & Inf(5)))\n" ] }, { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n", "\n", "zielonka_tree\n", "\n", "\n", "\n", "0\n", "\n", "{0,1,2,3,4,5}\n", "\n", "\n", "\n", "1\n", "\n", "{1,2,3,4,5}\n", "\n", "\n", "\n", "0->1\n", "\n", "\n", "\n", "\n", "\n", "2\n", "\n", "{0,1,3,4,5}\n", "\n", "\n", "\n", "0->2\n", "\n", "\n", "\n", "\n", "\n", "3\n", "\n", "{0,1,2,3,5}\n", "\n", "\n", "\n", "0->3\n", "\n", "\n", "\n", "\n", "\n", "4\n", "\n", "{2,3,4,5}\n", "\n", "\n", "\n", "1->4\n", "\n", "\n", "\n", "\n", "\n", "5\n", "\n", "{0,1,4,5}\n", "\n", "\n", "\n", "2->5\n", "\n", "\n", "\n", "\n", "\n", "6\n", "\n", "{0,1,2,3}\n", "\n", "\n", "\n", "3->6\n", "\n", "\n", "\n", "\n", "\n", "7\n", "\n", "{3,4,5}\n", "\n", "\n", "\n", "4->7\n", "\n", "\n", "\n", "\n", "\n", "8\n", "\n", "{2,3,5}\n", "\n", "\n", "\n", "4->8\n", "\n", "\n", "\n", "\n", "\n", "9\n", "\n", "{1,4,5}\n", "\n", "\n", "\n", "5->9\n", "\n", "\n", "\n", "\n", "\n", "10\n", "\n", "{0,1,5}\n", "\n", "\n", "\n", "5->10\n", "\n", "\n", "\n", "\n", "\n", "11\n", "\n", "{1,2,3}\n", "\n", "\n", "\n", "6->11\n", "\n", "\n", "\n", "\n", "\n", "12\n", "\n", "{0,1,3}\n", "\n", "\n", "\n", "6->12\n", "\n", "\n", "\n", "\n", "\n", "13\n", "\n", "{4,5}\n", "\n", "\n", "\n", "7->13\n", "\n", "\n", "\n", "\n", "\n", "14\n", "\n", "{2,3}\n", "\n", "\n", "\n", "8->14\n", "\n", "\n", "\n", "\n", "\n", "15\n", "\n", "{4,5}\n", "\n", "\n", "\n", "9->15\n", "\n", "\n", "\n", "\n", "\n", "16\n", "\n", "{0,1}\n", "\n", "\n", "\n", "10->16\n", "\n", "\n", "\n", "\n", "\n", "17\n", "\n", "{2,3}\n", "\n", "\n", "\n", "11->17\n", "\n", "\n", "\n", "\n", "\n", "18\n", "\n", "{0,1}\n", "\n", "\n", "\n", "12->18\n", "\n", "\n", "\n", "\n", "\n", "19\n", "\n", "{5}\n", "<19>\n", "\n", "\n", "\n", "13->19\n", "\n", "\n", "\n", "\n", "\n", "20\n", "\n", "{3}\n", "<20>\n", "\n", "\n", "\n", "14->20\n", "\n", "\n", "\n", "\n", "\n", "21\n", "\n", "{5}\n", "<21>\n", "\n", "\n", "\n", "15->21\n", "\n", "\n", "\n", "\n", "\n", "22\n", "\n", "{1}\n", "<22>\n", "\n", "\n", "\n", "16->22\n", "\n", "\n", "\n", "\n", "\n", "23\n", "\n", "{3}\n", "<23>\n", "\n", "\n", "\n", "17->23\n", "\n", "\n", "\n", "\n", "\n", "24\n", "\n", "{1}\n", "<24>\n", "\n", "\n", "\n", "18->24\n", "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " >" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/plain": [ "(6, 19, True, False, False)" ] }, "execution_count": 13, "metadata": {}, "output_type": "execute_result" } ], "source": [ "c = spot.acc_cond('Rabin 3')\n", "print(c)\n", "t = spot.zielonka_tree(c)\n", "display(t)\n", "t.num_branches(), t.first_branch(), t.has_rabin_shape(), t.has_streett_shape(), t.has_parity_shape()" ] }, { "cell_type": "code", "execution_count": 14, "id": "acquired-rogers", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "(6, (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)) & (Fin(4) | Inf(5)))\n" ] }, { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n", "\n", "zielonka_tree\n", "\n", "\n", "\n", "0\n", "\n", "{0,1,2,3,4,5}\n", "\n", "\n", "\n", "1\n", "\n", "{0,2,3,4,5}\n", "\n", "\n", "\n", "0->1\n", "\n", "\n", "\n", "\n", "\n", "2\n", "\n", "{0,1,2,4,5}\n", "\n", "\n", "\n", "0->2\n", "\n", "\n", "\n", "\n", "\n", "3\n", "\n", "{0,1,2,3,4}\n", "\n", "\n", "\n", "0->3\n", "\n", "\n", "\n", "\n", "\n", "4\n", "\n", "{2,3,4,5}\n", "\n", "\n", "\n", "1->4\n", "\n", "\n", "\n", "\n", "\n", "5\n", "\n", "{0,1,4,5}\n", "\n", "\n", "\n", "2->5\n", "\n", "\n", "\n", "\n", "\n", "6\n", "\n", "{0,1,2,3}\n", "\n", "\n", "\n", "3->6\n", "\n", "\n", "\n", "\n", "\n", "7\n", "\n", "{2,4,5}\n", "\n", "\n", "\n", "4->7\n", "\n", "\n", "\n", "\n", "\n", "8\n", "\n", "{2,3,4}\n", "\n", "\n", "\n", "4->8\n", "\n", "\n", "\n", "\n", "\n", "9\n", "\n", "{0,4,5}\n", "\n", "\n", "\n", "5->9\n", "\n", "\n", "\n", "\n", "\n", "10\n", "\n", "{0,1,4}\n", "\n", "\n", "\n", "5->10\n", "\n", "\n", "\n", "\n", "\n", "11\n", "\n", "{0,2,3}\n", "\n", "\n", "\n", "6->11\n", "\n", "\n", "\n", "\n", "\n", "12\n", "\n", "{0,1,2}\n", "\n", "\n", "\n", "6->12\n", "\n", "\n", "\n", "\n", "\n", "13\n", "\n", "{4,5}\n", "\n", "\n", "\n", "7->13\n", "\n", "\n", "\n", "\n", "\n", "14\n", "\n", "{2,3}\n", "\n", "\n", "\n", "8->14\n", "\n", "\n", "\n", "\n", "\n", "15\n", "\n", "{4,5}\n", "\n", "\n", "\n", "9->15\n", "\n", "\n", "\n", "\n", "\n", "16\n", "\n", "{0,1}\n", "\n", "\n", "\n", "10->16\n", "\n", "\n", "\n", "\n", "\n", "17\n", "\n", "{2,3}\n", "\n", "\n", "\n", "11->17\n", "\n", "\n", "\n", "\n", "\n", "18\n", "\n", "{0,1}\n", "\n", "\n", "\n", "12->18\n", "\n", "\n", "\n", "\n", "\n", "19\n", "\n", "{4}\n", "<19>\n", "\n", "\n", "\n", "13->19\n", "\n", "\n", "\n", "\n", "\n", "20\n", "\n", "{2}\n", "<20>\n", "\n", "\n", "\n", "14->20\n", "\n", "\n", "\n", "\n", "\n", "21\n", "\n", "{4}\n", "<21>\n", "\n", "\n", "\n", "15->21\n", "\n", "\n", "\n", "\n", "\n", "22\n", "\n", "{0}\n", "<22>\n", "\n", "\n", "\n", "16->22\n", "\n", "\n", "\n", "\n", "\n", "23\n", "\n", "{2}\n", "<23>\n", "\n", "\n", "\n", "17->23\n", "\n", "\n", "\n", "\n", "\n", "24\n", "\n", "{0}\n", "<24>\n", "\n", "\n", "\n", "18->24\n", "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " >" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/plain": [ "(6, 19, False, True, False)" ] }, "execution_count": 14, "metadata": {}, "output_type": "execute_result" } ], "source": [ "c = spot.acc_cond('Streett 3')\n", "print(c)\n", "t = spot.zielonka_tree(c)\n", "display(t)\n", "t.num_branches(), t.first_branch(), t.has_rabin_shape(), t.has_streett_shape(), t.has_parity_shape()" ] }, { "cell_type": "code", "execution_count": 15, "id": "minimal-douglas", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "(5, (Inf(0) & Fin(1)) | (Inf(2) & Fin(3) & Fin(4)))\n" ] }, { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n", "\n", "zielonka_tree\n", "\n", "\n", "\n", "0\n", "\n", "{0,1,2,3,4}\n", "\n", "\n", "\n", "1\n", "\n", "{0,2,3,4}\n", "\n", "\n", "\n", "0->1\n", "\n", "\n", "\n", "\n", "\n", "2\n", "\n", "{0,1,2}\n", "\n", "\n", "\n", "0->2\n", "\n", "\n", "\n", "\n", "\n", "3\n", "\n", "{2,3,4}\n", "\n", "\n", "\n", "1->3\n", "\n", "\n", "\n", "\n", "\n", "4\n", "\n", "{0,1}\n", "\n", "\n", "\n", "2->4\n", "\n", "\n", "\n", "\n", "\n", "5\n", "\n", "{2}\n", "<5>\n", "\n", "\n", "\n", "3->5\n", "\n", "\n", "\n", "\n", "\n", "6\n", "\n", "{0}\n", "<6>\n", "\n", "\n", "\n", "4->6\n", "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " >" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/plain": [ "(2, 5, True, False, False)" ] }, "execution_count": 15, "metadata": {}, "output_type": "execute_result" } ], "source": [ "c = spot.acc_cond('Inf(0)&Fin(1) | (Inf(2)&Fin(3)&Fin(4))')\n", "print(c)\n", "t = spot.zielonka_tree(c)\n", "display(t)\n", "t.num_branches(), t.first_branch(), t.has_rabin_shape(), t.has_streett_shape(), t.has_parity_shape()" ] }, { "cell_type": "code", "execution_count": 16, "id": "tired-thumbnail", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "(5, Fin(4) & (Inf(3) | (Fin(2) & (Inf(1) | Fin(0)))))\n" ] }, { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n", "\n", "zielonka_tree\n", "\n", "\n", "\n", "0\n", "\n", "{0,1,2,3,4}\n", "\n", "\n", "\n", "1\n", "\n", "{0,1,2,3}\n", "\n", "\n", "\n", "0->1\n", "\n", "\n", "\n", "\n", "\n", "2\n", "\n", "{0,1,2}\n", "\n", "\n", "\n", "1->2\n", "\n", "\n", "\n", "\n", "\n", "3\n", "\n", "{0,1}\n", "\n", "\n", "\n", "2->3\n", "\n", "\n", "\n", "\n", "\n", "4\n", "\n", "{0}\n", "<4>\n", "\n", "\n", "\n", "3->4\n", "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " >" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/plain": [ "(1, 4, True, True, True)" ] }, "execution_count": 16, "metadata": {}, "output_type": "execute_result" } ], "source": [ "c = spot.acc_cond('parity max odd 5')\n", "print(c)\n", "t = spot.zielonka_tree(c)\n", "display(t)\n", "t.num_branches(), t.first_branch(), t.has_rabin_shape(), t.has_streett_shape(), t.has_parity_shape()" ] }, { "cell_type": "code", "execution_count": 17, "id": "structured-palace", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "(0, f)\n" ] }, { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n", "\n", "zielonka_tree\n", "\n", "\n", "\n", "0\n", "\n", "{}\n", "<0>\n", "\n", "\n", "\n" ], "text/plain": [ " >" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/plain": [ "(1, 0, True, True, True)" ] }, "execution_count": 17, "metadata": {}, "output_type": "execute_result" } ], "source": [ "c = spot.acc_cond('f')\n", "print(c)\n", "t = spot.zielonka_tree(c)\n", "display(t)\n", "t.num_branches(), t.first_branch(), t.has_rabin_shape(), t.has_streett_shape(), t.has_parity_shape()" ] }, { "cell_type": "code", "execution_count": 18, "id": "plain-modern", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "(0, t)\n" ] }, { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n", "\n", "zielonka_tree\n", "\n", "\n", "\n", "0\n", "\n", "{}\n", "<0>\n", "\n", "\n", "\n" ], "text/plain": [ " >" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/plain": [ "(1, 0, True, True, True)" ] }, "execution_count": 18, "metadata": {}, "output_type": "execute_result" } ], "source": [ "c = spot.acc_cond('t')\n", "print(c)\n", "t = spot.zielonka_tree(c)\n", "display(t)\n", "t.num_branches(), t.first_branch(), t.has_rabin_shape(), t.has_streett_shape(), t.has_parity_shape()" ] }, { "cell_type": "code", "execution_count": 19, "id": "interesting-seller", "metadata": {}, "outputs": [], "source": [ "a = spot.automaton(\"\"\"HOA: v1 name: \"(FGp0 & ((XFp0 & F!p1) | F(Gp1 &\n", "XG!p0))) | G(F!p0 & (XFp0 | F!p1) & F(Gp1 | G!p0))\" States: 14 Start:\n", "0 AP: 2 \"p1\" \"p0\" Acceptance: 6 (Fin(0) & Fin(1)) | ((Fin(4)|Fin(5)) &\n", "(Inf(2)&Inf(3))) properties: trans-labels explicit-labels trans-acc\n", "complete properties: deterministic --BODY-- State: 0 [!0] 1 [0] 2\n", "State: 1 [!0&!1] 1 {0 1 2 3 5} [0&!1] 3 [!0&1] 4 [0&1] 5 State: 2\n", "[0&!1] 2 {1} [!0&1] 4 [!0&!1] 6 [0&1] 7 State: 3 [0&!1] 3 {1 3} [!0&1]\n", "4 [!0&!1] 6 {0 1 2 3 5} [0&1] 8 State: 4 [!0&!1] 4 {1 2 3 5} [!0&1] 4\n", "{2 4 5} [0&!1] 5 {1 3} [0&1] 5 {4} State: 5 [!0&1] 4 {2 4 5} [0&!1] 5\n", "{1 3} [0&1] 8 {2 4} [!0&!1] 9 {1 2 3 5} State: 6 [0&!1] 3 {1 3} [!0&1]\n", "4 [0&1] 5 [!0&!1] 10 State: 7 [!0&1] 4 [0&!1] 7 {1 3} [!0&!1] 11 [0&1]\n", "12 {0 4} State: 8 [!0&1] 4 {2 4 5} [0&1] 5 {4} [0&!1] 8 {1 3} [!0&!1]\n", "11 {1 3 5} State: 9 [!0&1] 4 {2 4 5} [0&!1] 5 {1 3} [0&1] 5 {4}\n", "[!0&!1] 11 {1 3 5} State: 10 [!0&1] 4 [0&1] 8 [!0&!1] 10 {0 1 2 3 5}\n", "[0&!1] 13 {1 2 3} State: 11 [!0&1] 4 {2 4 5} [0&!1] 8 {1 2 3} [0&1] 8\n", "{2 4} [!0&!1] 11 {1 2 3 5} State: 12 [!0&1] 4 [0&1] 7 {0 2 4} [!0&!1]\n", "9 [0&!1] 12 {1 3} State: 13 [!0&1] 4 [0&1] 5 [!0&!1] 10 {0 1 3 5}\n", "[0&!1] 13 {1 3} --END--\"\"\")" ] }, { "cell_type": "code", "execution_count": 20, "id": "informative-mainland", "metadata": {}, "outputs": [], "source": [ "b = spot.zielonka_tree_transform(a)" ] }, { "cell_type": "code", "execution_count": 21, "id": "angry-comedy", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "33" ] }, "execution_count": 21, "metadata": {}, "output_type": "execute_result" } ], "source": [ "b.num_states()" ] }, { "cell_type": "code", "execution_count": 22, "id": "contained-combat", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "True" ] }, "execution_count": 22, "metadata": {}, "output_type": "execute_result" } ], "source": [ "a.equivalent_to(b)" ] }, { "cell_type": "code", "execution_count": 23, "id": "paperback-handle", "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n", "\n", "\n", "(Fin(\n", "⓿\n", ") & (Fin(\n", "❸\n", ")|Fin(\n", "❹\n", ")) & (Inf(\n", "❶\n", ")&Inf(\n", "❷\n", "))) | Inf(\n", "❸\n", ")\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", "!p0 & p1\n", "❷\n", "❸\n", "\n", "\n", "\n", "0->0\n", "\n", "\n", "!p0 & !p1\n", "❷\n", "❸\n", "❹\n", "\n", "\n", "\n", "1\n", "\n", "1\n", "\n", "\n", "\n", "0->1\n", "\n", "\n", "p0 & !p1\n", "\n", "\n", "\n", "0->1\n", "\n", "\n", "p0 & p1\n", "❷\n", "❹\n", "\n", "\n", "\n", "1->0\n", "\n", "\n", "!p0 & !p1\n", "⓿\n", "❷\n", "❸\n", "❹\n", "\n", "\n", "\n", "1->1\n", "\n", "\n", "p0 & !p1\n", "❶\n", "\n", "\n", "\n", "1->1\n", "\n", "\n", "!p0 & p1\n", "❷\n", "❸\n", "\n", "\n", "\n", "1->1\n", "\n", "\n", "p0 & p1\n", "❶\n", "❷\n", "❹\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7efe6a34b960> >" ] }, "execution_count": 23, "metadata": {}, "output_type": "execute_result" } ], "source": [ "c = spot.automaton(\"\"\"\n", "HOA: v1\n", "States: 2\n", "Start: 0\n", "AP: 2 \"p1\" \"p0\"\n", "Acceptance: 5 (Fin(0) & (Fin(3)|Fin(4)) & (Inf(1)&Inf(2))) | Inf(3)\n", "properties: trans-labels explicit-labels trans-acc complete\n", "properties: deterministic stutter-invariant\n", "--BODY--\n", "State: 0\n", "[0&!1] 0 {2 3}\n", "[!0&!1] 0 {2 3 4}\n", "[!0&1] 1\n", "[0&1] 1 {2 4}\n", "State: 1\n", "[!0&!1] 0 {0 2 3 4}\n", "[!0&1] 1 {1}\n", "[0&!1] 1 {2 3}\n", "[0&1] 1 {1 2 4}\n", "--END--\n", "\"\"\"); c" ] }, { "cell_type": "code", "execution_count": 24, "id": "tired-webcam", "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n", "\n", "\n", "Inf(\n", "⓿\n", ") | (Fin(\n", "❶\n", ") & (Inf(\n", "❷\n", ") | (Fin(\n", "❸\n", ") & Inf(\n", "❹\n", "))))\n", "[parity min even 5]\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", "!p0 & p1\n", "⓿\n", "\n", "\n", "\n", "0->0\n", "\n", "\n", "!p0 & !p1\n", "⓿\n", "\n", "\n", "\n", "1\n", "\n", "1\n", "\n", "\n", "\n", "0->1\n", "\n", "\n", "p0 & !p1\n", "❹\n", "\n", "\n", "\n", "0->1\n", "\n", "\n", "p0 & p1\n", "❸\n", "\n", "\n", "\n", "1->0\n", "\n", "\n", "!p0 & !p1\n", "⓿\n", "\n", "\n", "\n", "1->1\n", "\n", "\n", "!p0 & p1\n", "⓿\n", "\n", "\n", "\n", "2\n", "\n", "2\n", "\n", "\n", "\n", "1->2\n", "\n", "\n", "p0 & !p1\n", "❷\n", "\n", "\n", "\n", "1->2\n", "\n", "\n", "p0 & p1\n", "❷\n", "\n", "\n", "\n", "2->0\n", "\n", "\n", "!p0 & !p1\n", "⓿\n", "\n", "\n", "\n", "2->1\n", "\n", "\n", "!p0 & p1\n", "⓿\n", "\n", "\n", "\n", "2->1\n", "\n", "\n", "p0 & p1\n", "❷\n", "\n", "\n", "\n", "2->2\n", "\n", "\n", "p0 & !p1\n", "❸\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7efe6a34b540> >" ] }, "execution_count": 24, "metadata": {}, "output_type": "execute_result" } ], "source": [ "d = spot.zielonka_tree_transform(c); d" ] }, { "cell_type": "code", "execution_count": 25, "id": "funny-taylor", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "True" ] }, "execution_count": 25, "metadata": {}, "output_type": "execute_result" } ], "source": [ "c.equivalent_to(d)" ] }, { "cell_type": "code", "execution_count": 26, "id": "liable-update", "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n", "\n", "\n", "Inf(\n", "⓿\n", ") & (Fin(\n", "❶\n", ")|Fin(\n", "❷\n", "))\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", "!a & !b\n", "❷\n", "\n", "\n", "\n", "0->0\n", "\n", "\n", "a & !b\n", "⓿\n", "❷\n", "\n", "\n", "\n", "1\n", "\n", "1\n", "\n", "\n", "\n", "0->1\n", "\n", "\n", "!a & b\n", "❶\n", "\n", "\n", "\n", "0->1\n", "\n", "\n", "a & b\n", "⓿\n", "❶\n", "\n", "\n", "\n", "1->0\n", "\n", "\n", "!a & !b\n", "\n", "\n", "\n", "1->0\n", "\n", "\n", "a & !b\n", "⓿\n", "\n", "\n", "\n", "1->1\n", "\n", "\n", "!a & b\n", "❶\n", "\n", "\n", "\n", "1->1\n", "\n", "\n", "a & b\n", "⓿\n", "❶\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7efe6a301ed0> >" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n", "\n", "\n", "Fin(\n", "⓿\n", ") & (Inf(\n", "❶\n", ") | (Fin(\n", "❷\n", ") & Inf(\n", "❸\n", ")))\n", "[parity min odd 4]\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", "!a & !b\n", "❷\n", "\n", "\n", "\n", "0->0\n", "\n", "\n", "a & !b\n", "❶\n", "\n", "\n", "\n", "1\n", "\n", "1\n", "\n", "\n", "\n", "0->1\n", "\n", "\n", "!a & b\n", "⓿\n", "\n", "\n", "\n", "0->1\n", "\n", "\n", "a & b\n", "⓿\n", "\n", "\n", "\n", "1->1\n", "\n", "\n", "!a & b\n", "❷\n", "\n", "\n", "\n", "1->1\n", "\n", "\n", "a & b\n", "❶\n", "\n", "\n", "\n", "2\n", "\n", "2\n", "\n", "\n", "\n", "1->2\n", "\n", "\n", "!a & !b\n", "❸\n", "\n", "\n", "\n", "1->2\n", "\n", "\n", "a & !b\n", "❶\n", "\n", "\n", "\n", "2->0\n", "\n", "\n", "!a & !b\n", "⓿\n", "\n", "\n", "\n", "2->0\n", "\n", "\n", "a & !b\n", "⓿\n", "\n", "\n", "\n", "2->1\n", "\n", "\n", "!a & b\n", "❷\n", "\n", "\n", "\n", "2->1\n", "\n", "\n", "a & b\n", "❶\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7efe6a301720> >" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "e = spot.translate('!(GFa -> (GFb & GF(!b & !Xb)))', 'gen', 'det')\n", "f = spot.zielonka_tree_transform(e)\n", "display(e,f)" ] }, { "cell_type": "code", "execution_count": 27, "id": "complimentary-person", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "True" ] }, "execution_count": 27, "metadata": {}, "output_type": "execute_result" } ], "source": [ "e.equivalent_to(f)" ] }, { "cell_type": "code", "execution_count": null, "id": "determined-bankruptcy", "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.9.2" } }, "nbformat": 4, "nbformat_minor": 5 }