diff --git a/NEWS b/NEWS index 23739d738..32a1b0f19 100644 --- a/NEWS +++ b/NEWS @@ -85,6 +85,11 @@ New in spot 2.10.6.dev (not yet released) - complement() used to always turn tautological acceptance conditions into Büchi. It now only does that if the automaton is modified. + - The zielonka_tree construction was optimized using the same + memoization trick that is used in ACD. Additionally it can now be + run with additional option to abort when the tree as an unwanted + shape, or to turn the tree into a DAG. + New in spot 2.10.6 (2022-05-18) Bugs fixed: diff --git a/spot/twaalgos/zlktree.cc b/spot/twaalgos/zlktree.cc index 2f87e6352..f31c46896 100644 --- a/spot/twaalgos/zlktree.cc +++ b/spot/twaalgos/zlktree.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2021 Laboratoire de Recherche et Developpement de +// Copyright (C) 2021, 2022 Laboratoire de Recherche et Developpement de // l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -109,7 +109,8 @@ namespace spot } } - zielonka_tree::zielonka_tree(const acc_cond& cond) + zielonka_tree::zielonka_tree(const acc_cond& cond, + zielonka_tree_options opt) { const acc_cond::acc_code& code = cond.get_acceptance(); auto all = cond.all_sets(); @@ -120,11 +121,47 @@ namespace spot nodes_[0].colors = all; nodes_[0].level = 0; + robin_hood::unordered_node_map nmap; + std::vector models; // This loop is a BFS over the increasing set of nodes. for (unsigned node = 0; node < nodes_.size(); ++node) { acc_cond::mark_t colors = nodes_[node].colors; + unsigned nextlvl = nodes_[node].level + 1; + + // Have we already seen this combination of colors previously? + // If yes, simply copy the children. + if (auto p = nmap.emplace(colors, node); !p.second) + { + unsigned fc = nodes_[p.first->second].first_child; + if (!fc) // this is a leaf + { + ++num_branches_; + continue; + } + if (!!(opt & zielonka_tree_options::MERGE_SUBTREES)) + { + nodes_[node].first_child = fc; + continue; + } + unsigned child = fc; + unsigned first = nodes_.size(); + nodes_[node].first_child = first; + do + { + auto& c = nodes_[child]; + child = c.next_sibling; + nodes_.push_back({node, static_cast(nodes_.size() + 1), + 0, nextlvl, c.colors}); + } + while (child != fc); + nodes_.back().next_sibling = first; + // We do not have to test the shape since this is the second time + // we see these colors; + continue; + } + bool is_accepting = code.accepting(colors); if (node == 0) is_even_ = is_accepting; @@ -145,15 +182,32 @@ namespace spot nodes_.reserve(first + num_children); for (auto& m: models) nodes_.push_back({node, static_cast(nodes_.size() + 1), - 0, nodes_[node].level + 1, m.model}); + 0, nextlvl, m.model}); nodes_.back().next_sibling = first; if (num_children > 1) { + bool abort = false; if (is_accepting) - has_rabin_shape_ = false; + { + has_rabin_shape_ = false; + if (!!(opt & zielonka_tree_options::ABORT_WRONG_SHAPE) + && !!(opt & zielonka_tree_options::CHECK_RABIN)) + abort = true; + } else - has_streett_shape_ = false; + { + has_streett_shape_ = false; + if (!!(opt & zielonka_tree_options::ABORT_WRONG_SHAPE) + && !!(opt & zielonka_tree_options::CHECK_STREETT)) + abort = true; + } + if (abort) + { + nodes_.clear(); + num_branches_ = 0; + return; + } } } @@ -523,14 +577,18 @@ namespace spot do { auto& c = nodes_[child]; + // We have to read anything we need from C + // before emplace_back, which may reallocate. + acc_cond::mark_t colors = c.colors; + unsigned minstate = c.minstate; + child = c.next_sibling; nodes_.emplace_back(c.edges, c.states); auto& n = nodes_.back(); n.parent = node; n.level = lvl + 1; n.scc = ref.scc; - n.colors = c.colors; - n.minstate = c.minstate; - child = c.next_sibling; + n.colors = colors; + n.minstate = minstate; } while (child != fc); chain_children(node, before, nodes_.size()); diff --git a/spot/twaalgos/zlktree.hh b/spot/twaalgos/zlktree.hh index 675224682..b8e47bc2a 100644 --- a/spot/twaalgos/zlktree.hh +++ b/spot/twaalgos/zlktree.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2021 Laboratoire de Recherche et Developpement de +// Copyright (C) 2021, 2022 Laboratoire de Recherche et Developpement de // l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -28,6 +28,68 @@ namespace spot { + /// \ingroup twa_acc_transform + /// \brief Options to alter the behavior of acd + enum class zielonka_tree_options + { + /// Build the ZlkTree, without checking its shape. + NONE = 0, + /// Check if the ZlkTree has Rabin shape. + /// This actually has no effect unless ABORT_WRONG_SHAPE is set, + /// because zielonka_tree always check the shape. + CHECK_RABIN = 1, + /// Check if the ZlkTree has Streett shape. + /// This actually has no effect unless ABORT_WRONG_SHAPE is set, + /// because zielonka_tree always check the shape. + CHECK_STREETT = 2, + /// Check if the ZlkTree has Parity shape + /// This actually has no effect unless ABORT_WRONG_SHAPE is set, + /// because zielonka_tree always check the shape. + CHECK_PARITY = CHECK_RABIN | CHECK_STREETT, + /// Abort the construction of the ZlkTree if it does not have the + /// shape that is tested. When that happens, num_branches() is set + /// to 0. + ABORT_WRONG_SHAPE = 4, + /// Fuse identical substree. This cannot be used with + /// zielonka_tree_transform(). However it saves memory if the + /// only use of the zielonka_tree to check the shape. + MERGE_SUBTREES = 8, + }; + +#ifndef SWIG + inline + bool operator!(zielonka_tree_options me) + { + return me == zielonka_tree_options::NONE; + } + + inline + zielonka_tree_options operator&(zielonka_tree_options left, + zielonka_tree_options right) + { + typedef std::underlying_type_t ut; + return static_cast(static_cast(left) + & static_cast(right)); + } + + inline + zielonka_tree_options operator|(zielonka_tree_options left, + zielonka_tree_options right) + { + typedef std::underlying_type_t ut; + return static_cast(static_cast(left) + | static_cast(right)); + } + + inline + zielonka_tree_options operator-(zielonka_tree_options left, + zielonka_tree_options right) + { + typedef std::underlying_type_t ut; + return static_cast(static_cast(left) + & ~static_cast(right)); + } +#endif /// \ingroup twa_acc_transform /// \brief Zielonka Tree implementation /// @@ -41,7 +103,8 @@ namespace spot { public: /// \brief Build a Zielonka tree from the acceptance condition. - zielonka_tree(const acc_cond& cond); + zielonka_tree(const acc_cond& cond, + zielonka_tree_options opt = zielonka_tree_options::NONE); /// \brief The number of branches in the Zielonka tree. /// diff --git a/tests/python/zlktree.ipynb b/tests/python/zlktree.ipynb index d46e2ce2c..ae44ad37d 100644 --- a/tests/python/zlktree.ipynb +++ b/tests/python/zlktree.ipynb @@ -216,7 +216,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "execution_count": 2, @@ -640,7 +640,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0c49328600> >" + " *' at 0x7f14701b7510> >" ] }, "execution_count": 10, @@ -1063,7 +1063,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0c493284b0> >" + " *' at 0x7f1470220960> >" ] }, "execution_count": 11, @@ -1256,7 +1256,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0c49328f30> >" + " *' at 0x7f14701b75d0> >" ] }, "execution_count": 13, @@ -1701,7 +1701,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0c49330420> >" + " *' at 0x7f1470142240> >" ] }, "execution_count": 14, @@ -2096,7 +2096,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -2427,7 +2427,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -2513,7 +2513,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -2624,7 +2624,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -2662,7 +2662,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -2700,7 +2700,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -2717,6 +2717,237 @@ " display(tcond)" ] }, + { + "cell_type": "markdown", + "id": "77db26c3", + "metadata": {}, + "source": [ + "## `zielonka_tree_options`\n", + "\n", + "The `zielonka_tree` class accepts a few options that can alter its behaviour.\n", + "\n", + "Options `CHECK_RABIN`, `CHECK_STREETT`, `CHECK_PARITY` can be combined with\n", + "`ABORT_WRONG_SHAPE` to abort the construction as soon as it is detected that the Zielonka tree has the wrong shape. When this happens, the number of branchs of the tree is set to 0.\n", + "\n", + "For instance we can check that the original acceptance condition does not behaves like a Parity condition." + ] + }, + { + "cell_type": "code", + "execution_count": 17, + "id": "4fa47daf", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "(4, (Fin(0) & Inf(1) & (Inf(2) | Fin(3))) | ((Inf(0) | Fin(1)) & Fin(2) & Inf(3)))\n", + "0\n" + ] + } + ], + "source": [ + "print(c)\n", + "z = spot.zielonka_tree(c, spot.zielonka_tree_options_ABORT_WRONG_SHAPE \n", + " | spot.zielonka_tree_options_CHECK_PARITY)\n", + "print(z.num_branches())" + ] + }, + { + "cell_type": "markdown", + "id": "4786f64c", + "metadata": {}, + "source": [ + "Option `MERGE_SUBTREE` will fuse identical nodes, turning the tree into a DAG. (Actually, because this tree is stored as a left-child right-sibling tree, only the children of identical nodes are merged.):" + ] + }, + { + "cell_type": "code", + "execution_count": 18, + "id": "bc826090", + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "zielonka_tree\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "{0,1,2,3}\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "{1,2,3}\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "{0,1,3}\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "{2,3}\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "{1,3}\n", + "\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "{1,3}\n", + "\n", + "\n", + "\n", + "2->5\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "{0,1}\n", + "\n", + "\n", + "\n", + "2->6\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "7\n", + "\n", + "{3}\n", + "<7>\n", + "\n", + "\n", + "\n", + "3->7\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "8\n", + "\n", + "{1}\n", + "<8>\n", + "\n", + "\n", + "\n", + "4->8\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "9\n", + "\n", + "{3}\n", + "<9>\n", + "\n", + "\n", + "\n", + "4->9\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "5->8\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "5->9\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "10\n", + "\n", + "{1}\n", + "<10>\n", + "\n", + "\n", + "\n", + "6->10\n", + "\n", + "\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " >" + ] + }, + "execution_count": 18, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "spot.zielonka_tree(c, spot.zielonka_tree_options_MERGE_SUBTREES)" + ] + }, + { + "cell_type": "markdown", + "id": "9d7688b3", + "metadata": {}, + "source": [ + "Such a DAG cannot be used by `zielonka_tree_transform()`, but it saves memory if we are only checking the shape of the tree/DAG." + ] + }, { "cell_type": "markdown", "id": "75838579", @@ -2731,7 +2962,7 @@ }, { "cell_type": "code", - "execution_count": 17, + "execution_count": 19, "id": "ea3488b1", "metadata": {}, "outputs": [], @@ -2763,7 +2994,7 @@ }, { "cell_type": "code", - "execution_count": 18, + "execution_count": 20, "id": "fad721c0", "metadata": {}, "outputs": [ @@ -3862,10 +4093,10 @@ "};$(\"#acdaut0 #E9\").addClass(\"acdN0\");$(\"#acdaut0 #E10\").addClass(\"acdN0\");$(\"#acdaut0 #E11\").addClass(\"acdN0\");$(\"#acdaut0 #E12\").addClass(\"acdN0\");$(\"#acdaut0 #E13\").addClass(\"acdN0\");$(\"#acdaut0 #E14\").addClass(\"acdN0\");$(\"#acdaut0 #E15\").addClass(\"acdN0\");$(\"#acdaut0 #E16\").addClass(\"acdN0\");$(\"#acdaut0 #E21\").addClass(\"acdN0\");$(\"#acdaut0 #E22\").addClass(\"acdN0\");$(\"#acdaut0 #E23\").addClass(\"acdN0\");$(\"#acdaut0 #E24\").addClass(\"acdN0\");$(\"#acdaut0 #E25\").addClass(\"acdN0\");$(\"#acdaut0 #E26\").addClass(\"acdN0\");$(\"#acdaut0 #E27\").addClass(\"acdN0\");$(\"#acdaut0 #E28\").addClass(\"acdN0\");$(\"#acdaut0 #E33\").addClass(\"acdN0\");$(\"#acdaut0 #E34\").addClass(\"acdN0\");$(\"#acdaut0 #E35\").addClass(\"acdN0\");$(\"#acdaut0 #E36\").addClass(\"acdN0\");$(\"#acdaut0 #E31\").addClass(\"acdN1\");$(\"#acdaut0 #E32\").addClass(\"acdN1\");$(\"#acdaut0 #E39\").addClass(\"acdN1\");$(\"#acdaut0 #E40\").addClass(\"acdN1\");$(\"#acdaut0 #E5\").addClass(\"acdN2\");$(\"#acdaut0 #E7\").addClass(\"acdN2\");$(\"#acdaut0 #E17\").addClass(\"acdN2\");$(\"#acdaut0 #E1\").addClass(\"acdN3\");$(\"#acdaut0 #E10\").addClass(\"acdN4\");$(\"#acdaut0 #E12\").addClass(\"acdN4\");$(\"#acdaut0 #E13\").addClass(\"acdN4\");$(\"#acdaut0 #E15\").addClass(\"acdN4\");$(\"#acdaut0 #E21\").addClass(\"acdN4\");$(\"#acdaut0 #E22\").addClass(\"acdN4\");$(\"#acdaut0 #E23\").addClass(\"acdN5\");$(\"#acdaut0 #E24\").addClass(\"acdN5\");$(\"#acdaut0 #E34\").addClass(\"acdN5\");$(\"#acdaut0 #E36\").addClass(\"acdN5\");$(\"#acdaut0 #E14\").addClass(\"acdN6\");$(\"#acdaut0 #E15\").addClass(\"acdN6\");$(\"#acdaut0 #E22\").addClass(\"acdN6\");$(\"#acdaut0 #E23\").addClass(\"acdN6\");$(\"#acdaut0 #E14\").addClass(\"acdN7\");$(\"#acdaut0 #E16\").addClass(\"acdN7\");$(\"#acdaut0 #E26\").addClass(\"acdN7\");$(\"#acdaut0 #E9\").addClass(\"acdN8\");$(\"#acdaut0 #E40\").addClass(\"acdN9\");$(\"#acdaut0 #E5\").addClass(\"acdN10\");$(\"#acdaut0 #E23\").addClass(\"acdN11\");$(\"#acdaut0 #E14\").addClass(\"acdN12\");$(\"#acdaut0 #E23\").addClass(\"acdN13\");$(\"#acdaut0 #E14\").addClass(\"acdN14\");$(\"#acdaut0 #E1\").click(function(){acd0_edge(1);});$(\"#acdaut0 #E2\").click(function(){acd0_edge(2);});$(\"#acdaut0 #E3\").click(function(){acd0_edge(3);});$(\"#acdaut0 #E4\").click(function(){acd0_edge(4);});$(\"#acdaut0 #E5\").click(function(){acd0_edge(5);});$(\"#acdaut0 #E6\").click(function(){acd0_edge(6);});$(\"#acdaut0 #E7\").click(function(){acd0_edge(7);});$(\"#acdaut0 #E8\").click(function(){acd0_edge(8);});$(\"#acdaut0 #E9\").click(function(){acd0_edge(9);});$(\"#acdaut0 #E10\").click(function(){acd0_edge(10);});$(\"#acdaut0 #E11\").click(function(){acd0_edge(11);});$(\"#acdaut0 #E12\").click(function(){acd0_edge(12);});$(\"#acdaut0 #E13\").click(function(){acd0_edge(13);});$(\"#acdaut0 #E14\").click(function(){acd0_edge(14);});$(\"#acdaut0 #E15\").click(function(){acd0_edge(15);});$(\"#acdaut0 #E16\").click(function(){acd0_edge(16);});$(\"#acdaut0 #E17\").click(function(){acd0_edge(17);});$(\"#acdaut0 #E18\").click(function(){acd0_edge(18);});$(\"#acdaut0 #E19\").click(function(){acd0_edge(19);});$(\"#acdaut0 #E20\").click(function(){acd0_edge(20);});$(\"#acdaut0 #E21\").click(function(){acd0_edge(21);});$(\"#acdaut0 #E22\").click(function(){acd0_edge(22);});$(\"#acdaut0 #E23\").click(function(){acd0_edge(23);});$(\"#acdaut0 #E24\").click(function(){acd0_edge(24);});$(\"#acdaut0 #E25\").click(function(){acd0_edge(25);});$(\"#acdaut0 #E26\").click(function(){acd0_edge(26);});$(\"#acdaut0 #E27\").click(function(){acd0_edge(27);});$(\"#acdaut0 #E28\").click(function(){acd0_edge(28);});$(\"#acdaut0 #E29\").click(function(){acd0_edge(29);});$(\"#acdaut0 #E30\").click(function(){acd0_edge(30);});$(\"#acdaut0 #E31\").click(function(){acd0_edge(31);});$(\"#acdaut0 #E32\").click(function(){acd0_edge(32);});$(\"#acdaut0 #E33\").click(function(){acd0_edge(33);});$(\"#acdaut0 #E34\").click(function(){acd0_edge(34);});$(\"#acdaut0 #E35\").click(function(){acd0_edge(35);});$(\"#acdaut0 #E36\").click(function(){acd0_edge(36);});$(\"#acdaut0 #E37\").click(function(){acd0_edge(37);});$(\"#acdaut0 #E38\").click(function(){acd0_edge(38);});$(\"#acdaut0 #E39\").click(function(){acd0_edge(39);});$(\"#acdaut0 #E40\").click(function(){acd0_edge(40);});$(\"#acdaut0 #S0\").click(function(){acd0_state(0);});$(\"#acdaut0 #S1\").click(function(){acd0_state(1);});$(\"#acdaut0 #S2\").click(function(){acd0_state(2);});$(\"#acdaut0 #S3\").click(function(){acd0_state(3);});$(\"#acdaut0 #S4\").click(function(){acd0_state(4);});$(\"#acdaut0 #S5\").click(function(){acd0_state(5);});$(\"#acdaut0 #S6\").click(function(){acd0_state(6);});$(\"#acdaut0 #S7\").click(function(){acd0_state(7);});$(\"#acdaut0 #S8\").click(function(){acd0_state(8);});$(\"#acdaut0 #S9\").click(function(){acd0_state(9);});$(\"#acd0 #N0\").click(function(){acd0_node(0, 0);});$(\"#acd0 #N1\").click(function(){acd0_node(1, 1);});$(\"#acd0 #N2\").click(function(){acd0_node(2, 1);});$(\"#acd0 #N3\").click(function(){acd0_node(3, 1);});$(\"#acd0 #N4\").click(function(){acd0_node(4, 1);});$(\"#acd0 #N5\").click(function(){acd0_node(5, 1);});$(\"#acd0 #N6\").click(function(){acd0_node(6, 1);});$(\"#acd0 #N7\").click(function(){acd0_node(7, 1);});$(\"#acd0 #N8\").click(function(){acd0_node(8, 1);});$(\"#acd0 #N9\").click(function(){acd0_node(9, 0);});$(\"#acd0 #N10\").click(function(){acd0_node(10, 0);});$(\"#acd0 #N11\").click(function(){acd0_node(11, 0);});$(\"#acd0 #N12\").click(function(){acd0_node(12, 0);});$(\"#acd0 #N13\").click(function(){acd0_node(13, 0);});$(\"#acd0 #N14\").click(function(){acd0_node(14, 0);});" ], "text/plain": [ - " >" + " >" ] }, - "execution_count": 18, + "execution_count": 20, "metadata": {}, "output_type": "execute_result" } @@ -3886,7 +4117,7 @@ }, { "cell_type": "code", - "execution_count": 19, + "execution_count": 21, "id": "859a993a", "metadata": {}, "outputs": [ @@ -3896,7 +4127,7 @@ "False" ] }, - "execution_count": 19, + "execution_count": 21, "metadata": {}, "output_type": "execute_result" } @@ -3932,7 +4163,7 @@ }, { "cell_type": "code", - "execution_count": 20, + "execution_count": 22, "id": "a8bd0844", "metadata": {}, "outputs": [ @@ -3942,7 +4173,7 @@ "(4, 1)" ] }, - "execution_count": 20, + "execution_count": 22, "metadata": {}, "output_type": "execute_result" } @@ -3953,7 +4184,7 @@ }, { "cell_type": "code", - "execution_count": 21, + "execution_count": 23, "id": "93116a05", "metadata": {}, "outputs": [ @@ -3963,7 +4194,7 @@ "(4, 1)" ] }, - "execution_count": 21, + "execution_count": 23, "metadata": {}, "output_type": "execute_result" } @@ -3984,7 +4215,7 @@ }, { "cell_type": "code", - "execution_count": 22, + "execution_count": 24, "id": "23940b6a", "metadata": {}, "outputs": [ @@ -3994,7 +4225,7 @@ "(12, 0)" ] }, - "execution_count": 22, + "execution_count": 24, "metadata": {}, "output_type": "execute_result" } @@ -4005,7 +4236,7 @@ }, { "cell_type": "code", - "execution_count": 23, + "execution_count": 25, "id": "de7cbd02", "metadata": {}, "outputs": [ @@ -4015,7 +4246,7 @@ "(8, 0)" ] }, - "execution_count": 23, + "execution_count": 25, "metadata": {}, "output_type": "execute_result" } @@ -4026,7 +4257,7 @@ }, { "cell_type": "code", - "execution_count": 24, + "execution_count": 26, "id": "8b0305d4", "metadata": {}, "outputs": [ @@ -4036,7 +4267,7 @@ "(4, 0)" ] }, - "execution_count": 24, + "execution_count": 26, "metadata": {}, "output_type": "execute_result" } @@ -4047,7 +4278,7 @@ }, { "cell_type": "code", - "execution_count": 25, + "execution_count": 27, "id": "4f0a10f5", "metadata": {}, "outputs": [ @@ -4057,7 +4288,7 @@ "(4, 1)" ] }, - "execution_count": 25, + "execution_count": 27, "metadata": {}, "output_type": "execute_result" } @@ -4094,7 +4325,7 @@ }, { "cell_type": "code", - "execution_count": 26, + "execution_count": 28, "id": "2bd04c1f", "metadata": {}, "outputs": [ @@ -4104,7 +4335,7 @@ "4" ] }, - "execution_count": 26, + "execution_count": 28, "metadata": {}, "output_type": "execute_result" } @@ -4131,7 +4362,7 @@ }, { "cell_type": "code", - "execution_count": 27, + "execution_count": 29, "id": "e28035e8", "metadata": {}, "outputs": [ @@ -4737,10 +4968,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f0c49328840> >" + " *' at 0x7f14701670f0> >" ] }, - "execution_count": 27, + "execution_count": 29, "metadata": {}, "output_type": "execute_result" } @@ -4761,7 +4992,7 @@ }, { "cell_type": "code", - "execution_count": 28, + "execution_count": 30, "id": "numerical-education", "metadata": {}, "outputs": [ @@ -4771,7 +5002,7 @@ "True" ] }, - "execution_count": 28, + "execution_count": 30, "metadata": {}, "output_type": "execute_result" } @@ -4790,7 +5021,7 @@ }, { "cell_type": "code", - "execution_count": 29, + "execution_count": 31, "id": "3e239a0c", "metadata": {}, "outputs": [ @@ -5376,10 +5607,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f0c49328e70> >" + " *' at 0x7f1470167210> >" ] }, - "execution_count": 29, + "execution_count": 31, "metadata": {}, "output_type": "execute_result" } @@ -5401,7 +5632,7 @@ }, { "cell_type": "code", - "execution_count": 30, + "execution_count": 32, "id": "4f62e612", "metadata": {}, "outputs": [ @@ -5411,7 +5642,7 @@ "15" ] }, - "execution_count": 30, + "execution_count": 32, "metadata": {}, "output_type": "execute_result" } @@ -5422,7 +5653,7 @@ }, { "cell_type": "code", - "execution_count": 31, + "execution_count": 33, "id": "20f2a45c", "metadata": {}, "outputs": [ @@ -5432,7 +5663,7 @@ "27" ] }, - "execution_count": 31, + "execution_count": 33, "metadata": {}, "output_type": "execute_result" } @@ -5461,7 +5692,7 @@ }, { "cell_type": "code", - "execution_count": 32, + "execution_count": 34, "id": "7727735d", "metadata": {}, "outputs": [], @@ -5471,7 +5702,7 @@ }, { "cell_type": "code", - "execution_count": 33, + "execution_count": 35, "id": "2d0bbc0b", "metadata": {}, "outputs": [ @@ -5505,7 +5736,7 @@ }, { "cell_type": "code", - "execution_count": 34, + "execution_count": 36, "id": "78643aae", "metadata": {}, "outputs": [ @@ -5523,7 +5754,7 @@ }, { "cell_type": "code", - "execution_count": 35, + "execution_count": 37, "id": "13a7796b", "metadata": {}, "outputs": [], @@ -5533,7 +5764,7 @@ }, { "cell_type": "code", - "execution_count": 36, + "execution_count": 38, "id": "3ee900b7", "metadata": {}, "outputs": [ @@ -5564,7 +5795,7 @@ }, { "cell_type": "code", - "execution_count": 37, + "execution_count": 39, "id": "e12bb020", "metadata": {}, "outputs": [], @@ -5574,7 +5805,7 @@ }, { "cell_type": "code", - "execution_count": 38, + "execution_count": 40, "id": "813d15ed", "metadata": {}, "outputs": [ @@ -6673,10 +6904,10 @@ "};$(\"#acdaut1 #E9\").addClass(\"acdN0\");$(\"#acdaut1 #E10\").addClass(\"acdN0\");$(\"#acdaut1 #E11\").addClass(\"acdN0\");$(\"#acdaut1 #E12\").addClass(\"acdN0\");$(\"#acdaut1 #E13\").addClass(\"acdN0\");$(\"#acdaut1 #E14\").addClass(\"acdN0\");$(\"#acdaut1 #E15\").addClass(\"acdN0\");$(\"#acdaut1 #E16\").addClass(\"acdN0\");$(\"#acdaut1 #E21\").addClass(\"acdN0\");$(\"#acdaut1 #E22\").addClass(\"acdN0\");$(\"#acdaut1 #E23\").addClass(\"acdN0\");$(\"#acdaut1 #E24\").addClass(\"acdN0\");$(\"#acdaut1 #E25\").addClass(\"acdN0\");$(\"#acdaut1 #E26\").addClass(\"acdN0\");$(\"#acdaut1 #E27\").addClass(\"acdN0\");$(\"#acdaut1 #E28\").addClass(\"acdN0\");$(\"#acdaut1 #E33\").addClass(\"acdN0\");$(\"#acdaut1 #E34\").addClass(\"acdN0\");$(\"#acdaut1 #E35\").addClass(\"acdN0\");$(\"#acdaut1 #E36\").addClass(\"acdN0\");$(\"#acdaut1 #E31\").addClass(\"acdN1\");$(\"#acdaut1 #E32\").addClass(\"acdN1\");$(\"#acdaut1 #E39\").addClass(\"acdN1\");$(\"#acdaut1 #E40\").addClass(\"acdN1\");$(\"#acdaut1 #E5\").addClass(\"acdN2\");$(\"#acdaut1 #E7\").addClass(\"acdN2\");$(\"#acdaut1 #E17\").addClass(\"acdN2\");$(\"#acdaut1 #E1\").addClass(\"acdN3\");$(\"#acdaut1 #E10\").addClass(\"acdN4\");$(\"#acdaut1 #E12\").addClass(\"acdN4\");$(\"#acdaut1 #E13\").addClass(\"acdN4\");$(\"#acdaut1 #E15\").addClass(\"acdN4\");$(\"#acdaut1 #E21\").addClass(\"acdN4\");$(\"#acdaut1 #E22\").addClass(\"acdN4\");$(\"#acdaut1 #E14\").addClass(\"acdN5\");$(\"#acdaut1 #E15\").addClass(\"acdN5\");$(\"#acdaut1 #E22\").addClass(\"acdN5\");$(\"#acdaut1 #E23\").addClass(\"acdN5\");$(\"#acdaut1 #E23\").addClass(\"acdN6\");$(\"#acdaut1 #E24\").addClass(\"acdN6\");$(\"#acdaut1 #E34\").addClass(\"acdN6\");$(\"#acdaut1 #E36\").addClass(\"acdN6\");$(\"#acdaut1 #E14\").addClass(\"acdN7\");$(\"#acdaut1 #E16\").addClass(\"acdN7\");$(\"#acdaut1 #E26\").addClass(\"acdN7\");$(\"#acdaut1 #E9\").addClass(\"acdN8\");$(\"#acdaut1 #E40\").addClass(\"acdN9\");$(\"#acdaut1 #E5\").addClass(\"acdN10\");$(\"#acdaut1 #E14\").addClass(\"acdN11\");$(\"#acdaut1 #E23\").addClass(\"acdN12\");$(\"#acdaut1 #E23\").addClass(\"acdN13\");$(\"#acdaut1 #E14\").addClass(\"acdN14\");$(\"#acdaut1 #E1\").click(function(){acd1_edge(1);});$(\"#acdaut1 #E2\").click(function(){acd1_edge(2);});$(\"#acdaut1 #E3\").click(function(){acd1_edge(3);});$(\"#acdaut1 #E4\").click(function(){acd1_edge(4);});$(\"#acdaut1 #E5\").click(function(){acd1_edge(5);});$(\"#acdaut1 #E6\").click(function(){acd1_edge(6);});$(\"#acdaut1 #E7\").click(function(){acd1_edge(7);});$(\"#acdaut1 #E8\").click(function(){acd1_edge(8);});$(\"#acdaut1 #E9\").click(function(){acd1_edge(9);});$(\"#acdaut1 #E10\").click(function(){acd1_edge(10);});$(\"#acdaut1 #E11\").click(function(){acd1_edge(11);});$(\"#acdaut1 #E12\").click(function(){acd1_edge(12);});$(\"#acdaut1 #E13\").click(function(){acd1_edge(13);});$(\"#acdaut1 #E14\").click(function(){acd1_edge(14);});$(\"#acdaut1 #E15\").click(function(){acd1_edge(15);});$(\"#acdaut1 #E16\").click(function(){acd1_edge(16);});$(\"#acdaut1 #E17\").click(function(){acd1_edge(17);});$(\"#acdaut1 #E18\").click(function(){acd1_edge(18);});$(\"#acdaut1 #E19\").click(function(){acd1_edge(19);});$(\"#acdaut1 #E20\").click(function(){acd1_edge(20);});$(\"#acdaut1 #E21\").click(function(){acd1_edge(21);});$(\"#acdaut1 #E22\").click(function(){acd1_edge(22);});$(\"#acdaut1 #E23\").click(function(){acd1_edge(23);});$(\"#acdaut1 #E24\").click(function(){acd1_edge(24);});$(\"#acdaut1 #E25\").click(function(){acd1_edge(25);});$(\"#acdaut1 #E26\").click(function(){acd1_edge(26);});$(\"#acdaut1 #E27\").click(function(){acd1_edge(27);});$(\"#acdaut1 #E28\").click(function(){acd1_edge(28);});$(\"#acdaut1 #E29\").click(function(){acd1_edge(29);});$(\"#acdaut1 #E30\").click(function(){acd1_edge(30);});$(\"#acdaut1 #E31\").click(function(){acd1_edge(31);});$(\"#acdaut1 #E32\").click(function(){acd1_edge(32);});$(\"#acdaut1 #E33\").click(function(){acd1_edge(33);});$(\"#acdaut1 #E34\").click(function(){acd1_edge(34);});$(\"#acdaut1 #E35\").click(function(){acd1_edge(35);});$(\"#acdaut1 #E36\").click(function(){acd1_edge(36);});$(\"#acdaut1 #E37\").click(function(){acd1_edge(37);});$(\"#acdaut1 #E38\").click(function(){acd1_edge(38);});$(\"#acdaut1 #E39\").click(function(){acd1_edge(39);});$(\"#acdaut1 #E40\").click(function(){acd1_edge(40);});$(\"#acdaut1 #S0\").click(function(){acd1_state(0);});$(\"#acdaut1 #S1\").click(function(){acd1_state(1);});$(\"#acdaut1 #S2\").click(function(){acd1_state(2);});$(\"#acdaut1 #S3\").click(function(){acd1_state(3);});$(\"#acdaut1 #S4\").click(function(){acd1_state(4);});$(\"#acdaut1 #S5\").click(function(){acd1_state(5);});$(\"#acdaut1 #S6\").click(function(){acd1_state(6);});$(\"#acdaut1 #S7\").click(function(){acd1_state(7);});$(\"#acdaut1 #S8\").click(function(){acd1_state(8);});$(\"#acdaut1 #S9\").click(function(){acd1_state(9);});$(\"#acd1 #N0\").click(function(){acd1_node(0, 0);});$(\"#acd1 #N1\").click(function(){acd1_node(1, 1);});$(\"#acd1 #N2\").click(function(){acd1_node(2, 1);});$(\"#acd1 #N3\").click(function(){acd1_node(3, 1);});$(\"#acd1 #N4\").click(function(){acd1_node(4, 1);});$(\"#acd1 #N5\").click(function(){acd1_node(5, 1);});$(\"#acd1 #N6\").click(function(){acd1_node(6, 1);});$(\"#acd1 #N7\").click(function(){acd1_node(7, 1);});$(\"#acd1 #N8\").click(function(){acd1_node(8, 1);});$(\"#acd1 #N9\").click(function(){acd1_node(9, 0);});$(\"#acd1 #N10\").click(function(){acd1_node(10, 0);});$(\"#acd1 #N11\").click(function(){acd1_node(11, 0);});$(\"#acd1 #N12\").click(function(){acd1_node(12, 0);});$(\"#acd1 #N13\").click(function(){acd1_node(13, 0);});$(\"#acd1 #N14\").click(function(){acd1_node(14, 0);});" ], "text/plain": [ - " >" + " >" ] }, - "execution_count": 38, + "execution_count": 40, "metadata": {}, "output_type": "execute_result" } @@ -6695,7 +6926,7 @@ }, { "cell_type": "code", - "execution_count": 39, + "execution_count": 41, "id": "00acde97", "metadata": {}, "outputs": [ @@ -6705,7 +6936,7 @@ "4" ] }, - "execution_count": 39, + "execution_count": 41, "metadata": {}, "output_type": "execute_result" } @@ -6716,7 +6947,7 @@ }, { "cell_type": "code", - "execution_count": 40, + "execution_count": 42, "id": "23c5f4df", "metadata": {}, "outputs": [ @@ -6726,7 +6957,7 @@ "8" ] }, - "execution_count": 40, + "execution_count": 42, "metadata": {}, "output_type": "execute_result" } @@ -6737,7 +6968,7 @@ }, { "cell_type": "code", - "execution_count": 41, + "execution_count": 43, "id": "da0bbcbe", "metadata": {}, "outputs": [ @@ -6747,7 +6978,7 @@ "0" ] }, - "execution_count": 41, + "execution_count": 43, "metadata": {}, "output_type": "execute_result" } @@ -6758,7 +6989,7 @@ }, { "cell_type": "code", - "execution_count": 42, + "execution_count": 44, "id": "da0dc5bc", "metadata": {}, "outputs": [ @@ -6768,7 +6999,7 @@ "8" ] }, - "execution_count": 42, + "execution_count": 44, "metadata": {}, "output_type": "execute_result" } @@ -6788,7 +7019,7 @@ }, { "cell_type": "code", - "execution_count": 43, + "execution_count": 45, "id": "94999c2e", "metadata": {}, "outputs": [ @@ -7586,10 +7817,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f0c49342570> >" + " *' at 0x7f14700fe1e0> >" ] }, - "execution_count": 43, + "execution_count": 45, "metadata": {}, "output_type": "execute_result" } @@ -7611,7 +7842,7 @@ }, { "cell_type": "code", - "execution_count": 44, + "execution_count": 46, "id": "b57476cf", "metadata": {}, "outputs": [ @@ -7640,7 +7871,7 @@ }, { "cell_type": "code", - "execution_count": 45, + "execution_count": 47, "id": "f082b433", "metadata": {}, "outputs": [ @@ -7912,10 +8143,10 @@ "};$(\"#acdaut2 #E1\").addClass(\"acdN0\");$(\"#acdaut2 #E2\").addClass(\"acdN0\");$(\"#acdaut2 #E3\").addClass(\"acdN0\");$(\"#acdaut2 #E4\").addClass(\"acdN0\");$(\"#acdaut2 #E5\").addClass(\"acdN0\");$(\"#acdaut2 #E6\").addClass(\"acdN0\");$(\"#acdaut2 #E2\").addClass(\"acdN1\");$(\"#acdaut2 #E3\").addClass(\"acdN1\");$(\"#acdaut2 #E4\").addClass(\"acdN1\");$(\"#acdaut2 #E5\").addClass(\"acdN1\");$(\"#acdaut2 #E6\").addClass(\"acdN1\");$(\"#acdaut2 #E1\").addClass(\"acdN2\");$(\"#acdaut2 #E2\").addClass(\"acdN2\");$(\"#acdaut2 #E4\").addClass(\"acdN2\");$(\"#acdaut2 #E6\").addClass(\"acdN2\");$(\"#acdaut2 #E1\").click(function(){acd2_edge(1);});$(\"#acdaut2 #E2\").click(function(){acd2_edge(2);});$(\"#acdaut2 #E3\").click(function(){acd2_edge(3);});$(\"#acdaut2 #E4\").click(function(){acd2_edge(4);});$(\"#acdaut2 #E5\").click(function(){acd2_edge(5);});$(\"#acdaut2 #E6\").click(function(){acd2_edge(6);});$(\"#acdaut2 #S0\").click(function(){acd2_state(0);});$(\"#acdaut2 #S1\").click(function(){acd2_state(1);});$(\"#acdaut2 #S2\").click(function(){acd2_state(2);});$(\"#acd2 #N0\").click(function(){acd2_node(0, 1);});$(\"#acd2 #N1\").click(function(){acd2_node(1, 0);});$(\"#acd2 #N2\").click(function(){acd2_node(2, 0);});" ], "text/plain": [ - " >" + " >" ] }, - "execution_count": 45, + "execution_count": 47, "metadata": {}, "output_type": "execute_result" } @@ -7931,7 +8162,7 @@ }, { "cell_type": "code", - "execution_count": 46, + "execution_count": 48, "id": "597185c0", "metadata": {}, "outputs": [ @@ -7944,11 +8175,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -8122,10 +8353,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f0c480e0690> >" + " *' at 0x7f14700feb40> >" ] }, - "execution_count": 46, + "execution_count": 48, "metadata": {}, "output_type": "execute_result" } @@ -8154,7 +8385,7 @@ }, { "cell_type": "code", - "execution_count": 47, + "execution_count": 49, "id": "a4fd4105", "metadata": {}, "outputs": [ @@ -8426,10 +8657,10 @@ "};$(\"#acdaut3 #E1\").addClass(\"acdN0\");$(\"#acdaut3 #E2\").addClass(\"acdN0\");$(\"#acdaut3 #E3\").addClass(\"acdN0\");$(\"#acdaut3 #E4\").addClass(\"acdN0\");$(\"#acdaut3 #E5\").addClass(\"acdN0\");$(\"#acdaut3 #E6\").addClass(\"acdN0\");$(\"#acdaut3 #E1\").addClass(\"acdN1\");$(\"#acdaut3 #E2\").addClass(\"acdN1\");$(\"#acdaut3 #E4\").addClass(\"acdN1\");$(\"#acdaut3 #E6\").addClass(\"acdN1\");$(\"#acdaut3 #E2\").addClass(\"acdN2\");$(\"#acdaut3 #E3\").addClass(\"acdN2\");$(\"#acdaut3 #E4\").addClass(\"acdN2\");$(\"#acdaut3 #E5\").addClass(\"acdN2\");$(\"#acdaut3 #E6\").addClass(\"acdN2\");$(\"#acdaut3 #E1\").click(function(){acd3_edge(1);});$(\"#acdaut3 #E2\").click(function(){acd3_edge(2);});$(\"#acdaut3 #E3\").click(function(){acd3_edge(3);});$(\"#acdaut3 #E4\").click(function(){acd3_edge(4);});$(\"#acdaut3 #E5\").click(function(){acd3_edge(5);});$(\"#acdaut3 #E6\").click(function(){acd3_edge(6);});$(\"#acdaut3 #S0\").click(function(){acd3_state(0);});$(\"#acdaut3 #S1\").click(function(){acd3_state(1);});$(\"#acdaut3 #S2\").click(function(){acd3_state(2);});$(\"#acd3 #N0\").click(function(){acd3_node(0, 1);});$(\"#acd3 #N1\").click(function(){acd3_node(1, 0);});$(\"#acd3 #N2\").click(function(){acd3_node(2, 0);});" ], "text/plain": [ - " >" + " >" ] }, - "execution_count": 47, + "execution_count": 49, "metadata": {}, "output_type": "execute_result" } @@ -8440,7 +8671,7 @@ }, { "cell_type": "code", - "execution_count": 48, + "execution_count": 50, "id": "1a68f96a", "metadata": {}, "outputs": [ @@ -8453,11 +8684,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -8610,10 +8841,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f0c480e0de0> >" + " *' at 0x7f14700fea80> >" ] }, - "execution_count": 48, + "execution_count": 50, "metadata": {}, "output_type": "execute_result" } @@ -8636,7 +8867,7 @@ }, { "cell_type": "code", - "execution_count": 49, + "execution_count": 51, "id": "criminal-northwest", "metadata": {}, "outputs": [ @@ -8762,10 +8993,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f0c480e21e0> >" + " *' at 0x7f1470107240> >" ] }, - "execution_count": 49, + "execution_count": 51, "metadata": {}, "output_type": "execute_result" } @@ -8796,7 +9027,7 @@ }, { "cell_type": "code", - "execution_count": 50, + "execution_count": 52, "id": "63c7c062", "metadata": {}, "outputs": [ @@ -8874,10 +9105,10 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, - "execution_count": 50, + "execution_count": 52, "metadata": {}, "output_type": "execute_result" } @@ -8888,7 +9119,7 @@ }, { "cell_type": "code", - "execution_count": 51, + "execution_count": 53, "id": "balanced-investing", "metadata": {}, "outputs": [ @@ -9040,10 +9271,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f0c480e2360> >" + " *' at 0x7f1470107030> >" ] }, - "execution_count": 51, + "execution_count": 53, "metadata": {}, "output_type": "execute_result" } @@ -9054,7 +9285,7 @@ }, { "cell_type": "code", - "execution_count": 52, + "execution_count": 54, "id": "nutritional-rugby", "metadata": {}, "outputs": [], @@ -9064,7 +9295,7 @@ }, { "cell_type": "code", - "execution_count": 53, + "execution_count": 55, "id": "criminal-marking", "metadata": {}, "outputs": [ @@ -9333,10 +9564,10 @@ "};$(\"#acdaut4 #E1\").addClass(\"acdN0\");$(\"#acdaut4 #E2\").addClass(\"acdN0\");$(\"#acdaut4 #E3\").addClass(\"acdN0\");$(\"#acdaut4 #E4\").addClass(\"acdN0\");$(\"#acdaut4 #E5\").addClass(\"acdN0\");$(\"#acdaut4 #E6\").addClass(\"acdN0\");$(\"#acdaut4 #E7\").addClass(\"acdN0\");$(\"#acdaut4 #E8\").addClass(\"acdN0\");$(\"#acdaut4 #E6\").addClass(\"acdN1\");$(\"#acdaut4 #E1\").click(function(){acd4_edge(1);});$(\"#acdaut4 #E2\").click(function(){acd4_edge(2);});$(\"#acdaut4 #E3\").click(function(){acd4_edge(3);});$(\"#acdaut4 #E4\").click(function(){acd4_edge(4);});$(\"#acdaut4 #E5\").click(function(){acd4_edge(5);});$(\"#acdaut4 #E6\").click(function(){acd4_edge(6);});$(\"#acdaut4 #E7\").click(function(){acd4_edge(7);});$(\"#acdaut4 #E8\").click(function(){acd4_edge(8);});$(\"#acdaut4 #S0\").click(function(){acd4_state(0);});$(\"#acdaut4 #S1\").click(function(){acd4_state(1);});$(\"#acd4 #N0\").click(function(){acd4_node(0, 1);});$(\"#acd4 #N1\").click(function(){acd4_node(1, 0);});" ], "text/plain": [ - " >" + " >" ] }, - "execution_count": 53, + "execution_count": 55, "metadata": {}, "output_type": "execute_result" } @@ -9347,7 +9578,7 @@ }, { "cell_type": "code", - "execution_count": 54, + "execution_count": 56, "id": "e7760d51", "metadata": {}, "outputs": [ @@ -9357,7 +9588,7 @@ "0" ] }, - "execution_count": 54, + "execution_count": 56, "metadata": {}, "output_type": "execute_result" } @@ -9368,7 +9599,7 @@ }, { "cell_type": "code", - "execution_count": 55, + "execution_count": 57, "id": "unusual-dependence", "metadata": { "scrolled": true @@ -9477,10 +9708,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f0c480e2d50> >" + " *' at 0x7f1470107b70> >" ] }, - "execution_count": 55, + "execution_count": 57, "metadata": {}, "output_type": "execute_result" } @@ -9491,7 +9722,7 @@ }, { "cell_type": "code", - "execution_count": 56, + "execution_count": 58, "id": "d5440de1", "metadata": {}, "outputs": [ @@ -9504,11 +9735,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -9624,10 +9855,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f0c480ea150> >" + " *' at 0x7f147010d240> >" ] }, - "execution_count": 56, + "execution_count": 58, "metadata": {}, "output_type": "execute_result" } @@ -9638,7 +9869,7 @@ }, { "cell_type": "code", - "execution_count": 57, + "execution_count": 59, "id": "9ed0bc59", "metadata": {}, "outputs": [], @@ -9658,7 +9889,7 @@ }, { "cell_type": "code", - "execution_count": 58, + "execution_count": 60, "id": "deb92971", "metadata": {}, "outputs": [ @@ -9963,10 +10194,10 @@ "};$(\"#acdaut5 #E1\").addClass(\"acdN0\");$(\"#acdaut5 #E2\").addClass(\"acdN0\");$(\"#acdaut5 #E3\").addClass(\"acdN0\");$(\"#acdaut5 #E4\").addClass(\"acdN0\");$(\"#acdaut5 #E5\").addClass(\"acdN0\");$(\"#acdaut5 #E6\").addClass(\"acdN0\");$(\"#acdaut5 #E7\").addClass(\"acdN0\");$(\"#acdaut5 #E1\").addClass(\"acdN1\");$(\"#acdaut5 #E3\").addClass(\"acdN1\");$(\"#acdaut5 #E4\").addClass(\"acdN1\");$(\"#acdaut5 #E5\").addClass(\"acdN1\");$(\"#acdaut5 #E7\").addClass(\"acdN2\");$(\"#acdaut5 #E1\").click(function(){acd5_edge(1);});$(\"#acdaut5 #E2\").click(function(){acd5_edge(2);});$(\"#acdaut5 #E3\").click(function(){acd5_edge(3);});$(\"#acdaut5 #E4\").click(function(){acd5_edge(4);});$(\"#acdaut5 #E5\").click(function(){acd5_edge(5);});$(\"#acdaut5 #E6\").click(function(){acd5_edge(6);});$(\"#acdaut5 #E7\").click(function(){acd5_edge(7);});$(\"#acdaut5 #S0\").click(function(){acd5_state(0);});$(\"#acdaut5 #S1\").click(function(){acd5_state(1);});$(\"#acdaut5 #S2\").click(function(){acd5_state(2);});$(\"#acdaut5 #S3\").click(function(){acd5_state(3);});$(\"#acd5 #N0\").click(function(){acd5_node(0, 1);});$(\"#acd5 #N1\").click(function(){acd5_node(1, 0);});$(\"#acd5 #N2\").click(function(){acd5_node(2, 0);});" ], "text/plain": [ - " >" + " >" ] }, - "execution_count": 58, + "execution_count": 60, "metadata": {}, "output_type": "execute_result" } @@ -9984,7 +10215,7 @@ }, { "cell_type": "code", - "execution_count": 59, + "execution_count": 61, "id": "94a02201", "metadata": {}, "outputs": [ @@ -10091,10 +10322,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f0c480e2300> >" + " *' at 0x7f147010d5a0> >" ] }, - "execution_count": 59, + "execution_count": 61, "metadata": {}, "output_type": "execute_result" } @@ -10105,7 +10336,7 @@ }, { "cell_type": "code", - "execution_count": 60, + "execution_count": 62, "id": "d484ba8f", "metadata": {}, "outputs": [ @@ -10118,11 +10349,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -10221,10 +10452,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f0c480f0420> >" + " *' at 0x7f147010d6f0> >" ] }, - "execution_count": 60, + "execution_count": 62, "metadata": {}, "output_type": "execute_result" } @@ -10235,7 +10466,7 @@ }, { "cell_type": "code", - "execution_count": 61, + "execution_count": 63, "id": "3332e850", "metadata": {}, "outputs": [ @@ -10501,10 +10732,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f0c480f0840> >" + " *' at 0x7f1470116270> >" ] }, - "execution_count": 61, + "execution_count": 63, "metadata": {}, "output_type": "execute_result" } @@ -10525,7 +10756,7 @@ }, { "cell_type": "code", - "execution_count": 62, + "execution_count": 64, "id": "german-vienna", "metadata": {}, "outputs": [ @@ -10595,10 +10826,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f0c480f30c0> >" + " *' at 0x7f1470116630> >" ] }, - "execution_count": 62, + "execution_count": 64, "metadata": {}, "output_type": "execute_result" } @@ -10622,7 +10853,7 @@ }, { "cell_type": "code", - "execution_count": 63, + "execution_count": 65, "id": "chemical-primary", "metadata": {}, "outputs": [ @@ -10632,7 +10863,7 @@ "(spot.trival_maybe(), spot.trival(True))" ] }, - "execution_count": 63, + "execution_count": 65, "metadata": {}, "output_type": "execute_result" } @@ -10643,7 +10874,7 @@ }, { "cell_type": "code", - "execution_count": 64, + "execution_count": 66, "id": "hispanic-floor", "metadata": {}, "outputs": [ @@ -10706,10 +10937,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f0c480f3210> >" + " *' at 0x7f1470116450> >" ] }, - "execution_count": 64, + "execution_count": 66, "metadata": {}, "output_type": "execute_result" } @@ -10720,7 +10951,7 @@ }, { "cell_type": "code", - "execution_count": 65, + "execution_count": 67, "id": "central-london", "metadata": {}, "outputs": [ @@ -10730,7 +10961,7 @@ "(spot.trival(True), spot.trival(True))" ] }, - "execution_count": 65, + "execution_count": 67, "metadata": {}, "output_type": "execute_result" } @@ -10750,7 +10981,7 @@ ], "metadata": { "kernelspec": { - "display_name": "Python 3", + "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" }, diff --git a/tests/python/zlktree.py b/tests/python/zlktree.py index e1b0c9e7b..c3cb262f2 100644 --- a/tests/python/zlktree.py +++ b/tests/python/zlktree.py @@ -152,3 +152,12 @@ tc.assertTrue(a.equivalent_to(b)) b = spot.acd_transform_sbacc(a, False) tc.assertEqual(str(b.acc()), '(2, Fin(0) & Inf(1))') tc.assertTrue(a.equivalent_to(b)) + + +# This used to be very slow. +c = spot.acc_cond("Rabin 9") +n = spot.zielonka_tree(c).num_branches() +tc.assertEqual(n, 362880) +opt = spot.zielonka_tree_options_MERGE_SUBTREES; +n = spot.zielonka_tree(c, opt).num_branches() +tc.assertEqual(n, 9)