From fea0be96c1c77a764b3a8db42d3b3abbd356055e Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 24 Sep 2021 20:39:47 +0200 Subject: [PATCH] acd: add ORDER_HEURISTIC for state-based ACD-transform * spot/twaalgos/zlktree.cc, spot/twaalgos/zlktree.hh: Add the acd_options::ORDER_HEURISTIC and use it by default in acd_transform_sbacc(). * spot/misc/bitvect.hh (bitvect::count, bitvect::add_common): New methods. * tests/python/zlktree.ipynb: Adjust examples and discuss this heuristic. --- spot/misc/bitvect.hh | 36 + spot/twaalgos/zlktree.cc | 68 +- spot/twaalgos/zlktree.hh | 11 +- tests/python/zlktree.ipynb | 2094 ++++++++++++++++++++++++++---------- 4 files changed, 1655 insertions(+), 554 deletions(-) diff --git a/spot/misc/bitvect.hh b/spot/misc/bitvect.hh index d91653381..3588b406e 100644 --- a/spot/misc/bitvect.hh +++ b/spot/misc/bitvect.hh @@ -255,6 +255,16 @@ namespace spot return *this; } + bitvect& add_common(const bitvect& other1, const bitvect& other2) + { + SPOT_ASSERT(other1.size_ <= size_ && other2.size_ <= size_); + unsigned m = std::min(other2.block_count_, + std::min(other1.block_count_, block_count_)); + for (size_t i = 0; i < m; ++i) + storage_[i] |= other1.storage_[i] & other2.storage_[i]; + return *this; + } + bool intersects(const bitvect& other) { SPOT_ASSERT(other.size_ <= size_); @@ -302,6 +312,32 @@ namespace spot == (storage_[i] & mask)); } + unsigned count() const + { + size_t i; + const size_t bpb = 8 * sizeof(bitvect::block_t); + size_t rest = size() % bpb; + size_t c = 0; + for (i = 0; i < block_count_; ++i) + { + block_t v = storage_[i]; + if ((i == block_count_ - 1) && rest) + // The last block might not be fully used, scan only the + // relevant portion. + v &= (1UL << rest) - 1; +#ifdef __GNUC__ + c += __builtin_popcountl(v); +#else + while (v) + { + ++c; + v &= v - 1; + } +#endif + } + return c; + } + bool operator==(const bitvect& other) const { if (other.size_ != size_) diff --git a/spot/twaalgos/zlktree.cc b/spot/twaalgos/zlktree.cc index 0273e2c2c..a85ef0b55 100644 --- a/spot/twaalgos/zlktree.cc +++ b/spot/twaalgos/zlktree.cc @@ -20,6 +20,7 @@ #include "config.h" #include #include +#include #include #include #include @@ -439,6 +440,15 @@ namespace spot }; std::vector out; + std::unique_ptr seen_src; + std::unique_ptr seen_dst; + std::unique_ptr seen_dup; + if (!!(opt_ & acd_options::ORDER_HEURISTIC)) + { + seen_src.reset(make_bitvect(nstates)); + seen_dst.reset(make_bitvect(nstates)); + seen_dup.reset(make_bitvect(nstates)); + } // This loop is a BFS over the increasing set of nodes. for (unsigned node = 0; node < nodes_.size(); ++node) { @@ -483,9 +493,55 @@ namespace spot accepting_node ? negacc : posacc, nodes_[node].edges, callback); + if (!!(opt_ & acd_options::ORDER_HEURISTIC)) + { + // Find states that appear in multiple children + seen_dup->clear_all(); // duplicate states + seen_src->clear_all(); // union of all children states + for (auto& [sz, bv]: out) + { + seen_dst->clear_all(); // local states of the node + bv->foreach_set_index([&aut, &seen_dst](unsigned e) + { + seen_dst->set(aut->edge_storage(e).src); + }); + seen_dup->add_common(*seen_src, *seen_dst); + *seen_src |= *seen_dst; + } + // Now the union in seen_src is not useful anymore. Process + // each node again, but consider only the states that are in + // seen_dup. + for (auto& [sz, bv]: out) + { + seen_src->clear_all(); // local source of the node + bv->foreach_set_index([&aut, &seen_src, &seen_dup](unsigned e) + { + unsigned idx = aut->edge_storage(e).src; + if (seen_dup->get(idx)) + seen_src->set(idx); // store duplicates + }); + seen_dst->clear_all(); + // Count the number of states reached by leaving this node. + seen_src->foreach_set_index([&aut, bv=bv.get(), + &seen_dst](unsigned s) + { + for (auto& e: aut->out(s)) + if (!bv->get(aut->edge_number(e))) + seen_dst->set(e.dst); + }); + sz = seen_dst->count(); + } + // reorder by decreasing number of new states reached + std::stable_sort(out.begin(), out.end(), + [&](auto& p1, auto& p2) { + return p1.size > p2.size; + }); + } + unsigned before_size = nodes_.size(); for (const auto& [sz, bv]: out) { + (void)sz; unsigned vnum = trees_[scc].num_nodes++; allocate_vectors_maybe(vnum); nodes_.emplace_back(edge_vector(vnum), state_vector(vnum)); @@ -877,12 +933,13 @@ namespace spot // ACD, to template twa_graph_ptr - acd_transform_(const const_twa_graph_ptr& a, bool colored) + acd_transform_(const const_twa_graph_ptr& a, bool colored, + acd_options options = acd_options::NONE) { auto res = make_twa_graph(a->get_dict()); res->copy_ap_of(a); scc_info si(a, scc_info_options::TRACK_STATES); - acd theacd(si); + acd theacd(si, options); // If we desire non-colored output, we can omit the maximal // color of each SCC if it has the same parity as max_level. @@ -1022,9 +1079,12 @@ namespace spot } twa_graph_ptr - acd_transform_sbacc(const const_twa_graph_ptr& a, bool colored) + acd_transform_sbacc(const const_twa_graph_ptr& a, bool colored, + bool order_heuristic) { - return acd_transform_(a, colored); + return acd_transform_(a, colored, order_heuristic + ? acd_options::ORDER_HEURISTIC + : acd_options::NONE); } } diff --git a/spot/twaalgos/zlktree.hh b/spot/twaalgos/zlktree.hh index 17c142521..1fa8dfee8 100644 --- a/spot/twaalgos/zlktree.hh +++ b/spot/twaalgos/zlktree.hh @@ -167,6 +167,11 @@ namespace spot /// shape that is tested. When that happens, node_count() is set /// to 0. ABORT_WRONG_SHAPE = 4, + /// Order the children of a node by decreasing size of the number + /// of states they would introduce if that child appears as the + /// last child of an "ACD" round in the state-based version of the + /// ACD output. + ORDER_HEURISTIC = 8, }; #ifndef SWIG @@ -407,13 +412,15 @@ namespace spot /// optimal transition-based output (optimal in the sense of least /// number of duplicated states), while the acd_tansform_sbacc() variant /// produces state-based output from transition-based input and without - /// any optimality claim. + /// any optimality claim. The \a order_heuristics argument, enabled + /// by default activates the ORDER_HEURISTICS option of the ACD. /// @{ SPOT_API twa_graph_ptr acd_transform(const const_twa_graph_ptr& aut, bool colored = false); SPOT_API twa_graph_ptr acd_transform_sbacc(const const_twa_graph_ptr& aut, - bool colored = false); + bool colored = false, + bool order_heuristic = true); /// @} } diff --git a/tests/python/zlktree.ipynb b/tests/python/zlktree.ipynb index f4c822e9a..d46e2ce2c 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 0x7f296c3d8210> >" + " *' at 0x7f0c49328600> >" ] }, "execution_count": 10, @@ -1063,7 +1063,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f296c3d8fc0> >" + " *' at 0x7f0c493284b0> >" ] }, "execution_count": 11, @@ -1256,7 +1256,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f296c3d8c90> >" + " *' at 0x7f0c49328f30> >" ] }, "execution_count": 13, @@ -1701,7 +1701,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f296c3e1210> >" + " *' at 0x7f0c49330420> >" ] }, "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": {}, @@ -3862,7 +3862,7 @@ "};$(\"#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, @@ -4737,7 +4737,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f296c3d81e0> >" + " *' at 0x7f0c49328840> >" ] }, "execution_count": 27, @@ -5376,7 +5376,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f296cd16c30> >" + " *' at 0x7f0c49328e70> >" ] }, "execution_count": 29, @@ -5557,7 +5557,9 @@ "## State-based transformation\n", "\n", "The ACD usage can be modified slightly in order to produce a state-based automaton. The rules for stepping through the ACD are similar, except that when we detect that a cycle through all children of a node has been done, we return the current node without going to the leftmost leave of the next children. When stepping a transition from a node a child, we should act as if we were in the leftmost child of that node containing the source of tha transition. Stepping through a transition this way do not emit any color, instead the color of a state will be the level of its associated node.\n", - "(This modified transformation do not claim to be optimal, unlike the transition-based version.)" + "(This modified transformation do not claim to be optimal, unlike the transition-based version.)\n", + "\n", + "The `ORDER_HEURISTIC` used below will be explained in the next section, it justs alters ordering of children of the ACD in a way that the state-based transformation prefers." ] }, { @@ -5567,7 +5569,7 @@ "metadata": {}, "outputs": [], "source": [ - "theacd = spot.acd(a3)" + "theacd = spot.acd(a3, spot.acd_options_ORDER_HEURISTIC)" ] }, { @@ -5621,9 +5623,9 @@ "\n", "5\n", "\n", - "T: 23,24,34,36\n", - "{1,2,3,5}\n", - "Q: 5,8\n", + "T: 14,15,22,23\n", + "{1,2,3,4}\n", + "Q: 3,5\n", "lvl: 1\n", "\n", "\n", @@ -5636,9 +5638,9 @@ "\n", "6\n", "\n", - "T: 14,15,22,23\n", - "{1,2,3,4}\n", - "Q: 3,5\n", + "T: 23,24,34,36\n", + "{1,2,3,5}\n", + "Q: 5,8\n", "lvl: 1\n", "\n", "\n", @@ -5681,50 +5683,50 @@ "\n", "\n", "11\n", - "\n", - "T: 23\n", - "{1,3}\n", - "Q: 5\n", - "lvl: 2\n", - "<11>\n", + "\n", + "T: 14\n", + "{1,3}\n", + "Q: 3\n", + "lvl: 2\n", + "<11>\n", "\n", "\n", "\n", "5->11\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "12\n", - "\n", - "T: 14\n", - "{1,3}\n", - "Q: 3\n", - "lvl: 2\n", - "<12>\n", + "\n", + "T: 23\n", + "{1,3}\n", + "Q: 5\n", + "lvl: 2\n", + "<12>\n", "\n", - "\n", + "\n", "\n", - "6->12\n", - "\n", - "\n", + "5->12\n", + "\n", + "\n", "\n", "\n", "\n", "13\n", - "\n", - "T: 23\n", - "{1,3}\n", - "Q: 5\n", - "lvl: 2\n", - "<13>\n", + "\n", + "T: 23\n", + "{1,3}\n", + "Q: 5\n", + "lvl: 2\n", + "<13>\n", "\n", "\n", "\n", "6->13\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", @@ -6434,14 +6436,14 @@ "\n", "\n", "\n", - "\n", "5\n", "\n", - "T: 23,24,34,36\n", - "{1,2,3,5}\n", - "Q: 5,8\n", + "T: 14,15,22,23\n", + "{1,2,3,4}\n", + "Q: 3,5\n", "lvl: 1\n", "\n", "\n", @@ -6451,14 +6453,14 @@ "\n", "\n", "\n", - "\n", "6\n", "\n", - "T: 14,15,22,23\n", - "{1,2,3,4}\n", - "Q: 3,5\n", + "T: 23,24,34,36\n", + "{1,2,3,5}\n", + "Q: 5,8\n", "lvl: 1\n", "\n", "\n", @@ -6502,55 +6504,55 @@ "\n", "\n", "\n", - "\n", "11\n", - "\n", - "T: 23\n", - "{1,3}\n", - "Q: 5\n", - "lvl: 2\n", - "<11>\n", + "\n", + "T: 14\n", + "{1,3}\n", + "Q: 3\n", + "lvl: 2\n", + "<11>\n", "\n", "\n", "\n", "5->11\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", - "\n", "12\n", - "\n", - "T: 14\n", - "{1,3}\n", - "Q: 3\n", - "lvl: 2\n", - "<12>\n", + "\n", + "T: 23\n", + "{1,3}\n", + "Q: 5\n", + "lvl: 2\n", + "<12>\n", "\n", - "\n", + "\n", "\n", - "6->12\n", - "\n", - "\n", + "5->12\n", + "\n", + "\n", "\n", "\n", "\n", "13\n", - "\n", - "T: 23\n", - "{1,3}\n", - "Q: 5\n", - "lvl: 2\n", - "<13>\n", + "\n", + "T: 23\n", + "{1,3}\n", + "Q: 5\n", + "lvl: 2\n", + "<13>\n", "\n", "\n", "\n", "6->13\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "" + "};$(\"#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, @@ -6799,792 +6801,792 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Fin(\n", - "⓿\n", - ") & Inf(\n", - "❶\n", - ")\n", - "[Rabin 1]\n", + "\n", + "\n", + "\n", + "Fin(\n", + "⓿\n", + ") & Inf(\n", + "❶\n", + ")\n", + "[Rabin 1]\n", "\n", "\n", "\n", "0\n", - "\n", - "0#3\n", - "❶\n", + "\n", + "0#3\n", + "❶\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!p0 & !p1\n", + "\n", + "\n", + "!p0 & !p1\n", "\n", "\n", "\n", "1\n", - "\n", - "1#10\n", + "\n", + "1#10\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!p0 & p1\n", + "\n", + "\n", + "!p0 & p1\n", "\n", "\n", "\n", "2\n", - "\n", - "2#4\n", - "❶\n", + "\n", + "2#4\n", + "❶\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "p0 & !p1\n", + "\n", + "\n", + "p0 & !p1\n", "\n", "\n", "\n", "3\n", - "\n", - "3#4\n", - "❶\n", + "\n", + "3#4\n", + "❶\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "p0 & p1\n", + "\n", + "\n", + "p0 & p1\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!p0 & p1\n", + "\n", + "\n", + "!p0 & p1\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "p0 & !p1\n", + "\n", + "\n", + "p0 & !p1\n", "\n", "\n", "\n", "4\n", - "\n", - "4#2\n", - "❶\n", + "\n", + "4#2\n", + "❶\n", "\n", "\n", "\n", "1->4\n", - "\n", - "\n", - "!p0 & !p1\n", + "\n", + "\n", + "!p0 & !p1\n", "\n", "\n", "\n", "5\n", - "\n", - "5#4\n", - "❶\n", + "\n", + "5#4\n", + "❶\n", "\n", "\n", "\n", "1->5\n", - "\n", - "\n", - "p0 & p1\n", + "\n", + "\n", + "p0 & p1\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "p0 & !p1\n", + "\n", + "\n", + "p0 & !p1\n", "\n", "\n", "\n", "2->3\n", - "\n", - "\n", - "p0 & p1\n", + "\n", + "\n", + "p0 & p1\n", "\n", "\n", "\n", "6\n", - "\n", - "2#8\n", - "❶\n", + "\n", + "2#8\n", + "❶\n", "\n", "\n", "\n", "2->6\n", - "\n", - "\n", - "!p0 & !p1\n", + "\n", + "\n", + "!p0 & !p1\n", "\n", "\n", "\n", "7\n", - "\n", - "3#6\n", - "❶\n", + "\n", + "3#5\n", + "❶\n", "\n", "\n", "\n", "2->7\n", - "\n", - "\n", - "!p0 & p1\n", + "\n", + "\n", + "!p0 & p1\n", "\n", "\n", "\n", "3->2\n", - "\n", - "\n", - "p0 & !p1\n", + "\n", + "\n", + "p0 & !p1\n", "\n", "\n", "\n", "3->5\n", - "\n", - "\n", - "p0 & p1\n", + "\n", + "\n", + "p0 & p1\n", "\n", "\n", "\n", "3->7\n", - "\n", - "\n", - "!p0 & p1\n", + "\n", + "\n", + "!p0 & p1\n", "\n", "\n", "\n", "8\n", - "\n", - "6#7\n", - "❶\n", + "\n", + "6#7\n", + "❶\n", "\n", "\n", "\n", "3->8\n", - "\n", - "\n", - "!p0 & !p1\n", + "\n", + "\n", + "!p0 & !p1\n", "\n", "\n", "\n", "4->1\n", - "\n", - "\n", - "!p0 & p1\n", + "\n", + "\n", + "!p0 & p1\n", "\n", "\n", "\n", "4->2\n", - "\n", - "\n", - "p0 & !p1\n", + "\n", + "\n", + "p0 & !p1\n", "\n", "\n", "\n", "4->3\n", - "\n", - "\n", - "p0 & p1\n", + "\n", + "\n", + "p0 & p1\n", "\n", "\n", "\n", "9\n", - "\n", - "7#1\n", - "❶\n", + "\n", + "7#1\n", + "❶\n", "\n", "\n", "\n", "4->9\n", - "\n", - "\n", - "!p0 & !p1\n", + "\n", + "\n", + "!p0 & !p1\n", "\n", "\n", "\n", "5->2\n", - "\n", - "\n", - "p0 & !p1\n", + "\n", + "\n", + "p0 & !p1\n", "\n", "\n", "\n", "5->3\n", - "\n", - "\n", - "p0 & p1\n", + "\n", + "\n", + "p0 & p1\n", "\n", "\n", "\n", "10\n", - "\n", - "5#5\n", - "❶\n", + "\n", + "5#5\n", + "❶\n", "\n", "\n", "\n", "5->10\n", - "\n", - "\n", - "!p0 & p1\n", + "\n", + "\n", + "!p0 & p1\n", "\n", "\n", "\n", "11\n", - "\n", - "8#5\n", - "❶\n", + "\n", + "8#6\n", + "❶\n", "\n", "\n", "\n", "5->11\n", - "\n", - "\n", - "!p0 & !p1\n", + "\n", + "\n", + "!p0 & !p1\n", "\n", "\n", "\n", "6->6\n", - "\n", - "\n", - "!p0 & !p1\n", + "\n", + "\n", + "!p0 & !p1\n", "\n", "\n", "\n", "12\n", - "\n", - "2#0\n", - "⓿\n", + "\n", + "2#0\n", + "⓿\n", "\n", "\n", "\n", "6->12\n", - "\n", - "\n", - "p0 & !p1\n", + "\n", + "\n", + "p0 & !p1\n", "\n", "\n", "\n", "13\n", - "\n", - "3#0\n", - "⓿\n", + "\n", + "3#0\n", + "⓿\n", "\n", "\n", "\n", "6->13\n", - "\n", - "\n", - "!p0 & p1\n", + "\n", + "\n", + "!p0 & p1\n", "\n", "\n", "\n", "6->13\n", - "\n", - "\n", - "p0 & p1\n", + "\n", + "\n", + "p0 & p1\n", "\n", "\n", "\n", "7->6\n", - "\n", - "\n", - "p0 & !p1\n", + "\n", + "\n", + "p0 & !p1\n", "\n", "\n", "\n", "7->8\n", - "\n", - "\n", - "!p0 & !p1\n", + "\n", + "\n", + "!p0 & !p1\n", "\n", "\n", "\n", "14\n", - "\n", - "3#12\n", + "\n", + "3#11\n", "\n", "\n", "\n", "7->14\n", - "\n", - "\n", - "!p0 & p1\n", + "\n", + "\n", + "!p0 & p1\n", "\n", "\n", "\n", "15\n", - "\n", - "5#13\n", + "\n", + "5#12\n", "\n", "\n", "\n", "7->15\n", - "\n", - "\n", - "p0 & p1\n", + "\n", + "\n", + "p0 & p1\n", "\n", "\n", "\n", "8->6\n", - "\n", - "\n", - "p0 & !p1\n", + "\n", + "\n", + "p0 & !p1\n", "\n", "\n", "\n", "8->13\n", - "\n", - "\n", - "p0 & p1\n", + "\n", + "\n", + "p0 & p1\n", "\n", "\n", "\n", "16\n", - "\n", - "3#14\n", + "\n", + "3#14\n", "\n", "\n", "\n", "8->16\n", - "\n", - "\n", - "!p0 & p1\n", + "\n", + "\n", + "!p0 & p1\n", "\n", "\n", "\n", "17\n", - "\n", - "8#0\n", - "⓿\n", + "\n", + "8#0\n", + "⓿\n", "\n", "\n", "\n", "8->17\n", - "\n", - "\n", - "!p0 & !p1\n", + "\n", + "\n", + "!p0 & !p1\n", "\n", "\n", "\n", "9->2\n", - "\n", - "\n", - "p0 & !p1\n", + "\n", + "\n", + "p0 & !p1\n", "\n", "\n", "\n", "9->5\n", - "\n", - "\n", - "p0 & p1\n", + "\n", + "\n", + "p0 & p1\n", "\n", "\n", "\n", "9->9\n", - "\n", - "\n", - "!p0 & !p1\n", + "\n", + "\n", + "!p0 & !p1\n", "\n", "\n", "\n", "18\n", - "\n", - "9#9\n", + "\n", + "9#9\n", "\n", "\n", "\n", "9->18\n", - "\n", - "\n", - "!p0 & p1\n", + "\n", + "\n", + "!p0 & p1\n", "\n", "\n", "\n", "10->6\n", - "\n", - "\n", - "p0 & !p1\n", + "\n", + "\n", + "p0 & !p1\n", "\n", "\n", "\n", "10->7\n", - "\n", - "\n", - "p0 & p1\n", + "\n", + "\n", + "p0 & p1\n", "\n", "\n", "\n", "10->11\n", - "\n", - "\n", - "!p0 & !p1\n", + "\n", + "\n", + "!p0 & !p1\n", "\n", - "\n", - "\n", - "19\n", - "\n", - "5#11\n", - "\n", - "\n", + "\n", "\n", - "10->19\n", - "\n", - "\n", - "!p0 & p1\n", + "10->15\n", + "\n", + "\n", + "!p0 & p1\n", "\n", "\n", "\n", "11->6\n", - "\n", - "\n", - "p0 & !p1\n", + "\n", + "\n", + "p0 & !p1\n", "\n", "\n", "\n", "11->11\n", - "\n", - "\n", - "!p0 & !p1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "19\n", + "\n", + "5#13\n", "\n", "\n", "\n", "11->19\n", - "\n", - "\n", - "!p0 & p1\n", + "\n", + "\n", + "!p0 & p1\n", "\n", "\n", "\n", "20\n", - "\n", - "5#6\n", - "❶\n", + "\n", + "5#0\n", + "⓿\n", "\n", "\n", "\n", "11->20\n", - "\n", - "\n", - "p0 & p1\n", + "\n", + "\n", + "p0 & p1\n", "\n", "\n", "\n", "12->2\n", - "\n", - "\n", - "p0 & !p1\n", + "\n", + "\n", + "p0 & !p1\n", "\n", "\n", "\n", "12->3\n", - "\n", - "\n", - "p0 & p1\n", + "\n", + "\n", + "p0 & p1\n", "\n", "\n", "\n", "12->6\n", - "\n", - "\n", - "!p0 & !p1\n", + "\n", + "\n", + "!p0 & !p1\n", "\n", "\n", "\n", "12->7\n", - "\n", - "\n", - "!p0 & p1\n", + "\n", + "\n", + "!p0 & p1\n", "\n", "\n", "\n", "13->2\n", - "\n", - "\n", - "p0 & !p1\n", + "\n", + "\n", + "p0 & !p1\n", "\n", "\n", "\n", "13->5\n", - "\n", - "\n", - "p0 & p1\n", + "\n", + "\n", + "p0 & p1\n", "\n", "\n", "\n", "13->7\n", - "\n", - "\n", - "!p0 & p1\n", + "\n", + "\n", + "!p0 & p1\n", "\n", "\n", "\n", "13->8\n", - "\n", - "\n", - "!p0 & !p1\n", + "\n", + "\n", + "!p0 & !p1\n", "\n", "\n", "\n", "14->6\n", - "\n", - "\n", - "p0 & !p1\n", + "\n", + "\n", + "p0 & !p1\n", "\n", "\n", "\n", "14->8\n", - "\n", - "\n", - "!p0 & !p1\n", + "\n", + "\n", + "!p0 & !p1\n", "\n", "\n", "\n", "14->14\n", - "\n", - "\n", - "!p0 & p1\n", + "\n", + "\n", + "!p0 & p1\n", "\n", "\n", "\n", "14->15\n", - "\n", - "\n", - "p0 & p1\n", + "\n", + "\n", + "p0 & p1\n", "\n", "\n", "\n", "15->6\n", - "\n", - "\n", - "p0 & !p1\n", + "\n", + "\n", + "p0 & !p1\n", "\n", "\n", "\n", "15->7\n", - "\n", - "\n", - "p0 & p1\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "\n", + "15->11\n", + "\n", + "\n", + "!p0 & !p1\n", "\n", "\n", "\n", "15->15\n", - "\n", - "\n", - "!p0 & p1\n", - "\n", - "\n", - "\n", - "15->17\n", - "\n", - "\n", - "!p0 & !p1\n", + "\n", + "\n", + "!p0 & p1\n", "\n", "\n", "\n", "16->6\n", - "\n", - "\n", - "p0 & !p1\n", + "\n", + "\n", + "p0 & !p1\n", "\n", "\n", "\n", "16->8\n", - "\n", - "\n", - "!p0 & !p1\n", + "\n", + "\n", + "!p0 & !p1\n", "\n", "\n", "\n", "16->16\n", - "\n", - "\n", - "!p0 & p1\n", + "\n", + "\n", + "!p0 & p1\n", "\n", - "\n", - "\n", - "21\n", - "\n", - "5#0\n", - "⓿\n", - "\n", - "\n", + "\n", "\n", - "16->21\n", - "\n", - "\n", - "p0 & p1\n", + "16->20\n", + "\n", + "\n", + "p0 & p1\n", "\n", "\n", "\n", "17->6\n", - "\n", - "\n", - "p0 & !p1\n", + "\n", + "\n", + "p0 & !p1\n", "\n", "\n", "\n", "17->11\n", - "\n", - "\n", - "!p0 & !p1\n", + "\n", + "\n", + "!p0 & !p1\n", "\n", "\n", "\n", "17->19\n", - "\n", - "\n", - "!p0 & p1\n", + "\n", + "\n", + "!p0 & p1\n", "\n", "\n", "\n", "17->20\n", - "\n", - "\n", - "p0 & p1\n", + "\n", + "\n", + "p0 & p1\n", "\n", "\n", "\n", "18->2\n", - "\n", - "\n", - "p0 & !p1\n", + "\n", + "\n", + "p0 & !p1\n", "\n", "\n", "\n", "18->3\n", - "\n", - "\n", - "p0 & p1\n", + "\n", + "\n", + "p0 & p1\n", "\n", "\n", "\n", "18->9\n", - "\n", - "\n", - "!p0 & !p1\n", + "\n", + "\n", + "!p0 & !p1\n", "\n", "\n", "\n", "18->18\n", - "\n", - "\n", - "!p0 & p1\n", + "\n", + "\n", + "!p0 & p1\n", "\n", "\n", "\n", "19->6\n", - "\n", - "\n", - "p0 & !p1\n", - "\n", - "\n", - "\n", - "19->7\n", - "\n", - "\n", - "p0 & p1\n", + "\n", + "\n", + "p0 & !p1\n", "\n", "\n", "\n", "19->11\n", - "\n", - "\n", - "!p0 & !p1\n", + "\n", + "\n", + "!p0 & !p1\n", "\n", "\n", "\n", "19->19\n", - "\n", - "\n", - "!p0 & p1\n", + "\n", + "\n", + "!p0 & p1\n", "\n", - "\n", + "\n", + "\n", + "21\n", + "\n", + "3#7\n", + "❶\n", + "\n", + "\n", + "\n", + "19->21\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", "\n", - "20->6\n", - "\n", - "\n", - "p0 & !p1\n", + "20->2\n", + "\n", + "\n", + "p0 & !p1\n", "\n", - "\n", + "\n", "\n", - "20->7\n", - "\n", - "\n", - "p0 & p1\n", + "20->3\n", + "\n", + "\n", + "p0 & p1\n", "\n", - "\n", + "\n", "\n", - "20->15\n", - "\n", - "\n", - "!p0 & p1\n", + "20->10\n", + "\n", + "\n", + "!p0 & p1\n", "\n", - "\n", + "\n", "\n", - "20->17\n", - "\n", - "\n", - "!p0 & !p1\n", + "20->11\n", + "\n", + "\n", + "!p0 & !p1\n", "\n", - "\n", + "\n", "\n", - "21->2\n", - "\n", - "\n", - "p0 & !p1\n", + "21->6\n", + "\n", + "\n", + "p0 & !p1\n", "\n", - "\n", - "\n", - "21->3\n", - "\n", - "\n", - "p0 & p1\n", - "\n", - "\n", - "\n", - "21->10\n", - "\n", - "\n", - "!p0 & p1\n", - "\n", - "\n", + "\n", "\n", - "21->11\n", - "\n", - "\n", - "!p0 & !p1\n", + "21->8\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "21->16\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "21->20\n", + "\n", + "\n", + "p0 & p1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f296c3f3810> >" + " *' at 0x7f0c49342570> >" ] }, "execution_count": 43, @@ -7626,6 +7628,1002 @@ " spot.sbacc(spot.acd_transform(a3)).num_states())" ] }, + { + "cell_type": "markdown", + "id": "9f39b61d", + "metadata": {}, + "source": [ + "## An ordering heuristic for state-based transformation\n", + "\n", + "We now explain the `ORDER_HEURISTIC` option, by first looking at an example without it." + ] + }, + { + "cell_type": "code", + "execution_count": 45, + "id": "f082b433", + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "acd\n", + "\n", + "min even\n", + "\n", + "\n", + "0\n", + "\n", + "SCC #0\n", + "T: 1-6\n", + "{0,1}\n", + "Q: 0-2\n", + "lvl: 0\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "T: 2-6\n", + "{1}\n", + "Q: 0-2\n", + "lvl: 1\n", + "<1>\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "T: 1,2,4,6\n", + "{0}\n", + "Q: 0-2\n", + "lvl: 1\n", + "<2>\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "\n", + "\n", + "\n" + ], + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ")&Inf(\n", + "❶\n", + ")\n", + "[gen. Büchi 2]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "!p\n", + "⓿\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "p\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "!p\n", + "❶\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "p\n", + "\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "p\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "!p\n", + "❶\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "acd\n", + "\n", + "min even\n", + "\n", + "\n", + "0\n", + "\n", + "SCC #0\n", + "T: 1-6\n", + "{0,1}\n", + "Q: 0-2\n", + "lvl: 0\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "T: 2-6\n", + "{1}\n", + "Q: 0-2\n", + "lvl: 1\n", + "<1>\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "T: 1,2,4,6\n", + "{0}\n", + "Q: 0-2\n", + "lvl: 1\n", + "<2>\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + " >" + ] + }, + "execution_count": 45, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "a4 = spot.automaton(\"\"\"HOA: v1 States: 3 Start: \n", + "0 AP: 1 \"p\" acc-name: generalized-Buchi 2 Acceptance: \n", + "2 Inf(1)&Inf(0) properties: trans-labels implicit-labels \n", + "trans-acc complete deterministic --BODY-- State: 0 0 {0}\n", + "1 State: 1 1 {1} 2 State: 2 2 {1} 0 --END--\"\"\")\n", + "spot.acd(a4)" + ] + }, + { + "cell_type": "code", + "execution_count": 46, + "id": "597185c0", + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0#1\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0#2\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!p\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "1#1\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "p\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!p\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "1#2\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "p\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!p\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "2#1\n", + "\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "p\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "1#0\n", + "\n", + "\n", + "\n", + "3->5\n", + "\n", + "\n", + "!p\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "2#2\n", + "\n", + "\n", + "\n", + "3->6\n", + "\n", + "\n", + "p\n", + "\n", + "\n", + "\n", + "4->0\n", + "\n", + "\n", + "p\n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "!p\n", + "\n", + "\n", + "\n", + "5->2\n", + "\n", + "\n", + "!p\n", + "\n", + "\n", + "\n", + "5->4\n", + "\n", + "\n", + "p\n", + "\n", + "\n", + "\n", + "6->1\n", + "\n", + "\n", + "p\n", + "\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "2#0\n", + "\n", + "\n", + "\n", + "6->7\n", + "\n", + "\n", + "!p\n", + "\n", + "\n", + "\n", + "7->0\n", + "\n", + "\n", + "p\n", + "\n", + "\n", + "\n", + "7->4\n", + "\n", + "\n", + "!p\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f0c480e0690> >" + ] + }, + "execution_count": 46, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "s4 = spot.acd_transform_sbacc(a4, False, False) # The third argument disables the heuristic\n", + "s4.copy_state_names_from(a4)\n", + "s4" + ] + }, + { + "cell_type": "markdown", + "id": "03f0eda7", + "metadata": {}, + "source": [ + "One this example, we can see that whenever an edge leaves not 2, it creates a copy of the target state." + ] + }, + { + "cell_type": "markdown", + "id": "45596824", + "metadata": {}, + "source": [ + "The `ORDER_HEURISTIC` option of the ACD construction, attemps to order the children of a node by decreasing number of number of successors that are out of the node. It is activated by default inside `spot.acd_transform_sbacc()`." + ] + }, + { + "cell_type": "code", + "execution_count": 47, + "id": "a4fd4105", + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "acd\n", + "\n", + "min even\n", + "\n", + "\n", + "0\n", + "\n", + "SCC #0\n", + "T: 1-6\n", + "{0,1}\n", + "Q: 0-2\n", + "lvl: 0\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "T: 1,2,4,6\n", + "{0}\n", + "Q: 0-2\n", + "lvl: 1\n", + "<1>\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "T: 2-6\n", + "{1}\n", + "Q: 0-2\n", + "lvl: 1\n", + "<2>\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "\n", + "\n", + "\n" + ], + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ")&Inf(\n", + "❶\n", + ")\n", + "[gen. Büchi 2]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "!p\n", + "⓿\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "p\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "!p\n", + "❶\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "p\n", + "\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "p\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "!p\n", + "❶\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "acd\n", + "\n", + "min even\n", + "\n", + "\n", + "0\n", + "\n", + "SCC #0\n", + "T: 1-6\n", + "{0,1}\n", + "Q: 0-2\n", + "lvl: 0\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "T: 1,2,4,6\n", + "{0}\n", + "Q: 0-2\n", + "lvl: 1\n", + "<1>\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "T: 2-6\n", + "{1}\n", + "Q: 0-2\n", + "lvl: 1\n", + "<2>\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + " >" + ] + }, + "execution_count": 47, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "spot.acd(a4, spot.acd_options_ORDER_HEURISTIC)" + ] + }, + { + "cell_type": "code", + "execution_count": 48, + "id": "1a68f96a", + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0#1\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!p\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1#1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "p\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "1#2\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!p\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "2#1\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "p\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!p\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "2#2\n", + "\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "p\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "p\n", + "\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "!p\n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "!p\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "0#2\n", + "\n", + "\n", + "\n", + "4->5\n", + "\n", + "\n", + "p\n", + "\n", + "\n", + "\n", + "5->2\n", + "\n", + "\n", + "p\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "0#0\n", + "\n", + "\n", + "\n", + "5->6\n", + "\n", + "\n", + "!p\n", + "\n", + "\n", + "\n", + "6->0\n", + "\n", + "\n", + "!p\n", + "\n", + "\n", + "\n", + "6->1\n", + "\n", + "\n", + "p\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f0c480e0de0> >" + ] + }, + "execution_count": 48, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "s4b = spot.acd_transform_sbacc(a4)\n", + "s4b.copy_state_names_from(a4)\n", + "s4b" + ] + }, { "cell_type": "markdown", "id": "15f094c0", @@ -7638,7 +8636,7 @@ }, { "cell_type": "code", - "execution_count": 45, + "execution_count": 49, "id": "criminal-northwest", "metadata": {}, "outputs": [ @@ -7764,10 +8762,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f296c18e210> >" + " *' at 0x7f0c480e21e0> >" ] }, - "execution_count": 45, + "execution_count": 49, "metadata": {}, "output_type": "execute_result" } @@ -7798,7 +8796,7 @@ }, { "cell_type": "code", - "execution_count": 46, + "execution_count": 50, "id": "63c7c062", "metadata": {}, "outputs": [ @@ -7876,10 +8874,10 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, - "execution_count": 46, + "execution_count": 50, "metadata": {}, "output_type": "execute_result" } @@ -7890,7 +8888,7 @@ }, { "cell_type": "code", - "execution_count": 47, + "execution_count": 51, "id": "balanced-investing", "metadata": {}, "outputs": [ @@ -8042,10 +9040,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f296c18e030> >" + " *' at 0x7f0c480e2360> >" ] }, - "execution_count": 47, + "execution_count": 51, "metadata": {}, "output_type": "execute_result" } @@ -8056,7 +9054,7 @@ }, { "cell_type": "code", - "execution_count": 48, + "execution_count": 52, "id": "nutritional-rugby", "metadata": {}, "outputs": [], @@ -8066,7 +9064,7 @@ }, { "cell_type": "code", - "execution_count": 49, + "execution_count": 53, "id": "criminal-marking", "metadata": {}, "outputs": [ @@ -8129,7 +9127,7 @@ "\n", "\n", - "\n", + "\n", "\n", "(Fin(\n", "⓿\n", @@ -8152,7 +9150,7 @@ "0\n", "\n", "\n", - "\n", + "\n", "I->0\n", "\n", "\n", @@ -8270,7 +9268,7 @@ "\n", "\n", - "\n", + "\n", "acd\n", "\n", "min even\n", @@ -8298,7 +9296,7 @@ "<1>\n", "\n", "\n", - "\n", + "\n", "0->1\n", "\n", "\n", @@ -8306,39 +9304,39 @@ "\n", "\n", "" + " $(\"#acd4 #N\" + node).addClass(\"acdbold acdhigh\");\n", + "};$(\"#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": 49, + "execution_count": 53, "metadata": {}, "output_type": "execute_result" } @@ -8349,7 +9347,7 @@ }, { "cell_type": "code", - "execution_count": 50, + "execution_count": 54, "id": "e7760d51", "metadata": {}, "outputs": [ @@ -8359,7 +9357,7 @@ "0" ] }, - "execution_count": 50, + "execution_count": 54, "metadata": {}, "output_type": "execute_result" } @@ -8370,7 +9368,7 @@ }, { "cell_type": "code", - "execution_count": 51, + "execution_count": 55, "id": "unusual-dependence", "metadata": { "scrolled": true @@ -8479,10 +9477,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f296c193240> >" + " *' at 0x7f0c480e2d50> >" ] }, - "execution_count": 51, + "execution_count": 55, "metadata": {}, "output_type": "execute_result" } @@ -8493,7 +9491,7 @@ }, { "cell_type": "code", - "execution_count": 52, + "execution_count": 56, "id": "d5440de1", "metadata": {}, "outputs": [ @@ -8626,10 +9624,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f296c1934b0> >" + " *' at 0x7f0c480ea150> >" ] }, - "execution_count": 52, + "execution_count": 56, "metadata": {}, "output_type": "execute_result" } @@ -8640,7 +9638,7 @@ }, { "cell_type": "code", - "execution_count": 53, + "execution_count": 57, "id": "9ed0bc59", "metadata": {}, "outputs": [], @@ -8660,7 +9658,7 @@ }, { "cell_type": "code", - "execution_count": 54, + "execution_count": 58, "id": "deb92971", "metadata": {}, "outputs": [ @@ -8739,7 +9737,7 @@ "\n", "\n", - "\n", + "\n", "\n", "Inf(\n", "⓿\n", @@ -8759,7 +9757,7 @@ "0\n", "\n", "\n", - "\n", + "\n", "I->0\n", "\n", "\n", @@ -8879,7 +9877,7 @@ "\n", "\n", - "\n", + "\n", "acd\n", "\n", "min even\n", @@ -8911,7 +9909,7 @@ "<1>\n", "\n", "\n", - "\n", + "\n", "0->1\n", "\n", "\n", @@ -8928,7 +9926,7 @@ "<2>\n", "\n", "\n", - "\n", + "\n", "0->2\n", "\n", "\n", @@ -8936,39 +9934,39 @@ "\n", "\n", "" + " $(\"#acd5 #N\" + node).addClass(\"acdbold acdhigh\");\n", + "};$(\"#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": 54, + "execution_count": 58, "metadata": {}, "output_type": "execute_result" } @@ -8986,7 +9984,7 @@ }, { "cell_type": "code", - "execution_count": 55, + "execution_count": 59, "id": "94a02201", "metadata": {}, "outputs": [ @@ -9093,10 +10091,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f296c193b70> >" + " *' at 0x7f0c480e2300> >" ] }, - "execution_count": 55, + "execution_count": 59, "metadata": {}, "output_type": "execute_result" } @@ -9107,7 +10105,7 @@ }, { "cell_type": "code", - "execution_count": 56, + "execution_count": 60, "id": "d484ba8f", "metadata": {}, "outputs": [ @@ -9223,10 +10221,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f296c198330> >" + " *' at 0x7f0c480f0420> >" ] }, - "execution_count": 56, + "execution_count": 60, "metadata": {}, "output_type": "execute_result" } @@ -9237,7 +10235,7 @@ }, { "cell_type": "code", - "execution_count": 57, + "execution_count": 61, "id": "3332e850", "metadata": {}, "outputs": [ @@ -9503,10 +10501,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f296c1984e0> >" + " *' at 0x7f0c480f0840> >" ] }, - "execution_count": 57, + "execution_count": 61, "metadata": {}, "output_type": "execute_result" } @@ -9527,7 +10525,7 @@ }, { "cell_type": "code", - "execution_count": 58, + "execution_count": 62, "id": "german-vienna", "metadata": {}, "outputs": [ @@ -9597,10 +10595,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f296c198cf0> >" + " *' at 0x7f0c480f30c0> >" ] }, - "execution_count": 58, + "execution_count": 62, "metadata": {}, "output_type": "execute_result" } @@ -9624,7 +10622,7 @@ }, { "cell_type": "code", - "execution_count": 59, + "execution_count": 63, "id": "chemical-primary", "metadata": {}, "outputs": [ @@ -9634,7 +10632,7 @@ "(spot.trival_maybe(), spot.trival(True))" ] }, - "execution_count": 59, + "execution_count": 63, "metadata": {}, "output_type": "execute_result" } @@ -9645,7 +10643,7 @@ }, { "cell_type": "code", - "execution_count": 60, + "execution_count": 64, "id": "hispanic-floor", "metadata": {}, "outputs": [ @@ -9708,10 +10706,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f296c19e120> >" + " *' at 0x7f0c480f3210> >" ] }, - "execution_count": 60, + "execution_count": 64, "metadata": {}, "output_type": "execute_result" } @@ -9722,7 +10720,7 @@ }, { "cell_type": "code", - "execution_count": 61, + "execution_count": 65, "id": "central-london", "metadata": {}, "outputs": [ @@ -9732,7 +10730,7 @@ "(spot.trival(True), spot.trival(True))" ] }, - "execution_count": 61, + "execution_count": 65, "metadata": {}, "output_type": "execute_result" }