From 7b6cfd448c29319d9ddcc7e854c62f821dd1d738 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 31 May 2017 17:14:52 +0200 Subject: [PATCH] dot: fix printing of alternating automata Related to #208. * spot/twaalgos/dot.cc: Fix missing definitions of universal nodes, and inclusion of universal nodes inside of SCC when none of the destination comes back to the SCC. * tests/python/_altscc.ipynb: Adjust and add more test cases. * tests/core/alternating.test, tests/core/neverclaimread.test, tests/core/readsave.test, tests/core/sccdot.test, tests/python/decompose.ipynb: Adjust test cases. * NEWS: Mention the bug. --- NEWS | 5 + spot/twaalgos/dot.cc | 211 +++-- tests/core/alternating.test | 220 ++--- tests/core/neverclaimread.test | 8 +- tests/core/readsave.test | 8 +- tests/core/sccdot.test | 42 +- tests/python/_altscc.ipynb | 717 ++++++++++++--- tests/python/decompose.ipynb | 1536 ++++++++++++++++---------------- 8 files changed, 1593 insertions(+), 1154 deletions(-) diff --git a/NEWS b/NEWS index a939abeac..86bb18e02 100644 --- a/NEWS +++ b/NEWS @@ -6,6 +6,11 @@ New in spot 2.3.4.dev (not yet released) single ltl2tgba run could produce automata different from those produced by individual runs. + - The print_dot() function had a couple of issues when printing + alternating automata: in particular, when using flag 's' (display + SCC) or 'y' (split universal destination by colors) universal + edges could be connected to undefined states. + New in spot 2.3.4 (2017-05-11) Bugs fixed: diff --git a/spot/twaalgos/dot.cc b/spot/twaalgos/dot.cc index fd1d7e263..a71b9fddb 100644 --- a/spot/twaalgos/dot.cc +++ b/spot/twaalgos/dot.cc @@ -69,6 +69,8 @@ namespace spot std::vector>* sprod_ = nullptr; std::set* incomplete_ = nullptr; std::string* name_ = nullptr; + std::map, int> univ_done; + acc_cond::mark_t inf_sets_ = 0U; acc_cond::mark_t fin_sets_ = 0U; unsigned opt_shift_sets_ = 0; @@ -366,28 +368,39 @@ namespace spot return bdd_format_formula(aut_->get_dict(), label); } - std::set> done; - - void - print_dst(int dst, const char* style = nullptr, int scc_num = -1, - int color_num = -1) + std::string string_dst(int dst, int color_num = -1) { std::ostringstream tmp_dst; tmp_dst << dst; - if (scc_num >= 0) - tmp_dst << '.' << scc_num; - if (!done.emplace(std::make_pair(dst, color_num)).second) - return; - else if (!opt_shared_univ_dest_ && color_num > 0) + if (!opt_shared_univ_dest_ && color_num >= 0) tmp_dst << '.' << color_num; - std::string dest = tmp_dst.str(); - os_ << " " << dest << " [label=<>,shape=point]\n"; - for (unsigned d: aut_->univ_dests(dst)) + return tmp_dst.str(); + } + + void + print_dst(int dst, bool print_edges = false, + const char* style = nullptr, int color_num = -1) + { + int& univ = univ_done[std::make_pair(dst, color_num)]; + if (univ == 2) + return; + std::string dest = string_dst(dst, color_num); + if (univ == 0) + os_ << " " << dest << " [label=<>,shape=point]\n"; + if (print_edges) { - os_ << " " << dest << " -> " << d; - if (style && *style) - os_ << " [" << style << ']'; - os_ << '\n'; + for (unsigned d: aut_->univ_dests(dst)) + { + os_ << " " << dest << " -> " << d; + if (style && *style) + os_ << " [" << style << ']'; + os_ << '\n'; + } + univ = 2; + } + else + { + univ = 1; } } @@ -478,14 +491,9 @@ namespace spot int init = (int) aut_->get_init_state_number(); os_ << "=0]\n I -> " << init; if (init >= 0) - { - os_ << '\n'; - } + os_ << '\n'; else - { - os_ << " [arrowhead=onormal]\n"; - print_dst(init); - } + os_ << " [arrowhead=onormal]\n"; } void @@ -586,63 +594,63 @@ namespace spot void process_link(const twa_graph::edge_storage_t& t, int number, - int scc_num = -1) + bool print_edges) { - os_ << " " << t.src << " -> " << (int)t.dst; - if (scc_num >= 0) + if (print_edges) { - os_ << '.' << scc_num; - } - if (aut_->is_univ_dest(t.dst) && highlight_edges_ - && !opt_shared_univ_dest_) - { - auto idx = aut_->get_graph().index_of_edge(t); - auto iter = highlight_edges_->find(idx); - os_ << '.' << iter->second % palette_mod; - } - std::string label; - if (!opt_state_labels_) - label = bdd_format_formula(aut_->get_dict(), t.cond); - if (!opt_html_labels_) - { - os_ << " [label=\""; - escape_str(os_, label); - if (!mark_states_) - if (auto a = t.acc) - { - if (!opt_state_labels_) - os_ << "\\n"; - output_set(a); - } - os_ << '"'; - } - else - { - os_ << " [label=<"; - escape_html(os_, label); - if (!mark_states_) - if (auto a = t.acc) - { - if (!opt_state_labels_) - os_ << "
"; - output_html_set(a); - } - os_ << '>'; - } - if (opt_ordered_edges_ || opt_numbered_edges_) - { - os_ << ", taillabel=\""; - if (opt_ordered_edges_) - os_ << number; - if (opt_ordered_edges_ && opt_numbered_edges_) - os_ << ' '; - if (opt_numbered_edges_) - os_ << '#' << aut_->get_graph().index_of_edge(t); - os_ << '"'; + os_ << " " << t.src << " -> " << (int)t.dst; + if (aut_->is_univ_dest(t.dst) && highlight_edges_ + && !opt_shared_univ_dest_) + { + auto idx = aut_->get_graph().index_of_edge(t); + auto iter = highlight_edges_->find(idx); + if (iter != highlight_edges_->end()) + os_ << '.' << iter->second % palette_mod; + } + std::string label; + if (!opt_state_labels_) + label = bdd_format_formula(aut_->get_dict(), t.cond); + if (!opt_html_labels_) + { + os_ << " [label=\""; + escape_str(os_, label); + if (!mark_states_) + if (auto a = t.acc) + { + if (!opt_state_labels_) + os_ << "\\n"; + output_set(a); + } + os_ << '"'; + } + else + { + os_ << " [label=<"; + escape_html(os_, label); + if (!mark_states_) + if (auto a = t.acc) + { + if (!opt_state_labels_) + os_ << "
"; + output_html_set(a); + } + os_ << '>'; + } + if (opt_ordered_edges_ || opt_numbered_edges_) + { + os_ << ", taillabel=\""; + if (opt_ordered_edges_) + os_ << number; + if (opt_ordered_edges_ && opt_numbered_edges_) + os_ << ' '; + if (opt_numbered_edges_) + os_ << '#' << aut_->get_graph().index_of_edge(t); + os_ << '"'; + } } std::string highlight; - auto color_num = -1; + int color_num = -1; if (highlight_edges_) { auto idx = aut_->get_graph().index_of_edge(t); @@ -654,21 +662,20 @@ namespace spot << palette[iter->second % palette_mod] << '"'; highlight = o.str(); - os_ << ", " << highlight; + if (print_edges) + os_ << ", " << highlight; if (!opt_shared_univ_dest_) color_num = iter->second % palette_mod; } } - if (aut_->is_univ_dest(t.dst)) - os_ << ", arrowhead=onormal"; - os_ << "]\n"; - if (aut_->is_univ_dest(t.dst)) + if (print_edges) { - if (color_num >= 0) - print_dst(t.dst, highlight.c_str(), scc_num, color_num); - else - print_dst(t.dst, highlight.c_str(), scc_num); + if (aut_->is_univ_dest(t.dst)) + os_ << ", arrowhead=onormal"; + os_ << "]\n"; } + if (aut_->is_univ_dest(t.dst)) + print_dst(t.dst, print_edges, highlight.c_str(), color_num); } void print(const const_twa_graph_ptr& aut) @@ -773,39 +780,29 @@ namespace spot { process_state(s); int trans_num = 0; + unsigned scc_of_s = si->scc_of(s); for (auto& t : aut_->out(s)) - { - if (aut_->is_univ_dest(t.dst)) + for (unsigned d: aut_->univ_dests(t.dst)) + if (si->scc_of(d) == scc_of_s) { - 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++); + process_link(t, trans_num++, false); + break; } - else - process_link(t, trans_num++); - } } os_ << " }\n"; } } + int init = (int) aut_->get_init_state_number(); + if (init < 0) + print_dst(init, true); unsigned ns = aut_->num_states(); 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++, true); } end(); } diff --git a/tests/core/alternating.test b/tests/core/alternating.test index 6b51c42a5..a0878c310 100755 --- a/tests/core/alternating.test +++ b/tests/core/alternating.test @@ -62,66 +62,66 @@ digraph G { labelloc="t" I [label="", style=invis, width=0] I -> -11 [arrowhead=onormal] - -11 [label=<>,shape=point] - -11 -> 0 - -11 -> 2 subgraph cluster_0 { 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"] + -8 [label=<>,shape=point] } 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 - -1 -> 3 - 0 -> -4 [label="a & !b", style=bold, color="#F15854", arrowhead=onormal] - -4 [label=<>,shape=point] - -4 -> 1 [style=bold, color="#F15854"] - -4 -> 3 [style=bold, color="#F15854"] - -4 -> 5 [style=bold, color="#F15854"] } + -11 [label=<>,shape=point] + -11 -> 0 + -11 -> 2 + 0 -> -1 [label="b", arrowhead=onormal] + -1 [label=<>,shape=point] + -1 -> 1 + -1 -> 3 + 0 -> -4 [label="a & !b", style=bold, color="#F15854", arrowhead=onormal] + -4 [label=<>,shape=point] + -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 -> 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 @@ -508,19 +508,19 @@ digraph G { edge [fontname="Lato"] I [label="", style=invis, width=0] I -> -1 [arrowhead=onormal] - -1 [label=<>,shape=point] - -1 -> 0 - -1 -> 1 + -1 [label=<>,shape=point] + -1 -> 0 + -1 -> 1 0 [label=<0>] 0 -> 0 [label=] 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"] + -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", $style] - -1.2 [label=<>,shape=point] - -1.2 -> 0 [style=bold, color="#FAA43A"] - -1.2 -> 1 [style=bold, color="#FAA43A"] + -1.2 [label=<>,shape=point] + -1.2 -> 0 [style=bold, color="#FAA43A"] + -1.2 -> 1 [style=bold, color="#FAA43A"] 1 [label=<1>] 1 -> 1 [label=] } @@ -574,52 +574,52 @@ digraph G { color=green label="" 4 [label="t"] - 4 -> 4 [label=<1>] } subgraph cluster_1 { color=green label="" 1 [label="G(a & b)"] - 1 -> 1 [label=] } subgraph cluster_2 { color=red label="" 2 [label="F!a"] - 2 -> 4 [label=] - 2 -> 2 [label=❶>] } subgraph cluster_3 { color=red label="" 3 [label="F!b"] - 3 -> 4 [label=] - 3 -> 3 [label=⓿>] } subgraph cluster_4 { color=green label="" 0 [label="c R (c | G(a & b) | (F!b & F!a))"] + -1 [label=<>,shape=point] + -4 [label=<>,shape=point] + -7 [label=<>,shape=point] + -10 [label=<>,shape=point] + } 0 -> 4 [label=] 0 -> 0 [label=] - 0 -> -1.4 [label=, arrowhead=onormal] - -1.4 [label=<>,shape=point] - -1.4 -> 0 - -1.4 -> 1 - 0 -> -4.4 [label=, arrowhead=onormal] - -4.4 [label=<>,shape=point] - -4.4 -> 0 - -4.4 -> 2 - 0 -> -7.4 [label=, arrowhead=onormal] - -7.4 [label=<>,shape=point] - -7.4 -> 0 - -7.4 -> 3 - 0 -> -10.4 [label=, arrowhead=onormal] - -10.4 [label=<>,shape=point] - -10.4 -> 0 - -10.4 -> 2 - -10.4 -> 3 - } + 0 -> -1 [label=, arrowhead=onormal] + -1 -> 0 + -1 -> 1 + 0 -> -4 [label=, arrowhead=onormal] + -4 -> 0 + -4 -> 2 + 0 -> -7 [label=, arrowhead=onormal] + -7 -> 0 + -7 -> 3 + 0 -> -10 [label=, arrowhead=onormal] + -10 -> 0 + -10 -> 2 + -10 -> 3 + 1 -> 1 [label=] + 2 -> 4 [label=] + 2 -> 2 [label=❶>] + 3 -> 4 [label=] + 3 -> 3 [label=⓿>] + 4 -> 4 [label=<1>] } EOF @@ -670,48 +670,48 @@ digraph G { color=green label="" 4 [label="t"] - 4 -> 4 [label=<1>] } subgraph cluster_1 { color=red label="" 2 [label="F!a"] - 2 -> 4 [label=] - 2 -> 2 [label=❶>] } subgraph cluster_2 { color=red label="" 3 [label="F!b"] - 3 -> 4 [label=] - 3 -> 3 [label=⓿>] } subgraph cluster_3 { color=green label="" 0 [label="c R (c | G(a & b) | (F!b & F!a))"] + -1 [label=<>,shape=point] + -4 [label=<>,shape=point] + -7 [label=<>,shape=point] + 1 [label="G(a & b)"] + -10 [label=<>,shape=point] + } 0 -> 4 [label=] 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 - 0 -> -7.3 [label=, arrowhead=onormal] - -7.3 [label=<>,shape=point] - -7.3 -> 0 - -7.3 -> 3 - 1 [label="G(a & b)"] + 0 -> -1 [label=, arrowhead=onormal] + -1 -> 0 + -1 -> 1 + 0 -> -4 [label=, arrowhead=onormal] + -4 -> 0 + -4 -> 2 + 0 -> -7 [label=, arrowhead=onormal] + -7 -> 0 + -7 -> 3 1 -> 1 [label=] - 1 -> -10.3 [label=, arrowhead=onormal] - -10.3 [label=<>,shape=point] - -10.3 -> 0 - -10.3 -> 2 - -10.3 -> 3 - } + 1 -> -10 [label=, arrowhead=onormal] + -10 -> 0 + -10 -> 2 + -10 -> 3 + 2 -> 4 [label=] + 2 -> 2 [label=❶>] + 3 -> 4 [label=] + 3 -> 3 [label=⓿>] + 4 -> 4 [label=<1>] } EOF @@ -749,16 +749,16 @@ digraph G { I -> 0 0 [label=<0>] 0 -> -1.1 [label=, style=bold, color="#F17CB0", arrowhead=onormal] - -1.1 [label=<>,shape=point] - -1.1 -> 1 [style=bold, color="#F17CB0"] - -1.1 -> 2 [style=bold, color="#F17CB0"] + -1.1 [label=<>,shape=point] + -1.1 -> 1 [style=bold, color="#F17CB0"] + -1.1 -> 2 [style=bold, color="#F17CB0"] 1 [label=<1>] 1 -> -1.1 [label=, style=bold, color="#F17CB0", arrowhead=onormal] 2 [label=<2>] 2 -> -1.2 [label=, style=bold, color="#FAA43A", $style] - -1.2 [label=<>,shape=point] - -1.2 -> 1 [style=bold, color="#FAA43A"] - -1.2 -> 2 [style=bold, color="#FAA43A"] + -1.2 [label=<>,shape=point] + -1.2 -> 1 [style=bold, color="#FAA43A"] + -1.2 -> 2 [style=bold, color="#FAA43A"] } EOF @@ -796,19 +796,19 @@ digraph G { I -> 0 0 [label=<0>] 0 -> -1.1 [label=, style=bold, color="#F17CB0", arrowhead=onormal] - -1.1 [label=<>,shape=point] - -1.1 -> 1 [style=bold, color="#F17CB0"] - -1.1 -> 2 [style=bold, color="#F17CB0"] + -1.1 [label=<>,shape=point] + -1.1 -> 1 [style=bold, color="#F17CB0"] + -1.1 -> 2 [style=bold, color="#F17CB0"] 1 [label=<1>] 1 -> -1.3 [label=, style=bold, color="#B276B2", arrowhead=onormal] - -1.3 [label=<>,shape=point] - -1.3 -> 1 [style=bold, color="#B276B2"] - -1.3 -> 2 [style=bold, color="#B276B2"] + -1.3 [label=<>,shape=point] + -1.3 -> 1 [style=bold, color="#B276B2"] + -1.3 -> 2 [style=bold, color="#B276B2"] 2 [label=<2>] 2 -> -1.2 [label=, style=bold, color="#FAA43A", $style] - -1.2 [label=<>,shape=point] - -1.2 -> 1 [style=bold, color="#FAA43A"] - -1.2 -> 2 [style=bold, color="#FAA43A"] + -1.2 [label=<>,shape=point] + -1.2 -> 1 [style=bold, color="#FAA43A"] + -1.2 -> 2 [style=bold, color="#FAA43A"] } EOF @@ -853,35 +853,35 @@ digraph G { 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 + -1 [label=<>,shape=point] + -4 [label=<>,shape=point] } + 0 -> 0 [label=] + 0 -> -1 [label=, arrowhead=onormal] + -1 -> 0 + -1 -> 1 + 0 -> -4 [label=, arrowhead=onormal] + -4 -> 0 + -4 -> 2 + 1 -> 3 [label=] + 1 -> 1 [label=] + 2 -> 2 [label=] + 3 -> 3 [label=<1>] } EOF diff --git a/tests/core/neverclaimread.test b/tests/core/neverclaimread.test index e2f80f92e..1dd675afe 100755 --- a/tests/core/neverclaimread.test +++ b/tests/core/neverclaimread.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de -# Recherche et Développement de l'Epita (LRDE). +# Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2017 Laboratoire +# de Recherche et Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -336,15 +336,15 @@ digraph G { color=green label="" 1 [label="1", peripheries=2] - 1 -> 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 0fd2efe60..9da8a8a49 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"] - 3 -> 1 [label="a"] - 3 -> 0 [label="b"] } + 0 -> 0 [label="b"] + 1 -> 1 [label="a"] 2 [label="s2"] 2 -> 0 [label="b"] + 3 -> 1 [label="a"] + 3 -> 0 [label="b"] } EOF diff --git a/tests/core/sccdot.test b/tests/core/sccdot.test index 75ddb3dfd..919467a5d 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"] - 3 [label="3"] + 2 -> 0 [label="a"] + 2 -> 7 [label="b"] 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 68964929a..4fd410b24 100644 --- a/tests/python/_altscc.ipynb +++ b/tests/python/_altscc.ipynb @@ -35,6 +35,7 @@ "cell_type": "code", "collapsed": true, "input": [ + "from IPython.display import display\n", "import spot\n", "spot.setup(show_default='.bas')" ], @@ -77,74 +78,74 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", - "Inf(\n", - "\u24ff\n", - ")\n", + "\n", + "Inf(\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", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "-1->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "1\n", + "\n", + "1\n", "\n", "\n", "-1->1\n", - "\n", - "\n", + "\n", + "\n", "\n", - "\n", - "0->0\n", - "\n", - "\n", - "a\n", + "\n", + "0\n", + "\n", + "0\n", "\n", - "\n", - "0->1\n", - "\n", - "\n", - "!a\n", + "\n", + "-1->0\n", + "\n", + "\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "b\n", - "\u24ff\n", + "1->1\n", + "\n", + "\n", + "b\n", + "\u24ff\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7faa50350420> >" + " *' at 0x7f1946fe0e40> >" ] } ], @@ -189,73 +190,68 @@ "\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", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "-1->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "1\n", + "\n", + "1\n", "\n", "\n", "-1->1\n", - "\n", - "\n", + "\n", + "\n", "\n", - "\n", - "-1.1\n", - "\n", - "-1.1\n", + "\n", + "0\n", + "\n", + "0\n", "\n", - "\n", - "0->-1.1\n", - "\n", - "\n", - "a\n", - "\u24ff\n", + "\n", + "-1->0\n", + "\n", + "\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "b\n", + "1->1\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "0->-1\n", + "\n", + "\n", + "a\n", + "\u24ff\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7faa50350810> >" + " *' at 0x7f1946fe05a0> >" ] } ], @@ -288,7 +284,7 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 5, + "prompt_number": 4, "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", @@ -324,18 +320,18 @@ "\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", @@ -346,30 +342,25 @@ "\n", "\n", "0->1\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", - "\n", - "-1.0\n", - "\n", - "-1.0\n", - "\n", - "\n", - "1->-1.0\n", - "\n", - "\n", - "b\n", + "\n", + "1->-1\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7faa50350870> >" + " *' at 0x7f1946fe05d0> >" ] } ], - "prompt_number": 5 + "prompt_number": 4 }, { "cell_type": "code", @@ -396,7 +387,7 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 6, + "prompt_number": 5, "svg": [ "\n", "!a\n", "\u24ff\n", "\n", - "\n", - "-1.0\n", + "\n", + "-1\n", "\n", "\n", - "\n", - "1->-1.0\n", + "\n", + "1->-1\n", "\n", "\n", "b\n", "\n", - "\n", - "-1.0->0\n", + "\n", + "-1->0\n", "\n", "\n", "\n", - "\n", - "-1.0->1\n", + "\n", + "-1->1\n", "\n", "\n", "\n", @@ -468,11 +459,11 @@ "\n" ], "text": [ - " *' at 0x7faa503508a0> >" + " *' at 0x7f1946fe0660> >" ] } ], - "prompt_number": 6 + "prompt_number": 5 }, { "cell_type": "code", @@ -499,7 +490,7 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 7, + "prompt_number": 6, "svg": [ "\n", "\n", "!a\n", "\n", - "\n", - "-1.0\n", + "\n", + "-1\n", "\n", "\n", - "\n", - "1->-1.0\n", + "\n", + "1->-1\n", "\n", "\n", "b\n", "\u24ff\n", "\n", - "\n", - "-1.0->0\n", + "\n", + "-1->0\n", "\n", "\n", "\n", - "\n", - "-1.0->1\n", + "\n", + "-1->1\n", "\n", "\n", "\n", @@ -572,11 +563,457 @@ "\n" ], "text": [ - " *' at 0x7faa50350cc0> >" + " *' at 0x7f1946fe0570> >" ] } ], - "prompt_number": 7 + "prompt_number": 6 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "A corner case for the dot printer" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "for a in spot.automata('''\n", + "HOA: v1\n", + "States: 3\n", + "Start: 0\n", + "AP: 2 \"a\" \"b\"\n", + "Acceptance: 1 Fin(0)\n", + "--BODY--\n", + "State: 0\n", + "[0] 1&2\n", + "State: 1\n", + "[1] 1&2 {0}\n", + "State: 2\n", + "[1] 2\n", + "--END--\n", + "HOA: v1\n", + "States: 3\n", + "Start: 0\n", + "AP: 2 \"a\" \"b\"\n", + "Acceptance: 1 Fin(0)\n", + "--BODY--\n", + "State: 0\n", + "[0] 1&2\n", + "State: 1\n", + "[1] 1 {0}\n", + "State: 2\n", + "[1] 2\n", + "--END--\n", + "'''):\n", + " display(a)\n", + "\n", + "a = spot.automaton('''\n", + "HOA: v1\n", + "States: 3\n", + "Start: 0&2\n", + "AP: 2 \"a\" \"b\"\n", + "Acceptance: 1 Fin(0)\n", + "spot.highlight.edges: 2 2\n", + "--BODY--\n", + "State: 0\n", + "[0] 1&2\n", + "State: 1\n", + "[1] 1&2 {0}\n", + "State: 2\n", + "[1] 1&2\n", + "--END--\n", + "''')\n", + "display(a, a.show('.basy'))" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Fin(\n", + "\u24ff\n", + ")\n", + "cluster_0\n", + "\n", + "\n", + "cluster_1\n", + "\n", + "\n", + "cluster_2\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "-1\n", + "\n", + "\n", + "\n", + "0->-1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "1->-1\n", + "\n", + "\n", + "b\n", + "\u24ff\n", + "\n", + "\n", + "-1->2\n", + "\n", + "\n", + "\n", + "\n", + "-1->1\n", + "\n", + "\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7f1946f72c00> >" + ] + }, + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Fin(\n", + "\u24ff\n", + ")\n", + "cluster_0\n", + "\n", + "\n", + "cluster_1\n", + "\n", + "\n", + "cluster_2\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "-1\n", + "\n", + "\n", + "\n", + "0->-1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "b\n", + "\u24ff\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "-1->1\n", + "\n", + "\n", + "\n", + "\n", + "-1->2\n", + "\n", + "\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7f1946f72870> >" + ] + }, + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Fin(\n", + "\u24ff\n", + ")\n", + "cluster_0\n", + "\n", + "\n", + "cluster_1\n", + "\n", + "\n", + "\n", + "\n", + "-4\n", + "\n", + "\n", + "\n", + "I->-4\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "-4->2\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "-4->0\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "-1\n", + "\n", + "\n", + "\n", + "1->-1\n", + "\n", + "\n", + "b\n", + "\u24ff\n", + "\n", + "\n", + "-1->1\n", + "\n", + "\n", + "\n", + "\n", + "-1->2\n", + "\n", + "\n", + "\n", + "\n", + "2->-1\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "0->-1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7f1946f72c00> >" + ] + }, + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "Fin(\n", + "\u24ff\n", + ")\n", + "cluster_0\n", + "\n", + "\n", + "cluster_1\n", + "\n", + "\n", + "\n", + "\n", + "-4\n", + "\n", + "\n", + "\n", + "I->-4\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "-4->2\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "-4->0\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "-1.2\n", + "\n", + "\n", + "\n", + "1->-1.2\n", + "\n", + "\n", + "b\n", + "\u24ff\n", + "\n", + "\n", + "-1.2->1\n", + "\n", + "\n", + "\n", + "\n", + "-1.2->2\n", + "\n", + "\n", + "\n", + "\n", + "-1\n", + "\n", + "\n", + "\n", + "2->-1\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "-1->1\n", + "\n", + "\n", + "\n", + "\n", + "-1->2\n", + "\n", + "\n", + "\n", + "\n", + "0->-1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + } + ], + "prompt_number": 9 }, { "cell_type": "code", diff --git a/tests/python/decompose.ipynb b/tests/python/decompose.ipynb index 9f21cc2e2..68ea84c15 100644 --- a/tests/python/decompose.ipynb +++ b/tests/python/decompose.ipynb @@ -112,7 +112,7 @@ "\n", "\n", "\n", - "1->1\n", + "1->1\n", "\n", "\n", "!a & !c\n", @@ -124,7 +124,7 @@ "0\n", "\n", "\n", - "1->0\n", + "1->0\n", "\n", "\n", "a & b & !c\n", @@ -135,7 +135,7 @@ "3\n", "\n", "\n", - "1->3\n", + "1->3\n", "\n", "\n", "c\n", @@ -146,7 +146,7 @@ "2\n", "\n", "\n", - "1->2\n", + "1->2\n", "\n", "\n", "a & !c\n", @@ -159,7 +159,7 @@ "\u24ff\n", "\n", "\n", - "3->3\n", + "3->3\n", "\n", "\n", "1\n", @@ -171,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", @@ -211,7 +211,7 @@ "\n" ], "text": [ - " *' at 0x7fd270264810> >" + " *' at 0x7fa1681b0690> >" ] } ], @@ -278,7 +278,7 @@ "\n", "\n", "\n", - "0->0\n", + "0->0\n", "\n", "\n", "!a & !c\n", @@ -289,7 +289,7 @@ "1\n", "\n", "\n", - "0->1\n", + "0->1\n", "\n", "\n", "a & b & !c\n", @@ -300,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", @@ -328,7 +328,7 @@ "\n" ], "text": [ - " *' at 0x7fd270264840> >" + " *' at 0x7fa1681b0660> >" ] } ], @@ -390,7 +390,7 @@ "\n", "\n", "\n", - "0->0\n", + "0->0\n", "\n", "\n", "!a & !c\n", @@ -401,7 +401,7 @@ "2\n", "\n", "\n", - "0->2\n", + "0->2\n", "\n", "\n", "c\n", @@ -412,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", @@ -430,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", @@ -469,7 +469,7 @@ "\n" ], "text": [ - " *' at 0x7fd270264cc0> >" + " *' at 0x7fa1681b03f0> >" ] } ], @@ -559,7 +559,7 @@ "\n" ], "text": [ - " *' at 0x7fd270264450> >" + " *' at 0x7fa1681b0510> >" ] } ], @@ -636,7 +636,7 @@ "\n" ], "text": [ - " *' at 0x7fd270264cf0> >" + " *' at 0x7fa1681b0ed0> >" ] } ], @@ -700,7 +700,7 @@ "\n", "\n", "\n", - "0->0\n", + "0->0\n", "\n", "\n", "!a & !c\n", @@ -712,7 +712,7 @@ "1\n", "\n", "\n", - "0->1\n", + "0->1\n", "\n", "\n", "a & b & !c\n", @@ -723,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", @@ -752,7 +752,7 @@ "\n" ], "text": [ - " *' at 0x7fd270264270> >" + " *' at 0x7fa1681b05a0> >" ] }, { @@ -795,7 +795,7 @@ "\n", "\n", "\n", - "0->0\n", + "0->0\n", "\n", "\n", "!a & !c\n", @@ -807,7 +807,7 @@ "2\n", "\n", "\n", - "0->2\n", + "0->2\n", "\n", "\n", "c\n", @@ -818,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", @@ -836,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", @@ -876,7 +876,7 @@ "\n" ], "text": [ - " *' at 0x7fd270264180> >" + " *' at 0x7fa1681b05d0> >" ] }, { @@ -922,7 +922,7 @@ "\n", "\n", "\n", - "0->0\n", + "0->0\n", "\n", "\n", "!a & !c\n", @@ -933,7 +933,7 @@ "1\n", "\n", "\n", - "0->1\n", + "0->1\n", "\n", "\n", "a & b & !c\n", @@ -944,7 +944,7 @@ "3\n", "\n", "\n", - "0->3\n", + "0->3\n", "\n", "\n", "c\n", @@ -955,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", @@ -980,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", @@ -1019,7 +1019,7 @@ "\n" ], "text": [ - " *' at 0x7fd2702642d0> >" + " *' at 0x7fa1681b0e70> >" ] } ], @@ -1172,7 +1172,7 @@ "\u2777\n", "\n", "\n", - "2->6\n", + "2->6\n", "\n", "\n", "c\n", @@ -1185,7 +1185,7 @@ "\u2777\n", "\n", "\n", - "2->5\n", + "2->5\n", "\n", "\n", "!a & !c\n", @@ -1198,7 +1198,7 @@ "\u2777\n", "\n", "\n", - "2->3\n", + "2->3\n", "\n", "\n", "a & !b & !c\n", @@ -1211,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", @@ -1229,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", @@ -1247,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", @@ -1271,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", @@ -1319,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", @@ -1424,7 +1424,7 @@ "\n" ], "text": [ - " *' at 0x7fd270264180> >" + " *' at 0x7fa1681b04b0> >" ] } ], @@ -1507,7 +1507,7 @@ "\u24ff\n", "\n", "\n", - "0->4\n", + "0->4\n", "\n", "\n", "c\n", @@ -1518,7 +1518,7 @@ "3\n", "\n", "\n", - "0->3\n", + "0->3\n", "\n", "\n", "!a & !c\n", @@ -1526,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", @@ -1540,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", @@ -1557,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", @@ -1574,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", @@ -1597,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", @@ -1644,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", @@ -1749,7 +1749,7 @@ "\n" ], "text": [ - " *' at 0x7fd270264db0> >" + " *' at 0x7fa16814e420> >" ] }, { @@ -1762,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 0x7fd270264390> >" + " *' at 0x7fa1681b0540> >" ] }, { @@ -1960,173 +1960,173 @@ " -->\n", "\n", "\n", - "\n", + " viewBox=\"0.00 0.00 713.36 244.72\" 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 0x7fd270264270> >" + " *' at 0x7fa1681b0360> >" ] } ], @@ -2215,7 +2215,7 @@ "\u2777\n", "\n", "\n", - "0->4\n", + "0->4\n", "\n", "\n", "c\n", @@ -2228,7 +2228,7 @@ "\u2777\n", "\n", "\n", - "0->3\n", + "0->3\n", "\n", "\n", "!a & !c\n", @@ -2236,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", @@ -2250,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", @@ -2267,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", @@ -2284,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", @@ -2308,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", @@ -2356,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", @@ -2461,7 +2461,7 @@ "\n" ], "text": [ - " *' at 0x7fd270264e40> >" + " *' at 0x7fa1681b03c0> >" ] } ], @@ -2558,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", @@ -2605,7 +2605,7 @@ "\n" ], "text": [ - " *' at 0x7fd2702fd4b0> >" + " *' at 0x7fa16814e4b0> >" ] }, { @@ -2645,7 +2645,7 @@ "\n", "\n", "\n", - "2->2\n", + "2->2\n", "\n", "\n", "!a & !c\n", @@ -2656,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", @@ -2667,7 +2667,7 @@ "3\n", "\n", "\n", - "2->3\n", + "2->3\n", "\n", "\n", "a & b & !c\n", @@ -2685,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", @@ -2724,7 +2724,7 @@ "\n" ], "text": [ - " *' at 0x7fd270264d80> >" + " *' at 0x7fa16823e5a0> >" ] }, { @@ -2783,7 +2783,7 @@ "\u2777\n", "\n", "\n", - "0->3\n", + "0->3\n", "\n", "\n", "!a & !c\n", @@ -2794,7 +2794,7 @@ "1\n", "\n", "\n", - "0->1\n", + "0->1\n", "\n", "\n", "a & !b & !c\n", @@ -2805,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", @@ -2823,7 +2823,7 @@ "\u2777\n", "\n", "\n", - "3->4\n", + "3->4\n", "\n", "\n", "a & !b & !c\n", @@ -2835,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", @@ -2904,7 +2904,7 @@ "\n" ], "text": [ - " *' at 0x7fd270264870> >" + " *' at 0x7fa1681b0ea0> >" ] } ], @@ -3034,7 +3034,7 @@ "\n", "\n", "\n", - "7->7\n", + "7->7\n", "\n", "\n", "!a & !c\n", @@ -3047,7 +3047,7 @@ "\u2778\n", "\n", "\n", - "7->4\n", + "7->4\n", "\n", "\n", "c\n", @@ -3059,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", @@ -3090,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", @@ -3108,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", @@ -3132,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", - "6->7\n", - "\n", - "\n", - "!a & !c\n", - "\n", - "\n", - "6->4\n", - "\n", - "\n", - "!a & c\n", - "\n", - "\n", - "6->3\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", - "6->5\n", - "\n", - "\n", - "a & b & c\n", - "\n", - "\n", - "6->2\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", - "\n", - "6->6\n", - "\n", - "\n", - "a & b & !c\n", - "\n", "\n", - "1->7\n", - "\n", - "\n", - "!a & !c\n", + "1->7\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "1->4\n", + "1->4\n", "\n", "\n", "!a & c\n", "\n", "\n", - "1->3\n", + "1->3\n", "\n", "\n", "a & !b & c\n", "\n", "\n", - "1->0\n", + "1->0\n", "\n", "\n", "a & b & c\n", "\n", "\n", - "1->2\n", - "\n", - "\n", - "a & !b & !c\n", + "1->2\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "1->1\n", + "1->1\n", "\n", "\n", "a & b & !c\n", "\n", + "\n", + "6->7\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "6->4\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "6->3\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "6->5\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "6->2\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "6->6\n", + "\n", + "\n", + "a & b & !c\n", + "\n", "\n", "\n" ], "text": [ - " *' at 0x7fd270281180> >" + " *' at 0x7fa16814e420> >" ] } ], @@ -3326,7 +3326,7 @@ "\n", "\n", "\n", - "0->0\n", + "0->0\n", "\n", "\n", "!a & !c\n", @@ -3338,7 +3338,7 @@ "\u24ff\n", "\n", "\n", - "0->2\n", + "0->2\n", "\n", "\n", "c\n", @@ -3350,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", @@ -3380,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", @@ -3398,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", @@ -3422,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", - "3->0\n", - "\n", - "\n", - "!a & !c\n", - "\n", - "\n", - "3->2\n", - "\n", - "\n", - "!a & c\n", - "\n", - "\n", - "3->4\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", - "3->5\n", - "\n", - "\n", - "a & b & 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", - "6->0\n", + "6->0\n", "\n", "\n", "!a & !c\n", "\n", "\n", - "6->2\n", + "6->2\n", "\n", "\n", "!a & c\n", "\n", "\n", - "6->4\n", + "6->4\n", "\n", "\n", "a & !b & c\n", "\n", "\n", - "6->7\n", + "6->7\n", "\n", "\n", "a & b & c\n", "\n", "\n", - "6->1\n", + "6->1\n", "\n", "\n", "a & !b & !c\n", "\n", "\n", - "6->6\n", + "6->6\n", "\n", "\n", "a & b & !c\n", "\n", + "\n", + "3->0\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "3->5\n", + "\n", + "\n", + "a & b & 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 0x7fd270281120> >" + " *' at 0x7fa16814e4b0> >" ] }, { @@ -3592,7 +3592,7 @@ "\n", "\n", "\n", - "0->0\n", + "0->0\n", "\n", "\n", "!a & !c\n", @@ -3604,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", @@ -3628,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", - "2->0\n", - "\n", - "\n", - "!a & !c\n", - "\n", - "\n", - "2->3\n", - "\n", - "\n", - "a & b & c\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "a & b & !c\n", - "\n", "\n", - "4->0\n", + "4->0\n", "\n", "\n", "!a & !c\n", "\n", "\n", - "4->1\n", + "4->1\n", "\n", "\n", "a & !b & !c\n", "\n", "\n", - "4->4\n", + "4->4\n", "\n", "\n", "a & b & !c\n", "\n", + "\n", + "2->0\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & b & !c\n", + "\n", "\n", "\n" ], "text": [ - " *' at 0x7fd270264360> >" + " *' at 0x7fa1681b0e40> >" ] }, { @@ -3737,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", - "2->0\n", - "\n", - "\n", - "!a & !c\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "a & b & !c\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "3->0\n", - "\n", - "\n", - "!a & !c\n", + "3->0\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", - "3->1\n", - "\n", - "\n", - "a & !b & !c\n", + "3->1\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "a & b & !c\n", + "3->3\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7fd270264d80> >" + " *' at 0x7fa1681b05a0> >" ] } ], @@ -3917,7 +3917,7 @@ "\n", "\n", "\n", - "0->0\n", + "0->0\n", "\n", "\n", "!a & !c\n", @@ -3930,7 +3930,7 @@ "\u2778\n", "\n", "\n", - "0->2\n", + "0->2\n", "\n", "\n", "c\n", @@ -3942,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", @@ -3972,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", @@ -3990,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", @@ -4014,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", - "3->0\n", - "\n", - "\n", - "!a & !c\n", - "\n", - "\n", - "3->2\n", - "\n", - "\n", - "!a & c\n", - "\n", - "\n", - "3->4\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", - "3->5\n", - "\n", - "\n", - "a & b & 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", - "6->0\n", + "6->0\n", "\n", "\n", "!a & !c\n", "\n", "\n", - "6->2\n", + "6->2\n", "\n", "\n", "!a & c\n", "\n", "\n", - "6->4\n", + "6->4\n", "\n", "\n", "a & !b & c\n", "\n", "\n", - "6->7\n", + "6->7\n", "\n", "\n", "a & b & c\n", "\n", "\n", - "6->1\n", + "6->1\n", "\n", "\n", "a & !b & !c\n", "\n", "\n", - "6->6\n", + "6->6\n", "\n", "\n", "a & b & !c\n", "\n", + "\n", + "3->0\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "3->5\n", + "\n", + "\n", + "a & b & 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 0x7fd270281240> >" + " *' at 0x7fa16814e450> >" ] } ], @@ -4211,7 +4211,7 @@ "\n", "\n", "\n", - "0->0\n", + "0->0\n", "\n", "\n", "a & !c\n", @@ -4222,7 +4222,7 @@ "1\n", "\n", "\n", - "0->1\n", + "0->1\n", "\n", "\n", "a & c\n", @@ -4233,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", @@ -4254,7 +4254,7 @@ "\n" ], "text": [ - " *' at 0x7fd270281870> >" + " *' at 0x7fa16814e660> >" ] } ], @@ -4319,7 +4319,7 @@ "\n", "\n", "\n", - "0->0\n", + "0->0\n", "\n", "\n", "a & !c\n", @@ -4331,13 +4331,13 @@ "\u24ff\n", "\n", "\n", - "0->1\n", + "0->1\n", "\n", "\n", "a & b & !c\n", "\n", "\n", - "1->1\n", + "1->1\n", "\n", "\n", "b\n", @@ -4346,7 +4346,7 @@ "\n" ], "text": [ - " *' at 0x7fd270264270> >" + " *' at 0x7fa16814e5d0> >" ] }, { @@ -4385,7 +4385,7 @@ "\n", "\n", "\n", - "0->0\n", + "0->0\n", "\n", "\n", "a & !c\n", @@ -4397,13 +4397,13 @@ "\u24ff\n", "\n", "\n", - "0->1\n", + "0->1\n", "\n", "\n", "a & c\n", "\n", "\n", - "1->1\n", + "1->1\n", "\n", "\n", "1\n", @@ -4412,7 +4412,7 @@ "\n" ], "text": [ - " *' at 0x7fd270264270> >" + " *' at 0x7fa16823e5a0> >" ] } ], @@ -4471,7 +4471,7 @@ "\n", "\n", "\n", - "0->0\n", + "0->0\n", "\n", "\n", "a & !c\n", @@ -4483,13 +4483,13 @@ "\u24ff\n", "\n", "\n", - "0->1\n", + "0->1\n", "\n", "\n", "a & c\n", "\n", "\n", - "1->1\n", + "1->1\n", "\n", "\n", "1\n", @@ -4498,7 +4498,7 @@ "\n" ], "text": [ - " *' at 0x7fd270264300> >" + " *' at 0x7fa16814e540> >" ] } ], @@ -4591,7 +4591,7 @@ "\n", "\n", "\n", - "0->0\n", + "0->0\n", "\n", "\n", "a\n", @@ -4602,7 +4602,7 @@ "1\n", "\n", "\n", - "0->1\n", + "0->1\n", "\n", "\n", "!a\n", @@ -4613,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", @@ -4631,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", @@ -4653,7 +4653,7 @@ "\n" ], "text": [ - " *' at 0x7fd270264420> >" + " *' at 0x7fa16814e990> >" ] } ], @@ -4721,7 +4721,7 @@ "\n", "\n", "\n", - "0->0\n", + "0->0\n", "\n", "\n", "a\n", @@ -4732,7 +4732,7 @@ "1\n", "\n", "\n", - "0->1\n", + "0->1\n", "\n", "\n", "!a\n", @@ -4743,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", @@ -4761,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", @@ -4782,7 +4782,7 @@ "\n" ], "text": [ - " *' at 0x7fd270264ed0> >" + " *' at 0x7fa16814ea50> >" ] }, { @@ -4822,7 +4822,7 @@ "\n", "\n", "\n", - "0->0\n", + "0->0\n", "\n", "\n", "a\n", @@ -4834,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", @@ -4853,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", @@ -4870,7 +4870,7 @@ "\n" ], "text": [ - " *' at 0x7fd270264ea0> >" + " *' at 0x7fa1681b0e70> >" ] }, { @@ -4920,7 +4920,7 @@ "\n", "\n", "\n", - "0->0\n", + "0->0\n", "\n", "\n", "a\n", @@ -4932,7 +4932,7 @@ "1\n", "\n", "\n", - "0->1\n", + "0->1\n", "\n", "\n", "!a\n", @@ -4944,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", @@ -4963,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", @@ -4987,7 +4987,7 @@ "\n" ], "text": [ - " *' at 0x7fd270264330> >" + " *' at 0x7fa16814eab0> >" ] } ],