diff --git a/tests/python/satmin.ipynb b/tests/python/satmin.ipynb index 74ba91ed9..a34f9d170 100644 --- a/tests/python/satmin.ipynb +++ b/tests/python/satmin.ipynb @@ -256,7 +256,7 @@ "\n" ], "text/plain": [ - " *' at 0x7feac4659ea0> >" + " *' at 0x7f7b085aaea0> >" ] }, "execution_count": 3, @@ -444,7 +444,7 @@ "\n" ], "text/plain": [ - " *' at 0x7feac4610ab0> >" + " *' at 0x7f7b0861fc90> >" ] }, "execution_count": 4, @@ -680,7 +680,7 @@ "\n" ], "text/plain": [ - " *' at 0x7feac4610a50> >" + " *' at 0x7f7b085b5060> >" ] }, "execution_count": 5, @@ -913,7 +913,7 @@ "\n" ], "text/plain": [ - " *' at 0x7feac4610c30> >" + " *' at 0x7f7b08561b70> >" ] }, "execution_count": 6, @@ -934,56 +934,6 @@ "large" ] }, - { - "cell_type": "code", - "execution_count": 7, - "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "HOA: v1\n", - "name: \"& | F G a F b F G c\"\n", - "States: 6\n", - "Start: 5\n", - "AP: 3 \"a\" \"c\" \"b\"\n", - "acc-name: Rabin 2\n", - "Acceptance: 4 (Fin(0) & Inf(1)) | (Fin(2) & Inf(3))\n", - "properties: trans-labels explicit-labels state-acc complete\n", - "properties: deterministic stutter-invariant\n", - "--BODY--\n", - "State: 0 {1 3}\n", - "[0&1] 0\n", - "[!0&1] 1\n", - "[!1] 4\n", - "State: 1 {0 3}\n", - "[1] 1\n", - "[!1] 4\n", - "State: 2 {1 2}\n", - "[1] 2\n", - "[!1] 4\n", - "State: 3 {1 2}\n", - "[0&1&2] 0\n", - "[0&1&!2] 3\n", - "[!0&2 | !1&2] 4\n", - "[!0&!2 | !1&!2] 5\n", - "State: 4 {0 2}\n", - "[1] 2\n", - "[!1] 4\n", - "State: 5 {0 2}\n", - "[1&2] 2\n", - "[0&1&!2] 3\n", - "[!1&2] 4\n", - "[!0&!2 | !1&!2] 5\n", - "--END--\n" - ] - } - ], - "source": [ - "print(large.to_str())" - ] - }, { "cell_type": "markdown", "metadata": {}, @@ -993,7 +943,7 @@ }, { "cell_type": "code", - "execution_count": 8, + "execution_count": 7, "metadata": {}, "outputs": [ { @@ -1112,10 +1062,10 @@ "\n" ], "text/plain": [ - " *' at 0x7feac46105a0> >" + " *' at 0x7f7b08561b40> >" ] }, - "execution_count": 8, + "execution_count": 7, "metadata": {}, "output_type": "execute_result" } @@ -1133,7 +1083,7 @@ }, { "cell_type": "code", - "execution_count": 9, + "execution_count": 8, "metadata": {}, "outputs": [ { @@ -1284,10 +1234,10 @@ "\n" ], "text/plain": [ - " *' at 0x7feac4610a20> >" + " *' at 0x7f7b08561c00> >" ] }, - "execution_count": 9, + "execution_count": 8, "metadata": {}, "output_type": "execute_result" } @@ -1305,7 +1255,7 @@ }, { "cell_type": "code", - "execution_count": 10, + "execution_count": 9, "metadata": {}, "outputs": [ { @@ -1450,10 +1400,10 @@ "\n" ], "text/plain": [ - " *' at 0x7feac4610b70> >" + " *' at 0x7f7b08561bd0> >" ] }, - "execution_count": 10, + "execution_count": 9, "metadata": {}, "output_type": "execute_result" } @@ -1475,7 +1425,7 @@ }, { "cell_type": "code", - "execution_count": 11, + "execution_count": 10, "metadata": {}, "outputs": [ { @@ -1522,7 +1472,7 @@ " NaN\n", " 1428\n", " 73430\n", - " 3\n", + " 4\n", " 0\n", " 1\n", " 0\n", @@ -1536,9 +1486,9 @@ " 40\n", " 3960\n", " 336307\n", - " 12\n", + " 13\n", " 1\n", - " 20\n", + " 19\n", " 0\n", " \n", " \n", @@ -1550,7 +1500,7 @@ " 32\n", " 2008\n", " 116372\n", - " 4\n", + " 5\n", " 0\n", " 4\n", " 0\n", @@ -1566,9 +1516,9 @@ "2 5 4 4 12 32 2008 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", - "0 73430 3 0 1 0 \n", - "1 336307 12 1 20 0 \n", - "2 116372 4 0 4 0 " + "0 73430 4 0 1 0 \n", + "1 336307 13 1 19 0 \n", + "2 116372 5 0 4 0 " ] }, "metadata": {}, @@ -1716,10 +1666,10 @@ "\n" ], "text/plain": [ - " *' at 0x7feac8bff780> >" + " *' at 0x7f7b0cb8d6f0> >" ] }, - "execution_count": 11, + "execution_count": 10, "metadata": {}, "output_type": "execute_result" } @@ -1737,7 +1687,7 @@ }, { "cell_type": "code", - "execution_count": 12, + "execution_count": 11, "metadata": {}, "outputs": [ { @@ -1784,7 +1734,7 @@ " NaN\n", " 483\n", " 24470\n", - " 1\n", + " 2\n", " 0\n", " 0\n", " 0\n", @@ -1798,9 +1748,9 @@ " 40\n", " 1335\n", " 111187\n", - " 4\n", + " 5\n", " 0\n", - " 2\n", + " 4\n", " 0\n", " \n", " \n", @@ -1812,7 +1762,7 @@ " 32\n", " 856\n", " 57332\n", - " 2\n", + " 3\n", " 0\n", " 1\n", " 0\n", @@ -1828,9 +1778,9 @@ "2 2 4 4 12 32 856 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", - "0 24470 1 0 0 0 \n", - "1 111187 4 0 2 0 \n", - "2 57332 2 0 1 0 " + "0 24470 2 0 0 0 \n", + "1 111187 5 0 4 0 \n", + "2 57332 3 0 1 0 " ] }, "metadata": {}, @@ -1978,10 +1928,10 @@ "\n" ], "text/plain": [ - " *' at 0x7feac8bffb40> >" + " *' at 0x7f7b0cb8dc00> >" ] }, - "execution_count": 12, + "execution_count": 11, "metadata": {}, "output_type": "execute_result" } @@ -2001,7 +1951,7 @@ }, { "cell_type": "code", - "execution_count": 13, + "execution_count": 12, "metadata": {}, "outputs": [ { @@ -2048,8 +1998,8 @@ " 40\n", " 3050\n", " 437037\n", - " 16\n", - " 1\n", + " 20\n", + " 0\n", " 17\n", " 0\n", " \n", @@ -2062,9 +2012,9 @@ " 16\n", " 488\n", " 28449\n", - " 1\n", + " 2\n", + " 0\n", " 0\n", - " 1\n", " 0\n", " \n", " \n", @@ -2092,8 +2042,8 @@ "2 2 1 NaN NaN NaN 68 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", - "0 437037 16 1 17 0 \n", - "1 28449 1 0 1 0 \n", + "0 437037 20 0 17 0 \n", + "1 28449 2 0 0 0 \n", "2 1285 0 0 0 0 " ] }, @@ -2192,10 +2142,10 @@ "\n" ], "text/plain": [ - " *' at 0x7feac8bffd80> >" + " *' at 0x7f7b0cb8dd50> >" ] }, - "execution_count": 13, + "execution_count": 12, "metadata": {}, "output_type": "execute_result" } @@ -2213,7 +2163,7 @@ }, { "cell_type": "code", - "execution_count": 14, + "execution_count": 13, "metadata": {}, "outputs": [ { @@ -2260,9 +2210,9 @@ " 48\n", " 3894\n", " 258719\n", - " 8\n", + " 9\n", " 0\n", - " 7\n", + " 6\n", " 0\n", " \n", " \n", @@ -2274,7 +2224,7 @@ " 40\n", " 2005\n", " 106302\n", - " 3\n", + " 5\n", " 0\n", " 2\n", " 0\n", @@ -2290,7 +2240,7 @@ " 24632\n", " 1\n", " 0\n", - " 0\n", + " 1\n", " 0\n", " \n", " \n", @@ -2302,7 +2252,7 @@ " NaN\n", " 363\n", " 10553\n", - " 1\n", + " 0\n", " 0\n", " 0\n", " 0\n", @@ -2319,10 +2269,10 @@ "3 4 3 NaN NaN NaN 363 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", - "0 258719 8 0 7 0 \n", - "1 106302 3 0 2 0 \n", - "2 24632 1 0 0 0 \n", - "3 10553 1 0 0 0 " + "0 258719 9 0 6 0 \n", + "1 106302 5 0 2 0 \n", + "2 24632 1 0 1 0 \n", + "3 10553 0 0 0 0 " ] }, "metadata": {}, @@ -2459,10 +2409,10 @@ "\n" ], "text/plain": [ - " *' at 0x7feac8bffed0> >" + " *' at 0x7f7b0cb8dde0> >" ] }, - "execution_count": 14, + "execution_count": 13, "metadata": {}, "output_type": "execute_result" } @@ -2493,7 +2443,7 @@ }, { "cell_type": "code", - "execution_count": 15, + "execution_count": 14, "metadata": {}, "outputs": [ { @@ -2540,7 +2490,7 @@ " NaN\n", " 3899\n", " 258963\n", - " 8\n", + " 10\n", " 0\n", " 3\n", " 0\n", @@ -2570,7 +2520,7 @@ " 258963\n", " 0\n", " 0\n", - " 1\n", + " 0\n", " 0\n", " \n", " \n", @@ -2584,9 +2534,9 @@ "2 6 4 4 11 32 3899 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", - "0 258963 8 0 3 0 \n", + "0 258963 10 0 3 0 \n", "1 258963 0 0 1 0 \n", - "2 258963 0 0 1 0 " + "2 258963 0 0 0 0 " ] }, "metadata": {}, @@ -2723,10 +2673,10 @@ "\n" ], "text/plain": [ - " *' at 0x7feac8bffe70> >" + " *' at 0x7f7b08561690> >" ] }, - "execution_count": 15, + "execution_count": 14, "metadata": {}, "output_type": "execute_result" } @@ -2746,7 +2696,7 @@ }, { "cell_type": "code", - "execution_count": 16, + "execution_count": 15, "metadata": {}, "outputs": [ { @@ -2793,7 +2743,7 @@ " 48\n", " 3894\n", " 258719\n", - " 9\n", + " 10\n", " 0\n", " 6\n", " 0\n", @@ -2809,7 +2759,7 @@ " 258767\n", " 0\n", " 0\n", - " 1\n", + " 0\n", " 0\n", " \n", " \n", @@ -2821,7 +2771,7 @@ " 32\n", " 3894\n", " 258815\n", - " 0\n", + " 1\n", " 0\n", " 0\n", " 0\n", @@ -2852,9 +2802,9 @@ "3 4 3 NaN NaN NaN 363 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", - "0 258719 9 0 6 0 \n", - "1 258767 0 0 1 0 \n", - "2 258815 0 0 0 0 \n", + "0 258719 10 0 6 0 \n", + "1 258767 0 0 0 0 \n", + "2 258815 1 0 0 0 \n", "3 10325 0 0 1 0 " ] }, @@ -2985,10 +2935,10 @@ "\n" ], "text/plain": [ - " *' at 0x7feac8ba9150> >" + " *' at 0x7f7b08561ab0> >" ] }, - "execution_count": 16, + "execution_count": 15, "metadata": {}, "output_type": "execute_result" } @@ -3010,7 +2960,7 @@ }, { "cell_type": "code", - "execution_count": 17, + "execution_count": 16, "metadata": {}, "outputs": [ { @@ -3137,7 +3087,7 @@ "\n" ], "text/plain": [ - " *' at 0x7feac8ba9270> >" + " *' at 0x7f7b0cb610f0> >" ] }, "metadata": {}, @@ -3188,9 +3138,9 @@ " 48\n", " 3894\n", " 258719\n", - " 9\n", + " 10\n", " 0\n", - " 6\n", + " 5\n", " 0\n", " HOA: v1 States: 6 Start: 0 AP: 3 \"a\" \"c\" \"b\" a...\n", " \n", @@ -3205,7 +3155,7 @@ " 258767\n", " 0\n", " 0\n", - " 1\n", + " 0\n", " 0\n", " HOA: v1 States: 5 Start: 0 AP: 3 \"a\" \"c\" \"b\" a...\n", " \n", @@ -3235,7 +3185,7 @@ " 10325\n", " 0\n", " 0\n", - " 0\n", + " 1\n", " 0\n", " NaN\n", " \n", @@ -3251,10 +3201,10 @@ "3 4 3 NaN NaN NaN 363 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \\\n", - "0 258719 9 0 6 0 \n", - "1 258767 0 0 1 0 \n", + "0 258719 10 0 5 0 \n", + "1 258767 0 0 0 0 \n", "2 258815 0 0 0 0 \n", - "3 10325 0 0 0 0 \n", + "3 10325 0 0 1 0 \n", "\n", " automaton \n", "0 HOA: v1 States: 6 Start: 0 AP: 3 \"a\" \"c\" \"b\" a... \n", @@ -3282,7 +3232,7 @@ }, { "cell_type": "code", - "execution_count": 18, + "execution_count": 17, "metadata": {}, "outputs": [ { @@ -3492,7 +3442,7 @@ "\n" ], "text/plain": [ - " *' at 0x7feac8ba91b0> >" + " *' at 0x7f7b0cb61300> >" ] }, "metadata": {}, @@ -3664,7 +3614,7 @@ "\n" ], "text/plain": [ - " *' at 0x7feac8ba92a0> >" + " *' at 0x7f7b0cb613f0> >" ] }, "metadata": {}, @@ -3801,7 +3751,7 @@ "\n" ], "text/plain": [ - " *' at 0x7feac8ba9090> >" + " *' at 0x7f7b0cb61480> >" ] }, "metadata": {}, @@ -3828,7 +3778,7 @@ }, { "cell_type": "code", - "execution_count": 19, + "execution_count": 18, "metadata": {}, "outputs": [ { @@ -4033,10 +3983,10 @@ "\n" ], "text/plain": [ - " *' at 0x7feac4610c30> >" + " *' at 0x7f7b08561b70> >" ] }, - "execution_count": 19, + "execution_count": 18, "metadata": {}, "output_type": "execute_result" } @@ -4054,7 +4004,7 @@ }, { "cell_type": "code", - "execution_count": 20, + "execution_count": 19, "metadata": {}, "outputs": [ { @@ -4101,9 +4051,9 @@ " NaN\n", " 975\n", " 32912\n", - " 2\n", - " 0\n", + " 1\n", " 0\n", + " 1\n", " 0\n", " \n", " \n", @@ -4115,8 +4065,8 @@ " 32\n", " 2705\n", " 150257\n", - " 5\n", - " 1\n", + " 6\n", + " 0\n", " 3\n", " 0\n", " \n", @@ -4130,8 +4080,8 @@ "1 6 5 4 10 32 2705 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", - "0 32912 2 0 0 0 \n", - "1 150257 5 1 3 0 " + "0 32912 1 0 1 0 \n", + "1 150257 6 0 3 0 " ] }, "metadata": {}, @@ -4261,10 +4211,10 @@ "\n" ], "text/plain": [ - " *' at 0x7feac8ba9330> >" + " *' at 0x7f7b0cb61510> >" ] }, - "execution_count": 20, + "execution_count": 19, "metadata": {}, "output_type": "execute_result" } @@ -4276,7 +4226,7 @@ }, { "cell_type": "code", - "execution_count": 21, + "execution_count": 20, "metadata": {}, "outputs": [ { @@ -4325,7 +4275,7 @@ " 77340\n", " 3\n", " 0\n", - " 2\n", + " 1\n", " 0\n", " \n", " \n", @@ -4353,7 +4303,7 @@ " 10496\n", " 0\n", " 0\n", - " 1\n", + " 0\n", " 0\n", " \n", " \n", @@ -4367,9 +4317,9 @@ "2 4 3 NaN NaN NaN 363 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", - "0 77340 3 0 2 0 \n", + "0 77340 3 0 1 0 \n", "1 3129 0 0 0 0 \n", - "2 10496 0 0 1 0 " + "2 10496 0 0 0 0 " ] }, "metadata": {}, @@ -4513,10 +4463,10 @@ "\n" ], "text/plain": [ - " *' at 0x7feac8ba9630> >" + " *' at 0x7f7b085aaf30> >" ] }, - "execution_count": 21, + "execution_count": 20, "metadata": {}, "output_type": "execute_result" } @@ -4537,7 +4487,7 @@ }, { "cell_type": "code", - "execution_count": 22, + "execution_count": 21, "metadata": {}, "outputs": [ { @@ -4586,7 +4536,7 @@ " 135032\n", " 5\n", " 0\n", - " 3\n", + " 2\n", " 0\n", " \n", " \n", @@ -4598,7 +4548,7 @@ "0 2 7 5 14 40 1869 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", - "0 135032 5 0 3 0 " + "0 135032 5 0 2 0 " ] }, "metadata": {}, @@ -4763,10 +4713,10 @@ "\n" ], "text/plain": [ - " *' at 0x7feac8ba9660> >" + " *' at 0x7f7b0cb61660> >" ] }, - "execution_count": 22, + "execution_count": 21, "metadata": {}, "output_type": "execute_result" }