diff --git a/NEWS b/NEWS index f42fcfc43..d0e7d7e1b 100644 --- a/NEWS +++ b/NEWS @@ -41,6 +41,10 @@ New in spot 2.3.0.dev (not yet released) caused any user-defined CPPFLAGS to be ignored while building Spot. + - The display of clusters with universal edges was confused, because the + intermediate node was not in the cluster even if one of the target was + in the same one. + New in spot 2.3 (2017-01-19) Build: diff --git a/spot/twaalgos/dot.cc b/spot/twaalgos/dot.cc index 2c5d2908d..fd1d7e263 100644 --- a/spot/twaalgos/dot.cc +++ b/spot/twaalgos/dot.cc @@ -369,7 +369,8 @@ namespace spot std::set> done; void - print_dst(int dst, const char* style = nullptr, int color_num = -1) + print_dst(int dst, const char* style = nullptr, int scc_num = -1, + int color_num = -1) { std::ostringstream tmp_dst; tmp_dst << dst; @@ -584,9 +585,14 @@ namespace spot } void - process_link(const twa_graph::edge_storage_t& t, int number) + process_link(const twa_graph::edge_storage_t& t, int number, + int scc_num = -1) { os_ << " " << t.src << " -> " << (int)t.dst; + if (scc_num >= 0) + { + os_ << '.' << scc_num; + } if (aut_->is_univ_dest(t.dst) && highlight_edges_ && !opt_shared_univ_dest_) { @@ -659,9 +665,9 @@ namespace spot if (aut_->is_univ_dest(t.dst)) { if (color_num >= 0) - print_dst(t.dst, highlight.c_str(), color_num); + print_dst(t.dst, highlight.c_str(), scc_num, color_num); else - print_dst(t.dst, highlight.c_str()); + print_dst(t.dst, highlight.c_str(), scc_num); } } @@ -764,7 +770,29 @@ namespace spot os_ << " label=\"\"\n"; } for (auto s: si->states_of(i)) - process_state(s); + { + process_state(s); + int trans_num = 0; + for (auto& t : aut_->out(s)) + { + if (aut_->is_univ_dest(t.dst)) + { + bool to_write = false; + for (unsigned d: aut_->univ_dests(t.dst)) + { + to_write = si->scc_of(d) == si->scc_of(s); + if (to_write) + break; + } + if (to_write) + process_link(t, trans_num++, i); + else + process_link(t, trans_num++); + } + else + process_link(t, trans_num++); + } + } os_ << " }\n"; } } @@ -772,10 +800,12 @@ namespace spot for (unsigned n = 0; n < ns; ++n) { if (!si || !si->reachable_state(n)) - process_state(n); - int trans_num = 0; - for (auto& t: aut_->out(n)) - process_link(t, trans_num++); + { + process_state(n); + int trans_num = 0; + for (auto& t: aut_->out(n)) + process_link(t, trans_num++); + } } end(); } diff --git a/tests/core/alternating.test b/tests/core/alternating.test index 7f20b953f..d8c0f3605 100755 --- a/tests/core/alternating.test +++ b/tests/core/alternating.test @@ -69,37 +69,49 @@ digraph G { color=green label="" 2 [label="G(a)"] + 2 -> 2 [label="a"] } subgraph cluster_1 { color=red label="" 1 [label="FG(a)\n⓿"] + 1 -> 2 [label="a"] + 1 -> 1 [label="1"] } subgraph cluster_2 { color=green label="" 6 [label="t"] + 6 -> 6 [label="1"] } subgraph cluster_3 { color=red label="" 4 [label="F(b)\n⓿"] + 4 -> 6 [label="b"] + 4 -> 4 [label="!b"] } subgraph cluster_4 { color=green label="" 3 [label="GF(b)"] + 3 -> 3 [label="b"] + 3 -> -8.4 [label="!b", style=bold, color="#FAA43A", arrowhead=onormal] + -8.4 [label=<>,shape=point] + -8.4 -> 3 [style=bold, color="#FAA43A"] + -8.4 -> 4 [style=bold, color="#FAA43A"] } subgraph cluster_5 { color=red label="" 5 [label="((a) U (b))\n⓿"] + 5 -> 6 [label="b"] + 5 -> 5 [label="a & !b"] } subgraph cluster_6 { color=black label="" 0 [label="((((a) U (b)) && GF(b)) && FG(a))"] - } 0 -> -1 [label="b", arrowhead=onormal] -1 [label=<>,shape=point] -1 -> 1 @@ -109,19 +121,7 @@ digraph G { -4 -> 1 [style=bold, color="#F15854"] -4 -> 3 [style=bold, color="#F15854"] -4 -> 5 [style=bold, color="#F15854"] - 1 -> 2 [label="a"] - 1 -> 1 [label="1"] - 2 -> 2 [label="a"] - 3 -> 3 [label="b"] - 3 -> -8 [label="!b", style=bold, color="#FAA43A", arrowhead=onormal] - -8 [label=<>,shape=point] - -8 -> 3 [style=bold, color="#FAA43A"] - -8 -> 4 [style=bold, color="#FAA43A"] - 4 -> 6 [label="b"] - 4 -> 4 [label="!b"] - 5 -> 6 [label="b"] - 5 -> 5 [label="a & !b"] - 6 -> 6 [label="1"] + } } EOF @@ -353,7 +353,7 @@ State: 0 EOF diff out5 expect -# Test if split option is correct +# Test if split option with color is correct cat >ex6< ex6.dot +style='arrowhead=onormal' cat >expect6.dot< 1 0 [label=<0>] 0 -> 0 [label=] - 0 -> -1.1 [label=, style=bold, color="#F17CB0", arrowhead=onormal] + 0 -> -1.1 [label=, style=bold, color="#F17CB0", $style] -1.1 [label=<>,shape=point] -1.1 -> 0 [style=bold, color="#F17CB0"] -1.1 -> 1 [style=bold, color="#F17CB0"] - 0 -> -1.2 [label=, style=bold, color="#FAA43A", arrowhead=onormal] + 0 -> -1.2 [label=, style=bold, color="#FAA43A", $style] -1.2 [label=<>,shape=point] -1.2 -> 0 [style=bold, color="#FAA43A"] -1.2 -> 1 [style=bold, color="#FAA43A"] @@ -690,6 +691,79 @@ EOF diff ex10.dot expect10.dot +cat >ex11 < ex11.dot + +cat >expect11.dot <⓿)> + labelloc="t" + fontname="Lato" + node [fontname="Lato"] + edge [fontname="Lato"] + I [label="", style=invis, width=0] + I -> 0 + subgraph cluster_0 { + color=green + label="" + 3 [label="t"] + 3 -> 3 [label=<1>] + } + subgraph cluster_1 { + color=green + label="" + 1 [label="Fa"] + 1 -> 3 [label=] + 1 -> 1 [label=] + } + subgraph cluster_2 { + color=green + label="" + 2 [label="G!a"] + 2 -> 2 [label=] + } + subgraph cluster_3 { + color=green + label="" + 0 [label="G((b & Fa) | (!b & G!a))"] + 0 -> 0 [label=] + 0 -> -1.3 [label=, arrowhead=onormal] + -1.3 [label=<>,shape=point] + -1.3 -> 0 + -1.3 -> 1 + 0 -> -4.3 [label=, arrowhead=onormal] + -4.3 [label=<>,shape=point] + -4.3 -> 0 + -4.3 -> 2 + } +} +EOF + +diff ex11.dot expect11.dot + # Detect cases where alternation-removal cannot work. cat >in < 1 [label="1"] } subgraph cluster_1 { color=red label="" 0 [label="0"] - } 0 -> 1 [label="b"] 0 -> 0 [label="0"] - 1 -> 1 [label="1"] + } } EOF diff stdout expected diff --git a/tests/core/readsave.test b/tests/core/readsave.test index 1d1eb5603..40cf0e634 100755 --- a/tests/core/readsave.test +++ b/tests/core/readsave.test @@ -327,21 +327,21 @@ digraph G { subgraph cluster_0 { color=green 1 [label="s1", peripheries=2] + 1 -> 1 [label="a"] } subgraph cluster_1 { color=green 0 [label="s0", peripheries=2] + 0 -> 0 [label="b"] } subgraph cluster_2 { color=black 3 [label="s3"] - } - 0 -> 0 [label="b"] - 1 -> 1 [label="a"] - 2 [label="s2"] - 2 -> 0 [label="b"] 3 -> 1 [label="a"] 3 -> 0 [label="b"] + } + 2 [label="s2"] + 2 -> 0 [label="b"] } EOF diff --git a/tests/core/sccdot.test b/tests/core/sccdot.test index 919467a5d..75ddb3dfd 100755 --- a/tests/core/sccdot.test +++ b/tests/core/sccdot.test @@ -83,67 +83,67 @@ digraph G { color=grey label="" 5 [label="5"] + 5 -> 6 [label="1"] 6 [label="6"] + 6 -> 5 [label="1"] } subgraph cluster_1 { color=grey label="" 0 [label="0"] + 0 -> 0 [label="a & b\n{0,1,2}"] + 0 -> 0 [label="!a & !b\n{2}"] + 0 -> 5 [label="a\n{2}"] } subgraph cluster_2 { color=green label="" 9 [label="9"] + 9 -> 9 [label="!a & b\n{0,2}"] + 9 -> 10 [label="a & b\n{0,1}"] 10 [label="10"] + 10 -> 9 [label="!a & b\n{0,1}"] + 10 -> 10 [label="a & b\n{0,2}"] } subgraph cluster_3 { color=green label="" 8 [label="8"] + 8 -> 8 [label="!a & b\n{0,2}"] + 8 -> 8 [label="a & b\n{0,1}"] + 8 -> 9 [label="1"] } subgraph cluster_4 { color=green label="" 7 [label="7"] + 7 -> 7 [label="!a & b\n{0,1}"] + 7 -> 7 [label="a & b\n{0,2}"] + 7 -> 8 [label="1"] } subgraph cluster_5 { color=black label="" 2 [label="2"] + 2 -> 0 [label="a"] + 2 -> 7 [label="b"] } subgraph cluster_6 { color=red label="" 4 [label="4"] + 4 -> 4 [label="!b\n{1,2}"] + 4 -> 2 [label="b"] } subgraph cluster_7 { color=green label="" 1 [label="1"] - 3 [label="3"] - } - 0 -> 0 [label="a & b\n{0,1,2}"] - 0 -> 0 [label="!a & !b\n{2}"] - 0 -> 5 [label="a\n{2}"] 1 -> 4 [label="b"] 1 -> 3 [label="a & !b"] - 2 -> 0 [label="a"] - 2 -> 7 [label="b"] + 3 [label="3"] 3 -> 1 [label="a & b\n{0,1}"] - 4 -> 4 [label="!b\n{1,2}"] - 4 -> 2 [label="b"] - 5 -> 6 [label="1"] - 6 -> 5 [label="1"] - 7 -> 7 [label="!a & b\n{0,1}"] - 7 -> 7 [label="a & b\n{0,2}"] - 7 -> 8 [label="1"] - 8 -> 8 [label="!a & b\n{0,2}"] - 8 -> 8 [label="a & b\n{0,1}"] - 8 -> 9 [label="1"] - 9 -> 9 [label="!a & b\n{0,2}"] - 9 -> 10 [label="a & b\n{0,1}"] - 10 -> 9 [label="!a & b\n{0,1}"] - 10 -> 10 [label="a & b\n{0,2}"] + } } EOF diff --git a/tests/python/_altscc.ipynb b/tests/python/_altscc.ipynb index 1a5da1624..68964929a 100644 --- a/tests/python/_altscc.ipynb +++ b/tests/python/_altscc.ipynb @@ -15,7 +15,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.5.2+" + "version": "3.5.3" }, "name": "" }, @@ -122,19 +122,19 @@ "\n", "\n", "\n", - "0->0\n", + "0->0\n", "\n", "\n", "a\n", "\n", "\n", - "0->1\n", + "0->1\n", "\n", "\n", "!a\n", "\n", "\n", - "1->1\n", + "1->1\n", "\n", "\n", "b\n", @@ -144,7 +144,7 @@ "\n" ], "text": [ - " *' at 0x7f7620378330> >" + " *' at 0x7faa50350420> >" ] } ], @@ -189,68 +189,73 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", - "Fin(\n", - "\u24ff\n", - ")\n", + "\n", + "Fin(\n", + "\u24ff\n", + ")\n", "cluster_0\n", - "\n", + "\n", "\n", "cluster_1\n", - "\n", + "\n", "\n", "\n", "\n", "-1\n", - "\n", + "\n", "\n", "\n", "I->-1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "-1->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "-1->1\n", - "\n", - "\n", + "\n", + "\n", "\n", - "\n", - "0->-1\n", - "\n", - "\n", - "a\n", - "\u24ff\n", + "\n", + "-1.1\n", + "\n", + "-1.1\n", + "\n", + "\n", + "0->-1.1\n", + "\n", + "\n", + "a\n", + "\u24ff\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "b\n", + "1->1\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7f7620378870> >" + " *' at 0x7faa50350810> >" ] } ], @@ -276,12 +281,14 @@ "''')" ], "language": "python", - "metadata": {}, + "metadata": { + "scrolled": true + }, "outputs": [ { "metadata": {}, "output_type": "pyout", - "prompt_number": 4, + "prompt_number": 5, "svg": [ "\n", "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", - "Fin(\n", - "\u24ff\n", - ")\n", + "\n", + "Fin(\n", + "\u24ff\n", + ")\n", "cluster_0\n", - "\n", + "\n", "\n", "\n", "\n", "-1\n", - "\n", + "\n", "\n", "\n", "I->-1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "-1->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "-1->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a\n", - "\u24ff\n", + "\n", + "\n", + "a\n", + "\u24ff\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", - "\n", - "1->-1\n", - "\n", - "\n", - "b\n", + "\n", + "-1.0\n", + "\n", + "-1.0\n", + "\n", + "\n", + "1->-1.0\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7f7620378390> >" + " *' at 0x7faa50350870> >" ] } ], - "prompt_number": 4 + "prompt_number": 5 }, { "cell_type": "code", @@ -384,7 +396,7 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 5, + "prompt_number": 6, "svg": [ "\n", "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", - "Fin(\n", - "\u24ff\n", - ")\n", + "\n", + "Fin(\n", + "\u24ff\n", + ")\n", "cluster_0\n", - "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!a\n", - "\u24ff\n", + "\n", + "\n", + "!a\n", + "\u24ff\n", "\n", - "\n", - "-1\n", - "\n", + "\n", + "-1.0\n", + "\n", "\n", - "\n", - "1->-1\n", - "\n", - "\n", - "b\n", + "\n", + "1->-1.0\n", + "\n", + "\n", + "b\n", "\n", - "\n", - "-1->0\n", - "\n", - "\n", + "\n", + "-1.0->0\n", + "\n", + "\n", "\n", - "\n", - "-1->1\n", - "\n", - "\n", + "\n", + "-1.0->1\n", + "\n", + "\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7f76203783c0> >" + " *' at 0x7faa503508a0> >" ] } ], - "prompt_number": 5 + "prompt_number": 6 }, { "cell_type": "code", @@ -487,7 +499,7 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 6, + "prompt_number": 7, "svg": [ "\n", "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", - "Fin(\n", - "\u24ff\n", - ")\n", + "\n", + "Fin(\n", + "\u24ff\n", + ")\n", "cluster_0\n", - "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a\n", - "\u24ff\n", + "\n", + "\n", + "a\n", + "\u24ff\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", - "\n", - "-1\n", - "\n", + "\n", + "-1.0\n", + "\n", "\n", - "\n", - "1->-1\n", - "\n", - "\n", - "b\n", - "\u24ff\n", + "\n", + "1->-1.0\n", + "\n", + "\n", + "b\n", + "\u24ff\n", "\n", - "\n", - "-1->0\n", - "\n", - "\n", + "\n", + "-1.0->0\n", + "\n", + "\n", "\n", - "\n", - "-1->1\n", - "\n", - "\n", + "\n", + "-1.0->1\n", + "\n", + "\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7f7620378360> >" + " *' at 0x7faa50350cc0> >" ] } ], - "prompt_number": 6 + "prompt_number": 7 }, { "cell_type": "code", diff --git a/tests/python/decompose.ipynb b/tests/python/decompose.ipynb index 386112577..9f21cc2e2 100644 --- a/tests/python/decompose.ipynb +++ b/tests/python/decompose.ipynb @@ -15,10 +15,9 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.4.3+" + "version": "3.5.3" }, - "name": "", - "signature": "sha256:ddf44352825d3260c20b0a4d29b4972c9cd5be57b3a48bcdf8afe8acaee5eba6" + "name": "" }, "nbformat": 3, "nbformat_minor": 0, @@ -113,7 +112,7 @@ "\n", "\n", "\n", - "1->1\n", + "1->1\n", "\n", "\n", "!a & !c\n", @@ -125,7 +124,7 @@ "0\n", "\n", "\n", - "1->0\n", + "1->0\n", "\n", "\n", "a & b & !c\n", @@ -136,7 +135,7 @@ "3\n", "\n", "\n", - "1->3\n", + "1->3\n", "\n", "\n", "c\n", @@ -147,7 +146,7 @@ "2\n", "\n", "\n", - "1->2\n", + "1->2\n", "\n", "\n", "a & !c\n", @@ -160,7 +159,7 @@ "\u24ff\n", "\n", "\n", - "3->3\n", + "3->3\n", "\n", "\n", "1\n", @@ -172,38 +171,38 @@ "4\n", "\n", "\n", - "4->3\n", + "4->3\n", "\n", "\n", "!a\n", "\n", "\n", - "4->4\n", + "4->4\n", "\n", "\n", "a\n", "\n", "\n", - "2->1\n", + "2->1\n", "\n", "\n", "!a & !c\n", "\u24ff\n", "\n", "\n", - "2->3\n", + "2->3\n", "\n", "\n", "!a & c\n", "\n", "\n", - "2->4\n", + "2->4\n", "\n", "\n", "a & c\n", "\n", "\n", - "2->2\n", + "2->2\n", "\n", "\n", "a & !c\n", @@ -212,7 +211,7 @@ "\n" ], "text": [ - " *' at 0x7f7340048a20> >" + " *' at 0x7fd270264810> >" ] } ], @@ -279,7 +278,7 @@ "\n", "\n", "\n", - "0->0\n", + "0->0\n", "\n", "\n", "!a & !c\n", @@ -290,7 +289,7 @@ "1\n", "\n", "\n", - "0->1\n", + "0->1\n", "\n", "\n", "a & b & !c\n", @@ -301,13 +300,13 @@ "2\n", "\n", "\n", - "0->2\n", + "0->2\n", "\n", "\n", "a & !c\n", "\n", "\n", - "1->1\n", + "1->1\n", "\n", "\n", "b\n", @@ -329,7 +328,7 @@ "\n" ], "text": [ - " *' at 0x7f7340048990> >" + " *' at 0x7fd270264840> >" ] } ], @@ -391,7 +390,7 @@ "\n", "\n", "\n", - "0->0\n", + "0->0\n", "\n", "\n", "!a & !c\n", @@ -402,7 +401,7 @@ "2\n", "\n", "\n", - "0->2\n", + "0->2\n", "\n", "\n", "c\n", @@ -413,13 +412,13 @@ "1\n", "\n", "\n", - "0->1\n", + "0->1\n", "\n", "\n", "a & !c\n", "\n", "\n", - "2->2\n", + "2->2\n", "\n", "\n", "1\n", @@ -431,37 +430,37 @@ "3\n", "\n", "\n", - "3->2\n", + "3->2\n", "\n", "\n", "!a\n", "\n", "\n", - "3->3\n", + "3->3\n", "\n", "\n", "a\n", "\n", "\n", - "1->0\n", + "1->0\n", "\n", "\n", "!a & !c\n", "\n", "\n", - "1->2\n", + "1->2\n", "\n", "\n", "!a & c\n", "\n", "\n", - "1->3\n", + "1->3\n", "\n", "\n", "a & c\n", "\n", "\n", - "1->1\n", + "1->1\n", "\n", "\n", "a & !c\n", @@ -470,7 +469,7 @@ "\n" ], "text": [ - " *' at 0x7f73400489c0> >" + " *' at 0x7fd270264cc0> >" ] } ], @@ -560,7 +559,7 @@ "\n" ], "text": [ - " *' at 0x7f7340048bd0> >" + " *' at 0x7fd270264450> >" ] } ], @@ -637,7 +636,7 @@ "\n" ], "text": [ - " *' at 0x7f734006f3c0> >" + " *' at 0x7fd270264cf0> >" ] } ], @@ -701,7 +700,7 @@ "\n", "\n", "\n", - "0->0\n", + "0->0\n", "\n", "\n", "!a & !c\n", @@ -713,7 +712,7 @@ "1\n", "\n", "\n", - "0->1\n", + "0->1\n", "\n", "\n", "a & b & !c\n", @@ -724,13 +723,13 @@ "2\n", "\n", "\n", - "0->2\n", + "0->2\n", "\n", "\n", "a & !c\n", "\n", "\n", - "1->1\n", + "1->1\n", "\n", "\n", "b\n", @@ -753,7 +752,7 @@ "\n" ], "text": [ - " *' at 0x7f734006f060> >" + " *' at 0x7fd270264270> >" ] }, { @@ -796,7 +795,7 @@ "\n", "\n", "\n", - "0->0\n", + "0->0\n", "\n", "\n", "!a & !c\n", @@ -808,7 +807,7 @@ "2\n", "\n", "\n", - "0->2\n", + "0->2\n", "\n", "\n", "c\n", @@ -819,13 +818,13 @@ "1\n", "\n", "\n", - "0->1\n", + "0->1\n", "\n", "\n", "a & !c\n", "\n", "\n", - "2->2\n", + "2->2\n", "\n", "\n", "1\n", @@ -837,38 +836,38 @@ "3\n", "\n", "\n", - "3->2\n", + "3->2\n", "\n", "\n", "!a\n", "\n", "\n", - "3->3\n", + "3->3\n", "\n", "\n", "a\n", "\n", "\n", - "1->0\n", + "1->0\n", "\n", "\n", "!a & !c\n", "\u24ff\n", "\n", "\n", - "1->2\n", + "1->2\n", "\n", "\n", "!a & c\n", "\n", "\n", - "1->3\n", + "1->3\n", "\n", "\n", "a & c\n", "\n", "\n", - "1->1\n", + "1->1\n", "\n", "\n", "a & !c\n", @@ -877,7 +876,7 @@ "\n" ], "text": [ - " *' at 0x7f734006f3f0> >" + " *' at 0x7fd270264180> >" ] }, { @@ -923,7 +922,7 @@ "\n", "\n", "\n", - "0->0\n", + "0->0\n", "\n", "\n", "!a & !c\n", @@ -934,7 +933,7 @@ "1\n", "\n", "\n", - "0->1\n", + "0->1\n", "\n", "\n", "a & b & !c\n", @@ -945,7 +944,7 @@ "3\n", "\n", "\n", - "0->3\n", + "0->3\n", "\n", "\n", "c\n", @@ -956,20 +955,20 @@ "2\n", "\n", "\n", - "0->2\n", + "0->2\n", "\n", "\n", "a & !c\n", "\n", "\n", - "1->1\n", + "1->1\n", "\n", "\n", "b\n", "\u24ff\n", "\n", "\n", - "3->3\n", + "3->3\n", "\n", "\n", "1\n", @@ -981,37 +980,37 @@ "4\n", "\n", "\n", - "4->3\n", + "4->3\n", "\n", "\n", "!a\n", "\n", "\n", - "4->4\n", + "4->4\n", "\n", "\n", "a\n", "\n", "\n", - "2->0\n", + "2->0\n", "\n", "\n", "!a & !c\n", "\n", "\n", - "2->3\n", + "2->3\n", "\n", "\n", "!a & c\n", "\n", "\n", - "2->4\n", + "2->4\n", "\n", "\n", "a & c\n", "\n", "\n", - "2->2\n", + "2->2\n", "\n", "\n", "a & !c\n", @@ -1020,7 +1019,7 @@ "\n" ], "text": [ - " *' at 0x7f734006f060> >" + " *' at 0x7fd2702642d0> >" ] } ], @@ -1173,7 +1172,7 @@ "\u2777\n", "\n", "\n", - "2->6\n", + "2->6\n", "\n", "\n", "c\n", @@ -1186,7 +1185,7 @@ "\u2777\n", "\n", "\n", - "2->5\n", + "2->5\n", "\n", "\n", "!a & !c\n", @@ -1199,7 +1198,7 @@ "\u2777\n", "\n", "\n", - "2->3\n", + "2->3\n", "\n", "\n", "a & !b & !c\n", @@ -1212,16 +1211,16 @@ "\u2777\n", "\n", "\n", - "2->4\n", + "2->4\n", "\n", "\n", "a & b & !c\n", "\n", "\n", - "6->6\n", + "6->6\n", "\n", "\n", - "1\n", + "1\n", "\n", "\n", "1\n", @@ -1230,13 +1229,13 @@ "\u2777\n", "\n", "\n", - "1->6\n", + "1->6\n", "\n", "\n", "!a\n", "\n", "\n", - "1->1\n", + "1->1\n", "\n", "\n", "a\n", @@ -1248,19 +1247,19 @@ "\u2778\n", "\n", "\n", - "8->6\n", + "8->6\n", "\n", "\n", "!a\n", "\n", "\n", - "8->1\n", + "8->1\n", "\n", "\n", "a & !b\n", "\n", "\n", - "8->8\n", + "8->8\n", "\n", "\n", "a & b\n", @@ -1272,43 +1271,43 @@ "\u2777\n", "\n", "\n", - "0->6\n", + "0->6\n", "\n", "\n", "!a & c\n", "\n", "\n", - "0->1\n", + "0->1\n", "\n", "\n", "a & c\n", "\n", "\n", - "0->0\n", + "0->0\n", "\n", "\n", "a & !c\n", "\n", "\n", - "0->5\n", + "0->5\n", "\n", "\n", "!a & !c\n", "\n", "\n", - "5->6\n", + "5->6\n", "\n", "\n", "c\n", "\n", "\n", - "5->0\n", + "5->0\n", "\n", "\n", "a & !b & !c\n", "\n", "\n", - "5->5\n", + "5->5\n", "\n", "\n", "!a & !c\n", @@ -1320,103 +1319,103 @@ "\u2778\n", "\n", "\n", - "5->7\n", + "5->7\n", "\n", "\n", "a & b & !c\n", "\n", "\n", - "7->6\n", + "7->6\n", "\n", "\n", "!a & c\n", "\n", "\n", - "7->1\n", + "7->1\n", "\n", "\n", "a & !b & c\n", "\n", "\n", - "7->8\n", + "7->8\n", "\n", "\n", "a & b & c\n", "\n", "\n", - "7->0\n", + "7->0\n", "\n", "\n", "a & !b & !c\n", "\n", "\n", - "7->5\n", + "7->5\n", "\n", "\n", "!a & !c\n", "\n", "\n", - "7->7\n", + "7->7\n", "\n", "\n", "a & b & !c\n", "\n", "\n", - "3->6\n", + "3->6\n", "\n", "\n", "!a & c\n", "\n", "\n", - "3->1\n", + "3->1\n", "\n", "\n", "a & c\n", "\n", "\n", - "3->0\n", + "3->0\n", "\n", "\n", "a & !c\n", "\n", "\n", - "3->5\n", + "3->5\n", "\n", "\n", "!a & !c\n", "\n", "\n", - "4->6\n", + "4->6\n", "\n", "\n", "!a & c\n", "\n", "\n", - "4->1\n", + "4->1\n", "\n", "\n", "a & !b & c\n", "\n", "\n", - "4->8\n", + "4->8\n", "\n", "\n", "a & b & c\n", "\n", "\n", - "4->0\n", + "4->0\n", "\n", "\n", "a & !b & !c\n", "\n", "\n", - "4->5\n", + "4->5\n", "\n", "\n", "!a & !c\n", "\n", "\n", - "4->7\n", + "4->7\n", "\n", "\n", "a & b & !c\n", @@ -1425,7 +1424,7 @@ "\n" ], "text": [ - " *' at 0x7f734006f090> >" + " *' at 0x7fd270264180> >" ] } ], @@ -1508,7 +1507,7 @@ "\u24ff\n", "\n", "\n", - "0->4\n", + "0->4\n", "\n", "\n", "c\n", @@ -1519,7 +1518,7 @@ "3\n", "\n", "\n", - "0->3\n", + "0->3\n", "\n", "\n", "!a & !c\n", @@ -1527,10 +1526,10 @@ "\n", "1\n", "\n", - "1\n", + "1\n", "\n", "\n", - "0->1\n", + "0->1\n", "\n", "\n", "a & !b & !c\n", @@ -1541,16 +1540,16 @@ "2\n", "\n", "\n", - "0->2\n", + "0->2\n", "\n", "\n", "a & b & !c\n", "\n", "\n", - "4->4\n", + "4->4\n", "\n", "\n", - "1\n", + "1\n", "\n", "\n", "7\n", @@ -1558,13 +1557,13 @@ "7\n", "\n", "\n", - "7->4\n", + "7->4\n", "\n", "\n", "!a\n", "\n", "\n", - "7->7\n", + "7->7\n", "\n", "\n", "a\n", @@ -1575,19 +1574,19 @@ "8\n", "\n", "\n", - "8->4\n", + "8->4\n", "\n", "\n", "!a\n", "\n", "\n", - "8->7\n", + "8->7\n", "\n", "\n", "a & !b\n", "\n", "\n", - "8->8\n", + "8->8\n", "\n", "\n", "a & b\n", @@ -1598,43 +1597,43 @@ "5\n", "\n", "\n", - "5->4\n", + "5->4\n", "\n", "\n", "!a & c\n", "\n", "\n", - "5->7\n", + "5->7\n", "\n", "\n", "a & c\n", "\n", "\n", - "5->5\n", + "5->5\n", "\n", "\n", "a & !c\n", "\n", "\n", - "5->3\n", - "\n", - "\n", - "!a & !c\n", + "5->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "3->4\n", + "3->4\n", "\n", "\n", "c\n", "\n", "\n", - "3->5\n", + "3->5\n", "\n", "\n", "a & !b & !c\n", "\n", "\n", - "3->3\n", + "3->3\n", "\n", "\n", "!a & !c\n", @@ -1645,103 +1644,103 @@ "6\n", "\n", "\n", - "3->6\n", + "3->6\n", "\n", "\n", "a & b & !c\n", "\n", "\n", - "6->4\n", + "6->4\n", "\n", "\n", "!a & c\n", "\n", "\n", - "6->7\n", + "6->7\n", "\n", "\n", "a & !b & c\n", "\n", "\n", - "6->8\n", + "6->8\n", "\n", "\n", "a & b & c\n", "\n", "\n", - "6->5\n", + "6->5\n", "\n", "\n", "a & !b & !c\n", "\n", "\n", - "6->3\n", + "6->3\n", "\n", "\n", "!a & !c\n", "\n", "\n", - "6->6\n", + "6->6\n", "\n", "\n", "a & b & !c\n", "\n", "\n", - "1->4\n", + "1->4\n", "\n", "\n", "!a & c\n", "\n", "\n", - "1->7\n", + "1->7\n", "\n", "\n", "a & c\n", "\n", "\n", - "1->5\n", + "1->5\n", "\n", "\n", "a & !c\n", "\n", "\n", - "1->3\n", + "1->3\n", "\n", "\n", "!a & !c\n", "\n", "\n", - "2->4\n", + "2->4\n", "\n", "\n", "!a & c\n", "\n", "\n", - "2->7\n", + "2->7\n", "\n", "\n", "a & !b & c\n", "\n", "\n", - "2->8\n", + "2->8\n", "\n", "\n", "a & b & c\n", "\n", "\n", - "2->5\n", + "2->5\n", "\n", "\n", "a & !b & !c\n", "\n", "\n", - "2->3\n", + "2->3\n", "\n", "\n", "!a & !c\n", "\n", "\n", - "2->6\n", + "2->6\n", "\n", "\n", "a & b & !c\n", @@ -1750,7 +1749,7 @@ "\n" ], "text": [ - " *' at 0x7f734006f0c0> >" + " *' at 0x7fd270264db0> >" ] }, { @@ -1763,191 +1762,191 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", - "strictly weak\n", - "Inf(\n", - "\u24ff\n", - ")\n", + "\n", + "strictly weak\n", + "Inf(\n", + "\u24ff\n", + ")\n", "cluster_0\n", - "\n", + "\n", "\n", "cluster_1\n", - "\n", + "\n", "\n", "cluster_2\n", - "\n", + "\n", "\n", "cluster_3\n", - "\n", + "\n", "\n", "cluster_4\n", - "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", - "0->3\n", - "\n", - "\n", - "!a & !c\n", + "0->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a & !b & !c\n", + "0->1\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "a & b & !c\n", + "0->2\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", "6\n", - "\n", - "6\n", - "\u24ff\n", + "\n", + "6\n", + "\u24ff\n", "\n", "\n", - "6->6\n", - "\n", - "\n", - "a & b\n", + "6->6\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", - "4->4\n", - "\n", - "\n", - "a & !c\n", + "4->4\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", - "4->3\n", - "\n", - "\n", - "!a & !c\n", + "4->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "3->4\n", - "\n", - "\n", - "a & !b & !c\n", + "3->4\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "!a & !c\n", + "3->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", - "3->5\n", - "\n", - "\n", - "a & b & !c\n", + "3->5\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "5->6\n", - "\n", - "\n", - "a & b & c\n", + "5->6\n", + "\n", + "\n", + "a & b & c\n", "\n", "\n", - "5->4\n", - "\n", - "\n", - "a & !b & !c\n", + "5->4\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "5->3\n", - "\n", - "\n", - "!a & !c\n", + "5->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "5->5\n", - "\n", - "\n", - "a & b & !c\n", + "5->5\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "1->4\n", - "\n", - "\n", - "a & !c\n", + "1->4\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", - "1->3\n", - "\n", - "\n", - "!a & !c\n", + "1->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "2->6\n", - "\n", - "\n", - "a & b & c\n", + "2->6\n", + "\n", + "\n", + "a & b & c\n", "\n", "\n", - "2->4\n", - "\n", - "\n", - "a & !b & !c\n", + "2->4\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "2->3\n", - "\n", - "\n", - "!a & !c\n", + "2->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "2->5\n", - "\n", - "\n", - "a & b & !c\n", + "2->5\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7f734006f060> >" + " *' at 0x7fd270264390> >" ] }, { @@ -1961,173 +1960,173 @@ " -->\n", "\n", "\n", - "\n", + " viewBox=\"0.00 0.00 713.36 244.63\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", + "\n", "G\n", - "\n", - "strong\n", - "(Fin(\n", - "\u24ff\n", - ") & Inf(\n", - "\u2776\n", - ")) | (Fin(\n", - "\u2777\n", - ") & Inf(\n", - "\u2778\n", - "))\n", + "\n", + "strong\n", + "(Fin(\n", + "\u24ff\n", + ") & Inf(\n", + "\u2776\n", + ")) | (Fin(\n", + "\u2777\n", + ") & Inf(\n", + "\u2778\n", + "))\n", "cluster_0\n", - "\n", + "\n", "\n", "cluster_1\n", - "\n", + "\n", "\n", "cluster_2\n", - "\n", + "\n", "\n", "cluster_3\n", - "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "3\n", - "\n", - "3\n", - "\u2776\n", - "\u2777\n", + "\n", + "3\n", + "\u2776\n", + "\u2777\n", "\n", "\n", - "0->3\n", - "\n", - "\n", - "!a & !c\n", + "0->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a & !b & !c\n", + "0->1\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "a & b & !c\n", + "0->2\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", "4\n", - "\n", - "4\n", - "\u2777\n", + "\n", + "4\n", + "\u2777\n", "\n", "\n", - "4->4\n", - "\n", - "\n", - "a & !c\n", + "4->4\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", - "4->3\n", - "\n", - "\n", - "!a & !c\n", + "4->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "3->4\n", - "\n", - "\n", - "a & !b & !c\n", + "3->4\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "!a & !c\n", + "3->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", "5\n", - "\n", - "5\n", - "\u2778\n", + "\n", + "5\n", + "\u2778\n", "\n", "\n", - "3->5\n", - "\n", - "\n", - "a & b & !c\n", + "3->5\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "5->4\n", - "\n", - "\n", - "a & !b & !c\n", + "5->4\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "5->3\n", - "\n", - "\n", - "!a & !c\n", + "5->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "5->5\n", - "\n", - "\n", - "a & b & !c\n", + "5->5\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "1->4\n", - "\n", - "\n", - "a & !c\n", + "1->4\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", - "1->3\n", - "\n", - "\n", - "!a & !c\n", + "1->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "2->4\n", - "\n", - "\n", - "a & !b & !c\n", + "2->4\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "2->3\n", - "\n", - "\n", - "!a & !c\n", + "2->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "2->5\n", - "\n", - "\n", - "a & b & !c\n", + "2->5\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7f734006f0c0> >" + " *' at 0x7fd270264270> >" ] } ], @@ -2216,7 +2215,7 @@ "\u2777\n", "\n", "\n", - "0->4\n", + "0->4\n", "\n", "\n", "c\n", @@ -2229,7 +2228,7 @@ "\u2777\n", "\n", "\n", - "0->3\n", + "0->3\n", "\n", "\n", "!a & !c\n", @@ -2237,10 +2236,10 @@ "\n", "1\n", "\n", - "1\n", + "1\n", "\n", "\n", - "0->1\n", + "0->1\n", "\n", "\n", "a & !b & !c\n", @@ -2251,16 +2250,16 @@ "2\n", "\n", "\n", - "0->2\n", + "0->2\n", "\n", "\n", "a & b & !c\n", "\n", "\n", - "4->4\n", + "4->4\n", "\n", "\n", - "1\n", + "1\n", "\n", "\n", "7\n", @@ -2268,13 +2267,13 @@ "7\n", "\n", "\n", - "7->4\n", + "7->4\n", "\n", "\n", "!a\n", "\n", "\n", - "7->7\n", + "7->7\n", "\n", "\n", "a\n", @@ -2285,19 +2284,19 @@ "8\n", "\n", "\n", - "8->4\n", + "8->4\n", "\n", "\n", "!a\n", "\n", "\n", - "8->7\n", + "8->7\n", "\n", "\n", "a & !b\n", "\n", "\n", - "8->8\n", + "8->8\n", "\n", "\n", "a & b\n", @@ -2309,43 +2308,43 @@ "\u2777\n", "\n", "\n", - "5->4\n", + "5->4\n", "\n", "\n", "!a & c\n", "\n", "\n", - "5->7\n", + "5->7\n", "\n", "\n", "a & c\n", "\n", "\n", - "5->5\n", + "5->5\n", "\n", "\n", "a & !c\n", "\n", "\n", - "5->3\n", - "\n", - "\n", - "!a & !c\n", + "5->3\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "3->4\n", + "3->4\n", "\n", "\n", "c\n", "\n", "\n", - "3->5\n", + "3->5\n", "\n", "\n", "a & !b & !c\n", "\n", "\n", - "3->3\n", + "3->3\n", "\n", "\n", "!a & !c\n", @@ -2357,103 +2356,103 @@ "\u2778\n", "\n", "\n", - "3->6\n", + "3->6\n", "\n", "\n", "a & b & !c\n", "\n", "\n", - "6->4\n", + "6->4\n", "\n", "\n", "!a & c\n", "\n", "\n", - "6->7\n", + "6->7\n", "\n", "\n", "a & !b & c\n", "\n", "\n", - "6->8\n", + "6->8\n", "\n", "\n", "a & b & c\n", "\n", "\n", - "6->5\n", + "6->5\n", "\n", "\n", "a & !b & !c\n", "\n", "\n", - "6->3\n", + "6->3\n", "\n", "\n", "!a & !c\n", "\n", "\n", - "6->6\n", + "6->6\n", "\n", "\n", "a & b & !c\n", "\n", "\n", - "1->4\n", + "1->4\n", "\n", "\n", "!a & c\n", "\n", "\n", - "1->7\n", + "1->7\n", "\n", "\n", "a & c\n", "\n", "\n", - "1->5\n", + "1->5\n", "\n", "\n", "a & !c\n", "\n", "\n", - "1->3\n", + "1->3\n", "\n", "\n", "!a & !c\n", "\n", "\n", - "2->4\n", + "2->4\n", "\n", "\n", "!a & c\n", "\n", "\n", - "2->7\n", + "2->7\n", "\n", "\n", "a & !b & c\n", "\n", "\n", - "2->8\n", + "2->8\n", "\n", "\n", "a & b & c\n", "\n", "\n", - "2->5\n", + "2->5\n", "\n", "\n", "a & !b & !c\n", "\n", "\n", - "2->3\n", + "2->3\n", "\n", "\n", "!a & !c\n", "\n", "\n", - "2->6\n", + "2->6\n", "\n", "\n", "a & b & !c\n", @@ -2462,7 +2461,7 @@ "\n" ], "text": [ - " *' at 0x7f734006fbd0> >" + " *' at 0x7fd270264e40> >" ] } ], @@ -2559,12 +2558,12 @@ "0->0\n", "\n", "\n", - "1\n", + "1\n", "\n", "\n", "1\n", "\n", - "1\n", + "1\n", "\n", "\n", "1->0\n", @@ -2606,7 +2605,7 @@ "\n" ], "text": [ - " *' at 0x7f734006ff60> >" + " *' at 0x7fd2702fd4b0> >" ] }, { @@ -2646,7 +2645,7 @@ "\n", "\n", "\n", - "2->2\n", + "2->2\n", "\n", "\n", "!a & !c\n", @@ -2657,10 +2656,10 @@ "1\n", "\n", "\n", - "2->1\n", - "\n", - "\n", - "a & !b & !c\n", + "2->1\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", "3\n", @@ -2668,7 +2667,7 @@ "3\n", "\n", "\n", - "2->3\n", + "2->3\n", "\n", "\n", "a & b & !c\n", @@ -2686,13 +2685,13 @@ "a & b\n", "\n", "\n", - "1->2\n", - "\n", - "\n", - "!a & !c\n", + "1->2\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "1->1\n", + "1->1\n", "\n", "\n", "a & !c\n", @@ -2725,7 +2724,7 @@ "\n" ], "text": [ - " *' at 0x7f734006fcc0> >" + " *' at 0x7fd270264d80> >" ] }, { @@ -2784,7 +2783,7 @@ "\u2777\n", "\n", "\n", - "0->3\n", + "0->3\n", "\n", "\n", "!a & !c\n", @@ -2795,7 +2794,7 @@ "1\n", "\n", "\n", - "0->1\n", + "0->1\n", "\n", "\n", "a & !b & !c\n", @@ -2806,13 +2805,13 @@ "2\n", "\n", "\n", - "0->2\n", + "0->2\n", "\n", "\n", "a & b & !c\n", "\n", "\n", - "3->3\n", + "3->3\n", "\n", "\n", "!a & !c\n", @@ -2824,7 +2823,7 @@ "\u2777\n", "\n", "\n", - "3->4\n", + "3->4\n", "\n", "\n", "a & !b & !c\n", @@ -2836,67 +2835,67 @@ "\u2778\n", "\n", "\n", - "3->5\n", + "3->5\n", "\n", "\n", "a & b & !c\n", "\n", "\n", - "4->3\n", + "4->3\n", "\n", "\n", "!a & !c\n", "\n", "\n", - "4->4\n", + "4->4\n", "\n", "\n", "a & !c\n", "\n", "\n", - "5->3\n", + "5->3\n", "\n", "\n", "!a & !c\n", "\n", "\n", - "5->4\n", + "5->4\n", "\n", "\n", "a & !b & !c\n", "\n", "\n", - "5->5\n", + "5->5\n", "\n", "\n", "a & b & !c\n", "\n", "\n", - "1->3\n", + "1->3\n", "\n", "\n", "!a & !c\n", "\n", "\n", - "1->4\n", + "1->4\n", "\n", "\n", "a & !c\n", "\n", "\n", - "2->3\n", + "2->3\n", "\n", "\n", "!a & !c\n", "\n", "\n", - "2->4\n", + "2->4\n", "\n", "\n", "a & !b & !c\n", "\n", "\n", - "2->5\n", + "2->5\n", "\n", "\n", "a & b & !c\n", @@ -2905,7 +2904,7 @@ "\n" ], "text": [ - " *' at 0x7f734006f6c0> >" + " *' at 0x7fd270264870> >" ] } ], @@ -3035,7 +3034,7 @@ "\n", "\n", "\n", - "7->7\n", + "7->7\n", "\n", "\n", "!a & !c\n", @@ -3048,7 +3047,7 @@ "\u2778\n", "\n", "\n", - "7->4\n", + "7->4\n", "\n", "\n", "c\n", @@ -3060,28 +3059,28 @@ "\u2777\n", "\n", "\n", - "7->2\n", + "7->2\n", "\n", "\n", "a & !b & !c\n", "\n", "\n", - "6\n", + "6\n", "\n", "6\n", "\u2778\n", "\n", "\n", - "7->6\n", + "7->6\n", "\n", "\n", "a & b & !c\n", "\n", "\n", - "4->4\n", + "4->4\n", "\n", "\n", - "1\n", + "1\n", "\n", "\n", "3\n", @@ -3091,13 +3090,13 @@ "\u2778\n", "\n", "\n", - "3->4\n", + "3->4\n", "\n", "\n", "!a\n", "\n", "\n", - "3->3\n", + "3->3\n", "\n", "\n", "a\n", @@ -3109,19 +3108,19 @@ "\u2777\n", "\n", "\n", - "0->4\n", + "0->4\n", "\n", "\n", "!a\n", "\n", "\n", - "0->3\n", + "0->3\n", "\n", "\n", "a & !b\n", "\n", "\n", - "0->0\n", + "0->0\n", "\n", "\n", "a & b\n", @@ -3133,136 +3132,136 @@ "\u2778\n", "\n", "\n", - "5->4\n", + "5->4\n", "\n", "\n", "!a\n", "\n", "\n", - "5->3\n", + "5->3\n", "\n", "\n", "a & !b\n", "\n", "\n", - "5->5\n", + "5->5\n", "\n", "\n", "a & b\n", "\n", "\n", - "2->7\n", - "\n", - "\n", - "!a & !c\n", + "2->7\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "2->4\n", + "2->4\n", "\n", "\n", "!a & c\n", "\n", "\n", - "2->3\n", + "2->3\n", "\n", "\n", "a & c\n", "\n", "\n", - "2->2\n", + "2->2\n", "\n", "\n", "a & !b & !c\n", "\n", "\n", - "1\n", + "1\n", "\n", "1\n", "\u2777\n", "\n", "\n", - "2->1\n", + "2->1\n", "\n", "\n", "a & b & !c\n", "\n", - "\n", - "1->7\n", - "\n", - "\n", - "!a & !c\n", - "\n", - "\n", - "1->4\n", - "\n", - "\n", - "!a & c\n", - "\n", - "\n", - "1->3\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "a & b & c\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "a & b & !c\n", - "\n", "\n", - "6->7\n", - "\n", - "\n", - "!a & !c\n", + "6->7\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "6->4\n", + "6->4\n", "\n", "\n", "!a & c\n", "\n", "\n", - "6->3\n", + "6->3\n", "\n", "\n", "a & !b & c\n", "\n", "\n", - "6->5\n", + "6->5\n", "\n", "\n", "a & b & c\n", "\n", "\n", - "6->2\n", + "6->2\n", "\n", "\n", "a & !b & !c\n", "\n", "\n", - "6->6\n", + "6->6\n", "\n", "\n", "a & b & !c\n", "\n", + "\n", + "1->7\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & b & !c\n", + "\n", "\n", "\n" ], "text": [ - " *' at 0x7f733338d0f0> >" + " *' at 0x7fd270281180> >" ] } ], @@ -3327,7 +3326,7 @@ "\n", "\n", "\n", - "0->0\n", + "0->0\n", "\n", "\n", "!a & !c\n", @@ -3339,7 +3338,7 @@ "\u24ff\n", "\n", "\n", - "0->2\n", + "0->2\n", "\n", "\n", "c\n", @@ -3351,28 +3350,28 @@ "\u2777\n", "\n", "\n", - "0->1\n", + "0->1\n", "\n", "\n", "a & !b & !c\n", "\n", "\n", - "3\n", + "3\n", "\n", "3\n", "\u2777\n", "\n", "\n", - "0->3\n", + "0->3\n", "\n", "\n", "a & b & !c\n", "\n", "\n", - "2->2\n", + "2->2\n", "\n", "\n", - "1\n", + "1\n", "\n", "\n", "4\n", @@ -3381,13 +3380,13 @@ "\u2777\n", "\n", "\n", - "4->2\n", + "4->2\n", "\n", "\n", "!a\n", "\n", "\n", - "4->4\n", + "4->4\n", "\n", "\n", "a\n", @@ -3399,19 +3398,19 @@ "\u2777\n", "\n", "\n", - "7->2\n", + "7->2\n", "\n", "\n", "!a\n", "\n", "\n", - "7->4\n", + "7->4\n", "\n", "\n", "a & !b\n", "\n", "\n", - "7->7\n", + "7->7\n", "\n", "\n", "a & b\n", @@ -3423,136 +3422,136 @@ "\u2777\n", "\n", "\n", - "5->2\n", + "5->2\n", "\n", "\n", "!a\n", "\n", "\n", - "5->4\n", + "5->4\n", "\n", "\n", "a & !b\n", "\n", "\n", - "5->5\n", + "5->5\n", "\n", "\n", "a & b\n", "\n", "\n", - "1->0\n", + "1->0\n", "\n", "\n", "!a & !c\n", "\n", "\n", - "1->2\n", + "1->2\n", "\n", "\n", "!a & c\n", "\n", "\n", - "1->4\n", + "1->4\n", "\n", "\n", "a & c\n", "\n", "\n", - "1->1\n", + "1->1\n", "\n", "\n", "a & !b & !c\n", "\n", "\n", - "6\n", + "6\n", "\n", "6\n", "\u2777\n", "\n", "\n", - "1->6\n", + "1->6\n", "\n", "\n", "a & b & !c\n", "\n", - "\n", - "6->0\n", - "\n", - "\n", - "!a & !c\n", - "\n", - "\n", - "6->2\n", - "\n", - "\n", - "!a & c\n", - "\n", - "\n", - "6->4\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", - "6->7\n", - "\n", - "\n", - "a & b & c\n", - "\n", - "\n", - "6->1\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", - "\n", - "6->6\n", - "\n", - "\n", - "a & b & !c\n", - "\n", "\n", - "3->0\n", + "3->0\n", "\n", "\n", "!a & !c\n", "\n", "\n", - "3->2\n", + "3->2\n", "\n", "\n", "!a & c\n", "\n", "\n", - "3->4\n", + "3->4\n", "\n", "\n", "a & !b & c\n", "\n", "\n", - "3->5\n", + "3->5\n", "\n", "\n", "a & b & c\n", "\n", "\n", - "3->1\n", + "3->1\n", "\n", "\n", "a & !b & !c\n", "\n", "\n", - "3->3\n", + "3->3\n", "\n", "\n", "a & b & !c\n", "\n", + "\n", + "6->0\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "6->2\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "6->4\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "6->7\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "6->1\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "6->6\n", + "\n", + "\n", + "a & b & !c\n", + "\n", "\n", "\n" ], "text": [ - " *' at 0x7f733338d090> >" + " *' at 0x7fd270281120> >" ] }, { @@ -3593,7 +3592,7 @@ "\n", "\n", "\n", - "0->0\n", + "0->0\n", "\n", "\n", "!a & !c\n", @@ -3605,22 +3604,22 @@ "\u2777\n", "\n", "\n", - "0->1\n", + "0->1\n", "\n", "\n", "a & !b & !c\n", "\n", "\n", - "2\n", + "2\n", "\n", "2\n", "\u2777\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "a & b & !c\n", + "0->2\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", "3\n", @@ -3629,82 +3628,82 @@ "\u24ff\n", "\n", "\n", - "3->3\n", + "3->3\n", "\n", "\n", "a & b\n", "\n", "\n", - "1->0\n", + "1->0\n", "\n", "\n", "!a & !c\n", "\n", "\n", - "1->1\n", + "1->1\n", "\n", "\n", "a & !b & !c\n", "\n", "\n", - "4\n", + "4\n", "\n", "4\n", "\u2777\n", "\n", "\n", - "1->4\n", + "1->4\n", "\n", "\n", "a & b & !c\n", "\n", - "\n", - "4->0\n", - "\n", - "\n", - "!a & !c\n", - "\n", - "\n", - "4->1\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", - "\n", - "4->4\n", - "\n", - "\n", - "a & b & !c\n", - "\n", "\n", - "2->0\n", - "\n", - "\n", - "!a & !c\n", + "2->0\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "2->3\n", + "2->3\n", "\n", "\n", "a & b & c\n", "\n", "\n", - "2->1\n", + "2->1\n", "\n", "\n", "a & !b & !c\n", "\n", "\n", - "2->2\n", + "2->2\n", "\n", "\n", "a & b & !c\n", "\n", + "\n", + "4->0\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "4->1\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "a & b & !c\n", + "\n", "\n", "\n" ], "text": [ - " *' at 0x7f734006f6c0> >" + " *' at 0x7fd270264360> >" ] }, { @@ -3738,110 +3737,110 @@ "\n", "\n", "0\n", - "\n", - "0\n", - "\u2778\n", + "\n", + "0\n", + "\u2778\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!a & !c\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", "1\n", - "\n", - "1\n", - "\u2777\n", + "\n", + "1\n", + "\u2777\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a & !b & !c\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "2\n", - "\n", - "2\n", - "\u2778\n", + "2\n", + "\n", + "2\n", + "\u2778\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "a & b & !c\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "!a & !c\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & !b & !c\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "3\n", - "\n", - "3\n", - "\u2777\n", + "3\n", + "\n", + "3\n", + "\u2777\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "a & b & !c\n", - "\n", - "\n", - "3->0\n", - "\n", - "\n", - "!a & !c\n", - "\n", - "\n", - "3->1\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "a & b & !c\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "2->0\n", - "\n", - "\n", - "!a & !c\n", + "2->0\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "2->1\n", - "\n", - "\n", - "a & !b & !c\n", + "2->1\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "a & b & !c\n", + "2->2\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7f733338d090> >" + " *' at 0x7fd270264d80> >" ] } ], @@ -3918,7 +3917,7 @@ "\n", "\n", "\n", - "0->0\n", + "0->0\n", "\n", "\n", "!a & !c\n", @@ -3931,7 +3930,7 @@ "\u2778\n", "\n", "\n", - "0->2\n", + "0->2\n", "\n", "\n", "c\n", @@ -3943,28 +3942,28 @@ "\u2777\n", "\n", "\n", - "0->1\n", + "0->1\n", "\n", "\n", "a & !b & !c\n", "\n", "\n", - "3\n", + "3\n", "\n", "3\n", "\u2778\n", "\n", "\n", - "0->3\n", + "0->3\n", "\n", "\n", "a & b & !c\n", "\n", "\n", - "2->2\n", + "2->2\n", "\n", "\n", - "1\n", + "1\n", "\n", "\n", "4\n", @@ -3973,13 +3972,13 @@ "\u2777\n", "\n", "\n", - "4->2\n", + "4->2\n", "\n", "\n", "!a\n", "\n", "\n", - "4->4\n", + "4->4\n", "\n", "\n", "a\n", @@ -3991,19 +3990,19 @@ "\u2777\n", "\n", "\n", - "7->2\n", + "7->2\n", "\n", "\n", "!a\n", "\n", "\n", - "7->4\n", + "7->4\n", "\n", "\n", "a & !b\n", "\n", "\n", - "7->7\n", + "7->7\n", "\n", "\n", "a & b\n", @@ -4015,136 +4014,136 @@ "\u2777\n", "\n", "\n", - "5->2\n", + "5->2\n", "\n", "\n", "!a\n", "\n", "\n", - "5->4\n", + "5->4\n", "\n", "\n", "a & !b\n", "\n", "\n", - "5->5\n", + "5->5\n", "\n", "\n", "a & b\n", "\n", "\n", - "1->0\n", + "1->0\n", "\n", "\n", "!a & !c\n", "\n", "\n", - "1->2\n", + "1->2\n", "\n", "\n", "!a & c\n", "\n", "\n", - "1->4\n", + "1->4\n", "\n", "\n", "a & c\n", "\n", "\n", - "1->1\n", + "1->1\n", "\n", "\n", "a & !b & !c\n", "\n", "\n", - "6\n", + "6\n", "\n", "6\n", "\u2777\n", "\n", "\n", - "1->6\n", + "1->6\n", "\n", "\n", "a & b & !c\n", "\n", - "\n", - "6->0\n", - "\n", - "\n", - "!a & !c\n", - "\n", - "\n", - "6->2\n", - "\n", - "\n", - "!a & c\n", - "\n", - "\n", - "6->4\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", - "6->7\n", - "\n", - "\n", - "a & b & c\n", - "\n", - "\n", - "6->1\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", - "\n", - "6->6\n", - "\n", - "\n", - "a & b & !c\n", - "\n", "\n", - "3->0\n", + "3->0\n", "\n", "\n", "!a & !c\n", "\n", "\n", - "3->2\n", + "3->2\n", "\n", "\n", "!a & c\n", "\n", "\n", - "3->4\n", + "3->4\n", "\n", "\n", "a & !b & c\n", "\n", "\n", - "3->5\n", + "3->5\n", "\n", "\n", "a & b & c\n", "\n", "\n", - "3->1\n", + "3->1\n", "\n", "\n", "a & !b & !c\n", "\n", "\n", - "3->3\n", + "3->3\n", "\n", "\n", "a & b & !c\n", "\n", + "\n", + "6->0\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "6->2\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "6->4\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "6->7\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "6->1\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "6->6\n", + "\n", + "\n", + "a & b & !c\n", + "\n", "\n", "\n" ], "text": [ - " *' at 0x7f733338d1e0> >" + " *' at 0x7fd270281240> >" ] } ], @@ -4212,7 +4211,7 @@ "\n", "\n", "\n", - "0->0\n", + "0->0\n", "\n", "\n", "a & !c\n", @@ -4223,7 +4222,7 @@ "1\n", "\n", "\n", - "0->1\n", + "0->1\n", "\n", "\n", "a & c\n", @@ -4234,19 +4233,19 @@ "2\n", "\n", "\n", - "0->2\n", + "0->2\n", "\n", "\n", "a & b & !c\n", "\n", "\n", - "1->1\n", + "1->1\n", "\n", "\n", "1\n", "\n", "\n", - "2->2\n", + "2->2\n", "\n", "\n", "b\n", @@ -4255,7 +4254,7 @@ "\n" ], "text": [ - " *' at 0x7f733338d360> >" + " *' at 0x7fd270281870> >" ] } ], @@ -4320,7 +4319,7 @@ "\n", "\n", "\n", - "0->0\n", + "0->0\n", "\n", "\n", "a & !c\n", @@ -4338,7 +4337,7 @@ "a & b & !c\n", "\n", "\n", - "1->1\n", + "1->1\n", "\n", "\n", "b\n", @@ -4347,7 +4346,7 @@ "\n" ], "text": [ - " *' at 0x7f733338d3c0> >" + " *' at 0x7fd270264270> >" ] }, { @@ -4386,7 +4385,7 @@ "\n", "\n", "\n", - "0->0\n", + "0->0\n", "\n", "\n", "a & !c\n", @@ -4404,7 +4403,7 @@ "a & c\n", "\n", "\n", - "1->1\n", + "1->1\n", "\n", "\n", "1\n", @@ -4413,7 +4412,7 @@ "\n" ], "text": [ - " *' at 0x7f733338d3c0> >" + " *' at 0x7fd270264270> >" ] } ], @@ -4472,7 +4471,7 @@ "\n", "\n", "\n", - "0->0\n", + "0->0\n", "\n", "\n", "a & !c\n", @@ -4490,7 +4489,7 @@ "a & c\n", "\n", "\n", - "1->1\n", + "1->1\n", "\n", "\n", "1\n", @@ -4499,7 +4498,7 @@ "\n" ], "text": [ - " *' at 0x7f733338d420> >" + " *' at 0x7fd270264300> >" ] } ], @@ -4592,7 +4591,7 @@ "\n", "\n", "\n", - "0->0\n", + "0->0\n", "\n", "\n", "a\n", @@ -4603,7 +4602,7 @@ "1\n", "\n", "\n", - "0->1\n", + "0->1\n", "\n", "\n", "!a\n", @@ -4614,14 +4613,14 @@ "3\n", "\n", "\n", - "3->3\n", + "3->3\n", "\n", "\n", "1\n", "\u24ff\n", "\n", "\n", - "1->1\n", + "1->1\n", "\n", "\n", "a\n", @@ -4632,20 +4631,20 @@ "2\n", "\n", "\n", - "1->2\n", + "1->2\n", "\n", "\n", "!a\n", "\u24ff\n", "\n", "\n", - "2->3\n", + "2->3\n", "\n", "\n", "!a\n", "\n", "\n", - "2->1\n", + "2->1\n", "\n", "\n", "a\n", @@ -4654,7 +4653,7 @@ "\n" ], "text": [ - " *' at 0x7f733338d4b0> >" + " *' at 0x7fd270264420> >" ] } ], @@ -4722,7 +4721,7 @@ "\n", "\n", "\n", - "0->0\n", + "0->0\n", "\n", "\n", "a\n", @@ -4733,7 +4732,7 @@ "1\n", "\n", "\n", - "0->1\n", + "0->1\n", "\n", "\n", "!a\n", @@ -4744,14 +4743,14 @@ "3\n", "\n", "\n", - "3->3\n", + "3->3\n", "\n", "\n", "1\n", "\u24ff\n", "\n", "\n", - "1->1\n", + "1->1\n", "\n", "\n", "a\n", @@ -4762,19 +4761,19 @@ "2\n", "\n", "\n", - "1->2\n", + "1->2\n", "\n", "\n", "!a\n", "\n", "\n", - "2->3\n", + "2->3\n", "\n", "\n", "!a\n", "\n", "\n", - "2->1\n", + "2->1\n", "\n", "\n", "a\n", @@ -4783,7 +4782,7 @@ "\n" ], "text": [ - " *' at 0x7f734006f6c0> >" + " *' at 0x7fd270264ed0> >" ] }, { @@ -4823,7 +4822,7 @@ "\n", "\n", "\n", - "0->0\n", + "0->0\n", "\n", "\n", "a\n", @@ -4835,14 +4834,14 @@ "1\n", "\n", "\n", - "0->1\n", + "0->1\n", "\n", "\n", "!a\n", "\u24ff\n", "\n", "\n", - "1->1\n", + "1->1\n", "\n", "\n", "a\n", @@ -4854,14 +4853,14 @@ "2\n", "\n", "\n", - "1->2\n", + "1->2\n", "\n", "\n", "!a\n", "\u24ff\n", "\n", "\n", - "2->1\n", + "2->1\n", "\n", "\n", "a\n", @@ -4871,7 +4870,7 @@ "\n" ], "text": [ - " *' at 0x7f734006fc60> >" + " *' at 0x7fd270264ea0> >" ] }, { @@ -4921,7 +4920,7 @@ "\n", "\n", "\n", - "0->0\n", + "0->0\n", "\n", "\n", "a\n", @@ -4933,7 +4932,7 @@ "1\n", "\n", "\n", - "0->1\n", + "0->1\n", "\n", "\n", "!a\n", @@ -4945,14 +4944,14 @@ "3\n", "\n", "\n", - "3->3\n", + "3->3\n", "\n", "\n", "1\n", "\u24ff\n", "\n", "\n", - "1->1\n", + "1->1\n", "\n", "\n", "a\n", @@ -4964,21 +4963,21 @@ "2\n", "\n", "\n", - "1->2\n", + "1->2\n", "\n", "\n", "!a\n", "\u24ff\n", "\n", "\n", - "2->3\n", + "2->3\n", "\n", "\n", "!a\n", "\u24ff\n", "\n", "\n", - "2->1\n", + "2->1\n", "\n", "\n", "a\n", @@ -4988,7 +4987,7 @@ "\n" ], "text": [ - " *' at 0x7f734006fc60> >" + " *' at 0x7fd270264330> >" ] } ], @@ -5001,10 +5000,19 @@ "language": "python", "metadata": {}, "outputs": [], - "prompt_number": 20 + "prompt_number": null + }, + { + "cell_type": "code", + "collapsed": true, + "input": [], + "language": "python", + "metadata": {}, + "outputs": [], + "prompt_number": null } ], "metadata": {} } ] -} \ No newline at end of file +}