From f6607f1a2c7695be9d59aa5ee5dabf60510afa2d Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 18 May 2017 16:46:11 +0200 Subject: [PATCH 01/13] bin: release all subformulas between runs Fixes #262, reported by Maximilien Colange. * bin/common_output.cc, bin/common_aoutput.cc, bin/common_aoutput.hh: Clear the set of atomic propositions if --stats=%[...]x was used. * spot/twa/bdddict.cc: Release any formula associated to a BDD when it is unregistered, do not wait for the dictionary's destruction. This was the main culprit for #262. * tests/core/ltl2tgba.test: Add test cases. * NEWS: Mention the bug. --- NEWS | 6 +++++- bin/common_aoutput.cc | 2 ++ bin/common_aoutput.hh | 6 +++++- bin/common_output.cc | 8 +++++++- spot/twa/bdddict.cc | 14 +++++--------- tests/core/ltl2tgba.test | 17 +++++++++++++++++ 6 files changed, 41 insertions(+), 12 deletions(-) diff --git a/NEWS b/NEWS index 90cf66bb0..a939abeac 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,10 @@ New in spot 2.3.4.dev (not yet released) - Nothing yet. + Bugs fixed: + + - We have fixed new cases where translating multiple formula in a + single ltl2tgba run could produce automata different from those + produced by individual runs. New in spot 2.3.4 (2017-05-11) diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc index 182caf2ba..18a9ef6fb 100644 --- a/bin/common_aoutput.cc +++ b/bin/common_aoutput.cc @@ -513,6 +513,8 @@ hoa_stat_printer::print(const spot::const_parsed_aut_ptr& haut, output_aut_ = nullptr; input_aut_ = nullptr; haut_scc_.reset(); + aut_ap_.clear(); + haut_ap_.clear(); return res; } diff --git a/bin/common_aoutput.hh b/bin/common_aoutput.hh index 83a774438..678b65bea 100644 --- a/bin/common_aoutput.hh +++ b/bin/common_aoutput.hh @@ -121,11 +121,15 @@ protected: }); } public: + void clear() + { + val_.clear(); + } template void set(T begin, T end) { - val_.clear(); + clear(); val_.insert(val_.end(), begin, end); sort(); } diff --git a/bin/common_output.cc b/bin/common_output.cc index abe85a819..674d19d20 100644 --- a/bin/common_output.cc +++ b/bin/common_output.cc @@ -239,7 +239,13 @@ namespace size_ = spot::length(f); if (has('h')) class_ = spot::mp_class(f); - return format(format_); + auto& res = format(format_); + // Make sure we do not store the formula until the next one is + // printed, as the order in which APs are registered may + // influence the automata output. + fl_ = nullptr; + ap_.clear(); + return res; } private: diff --git a/spot/twa/bdddict.cc b/spot/twa/bdddict.cc index 07b8280c3..ef601ad70 100644 --- a/spot/twa/bdddict.cc +++ b/spot/twa/bdddict.cc @@ -235,7 +235,6 @@ namespace spot // ME was the last user of this variable. // Let's free it. First, we need to find // if this is a Var or an Acc variable. - int n = 1; formula f = nullptr; switch (bdd_map[v].type) { @@ -249,21 +248,19 @@ namespace spot break; case anon: { - bdd_dict_priv::free_anonymous_list_of_type::iterator i; // Nobody use this variable as an anonymous variable // anymore, so remove it entirely from the anonymous // free list so it can be used for something else. - for (i = priv_->free_anonymous_list_of.begin(); - i != priv_->free_anonymous_list_of.end(); ++i) - i->second.remove(v, n); + for (auto& fal: priv_->free_anonymous_list_of) + fal.second.remove(v, 1); break; } } // Actually release the associated BDD variables, and the // formula itself. - priv_->release_variables(v, n); - while (n--) - bdd_map[v + n].type = anon; + priv_->release_variables(v, 1); + bdd_map[v].type = anon; + bdd_map[v].f = nullptr; } void @@ -326,7 +323,6 @@ namespace spot bdd_dict::assert_emptiness() const { bool fail = false; - bool var_seen = false; bool acc_seen = false; bool refs_seen = false; diff --git a/tests/core/ltl2tgba.test b/tests/core/ltl2tgba.test index 7b82b172c..a1c08208d 100755 --- a/tests/core/ltl2tgba.test +++ b/tests/core/ltl2tgba.test @@ -238,3 +238,20 @@ genltl --go-theta=18 | ltl2tgba --low --any -q (ltl2tgba Fb ; ltl2tgba 'GFa & GFb') >out1 ltl2tgba Fb 'GFa & GFb' >out2 diff out1 out2 + +# Because atomic proposition were not released by bdd_dict, different +# order of transitions could be observed in automata output after a +# previous translation by the same process. (issue #262). +ltl2tgba --low --any 'Xp1 xor (Fp1 M (!p1 M (Fp0 W p1)))' \ + 'Fp0 -> XXG(1 U Gp1)' > res1 +ltl2tgba --low --any 'Xp1 xor (Fp1 M (!p1 M (Fp0 W p1)))' >res2 +ltl2tgba --low --any 'Fp0 -> XXG(1 U Gp1)' >>res2 +diff res1 res2 + +# The same should work when printing SCCs or atomic propositions +s='--stats=%c,%[,]x' +ltl2tgba --low --any 'Xp1 xor (Fp1 M (!p1 M (Fp0 W p1)))' \ + 'Fp0 -> XXG(1 U Gp1)' "$s" >res1 +ltl2tgba --low --any 'Xp1 xor (Fp1 M (!p1 M (Fp0 W p1)))' "$s" >res2 +ltl2tgba --low --any 'Fp0 -> XXG(1 U Gp1)' "$s" >>res2 +diff res1 res2 From 7b6cfd448c29319d9ddcc7e854c62f821dd1d738 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 31 May 2017 17:14:52 +0200 Subject: [PATCH 02/13] 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> >" ] } ], From ae0e84ac9e9a96d3d415f9864235634462588eba Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 2 Jun 2017 11:23:42 +0200 Subject: [PATCH 03/13] simulation: do not depend on bdd numbers for ordering classes Fixes #262 again. Reported by Maximilien Colange. * spot/twaalgos/simulation.cc: Use state numbers to order classes, not their signatures. The problem was that even if two simulation of the same automaton assign the same signature, the BDD identifier used for that signature might be different, and therefore the ordering obtained by using BDDs as keys in a map can be different. A side-effect of this change is that the order of states in automata produced by simulation-based reduction may change; many tests had to be updated. * tests/core/ltl2tgba.test: Add a new test case based on Maximilien's report. * tests/core/complement.test, tests/core/det.test, tests/core/parseaut.test, tests/core/prodor.test, tests/python/atva16-fig2a.ipynb, tests/python/automata.ipynb, tests/python/decompose.ipynb, tests/python/highlighting.ipynb, tests/python/piperead.ipynb, tests/python/testingaut.ipynb, tests/python/word.ipynb: Update test cases for new order of states. --- spot/twaalgos/simulation.cc | 52 +- tests/core/complement.test | 4 +- tests/core/det.test | 42 +- tests/core/ltl2tgba.test | 8 + tests/core/parseaut.test | 50 +- tests/core/prodor.test | 10 +- tests/python/atva16-fig2a.ipynb | 118 ++--- tests/python/automata.ipynb | 839 ++++++++++++++++---------------- tests/python/decompose.ipynb | 518 ++++++++++---------- tests/python/highlighting.ipynb | 106 ++-- tests/python/piperead.ipynb | 76 ++- tests/python/testingaut.ipynb | 532 ++++++++++---------- tests/python/word.ipynb | 224 ++++++--- 13 files changed, 1337 insertions(+), 1242 deletions(-) diff --git a/spot/twaalgos/simulation.cc b/spot/twaalgos/simulation.cc index e59ed5e4a..2b4e51786 100644 --- a/spot/twaalgos/simulation.cc +++ b/spot/twaalgos/simulation.cc @@ -275,7 +275,7 @@ namespace spot // We run through the map bdd/list, and we update // the previous_class_ with the new data. - for (auto& p: bdd_lstate_) + for (auto& p: sorted_classes_) { // If the signature of a state is bddfalse (no // edges) the class of this state is bddfalse @@ -283,11 +283,11 @@ namespace spot // simplifications in the signature by removing a // edge which has as a destination a state with // no outgoing edge. - if (p.first == bddfalse) - for (auto s: p.second) + if (p->first == bddfalse) + for (unsigned s: p->second) previous_class_[s] = bddfalse; else - for (auto s: p.second) + for (unsigned s: p->second) previous_class_[s] = *it_bdd; ++it_bdd; } @@ -302,10 +302,10 @@ namespace spot { update_previous_class(); nb_partition_before = bdd_lstate_.size(); - bdd_lstate_.clear(); nb_po_before = po_size_; po_size_ = 0; update_sig(); + // print_partition(); go_to_next_it(); } @@ -347,8 +347,18 @@ namespace spot void update_sig() { + bdd_lstate_.clear(); + sorted_classes_.clear(); for (unsigned s = 0; s < size_a_; ++s) - bdd_lstate_[compute_sig(s)].emplace_back(s); + { + bdd sig = compute_sig(s); + auto p = bdd_lstate_.emplace(std::piecewise_construct, + std::make_tuple(sig), + std::make_tuple()); + p.first->second.emplace_back(s); + if (p.second) + sorted_classes_.emplace_back(p.first); + } } @@ -390,7 +400,7 @@ namespace spot std::list::iterator it_bdd = used_var_.begin(); - for (auto& p: bdd_lstate_) + for (auto& p: sorted_classes_) { // If the signature of a state is bddfalse (no edges) the // class of this state is bddfalse instead of an anonymous @@ -398,9 +408,9 @@ namespace spot // removing an edge which has as a destination a state // with no outgoing edge. bdd acc = bddfalse; - if (p.first != bddfalse) + if (p->first != bddfalse) acc = *it_bdd; - now_to_next.emplace_back(p.first, acc); + now_to_next.emplace_back(p->first, acc); ++it_bdd; } @@ -446,10 +456,10 @@ namespace spot if (implications) implications->resize(bdd_lstate_.size()); - // Create one state per partition. - for (auto& p: bdd_lstate_) + // Create one state per class. + for (auto& p: sorted_classes_) { - bdd cl = previous_class_[p.second.front()]; + bdd cl = previous_class_[p->second.front()]; // A state may be referred to either by // its class, or by all the implied classes. auto s = gb->new_state(cl.id()); @@ -472,14 +482,14 @@ namespace spot auto all_inf = all_inf_; // For each class, we will create // all the edges between the states. - for (auto& p: bdd_lstate_) + for (auto& p: sorted_classes_) { // All states in p.second have the same class, so just // pick the class of the first one first one. - bdd src = previous_class_[p.second.front()]; + bdd src = previous_class_[p->second.front()]; // Get the signature to derive successors. - bdd sig = compute_sig(p.second.front()); + bdd sig = compute_sig(p->second.front()); if (Cosimulation) sig = bdd_compose(sig, bddfalse, bdd_var(bdd_initial)); @@ -613,12 +623,12 @@ namespace spot // where is the new class name. void print_partition() { - for (auto& p: bdd_lstate_) + for (auto& p: sorted_classes_) { std::cerr << "partition: " - << bdd_format_isop(a_->get_dict(), p.first) + << bdd_format_isop(a_->get_dict(), p->first) << std::endl; - for (auto s: p.second) + for (auto s: p->second) std::cerr << " - " << a_->format_state(a_->state_from_number(s)) << '\n'; @@ -646,9 +656,13 @@ namespace spot // Represent the class of each state at the previous iteration. vector_state_bdd previous_class_; - // The list of state for each class at the current_iteration. + // The list of states for each class at the current_iteration. // Computed in `update_sig'. map_bdd_lstate bdd_lstate_; + // The above map, sorted by states number instead of BDD + // identifier to avoid non-determinism while iterating over all + // states. + std::vector sorted_classes_; // The queue of free bdd. They will be used as the identifier // for the class. diff --git a/tests/core/complement.test b/tests/core/complement.test index 6a1f4c1c2..2ef1566ac 100755 --- a/tests/core/complement.test +++ b/tests/core/complement.test @@ -118,11 +118,11 @@ properties: trans-labels explicit-labels trans-acc complete properties: deterministic stutter-invariant --BODY-- State: 0 -[0] 1 {1} [!0] 0 -State: 1 [0] 1 {1} +State: 1 [!0] 0 {0} +[0] 1 {1} --END-- EOF diff out expected diff --git a/tests/core/det.test b/tests/core/det.test index 9d4014ee5..eeb7d3c22 100755 --- a/tests/core/det.test +++ b/tests/core/det.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et -# Développement de l'Epita (LRDE). +# Copyright (C) 2013-2017 Laboratoire de Recherche et Développement de +# l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -148,20 +148,20 @@ cat >expected-nd.hoa <expected-rand.hoa <expected-rand2.hoa <res2 ltl2tgba --low --any 'Fp0 -> XXG(1 U Gp1)' "$s" >>res2 diff res1 res2 + +# Another case where different but isomorphic automata +# were output (issue #262 again). +f1='F(Gp0 <-> Gp1)' +f2='Gp1 | FGp0' +(ltl2tgba -xsimul=1 --low "$f1"; ltl2tgba -xsimul=1 --low "$f2") > res1 +ltl2tgba -xsimul=1 --low "$f1" "$f2" > res2 +diff res1 res2 diff --git a/tests/core/parseaut.test b/tests/core/parseaut.test index 9c5c64dd9..63b9106e7 100755 --- a/tests/core/parseaut.test +++ b/tests/core/parseaut.test @@ -1692,7 +1692,7 @@ cat >expected <\u2776\n", ")\n", "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "1\n", - "\n", "\n", - "0\n", - "\n", - "0\n", + "0\n", + "\n", + "0\n", "\n", - "\n", - "1->0\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a | b\n", "\n", "\n", "2\n", "\n", "2\n", "\n", - "\n", - "1->2\n", - "\n", - "\n", - "a | b\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a & !b\n", "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!a & !b\n", - "\u24ff\n", - "\u2776\n", + "\n", + "1->1\n", + "\n", + "\n", + "!a & b\n", + "\u2776\n", "\n", - "\n", - "2->2\n", - "\n", - "\n", - "!a & b\n", - "\u2776\n", + "\n", + "1->1\n", + "\n", + "\n", + "!a & !b\n", "\n", - "\n", - "2->2\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & b\n", + "\u24ff\n", + "\u2776\n", "\n", - "\n", - "2->2\n", - "\n", - "\n", - "a & b\n", - "\u24ff\n", - "\u2776\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !b\n", + "\u24ff\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "a & !b\n", - "\u24ff\n", + "\n", + "\n", + "!a & !b\n", + "\u24ff\n", + "\u2776\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7f79506d2900> >" + " *' at 0x7f6b2060be40> >" ] } ], diff --git a/tests/python/automata.ipynb b/tests/python/automata.ipynb index dec25e75f..1c8ceacbf 100644 --- a/tests/python/automata.ipynb +++ b/tests/python/automata.ipynb @@ -15,10 +15,9 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.4.3+" + "version": "3.5.3" }, - "name": "", - "signature": "sha256:4ddb9b8fc1c41bacd7e47f70861303cde0ad425f842ade8e1f23ee74738914b0" + "name": "" }, "nbformat": 3, "nbformat_minor": 0, @@ -178,7 +177,7 @@ "\n" ], "text": [ - " *' at 0x7fe334de9900> >" + " *' at 0x7fb9189349f0> >" ] } ], @@ -317,7 +316,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -470,7 +469,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -570,7 +569,7 @@ "\n" ], "text": [ - " *' at 0x7fe33c8331b0> >" + " *' at 0x7fb9188abd80> >" ] } ], @@ -640,7 +639,7 @@ "\n" ], "text": [ - " *' at 0x7fe33c833060> >" + " *' at 0x7fb9188abe40> >" ] } ], @@ -716,7 +715,7 @@ "\n" ], "text": [ - " *' at 0x7fe33c8330f0> >" + " *' at 0x7fb9188abdb0> >" ] } ], @@ -839,7 +838,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -1029,7 +1028,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -1062,121 +1061,121 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "a | b\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "a | b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "0->4\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "b\n", - "\u24ff\n", + "\n", + "\n", + "b\n", + "\u24ff\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "!b\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!a & !b\n", - "\u24ff\n", + "\n", + "\n", + "a | b\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", - "3->2\n", - "\n", - "\n", - "!a & !b\n", + "3->2\n", + "\n", + "\n", + "a | b\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "a | b\n", - "\n", - "\n", - "3->4\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "4->3\n", - "\n", - "\n", - "a | b\n", + "3->3\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", + "\u24ff\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7fe33c833300> >" + " *' at 0x7fb9188ab5d0> >" ] } ], @@ -1215,69 +1214,69 @@ "G\n", "\n", "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "1\n", - "\n", "\n", - "0\n", - "\n", - "0\n", + "0\n", + "\n", + "0\n", "\n", - "\n", - "1->0\n", - "\n", - "\n", - "!a\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b\n", "\n", "\n", "2\n", "\n", "2\n", "\n", - "\n", - "1->2\n", - "\n", - "\n", - "b\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a\n", "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!a\n", - "\u24ff\n", + "\n", + "1->1\n", + "\n", + "\n", + "b\n", + "\u24ff\n", "\n", - "\n", - "2->2\n", - "\n", - "\n", - "b\n", - "\u24ff\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "!a\n", + "\u24ff\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7fe33c8332d0> >" + " *' at 0x7fb9188abe10> >" ] } ], @@ -1335,67 +1334,67 @@ "\n", "1\n", "\n", - "\n", "1\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "b\n", "\n", "\n", "2\n", "\n", + "\n", "2\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "!a\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "!b\n", "\n", "\n", "3\n", - "\n", - "\n", - "3\n", + "\n", + "\n", + "3\n", "\n", - "\n", - "2->3\n", - "\n", - "\n", - "b\n", + "\n", + "1->3\n", + "\n", + "\n", + "b\n", "\n", - "\n", - "3->2\n", - "\n", - "\n", - "!b\n", + "\n", + "2->2\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "!b\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7fe33c833120> >" + " *' at 0x7fb918910f60> >" ] } ], @@ -1494,7 +1493,7 @@ "\n" ], "text": [ - " *' at 0x7fe33c833330> >" + " *' at 0x7fb9188abb70> >" ] } ], @@ -1964,7 +1963,7 @@ "\n" ], "text": [ - " *' at 0x7fe33c8332a0> >" + " *' at 0x7fb9191c2720> >" ] } ], @@ -2161,7 +2160,7 @@ "" ], "text": [ - "" + "" ] }, { @@ -2286,149 +2285,149 @@ "" ], "text": [ - "" + "" ] }, { "metadata": {}, "output_type": "display_data", "svg": [ - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", - "Inf(\n", - "\u24ff\n", - ")\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")\n", "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "a\n", - "\u24ff\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "1->3\n", - "\n", - "\n", - "!a\n", - "\n", "\n", - "0\n", - "\n", - "0\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!a & !b\n", - "\u24ff\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\u24ff\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!a & b\n", + "\u24ff\n", "\n", "\n", - "4\n", - "\n", - "4\n", + "4\n", + "\n", + "4\n", "\n", - "\n", - "0->4\n", - "\n", - "\n", - "a | b\n", + "\n", + "1->4\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "2->4\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "2->3\n", - "\n", - "\n", - "!a & b\n", - "\u24ff\n", - "\n", - "\n", - "3->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "3->0\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "1\n", "\n", "\n", "3->4\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "3->2\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a | b\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", + "\u24ff\n", "\n", "\n", "" ], "text": [ - "" + "" ] }, { @@ -2441,145 +2440,145 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", - "I->2\n", - "\n", - "\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "1\n", - "\n", "\n", - "0\n", - "\n", - "\n", - "0\n", + "0\n", + "\n", + "0\n", "\n", - "\n", - "2->0\n", - "\n", - "\n", - "a\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b\n", "\n", "\n", - "3\n", - "\n", - "3\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "2->3\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", - "0->2\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "4\n", - "\n", - "4\n", - "\n", - "\n", - "0->4\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "0->5\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", - "4->4\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "4->5\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", - "5->2\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "5->4\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "5->1\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "5->3\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "3->4\n", "\n", "\n", "a & !b\n", "\n", - "\n", - "3->1\n", + "\n", + "5\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "2->5\n", "\n", "\n", "!a & !b\n", "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "4->0\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "4->5\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "5->5\n", + "\n", + "\n", + "!a & !b\n", + "\n", "\n", "\n" ], "text": [ - " *' at 0x7fe334d5cae0> >" + " *' at 0x7fb918234300> >" ] } ], @@ -2735,7 +2734,7 @@ "\n" ], "text": [ - " *' at 0x7fe334d5cfc0> >" + " *' at 0x7fb918234270> >" ] } ], @@ -2805,7 +2804,7 @@ "\n" ], "text": [ - " *' at 0x7fe334d5cae0> >" + " *' at 0x7fb918234330> >" ] } ], @@ -2877,7 +2876,7 @@ "" ], "text": [ - "" + "" ] }, { @@ -2930,7 +2929,7 @@ "" ], "text": [ - "" + "" ] }, { @@ -3042,7 +3041,7 @@ "" ], "text": [ - "" + "" ] }, { @@ -3154,7 +3153,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -3169,7 +3168,7 @@ }, { "cell_type": "code", - "collapsed": true, + "collapsed": false, "input": [ "a = spot.translate('FGa')\n", "display(a)\n", @@ -3194,35 +3193,35 @@ "G\n", "\n", "\n", - "\n", - "1\n", + "\n", + "0\n", "\n", - "1\n", + "0\n", "\n", - "\n", - "I->1\n", + "\n", + "I->0\n", "\n", "\n", "\n", - "\n", - "1->1\n", + "\n", + "0->0\n", "\n", "\n", - "1\n", + "1\n", "\n", - "\n", - "0\n", + "\n", + "1\n", "\n", - "0\n", + "1\n", "\n", - "\n", - "1->0\n", + "\n", + "0->1\n", "\n", "\n", "a\n", "\n", - "\n", - "0->0\n", + "\n", + "1->1\n", "\n", "\n", "a\n", @@ -3232,7 +3231,7 @@ "\n" ], "text": [ - " *' at 0x7fe33c833390> >" + " *' at 0x7fb9182341b0> >" ] }, { @@ -3280,7 +3279,7 @@ "\n", "\n", "\n", - "0->0\n", + "0->0\n", "\n", "\n", "!a\n", @@ -3291,21 +3290,21 @@ "1\n", "\n", "\n", - "0->1\n", + "0->1\n", "\n", "\n", "a\n", "\u2776\n", "\n", "\n", - "1->0\n", + "1->0\n", "\n", "\n", "!a\n", "\u24ff\n", "\n", "\n", - "1->1\n", + "1->1\n", "\n", "\n", "a\n", @@ -3315,7 +3314,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -3400,7 +3399,7 @@ "\n" ], "text": [ - " *' at 0x7fe33c747540> >" + " *' at 0x7fb9182344b0> >" ] } ], @@ -3410,7 +3409,7 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "Adding an automatic proposition to all edges" + "Adding an atomic proposition to all edges" ] }, { @@ -3489,7 +3488,7 @@ "\n" ], "text": [ - " *' at 0x7fe33c747540> >" + " *' at 0x7fb9182344b0> >" ] } ], @@ -3578,7 +3577,7 @@ "\n" ], "text": [ - " *' at 0x7fe33c747540> >" + " *' at 0x7fb9182344b0> >" ] } ], @@ -3588,4 +3587,4 @@ "metadata": {} } ] -} \ No newline at end of file +} diff --git a/tests/python/decompose.ipynb b/tests/python/decompose.ipynb index 68ea84c15..0518248d4 100644 --- a/tests/python/decompose.ipynb +++ b/tests/python/decompose.ipynb @@ -80,138 +80,138 @@ "\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", "cluster_2\n", - "\n", + "\n", "\n", "cluster_3\n", - "\n", + "\n", "\n", "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!a & !c\n", - "\u24ff\n", - "\n", "\n", - "0\n", - "\n", - "0\n", + "0\n", + "\n", + "0\n", "\n", - "\n", - "1->0\n", - "\n", - "\n", - "a & b & !c\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "1->3\n", - "\n", - "\n", - "c\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "a & !c\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "b\n", - "\u24ff\n", + "\n", + "\n", + "!a & !c\n", + "\u24ff\n", "\n", - "\n", - "3->3\n", - "\n", - "\n", - "1\n", - "\u24ff\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", + "\u24ff\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "b\n", + "\u24ff\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", - "\n", - "4->3\n", - "\n", - "\n", - "!a\n", + "\n", + "4->1\n", + "\n", + "\n", + "!a\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", - "\n", - "2->1\n", - "\n", - "\n", - "!a & !c\n", - "\u24ff\n", + "\n", + "3->0\n", + "\n", + "\n", + "!a & !c\n", + "\u24ff\n", "\n", - "\n", - "2->3\n", - "\n", - "\n", - "!a & c\n", + "\n", + "3->1\n", + "\n", + "\n", + "!a & c\n", "\n", - "\n", - "2->4\n", - "\n", - "\n", - "a & c\n", + "\n", + "3->4\n", + "\n", + "\n", + "a & c\n", "\n", - "\n", - "2->2\n", - "\n", - "\n", - "a & !c\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7fa1681b0690> >" + " *' at 0x7f3a2c7d9690> >" ] } ], @@ -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", @@ -328,7 +328,7 @@ "\n" ], "text": [ - " *' at 0x7fa1681b0660> >" + " *' at 0x7f3a2c7d9360> >" ] } ], @@ -395,30 +395,30 @@ "\n", "!a & !c\n", "\n", - "\n", - "2\n", + "\n", + "1\n", "\n", - "2\n", + "1\n", "\n", - "\n", - "0->2\n", + "\n", + "0->1\n", "\n", "\n", "c\n", "\n", - "\n", - "1\n", + "\n", + "2\n", "\n", - "1\n", + "2\n", "\n", - "\n", - "0->1\n", + "\n", + "0->2\n", "\n", "\n", "a & !c\n", "\n", - "\n", - "2->2\n", + "\n", + "1->1\n", "\n", "\n", "1\n", @@ -429,8 +429,8 @@ "\n", "3\n", "\n", - "\n", - "3->2\n", + "\n", + "3->1\n", "\n", "\n", "!a\n", @@ -441,26 +441,26 @@ "\n", "a\n", "\n", - "\n", - "1->0\n", + "\n", + "2->0\n", "\n", "\n", "!a & !c\n", "\n", - "\n", - "1->2\n", + "\n", + "2->1\n", "\n", "\n", "!a & c\n", "\n", - "\n", - "1->3\n", + "\n", + "2->3\n", "\n", "\n", "a & c\n", "\n", - "\n", - "1->1\n", + "\n", + "2->2\n", "\n", "\n", "a & !c\n", @@ -469,7 +469,7 @@ "\n" ], "text": [ - " *' at 0x7fa1681b03f0> >" + " *' at 0x7f3a2c7d9510> >" ] } ], @@ -559,7 +559,7 @@ "\n" ], "text": [ - " *' at 0x7fa1681b0510> >" + " *' at 0x7f3a2c7d9660> >" ] } ], @@ -636,7 +636,7 @@ "\n" ], "text": [ - " *' at 0x7fa1681b0ed0> >" + " *' at 0x7f3a2c7d9ed0> >" ] } ], @@ -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", @@ -752,7 +752,7 @@ "\n" ], "text": [ - " *' at 0x7fa1681b05a0> >" + " *' at 0x7f3a30923420> >" ] }, { @@ -801,30 +801,30 @@ "!a & !c\n", "\u24ff\n", "\n", - "\n", - "2\n", + "\n", + "1\n", "\n", - "2\n", + "1\n", "\n", - "\n", - "0->2\n", + "\n", + "0->1\n", "\n", "\n", "c\n", "\n", - "\n", - "1\n", + "\n", + "2\n", "\n", - "1\n", + "2\n", "\n", - "\n", - "0->1\n", + "\n", + "0->2\n", "\n", "\n", "a & !c\n", "\n", - "\n", - "2->2\n", + "\n", + "1->1\n", "\n", "\n", "1\n", @@ -835,8 +835,8 @@ "\n", "3\n", "\n", - "\n", - "3->2\n", + "\n", + "3->1\n", "\n", "\n", "!a\n", @@ -847,27 +847,27 @@ "\n", "a\n", "\n", - "\n", - "1->0\n", + "\n", + "2->0\n", "\n", "\n", "!a & !c\n", "\u24ff\n", "\n", - "\n", - "1->2\n", + "\n", + "2->1\n", "\n", "\n", "!a & c\n", "\n", - "\n", - "1->3\n", + "\n", + "2->3\n", "\n", "\n", "a & c\n", "\n", - "\n", - "1->1\n", + "\n", + "2->2\n", "\n", "\n", "a & !c\n", @@ -876,7 +876,7 @@ "\n" ], "text": [ - " *' at 0x7fa1681b05d0> >" + " *' at 0x7f3a2c7d9e40> >" ] }, { @@ -889,137 +889,137 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", - "option: wt\n", - "Inf(\n", - "\u24ff\n", - ")\n", + "\n", + "option: wt\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", "\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 & !c\n", + "0->0\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", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "0->3\n", - "\n", - "\n", - "c\n", + "0->1\n", + "\n", + "\n", + "c\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "2\n", + "\n", + "2\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "a & !c\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "b\n", - "\u24ff\n", + "\n", + "\n", + "1\n", + "\u24ff\n", "\n", - "\n", - "3->3\n", - "\n", - "\n", - "1\n", - "\u24ff\n", + "\n", + "2->2\n", + "\n", + "\n", + "b\n", + "\u24ff\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", - "\n", - "4->3\n", - "\n", - "\n", - "!a\n", + "\n", + "4->1\n", + "\n", + "\n", + "!a\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", - "\n", - "2->0\n", - "\n", - "\n", - "!a & !c\n", + "\n", + "3->0\n", + "\n", + "\n", + "!a & !c\n", "\n", - "\n", - "2->3\n", - "\n", - "\n", - "!a & c\n", + "\n", + "3->1\n", + "\n", + "\n", + "!a & c\n", "\n", - "\n", - "2->4\n", - "\n", - "\n", - "a & c\n", + "\n", + "3->4\n", + "\n", + "\n", + "a & c\n", "\n", - "\n", - "2->2\n", - "\n", - "\n", - "a & !c\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7fa1681b0e70> >" + " *' at 0x7f3a2c7d9540> >" ] } ], @@ -1424,7 +1424,7 @@ "\n" ], "text": [ - " *' at 0x7fa1681b04b0> >" + " *' at 0x7f3a2c777360> >" ] } ], @@ -1749,7 +1749,7 @@ "\n" ], "text": [ - " *' at 0x7fa16814e420> >" + " *' at 0x7f3a2c777450> >" ] }, { @@ -1946,7 +1946,7 @@ "\n" ], "text": [ - " *' at 0x7fa1681b0540> >" + " *' at 0x7f3a2c7d95d0> >" ] }, { @@ -2126,7 +2126,7 @@ "\n" ], "text": [ - " *' at 0x7fa1681b0360> >" + " *' at 0x7f3a2c7d9e40> >" ] } ], @@ -2461,7 +2461,7 @@ "\n" ], "text": [ - " *' at 0x7fa1681b03c0> >" + " *' at 0x7f3a30923420> >" ] } ], @@ -2605,7 +2605,7 @@ "\n" ], "text": [ - " *' at 0x7fa16814e4b0> >" + " *' at 0x7f3a2c7774e0> >" ] }, { @@ -2724,7 +2724,7 @@ "\n" ], "text": [ - " *' at 0x7fa16823e5a0> >" + " *' at 0x7f3a2c7d9e70> >" ] }, { @@ -2904,7 +2904,7 @@ "\n" ], "text": [ - " *' at 0x7fa1681b0ea0> >" + " *' at 0x7f3a2d0686f0> >" ] } ], @@ -3261,7 +3261,7 @@ "\n" ], "text": [ - " *' at 0x7fa16814e420> >" + " *' at 0x7f3a2c7774e0> >" ] } ], @@ -3551,7 +3551,7 @@ "\n" ], "text": [ - " *' at 0x7fa16814e4b0> >" + " *' at 0x7f3a2c7773f0> >" ] }, { @@ -3703,7 +3703,7 @@ "\n" ], "text": [ - " *' at 0x7fa1681b0e40> >" + " *' at 0x7f3a2c7d9e40> >" ] }, { @@ -3840,7 +3840,7 @@ "\n" ], "text": [ - " *' at 0x7fa1681b05a0> >" + " *' at 0x7f3a2c7d93f0> >" ] } ], @@ -4143,7 +4143,7 @@ "\n" ], "text": [ - " *' at 0x7fa16814e450> >" + " *' at 0x7f3a2c777510> >" ] } ], @@ -4254,7 +4254,7 @@ "\n" ], "text": [ - " *' at 0x7fa16814e660> >" + " *' at 0x7f3a2c777750> >" ] } ], @@ -4346,7 +4346,7 @@ "\n" ], "text": [ - " *' at 0x7fa16814e5d0> >" + " *' at 0x7f3a2c777870> >" ] }, { @@ -4412,7 +4412,7 @@ "\n" ], "text": [ - " *' at 0x7fa16823e5a0> >" + " *' at 0x7f3a2c7d9ea0> >" ] } ], @@ -4498,7 +4498,7 @@ "\n" ], "text": [ - " *' at 0x7fa16814e540> >" + " *' at 0x7f3a2c777930> >" ] } ], @@ -4653,7 +4653,7 @@ "\n" ], "text": [ - " *' at 0x7fa16814e990> >" + " *' at 0x7f3a2c777990> >" ] } ], @@ -4782,7 +4782,7 @@ "\n" ], "text": [ - " *' at 0x7fa16814ea50> >" + " *' at 0x7f3a2c777420> >" ] }, { @@ -4870,7 +4870,7 @@ "\n" ], "text": [ - " *' at 0x7fa1681b0e70> >" + " *' at 0x7f3a2c7d9540> >" ] }, { @@ -4987,7 +4987,7 @@ "\n" ], "text": [ - " *' at 0x7fa16814eab0> >" + " *' at 0x7f3a2c777a50> >" ] } ], diff --git a/tests/python/highlighting.ipynb b/tests/python/highlighting.ipynb index 04b9c5699..8b7c41e57 100644 --- a/tests/python/highlighting.ipynb +++ b/tests/python/highlighting.ipynb @@ -15,7 +15,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.5.3rc1" + "version": "3.5.3" }, "name": "" }, @@ -254,7 +254,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0b5ab70> >" + " *' at 0x7f98b673b870> >" ] } ], @@ -356,7 +356,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb270> >" + " *' at 0x7f98b66ad630> >" ] } ], @@ -571,7 +571,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb390> >" + " *' at 0x7f98b66ad300> >" ] } ], @@ -750,7 +750,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb390> >" + " *' at 0x7f98b66ad300> >" ] } ], @@ -830,7 +830,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb660> >" + " *' at 0x7f98b66ad7b0> >" ] }, { @@ -876,7 +876,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb300> >" + " *' at 0x7f98b66ad570> >" ] } ], @@ -962,7 +962,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb150> >" + " *' at 0x7f98b66ad750> >" ] } ], @@ -1087,7 +1087,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb150> >" + " *' at 0x7f98b66ad750> >" ] }, { @@ -1144,7 +1144,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb660> >" + " *' at 0x7f98b66ad7b0> >" ] }, { @@ -1190,7 +1190,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb300> >" + " *' at 0x7f98b66ad570> >" ] } ], @@ -1397,7 +1397,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb750> >" + " *' at 0x7f98b66ad510> >" ] }, { @@ -1471,7 +1471,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb630> >" + " *' at 0x7f98b66adb70> >" ] }, { @@ -1555,7 +1555,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb2d0> >" + " *' at 0x7f98b66ad3c0> >" ] } ], @@ -1701,7 +1701,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb810> >" + " *' at 0x7f98b66adcc0> >" ] } ], @@ -1846,7 +1846,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb810> >" + " *' at 0x7f98b66adcc0> >" ] } ], @@ -1989,7 +1989,7 @@ "\n" ], "text": [ - " *' at 0x7fd9b0aeb810> >" + " *' at 0x7f98b66adcc0> >" ] }, { @@ -2202,51 +2202,51 @@ "\n", "\n", "\n", - "\n", - "1\n", + "\n", + "0\n", "\n", - "1\n", + "0\n", "\n", - "\n", - "I->1\n", + "\n", + "I->0\n", "\n", "\n", "\n", - "\n", - "0\n", + "\n", + "1\n", "\n", - "0\n", + "1\n", "\n", - "\n", - "1->0\n", + "\n", + "0->1\n", "\n", "\n", "a\n", "\n", - "\n", - "2\n", + "\n", + "3\n", "\n", - "2\n", + "3\n", "\n", - "\n", - "1->2\n", + "\n", + "0->3\n", "\n", "\n", "!a & !b\n", "\n", - "\n", - "3\n", + "\n", + "2\n", "\n", - "3\n", + "2\n", "\n", - "\n", - "1->3\n", + "\n", + "0->2\n", "\n", "\n", "!a & b\n", "\n", - "\n", - "0->0\n", + "\n", + "1->1\n", "\n", "\n", "1\n", @@ -2317,26 +2317,26 @@ "\n", "!b & c\n", "\n", - "\n", - "2->4\n", + "\n", + "3->4\n", "\n", "\n", "a\n", "\n", - "\n", - "3->4\n", + "\n", + "2->4\n", "\n", "\n", "a\n", "\n", - "\n", - "3->2\n", + "\n", + "2->3\n", "\n", "\n", "!a & !b\n", "\n", - "\n", - "3->3\n", + "\n", + "2->2\n", "\n", "\n", "!a & b & !c\n", @@ -2346,8 +2346,8 @@ "\n", "5\n", "\n", - "\n", - "3->5\n", + "\n", + "2->5\n", "\n", "\n", "!a & b & c\n", @@ -2358,14 +2358,14 @@ "\n", "a\n", "\n", - "\n", - "5->2\n", + "\n", + "5->3\n", "\n", "\n", "!a & !b\n", "\n", - "\n", - "5->3\n", + "\n", + "5->2\n", "\n", "\n", "!a & b\n", diff --git a/tests/python/piperead.ipynb b/tests/python/piperead.ipynb index 4f9392704..874c75352 100644 --- a/tests/python/piperead.ipynb +++ b/tests/python/piperead.ipynb @@ -15,10 +15,9 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.4.3+" + "version": "3.5.3" }, - "name": "", - "signature": "sha256:8de782e4035d4a93101b749825f0975f5f8cee034332d048014ba13dfa232983" + "name": "" }, "nbformat": 3, "nbformat_minor": 0, @@ -111,7 +110,7 @@ "\n" ], "text": [ - " *' at 0x7fad7cc5f330> >" + " *' at 0x7f2bb6866420> >" ] }, { @@ -162,7 +161,7 @@ "\n" ], "text": [ - " *' at 0x7fad7cc5f4e0> >" + " *' at 0x7f2bb47205d0> >" ] }, { @@ -208,7 +207,7 @@ "\n" ], "text": [ - " *' at 0x7fad7cc5f270> >" + " *' at 0x7f2bb4720360> >" ] }, { @@ -227,36 +226,36 @@ "G\n", "\n", "\n", - "\n", - "1\n", + "\n", + "0\n", "\n", - "1\n", + "0\n", "\n", - "\n", - "I->1\n", + "\n", + "I->0\n", "\n", "\n", "\n", - "\n", - "0\n", + "\n", + "1\n", "\n", - "0\n", + "1\n", "\n", - "\n", - "1->0\n", + "\n", + "0->1\n", "\n", "\n", "a\n", "\n", - "\n", - "0->0\n", + "\n", + "1->1\n", "\n", "\n", "b\n", "\u24ff\n", "\n", - "\n", - "0->0\n", + "\n", + "1->1\n", "\n", "\n", "!b\n", @@ -265,7 +264,7 @@ "\n" ], "text": [ - " *' at 0x7fad7cc5f330> >" + " *' at 0x7f2bb47203f0> >" ] } ], @@ -342,7 +341,7 @@ "\n" ], "text": [ - " *' at 0x7fad7cc5f4e0> >" + " *' at 0x7f2bb4720660> >" ] } ], @@ -371,10 +370,11 @@ "evalue": "Command 'non-existing-command' returned non-zero exit status 127", "output_type": "pyerr", "traceback": [ - "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m\n\u001b[0;31mCalledProcessError\u001b[0m Traceback (most recent call last)", + "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m", + "\u001b[0;31mCalledProcessError\u001b[0m Traceback (most recent call last)", "\u001b[0;32m\u001b[0m in \u001b[0;36m\u001b[0;34m()\u001b[0m\n\u001b[0;32m----> 1\u001b[0;31m \u001b[0mspot\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mautomaton\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m'non-existing-command|'\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m", - "\u001b[0;32m/home/adl/git/spot/python/spot.py\u001b[0m in \u001b[0;36mautomaton\u001b[0;34m(filename, **kwargs)\u001b[0m\n\u001b[1;32m 457\u001b[0m See `spot.automata` for a list of supported formats.\"\"\"\n\u001b[1;32m 458\u001b[0m \u001b[0;32mtry\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 459\u001b[0;31m \u001b[0;32mreturn\u001b[0m \u001b[0mnext\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mautomata\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0;34m**\u001b[0m\u001b[0mkwargs\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 460\u001b[0m \u001b[0;32mexcept\u001b[0m \u001b[0mStopIteration\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 461\u001b[0m \u001b[0;32mraise\u001b[0m \u001b[0mRuntimeError\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m\"Failed to read automaton from {}\"\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mformat\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n", - "\u001b[0;32m/home/adl/git/spot/python/spot.py\u001b[0m in \u001b[0;36mautomata\u001b[0;34m(timeout, ignore_abort, trust_hoa, debug, *sources)\u001b[0m\n\u001b[1;32m 442\u001b[0m \u001b[0;32mdel\u001b[0m \u001b[0mproc\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 443\u001b[0m \u001b[0;32mif\u001b[0m \u001b[0mret\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 444\u001b[0;31m \u001b[0;32mraise\u001b[0m \u001b[0msubprocess\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mCalledProcessError\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mret\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mfilename\u001b[0m\u001b[0;34m[\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m-\u001b[0m\u001b[0;36m1\u001b[0m\u001b[0;34m]\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 445\u001b[0m \u001b[0;31m# deleting o explicitely now prevents Python 3.5 from\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 446\u001b[0m \u001b[0;31m# reporting the following error: \" 465\u001b[0;31m \u001b[0;32mreturn\u001b[0m \u001b[0mnext\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mautomata\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0;34m**\u001b[0m\u001b[0mkwargs\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 466\u001b[0m \u001b[0;32mexcept\u001b[0m \u001b[0mStopIteration\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 467\u001b[0m \u001b[0;32mraise\u001b[0m \u001b[0mRuntimeError\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m\"Failed to read automaton from {}\"\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mformat\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n", + "\u001b[0;32m/home/adl/git/spot/python/spot/__init__.py\u001b[0m in \u001b[0;36mautomata\u001b[0;34m(timeout, ignore_abort, trust_hoa, no_sid, debug, *sources)\u001b[0m\n\u001b[1;32m 448\u001b[0m \u001b[0;32mdel\u001b[0m \u001b[0mproc\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 449\u001b[0m \u001b[0;32mif\u001b[0m \u001b[0mret\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 450\u001b[0;31m \u001b[0;32mraise\u001b[0m \u001b[0msubprocess\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mCalledProcessError\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mret\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mfilename\u001b[0m\u001b[0;34m[\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m-\u001b[0m\u001b[0;36m1\u001b[0m\u001b[0;34m]\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 451\u001b[0m \u001b[0;31m# deleting o explicitely now prevents Python 3.5 from\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 452\u001b[0m \u001b[0;31m# reporting the following error: \"\n" ], "text": [ - " *' at 0x7fad7cc5f780> >" + " *' at 0x7f2bb4720570> >" ] }, { @@ -453,9 +453,10 @@ "evalue": "Command 'ltl2tgba \"syntax U U error\"' returned non-zero exit status 2", "output_type": "pyerr", "traceback": [ - "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m\n\u001b[0;31mCalledProcessError\u001b[0m Traceback (most recent call last)", + "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m", + "\u001b[0;31mCalledProcessError\u001b[0m Traceback (most recent call last)", "\u001b[0;32m\u001b[0m in \u001b[0;36m\u001b[0;34m()\u001b[0m\n\u001b[0;32m----> 1\u001b[0;31m \u001b[0;32mfor\u001b[0m \u001b[0ma\u001b[0m \u001b[0;32min\u001b[0m \u001b[0mspot\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mautomata\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m\"ltl2tgba 'a U b'|\"\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0;34m'ltl2tgba \"syntax U U error\"|'\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 2\u001b[0m \u001b[0mdisplay\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0ma\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n", - "\u001b[0;32m/home/adl/git/spot/python/spot.py\u001b[0m in \u001b[0;36mautomata\u001b[0;34m(timeout, ignore_abort, trust_hoa, debug, *sources)\u001b[0m\n\u001b[1;32m 442\u001b[0m \u001b[0;32mdel\u001b[0m \u001b[0mproc\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 443\u001b[0m \u001b[0;32mif\u001b[0m \u001b[0mret\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 444\u001b[0;31m \u001b[0;32mraise\u001b[0m \u001b[0msubprocess\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mCalledProcessError\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mret\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mfilename\u001b[0m\u001b[0;34m[\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m-\u001b[0m\u001b[0;36m1\u001b[0m\u001b[0;34m]\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 445\u001b[0m \u001b[0;31m# deleting o explicitely now prevents Python 3.5 from\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 446\u001b[0m \u001b[0;31m# reporting the following error: \" 450\u001b[0;31m \u001b[0;32mraise\u001b[0m \u001b[0msubprocess\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mCalledProcessError\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mret\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mfilename\u001b[0m\u001b[0;34m[\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m-\u001b[0m\u001b[0;36m1\u001b[0m\u001b[0;34m]\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 451\u001b[0m \u001b[0;31m# deleting o explicitely now prevents Python 3.5 from\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 452\u001b[0m \u001b[0;31m# reporting the following error: \" 465\u001b[0;31m \u001b[0;32mreturn\u001b[0m \u001b[0mnext\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mautomata\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0;34m**\u001b[0m\u001b[0mkwargs\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 466\u001b[0m \u001b[0;32mexcept\u001b[0m \u001b[0mStopIteration\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n", + "\u001b[0;31mStopIteration\u001b[0m: ", + "\nDuring handling of the above exception, another exception occurred:\n", + "\u001b[0;31mRuntimeError\u001b[0m Traceback (most recent call last)", "\u001b[0;32m\u001b[0m in \u001b[0;36m\u001b[0;34m()\u001b[0m\n\u001b[0;32m----> 1\u001b[0;31m \u001b[0mspot\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mautomaton\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m'true|'\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m", - "\u001b[0;32m/home/adl/git/spot/python/spot.py\u001b[0m in \u001b[0;36mautomaton\u001b[0;34m(filename, **kwargs)\u001b[0m\n\u001b[1;32m 459\u001b[0m \u001b[0;32mreturn\u001b[0m \u001b[0mnext\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mautomata\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0;34m**\u001b[0m\u001b[0mkwargs\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 460\u001b[0m \u001b[0;32mexcept\u001b[0m \u001b[0mStopIteration\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 461\u001b[0;31m \u001b[0;32mraise\u001b[0m \u001b[0mRuntimeError\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m\"Failed to read automaton from {}\"\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mformat\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 462\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 463\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n", + "\u001b[0;32m/home/adl/git/spot/python/spot/__init__.py\u001b[0m in \u001b[0;36mautomaton\u001b[0;34m(filename, **kwargs)\u001b[0m\n\u001b[1;32m 465\u001b[0m \u001b[0;32mreturn\u001b[0m \u001b[0mnext\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mautomata\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0;34m**\u001b[0m\u001b[0mkwargs\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 466\u001b[0m \u001b[0;32mexcept\u001b[0m \u001b[0mStopIteration\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 467\u001b[0;31m \u001b[0;32mraise\u001b[0m \u001b[0mRuntimeError\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m\"Failed to read automaton from {}\"\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mformat\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 468\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 469\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n", "\u001b[0;31mRuntimeError\u001b[0m: Failed to read automaton from true|" ] } ], "prompt_number": 6 - }, - { - "cell_type": "code", - "collapsed": false, - "input": [], - "language": "python", - "metadata": {}, - "outputs": [] } ], "metadata": {} } ] -} \ No newline at end of file +} diff --git a/tests/python/testingaut.ipynb b/tests/python/testingaut.ipynb index 9d7f44e85..1185ceb52 100644 --- a/tests/python/testingaut.ipynb +++ b/tests/python/testingaut.ipynb @@ -1,7 +1,23 @@ { "metadata": { - "name": "", - "signature": "sha256:1a85b698ebae51aaba0387d782d1cf5c6cdf54f69dd6b4b9c7189f8676eb4c88" + "kernelspec": { + "display_name": "Python 3", + "language": "python", + "name": "python3" + }, + "language_info": { + "codemirror_mode": { + "name": "ipython", + "version": 3 + }, + "file_extension": ".py", + "mimetype": "text/x-python", + "name": "python", + "nbconvert_exporter": "python", + "pygments_lexer": "ipython3", + "version": "3.5.3" + }, + "name": "" }, "nbformat": 3, "nbformat_minor": 0, @@ -58,36 +74,36 @@ "G\n", "\n", "\n", - "\n", - "1\n", + "\n", + "0\n", "\n", - "1\n", + "0\n", "\n", - "\n", - "I->1\n", + "\n", + "I->0\n", "\n", "\n", "\n", - "\n", - "1->1\n", + "\n", + "0->0\n", "\n", "\n", "a\n", "\n", - "\n", - "0\n", + "\n", + "1\n", "\n", "\n", - "0\n", + "1\n", "\n", - "\n", - "1->0\n", + "\n", + "0->1\n", "\n", "\n", "b\n", "\n", - "\n", - "0->0\n", + "\n", + "1->1\n", "\n", "\n", "b\n", @@ -96,7 +112,7 @@ "\n" ], "text": [ - " *' at 0x7f2e817bf6c0> >" + " *' at 0x7f99b4744e40> >" ] } ], @@ -125,240 +141,240 @@ "output_type": "pyout", "prompt_number": 3, "svg": [ - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "1\n", - "\n", - "init\n", + "\n", + "init\n", "\n", "\n", "0->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "2\n", - "\n", - "1\n", - "!a & b\n", + "\n", + "0\n", + "!a & b\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "3\n", - "\n", - "1\n", - "a & b\n", + "\n", + "0\n", + "a & b\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "4\n", - "\n", - "1\n", - "a & !b\n", + "\n", + "0\n", + "a & !b\n", "\n", "\n", "1->4\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "5\n", - "\n", - "\n", - "0\n", - "a & b\n", + "\n", + "\n", + "1\n", + "a & b\n", "\n", "\n", "2->5\n", - "\n", - "\n", - "{a}\n", + "\n", + "\n", + "{a}\n", "\n", "\n", "6\n", - "\n", - "\n", - "0\n", - "!a & b\n", + "\n", + "\n", + "1\n", + "!a & b\n", "\n", "\n", "2->6\n", - "\n", - "\n", - "{}\n", + "\n", + "\n", + "{}\n", "\n", "\n", "7\n", - "\n", - "\n", - "0\n", - "a & !b\n", + "\n", + "\n", + "1\n", + "a & !b\n", "\n", "\n", "2->7\n", - "\n", - "\n", - "{a, b}\n", + "\n", + "\n", + "{a, b}\n", "\n", "\n", "8\n", - "\n", - "\n", - "0\n", - "!a & !b\n", + "\n", + "\n", + "1\n", + "!a & !b\n", "\n", "\n", "2->8\n", - "\n", - "\n", - "{b}\n", + "\n", + "\n", + "{b}\n", "\n", "\n", - "3->2\n", - "\n", - "\n", - "{a}\n", + "3->2\n", + "\n", + "\n", + "{a}\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "{}\n", + "3->3\n", + "\n", + "\n", + "{}\n", "\n", "\n", - "3->4\n", - "\n", - "\n", - "{b}\n", + "3->4\n", + "\n", + "\n", + "{b}\n", "\n", "\n", - "3->5\n", - "\n", - "\n", - "{}\n", + "3->5\n", + "\n", + "\n", + "{}\n", "\n", "\n", - "3->6\n", - "\n", - "\n", - "{a}\n", + "3->6\n", + "\n", + "\n", + "{a}\n", "\n", "\n", - "3->7\n", - "\n", - "\n", - "{b}\n", + "3->7\n", + "\n", + "\n", + "{b}\n", "\n", "\n", - "3->8\n", - "\n", - "\n", - "{a, b}\n", + "3->8\n", + "\n", + "\n", + "{a, b}\n", "\n", "\n", "9\n", - "\n", - "1\n", - "!a & !b\n", + "\n", + "0\n", + "!a & !b\n", "\n", "\n", - "3->9\n", - "\n", - "\n", - "{a, b}\n", + "3->9\n", + "\n", + "\n", + "{a, b}\n", "\n", "\n", "4->2\n", - "\n", - "\n", - "{a, b}\n", + "\n", + "\n", + "{a, b}\n", "\n", "\n", "4->3\n", - "\n", - "\n", - "{b}\n", + "\n", + "\n", + "{b}\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "{}\n", + "\n", + "\n", + "{}\n", "\n", "\n", "4->9\n", - "\n", - "\n", - "{a}\n", + "\n", + "\n", + "{a}\n", "\n", "\n", "5->5\n", - "\n", - "\n", - "{}\n", + "\n", + "\n", + "{}\n", "\n", "\n", "5->6\n", - "\n", - "\n", - "{a}\n", + "\n", + "\n", + "{a}\n", "\n", "\n", "5->7\n", - "\n", - "\n", - "{b}\n", + "\n", + "\n", + "{b}\n", "\n", "\n", "5->8\n", - "\n", - "\n", - "{a, b}\n", + "\n", + "\n", + "{a, b}\n", "\n", "\n", "6->5\n", - "\n", - "\n", - "{a}\n", + "\n", + "\n", + "{a}\n", "\n", "\n", "6->6\n", - "\n", - "\n", - "{}\n", + "\n", + "\n", + "{}\n", "\n", "\n", "6->7\n", - "\n", - "\n", - "{a, b}\n", + "\n", + "\n", + "{a, b}\n", "\n", "\n", "6->8\n", - "\n", - "\n", - "{b}\n", + "\n", + "\n", + "{b}\n", "\n", "\n", "" ], "text": [ - "" + "" ] } ], @@ -386,124 +402,124 @@ "output_type": "pyout", "prompt_number": 4, "svg": [ - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "1\n", - "\n", - "init\n", + "\n", + "init\n", "\n", "\n", "0->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "2\n", - "\n", - "1\n", - "!a & b\n", + "\n", + "0\n", + "!a & b\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "3\n", - "\n", - "1\n", - "a & b\n", + "\n", + "0\n", + "a & b\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "4\n", - "\n", - "1\n", - "a & !b\n", + "\n", + "0\n", + "a & !b\n", "\n", "\n", "1->4\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "5\n", - "\n", - "\n", - "0\n", - "a & b\n", + "\n", + "\n", + "1\n", + "a & b\n", "\n", "\n", "2->5\n", - "\n", - "\n", - "{a}\n", + "\n", + "\n", + "{a}\n", "\n", "\n", - "3->2\n", - "\n", - "\n", - "{a}\n", + "3->2\n", + "\n", + "\n", + "{a}\n", "\n", "\n", - "3->4\n", - "\n", - "\n", - "{b}\n", + "3->4\n", + "\n", + "\n", + "{b}\n", "\n", "\n", "6\n", - "\n", - "\n", - "0\n", - "!a & b\n", + "\n", + "\n", + "1\n", + "!a & b\n", "\n", "\n", - "3->6\n", - "\n", - "\n", - "{a}\n", + "3->6\n", + "\n", + "\n", + "{a}\n", "\n", "\n", "4->2\n", - "\n", - "\n", - "{a, b}\n", + "\n", + "\n", + "{a, b}\n", "\n", "\n", "4->3\n", - "\n", - "\n", - "{b}\n", + "\n", + "\n", + "{b}\n", "\n", "\n", "5->6\n", - "\n", - "\n", - "{a}\n", + "\n", + "\n", + "{a}\n", "\n", "\n", "6->5\n", - "\n", - "\n", - "{a}\n", + "\n", + "\n", + "{a}\n", "\n", "\n", "" ], "text": [ - "" + "" ] } ], @@ -530,122 +546,114 @@ "output_type": "pyout", "prompt_number": 5, "svg": [ - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "1\n", - "\n", - "init\n", + "\n", + "init\n", "\n", "\n", "0->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "4\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "1->4\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "5\n", - "\n", - "\n", - "4\n", + "\n", + "\n", + "4\n", "\n", "\n", "2->5\n", - "\n", - "\n", - "{a}\n", + "\n", + "\n", + "{a}\n", "\n", "\n", - "3->2\n", - "\n", - "\n", - "{a}\n", + "3->2\n", + "\n", + "\n", + "{a}\n", "\n", "\n", - "3->4\n", - "\n", - "\n", - "{b}\n", + "3->4\n", + "\n", + "\n", + "{b}\n", "\n", "\n", - "3->5\n", - "\n", - "\n", - "{a}\n", + "3->5\n", + "\n", + "\n", + "{a}\n", "\n", "\n", "4->2\n", - "\n", - "\n", - "{a, b}\n", + "\n", + "\n", + "{a, b}\n", "\n", "\n", "4->3\n", - "\n", - "\n", - "{b}\n", + "\n", + "\n", + "{b}\n", "\n", "\n", "5->5\n", - "\n", - "\n", - "{a}\n", + "\n", + "\n", + "{a}\n", "\n", "\n", "" ], "text": [ - "" + "" ] } ], "prompt_number": 5 - }, - { - "cell_type": "code", - "collapsed": false, - "input": [], - "language": "python", - "metadata": {}, - "outputs": [] } ], "metadata": {} } ] -} \ No newline at end of file +} diff --git a/tests/python/word.ipynb b/tests/python/word.ipynb index 7e554b7d3..d5e7e61ec 100644 --- a/tests/python/word.ipynb +++ b/tests/python/word.ipynb @@ -1,7 +1,23 @@ { "metadata": { - "name": "", - "signature": "sha256:4fc3934cf5fa0e612923dc4253b5e40115b103a93f588595a6706ec77e7994a9" + "kernelspec": { + "display_name": "Python 3", + "language": "python", + "name": "python3" + }, + "language_info": { + "codemirror_mode": { + "name": "ipython", + "version": 3 + }, + "file_extension": ".py", + "mimetype": "text/x-python", + "name": "python", + "nbconvert_exporter": "python", + "pygments_lexer": "ipython3", + "version": "3.5.3" + }, + "name": "" }, "nbformat": 3, "nbformat_minor": 0, @@ -31,7 +47,7 @@ "cell_type": "code", "collapsed": false, "input": [ - "aut = spot.translate('G(Fa <-> Xb)'); aut" + "aut = spot.translate('G(Fa <-> XXb)'); aut" ], "language": "python", "metadata": {}, @@ -47,99 +63,150 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\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", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", - "\n", - "0->3\n", - "\n", - "\n", - "!a\n", + "\n", + "1->3\n", + "\n", + "\n", + "a\n", "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!a & b\n", + "\n", + "4\n", + "\n", + "4\n", "\n", - "\n", - "1->2\n", - "\n", - "\n", - "a & b\n", - "\u24ff\n", + "\n", + "1->4\n", + "\n", + "\n", + "!a\n", "\n", - "\n", - "2->1\n", - "\n", - "\n", - "!a & b\n", + "\n", + "5\n", + "\n", + "5\n", "\n", - "\n", - "2->2\n", - "\n", - "\n", - "a & b\n", - "\u24ff\n", + "\n", + "1->5\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "2->3\n", - "\n", - "\n", - "!a & b\n", + "2->3\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "6\n", + "\n", + "6\n", + "\n", + "\n", + "2->6\n", + "\n", + "\n", + "!a\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "!a & !b\n", - "\u24ff\n", + "\n", + "\n", + "a & b\n", + "\u24ff\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "3->5\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "a & b\n", + "\u24ff\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "5->6\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "6->6\n", + "\n", + "\n", + "!a & !b\n", + "\u24ff\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7fb71c0e18a0> >" + " *' at 0x7fdf783f0510> >" ] } ], @@ -168,12 +235,12 @@ "text": [ "Prefix:\n", " 0\n", - " | !a\n", - "Cycle:\n", + " | a\n", " 1\n", - " | a & b\t{0}\n", - " 2\n", - " | !a & b" + " | a\n", + "Cycle:\n", + " 3\n", + " | a & b\t{0}" ] } ], @@ -200,7 +267,7 @@ "output_type": "stream", "stream": "stdout", "text": [ - "!a\n", + "a\n", "{0}\n" ] } @@ -228,7 +295,7 @@ "output_type": "pyout", "prompt_number": 5, "text": [ - "!a; cycle{a & b; !a & b}" + "a; a; cycle{a & b}" ] } ], @@ -246,8 +313,8 @@ "collapsed": false, "input": [ "print(spot.bdd_format_formula(aut.get_dict(), word.prefix[0]))\n", - "print(spot.bdd_format_formula(aut.get_dict(), word.cycle[0]))\n", - "print(spot.bdd_format_formula(aut.get_dict(), word.cycle[1]))" + "print(spot.bdd_format_formula(aut.get_dict(), word.prefix[1]))\n", + "print(spot.bdd_format_formula(aut.get_dict(), word.cycle[0]))" ], "language": "python", "metadata": {}, @@ -256,9 +323,9 @@ "output_type": "stream", "stream": "stdout", "text": [ - "!a\n", - "a & b\n", - "!a & b\n" + "a\n", + "a\n", + "a & b\n" ] } ], @@ -268,7 +335,7 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "Calling `simplifify()` will produce a shorter word that is compatible with the original word. For instance in the above word, the initial `!a` is compatible with both `a & b` and `!a & b`. The word obtained by restricting `!a` to `!a & b` is therefore still accepted, but it allows removing the prefix by rotating the cycle:" + "Calling `simplifify()` will produce a shorter word that is compatible with the original word. For instance in the above word, the initial `a` is compatible with both `a & b` and `a & !b`. The word obtained by restricting `a` to `a & b` is therefore still accepted, allowing us to remove the prefix." ] }, { @@ -286,7 +353,7 @@ "output_type": "pyout", "prompt_number": 7, "text": [ - "cycle{!a & b; a & b}" + "cycle{a & b}" ] } ], @@ -313,7 +380,7 @@ "output_type": "pyout", "prompt_number": 8, "text": [ - "cycle{!a & b; a & b}" + "cycle{a & b}" ] } ], @@ -478,7 +545,7 @@ "\n" ], "text": [ - " *' at 0x7fb71c0e1a20> >" + " *' at 0x7fdf783f0e40> >" ] } ], @@ -598,9 +665,10 @@ "evalue": "a twa_word may not have an empty cycle", "output_type": "pyerr", "traceback": [ - "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m\n\u001b[0;31mRuntimeError\u001b[0m Traceback (most recent call last)", + "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m", + "\u001b[0;31mRuntimeError\u001b[0m Traceback (most recent call last)", "\u001b[0;32m\u001b[0m in \u001b[0;36m\u001b[0;34m()\u001b[0m\n\u001b[1;32m 1\u001b[0m \u001b[0;31m# ... as long as this word is not printed.\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m----> 2\u001b[0;31m \u001b[0mprint\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mw\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m", - "\u001b[0;32m/home/adl/git/spot/python/spot/impl.py\u001b[0m in \u001b[0;36m__str__\u001b[0;34m(self)\u001b[0m\n\u001b[1;32m 3599\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 3600\u001b[0m \u001b[0;32mdef\u001b[0m \u001b[0m__str__\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mself\u001b[0m\u001b[0;34m)\u001b[0m \u001b[0;34m->\u001b[0m \u001b[0;34m\"std::string\"\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m-> 3601\u001b[0;31m \u001b[0;32mreturn\u001b[0m \u001b[0m_impl\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mtwa_word___str__\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mself\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 3602\u001b[0m \u001b[0mtwa_word_swigregister\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0m_impl\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mtwa_word_swigregister\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 3603\u001b[0m \u001b[0mtwa_word_swigregister\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mtwa_word\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n", + "\u001b[0;32m/home/adl/git/spot/python/spot/impl.py\u001b[0m in \u001b[0;36m__str__\u001b[0;34m(self)\u001b[0m\n\u001b[1;32m 4160\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 4161\u001b[0m \u001b[0;32mdef\u001b[0m \u001b[0m__str__\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mself\u001b[0m\u001b[0;34m)\u001b[0m \u001b[0;34m->\u001b[0m \u001b[0;34m\"std::string\"\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m-> 4162\u001b[0;31m \u001b[0;32mreturn\u001b[0m \u001b[0m_impl\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mtwa_word___str__\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mself\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 4163\u001b[0m \u001b[0mtwa_word_swigregister\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0m_impl\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mtwa_word_swigregister\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 4164\u001b[0m \u001b[0mtwa_word_swigregister\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mtwa_word\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n", "\u001b[0;31mRuntimeError\u001b[0m: a twa_word may not have an empty cycle" ] } @@ -611,4 +679,4 @@ "metadata": {} } ] -} \ No newline at end of file +} From 526b299de8ea0e2a341b7875d62eb09de7f3f5ea Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 2 Jun 2017 19:07:34 +0200 Subject: [PATCH 04/13] work around change in pandas 0.20 * tests/core/ltlcross4.test: Replace describe() by agg() to work around a backward incompatible change in pandas 0.20. --- tests/core/ltlcross4.test | 44 +++++++++++++-------------------------- 1 file changed, 15 insertions(+), 29 deletions(-) diff --git a/tests/core/ltlcross4.test b/tests/core/ltlcross4.test index 2f0c5f5ca..e710fcfee 100755 --- a/tests/core/ltlcross4.test +++ b/tests/core/ltlcross4.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et +# Copyright (C) 2012-2014, 2017 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -40,49 +40,35 @@ cat >test.py <out.1 # remove trailing whitespace from pandas' output, -# and limit to 26 lines, because Pandas 0.13 adds +# and limit to 6 lines, because Pandas 0.13 adds # the size of the dataframe afterwards. -sed 's/[ \t]*$//g;26q' py.out +sed 's/[ \t]*$//g;6q' py.out cat >expected < Date: Sat, 3 Jun 2017 11:03:58 +0200 Subject: [PATCH 05/13] * tests/core/ltlcross4.test: Ignore space diff in pandas' output. --- tests/core/ltlcross4.test | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/tests/core/ltlcross4.test b/tests/core/ltlcross4.test index e710fcfee..84c0ada0d 100755 --- a/tests/core/ltlcross4.test +++ b/tests/core/ltlcross4.test @@ -57,18 +57,19 @@ EOF # will exit 77 if panda is not installed $PYTHON test.py >out.1 -# remove trailing whitespace from pandas' output, -# and limit to 6 lines, because Pandas 0.13 adds -# the size of the dataframe afterwards. -sed 's/[ \t]*$//g;6q' py.out +# remove trailing whitespace from pandas' output, and limit to 6 +# lines, because Pandas 0.13 adds the size of the dataframe +# afterwards. Alse the spacing between columns differs from version +# to version. +sed 's/[ \t]*$//g;6q' py.out cat >expected < Date: Wed, 7 Jun 2017 17:05:25 +0200 Subject: [PATCH 06/13] ikwiad: fix accepting run printing * tests/core/ikwiad.cc: here. --- tests/core/ikwiad.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/core/ikwiad.cc b/tests/core/ikwiad.cc index 73a0e9ac8..1e8c6382a 100644 --- a/tests/core/ikwiad.cc +++ b/tests/core/ikwiad.cc @@ -1531,7 +1531,7 @@ checked_main(int argc, char** argv) if (graph_run_tgba_opt) spot::print_dot(std::cout, run->as_twa()); else - std::cout << run; + std::cout << *run; tm.stop("printing accepting run"); } } From 97e903b13d9742e2ffd8681b1762de5f3dc9db84 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 7 Jun 2017 14:46:55 +0200 Subject: [PATCH 07/13] libtool: surrender to Debian's castrated libtool The libtool version distributed by Debian is patched to *not* propagate dependencies (i.e., if libA depends on libB, then linking against libA will not automatically link against libB, it has to be explicit), contrary to what the Libtool manual document. So now we explicitly link against both libA and libB in such case. * configure.ac: Remove the workaround that does not work for MinGW. * doc/org/compile.org: Mention the issue. * bin/Makefile.am, tests/Makefile.am, spot/ltsmin/Makefile.am, doc/org/g++wrap.in: Make the dependencies explicit. --- bin/Makefile.am | 3 ++- configure.ac | 6 ------ doc/org/compile.org | 6 ++++-- doc/org/g++wrap.in | 3 ++- spot/ltsmin/Makefile.am | 2 ++ tests/Makefile.am | 5 +++-- 6 files changed, 13 insertions(+), 12 deletions(-) diff --git a/bin/Makefile.am b/bin/Makefile.am index 85e5ca059..d1f64ff95 100644 --- a/bin/Makefile.am +++ b/bin/Makefile.am @@ -25,7 +25,8 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS) LDADD = \ libcommon.a \ $(top_builddir)/lib/libgnu.la \ - $(top_builddir)/spot/libspot.la + $(top_builddir)/spot/libspot.la \ + $(top_builddir)/buddy/src/libbddx.la noinst_LIBRARIES = libcommon.a libcommon_a_SOURCES = \ diff --git a/configure.ac b/configure.ac index 9489dcf03..f4004c6c0 100644 --- a/configure.ac +++ b/configure.ac @@ -171,12 +171,6 @@ AC_CHECK_FUNCS([times kill alarm sigaction]) LT_CONFIG_LTDL_DIR([ltdl]) LT_INIT([win32-dll]) LTDL_INIT([subproject convenience]) -# Debian resets this to no, but this break both Spot and the libtool -# test suite itself. Instead of requiring developer to install a -# non-patched version of Libtool on any Debian they use, we just -# cancel the effect of Debian's patch here. -link_all_deplibs=yes -link_all_deplibs_CXX=yes AX_BSYMBOLIC diff --git a/doc/org/compile.org b/doc/org/compile.org index 17c219a8c..7f0bd04bc 100644 --- a/doc/org/compile.org +++ b/doc/org/compile.org @@ -210,8 +210,10 @@ library. This should be as simple as adding =-lbddx= after =-lspot= in the first three cases. In the fourth case where =libtool= is used to link against -=libspot.la= linking against =libbddx.la= is not necessary because -Libtool already handles such dependencies. +=libspot.la= linking against =libbddx.la= should not be necessary because +Libtool already handles such dependencies. However the version of =libtool= +distributed with Debian is patched to ignore those dependencies, so in this +case you 2 * Additional suggestions diff --git a/doc/org/g++wrap.in b/doc/org/g++wrap.in index 4bd319840..7a11c0d8b 100755 --- a/doc/org/g++wrap.in +++ b/doc/org/g++wrap.in @@ -3,4 +3,5 @@ # example run from the org-mode file are all linked with Spot. exec @top_builddir@/libtool link @CXX@ -std=c++11 -Wall \ -I@abs_top_builddir@ -I@abs_top_srcdir@ -I@abs_top_srcdir@/buddy/src \ - "$@" @abs_top_builddir@/spot/libspot.la + "$@" @abs_top_builddir@/spot/libspot.la \ + @abs_top_builddir@/buddy/src/libbddx.la diff --git a/spot/ltsmin/Makefile.am b/spot/ltsmin/Makefile.am index fee392da7..3204ba4c9 100644 --- a/spot/ltsmin/Makefile.am +++ b/spot/ltsmin/Makefile.am @@ -28,9 +28,11 @@ ltsmin_HEADERS = ltsmin.hh lib_LTLIBRARIES = libspotltsmin.la libspotltsmin_la_DEPENDENCIES = \ $(top_builddir)/spot/libspot.la \ + $(top_builddir)/buddy/src/libbddx.la \ $(LTDLDEPS) libspotltsmin_la_LIBADD = \ $(top_builddir)/spot/libspot.la \ + $(top_builddir)/buddy/src/libbddx.la \ $(LIBLTDL) -lpthread libspotltsmin_la_LDFLAGS = -no-undefined $(SYMBOLIC_LDFLAGS) libspotltsmin_la_SOURCES = ltsmin.cc diff --git a/tests/Makefile.am b/tests/Makefile.am index efc77fe19..fd2d01047 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -24,7 +24,8 @@ AUTOMAKE_OPTIONS = subdir-objects AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) AM_CXXFLAGS = $(WARNING_CXXFLAGS) -LDADD = $(top_builddir)/spot/libspot.la +LDADD = $(top_builddir)/spot/libspot.la $(top_builddir)/buddy/src/libbddx.la + # Explicitely set it to avoid default value ".test" TEST_EXTENSIONS = @@ -377,7 +378,7 @@ if USE_LTSMIN check_PROGRAMS += ltsmin/modelcheck ltsmin_modelcheck_SOURCES = ltsmin/modelcheck.cc -ltsmin_modelcheck_LDADD = $(top_builddir)/spot/ltsmin/libspotltsmin.la +ltsmin_modelcheck_LDADD = $(top_builddir)/spot/ltsmin/libspotltsmin.la $(LDADD) check_SCRIPTS += ltsmin/defs From 20a4959ff609d957bc9dcd94b8eb85b6b955b873 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 19 Jun 2017 17:06:56 +0200 Subject: [PATCH 08/13] stats: fix slow %s and inappropriate %S output Fixes #269. * spot/twaalgos/stats.cc: Use twa_statistics instead of twa_sub_statistics when %t is not used. * bin/common_aoutput.cc: Likewise, also fix %S to use twa_statistics instead of num_states(), and document that %s,%t,%e all return statistics about the reachable part of the automaton. * tests/core/format.test: Add more tests. * NEWS: Document the issue. --- NEWS | 6 ++++ bin/common_aoutput.cc | 18 +++++------- spot/twaalgos/stats.cc | 2 +- tests/core/format.test | 66 ++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 81 insertions(+), 11 deletions(-) diff --git a/NEWS b/NEWS index 86bb18e02..21d59a354 100644 --- a/NEWS +++ b/NEWS @@ -11,6 +11,12 @@ New in spot 2.3.4.dev (not yet released) SCC) or 'y' (split universal destination by colors) universal edges could be connected to undefined states. + - Using --stats=%s or --stats=%s or --stats=%t could take an + unnecessary long time on automata with many atomic propositions, + due to a typo. Furthermore, %s/%e/%t/%E/%T were printing + a number of reachable states/edges/transitions, but %S was + incorrectly counting all states even unreachable. + New in spot 2.3.4 (2017-05-11) Bugs fixed: diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc index 18a9ef6fb..10ddaee8b 100644 --- a/bin/common_aoutput.cc +++ b/bin/common_aoutput.cc @@ -166,11 +166,11 @@ static const argp_option io_options[] = { "%M, %m", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "name of the automaton", 0 }, { "%S, %s", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, - "number of states", 0 }, + "number of reachable states", 0 }, { "%E, %e", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, - "number of edges", 0 }, + "number of reachable edges", 0 }, { "%T, %t", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, - "number of transitions", 0 }, + "number of reachable transitions", 0 }, { "%A, %a", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "number of acceptance sets", 0 }, { "%G, %g", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, @@ -227,11 +227,11 @@ static const argp_option o_options[] = { "%m", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "name of the automaton", 0 }, { "%s", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, - "number of states", 0 }, + "number of reachable states", 0 }, { "%e", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, - "number of edges", 0 }, + "number of reachable edges", 0 }, { "%t", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, - "number of transitions", 0 }, + "number of reachable transitions", 0 }, { "%a", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "number of acceptance sets", 0 }, { "%g", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, @@ -422,9 +422,9 @@ hoa_stat_printer::print(const spot::const_parsed_aut_ptr& haut, haut_edges_ = s.edges; haut_trans_ = s.transitions; } - else if (has('E')) + else if (has('E') || has('S')) { - spot::twa_sub_statistics s = sub_stats_reachable(haut->aut); + spot::twa_statistics s = stats_reachable(haut->aut); haut_states_ = s.states; haut_edges_ = s.edges; } @@ -436,8 +436,6 @@ hoa_stat_printer::print(const spot::const_parsed_aut_ptr& haut, else haut_name_.val().clear(); } - if (has('S')) - haut_states_ = haut->aut->num_states(); if (has('A')) haut_acc_ = haut->aut->acc().num_sets(); diff --git a/spot/twaalgos/stats.cc b/spot/twaalgos/stats.cc index e521c7efe..db9c998b7 100644 --- a/spot/twaalgos/stats.cc +++ b/spot/twaalgos/stats.cc @@ -346,7 +346,7 @@ namespace spot } else if (has('s') || has('e')) { - twa_sub_statistics s = sub_stats_reachable(aut); + twa_statistics s = stats_reachable(aut); states_ = s.states; edges_ = s.edges; } diff --git a/tests/core/format.test b/tests/core/format.test index 5b5073241..8f178b3ba 100644 --- a/tests/core/format.test +++ b/tests/core/format.test @@ -74,3 +74,69 @@ test "1,3,1,3,2,1,0" = "$out" ltl2tgba 'a' --stats='%[z]c' 2>stderr && exit 1 cat stderr grep -F "ltl2tgba: unknown option 'z' in '%[z]c'" stderr + + +# From issue #269. +f='!X(FG((a & b) | (a & c) | (a & d) | (a & e) | (a & f) | (g & h) | +(g & i) | (g & j) | (g & k) | (g & l) | (m & n) | (m & o) | (m & p) | +(m & q) | (m & r) | (s & t) | (s & u) | (s & v) | (s & w) | (s & x) | +(y & z) | (ab & y) | (bb & y) | (cb & y) | (db & y) | (eb & g) | (c & +eb) | (d & eb) | (e & eb) | (eb & f) | (b & m) | (b & i) | (b & j) | +(b & k) | (b & l) | (h & s) | (h & o) | (h & p) | (h & q) | (h & r) | +(n & y) | (n & u) | (n & v) | (n & w) | (n & x) | (fb & t) | (ab & t) +| (bb & t) | (cb & t) | (db & t) | (g & gb) | (b & gb) | (d & gb) | +(e & gb) | (f & gb) | (c & m) | (c & h) | (c & j) | (c & k) | (c & l) | +(i & s) | (i & n) | (i & p) | (i & q) | (i & r) | (o & y) | (o & t) | +(o & v) | (o & w) | (o & x) | (fb & u) | (u & z) | (bb & u) | (cb & +u) | (db & u) | (g & hb) | (b & hb) | (c & hb) | (e & hb) | (f & hb) | +(d & m) | (d & h) | (d & i) | (d & k) | (d & l) | (j & s) | (j & n) | +(j & o) | (j & q) | (j & r) | (p & y) | (p & t) | (p & u) | (p & w) | +(p & x) | (fb & v) | (v & z) | (ab & v) | (cb & v) | (db & v) | (g & +ib) | (b & ib) | (c & ib) | (d & ib) | (f & ib) | (e & m) | (e & h) | +(e & i) | (e & j) | (e & l) | (k & s) | (k & n) | (k & o) | (k & p) | +(k & r) | (q & y) | (q & t) | (q & u) | (q & v) | (q & x) | (fb & w) | +(w & z) | (ab & w) | (bb & w) | (db & w) | (g & jb) | (b & jb) | (c & +jb) | (d & jb) | (e & jb) | (f & m) | (f & h) | (f & i) | (f & j) | +(f & k) | (l & s) | (l & n) | (l & o) | (l & p) | (l & q) | (r & y) | +(r & t) | (r & u) | (r & v) | (r & w) | (fb & x) | (x & z) | (ab & x) | +(bb & x) | (cb & x)) U ((a & b) | (a & c) | (a & d) | (a & e) | (a & f) | +(g & h) | (g & i) | (g & j) | (g & k) | (g & l) | (m & n) | (m & o) | +(m & p) | (m & q) | (m & r) | (s & t) | (s & u) | (s & v) | (s & w) | +(s & x) | (y & z) | (ab & y) | (bb & y) | (cb & y) | (db & y) | (eb & +g) | (c & eb) | (d & eb) | (e & eb) | (eb & f) | (b & m) | (b & i) | +(b & j) | (b & k) | (b & l) | (h & s) | (h & o) | (h & p) | (h & q) | +(h & r) | (n & y) | (n & u) | (n & v) | (n & w) | (n & x) | (fb & t) | +(ab & t) | (bb & t) | (cb & t) | (db & t) | (g & gb) | (b & gb) | (d & +gb) | (e & gb) | (f & gb) | (c & m) | (c & h) | (c & j) | (c & k) | +(c & l) | (i & s) | (i & n) | (i & p) | (i & q) | (i & r) | (o & y) | +(o & t) | (o & v) | (o & w) | (o & x) | (fb & u) | (u & z) | (bb & u) +| (cb & u) | (db & u) | (g & hb) | (b & hb) | (c & hb) | (e & hb) | +(f & hb) | (d & m) | (d & h) | (d & i) | (d & k) | (d & l) | (j & s) | +(j & n) | (j & o) | (j & q) | (j & r) | (p & y) | (p & t) | (p & u) | +(p & w) | (p & x) | (fb & v) | (v & z) | (ab & v) | (cb & v) | (db & +v) | (g & ib) | (b & ib) | (c & ib) | (d & ib) | (f & ib) | (e & m) | +(e & h) | (e & i) | (e & j) | (e & l) | (k & s) | (k & n) | (k & o) | +(k & p) | (k & r) | (q & y) | (q & t) | (q & u) | (q & v) | (q & x) | +(fb & w) | (w & z) | (ab & w) | (bb & w) | (db & w) | (g & jb) | (b & +jb) | (c & jb) | (d & jb) | (e & jb) | (f & m) | (f & h) | (f & i) | +(f & j) | (f & k) | (l & s) | (l & n) | (l & o) | (l & p) | (l & q) | +(r & y) | (r & t) | (r & u) | (r & v) | (r & w) | (fb & x) | (x & z) | +(ab & x) | (bb & x) | (cb & x)))' +test 3,5 = `ltl2tgba --low --any --stats=%s,%e "$f"` + +cat >foo < Date: Mon, 19 Jun 2017 18:00:10 +0200 Subject: [PATCH 09/13] doc: Jessie -> Stretch * doc/org/install.org: Update. --- doc/org/install.org | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/doc/org/install.org b/doc/org/install.org index c60d5c64d..871cdf512 100644 --- a/doc/org/install.org +++ b/doc/org/install.org @@ -55,7 +55,7 @@ process. We build Debian packages for amd64 and i386, for both releases and the development versions. Packages for releases are built for Debian -Jessie (a.k.a. Debian stable) while packages for development are built +Stretch (a.k.a. Debian stable) while packages for development are built for Sid (a.k.a. Debian unstable). Here is how to install the stable packages: @@ -83,12 +83,6 @@ examples). The packages containing the libraries (=libspot0=, =libbddx0=, =libspotltsmin0=) are automatically installed as dependencies of the previous packages. -The stable packages should work in a recent *Ubuntu* as well, provided you -also add a path to a repository that distributes the GCC 4.9 runtime. -You can do that for instance with: - -#+BEGIN_SRC sh -add-apt-repository -y ppa:ubuntu-toolchain-r/test #+END_SRC * Installing from git From 3f71521625d421d819d2a83c1f215d735620dd5b Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 20 Jun 2017 15:17:28 +0200 Subject: [PATCH 10/13] [buddy] fix handling of bdd_apply_biimp * src/bddop.c: Fix shortcut. --- buddy/src/bddop.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/buddy/src/bddop.c b/buddy/src/bddop.c index b61eb9a96..5bd5821ee 100644 --- a/buddy/src/bddop.c +++ b/buddy/src/bddop.c @@ -656,8 +656,8 @@ static BDD apply_rec(BDD l, BDD r) l = r; \ r = tmp; \ } \ - if (ISCONST(l)) \ - return 0; \ + if (ISONE(l)) \ + return rec(r); \ break; \ case bddop_less: /* l < r = r - l */ \ { \ From d62d8482087d8422139483353d65482886a167b9 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 20 Jun 2017 16:09:56 +0200 Subject: [PATCH 11/13] ltsmin: catch exceptions by reference * spot/ltsmin/ltsmin.cc, tests/ltsmin/modelcheck.cc: Here. --- spot/ltsmin/ltsmin.cc | 2 +- tests/ltsmin/modelcheck.cc | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/spot/ltsmin/ltsmin.cc b/spot/ltsmin/ltsmin.cc index b8e53610d..8dd65c309 100644 --- a/spot/ltsmin/ltsmin.cc +++ b/spot/ltsmin/ltsmin.cc @@ -1112,7 +1112,7 @@ namespace spot { convert_aps(to_observe, iface, dict, dead, *ps); } - catch (std::runtime_error) + catch (const std::runtime_error&) { delete ps; dict->unregister_all_my_variables(iface.get()); diff --git a/tests/ltsmin/modelcheck.cc b/tests/ltsmin/modelcheck.cc index 1b32d285e..7a5cc9f7e 100644 --- a/tests/ltsmin/modelcheck.cc +++ b/tests/ltsmin/modelcheck.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire de +// Copyright (C) 2011, 2012, 2013, 2014, 2015, 2016, 2017 Laboratoire de // Recherche et Developpement de l'Epita (LRDE) // // This file is part of Spot, a model checking library. @@ -282,7 +282,7 @@ checked_main(int argc, char **argv) { res = ec->check(); } - catch (std::bad_alloc) + catch (const std::bad_alloc&) { std::cerr << "Out of memory during emptiness check." << std::endl; @@ -326,7 +326,7 @@ checked_main(int argc, char **argv) { run = res->accepting_run(); } - catch (std::bad_alloc) + catch (const std::bad_alloc&) { std::cerr << "Out of memory while looking for counterexample." << std::endl; From af000edbf929800872a9de8a851139d33feab0d2 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 22 Jun 2017 06:58:01 +0200 Subject: [PATCH 12/13] Release Spot 2.3.5 * NEWS, configure.ac, doc/org/setup.org: Update version. --- NEWS | 7 +++++-- configure.ac | 2 +- doc/org/setup.org | 10 +++++----- 3 files changed, 11 insertions(+), 8 deletions(-) diff --git a/NEWS b/NEWS index 21d59a354..277178a3b 100644 --- a/NEWS +++ b/NEWS @@ -1,8 +1,8 @@ -New in spot 2.3.4.dev (not yet released) +New in spot 2.3.5 (2017-06-22) Bugs fixed: - - We have fixed new cases where translating multiple formula in a + - We have fixed new cases where translating multiple formulas in a single ltl2tgba run could produce automata different from those produced by individual runs. @@ -17,6 +17,9 @@ New in spot 2.3.4.dev (not yet released) a number of reachable states/edges/transitions, but %S was incorrectly counting all states even unreachable. + - Our verson of BuDDy had an incorrect optimization for the + biimp operator. + New in spot 2.3.4 (2017-05-11) Bugs fixed: diff --git a/configure.ac b/configure.ac index f4004c6c0..d94d434be 100644 --- a/configure.ac +++ b/configure.ac @@ -21,7 +21,7 @@ # along with this program. If not, see . AC_PREREQ([2.61]) -AC_INIT([spot], [2.3.4.dev], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.3.5], [spot@lrde.epita.fr]) AC_CONFIG_AUX_DIR([tools]) AC_CONFIG_MACRO_DIR([m4]) AM_INIT_AUTOMAKE([1.11 gnu tar-ustar color-tests parallel-tests]) diff --git a/doc/org/setup.org b/doc/org/setup.org index 9e28e96ca..d1b1c869d 100644 --- a/doc/org/setup.org +++ b/doc/org/setup.org @@ -1,8 +1,8 @@ #+OPTIONS: H:2 num:nil toc:t html-postamble:nil #+EMAIL: spot@lrde.epita.fr #+HTML_LINK_HOME: index.html -#+MACRO: SPOTVERSION 2.3.4 -#+MACRO: LASTRELEASE 2.3.4 -#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.3.4.tar.gz][=spot-2.3.4.tar.gz=]] -#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-3-4/NEWS][summary of the changes]] -#+MACRO: LASTDATE 2017-05-11 +#+MACRO: SPOTVERSION 2.3.5 +#+MACRO: LASTRELEASE 2.3.5 +#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.3.5.tar.gz][=spot-2.3.5.tar.gz=]] +#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-3-5/NEWS][summary of the changes]] +#+MACRO: LASTDATE 2017-06-22 From 6c3daf0cd4319d84891cfb586f9ec9168db2a70e Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 22 Jun 2017 07:03:15 +0200 Subject: [PATCH 13/13] bump version * NEWS, configure.ac: Bump version to 2.3.5.dev. --- NEWS | 4 ++++ configure.ac | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index 277178a3b..56b7760e7 100644 --- a/NEWS +++ b/NEWS @@ -1,3 +1,7 @@ +New in spot 2.3.5.dev (not yet released) + + Nothing yet. + New in spot 2.3.5 (2017-06-22) Bugs fixed: diff --git a/configure.ac b/configure.ac index d94d434be..b81b820d6 100644 --- a/configure.ac +++ b/configure.ac @@ -21,7 +21,7 @@ # along with this program. If not, see . AC_PREREQ([2.61]) -AC_INIT([spot], [2.3.5], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.3.5.dev], [spot@lrde.epita.fr]) AC_CONFIG_AUX_DIR([tools]) AC_CONFIG_MACRO_DIR([m4]) AM_INIT_AUTOMAKE([1.11 gnu tar-ustar color-tests parallel-tests])