From 170d839c4baa9d5402f8feb6a8e5e1b41e0c2fbe Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 5 Sep 2021 16:56:54 +0200 Subject: [PATCH] acd: remove redundant nodes Reported by Florian Renkin. * spot/twaalgos/zlktree.cc (acd::_build): Use a sorted list to remove redundant children, has done in zielonka_tree. * tests/python/zlktree.ipynb: Add Florian's test case. * tests/python/toparity.py: Adjust, and revert some tests uncommented by mistake in a previous patch. --- spot/twaalgos/zlktree.cc | 65 +- tests/python/toparity.py | 14 +- tests/python/zlktree.ipynb | 2492 +++++++++++++++++++++++------------- 3 files changed, 1679 insertions(+), 892 deletions(-) diff --git a/spot/twaalgos/zlktree.cc b/spot/twaalgos/zlktree.cc index 105bfe19d..c31ec1509 100644 --- a/spot/twaalgos/zlktree.cc +++ b/spot/twaalgos/zlktree.cc @@ -20,9 +20,11 @@ #include "config.h" #include #include +#include #include #include #include +#include namespace spot { @@ -405,6 +407,13 @@ namespace spot } } + struct size_model + { + unsigned size; + std::unique_ptr trans; + }; + std::vector out; + // This loop is a BFS over the increasing set of nodes. for (unsigned node = 0; node < nodes_.size(); ++node) { @@ -412,26 +421,60 @@ namespace spot unsigned lvl = nodes_[node].level; bool accepting_node = (lvl & 1) != trees_[scc].is_even; + out.clear(); auto callback = [&](scc_info si, unsigned siscc) { - unsigned vnum = trees_[scc].num_nodes++; - allocate_vectors_maybe(vnum); - nodes_.emplace_back(edge_vector(vnum), state_vector(vnum)); - auto& n = nodes_.back(); - n.parent = node; - n.level = lvl + 1; - n.scc = scc; + bitvect* bv = make_bitvect(nedges); + unsigned sz = 0; for (auto& e: si.inner_edges_of(siscc)) { - n.edges[aut->edge_number(e)] = true; - n.states[e.src] = true; + bv->set(aut->edge_number(e)); + ++sz; } + auto iter = out.begin(); + while (iter != out.end()) + { + if (iter->size < sz) + // We have checked all larger models. + break; + if (bv->is_subset_of(*iter->trans)) + // ignore smaller models + { + delete bv; + return; + } + ++iter; + } + // insert the model + iter = out.insert(iter, {sz, std::unique_ptr(bv)}); + ++iter; + // erase all models it contains + out.erase(std::remove_if(iter, out.end(), + [&](auto& mod) { + return mod.trans->is_subset_of(*bv); + }), out.end()); }; - - unsigned before_size = nodes_.size(); maximal_accepting_loops_for_scc(*si_, scc, accepting_node ? negacc : posacc, nodes_[node].edges, callback); + + unsigned before_size = nodes_.size(); + for (const auto& [sz, bv]: out) + { + unsigned vnum = trees_[scc].num_nodes++; + allocate_vectors_maybe(vnum); + nodes_.emplace_back(edge_vector(vnum), state_vector(vnum)); + auto& n = nodes_.back(); + n.parent = node; + n.level = lvl + 1; + n.scc = scc; + for (unsigned e = 1; e < nedges; ++e) + if (bv->get(e)) + { + n.edges[e] = true; + n.states[aut->edge_storage(e).src] = true; + } + } unsigned after_size = nodes_.size(); unsigned children = after_size - before_size; diff --git a/tests/python/toparity.py b/tests/python/toparity.py index 8729da7b1..df226ebe4 100644 --- a/tests/python/toparity.py +++ b/tests/python/toparity.py @@ -116,7 +116,7 @@ def test(aut, expected_num_states=[], full=True): spot.reduce_parity_here(p1) assert spot.are_equivalent(aut, p1) if expected_num is not None: - print(p1.num_states(), expected_num) + # print(p1.num_states(), expected_num) assert p1.num_states() == expected_num if full and opt is not None: # Make sure passing opt is the same as setting @@ -240,11 +240,11 @@ State: 1 [!0&!1] 0 {1 2} --END--"""), [9, 3, 2, 3, 3, 3, 2, 2]) -#for i,f in enumerate(spot.randltl(10, 400)): -# test(spot.translate(f, "det", "G"), full=(i<100)) -# -#for f in spot.randltl(5, 2500): -# test(spot.translate(f), full=False) +for i,f in enumerate(spot.randltl(10, 200)): + test(spot.translate(f, "det", "G"), full=(i<50)) + +for f in spot.randltl(5, 500): + test(spot.translate(f), full=False) test(spot.automaton(""" @@ -278,7 +278,7 @@ State: 3 [!0&1] 2 {1 4} [0&1] 3 {0} --END-- -"""), [80, 47, 104, 104, 102, 29, 6, 6]) +"""), [80, 47, 104, 104, 102, 29, 6, 5]) test(spot.automaton(""" HOA: v1 diff --git a/tests/python/zlktree.ipynb b/tests/python/zlktree.ipynb index 9e4f7f637..c3b636caa 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 0x7fa2681f9db0> >" + " *' at 0x7f5114a4ec00> >" ] }, "execution_count": 10, @@ -1063,7 +1063,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa2681f96f0> >" + " *' at 0x7f5114a4ea20> >" ] }, "execution_count": 11, @@ -1256,7 +1256,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa2681f98d0> >" + " *' at 0x7f5114a4ef60> >" ] }, "execution_count": 13, @@ -1701,7 +1701,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa268204300> >" + " *' at 0x7f5114a4e8d0> >" ] }, "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": {}, @@ -2776,21 +2776,21 @@ "\n", "\n", - "\n", + "\n", "\n", "acd\n", - "\n", - "min odd\n", + "\n", + "min odd\n", "\n", "\n", "0\n", - "\n", - "SCC #0\n", - "T: 9-16,21-28,33-36\n", - "{1,2,3,4,5}\n", - "Q: 2,3,5,6,8\n", - "lvl: 0\n", + "\n", + "SCC #0\n", + "T: 9-16,21-28,33-36\n", + "{1,2,3,4,5}\n", + "Q: 2,3,5,6,8\n", + "lvl: 0\n", "\n", "\n", "\n", @@ -2805,8 +2805,8 @@ "\n", "\n", "0->4\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", @@ -2820,54 +2820,54 @@ "\n", "\n", "0->5\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "6\n", - "\n", - "T: 14,16,26\n", - "{1,2,3,5}\n", - "Q: 3,6\n", - "lvl: 1\n", + "\n", + "T: 14,15,22,23\n", + "{1,2,3,4}\n", + "Q: 3,5\n", + "lvl: 1\n", "\n", "\n", "\n", "0->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "7\n", - "\n", - "T: 9\n", - "{1,2,3,5}\n", - "Q: 2\n", - "lvl: 1\n", - "<7>\n", + "\n", + "T: 14,16,26\n", + "{1,2,3,5}\n", + "Q: 3,6\n", + "lvl: 1\n", "\n", "\n", "\n", "0->7\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "8\n", - "\n", - "T: 14,15,22,23\n", - "{1,2,3,4}\n", - "Q: 3,5\n", - "lvl: 1\n", + "\n", + "T: 9\n", + "{1,2,3,5}\n", + "Q: 2\n", + "lvl: 1\n", + "<8>\n", "\n", "\n", "\n", "0->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", @@ -2888,113 +2888,113 @@ "\n", "\n", "12\n", - "\n", - "T: 14\n", - "{1,3}\n", - "Q: 3\n", - "lvl: 2\n", - "<12>\n", + "\n", + "T: 14\n", + "{1,3}\n", + "Q: 3\n", + "lvl: 2\n", + "<12>\n", "\n", "\n", "\n", "6->12\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "13\n", - "\n", - "T: 14\n", - "{1,3}\n", - "Q: 3\n", - "lvl: 2\n", - "<13>\n", + "\n", + "T: 23\n", + "{1,3}\n", + "Q: 5\n", + "lvl: 2\n", + "<13>\n", "\n", - "\n", + "\n", "\n", - "8->13\n", - "\n", - "\n", + "6->13\n", + "\n", + "\n", "\n", "\n", "\n", "14\n", - "\n", - "T: 23\n", - "{1,3}\n", - "Q: 5\n", - "lvl: 2\n", - "<14>\n", + "\n", + "T: 14\n", + "{1,3}\n", + "Q: 3\n", + "lvl: 2\n", + "<14>\n", "\n", - "\n", + "\n", "\n", - "8->14\n", - "\n", - "\n", + "7->14\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "SCC #1\n", - "T: 31,32,39,40\n", - "{0,1,2,3,5}\n", - "Q: 7,9\n", - "lvl: 1\n", + "\n", + "SCC #1\n", + "T: 31,32,39,40\n", + "{0,1,2,3,5}\n", + "Q: 7,9\n", + "lvl: 1\n", "\n", "\n", "\n", "9\n", - "\n", - "T: 40\n", - "{1,3}\n", - "Q: 9\n", - "lvl: 2\n", - "<9>\n", + "\n", + "T: 40\n", + "{1,3}\n", + "Q: 9\n", + "lvl: 2\n", + "<9>\n", "\n", "\n", "\n", "1->9\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "SCC #2\n", - "T: 5,7,17\n", - "{0,1,2,3,5}\n", - "Q: 1,4\n", - "lvl: 1\n", + "\n", + "SCC #2\n", + "T: 5,7,17\n", + "{0,1,2,3,5}\n", + "Q: 1,4\n", + "lvl: 1\n", "\n", "\n", "\n", "10\n", - "\n", - "T: 5\n", - "{1,3}\n", - "Q: 1\n", - "lvl: 2\n", - "<10>\n", + "\n", + "T: 5\n", + "{1,3}\n", + "Q: 1\n", + "lvl: 2\n", + "<10>\n", "\n", "\n", "\n", "2->10\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "3\n", - "\n", - "SCC #3\n", - "T: 1\n", - "{0,1,2,3,5}\n", - "Q: 0\n", - "lvl: 1\n", - "<3>\n", + "\n", + "SCC #3\n", + "T: 1\n", + "{0,1,2,3,5}\n", + "Q: 0\n", + "lvl: 1\n", + "<3>\n", "\n", "\n", "\n" @@ -3584,12 +3584,12 @@ "\n", "\n", - "\n", + "\n", "\n", "acd\n", - "\n", - "min odd\n", + "\n", + "min odd\n", "\n", "\n", "0\n", - "\n", - "SCC #0\n", - "T: 9-16,21-28,33-36\n", - "{1,2,3,4,5}\n", - "Q: 2,3,5,6,8\n", - "lvl: 0\n", + "\n", + "SCC #0\n", + "T: 9-16,21-28,33-36\n", + "{1,2,3,4,5}\n", + "Q: 2,3,5,6,8\n", + "lvl: 0\n", "\n", "\n", "\n", "\n", "0->4\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "\n", "0->5\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "6\n", - "\n", - "T: 14,16,26\n", - "{1,2,3,5}\n", - "Q: 3,6\n", - "lvl: 1\n", + "\n", + "T: 14,15,22,23\n", + "{1,2,3,4}\n", + "Q: 3,5\n", + "lvl: 1\n", "\n", "\n", "\n", "0->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", - "\n", "7\n", - "\n", - "T: 9\n", - "{1,2,3,5}\n", - "Q: 2\n", - "lvl: 1\n", - "<7>\n", + "\n", + "T: 14,16,26\n", + "{1,2,3,5}\n", + "Q: 3,6\n", + "lvl: 1\n", "\n", "\n", "\n", "0->7\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", - "\n", "8\n", - "\n", - "T: 14,15,22,23\n", - "{1,2,3,4}\n", - "Q: 3,5\n", - "lvl: 1\n", + "\n", + "T: 9\n", + "{1,2,3,5}\n", + "Q: 2\n", + "lvl: 1\n", + "<8>\n", "\n", "\n", "\n", "0->8\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: 14\n", + "{1,3}\n", + "Q: 3\n", + "lvl: 2\n", + "<12>\n", "\n", "\n", "\n", "6->12\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", - "\n", "13\n", - "\n", - "T: 14\n", - "{1,3}\n", - "Q: 3\n", - "lvl: 2\n", - "<13>\n", + "\n", + "T: 23\n", + "{1,3}\n", + "Q: 5\n", + "lvl: 2\n", + "<13>\n", "\n", - "\n", + "\n", "\n", - "8->13\n", - "\n", - "\n", + "6->13\n", + "\n", + "\n", "\n", "\n", - "\n", "14\n", - "\n", - "T: 23\n", - "{1,3}\n", - "Q: 5\n", - "lvl: 2\n", - "<14>\n", + "\n", + "T: 14\n", + "{1,3}\n", + "Q: 3\n", + "lvl: 2\n", + "<14>\n", "\n", - "\n", + "\n", "\n", - "8->14\n", - "\n", - "\n", + "7->14\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "SCC #1\n", - "T: 31,32,39,40\n", - "{0,1,2,3,5}\n", - "Q: 7,9\n", - "lvl: 1\n", + "\n", + "SCC #1\n", + "T: 31,32,39,40\n", + "{0,1,2,3,5}\n", + "Q: 7,9\n", + "lvl: 1\n", "\n", "\n", "\n", "9\n", - "\n", - "T: 40\n", - "{1,3}\n", - "Q: 9\n", - "lvl: 2\n", - "<9>\n", + "\n", + "T: 40\n", + "{1,3}\n", + "Q: 9\n", + "lvl: 2\n", + "<9>\n", "\n", "\n", "\n", "1->9\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "SCC #2\n", - "T: 5,7,17\n", - "{0,1,2,3,5}\n", - "Q: 1,4\n", - "lvl: 1\n", + "\n", + "SCC #2\n", + "T: 5,7,17\n", + "{0,1,2,3,5}\n", + "Q: 1,4\n", + "lvl: 1\n", "\n", "\n", "\n", "10\n", - "\n", - "T: 5\n", - "{1,3}\n", - "Q: 1\n", - "lvl: 2\n", - "<10>\n", + "\n", + "T: 5\n", + "{1,3}\n", + "Q: 1\n", + "lvl: 2\n", + "<10>\n", "\n", "\n", "\n", "2->10\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "3\n", - "\n", - "SCC #3\n", - "T: 1\n", - "{0,1,2,3,5}\n", - "Q: 0\n", - "lvl: 1\n", - "<3>\n", + "\n", + "SCC #3\n", + "T: 1\n", + "{0,1,2,3,5}\n", + "Q: 0\n", + "lvl: 1\n", + "<3>\n", "\n", "\n", "\n", @@ -3859,10 +3859,10 @@ " ? \"acdacc acdbold\"\n", " : \"acdrej acdbold\");\n", " $(\"#acd0 #N\" + node).addClass(\"acdbold acdhigh\");\n", - "};$(\"#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 #E16\").addClass(\"acdN6\");$(\"#acdaut0 #E26\").addClass(\"acdN6\");$(\"#acdaut0 #E9\").addClass(\"acdN7\");$(\"#acdaut0 #E14\").addClass(\"acdN8\");$(\"#acdaut0 #E15\").addClass(\"acdN8\");$(\"#acdaut0 #E22\").addClass(\"acdN8\");$(\"#acdaut0 #E23\").addClass(\"acdN8\");$(\"#acdaut0 #E40\").addClass(\"acdN9\");$(\"#acdaut0 #E5\").addClass(\"acdN10\");$(\"#acdaut0 #E23\").addClass(\"acdN11\");$(\"#acdaut0 #E14\").addClass(\"acdN12\");$(\"#acdaut0 #E14\").addClass(\"acdN13\");$(\"#acdaut0 #E23\").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);});" + "};$(\"#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, @@ -3879,7 +3879,7 @@ "id": "0f2f00c4", "metadata": {}, "source": [ - "The nodes of the ACD represent various bits of informations. First, the root of each tree shows the number of the maximal SCC (as computed by `spot.scc_info`). Trivial maximal SCCs (without cycles) are omitted from the construction.\n", + "The nodes of the ACD represent various bits of informations. First, the root of each tree shows the number of the maximal SCC (as computed by `spot.scc_info`). Trivial maximal SCCs (without cycles) are omitted from the construction. Children are sorted by decreasing size of the SCCs they represent (i.e., decreasing count of edges).\n", "\n", "The numbers after `T:` list the edges that belong to the strongly connected component. The numbers are simply the indices of those edges in the automaton. Between braces are the colors covered by all those edges, to decide if a cycle formed by all these edges would be accepting. The numbers after `Q:` are the states touched by those edges. `lvl:` indicates the level of each node. Since some trees can have accepting roots while others have rejecting roots, the levels of some tree have been shifted down (i.e., the root start at levl 1 instead of 0) to ensure that all trees use the same parity. The parity of the decomposition (i.e., whether even levels are accepting) is indicated by the `is_even()` method." ] @@ -4012,7 +4012,7 @@ { "data": { "text/plain": [ - "(7, 0)" + "(8, 0)" ] }, "execution_count": 23, @@ -4033,7 +4033,7 @@ { "data": { "text/plain": [ - "(13, 0)" + "(4, 0)" ] }, "execution_count": 24, @@ -4054,7 +4054,7 @@ { "data": { "text/plain": [ - "(4, 0)" + "(8, 0)" ] }, "execution_count": 25, @@ -4142,600 +4142,600 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Fin(\n", - "⓿\n", - ") & (Inf(\n", - "❶\n", - ") | Fin(\n", - "❷\n", - "))\n", - "[parity min odd 3]\n", + "\n", + "\n", + "\n", + "Fin(\n", + "⓿\n", + ") & (Inf(\n", + "❶\n", + ") | Fin(\n", + "❷\n", + "))\n", + "[parity min odd 3]\n", "\n", "\n", "\n", "0\n", - "\n", - "0#3\n", + "\n", + "0#3\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!p0 & !p1\n", - "❶\n", + "\n", + "\n", + "!p0 & !p1\n", + "❶\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", + "\n", + "!p0 & p1\n", + "⓿\n", "\n", "\n", "\n", "2\n", - "\n", - "2#4\n", + "\n", + "2#4\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "p0 & !p1\n", - "⓿\n", + "\n", + "\n", + "p0 & !p1\n", + "⓿\n", "\n", "\n", "\n", "3\n", - "\n", - "3#4\n", + "\n", + "3#4\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "p0 & p1\n", - "⓿\n", + "\n", + "\n", + "p0 & p1\n", + "⓿\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!p0 & p1\n", - "❷\n", + "\n", + "\n", + "!p0 & p1\n", + "❷\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "p0 & !p1\n", - "⓿\n", + "\n", + "\n", + "p0 & !p1\n", + "⓿\n", "\n", "\n", "\n", "4\n", - "\n", - "4#2\n", + "\n", + "4#2\n", "\n", "\n", "\n", "1->4\n", - "\n", - "\n", - "!p0 & !p1\n", - "❶\n", + "\n", + "\n", + "!p0 & !p1\n", + "❶\n", "\n", "\n", "\n", "5\n", - "\n", - "5#4\n", + "\n", + "5#4\n", "\n", "\n", "\n", "1->5\n", - "\n", - "\n", - "p0 & p1\n", - "⓿\n", + "\n", + "\n", + "p0 & p1\n", + "⓿\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "p0 & !p1\n", - "❶\n", + "\n", + "\n", + "p0 & !p1\n", + "❶\n", "\n", "\n", "\n", "2->3\n", - "\n", - "\n", - "p0 & p1\n", - "❶\n", + "\n", + "\n", + "p0 & p1\n", + "❶\n", "\n", "\n", "\n", "6\n", - "\n", - "2#7\n", + "\n", + "2#8\n", "\n", "\n", "\n", "2->6\n", - "\n", - "\n", - "!p0 & !p1\n", - "⓿\n", + "\n", + "\n", + "!p0 & !p1\n", + "⓿\n", "\n", "\n", "\n", "7\n", - "\n", - "3#12\n", + "\n", + "3#12\n", "\n", "\n", "\n", "2->7\n", - "\n", - "\n", - "!p0 & p1\n", - "⓿\n", + "\n", + "\n", + "!p0 & p1\n", + "⓿\n", "\n", "\n", "\n", "3->2\n", - "\n", - "\n", - "p0 & !p1\n", - "❶\n", + "\n", + "\n", + "p0 & !p1\n", + "❶\n", "\n", "\n", "\n", "3->5\n", - "\n", - "\n", - "p0 & p1\n", - "❶\n", + "\n", + "\n", + "p0 & p1\n", + "❶\n", "\n", "\n", "\n", "3->7\n", - "\n", - "\n", - "!p0 & p1\n", - "⓿\n", + "\n", + "\n", + "!p0 & p1\n", + "⓿\n", "\n", "\n", "\n", "8\n", - "\n", - "6#6\n", + "\n", + "6#7\n", "\n", "\n", "\n", "3->8\n", - "\n", - "\n", - "!p0 & !p1\n", - "⓿\n", + "\n", + "\n", + "!p0 & !p1\n", + "⓿\n", "\n", "\n", "\n", "4->1\n", - "\n", - "\n", - "!p0 & p1\n", - "❶\n", + "\n", + "\n", + "!p0 & p1\n", + "❶\n", "\n", "\n", "\n", "4->2\n", - "\n", - "\n", - "p0 & !p1\n", - "⓿\n", + "\n", + "\n", + "p0 & !p1\n", + "⓿\n", "\n", "\n", "\n", "4->3\n", - "\n", - "\n", - "p0 & p1\n", - "⓿\n", + "\n", + "\n", + "p0 & p1\n", + "⓿\n", "\n", "\n", "\n", "9\n", - "\n", - "7#1\n", + "\n", + "7#1\n", "\n", "\n", "\n", "4->9\n", - "\n", - "\n", - "!p0 & !p1\n", - "⓿\n", + "\n", + "\n", + "!p0 & !p1\n", + "⓿\n", "\n", "\n", "\n", "5->2\n", - "\n", - "\n", - "p0 & !p1\n", - "❶\n", + "\n", + "\n", + "p0 & !p1\n", + "❶\n", "\n", "\n", "\n", "5->3\n", - "\n", - "\n", - "p0 & p1\n", - "❶\n", + "\n", + "\n", + "p0 & p1\n", + "❶\n", "\n", "\n", "\n", "10\n", - "\n", - "5#11\n", + "\n", + "5#11\n", "\n", "\n", "\n", "5->10\n", - "\n", - "\n", - "!p0 & p1\n", - "⓿\n", + "\n", + "\n", + "!p0 & p1\n", + "⓿\n", "\n", "\n", "\n", "11\n", - "\n", - "8#5\n", + "\n", + "8#5\n", "\n", "\n", "\n", "5->11\n", - "\n", - "\n", - "!p0 & !p1\n", - "⓿\n", + "\n", + "\n", + "!p0 & !p1\n", + "⓿\n", "\n", "\n", "\n", "6->2\n", - "\n", - "\n", - "p0 & !p1\n", - "⓿\n", + "\n", + "\n", + "p0 & !p1\n", + "⓿\n", + "\n", + "\n", + "\n", + "6->3\n", + "\n", + "\n", + "!p0 & p1\n", + "⓿\n", + "\n", + "\n", + "\n", + "6->3\n", + "\n", + "\n", + "p0 & p1\n", + "⓿\n", "\n", "\n", "\n", "6->6\n", - "\n", - "\n", - "!p0 & !p1\n", - "❶\n", - "\n", - "\n", - "\n", - "12\n", - "\n", - "3#13\n", - "\n", - "\n", - "\n", - "6->12\n", - "\n", - "\n", - "!p0 & p1\n", - "⓿\n", - "\n", - "\n", - "\n", - "6->12\n", - "\n", - "\n", - "p0 & p1\n", - "⓿\n", + "\n", + "\n", + "!p0 & !p1\n", + "❶\n", "\n", "\n", "\n", "7->6\n", - "\n", - "\n", - "p0 & !p1\n", - "⓿\n", + "\n", + "\n", + "p0 & !p1\n", + "⓿\n", "\n", "\n", "\n", "7->7\n", - "\n", - "\n", - "!p0 & p1\n", - "❷\n", + "\n", + "\n", + "!p0 & p1\n", + "❷\n", "\n", "\n", "\n", "7->8\n", - "\n", - "\n", - "!p0 & !p1\n", - "❶\n", + "\n", + "\n", + "!p0 & !p1\n", + "⓿\n", "\n", - "\n", - "\n", - "13\n", - "\n", - "5#14\n", + "\n", + "\n", + "12\n", + "\n", + "5#13\n", "\n", - "\n", + "\n", "\n", - "7->13\n", - "\n", - "\n", - "p0 & p1\n", - "⓿\n", + "7->12\n", + "\n", + "\n", + "p0 & p1\n", + "❶\n", + "\n", + "\n", + "\n", + "8->3\n", + "\n", + "\n", + "p0 & p1\n", + "⓿\n", "\n", "\n", "\n", "8->6\n", - "\n", - "\n", - "p0 & !p1\n", - "⓿\n", - "\n", - "\n", - "\n", - "8->7\n", - "\n", - "\n", - "!p0 & p1\n", - "❶\n", + "\n", + "\n", + "p0 & !p1\n", + "⓿\n", "\n", "\n", "\n", "8->11\n", - "\n", - "\n", - "!p0 & !p1\n", - "⓿\n", + "\n", + "\n", + "!p0 & !p1\n", + "⓿\n", "\n", - "\n", - "\n", - "8->12\n", - "\n", - "\n", - "p0 & p1\n", - "⓿\n", + "\n", + "\n", + "13\n", + "\n", + "3#14\n", + "\n", + "\n", + "\n", + "8->13\n", + "\n", + "\n", + "!p0 & p1\n", + "❶\n", "\n", "\n", "\n", "9->2\n", - "\n", - "\n", - "p0 & !p1\n", - "⓿\n", + "\n", + "\n", + "p0 & !p1\n", + "⓿\n", "\n", "\n", "\n", "9->5\n", - "\n", - "\n", - "p0 & p1\n", - "⓿\n", + "\n", + "\n", + "p0 & p1\n", + "⓿\n", "\n", "\n", "\n", "9->9\n", - "\n", - "\n", - "!p0 & !p1\n", - "❶\n", + "\n", + "\n", + "!p0 & !p1\n", + "❶\n", "\n", "\n", "\n", "14\n", - "\n", - "9#9\n", + "\n", + "9#9\n", "\n", "\n", "\n", "9->14\n", - "\n", - "\n", - "!p0 & p1\n", - "❶\n", + "\n", + "\n", + "!p0 & p1\n", + "❶\n", "\n", "\n", "\n", "10->6\n", - "\n", - "\n", - "p0 & !p1\n", - "⓿\n", + "\n", + "\n", + "p0 & !p1\n", + "⓿\n", "\n", "\n", "\n", "10->7\n", - "\n", - "\n", - "p0 & p1\n", - "⓿\n", + "\n", + "\n", + "p0 & p1\n", + "⓿\n", "\n", "\n", "\n", "10->10\n", - "\n", - "\n", - "!p0 & p1\n", - "❷\n", + "\n", + "\n", + "!p0 & p1\n", + "❷\n", "\n", "\n", "\n", "10->11\n", - "\n", - "\n", - "!p0 & !p1\n", - "❶\n", + "\n", + "\n", + "!p0 & !p1\n", + "❶\n", "\n", "\n", "\n", "11->6\n", - "\n", - "\n", - "p0 & !p1\n", - "⓿\n", + "\n", + "\n", + "p0 & !p1\n", + "⓿\n", "\n", "\n", "\n", "11->10\n", - "\n", - "\n", - "!p0 & p1\n", - "❶\n", + "\n", + "\n", + "!p0 & p1\n", + "❶\n", "\n", "\n", "\n", "11->11\n", - "\n", - "\n", - "!p0 & !p1\n", - "❶\n", + "\n", + "\n", + "!p0 & !p1\n", + "❶\n", "\n", - "\n", + "\n", "\n", - "11->13\n", - "\n", - "\n", - "p0 & p1\n", - "⓿\n", + "11->12\n", + "\n", + "\n", + "p0 & p1\n", + "⓿\n", "\n", - "\n", + "\n", "\n", - "12->2\n", - "\n", - "\n", - "p0 & !p1\n", - "⓿\n", + "12->6\n", + "\n", + "\n", + "p0 & !p1\n", + "⓿\n", "\n", - "\n", + "\n", + "\n", + "12->7\n", + "\n", + "\n", + "p0 & p1\n", + "❶\n", + "\n", + "\n", "\n", - "12->8\n", - "\n", - "\n", - "!p0 & !p1\n", - "⓿\n", + "12->11\n", + "\n", + "\n", + "!p0 & !p1\n", + "⓿\n", "\n", "\n", - "\n", - "12->12\n", - "\n", - "\n", - "!p0 & p1\n", - "❷\n", - "\n", - "\n", "\n", - "12->13\n", - "\n", - "\n", - "p0 & p1\n", - "❶\n", + "12->12\n", + "\n", + "\n", + "!p0 & p1\n", + "❷\n", "\n", - "\n", + "\n", + "\n", + "13->5\n", + "\n", + "\n", + "p0 & p1\n", + "⓿\n", + "\n", + "\n", "\n", - "13->2\n", - "\n", - "\n", - "p0 & !p1\n", - "⓿\n", + "13->6\n", + "\n", + "\n", + "p0 & !p1\n", + "⓿\n", "\n", - "\n", + "\n", "\n", - "13->11\n", - "\n", - "\n", - "!p0 & !p1\n", - "⓿\n", - "\n", - "\n", - "\n", - "13->12\n", - "\n", - "\n", - "p0 & p1\n", - "❶\n", + "13->8\n", + "\n", + "\n", + "!p0 & !p1\n", + "❶\n", "\n", "\n", - "\n", + "\n", "13->13\n", - "\n", - "\n", - "!p0 & p1\n", - "❷\n", + "\n", + "\n", + "!p0 & p1\n", + "❷\n", "\n", "\n", "\n", "14->2\n", - "\n", - "\n", - "p0 & !p1\n", - "⓿\n", + "\n", + "\n", + "p0 & !p1\n", + "⓿\n", "\n", "\n", "\n", "14->3\n", - "\n", - "\n", - "p0 & p1\n", - "⓿\n", + "\n", + "\n", + "p0 & p1\n", + "⓿\n", "\n", "\n", "\n", "14->9\n", - "\n", - "\n", - "!p0 & !p1\n", - "❶\n", + "\n", + "\n", + "!p0 & !p1\n", + "❶\n", "\n", "\n", "\n", "14->14\n", - "\n", - "\n", - "!p0 & p1\n", - "❷\n", + "\n", + "\n", + "!p0 & p1\n", + "❷\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fa2681f9d20> >" + " *' at 0x7f5114a6a480> >" ] }, "execution_count": 27, @@ -4801,580 +4801,580 @@ "\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", + "0#3\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!p0 & !p1\n", - "❶\n", + "\n", + "\n", + "!p0 & !p1\n", + "❶\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", + "2#4\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", + "3#4\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", + "4#2\n", "\n", "\n", "\n", "1->4\n", - "\n", - "\n", - "!p0 & !p1\n", - "❶\n", + "\n", + "\n", + "!p0 & !p1\n", + "❶\n", "\n", "\n", "\n", "5\n", - "\n", - "5#4\n", + "\n", + "5#4\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", + "\n", + "p0 & !p1\n", + "❶\n", "\n", "\n", "\n", "2->3\n", - "\n", - "\n", - "p0 & p1\n", - "❶\n", + "\n", + "\n", + "p0 & p1\n", + "❶\n", "\n", "\n", "\n", "6\n", - "\n", - "2#7\n", + "\n", + "2#8\n", "\n", "\n", "\n", "2->6\n", - "\n", - "\n", - "!p0 & !p1\n", - "⓿\n", + "\n", + "\n", + "!p0 & !p1\n", + "⓿\n", "\n", "\n", "\n", "7\n", - "\n", - "3#12\n", + "\n", + "3#12\n", "\n", "\n", "\n", "2->7\n", - "\n", - "\n", - "!p0 & p1\n", - "⓿\n", + "\n", + "\n", + "!p0 & p1\n", + "⓿\n", "\n", "\n", "\n", "3->2\n", - "\n", - "\n", - "p0 & !p1\n", - "❶\n", + "\n", + "\n", + "p0 & !p1\n", + "❶\n", "\n", "\n", "\n", "3->5\n", - "\n", - "\n", - "p0 & p1\n", - "❶\n", + "\n", + "\n", + "p0 & p1\n", + "❶\n", "\n", "\n", "\n", "3->7\n", - "\n", - "\n", - "!p0 & p1\n", - "⓿\n", + "\n", + "\n", + "!p0 & p1\n", + "⓿\n", "\n", "\n", "\n", "8\n", - "\n", - "6#6\n", + "\n", + "6#7\n", "\n", "\n", "\n", "3->8\n", - "\n", - "\n", - "!p0 & !p1\n", - "⓿\n", + "\n", + "\n", + "!p0 & !p1\n", + "⓿\n", "\n", "\n", "\n", "4->1\n", - "\n", - "\n", - "!p0 & p1\n", - "❶\n", + "\n", + "\n", + "!p0 & p1\n", + "❶\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", + "7#1\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", + "\n", + "p0 & !p1\n", + "❶\n", "\n", "\n", "\n", "5->3\n", - "\n", - "\n", - "p0 & p1\n", - "❶\n", + "\n", + "\n", + "p0 & p1\n", + "❶\n", "\n", "\n", "\n", "10\n", - "\n", - "5#11\n", + "\n", + "5#11\n", "\n", "\n", "\n", "5->10\n", - "\n", - "\n", - "!p0 & p1\n", - "⓿\n", + "\n", + "\n", + "!p0 & p1\n", + "⓿\n", "\n", "\n", "\n", "11\n", - "\n", - "8#5\n", + "\n", + "8#5\n", "\n", "\n", "\n", "5->11\n", - "\n", - "\n", - "!p0 & !p1\n", - "⓿\n", + "\n", + "\n", + "!p0 & !p1\n", + "⓿\n", "\n", "\n", "\n", "6->2\n", - "\n", - "\n", - "p0 & !p1\n", - "⓿\n", + "\n", + "\n", + "p0 & !p1\n", + "⓿\n", + "\n", + "\n", + "\n", + "6->3\n", + "\n", + "\n", + "!p0 & p1\n", + "⓿\n", + "\n", + "\n", + "\n", + "6->3\n", + "\n", + "\n", + "p0 & p1\n", + "⓿\n", "\n", "\n", "\n", "6->6\n", - "\n", - "\n", - "!p0 & !p1\n", - "❶\n", - "\n", - "\n", - "\n", - "12\n", - "\n", - "3#13\n", - "\n", - "\n", - "\n", - "6->12\n", - "\n", - "\n", - "!p0 & p1\n", - "⓿\n", - "\n", - "\n", - "\n", - "6->12\n", - "\n", - "\n", - "p0 & p1\n", - "⓿\n", + "\n", + "\n", + "!p0 & !p1\n", + "❶\n", "\n", "\n", "\n", "7->6\n", - "\n", - "\n", - "p0 & !p1\n", - "⓿\n", + "\n", + "\n", + "p0 & !p1\n", + "⓿\n", "\n", "\n", "\n", "7->7\n", - "\n", - "\n", - "!p0 & p1\n", + "\n", + "\n", + "!p0 & p1\n", "\n", "\n", "\n", "7->8\n", - "\n", - "\n", - "!p0 & !p1\n", - "❶\n", + "\n", + "\n", + "!p0 & !p1\n", + "⓿\n", "\n", - "\n", - "\n", - "13\n", - "\n", - "5#14\n", + "\n", + "\n", + "12\n", + "\n", + "5#13\n", "\n", - "\n", + "\n", "\n", - "7->13\n", - "\n", - "\n", - "p0 & p1\n", - "⓿\n", + "7->12\n", + "\n", + "\n", + "p0 & p1\n", + "❶\n", + "\n", + "\n", + "\n", + "8->3\n", + "\n", + "\n", + "p0 & p1\n", + "⓿\n", "\n", "\n", "\n", "8->6\n", - "\n", - "\n", - "p0 & !p1\n", - "⓿\n", - "\n", - "\n", - "\n", - "8->7\n", - "\n", - "\n", - "!p0 & p1\n", - "❶\n", + "\n", + "\n", + "p0 & !p1\n", + "⓿\n", "\n", "\n", "\n", "8->11\n", - "\n", - "\n", - "!p0 & !p1\n", - "⓿\n", + "\n", + "\n", + "!p0 & !p1\n", + "⓿\n", "\n", - "\n", - "\n", - "8->12\n", - "\n", - "\n", - "p0 & p1\n", - "⓿\n", + "\n", + "\n", + "13\n", + "\n", + "3#14\n", + "\n", + "\n", + "\n", + "8->13\n", + "\n", + "\n", + "!p0 & p1\n", + "❶\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", + "\n", + "!p0 & !p1\n", + "❶\n", "\n", "\n", "\n", "14\n", - "\n", - "9#9\n", + "\n", + "9#9\n", "\n", "\n", "\n", "9->14\n", - "\n", - "\n", - "!p0 & p1\n", - "❶\n", + "\n", + "\n", + "!p0 & p1\n", + "❶\n", "\n", "\n", "\n", "10->6\n", - "\n", - "\n", - "p0 & !p1\n", - "⓿\n", + "\n", + "\n", + "p0 & !p1\n", + "⓿\n", "\n", "\n", "\n", "10->7\n", - "\n", - "\n", - "p0 & p1\n", - "⓿\n", + "\n", + "\n", + "p0 & p1\n", + "⓿\n", "\n", "\n", "\n", "10->10\n", - "\n", - "\n", - "!p0 & p1\n", + "\n", + "\n", + "!p0 & p1\n", "\n", "\n", "\n", "10->11\n", - "\n", - "\n", - "!p0 & !p1\n", - "❶\n", + "\n", + "\n", + "!p0 & !p1\n", + "❶\n", "\n", "\n", "\n", "11->6\n", - "\n", - "\n", - "p0 & !p1\n", - "⓿\n", + "\n", + "\n", + "p0 & !p1\n", + "⓿\n", "\n", "\n", "\n", "11->10\n", - "\n", - "\n", - "!p0 & p1\n", - "❶\n", + "\n", + "\n", + "!p0 & p1\n", + "❶\n", "\n", "\n", "\n", "11->11\n", - "\n", - "\n", - "!p0 & !p1\n", - "❶\n", + "\n", + "\n", + "!p0 & !p1\n", + "❶\n", "\n", - "\n", + "\n", "\n", - "11->13\n", - "\n", - "\n", - "p0 & p1\n", - "⓿\n", + "11->12\n", + "\n", + "\n", + "p0 & p1\n", + "⓿\n", "\n", - "\n", + "\n", "\n", - "12->2\n", - "\n", - "\n", - "p0 & !p1\n", - "⓿\n", + "12->6\n", + "\n", + "\n", + "p0 & !p1\n", + "⓿\n", "\n", - "\n", + "\n", + "\n", + "12->7\n", + "\n", + "\n", + "p0 & p1\n", + "❶\n", + "\n", + "\n", "\n", - "12->8\n", - "\n", - "\n", - "!p0 & !p1\n", - "⓿\n", + "12->11\n", + "\n", + "\n", + "!p0 & !p1\n", + "⓿\n", "\n", "\n", - "\n", - "12->12\n", - "\n", - "\n", - "!p0 & p1\n", - "\n", - "\n", "\n", - "12->13\n", - "\n", - "\n", - "p0 & p1\n", - "❶\n", + "12->12\n", + "\n", + "\n", + "!p0 & p1\n", "\n", - "\n", + "\n", + "\n", + "13->5\n", + "\n", + "\n", + "p0 & p1\n", + "⓿\n", + "\n", + "\n", "\n", - "13->2\n", - "\n", - "\n", - "p0 & !p1\n", - "⓿\n", + "13->6\n", + "\n", + "\n", + "p0 & !p1\n", + "⓿\n", "\n", - "\n", + "\n", "\n", - "13->11\n", - "\n", - "\n", - "!p0 & !p1\n", - "⓿\n", - "\n", - "\n", - "\n", - "13->12\n", - "\n", - "\n", - "p0 & p1\n", - "❶\n", + "13->8\n", + "\n", + "\n", + "!p0 & !p1\n", + "❶\n", "\n", "\n", - "\n", + "\n", "13->13\n", - "\n", - "\n", - "!p0 & p1\n", + "\n", + "\n", + "!p0 & p1\n", "\n", "\n", "\n", "14->2\n", - "\n", - "\n", - "p0 & !p1\n", + "\n", + "\n", + "p0 & !p1\n", "\n", "\n", "\n", "14->3\n", - "\n", - "\n", - "p0 & p1\n", + "\n", + "\n", + "p0 & p1\n", "\n", "\n", "\n", "14->9\n", - "\n", - "\n", - "!p0 & !p1\n", - "❶\n", + "\n", + "\n", + "!p0 & !p1\n", + "❶\n", "\n", "\n", "\n", "14->14\n", - "\n", - "\n", - "!p0 & p1\n", + "\n", + "\n", + "!p0 & p1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fa2682f4c60> >" + " *' at 0x7f5114a611b0> >" ] }, "execution_count": 29, @@ -5603,7 +5603,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa268211ae0> >" + " *' at 0x7f5114a4e4e0> >" ] }, "execution_count": 33, @@ -5715,7 +5715,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "execution_count": 34, @@ -5881,7 +5881,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa2682117b0> >" + " *' at 0x7f5114a4eed0> >" ] }, "execution_count": 35, @@ -6174,7 +6174,7 @@ "};$(\"#acdaut1 #E1\").addClass(\"acdN0\");$(\"#acdaut1 #E2\").addClass(\"acdN0\");$(\"#acdaut1 #E3\").addClass(\"acdN0\");$(\"#acdaut1 #E4\").addClass(\"acdN0\");$(\"#acdaut1 #E5\").addClass(\"acdN0\");$(\"#acdaut1 #E6\").addClass(\"acdN0\");$(\"#acdaut1 #E7\").addClass(\"acdN0\");$(\"#acdaut1 #E8\").addClass(\"acdN0\");$(\"#acdaut1 #E6\").addClass(\"acdN1\");$(\"#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 #S0\").click(function(){acd1_state(0);});$(\"#acdaut1 #S1\").click(function(){acd1_state(1);});$(\"#acd1 #N0\").click(function(){acd1_node(0, 1);});$(\"#acd1 #N1\").click(function(){acd1_node(1, 0);});" ], "text/plain": [ - " >" + " >" ] }, "execution_count": 37, @@ -6297,7 +6297,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa2682163c0> >" + " *' at 0x7f5114a6e2a0> >" ] }, "execution_count": 38, @@ -6319,6 +6319,742 @@ "assert c.equivalent_to(d)" ] }, + { + "cell_type": "markdown", + "id": "36629c32", + "metadata": {}, + "source": [ + "Paritizing a generalized-Büchi automaton with `acd_transform()` produces a Büchi automaton.\n", + "The Zielonka-tree transformation produces a larger automaton because it ignores the transition structure, and also it uses an extra and unnecessary color (because it was not taught how to omit it)." + ] + }, + { + "cell_type": "code", + "execution_count": 40, + "id": "deb92971", + "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-7\n", + "{0,1,2,3}\n", + "Q: 0-3\n", + "lvl: 0\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "T: 1,3-5\n", + "{0,1,2}\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: 7\n", + "{0}\n", + "Q: 3\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", + ")&Inf(\n", + "❷\n", + ")&Inf(\n", + "❸\n", + ")\n", + "[gen. Büchi 4]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "!p0 & p1\n", + "⓿\n", + "❶\n", + "❷\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "!p0 & !p1\n", + "⓿\n", + "❶\n", + "❷\n", + "❸\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "!p0 & p1\n", + "⓿\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "!p0 & !p1\n", + "⓿\n", + "❶\n", + "❷\n", + "❸\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "p0 & !p1\n", + "⓿\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "!p0 & p1\n", + "⓿\n", + "❶\n", + "❷\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "!p0 & !p1\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-7\n", + "{0,1,2,3}\n", + "Q: 0-3\n", + "lvl: 0\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "T: 1,3-5\n", + "{0,1,2}\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: 7\n", + "{0}\n", + "Q: 3\n", + "lvl: 1\n", + "<2>\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + " >" + ] + }, + "execution_count": 40, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "g = spot.automaton(\"\"\"HOA: v1 States: 4 Start: 0 AP: 2 \"p0\" \"p1\"\n", + "acc-name: generalized-Buchi 4 Acceptance: 4\n", + "Inf(0)&Inf(1)&Inf(2)&Inf(3) properties: trans-labels explicit-labels\n", + "trans-acc --BODY-- State: 0 [!0&1] 2 {0 1 2} [!0&!1] 3 {0 1 2 3}\n", + "State: 1 [!0&1] 0 {0 1 2} [!0&!1] 2 {0} State: 2 [!0&1] 1 {0} State: 3\n", + "[!0&!1] 2 {0 1 2 3} [0&!1] 3 {0} --END--\"\"\")\n", + "\n", + "spot.acd(g)" + ] + }, + { + "cell_type": "code", + "execution_count": 41, + "id": "94a02201", + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "⓿\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!p0 & !p1\n", + "⓿\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f5114a6e930> >" + ] + }, + "execution_count": 41, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "spot.acd_transform(g)" + ] + }, + { + "cell_type": "code", + "execution_count": 42, + "id": "3332e850", + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ") | Fin(\n", + "❶\n", + ")\n", + "[gen. Streett 1]\n", + "\n", + "\n", + "\n", + "8\n", + "\n", + "8\n", + "\n", + "\n", + "\n", + "I->8\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "6\n", + "\n", + "\n", + "\n", + "8->6\n", + "\n", + "\n", + "!p0 & p1\n", + "❶\n", + "\n", + "\n", + "\n", + "11\n", + "\n", + "11\n", + "\n", + "\n", + "\n", + "8->11\n", + "\n", + "\n", + "!p0 & !p1\n", + "⓿\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!p0 & p1\n", + "❶\n", + "\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "!p0 & !p1\n", + "❶\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "!p0 & p1\n", + "⓿\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "p0 & !p1\n", + "❶\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "!p0 & !p1\n", + "⓿\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "3->5\n", + "\n", + "\n", + "!p0 & p1\n", + "❶\n", + "\n", + "\n", + "\n", + "4->6\n", + "\n", + "\n", + "!p0 & p1\n", + "⓿\n", + "\n", + "\n", + "\n", + "7\n", + "\n", + "7\n", + "\n", + "\n", + "\n", + "4->7\n", + "\n", + "\n", + "!p0 & !p1\n", + "⓿\n", + "\n", + "\n", + "\n", + "5->8\n", + "\n", + "\n", + "!p0 & p1\n", + "⓿\n", + "\n", + "\n", + "\n", + "5->3\n", + "\n", + "\n", + "!p0 & !p1\n", + "❶\n", + "\n", + "\n", + "\n", + "9\n", + "\n", + "9\n", + "\n", + "\n", + "\n", + "6->9\n", + "\n", + "\n", + "!p0 & p1\n", + "❶\n", + "\n", + "\n", + "\n", + "7->7\n", + "\n", + "\n", + "p0 & !p1\n", + "❶\n", + "\n", + "\n", + "\n", + "10\n", + "\n", + "10\n", + "\n", + "\n", + "\n", + "7->10\n", + "\n", + "\n", + "!p0 & !p1\n", + "⓿\n", + "\n", + "\n", + "\n", + "9->8\n", + "\n", + "\n", + "!p0 & p1\n", + "❶\n", + "\n", + "\n", + "\n", + "9->6\n", + "\n", + "\n", + "!p0 & !p1\n", + "❶\n", + "\n", + "\n", + "\n", + "10->2\n", + "\n", + "\n", + "!p0 & p1\n", + "⓿\n", + "\n", + "\n", + "\n", + "11->0\n", + "\n", + "\n", + "!p0 & !p1\n", + "⓿\n", + "\n", + "\n", + "\n", + "11->1\n", + "\n", + "\n", + "p0 & !p1\n", + "⓿\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f5114a6e630> >" + ] + }, + "execution_count": 42, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "spot.zielonka_tree_transform(g)" + ] + }, { "cell_type": "markdown", "id": "7d638d20", @@ -6331,7 +7067,7 @@ }, { "cell_type": "code", - "execution_count": 40, + "execution_count": 43, "id": "german-vienna", "metadata": {}, "outputs": [ @@ -6401,10 +7137,10 @@ "\n" ], "text/plain": [ - " *' at 0x7fa268216a50> >" + " *' at 0x7f5114a6ef00> >" ] }, - "execution_count": 40, + "execution_count": 43, "metadata": {}, "output_type": "execute_result" } @@ -6428,7 +7164,7 @@ }, { "cell_type": "code", - "execution_count": 41, + "execution_count": 44, "id": "chemical-primary", "metadata": {}, "outputs": [ @@ -6438,7 +7174,7 @@ "(spot.trival_maybe(), spot.trival(True))" ] }, - "execution_count": 41, + "execution_count": 44, "metadata": {}, "output_type": "execute_result" } @@ -6449,7 +7185,7 @@ }, { "cell_type": "code", - "execution_count": 42, + "execution_count": 45, "id": "hispanic-floor", "metadata": {}, "outputs": [ @@ -6512,10 +7248,10 @@ "\n" ], "text/plain": [ - " *' at 0x7fa268216270> >" + " *' at 0x7f51027c83c0> >" ] }, - "execution_count": 42, + "execution_count": 45, "metadata": {}, "output_type": "execute_result" } @@ -6526,7 +7262,7 @@ }, { "cell_type": "code", - "execution_count": 43, + "execution_count": 46, "id": "central-london", "metadata": {}, "outputs": [ @@ -6536,7 +7272,7 @@ "(spot.trival(True), spot.trival(True))" ] }, - "execution_count": 43, + "execution_count": 46, "metadata": {}, "output_type": "execute_result" } @@ -6544,6 +7280,14 @@ "source": [ "w2.prop_weak(), w2.prop_inherently_weak()" ] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "d25733d5", + "metadata": {}, + "outputs": [], + "source": [] } ], "metadata": {