diff --git a/NEWS b/NEWS index 44d9f0c6a..2bd28e0c7 100644 --- a/NEWS +++ b/NEWS @@ -14,6 +14,12 @@ New in spot 2.5.2.dev (not yet released) the command-line tools, as well as the various way to display automata using the Python bindings. + - When option "1" is passed to print_dot() to hide state names + and force the display of state numbers, the actual state names + is now moved to the "tooltip" field of the state. The SVG + files produced by "dot -Tsvg" will show those as popups. + This is also done for state labels of kripke structures. + - cleanup_parity() and cleanup_parity_here() are smarter and now remove from the acceptance condition the parity colors that are not used in the automaton. diff --git a/doc/org/tut51.org b/doc/org/tut51.org index 416b1c9c4..87a880cdf 100644 --- a/doc/org/tut51.org +++ b/doc/org/tut51.org @@ -469,13 +469,15 @@ counterexample: With a small variant of the above code, we could also display the counterexample on the state space, but only because our state space is -so small: displaying large state spaces is not sensible. Besides, highlighting -a run only works on =twa_graph= automata, so we need to convert the -Kripke structure to a =twa_graph=: this can be done with =make_twa_graph()=. But -now =k= is no longer a Kripke structure (also not generated -on-the-fly anymore), so the =print_dot()= function will display it as -a classical automaton with conditions on edges rather than state: -passing the option "~k~" to =print_dot()= will fix that. +so small: displaying large state spaces is not sensible. Besides, +highlighting a run only works on =twa_graph= automata, so we need to +convert the Kripke structure to a =twa_graph=: this can be done with +=make_twa_graph()=. But now =k= is no longer a Kripke structure (also +not generated on-the-fly anymore), so the =print_dot()= function will +display it as a classical automaton with conditions on edges rather +than state: passing the option "~k~" to =print_dot()= will fix that. +We also pass option "~A~" to hide the acceptance condition (which is +=t=, i.e., accepting every infinite run). #+NAME: demo-3-aux #+BEGIN_SRC C++ :exports none :noweb strip-export @@ -515,7 +517,7 @@ passing the option "~k~" to =print_dot()= will fix that. if (auto run = k->intersecting_run(af)) { run->highlight(5); // 5 is a color number. - spot::print_dot(std::cout, k, ".k"); + spot::print_dot(std::cout, k, ".kA"); } } #+END_SRC @@ -527,6 +529,58 @@ $txt #+RESULTS: [[file:kripke-3.svg]] +Note that labeling states with names (the first line) and the +valuation of all atomic propositions (the second line) will quickly +produce graphs with large nodes that are problematic to render. A +trick to reduce the clutter and the size of the graph is to pass +option "~1~" to =print_dot()=, changing the above call to +src_cpp[:exports code]{spot::print_dot(std::cout, k, ".kA1");}. This +will cause all states to be numbered instead, but if the automaton is +rendered as an SVG figure, the old label will still appear as a +tooltip when the mouse is over a state. Try that on the following +figure: + +#+NAME: demo-3b +#+BEGIN_SRC C++ :exports none :noweb strip-export :results verbatim + #include + #include + #include + #include + #include + <> + int main() + { + auto d = spot::make_bdd_dict(); + + // Parse the input formula. + spot::parsed_formula pf = spot::parse_infix_psl("GF(odd_x) -> GF(odd_y)"); + if (pf.format_errors(std::cerr)) + return 1; + + // Translate its negation. + spot::formula f = spot::formula::Not(pf.f); + spot::twa_graph_ptr af = spot::translator(d).run(f); + + // Convert demo_kripke into an explicit graph + spot::twa_graph_ptr k = + spot::make_twa_graph(std::make_shared(d), + spot::twa::prop_set::all(), true); + // Find a run of or demo_kripke that intersects af. + if (auto run = k->intersecting_run(af)) + { + run->highlight(5); // 5 is a color number. + spot::print_dot(std::cout, k, ".kA1"); + } + } +#+END_SRC + +#+BEGIN_SRC dot :file kripke-3b.svg :cmd circo :var txt=demo-3b :exports results +$txt +#+END_SRC + +#+RESULTS: +[[file:kripke-3b.svg]] + * Possible improvements The on-the-fly interface, especially as implemented here, involves a diff --git a/spot/twaalgos/dot.cc b/spot/twaalgos/dot.cc index 4e0f44e8c..3f63ecd80 100644 --- a/spot/twaalgos/dot.cc +++ b/spot/twaalgos/dot.cc @@ -112,7 +112,7 @@ namespace spot std::string opt_font_; std::string opt_node_color_; std::ostream& os_; - bool opt_want_state_names_ = true; + bool inline_state_names_ = true; unsigned max_states_ = -1U; // related to max_states_given_ bool opt_shared_univ_dest_ = true; @@ -189,7 +189,7 @@ namespace spot opt_numbered_edges_ = true; break; case '1': - opt_want_state_names_ = false; + inline_state_names_ = false; break; case 'a': opt_show_acc_ = true; @@ -576,19 +576,39 @@ namespace spot os_ << '}' << std::endl; } + bool print_state_name(std::ostream& os, unsigned s, + bool force_text = false) const + { + if (sn_ && s < sn_->size() && !(*sn_)[s].empty()) + { + if (force_text) + escape_str(os, (*sn_)[s]); + else + escape_for_output(os, (*sn_)[s]); + } + else if (sprod_) + { + os << (*sprod_)[s].first << ',' << (*sprod_)[s].second; + } + else + { + return false; + } + return true; + } + void process_state(unsigned s) { os_ << " " << s << " [" << label_pre_; - if (sn_ && s < sn_->size() && !(*sn_)[s].empty()) - escape_for_output(os_, (*sn_)[s]); - else if (sprod_) - os_ << (*sprod_)[s].first << ',' << (*sprod_)[s].second; - else + + if (!(inline_state_names_ && print_state_name(os_, s))) os_ << s; if (orig_ && s < orig_->size()) os_ << " (" << (*orig_)[s] << ')'; + bool include_state_labels = + opt_state_labels_ && (inline_state_names_ || opt_latex_); if (mark_states_ && !dcircles_) { acc_cond::mark_t acc = {}; @@ -603,13 +623,13 @@ namespace spot os_ << nl_; output_mark(acc); } - if (opt_state_labels_) + if (include_state_labels) format_state_label(os_ << nl_, s); os_ << label_post_; } else { - if (opt_state_labels_) + if (include_state_labels) format_state_label(os_ << nl_, s); os_ << label_post_; // Use state_acc_sets(), not state_is_accepting() because @@ -630,6 +650,21 @@ namespace spot << '"'; } } + if (!inline_state_names_ && (sn_ || sprod_ || opt_state_labels_) + && !opt_latex_) + { + std::ostringstream os; + bool nonempty = print_state_name(os, s, true); + if (opt_state_labels_) + { + if (nonempty) + os << '\n'; + format_state_label(os, s); + nonempty = true; + } + if (nonempty) + os_ << ", tooltip=\"" << os.str() << '"'; + } os_ << "]\n"; if (incomplete_ && incomplete_->find(s) != incomplete_->end()) os_ << " u" << s << " [label=\"...\", shape=none, width=0, height=0" @@ -707,19 +742,18 @@ namespace spot void print(const const_twa_graph_ptr& aut) { aut_ = aut; - if (opt_want_state_names_) + + sn_ = aut->get_named_prop>("state-names"); + // We have no names. Do we have product sources? + if (!sn_) { - sn_ = aut->get_named_prop>("state-names"); - // We have no names. Do we have product sources? - if (!sn_) - { - sprod_ = aut->get_named_prop - >> - ("product-states"); - if (sprod_ && aut->num_states() != sprod_->size()) - sprod_ = nullptr; - } + sprod_ = aut->get_named_prop + >> + ("product-states"); + if (sprod_ && aut->num_states() != sprod_->size()) + sprod_ = nullptr; } + if (opt_orig_show_) orig_ = aut->get_named_prop>("original-states"); if (opt_state_labels_) @@ -758,8 +792,10 @@ namespace spot && (aut_->acc().is_buchi() || aut_->acc().is_co_buchi())); if (opt_shape_ == ShapeAuto) { - if (sn_ || sprod_ || aut->num_states() > 100 - || opt_state_labels_ || orig_) + if ((inline_state_names_ && (sn_ || sprod_ || opt_state_labels_)) + || (opt_state_labels_ && opt_latex_) + || aut->num_states() > 100 + || orig_) { opt_shape_ = ShapeEllipse; // If all state names are short, prefer circles. diff --git a/tests/core/readsave.test b/tests/core/readsave.test index 9a5c0c2d6..19a361aa7 100755 --- a/tests/core/readsave.test +++ b/tests/core/readsave.test @@ -529,10 +529,10 @@ digraph G { node [shape="circle"] I [label="", style=invis, width=0] 0 [label="0"] - 1 [label="1\n⓿❸"] + 1 [label="1\n⓿❸", tooltip="test me"] 2 [label="2\n⓿❷❸"] 3 [label="3\n❸"] - 4 [label="4\n❷❸"] + 4 [label="4\n❷❸", tooltip="hihi"] 5 [label="5\n❶❸"] 6 [label="6\n⓿"] 7 [label="7\n⓿❷"] diff --git a/tests/python/alternation.ipynb b/tests/python/alternation.ipynb index cc49de118..6f235d1c2 100644 --- a/tests/python/alternation.ipynb +++ b/tests/python/alternation.ipynb @@ -3,9 +3,7 @@ { "cell_type": "code", "execution_count": 1, - "metadata": { - "collapsed": true - }, + "metadata": {}, "outputs": [], "source": [ "import spot\n", @@ -22,140 +20,178 @@ { "cell_type": "code", "execution_count": 2, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", - "Fin(\n", - "\n", - ")\n", - "[co-Büchi]\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "-1\n", - "\n", + "\n", + "-1\n", + "\n", "\n", "\n", - "0->-1\n", - "\n", - "\n", - "1\n", + "\n", + "0->-1\n", + "\n", + "\n", + "1\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", "\n", "\n", - "-1->1\n", - "\n", - "\n", + "\n", + "-1->1\n", + "\n", + "\n", "\n", "\n", - "3\n", - "\n", - "3\n", - "\n", + "\n", + "3\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "\n", "\n", "\n", - "-1->3\n", - "\n", - "\n", + "\n", + "-1->3\n", + "\n", + "\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "b\n", + "\n", + "1->1\n", + "\n", + "\n", + "b\n", "\n", "\n", - "-4\n", - "\n", + "\n", + "-4\n", + "\n", "\n", "\n", - "1->-4\n", - "\n", - "\n", - "!b\n", + "\n", + "1->-4\n", + "\n", + "\n", + "!b\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "1\n", + "\n", + "3->3\n", + "\n", + "\n", + "1\n", "\n", "\n", - "4\n", - "\n", - "4\n", + "\n", + "4\n", + "\n", + "\n", + "4\n", + "\n", + "\n", "\n", "\n", - "3->4\n", - "\n", - "\n", - "a\n", + "\n", + "3->4\n", + "\n", + "\n", + "a\n", "\n", "\n", - "-4->1\n", - "\n", - "\n", + "\n", + "-4->1\n", + "\n", + "\n", "\n", "\n", - "2\n", - "\n", - "2\n", - "\n", + "\n", + "2\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "\n", "\n", "\n", - "-4->2\n", - "\n", - "\n", + "\n", + "-4->2\n", + "\n", + "\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "!b\n", + "\n", + "2->2\n", + "\n", + "\n", + "!b\n", "\n", "\n", - "5\n", - "\n", - "5\n", + "\n", + "5\n", + "\n", + "\n", + "5\n", + "\n", + "\n", "\n", "\n", - "2->5\n", - "\n", - "\n", - "b\n", + "\n", + "2->5\n", + "\n", + "\n", + "b\n", "\n", "\n", - "5->5\n", - "\n", - "\n", - "1\n", + "\n", + "5->5\n", + "\n", + "\n", + "1\n", "\n", "\n", - "4->4\n", - "\n", - "\n", - "a\n", + "\n", + "4->4\n", + "\n", + "\n", + "a\n", "\n", "\n", "" @@ -203,9 +239,7 @@ { "cell_type": "code", "execution_count": 3, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -213,153 +247,172 @@ "\n", "\n", - "\n", "\n", "\n", - "\n", + "\n", "G\n", - "\n", - "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", - "[gen. Büchi 2]\n", + "\n", + "Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")\n", + "[gen. Büchi 2]\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "1\n", - "\n", - "1,3\n", + "\n", + "1\n", + "\n", + "1,3\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "1\n", + "\n", + "0->1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "b\n", + "\n", + "1->1\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", - "2\n", - "\n", - "1,4\n", + "\n", + "2\n", + "\n", + "1,4\n", "\n", "\n", - "1->2\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", "\n", "\n", - "3\n", - "\n", - "1,2,3\n", + "\n", + "3\n", + "\n", + "1,2,3\n", "\n", "\n", - "1->3\n", - "\n", - "\n", - "!b\n", + "\n", + "1->3\n", + "\n", + "\n", + "!b\n", "\n", "\n", "\n", - "4\n", - "\n", - "1,2,4\n", + "\n", + "4\n", + "\n", + "1,2,4\n", "\n", "\n", - "1->4\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", + "\n", + "1->4\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", "\n", "\n", - "2->4\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", + "\n", + "2->4\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", "\n", "\n", - "3->1\n", - "\n", - "\n", - "b\n", + "\n", + "3->1\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", - "3->2\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", + "\n", + "3->2\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "!b\n", + "\n", + "3->3\n", + "\n", + "\n", + "!b\n", "\n", "\n", - "3->4\n", - "\n", - "\n", - "a & !b\n", - "\n", + "\n", + "3->4\n", + "\n", + "\n", + "a & !b\n", + "\n", "\n", "\n", - "4->2\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", + "\n", + "4->2\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", "\n", "\n", - "4->4\n", - "\n", - "\n", - "a & !b\n", - "\n", + "\n", + "4->4\n", + "\n", + "\n", + "a & !b\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f79685fc7e0> >" + " *' at 0x7f74000699f0> >" ] }, "execution_count": 3, @@ -374,9 +427,7 @@ { "cell_type": "code", "execution_count": 4, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -384,135 +435,154 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "1\n", - "\n", - "1,3\n", + "\n", + "1\n", + "\n", + "1,3\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "1\n", + "\n", + "0->1\n", + "\n", + "\n", + "1\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "b\n", + "\n", + "1->1\n", + "\n", + "\n", + "b\n", "\n", "\n", - "2\n", - "\n", - "1,4\n", + "\n", + "2\n", + "\n", + "1,4\n", "\n", "\n", - "1->2\n", - "\n", - "\n", - "a & b\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & b\n", "\n", "\n", - "3\n", - "\n", - "1,2,3\n", + "\n", + "3\n", + "\n", + "1,2,3\n", "\n", "\n", - "1->3\n", - "\n", - "\n", - "!b\n", + "\n", + "1->3\n", + "\n", + "\n", + "!b\n", "\n", "\n", - "4\n", - "\n", - "1,2,4\n", + "\n", + "4\n", + "\n", + "1,2,4\n", "\n", "\n", - "1->4\n", - "\n", - "\n", - "a & !b\n", + "\n", + "1->4\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "a & b\n", - "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & b\n", + "\n", "\n", "\n", - "2->4\n", - "\n", - "\n", - "a & !b\n", - "\n", + "\n", + "2->4\n", + "\n", + "\n", + "a & !b\n", + "\n", "\n", "\n", - "3->1\n", - "\n", - "\n", - "b\n", + "\n", + "3->1\n", + "\n", + "\n", + "b\n", "\n", "\n", - "3->2\n", - "\n", - "\n", - "a & b\n", + "\n", + "3->2\n", + "\n", + "\n", + "a & b\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "!b\n", + "\n", + "3->3\n", + "\n", + "\n", + "!b\n", "\n", "\n", - "3->4\n", - "\n", - "\n", - "a & !b\n", + "\n", + "3->4\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", - "4->2\n", - "\n", - "\n", - "a & b\n", - "\n", + "\n", + "4->2\n", + "\n", + "\n", + "a & b\n", + "\n", "\n", "\n", - "4->4\n", - "\n", - "\n", - "a & !b\n", + "\n", + "4->4\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f79685fc1e0> >" + " *' at 0x7f74001bff30> >" ] }, "execution_count": 4, @@ -527,99 +597,117 @@ { "cell_type": "code", "execution_count": 5, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", - "Fin(\n", - "\n", - ")\n", - "[co-Büchi]\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", "\n", + "\n", + "\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "1\n", - "\n", - "1\n", - "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "\n", + "2\n", + "\n", + "2\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "!a\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "!a & b & p\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a & b & p\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "!b & p\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & p\n", "\n", "\n", - "1->2\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "1->2\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", - "-1\n", - "\n", + "\n", + "-1\n", + "\n", "\n", "\n", - "1->-1\n", - "\n", - "\n", - "a & b & p\n", + "\n", + "1->-1\n", + "\n", + "\n", + "a & b & p\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "1\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", "\n", "\n", - "-1->0\n", - "\n", - "\n", + "\n", + "-1->0\n", + "\n", + "\n", "\n", "\n", - "-1->1\n", - "\n", - "\n", + "\n", + "-1->1\n", + "\n", + "\n", "\n", "\n", "" @@ -660,9 +748,7 @@ { "cell_type": "code", "execution_count": 6, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -670,119 +756,135 @@ "\n", "\n", - "\n", "\n", "\n", - "\n", + " viewBox=\"0.00 0.00 563.89 194.87\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", + "\n", "G\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", "\n", - "0\n", - "\n", - "~0\n", + "\n", + "0\n", + "\n", + "~0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "1\n", - "\n", - "~1\n", + "\n", + "1\n", + "\n", + "~1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", "\n", "\n", - "2\n", - "\n", - "{}\n", + "\n", + "2\n", + "\n", + "{}\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "!a\n", - "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a\n", + "\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "!a & b & p\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a & b & p\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "!b & p\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & p\n", "\n", "\n", - "1->2\n", - "\n", - "\n", - "!a & !b\n", - "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!a & !b\n", + "\n", "\n", "\n", - "3\n", - "\n", - "~1,~0\n", + "\n", + "3\n", + "\n", + "~1,~0\n", "\n", "\n", - "1->3\n", - "\n", - "\n", - "a & b & p\n", + "\n", + "1->3\n", + "\n", + "\n", + "a & b & p\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", - "3->0\n", - "\n", - "\n", - "!a & b & p\n", + "\n", + "3->0\n", + "\n", + "\n", + "!a & b & p\n", "\n", "\n", - "3->1\n", - "\n", - "\n", - "a & !b & p\n", + "\n", + "3->1\n", + "\n", + "\n", + "a & !b & p\n", "\n", "\n", - "3->2\n", - "\n", - "\n", - "!a & !b\n", - "\n", + "\n", + "3->2\n", + "\n", + "\n", + "!a & !b\n", + "\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "a & b & p\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & b & p\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f79685fc630> >" + " *' at 0x7f7400069900> >" ] }, "execution_count": 6, @@ -797,135 +899,160 @@ { "cell_type": "code", "execution_count": 7, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", - "Fin(\n", - "\n", - ")\n", - "[co-Büchi]\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", "\n", "\n", - "3\n", - "\n", - "3\n", + "\n", + "3\n", + "\n", + "3\n", "\n", "\n", - "I->3\n", - "\n", - "\n", + "\n", + "I->3\n", + "\n", + "\n", "\n", "\n", - "-4\n", - "\n", + "\n", + "-4\n", + "\n", "\n", "\n", - "3->-4\n", - "\n", - "\n", - "a\n", + "\n", + "3->-4\n", + "\n", + "\n", + "a\n", "\n", "\n", - "0\n", - "\n", - "0\n", - "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "\n", "\n", "\n", - "1\n", - "\n", - "1\n", - "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "\n", + "2\n", + "\n", + "2\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "!a\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "!a & b & p\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a & b & p\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "!b & p\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & p\n", "\n", "\n", - "1->2\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "1->2\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", - "-1\n", - "\n", + "\n", + "-1\n", + "\n", "\n", "\n", - "1->-1\n", - "\n", - "\n", - "a & b & p\n", + "\n", + "1->-1\n", + "\n", + "\n", + "a & b & p\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "1\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", "\n", "\n", - "-1->0\n", - "\n", - "\n", + "\n", + "-1->0\n", + "\n", + "\n", "\n", "\n", - "-1->1\n", - "\n", - "\n", + "\n", + "-1->1\n", + "\n", + "\n", "\n", "\n", - "-4->0\n", - "\n", - "\n", + "\n", + "-4->0\n", + "\n", + "\n", "\n", "\n", - "4\n", - "\n", - "4\n", + "\n", + "4\n", + "\n", + "4\n", "\n", "\n", - "-4->4\n", - "\n", - "\n", + "\n", + "-4->4\n", + "\n", + "\n", "\n", "\n", - "4->3\n", - "\n", - "\n", - "1\n", + "\n", + "4->3\n", + "\n", + "\n", + "1\n", "\n", "\n", "" @@ -969,9 +1096,7 @@ { "cell_type": "code", "execution_count": 8, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -979,164 +1104,188 @@ "\n", "\n", - "\n", "\n", "\n", - "\n", + " viewBox=\"0.00 0.00 734.00 175.72\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", + "\n", "G\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", "\n", - "0\n", - "\n", - "3\n", + "\n", + "0\n", + "\n", + "3\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "1\n", - "\n", - "~0,4\n", + "\n", + "1\n", + "\n", + "~0,4\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a\n", - "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "!a\n", - "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a\n", + "\n", "\n", "\n", - "2\n", - "\n", - "3,~1\n", + "\n", + "2\n", + "\n", + "3,~1\n", "\n", "\n", - "1->2\n", - "\n", - "\n", - "a\n", + "\n", + "1->2\n", + "\n", + "\n", + "a\n", "\n", "\n", - "3\n", - "\n", - "4,~1,~0\n", + "\n", + "3\n", + "\n", + "4,~1,~0\n", "\n", "\n", - "2->3\n", - "\n", - "\n", - "a & b & p\n", + "\n", + "2->3\n", + "\n", + "\n", + "a & b & p\n", "\n", "\n", - "4\n", - "\n", - "0,4,~1\n", + "\n", + "4\n", + "\n", + "0,4,~1\n", "\n", "\n", - "2->4\n", - "\n", - "\n", - "a & !b & p\n", + "\n", + "2->4\n", + "\n", + "\n", + "a & !b & p\n", "\n", "\n", - "3->0\n", - "\n", - "\n", - "!a & !b\n", - "\n", + "\n", + "3->0\n", + "\n", + "\n", + "!a & !b\n", + "\n", "\n", "\n", - "3->2\n", - "\n", - "\n", - "a & !b & p\n", + "\n", + "3->2\n", + "\n", + "\n", + "a & !b & p\n", "\n", "\n", - "5\n", - "\n", - "3,~0\n", + "\n", + "5\n", + "\n", + "3,~0\n", "\n", "\n", - "3->5\n", - "\n", - "\n", - "!a & b & p\n", + "\n", + "3->5\n", + "\n", + "\n", + "!a & b & p\n", "\n", "\n", - "6\n", - "\n", - "3,~1,~0\n", + "\n", + "6\n", + "\n", + "3,~1,~0\n", "\n", "\n", - "3->6\n", - "\n", - "\n", - "a & b & p\n", + "\n", + "3->6\n", + "\n", + "\n", + "a & b & p\n", "\n", "\n", - "4->0\n", - "\n", - "\n", - "!a & !b\n", - "\n", + "\n", + "4->0\n", + "\n", + "\n", + "!a & !b\n", + "\n", "\n", "\n", - "4->2\n", - "\n", - "\n", - "a & !b & p\n", + "\n", + "4->2\n", + "\n", + "\n", + "a & !b & p\n", "\n", "\n", - "4->5\n", - "\n", - "\n", - "!a & b & p\n", + "\n", + "4->5\n", + "\n", + "\n", + "!a & b & p\n", "\n", "\n", - "4->6\n", - "\n", - "\n", - "a & b & p\n", + "\n", + "4->6\n", + "\n", + "\n", + "a & b & p\n", "\n", "\n", - "5->4\n", - "\n", - "\n", - "a\n", + "\n", + "5->4\n", + "\n", + "\n", + "a\n", "\n", "\n", - "6->3\n", - "\n", - "\n", - "a & b & p\n", + "\n", + "6->3\n", + "\n", + "\n", + "a & b & p\n", "\n", "\n", - "6->4\n", - "\n", - "\n", - "a & !b & p\n", + "\n", + "6->4\n", + "\n", + "\n", + "a & !b & p\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f79685fc6f0> >" + " *' at 0x7f7400079150> >" ] }, "execution_count": 8, @@ -1151,173 +1300,205 @@ { "cell_type": "code", "execution_count": 9, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", - "Fin(\n", - "\n", - ")\n", - "[co-Büchi]\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", "\n", "\n", - "-7\n", - "\n", + "\n", + "-7\n", + "\n", "\n", "\n", - "I->-7\n", - "\n", - "\n", + "\n", + "I->-7\n", + "\n", + "\n", "\n", "\n", - "0\n", - "\n", - "0\n", - "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "\n", "\n", "\n", - "-7->0\n", - "\n", - "\n", + "\n", + "-7->0\n", + "\n", + "\n", "\n", "\n", - "3\n", - "\n", - "3\n", + "\n", + "3\n", + "\n", + "3\n", "\n", "\n", - "-7->3\n", - "\n", - "\n", + "\n", + "-7->3\n", + "\n", + "\n", "\n", "\n", - "1\n", - "\n", - "1\n", - "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "\n", + "2\n", + "\n", + "2\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "!a\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "a\n", + "\n", + "3->3\n", + "\n", + "\n", + "a\n", "\n", "\n", - "-4\n", - "\n", + "\n", + "-4\n", + "\n", "\n", "\n", - "3->-4\n", - "\n", - "\n", - "!a\n", + "\n", + "3->-4\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "!a & b & p\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a & b & p\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "!b & p\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & p\n", "\n", "\n", - "1->2\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "1->2\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", - "-1\n", - "\n", + "\n", + "-1\n", + "\n", "\n", "\n", - "1->-1\n", - "\n", - "\n", - "a & b & p\n", + "\n", + "1->-1\n", + "\n", + "\n", + "a & b & p\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "1\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", "\n", "\n", - "-1->0\n", - "\n", - "\n", + "\n", + "-1->0\n", + "\n", + "\n", "\n", "\n", - "-1->1\n", - "\n", - "\n", + "\n", + "-1->1\n", + "\n", + "\n", "\n", "\n", - "-4->3\n", - "\n", - "\n", + "\n", + "-4->3\n", + "\n", + "\n", "\n", "\n", - "4\n", - "\n", - "4\n", - "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", "\n", "\n", - "-4->4\n", - "\n", - "\n", + "\n", + "-4->4\n", + "\n", + "\n", "\n", "\n", - "4->4\n", - "\n", - "\n", - "!a\n", + "\n", + "4->4\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "5\n", - "\n", - "5\n", + "\n", + "5\n", + "\n", + "5\n", "\n", "\n", - "4->5\n", - "\n", - "\n", - "a\n", + "\n", + "4->5\n", + "\n", + "\n", + "a\n", "\n", "\n", - "5->5\n", - "\n", - "\n", - "1\n", + "\n", + "5->5\n", + "\n", + "\n", + "1\n", "\n", "\n", "" @@ -1365,9 +1546,7 @@ { "cell_type": "code", "execution_count": 10, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -1375,224 +1554,254 @@ "\n", "\n", - "\n", "\n", "\n", - "\n", + " viewBox=\"0.00 0.00 734.00 336.31\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", + "\n", "G\n", - "\n", - "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", - "[gen. Büchi 2]\n", + "\n", + "Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")\n", + "[gen. Büchi 2]\n", "\n", "\n", - "0\n", - "\n", - "~0,3\n", + "\n", + "0\n", + "\n", + "~0,3\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "1\n", - "\n", - "3,~1\n", + "\n", + "1\n", + "\n", + "3,~1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "a\n", - "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\n", "\n", "\n", - "2\n", - "\n", - "3,4\n", + "\n", + "2\n", + "\n", + "3,4\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "a & !b & p\n", - "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !b & p\n", + "\n", "\n", "\n", - "1->2\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", "\n", "\n", - "4\n", - "\n", - "3,4,~1\n", + "\n", + "4\n", + "\n", + "3,4,~1\n", "\n", "\n", - "1->4\n", - "\n", - "\n", - "!a & !b & p\n", - "\n", + "\n", + "1->4\n", + "\n", + "\n", + "!a & !b & p\n", + "\n", "\n", "\n", - "5\n", - "\n", - "3,4,~0\n", + "\n", + "5\n", + "\n", + "3,4,~0\n", "\n", "\n", - "1->5\n", - "\n", - "\n", - "!a & b & p\n", - "\n", + "\n", + "1->5\n", + "\n", + "\n", + "!a & b & p\n", + "\n", "\n", "\n", - "6\n", - "\n", - "3,~1,~0\n", + "\n", + "6\n", + "\n", + "3,~1,~0\n", "\n", "\n", - "1->6\n", - "\n", - "\n", - "a & b & p\n", - "\n", + "\n", + "1->6\n", + "\n", + "\n", + "a & b & p\n", + "\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "!a\n", - "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!a\n", + "\n", "\n", "\n", - "3\n", - "\n", - "3\n", + "\n", + "3\n", + "\n", + "3\n", "\n", "\n", - "2->3\n", - "\n", - "\n", - "a\n", - "\n", - "\n", + "\n", + "2->3\n", + "\n", + "\n", + "a\n", + "\n", + "\n", "\n", "\n", - "4->1\n", - "\n", - "\n", - "a & !b & p\n", - "\n", + "\n", + "4->1\n", + "\n", + "\n", + "a & !b & p\n", + "\n", "\n", "\n", - "4->2\n", - "\n", - "\n", - "!a & !b\n", - "\n", + "\n", + "4->2\n", + "\n", + "\n", + "!a & !b\n", + "\n", "\n", "\n", - "4->4\n", - "\n", - "\n", - "!a & !b & p\n", + "\n", + "4->4\n", + "\n", + "\n", + "!a & !b & p\n", "\n", "\n", - "4->5\n", - "\n", - "\n", - "!a & b & p\n", + "\n", + "4->5\n", + "\n", + "\n", + "!a & b & p\n", "\n", "\n", - "4->6\n", - "\n", - "\n", - "a & b & p\n", - "\n", + "\n", + "4->6\n", + "\n", + "\n", + "a & b & p\n", + "\n", "\n", "\n", - "5->1\n", - "\n", - "\n", - "a\n", - "\n", + "\n", + "5->1\n", + "\n", + "\n", + "a\n", + "\n", "\n", "\n", - "5->2\n", - "\n", - "\n", - "!a\n", - "\n", + "\n", + "5->2\n", + "\n", + "\n", + "!a\n", + "\n", "\n", "\n", - "6->1\n", - "\n", - "\n", - "a & !b & p\n", - "\n", + "\n", + "6->1\n", + "\n", + "\n", + "a & !b & p\n", + "\n", "\n", "\n", - "6->2\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", + "\n", + "6->2\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", "\n", "\n", - "6->5\n", - "\n", - "\n", - "!a & b & p\n", - "\n", + "\n", + "6->5\n", + "\n", + "\n", + "!a & b & p\n", + "\n", "\n", "\n", - "6->6\n", - "\n", - "\n", - "a & b & p\n", - "\n", + "\n", + "6->6\n", + "\n", + "\n", + "a & b & p\n", + "\n", "\n", "\n", - "3->2\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", + "\n", + "3->2\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "a\n", - "\n", - "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a\n", + "\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f79685fc7b0> >" + " *' at 0x7f7400069c90> >" ] }, "execution_count": 10, @@ -1607,9 +1816,7 @@ { "cell_type": "code", "execution_count": 11, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -1617,83 +1824,94 @@ "\n", "\n", - "\n", "\n", "\n", - "\n", + "\n", "G\n", - "\n", - "Fin(\n", - "\n", - ")\n", - "[co-Büchi]\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", "\n", "\n", - "0\n", - "\n", - "GF(a)\n", + "\n", + "0\n", + "\n", + "GF(a)\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "-1\n", - "\n", + "\n", + "-1\n", + "\n", "\n", "\n", - "0->-1\n", - "\n", - "\n", - "1\n", + "\n", + "0->-1\n", + "\n", + "\n", + "1\n", "\n", "\n", - "-1->0\n", - "\n", - "\n", + "\n", + "-1->0\n", + "\n", + "\n", "\n", "\n", - "1\n", - "\n", - "F(a)\n", - "\n", + "\n", + "1\n", + "\n", + "F(a)\n", + "\n", "\n", "\n", - "-1->1\n", - "\n", - "\n", + "\n", + "-1->1\n", + "\n", + "\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "1\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", "\n", "\n", - "2\n", - "\n", - "t\n", + "\n", + "2\n", + "\n", + "t\n", "\n", "\n", - "1->2\n", - "\n", - "\n", - "a\n", + "\n", + "1->2\n", + "\n", + "\n", + "a\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "1\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f79685fcae0> >" + " *' at 0x7f740008b360> >" ] }, "execution_count": 11, @@ -1727,9 +1945,7 @@ { "cell_type": "code", "execution_count": 12, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -1737,59 +1953,65 @@ "\n", "\n", - "\n", "\n", "\n", "\n", "G\n", - "\n", - "Inf(\n", + "\n", + "Inf(\n", "\n", - ")\n", - "[Büchi]\n", + ")\n", + "[Büchi]\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "1\n", - "\n", - "0,1\n", + "\n", + "1\n", + "\n", + "0,1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "1\n", + "\n", + "0->1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "1\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "a\n", + "\n", + "1->1\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f79685fc840> >" + " *' at 0x7f7400150090> >" ] }, "execution_count": 12, @@ -1818,7 +2040,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.5.4" + "version": "3.6.5" } }, "nbformat": 4, diff --git a/tests/python/automata.ipynb b/tests/python/automata.ipynb index 745ae3752..6150b6c02 100644 --- a/tests/python/automata.ipynb +++ b/tests/python/automata.ipynb @@ -164,7 +164,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fde206230c0> >" + " *' at 0x7f76ec2fef30> >" ] }, "execution_count": 2, @@ -604,7 +604,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fde2053ec60> >" + " *' at 0x7f76ec222d80> >" ] }, "execution_count": 6, @@ -681,7 +681,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fde2053ed50> >" + " *' at 0x7f76ec222b40> >" ] }, "execution_count": 7, @@ -765,7 +765,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fde2053e870> >" + " *' at 0x7f76ec2229c0> >" ] }, "execution_count": 8, @@ -1287,7 +1287,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fde2055f840> >" + " *' at 0x7f76ec245780> >" ] }, "execution_count": 12, @@ -1402,7 +1402,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fde2055f4e0> >" + " *' at 0x7f76ec245060> >" ] }, "execution_count": 13, @@ -1534,7 +1534,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fde2055f9c0> >" + " *' at 0x7f76ec245900> >" ] }, "execution_count": 14, @@ -1647,7 +1647,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fde2055f870> >" + " *' at 0x7f76ec2459c0> >" ] }, "execution_count": 15, @@ -2193,7 +2193,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fde2055f990> >" + " *' at 0x7f76ec222960> >" ] }, "execution_count": 16, @@ -2405,7 +2405,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fde2055f090> >" + " *' at 0x7f76ec245b40> >" ] }, "metadata": {}, @@ -2556,7 +2556,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fde2053ea50> >" + " *' at 0x7f76ec232180> >" ] }, "metadata": {}, @@ -2729,7 +2729,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fde2055fc60> >" + " *' at 0x7f76ec245c90> >" ] }, "metadata": {}, @@ -2905,7 +2905,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fde2055fb70> >" + " *' at 0x7f76ec245bd0> >" ] }, "metadata": {}, @@ -3092,7 +3092,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fde2055ff00> >" + " *' at 0x7f76ec245e40> >" ] }, "execution_count": 21, @@ -3169,7 +3169,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fde2055ff90> >" + " *' at 0x7f76ec222e40> >" ] }, "execution_count": 22, @@ -3458,8 +3458,11 @@ "\n", "\n", "0\n", + "\n", "\n", "0\n", + "\n", + "\n", "\n", "\n", "\n", @@ -3478,8 +3481,11 @@ "\n", "\n", "1\n", + "\n", "\n", "1\n", + "\n", + "\n", "\n", "\n", "\n", @@ -3492,8 +3498,11 @@ "\n", "\n", "2\n", + "\n", "\n", "2\n", + "\n", + "\n", "\n", "\n", "\n", @@ -3506,8 +3515,11 @@ "\n", "\n", "3\n", + "\n", "\n", "3\n", + "\n", + "\n", "\n", "\n", "\n", @@ -3655,7 +3667,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fde2053eae0> >" + " *' at 0x7f76ec222870> >" ] }, "metadata": {}, @@ -3756,7 +3768,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fde2055f780> >" + " *' at 0x7f76ec2458d0> >" ] }, "execution_count": 25, @@ -3830,7 +3842,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fde2056bc30> >" + " *' at 0x7f76ec245de0> >" ] }, "execution_count": 26, @@ -3996,7 +4008,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fde2056b270> >" + " *' at 0x7f76ec251e10> >" ] }, "execution_count": 28, @@ -4083,7 +4095,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fde2053eae0> >" + " *' at 0x7f76ec222870> >" ] }, "metadata": {}, @@ -4152,7 +4164,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fde2053eae0> >" + " *' at 0x7f76ec222870> >" ] }, "metadata": {}, @@ -4243,7 +4255,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fde2053eae0> >" + " *' at 0x7f76ec222870> >" ] }, "execution_count": 30, @@ -4276,7 +4288,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.6.5rc1" + "version": "3.6.5" } }, "nbformat": 4, diff --git a/tests/python/product.ipynb b/tests/python/product.ipynb index b083245bd..f6ef83aa4 100644 --- a/tests/python/product.ipynb +++ b/tests/python/product.ipynb @@ -42,311 +42,352 @@ "
\n", "\n", "G\n", - "\n", - "Inf(\n", + "\n", + "Inf(\n", "\n", - ")\n", - "[Büchi]\n", + ")\n", + "[Büchi]\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "I->1\n", - "\n", - "\n", + "\n", + "I->1\n", + "\n", + "\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "1\n", + "\n", + "1->0\n", + "\n", + "\n", + "1\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "a & !b\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "\n", + "2\n", + "\n", + "2\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "b\n", + "\n", + "0->2\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "1\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", - "\n", + "\n", "\n", "G\n", - "\n", - "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", - "[gen. Büchi 2]\n", + "\n", + "Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")\n", + "[gen. Büchi 2]\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "!b & c\n", - "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & c\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", + "\n", + "0->0\n", + "\n", + "\n", + "b\n", + "\n", + "\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "!b & !c\n", + "\n", + "0->1\n", + "\n", + "\n", + "!b & !c\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "!b & c\n", - "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!b & c\n", + "\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "!b & !c\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & !c\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "b & !c\n", - "\n", + "\n", + "1->1\n", + "\n", + "\n", + "b & !c\n", + "\n", "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", - "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", - "[gen. Büchi 3]\n", + "\n", + "Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")\n", + "[gen. Büchi 3]\n", "\n", "\n", - "0\n", - "\n", - "1,0\n", + "\n", + "0\n", + "\n", + "1,0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "1\n", - "\n", - "0,0\n", + "\n", + "1\n", + "\n", + "0,0\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "!b & c\n", - "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!b & c\n", + "\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "b\n", - "\n", - "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b\n", + "\n", + "\n", "\n", "\n", - "2\n", - "\n", - "0,1\n", + "\n", + "2\n", + "\n", + "0,1\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "!b & !c\n", + "\n", + "0->2\n", + "\n", + "\n", + "!b & !c\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", "\n", "\n", - "1->2\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", "\n", "\n", - "3\n", - "\n", - "2,0\n", + "\n", + "3\n", + "\n", + "2,0\n", "\n", "\n", - "1->3\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", + "\n", + "1->3\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", "\n", "\n", - "2->1\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", + "\n", + "2->1\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", "\n", "\n", - "2->3\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", - "\n", + "\n", + "2->3\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", "\n", "\n", - "4\n", - "\n", - "2,1\n", + "\n", + "4\n", + "\n", + "2,1\n", "\n", "\n", - "2->4\n", - "\n", - "\n", - "b & !c\n", - "\n", - "\n", + "\n", + "2->4\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", + "\n", + "3->3\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", "\n", "\n", - "3->4\n", - "\n", - "\n", - "!b & !c\n", - "\n", + "\n", + "3->4\n", + "\n", + "\n", + "!b & !c\n", + "\n", "\n", "\n", - "4->3\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", + "\n", + "4->3\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", "\n", "\n", - "4->3\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", - "\n", + "\n", + "4->3\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", "\n", "\n", - "4->4\n", - "\n", - "\n", - "!b & !c\n", - "\n", + "\n", + "4->4\n", + "\n", + "\n", + "!b & !c\n", + "\n", "\n", "\n", - "4->4\n", - "\n", - "\n", - "b & !c\n", - "\n", - "\n", + "\n", + "4->4\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", "\n", "\n", "
" @@ -389,311 +430,352 @@ "
\n", "\n", "G\n", - "\n", - "Inf(\n", + "\n", + "Inf(\n", "\n", - ")\n", - "[Büchi]\n", + ")\n", + "[Büchi]\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "I->1\n", - "\n", - "\n", + "\n", + "I->1\n", + "\n", + "\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "1\n", + "\n", + "1->0\n", + "\n", + "\n", + "1\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "a & !b\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "\n", + "2\n", + "\n", + "2\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "b\n", + "\n", + "0->2\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "1\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", - "\n", + "\n", "\n", "G\n", - "\n", - "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", - "[gen. Büchi 2]\n", + "\n", + "Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")\n", + "[gen. Büchi 2]\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "!b & c\n", - "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & c\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", + "\n", + "0->0\n", + "\n", + "\n", + "b\n", + "\n", + "\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "!b & !c\n", + "\n", + "0->1\n", + "\n", + "\n", + "!b & !c\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "!b & c\n", - "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!b & c\n", + "\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "!b & !c\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & !c\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "b & !c\n", - "\n", + "\n", + "1->1\n", + "\n", + "\n", + "b & !c\n", + "\n", "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", - "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", - "[gen. Büchi 3]\n", + "\n", + "Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")\n", + "[gen. Büchi 3]\n", "\n", "\n", - "0\n", - "\n", - "1,0\n", + "\n", + "0\n", + "\n", + "1,0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "1\n", - "\n", - "0,0\n", + "\n", + "1\n", + "\n", + "0,0\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "!b & c\n", - "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!b & c\n", + "\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "b\n", - "\n", - "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b\n", + "\n", + "\n", "\n", "\n", - "2\n", - "\n", - "0,1\n", + "\n", + "2\n", + "\n", + "0,1\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "!b & !c\n", + "\n", + "0->2\n", + "\n", + "\n", + "!b & !c\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", "\n", "\n", - "1->2\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", "\n", "\n", - "3\n", - "\n", - "2,0\n", + "\n", + "3\n", + "\n", + "2,0\n", "\n", "\n", - "1->3\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", + "\n", + "1->3\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", "\n", "\n", - "2->1\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", + "\n", + "2->1\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", "\n", "\n", - "2->3\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", - "\n", + "\n", + "2->3\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", "\n", "\n", - "4\n", - "\n", - "2,1\n", + "\n", + "4\n", + "\n", + "2,1\n", "\n", "\n", - "2->4\n", - "\n", - "\n", - "b & !c\n", - "\n", - "\n", + "\n", + "2->4\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", + "\n", + "3->3\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", "\n", "\n", - "3->4\n", - "\n", - "\n", - "!b & !c\n", - "\n", + "\n", + "3->4\n", + "\n", + "\n", + "!b & !c\n", + "\n", "\n", "\n", - "4->3\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", + "\n", + "4->3\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", "\n", "\n", - "4->3\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", - "\n", + "\n", + "4->3\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", "\n", "\n", - "4->4\n", - "\n", - "\n", - "!b & !c\n", - "\n", + "\n", + "4->4\n", + "\n", + "\n", + "!b & !c\n", + "\n", "\n", "\n", - "4->4\n", - "\n", - "\n", - "b & !c\n", - "\n", - "\n", + "\n", + "4->4\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", "\n", "\n", "
" @@ -743,274 +825,315 @@ "
\n", "\n", "G\n", - "\n", - "Inf(\n", + "\n", + "Inf(\n", "\n", - ")\n", - "[Büchi]\n", + ")\n", + "[Büchi]\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "I->1\n", - "\n", - "\n", + "\n", + "I->1\n", + "\n", + "\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "1\n", + "\n", + "1->0\n", + "\n", + "\n", + "1\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "a & !b\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "\n", + "2\n", + "\n", + "2\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "b\n", + "\n", + "0->2\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "1\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", - "\n", + "\n", "\n", "G\n", - "\n", - "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", - "[gen. Büchi 2]\n", + "\n", + "Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")\n", + "[gen. Büchi 2]\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "!b & c\n", - "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & c\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", + "\n", + "0->0\n", + "\n", + "\n", + "b\n", + "\n", + "\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "!b & !c\n", + "\n", + "0->1\n", + "\n", + "\n", + "!b & !c\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "!b & c\n", - "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!b & c\n", + "\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "!b & !c\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & !c\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "b & !c\n", - "\n", + "\n", + "1->1\n", + "\n", + "\n", + "b & !c\n", + "\n", "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", - "t\n", - "[all]\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "!b & c\n", + "\n", + "0->1\n", + "\n", + "\n", + "!b & c\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "b\n", + "\n", + "0->1\n", + "\n", + "\n", + "b\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "\n", + "2\n", + "\n", + "2\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "!b & !c\n", + "\n", + "0->2\n", + "\n", + "\n", + "!b & !c\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "a & !b & c\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !b & c\n", "\n", "\n", - "1->2\n", - "\n", - "\n", - "a & !b & !c\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "3\n", - "\n", - "3\n", + "\n", + "3\n", + "\n", + "3\n", "\n", "\n", - "1->3\n", - "\n", - "\n", - "b\n", + "\n", + "1->3\n", + "\n", + "\n", + "b\n", "\n", "\n", - "2->1\n", - "\n", - "\n", - "a & !b & c\n", + "\n", + "2->1\n", + "\n", + "\n", + "a & !b & c\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "a & !b & !c\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", - "2->3\n", - "\n", - "\n", - "b & c\n", + "\n", + "2->3\n", + "\n", + "\n", + "b & c\n", "\n", "\n", - "4\n", - "\n", - "4\n", + "\n", + "4\n", + "\n", + "4\n", "\n", "\n", - "2->4\n", - "\n", - "\n", - "b & !c\n", + "\n", + "2->4\n", + "\n", + "\n", + "b & !c\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "!b & c\n", + "\n", + "3->3\n", + "\n", + "\n", + "!b & c\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "b\n", + "\n", + "3->3\n", + "\n", + "\n", + "b\n", "\n", "\n", - "3->4\n", - "\n", - "\n", - "!b & !c\n", + "\n", + "3->4\n", + "\n", + "\n", + "!b & !c\n", "\n", "\n", - "4->3\n", - "\n", - "\n", - "!b & c\n", + "\n", + "4->3\n", + "\n", + "\n", + "!b & c\n", "\n", "\n", - "4->3\n", - "\n", - "\n", - "b & c\n", + "\n", + "4->3\n", + "\n", + "\n", + "b & c\n", "\n", "\n", - "4->4\n", - "\n", - "\n", - "!b & !c\n", + "\n", + "4->4\n", + "\n", + "\n", + "!b & !c\n", "\n", "\n", - "4->4\n", - "\n", - "\n", - "b & !c\n", + "\n", + "4->4\n", + "\n", + "\n", + "b & !c\n", "\n", "\n", "
" @@ -1131,311 +1254,352 @@ "
\n", "\n", "G\n", - "\n", - "Inf(\n", + "\n", + "Inf(\n", "\n", - ")\n", - "[Büchi]\n", + ")\n", + "[Büchi]\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "I->1\n", - "\n", - "\n", + "\n", + "I->1\n", + "\n", + "\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "1\n", + "\n", + "1->0\n", + "\n", + "\n", + "1\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "a & !b\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "\n", + "2\n", + "\n", + "2\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "b\n", + "\n", + "0->2\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "1\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", - "\n", + "\n", "\n", "G\n", - "\n", - "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", - "[gen. Büchi 2]\n", + "\n", + "Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")\n", + "[gen. Büchi 2]\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "!b & c\n", - "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & c\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", + "\n", + "0->0\n", + "\n", + "\n", + "b\n", + "\n", + "\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "!b & !c\n", + "\n", + "0->1\n", + "\n", + "\n", + "!b & !c\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "!b & c\n", - "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!b & c\n", + "\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "!b & !c\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & !c\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "b & !c\n", - "\n", + "\n", + "1->1\n", + "\n", + "\n", + "b & !c\n", + "\n", "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", - "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", - "[gen. Büchi 3]\n", + "\n", + "Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")\n", + "[gen. Büchi 3]\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "!b & c\n", - "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!b & c\n", + "\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "b\n", - "\n", - "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b\n", + "\n", + "\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "\n", + "2\n", + "\n", + "2\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "!b & !c\n", + "\n", + "0->2\n", + "\n", + "\n", + "!b & !c\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", "\n", "\n", - "1->2\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", "\n", "\n", - "3\n", - "\n", - "3\n", + "\n", + "3\n", + "\n", + "3\n", "\n", "\n", - "1->3\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", + "\n", + "1->3\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", "\n", "\n", - "2->1\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", + "\n", + "2->1\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", "\n", "\n", - "2->3\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", - "\n", + "\n", + "2->3\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", "\n", "\n", - "4\n", - "\n", - "4\n", + "\n", + "4\n", + "\n", + "4\n", "\n", "\n", - "2->4\n", - "\n", - "\n", - "b & !c\n", - "\n", - "\n", + "\n", + "2->4\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", + "\n", + "3->3\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", "\n", "\n", - "3->4\n", - "\n", - "\n", - "!b & !c\n", - "\n", + "\n", + "3->4\n", + "\n", + "\n", + "!b & !c\n", + "\n", "\n", "\n", - "4->3\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", + "\n", + "4->3\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", "\n", "\n", - "4->3\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", - "\n", + "\n", + "4->3\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", "\n", "\n", - "4->4\n", - "\n", - "\n", - "!b & !c\n", - "\n", + "\n", + "4->4\n", + "\n", + "\n", + "!b & !c\n", + "\n", "\n", "\n", - "4->4\n", - "\n", - "\n", - "b & !c\n", - "\n", - "\n", + "\n", + "4->4\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", "\n", "\n", "
" @@ -1624,311 +1788,352 @@ "
\n", "\n", "G\n", - "\n", - "Inf(\n", + "\n", + "Inf(\n", "\n", - ")\n", - "[Büchi]\n", + ")\n", + "[Büchi]\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "I->1\n", - "\n", - "\n", + "\n", + "I->1\n", + "\n", + "\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "1\n", + "\n", + "1->0\n", + "\n", + "\n", + "1\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "a & !b\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "\n", + "2\n", + "\n", + "2\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "b\n", + "\n", + "0->2\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "1\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", - "\n", + "\n", "\n", "G\n", - "\n", - "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", - "[gen. Büchi 2]\n", + "\n", + "Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")\n", + "[gen. Büchi 2]\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "!b & c\n", - "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & c\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", + "\n", + "0->0\n", + "\n", + "\n", + "b\n", + "\n", + "\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "!b & !c\n", + "\n", + "0->1\n", + "\n", + "\n", + "!b & !c\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "!b & c\n", - "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!b & c\n", + "\n", "\n", "\n", - "1->0\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "!b & !c\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & !c\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "b & !c\n", - "\n", + "\n", + "1->1\n", + "\n", + "\n", + "b & !c\n", + "\n", "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", - "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", - "[gen. Büchi 3]\n", + "\n", + "Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")\n", + "[gen. Büchi 3]\n", "\n", "\n", - "0\n", - "\n", - "1,0\n", + "\n", + "0\n", + "\n", + "1,0\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "1\n", - "\n", - "0,0\n", + "\n", + "1\n", + "\n", + "0,0\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "!b & c\n", - "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!b & c\n", + "\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "b\n", - "\n", - "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b\n", + "\n", + "\n", "\n", "\n", - "2\n", - "\n", - "0,1\n", + "\n", + "2\n", + "\n", + "0,1\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "!b & !c\n", + "\n", + "0->2\n", + "\n", + "\n", + "!b & !c\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", "\n", "\n", - "1->2\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", "\n", "\n", - "3\n", - "\n", - "2,0\n", + "\n", + "3\n", + "\n", + "2,0\n", "\n", "\n", - "1->3\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", + "\n", + "1->3\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", "\n", "\n", - "2->1\n", - "\n", - "\n", - "a & !b & c\n", - "\n", - "\n", + "\n", + "2->1\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "a & !b & !c\n", - "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", "\n", "\n", - "2->3\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", - "\n", + "\n", + "2->3\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", "\n", "\n", - "4\n", - "\n", - "2,1\n", + "\n", + "4\n", + "\n", + "2,1\n", "\n", "\n", - "2->4\n", - "\n", - "\n", - "b & !c\n", - "\n", - "\n", + "\n", + "2->4\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", + "\n", + "3->3\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", "\n", "\n", - "3->4\n", - "\n", - "\n", - "!b & !c\n", - "\n", + "\n", + "3->4\n", + "\n", + "\n", + "!b & !c\n", + "\n", "\n", "\n", - "4->3\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", + "\n", + "4->3\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", "\n", "\n", - "4->3\n", - "\n", - "\n", - "b & c\n", - "\n", - "\n", - "\n", + "\n", + "4->3\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", "\n", "\n", - "4->4\n", - "\n", - "\n", - "!b & !c\n", - "\n", + "\n", + "4->4\n", + "\n", + "\n", + "!b & !c\n", + "\n", "\n", "\n", - "4->4\n", - "\n", - "\n", - "b & !c\n", - "\n", - "\n", + "\n", + "4->4\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", "\n", "\n", "
" @@ -2009,7 +2214,7 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "For development, it is useful to know that we can force the automaton printer to show the real state numbers (not the pairs) by passing option `1`, and that we can retrieve the associated pairs ourselves." + "For development, it is useful to know that we can force the automaton printer to show the real state numbers (not the pairs) by passing option `1`, and that we can retrieve the associated pairs ourselves. Note that the pairs also appear as tooltips when we mouse over the states." ] }, { @@ -2023,176 +2228,214 @@ "\n", "\n", "G\n", - "\n", - "Inf(\n", + "\n", + "Inf(\n", "\n", - ")&Inf(\n", + ")&Inf(\n", "\n", - ")&Inf(\n", + ")&Inf(\n", "\n", - ")\n", - "[gen. Büchi 3]\n", + ")\n", + "[gen. Büchi 3]\n", "\n", "\n", - "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", "\n", "\n", - "I->0\n", - "\n", - "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "!b & c\n", + "\n", + "0->1\n", + "\n", + "\n", + "!b & c\n", "\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "b\n", + "\n", + "0->1\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "\n", + "2\n", + "\n", + "\n", + "2\n", + "\n", + "\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "!b & !c\n", + "\n", + "0->2\n", + "\n", + "\n", + "!b & !c\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "a & !b & c\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !b & c\n", "\n", "\n", "\n", "\n", - "1->2\n", - "\n", - "\n", - "a & !b & !c\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", "\n", - "3\n", - "\n", - "3\n", + "\n", + "3\n", + "\n", + "\n", + "3\n", + "\n", + "\n", "\n", "\n", - "1->3\n", - "\n", - "\n", - "b\n", + "\n", + "1->3\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "\n", "\n", - "2->1\n", - "\n", - "\n", - "a & !b & c\n", + "\n", + "2->1\n", + "\n", + "\n", + "a & !b & c\n", "\n", "\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "a & !b & !c\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", "\n", - "2->3\n", - "\n", - "\n", - "b & c\n", + "\n", + "2->3\n", + "\n", + "\n", + "b & c\n", "\n", "\n", "\n", "\n", "\n", - "4\n", - "\n", - "4\n", + "\n", + "4\n", + "\n", + "\n", + "4\n", + "\n", + "\n", "\n", "\n", - "2->4\n", - "\n", - "\n", - "b & !c\n", + "\n", + "2->4\n", + "\n", + "\n", + "b & !c\n", "\n", "\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "!b & c\n", + "\n", + "3->3\n", + "\n", + "\n", + "!b & c\n", "\n", "\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "b\n", + "\n", + "3->3\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "\n", "\n", - "3->4\n", - "\n", - "\n", - "!b & !c\n", + "\n", + "3->4\n", + "\n", + "\n", + "!b & !c\n", "\n", "\n", "\n", - "4->3\n", - "\n", - "\n", - "!b & c\n", + "\n", + "4->3\n", + "\n", + "\n", + "!b & c\n", "\n", "\n", "\n", "\n", - "4->3\n", - "\n", - "\n", - "b & c\n", + "\n", + "4->3\n", + "\n", + "\n", + "b & c\n", "\n", "\n", "\n", "\n", "\n", - "4->4\n", - "\n", - "\n", - "!b & !c\n", + "\n", + "4->4\n", + "\n", + "\n", + "!b & !c\n", "\n", "\n", "\n", - "4->4\n", - "\n", - "\n", - "b & !c\n", + "\n", + "4->4\n", + "\n", + "\n", + "b & !c\n", "\n", "\n", "\n", @@ -2243,7 +2486,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "234 µs ± 14.8 µs per loop (mean ± std. dev. of 7 runs, 1000 loops each)\n" + "252 µs ± 4.96 µs per loop (mean ± std. dev. of 7 runs, 1000 loops each)\n" ] } ], @@ -2260,7 +2503,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "3.45 µs ± 160 ns per loop (mean ± std. dev. of 7 runs, 100000 loops each)\n" + "3.4 µs ± 210 ns per loop (mean ± std. dev. of 7 runs, 100000 loops each)\n" ] } ], @@ -2272,7 +2515,7 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "Depending on the machine where this notebook has been run, using the C++ version of the product can be 1 to 2 order of magnitude faster. This is due to all the type conversions (converting Python types to C++ types) that occurs everytime a function/method of Spot is called from Python. When calling high-level C++ functions (such as `spot.product()`) from Python, the overhead is negligible because most of the time is spent on the C++ side, actually executing the function. However when calling low-level functions (such as `new_edge()`, `new_state()`, `out()`) most of the time is spent converting the arguments from Python to C++ and the results from C++ to Python.\n", + "Depending on the machine where this notebook has been run, using the C++ version of the product can be 1 to 2 orders of magnitude faster. This is due to all the type conversions (converting Python types to C++ types) that occurs everytime a function/method of Spot is called from Python. When calling high-level C++ functions (such as `spot.product()`) from Python, the overhead is negligible because most of the time is spent on the C++ side, actually executing the function. However when calling low-level functions (such as `new_edge()`, `new_state()`, `out()`) most of the time is spent converting the arguments from Python to C++ and the results from C++ to Python.\n", "\n", "Despite that speed difference, Python can be useful to prototype an algorithm before implementing it in C++." ] @@ -2294,7 +2537,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.6.4+" + "version": "3.6.5" } }, "nbformat": 4,