From dd587476593a8b179d1fafaf24d7dfccf517e355 Mon Sep 17 00:00:00 2001 From: Florian Renkin Date: Mon, 21 Mar 2022 13:56:50 +0100 Subject: [PATCH] synthesis.ipynb: remove useless import * tests/python/synthesis.ipynb: here. --- tests/python/synthesis.ipynb | 3589 +++++++++++++++++----------------- 1 file changed, 1778 insertions(+), 1811 deletions(-) diff --git a/tests/python/synthesis.ipynb b/tests/python/synthesis.ipynb index 47cafbf41..3738e6f72 100644 --- a/tests/python/synthesis.ipynb +++ b/tests/python/synthesis.ipynb @@ -3,19 +3,16 @@ { "cell_type": "code", "execution_count": 1, - "id": "1b9b5964", "metadata": {}, "outputs": [], "source": [ "import spot\n", "spot.setup()\n", - "from spot.jupyter import display_inline\n", - "import time" + "from spot.jupyter import display_inline" ] }, { "cell_type": "markdown", - "id": "b465c6ba", "metadata": {}, "source": [ "This notebook presents functions that can be used to solve the Reactive Synthesis problem using games.\n", @@ -40,7 +37,6 @@ { "cell_type": "code", "execution_count": 2, - "id": "8576bdad", "metadata": {}, "outputs": [ { @@ -57,647 +53,647 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "Fin(\n", - "\n", - ") & (Inf(\n", - "\n", - ") | Fin(\n", - "\n", - "))\n", - "[parity max odd 3]\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ") & (Inf(\n", + "\n", + ") | Fin(\n", + "\n", + "))\n", + "[parity max odd 3]\n", "\n", "\n", "\n", "9\n", - "\n", - "9\n", + "\n", + "9\n", "\n", "\n", "\n", "I->9\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "25\n", - "\n", - "25\n", + "\n", + "25\n", "\n", "\n", "\n", "9->25\n", - "\n", - "\n", - "!i0 & !i1\n", - "\n", + "\n", + "\n", + "!i0 & !i1\n", + "\n", "\n", "\n", "\n", "26\n", - "\n", - "26\n", + "\n", + "26\n", "\n", "\n", "\n", "9->26\n", - "\n", - "\n", - "i0 & !i1\n", - "\n", + "\n", + "\n", + "i0 & !i1\n", + "\n", "\n", "\n", "\n", "27\n", - "\n", - "27\n", + "\n", + "27\n", "\n", "\n", "\n", "9->27\n", - "\n", - "\n", - "!i0 & i1\n", - "\n", + "\n", + "\n", + "!i0 & i1\n", + "\n", "\n", "\n", "\n", "28\n", - "\n", - "28\n", + "\n", + "28\n", "\n", "\n", "\n", "9->28\n", - "\n", - "\n", - "i0 & i1\n", - "\n", + "\n", + "\n", + "i0 & i1\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "10\n", - "\n", - "10\n", + "\n", + "10\n", "\n", "\n", "\n", "0->10\n", - "\n", - "\n", - "!i1\n", - "\n", + "\n", + "\n", + "!i1\n", + "\n", "\n", "\n", "\n", "11\n", - "\n", - "11\n", + "\n", + "11\n", "\n", "\n", "\n", "0->11\n", - "\n", - "\n", - "i1\n", - "\n", + "\n", + "\n", + "i1\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "10->1\n", - "\n", - "\n", - "o0\n", - "\n", + "\n", + "\n", + "o0\n", + "\n", "\n", "\n", "\n", "11->0\n", - "\n", - "\n", - "o0\n", - "\n", + "\n", + "\n", + "o0\n", + "\n", "\n", "\n", "\n", "12\n", - "\n", - "12\n", + "\n", + "12\n", "\n", "\n", "\n", "1->12\n", - "\n", - "\n", - "!i1\n", - "\n", + "\n", + "\n", + "!i1\n", + "\n", "\n", "\n", "\n", "13\n", - "\n", - "13\n", + "\n", + "13\n", "\n", "\n", "\n", "1->13\n", - "\n", - "\n", - "i1\n", - "\n", + "\n", + "\n", + "i1\n", + "\n", "\n", "\n", "\n", "12->1\n", - "\n", - "\n", - "!o0\n", - "\n", + "\n", + "\n", + "!o0\n", + "\n", "\n", "\n", "\n", "13->0\n", - "\n", - "\n", - "!o0\n", - "\n", + "\n", + "\n", + "!o0\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "14\n", - "\n", - "14\n", + "\n", + "14\n", "\n", "\n", "\n", "2->14\n", - "\n", - "\n", - "i1\n", - "\n", + "\n", + "\n", + "i1\n", + "\n", "\n", "\n", "\n", "16\n", - "\n", - "16\n", + "\n", + "16\n", "\n", "\n", "\n", "2->16\n", - "\n", - "\n", - "!i1\n", - "\n", + "\n", + "\n", + "!i1\n", + "\n", "\n", "\n", "\n", "15\n", - "\n", - "15\n", + "\n", + "15\n", "\n", "\n", "\n", "14->15\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "16->2\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "3->13\n", - "\n", - "\n", - "i1\n", - "\n", + "\n", + "\n", + "i1\n", + "\n", "\n", "\n", "\n", "17\n", - "\n", - "17\n", + "\n", + "17\n", "\n", "\n", "\n", "3->17\n", - "\n", - "\n", - "!i1\n", - "\n", + "\n", + "\n", + "!i1\n", + "\n", "\n", "\n", "\n", "17->2\n", - "\n", - "\n", - "o0\n", - "\n", + "\n", + "\n", + "o0\n", + "\n", "\n", "\n", "\n", "17->3\n", - "\n", - "\n", - "!o0\n", - "\n", + "\n", + "\n", + "!o0\n", + "\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "4->14\n", - "\n", - "\n", - "i0\n", - "\n", + "\n", + "\n", + "i0\n", + "\n", "\n", "\n", "\n", "18\n", - "\n", - "18\n", + "\n", + "18\n", "\n", "\n", "\n", "4->18\n", - "\n", - "\n", - "!i0\n", - "\n", + "\n", + "\n", + "!i0\n", + "\n", "\n", "\n", "\n", "18->4\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "5->14\n", - "\n", - "\n", - "i0 & i1\n", - "\n", + "\n", + "\n", + "i0 & i1\n", + "\n", "\n", "\n", "\n", "5->16\n", - "\n", - "\n", - "i0 & !i1\n", - "\n", + "\n", + "\n", + "i0 & !i1\n", + "\n", "\n", "\n", "\n", "5->18\n", - "\n", - "\n", - "!i0 & i1\n", - "\n", + "\n", + "\n", + "!i0 & i1\n", + "\n", "\n", "\n", "\n", "19\n", - "\n", - "19\n", + "\n", + "19\n", "\n", "\n", "\n", "5->19\n", - "\n", - "\n", - "!i0 & !i1\n", - "\n", + "\n", + "\n", + "!i0 & !i1\n", + "\n", "\n", "\n", "\n", "19->5\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "6->10\n", - "\n", - "\n", - "i0 & !i1\n", - "\n", + "\n", + "\n", + "i0 & !i1\n", + "\n", "\n", "\n", "\n", "6->11\n", - "\n", - "\n", - "i0 & i1\n", - "\n", + "\n", + "\n", + "i0 & i1\n", + "\n", "\n", "\n", "\n", "20\n", - "\n", - "20\n", + "\n", + "20\n", "\n", "\n", "\n", "6->20\n", - "\n", - "\n", - "!i0 & !i1\n", - "\n", + "\n", + "\n", + "!i0 & !i1\n", + "\n", "\n", "\n", "\n", "21\n", - "\n", - "21\n", + "\n", + "21\n", "\n", "\n", "\n", "6->21\n", - "\n", - "\n", - "!i0 & i1\n", - "\n", + "\n", + "\n", + "!i0 & i1\n", + "\n", "\n", "\n", "\n", "20->4\n", - "\n", - "\n", - "!o0\n", - "\n", + "\n", + "\n", + "!o0\n", + "\n", "\n", "\n", "\n", "7\n", - "\n", - "7\n", + "\n", + "7\n", "\n", "\n", "\n", "20->7\n", - "\n", - "\n", - "o0\n", - "\n", + "\n", + "\n", + "o0\n", + "\n", "\n", "\n", "\n", "21->4\n", - "\n", - "\n", - "!o0\n", - "\n", + "\n", + "\n", + "!o0\n", + "\n", "\n", "\n", "\n", "21->6\n", - "\n", - "\n", - "o0\n", - "\n", + "\n", + "\n", + "o0\n", + "\n", "\n", "\n", "\n", "7->12\n", - "\n", - "\n", - "i0 & !i1\n", - "\n", + "\n", + "\n", + "i0 & !i1\n", + "\n", "\n", "\n", "\n", "7->13\n", - "\n", - "\n", - "i0 & i1\n", - "\n", + "\n", + "\n", + "i0 & i1\n", + "\n", "\n", "\n", "\n", "22\n", - "\n", - "22\n", + "\n", + "22\n", "\n", "\n", "\n", "7->22\n", - "\n", - "\n", - "!i0 & !i1\n", - "\n", + "\n", + "\n", + "!i0 & !i1\n", + "\n", "\n", "\n", "\n", "23\n", - "\n", - "23\n", + "\n", + "23\n", "\n", "\n", "\n", "7->23\n", - "\n", - "\n", - "!i0 & i1\n", - "\n", + "\n", + "\n", + "!i0 & i1\n", + "\n", "\n", "\n", "\n", "22->4\n", - "\n", - "\n", - "o0\n", - "\n", + "\n", + "\n", + "o0\n", + "\n", "\n", "\n", "\n", "22->7\n", - "\n", - "\n", - "!o0\n", - "\n", + "\n", + "\n", + "!o0\n", + "\n", "\n", "\n", "\n", "23->4\n", - "\n", - "\n", - "o0\n", - "\n", + "\n", + "\n", + "o0\n", + "\n", "\n", "\n", "\n", "23->6\n", - "\n", - "\n", - "!o0\n", - "\n", + "\n", + "\n", + "!o0\n", + "\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "8->13\n", - "\n", - "\n", - "i0 & i1\n", - "\n", + "\n", + "\n", + "i0 & i1\n", + "\n", "\n", "\n", "\n", "8->17\n", - "\n", - "\n", - "i0 & !i1\n", - "\n", + "\n", + "\n", + "i0 & !i1\n", + "\n", "\n", "\n", "\n", "8->23\n", - "\n", - "\n", - "!i0 & i1\n", - "\n", + "\n", + "\n", + "!i0 & i1\n", + "\n", "\n", "\n", "\n", "24\n", - "\n", - "24\n", + "\n", + "24\n", "\n", "\n", "\n", "8->24\n", - "\n", - "\n", - "!i0 & !i1\n", - "\n", + "\n", + "\n", + "!i0 & !i1\n", + "\n", "\n", "\n", "\n", "24->5\n", - "\n", - "\n", - "o0\n", - "\n", + "\n", + "\n", + "o0\n", + "\n", "\n", "\n", "\n", "24->8\n", - "\n", - "\n", - "!o0\n", - "\n", + "\n", + "\n", + "!o0\n", + "\n", "\n", "\n", "\n", "25->8\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "26->3\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "27->6\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "28->0\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "15->14\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f7a0c2640c0> >" + " *' at 0x7fb964737d50> >" ] }, "metadata": {}, @@ -716,7 +712,6 @@ }, { "cell_type": "markdown", - "id": "fbd7095b", "metadata": {}, "source": [ "Solving the game, is done with `solve_game()` as with any game. There is also a version that takes a `synthesis_info` as second argument in case the time it takes has to be recorded. Here passing `si` or not makes no difference." @@ -725,7 +720,6 @@ { "cell_type": "code", "execution_count": 3, - "id": "02d7525e", "metadata": {}, "outputs": [ { @@ -741,586 +735,586 @@ "\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", - "Fin(\n", - "\n", - ") & (Inf(\n", - "\n", - ") | Fin(\n", - "\n", - "))\n", - "[parity max odd 3]\n", + " viewBox=\"0.00 0.00 650.40 360.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", + "\n", + "\n", + "Fin(\n", + "\n", + ") & (Inf(\n", + "\n", + ") | Fin(\n", + "\n", + "))\n", + "[parity max odd 3]\n", "\n", "\n", "\n", "9\n", - "\n", - "9\n", + "\n", + "9\n", "\n", "\n", "\n", "I->9\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "25\n", - "\n", - "25\n", + "\n", + "25\n", "\n", "\n", "\n", "9->25\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "26\n", - "\n", - "26\n", + "\n", + "26\n", "\n", "\n", "\n", "9->26\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "27\n", - "\n", - "27\n", + "\n", + "27\n", "\n", "\n", "\n", "9->27\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "28\n", - "\n", - "28\n", + "\n", + "28\n", "\n", "\n", "\n", "9->28\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "10\n", - "\n", - "10\n", + "\n", + "10\n", "\n", "\n", "\n", "0->10\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "11\n", - "\n", - "11\n", + "\n", + "11\n", "\n", "\n", "\n", "0->11\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "10->1\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "11->0\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "12\n", - "\n", - "12\n", + "\n", + "12\n", "\n", "\n", "\n", "1->12\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "13\n", - "\n", - "13\n", + "\n", + "13\n", "\n", "\n", "\n", "1->13\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "12->1\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "13->0\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "14\n", - "\n", - "14\n", + "\n", + "14\n", "\n", "\n", "\n", "2->14\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "16\n", - "\n", - "16\n", + "\n", + "16\n", "\n", "\n", "\n", "2->16\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "15\n", - "\n", - "15\n", + "\n", + "15\n", "\n", "\n", "\n", "14->15\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "16->2\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "3->13\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "17\n", - "\n", - "17\n", + "\n", + "17\n", "\n", "\n", "\n", "3->17\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "17->2\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "17->3\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "4->14\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "18\n", - "\n", - "18\n", + "\n", + "18\n", "\n", "\n", "\n", "4->18\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "18->4\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "5->14\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "5->16\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "5->18\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "19\n", - "\n", - "19\n", + "\n", + "19\n", "\n", "\n", "\n", "5->19\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "19->5\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "6->10\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "6->11\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "20\n", - "\n", - "20\n", + "\n", + "20\n", "\n", "\n", "\n", "6->20\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "21\n", - "\n", - "21\n", + "\n", + "21\n", "\n", "\n", "\n", "6->21\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "20->4\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "7\n", - "\n", - "7\n", + "\n", + "7\n", "\n", "\n", "\n", "20->7\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "21->4\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "21->6\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "7->12\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "7->13\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "22\n", - "\n", - "22\n", + "\n", + "22\n", "\n", "\n", "\n", "7->22\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "23\n", - "\n", - "23\n", + "\n", + "23\n", "\n", "\n", "\n", "7->23\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "22->4\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "22->7\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "23->4\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "23->6\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "8->13\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "8->17\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "8->23\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "24\n", - "\n", - "24\n", + "\n", + "24\n", "\n", "\n", "\n", "8->24\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "24->5\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "24->8\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "25->8\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "26->3\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "27->6\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "28->0\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "15->14\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n" @@ -1342,7 +1336,6 @@ }, { "cell_type": "markdown", - "id": "d66f3da1", "metadata": {}, "source": [ "Once a strategy has been found, it can be extracted as an automaton and simplified using 6 different levels (the default is 2). The output should be interpreted as a Mealy automaton, where transition have the form `(ins)&(outs)` where `ins` and `outs` are Boolean formulas representing possible inputs and outputs (they could be more than just conjunctions of atomic proposition). Mealy machines with this type of labels are called \"separated\" in Spot." @@ -1351,7 +1344,6 @@ { "cell_type": "code", "execution_count": 4, - "id": "89342e18", "metadata": {}, "outputs": [ { @@ -1367,309 +1359,309 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "\n", - "!i0 & !i1\n", - "/\n", - "\n", - "1\n", + "\n", + "\n", + "\n", + "!i0 & !i1\n", + "/\n", + "\n", + "1\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "\n", - "i0 & !i1\n", - "/\n", - "\n", - "1\n", + "\n", + "\n", + "\n", + "i0 & !i1\n", + "/\n", + "\n", + "1\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "\n", - "!i0 & i1\n", - "/\n", - "\n", - "1\n", + "\n", + "\n", + "\n", + "!i0 & i1\n", + "/\n", + "\n", + "1\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "0->4\n", - "\n", - "\n", - "\n", - "i0 & i1\n", - "/\n", - "\n", - "1\n", + "\n", + "\n", + "\n", + "i0 & i1\n", + "/\n", + "\n", + "1\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "\n", - "!i0 & !i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i0 & !i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "\n", - "i0 & !i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i0 & !i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "\n", - "!i0 & i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i0 & i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "1->4\n", - "\n", - "\n", - "\n", - "i0 & i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i0 & i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "\n", - "!i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "2->4\n", - "\n", - "\n", - "\n", - "i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "\n", - "!i0 & i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "!i0 & i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "3->4\n", - "\n", - "\n", - "\n", - "i0 & i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "i0 & i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "3->5\n", - "\n", - "\n", - "\n", - "i0 & !i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "i0 & !i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "3->6\n", - "\n", - "\n", - "\n", - "!i0 & !i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "!i0 & !i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "\n", - "i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "4->5\n", - "\n", - "\n", - "\n", - "!i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "!i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "5->4\n", - "\n", - "\n", - "\n", - "i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "5->5\n", - "\n", - "\n", - "\n", - "!i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "6->3\n", - "\n", - "\n", - "\n", - "!i0 & i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i0 & i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "6->4\n", - "\n", - "\n", - "\n", - "i0 & i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i0 & i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "6->5\n", - "\n", - "\n", - "\n", - "i0 & !i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i0 & !i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "6->6\n", - "\n", - "\n", - "\n", - "!i0 & !i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i0 & !i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f7a0c264e40> >" + " *' at 0x7fb9646b7870> >" ] }, "metadata": {}, @@ -1688,175 +1680,175 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "\n", - "!i0 & !i1\n", - "/\n", - "\n", - "1\n", + "\n", + "\n", + "\n", + "!i0 & !i1\n", + "/\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "\n", - "i0 & !i1\n", - "/\n", - "\n", - "1\n", + "\n", + "\n", + "\n", + "i0 & !i1\n", + "/\n", + "\n", + "1\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "\n", - "!i0 & i1\n", - "/\n", - "\n", - "1\n", + "\n", + "\n", + "\n", + "!i0 & i1\n", + "/\n", + "\n", + "1\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "\n", - "i0 & i1\n", - "/\n", - "\n", - "1\n", + "\n", + "\n", + "\n", + "i0 & i1\n", + "/\n", + "\n", + "1\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "\n", - "i0 & !i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i0 & !i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "\n", - "!i0 & !i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i0 & !i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "\n", - "i0 & i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i0 & i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "\n", - "!i0 & i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i0 & i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "\n", - "i0 & !i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "i0 & !i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "\n", - "!i0 & !i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "!i0 & !i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "\n", - "i0 & i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "i0 & i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "\n", - "!i0 & i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "!i0 & i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f7a0c264d50> >" + " *' at 0x7fb9646b7de0> >" ] }, "metadata": {}, @@ -1875,125 +1867,125 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "I->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "\n", - "i0 & i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "i0 & i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "\n", - "!i0 & i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "!i0 & i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "\n", - "i0 & !i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "i0 & !i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "\n", - "!i0 & !i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "!i0 & !i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "\n", - "i0 & i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i0 & i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "\n", - "!i0 & i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i0 & i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "\n", - "i0 & !i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i0 & !i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "\n", - "!i0 & !i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i0 & !i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f7a0c2643c0> >" + " *' at 0x7fb9646b7630> >" ] }, "metadata": {}, @@ -2012,81 +2004,81 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "\n", - "i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "\n", - "!i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "!i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "\n", - "i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "\n", - "!i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f7a0c264a20> >" + " *' at 0x7fb9646b77b0> >" ] }, "metadata": {}, @@ -2105,81 +2097,81 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "\n", - "!i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "\n", - "i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "\n", - "!i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "!i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "\n", - "i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f7a0c264ea0> >" + " *' at 0x7fb9646b7f00> >" ] }, "metadata": {}, @@ -2198,125 +2190,125 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "\n", - "i0 & i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "i0 & i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "\n", - "!i0 & i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "!i0 & i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "\n", - "i0 & !i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "i0 & !i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "\n", - "!i0 & !i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "!i0 & !i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "\n", - "i0 & i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i0 & i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "\n", - "!i0 & i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i0 & i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "\n", - "i0 & !i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i0 & !i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "\n", - "!i0 & !i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i0 & !i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f7a0c2646f0> >" + " *' at 0x7fb9646b74b0> >" ] }, "metadata": {}, @@ -2350,7 +2342,6 @@ }, { "cell_type": "markdown", - "id": "435c9bae", "metadata": {}, "source": [ "If needed, a separated Mealy machine can be turned into game shape using `split_sepearated_mealy()`, which is more efficient than `split_2step()`." @@ -2359,7 +2350,6 @@ { "cell_type": "code", "execution_count": 5, - "id": "688a1ced", "metadata": {}, "outputs": [ { @@ -2368,260 +2358,260 @@ "
\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "\n", - "i0 & i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "i0 & i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "\n", - "!i0 & i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "!i0 & i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "\n", - "i0 & !i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "i0 & !i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "\n", - "!i0 & !i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "!i0 & !i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "\n", - "i0 & i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i0 & i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "\n", - "!i0 & i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i0 & i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "\n", - "i0 & !i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i0 & !i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "\n", - "!i0 & !i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i0 & !i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "
\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "t\n", - "[all]\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "i0 & !i1\n", + "\n", + "\n", + "i0 & !i1\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!i0 & !i1\n", + "\n", + "\n", + "!i0 & !i1\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "i0 & i1\n", + "\n", + "\n", + "i0 & i1\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "!i0 & i1\n", + "\n", + "\n", + "!i0 & i1\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "o0\n", + "\n", + "\n", + "o0\n", "\n", "\n", "\n", "3->0\n", - "\n", - "\n", - "o0\n", + "\n", + "\n", + "o0\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "1->4\n", - "\n", - "\n", - "i0 & i1\n", + "\n", + "\n", + "i0 & i1\n", "\n", "\n", "\n", "1->4\n", - "\n", - "\n", - "!i0 & i1\n", + "\n", + "\n", + "!i0 & i1\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "1->5\n", - "\n", - "\n", - "i0 & !i1\n", + "\n", + "\n", + "i0 & !i1\n", "\n", "\n", "\n", "1->5\n", - "\n", - "\n", - "!i0 & !i1\n", + "\n", + "\n", + "!i0 & !i1\n", "\n", "\n", "\n", "4->0\n", - "\n", - "\n", - "!o0\n", + "\n", + "\n", + "!o0\n", "\n", "\n", "\n", "5->1\n", - "\n", - "\n", - "!o0\n", + "\n", + "\n", + "!o0\n", "\n", "\n", "\n", @@ -2641,10 +2631,9 @@ }, { "cell_type": "markdown", - "id": "e3bb2d7d", "metadata": {}, "source": [ - "# Converting the separated mealy machine to AIG\n", + "# Converting the separated Mealy machine to AIG\n", "\n", "A separated Mealy machine can be converted to a circuit in the [AIGER format](http://fmv.jku.at/aiger/FORMAT.aiger) using `mealy_machine_to_aig()`. This takes a second argument specifying what type of encoding to use (exactly like `ltlsynt`'s `--aiger=...` option). \n", "\n", @@ -2654,7 +2643,6 @@ { "cell_type": "code", "execution_count": 6, - "id": "b5fea2d1", "metadata": {}, "outputs": [ { @@ -2663,60 +2651,60 @@ "\n", "\n", - "\n", "\n", - "\n", + "\n", "\n", - "\n", + "\n", "\n", "\n", "6\n", - "\n", - "L0_out\n", + "\n", + "L0_out\n", "\n", "\n", "\n", "o0\n", - "\n", - "o0\n", + "\n", + "o0\n", "\n", "\n", "\n", "6->o0:s\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "L0\n", - "\n", - "L0_in\n", + "\n", + "L0_in\n", "\n", "\n", "\n", "2\n", - "\n", - "i1\n", + "\n", + "i1\n", "\n", "\n", "\n", "2->L0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4\n", - "\n", - "i0\n", + "\n", + "i0\n", "\n", "\n", "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -2730,7 +2718,6 @@ }, { "cell_type": "markdown", - "id": "2a1a6fc9", "metadata": {}, "source": [ "While we are at it, let us mention that you can render those circuits horizontally as follows:" @@ -2739,7 +2726,6 @@ { "cell_type": "code", "execution_count": 7, - "id": "f909d578", "metadata": {}, "outputs": [ { @@ -2748,54 +2734,54 @@ "\n", "\n", - "\n", "\n", - "\n", + "\n", "\n", - "\n", + "\n", "\n", "\n", "6\n", - "\n", - "L0_out\n", + "\n", + "L0_out\n", "\n", "\n", "\n", "o0\n", - "\n", - "o0\n", + "\n", + "o0\n", "\n", "\n", "\n", "6->o0:w\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "L0\n", - "\n", - "L0_in\n", + "\n", + "L0_in\n", "\n", "\n", "\n", "2\n", - "\n", - "i1\n", + "\n", + "i1\n", "\n", "\n", "\n", "2->L0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4\n", - "\n", - "i0\n", + "\n", + "i0\n", "\n", "\n", "\n" @@ -2815,7 +2801,6 @@ }, { "cell_type": "markdown", - "id": "2c87313f", "metadata": {}, "source": [ "To encode the circuit in the AIGER format (ASCII version) use:" @@ -2824,7 +2809,6 @@ { "cell_type": "code", "execution_count": 8, - "id": "1b787f50", "metadata": {}, "outputs": [ { @@ -2848,7 +2832,6 @@ }, { "cell_type": "markdown", - "id": "72038258", "metadata": {}, "source": [ "# Adding more inputs and outputs by force" @@ -2856,7 +2839,6 @@ }, { "cell_type": "markdown", - "id": "3fbb3c2f", "metadata": {}, "source": [ "It can happen that propositions declared as output are ommited in the aig circuit (either because they are not part of the specification, or because they do not appear in the winning strategy). In that case those \n", @@ -2868,7 +2850,6 @@ { "cell_type": "code", "execution_count": 9, - "id": "8ed4e382", "metadata": {}, "outputs": [ { @@ -2877,159 +2858,159 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")\n", - "[Streett 1]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ") | Fin(\n", + "\n", + ")\n", + "[Streett 1]\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "I->3\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "3->6\n", - "\n", - "\n", - "i0\n", - "\n", + "\n", + "\n", + "i0\n", + "\n", "\n", "\n", "\n", "7\n", - "\n", - "7\n", + "\n", + "7\n", "\n", "\n", "\n", "3->7\n", - "\n", - "\n", - "!i0\n", - "\n", + "\n", + "\n", + "!i0\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "0->4\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "4->0\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "1->5\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "5->1\n", - "\n", - "\n", - "!o0\n", - "\n", + "\n", + "\n", + "!o0\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "2->6\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "6->0\n", - "\n", - "\n", - "o0\n", - "\n", + "\n", + "\n", + "o0\n", + "\n", "\n", "\n", "\n", "6->2\n", - "\n", - "\n", - "!o0\n", - "\n", + "\n", + "\n", + "!o0\n", + "\n", "\n", "\n", "\n", "7->1\n", - "\n", - "\n", - "!o0\n", - "\n", + "\n", + "\n", + "!o0\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f7a0c009f00> >" + " *' at 0x7fb9646b7570> >" ] }, "metadata": {}, @@ -3041,112 +3022,112 @@ "\n", "\n", - "\n", "\n", "\n", "\n", - "\n", - "t\n", - "[all]\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "i0\n", + "\n", + "\n", + "i0\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "0->4\n", - "\n", - "\n", - "!i0\n", + "\n", + "\n", + "!i0\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "o0\n", + "\n", + "\n", + "o0\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "4->3\n", - "\n", - "\n", - "!o0\n", + "\n", + "\n", + "!o0\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "1->5\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "5->1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "3->4\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f7a0c009180> >" + " *' at 0x7fb9646b7630> >" ] }, "metadata": {}, @@ -3158,144 +3139,144 @@ "
\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", - "t\n", - "[all]\n", + " viewBox=\"0.00 0.00 282.00 148.79\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", + "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "i0\n", + "\n", + "\n", + "i0\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "!i0\n", + "\n", + "\n", + "!i0\n", "\n", "\n", "\n", "2->0\n", - "\n", - "\n", - "o0\n", + "\n", + "\n", + "o0\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "3->1\n", - "\n", - "\n", - "!o0\n", + "\n", + "\n", + "!o0\n", "\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "
\n", "\n", - "\n", "\n", "\n", "\n", - "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "\n", - "i0\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "i0\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", + "\n", + "\n", "\n", - "!i0\n", - "/\n", + "!i0\n", + "/\n", "\n", - "!o0\n", + "!o0\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", + "\n", + "\n", "\n", - "1\n", - "/\n", + "1\n", + "/\n", "\n", - "!o0\n", + "!o0\n", "\n", "\n", "\n", @@ -3314,72 +3295,72 @@ "\n", "\n", - "\n", "\n", "\n", + " viewBox=\"0.00 0.00 143.20 352.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", "\n", - "\n", + "\n", "\n", "\n", "4\n", - "\n", - "L0_out\n", + "\n", + "L0_out\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "4->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "L0\n", - "\n", - "L0_in\n", + "\n", + "L0_in\n", "\n", "\n", "\n", "6->L0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "o0\n", - "\n", - "o0\n", + "\n", + "o0\n", "\n", "\n", "\n", "6->o0:s\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "i0\n", + "\n", + "i0\n", "\n", "\n", "\n", "2->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -3401,7 +3382,6 @@ }, { "cell_type": "markdown", - "id": "a82ca6c6", "metadata": {}, "source": [ "To force the presence of extra variables in the circuit, they can be passed to `mealy_machine_to_aig()`." @@ -3410,7 +3390,6 @@ { "cell_type": "code", "execution_count": 10, - "id": "a86436a7", "metadata": {}, "outputs": [ { @@ -3419,96 +3398,96 @@ "\n", "\n", - "\n", "\n", - "\n", + "\n", "\n", - "\n", + "\n", "\n", "\n", "6\n", - "\n", - "L0_out\n", + "\n", + "L0_out\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "6->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "L0\n", - "\n", - "L0_in\n", + "\n", + "L0_in\n", "\n", "\n", "\n", "8->L0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "o0\n", - "\n", - "o0\n", + "\n", + "o0\n", "\n", "\n", "\n", "8->o0:s\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "o1\n", - "\n", - "o1\n", + "\n", + "o1\n", "\n", "\n", "\n", "2\n", - "\n", - "i0\n", + "\n", + "i0\n", "\n", "\n", "\n", "2->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4\n", - "\n", - "i1\n", + "\n", + "i1\n", "\n", "\n", "\n", "0\n", - "\n", - "False\n", + "\n", + "False\n", "\n", "\n", "\n", "0->o1:s\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -3521,7 +3500,6 @@ }, { "cell_type": "markdown", - "id": "9af5c9b9", "metadata": {}, "source": [ "# Combining Mealy machines\n", @@ -3531,7 +3509,7 @@ "\n", "This can be done in two ways:\n", "\n", - "1. Using the function `mealy_machines_to_aig()`, which takes a vector of separated mealy machines as argument.\n", + "1. Using the function `mealy_machines_to_aig()`, which takes a vector of separated Mealy machines as argument.\n", "2. Combine the mealy machines into one before passing it to `mealy_machine_to aig(). This currently only supports input complete machines of the same type (mealy/separated mealy/split mealy)\n", "\n", "Note that the method version is usually preferable as it is faster.\n", @@ -3541,7 +3519,6 @@ { "cell_type": "code", "execution_count": 11, - "id": "750e55f5", "metadata": {}, "outputs": [ { @@ -3557,150 +3534,150 @@ "
\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")\n", - "[Streett 1]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ") | Fin(\n", + "\n", + ")\n", + "[Streett 1]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "(!i0 & !i1) | (i0 & i1)\n", - "\n", + "\n", + "\n", + "(!i0 & !i1) | (i0 & i1)\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "(!i0 & i1) | (i0 & !i1)\n", - "\n", + "\n", + "\n", + "(!i0 & i1) | (i0 & !i1)\n", + "\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "!o0\n", - "\n", + "\n", + "\n", + "!o0\n", + "\n", "\n", "\n", "\n", "2->0\n", - "\n", - "\n", - "o0\n", - "\n", + "\n", + "\n", + "o0\n", + "\n", "\n", "\n", "\n", "
\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")\n", - "[Streett 1]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ") | Fin(\n", + "\n", + ")\n", + "[Streett 1]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "(!i0 & !i1) | (i0 & i1)\n", - "\n", + "\n", + "\n", + "(!i0 & !i1) | (i0 & i1)\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "(!i0 & i1) | (i0 & !i1)\n", - "\n", + "\n", + "\n", + "(!i0 & i1) | (i0 & !i1)\n", + "\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "o1\n", - "\n", + "\n", + "\n", + "o1\n", + "\n", "\n", "\n", "\n", "2->0\n", - "\n", - "\n", - "!o1\n", - "\n", + "\n", + "\n", + "!o1\n", + "\n", "\n", "\n", "\n", @@ -3726,94 +3703,94 @@ "
\n", "\n", - "\n", "\n", - "\n", + "\n", "\n", - "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "\n", - "(!i0 & !i1) | (i0 & i1)\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "(!i0 & !i1) | (i0 & i1)\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "\n", - "(!i0 & i1) | (i0 & !i1)\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "(!i0 & i1) | (i0 & !i1)\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "
\n", "\n", - "\n", "\n", - "\n", + "\n", "\n", - "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "\n", - "(!i0 & !i1) | (i0 & i1)\n", - "/\n", - "\n", - "o1\n", + "\n", + "\n", + "\n", + "(!i0 & !i1) | (i0 & i1)\n", + "/\n", + "\n", + "o1\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "\n", - "(!i0 & i1) | (i0 & !i1)\n", - "/\n", - "\n", - "!o1\n", + "\n", + "\n", + "\n", + "(!i0 & i1) | (i0 & !i1)\n", + "/\n", + "\n", + "!o1\n", "\n", "\n", "\n", @@ -3839,108 +3816,108 @@ "\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "10\n", - "\n", - "10\n", + "\n", + "10\n", "\n", "\n", "\n", "6->10\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "8->10\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "o0\n", - "\n", - "o0\n", + "\n", + "o0\n", "\n", "\n", "\n", "10->o0:s\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "o1\n", - "\n", - "o1\n", + "\n", + "o1\n", "\n", "\n", "\n", "10->o1:s\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "i0\n", + "\n", + "i0\n", "\n", "\n", "\n", "2->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4\n", - "\n", - "i1\n", + "\n", + "i1\n", "\n", "\n", "\n", "4->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -3959,53 +3936,53 @@ "\n", "\n", - "\n", "\n", - "\n", + "\n", "\n", - "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0,0\n", + "\n", + "0,0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "\n", - "(!i0 & !i1) | (i0 & i1)\n", - "/\n", - "\n", - "!o0 & o1\n", + "\n", + "\n", + "\n", + "(!i0 & !i1) | (i0 & i1)\n", + "/\n", + "\n", + "!o0 & o1\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "\n", - "(!i0 & i1) | (i0 & !i1)\n", - "/\n", - "\n", - "o0 & !o1\n", + "\n", + "\n", + "\n", + "(!i0 & i1) | (i0 & !i1)\n", + "/\n", + "\n", + "o0 & !o1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f7a0c009de0> >" + " *' at 0x7fb9646b7c60> >" ] }, "metadata": {}, @@ -4017,108 +3994,108 @@ "\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "10\n", - "\n", - "10\n", + "\n", + "10\n", "\n", "\n", "\n", "6->10\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "8->10\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "o0\n", - "\n", - "o0\n", + "\n", + "o0\n", "\n", "\n", "\n", "10->o0:s\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "o1\n", - "\n", - "o1\n", + "\n", + "o1\n", "\n", "\n", "\n", "10->o1:s\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "i0\n", + "\n", + "i0\n", "\n", "\n", "\n", "2->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4\n", - "\n", - "i1\n", + "\n", + "i1\n", "\n", "\n", "\n", "4->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -4152,7 +4129,6 @@ }, { "cell_type": "markdown", - "id": "5102e762", "metadata": {}, "source": [ "# Reading an AIGER-file\n", @@ -4167,7 +4143,6 @@ { "cell_type": "code", "execution_count": 12, - "id": "29d37752", "metadata": {}, "outputs": [], "source": [ @@ -4188,7 +4163,6 @@ { "cell_type": "code", "execution_count": 13, - "id": "8989722d", "metadata": {}, "outputs": [ { @@ -4197,108 +4171,108 @@ "\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "10\n", - "\n", - "10\n", + "\n", + "10\n", "\n", "\n", "\n", "6->10\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "o1\n", - "\n", - "d\n", + "\n", + "d\n", "\n", "\n", "\n", "6->o1:s\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "8->10\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "o0\n", - "\n", - "c\n", + "\n", + "c\n", "\n", "\n", "\n", "10->o0:s\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "a\n", + "\n", + "a\n", "\n", "\n", "\n", "2->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4\n", - "\n", - "b\n", + "\n", + "b\n", "\n", "\n", "\n", "4->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -4313,7 +4287,6 @@ { "cell_type": "code", "execution_count": 14, - "id": "9560f368", "metadata": {}, "outputs": [ { @@ -4342,7 +4315,6 @@ { "cell_type": "code", "execution_count": 15, - "id": "9dadee6a", "metadata": {}, "outputs": [ { @@ -4359,7 +4331,6 @@ }, { "cell_type": "markdown", - "id": "734f10f1", "metadata": {}, "source": [ "An AIG circuit can be transformed into a monitor/Mealy machine. This can be used for instance to check that it does not intersect the negation of the specification." @@ -4368,7 +4339,6 @@ { "cell_type": "code", "execution_count": 16, - "id": "b29c95b4", "metadata": {}, "outputs": [ { @@ -4377,52 +4347,52 @@ "\n", "\n", - "\n", "\n", - "\n", + "\n", "\n", - "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "\n", - "!a & !b\n", - "/\n", - "\n", - "!c & !d\n", - "\n", - "a & b\n", - "/\n", - "\n", - "!c & d\n", - "\n", - "(!a & b) | (a & !b)\n", - "/\n", - "\n", - "c & !d\n", + "\n", + "\n", + "\n", + "!a & !b\n", + "/\n", + "\n", + "!c & !d\n", + "\n", + "a & b\n", + "/\n", + "\n", + "!c & d\n", + "\n", + "(!a & b) | (a & !b)\n", + "/\n", + "\n", + "c & !d\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f7a0c2640c0> >" + " *' at 0x7fb9646c8360> >" ] }, "execution_count": 16, @@ -4436,7 +4406,6 @@ }, { "cell_type": "markdown", - "id": "09cad9f5", "metadata": {}, "source": [ "Note that the generation of aiger circuits from Mealy machines is flexible and accepts separated Mealy machines\n", @@ -4446,7 +4415,6 @@ { "cell_type": "code", "execution_count": 17, - "id": "62ebedae", "metadata": {}, "outputs": [ { @@ -4455,114 +4423,114 @@ "
\n", "\n", - "\n", "\n", - "\n", + "\n", "\n", - "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "\n", - "(!i0 & !i1) | (i0 & i1)\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "(!i0 & !i1) | (i0 & i1)\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "\n", - "(!i0 & i1) | (i0 & !i1)\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "(!i0 & i1) | (i0 & !i1)\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "
\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "t\n", - "[all]\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "(!i0 & !i1) | (i0 & i1)\n", + "\n", + "\n", + "(!i0 & !i1) | (i0 & i1)\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "(!i0 & i1) | (i0 & !i1)\n", + "\n", + "\n", + "(!i0 & i1) | (i0 & !i1)\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "!o0\n", + "\n", + "\n", + "!o0\n", "\n", "\n", "\n", "2->0\n", - "\n", - "\n", - "o0\n", + "\n", + "\n", + "o0\n", "\n", "\n", "\n", @@ -4594,7 +4562,6 @@ { "cell_type": "code", "execution_count": 18, - "id": "4a0bb1a7", "metadata": {}, "outputs": [ { @@ -4603,180 +4570,180 @@ "
\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "10\n", - "\n", - "10\n", + "\n", + "10\n", "\n", "\n", "\n", "6->10\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "8->10\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "o0\n", - "\n", - "o0\n", + "\n", + "o0\n", "\n", "\n", "\n", "10->o0:s\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "i0\n", + "\n", + "i0\n", "\n", "\n", "\n", "2->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4\n", - "\n", - "i1\n", + "\n", + "i1\n", "\n", "\n", "\n", "4->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "
\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "10\n", - "\n", - "10\n", + "\n", + "10\n", "\n", "\n", "\n", "6->10\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "8->10\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "o0\n", - "\n", - "o0\n", + "\n", + "o0\n", "\n", "\n", "\n", "10->o0:s\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "i0\n", + "\n", + "i0\n", "\n", "\n", "\n", "2->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4\n", - "\n", - "i1\n", + "\n", + "i1\n", "\n", "\n", "\n", "4->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", @@ -4797,7 +4764,7 @@ ], "metadata": { "kernelspec": { - "display_name": "Python 3 (ipykernel)", + "display_name": "Python 3", "language": "python", "name": "python3" }, @@ -4811,7 +4778,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.8.10" + "version": "3.7.3" } }, "nbformat": 4,