From 86c22d98bc153234757fbb30ea2de49f12852623 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 31 Aug 2021 15:17:56 +0200 Subject: [PATCH] zlktree: remimplement zielonka_tree without BDDs * spot/twaalgos/zlktree.cc (zielonka_tree): Find the models using a recursive procedure on the acceptance condition, without conversion to BDD. * tests/python/_zlktree.ipynb: Adjust to a different order of nodes. --- spot/twaalgos/zlktree.cc | 153 ++++++++++++++---------------------- tests/python/_zlktree.ipynb | 54 ++++++------- 2 files changed, 88 insertions(+), 119 deletions(-) diff --git a/spot/twaalgos/zlktree.cc b/spot/twaalgos/zlktree.cc index 0940ae46c..1641d76b9 100644 --- a/spot/twaalgos/zlktree.cc +++ b/spot/twaalgos/zlktree.cc @@ -22,41 +22,13 @@ #include #include #include -#include "spot/priv/bddalloc.hh" namespace spot { - zielonka_tree::zielonka_tree(const acc_cond& cond) + namespace { - const acc_cond::acc_code& code = cond.get_acceptance(); - auto used = code.used_sets(); - unsigned c = used.count(); - unsigned max = used.max_set(); - - bdd_allocator ba; - int base = ba.allocate_variables(c); - assert(base == 0); - std::vector col_to_bdd(max ? max : 1, bddfalse); - std::vector bdd_to_col(c); - bdd all_neg = bddtrue; - for (unsigned i = 0; i < max; ++i) - if (used.has(i)) - { - bdd_to_col[base] = i; - all_neg &= bdd_nithvar(base); - col_to_bdd[i] = bdd_ithvar(base++); - } - - bdd poscond = code.to_bdd(col_to_bdd.data()); - bdd negcond = !poscond; - - nodes_.emplace_back(); - nodes_[0].parent = 0; - nodes_[0].colors = used; - nodes_[0].level = 0; - - // Or goal is the find the list of maximal models for a formula named - // cond and defined later for each node. + // Or goal is the find the list of maximal models for a formula + // named cond and defined later for each node. // // For instance if cond is satisfied by {1}, {3}, {1,2}, {1,2,3}, // {0,3}, and {0,1,3}, then the maximal models are {1,2,3} and @@ -76,8 +48,61 @@ namespace spot unsigned size; acc_cond::mark_t model; }; - std::vector models; + void max_models(acc_cond cond, + acc_cond::mark_t colors, + std::vector& out) + { + if (!colors) + return; + if (cond.accepting(colors)) + { + unsigned sz = colors.count(); + auto iter = out.begin(); + while (iter != out.end()) + { + if (iter->size < sz) + // We have checked all larger models. + break; + if (colors.subset(iter->model)) + // curmodel is covered by iter->model. + return; + ++iter; + } + // insert the model + iter = out.insert(iter, {sz, colors}); + ++iter; + // erase all models it contains + out.erase(std::remove_if(iter, out.end(), + [&](auto& mod) { + return mod.model.subset(colors); + }), out.end()); + } + else if (acc_cond::mark_t fu = cond.fin_unit()) + { + max_models(cond.remove(fu, true), colors - fu, out); + } + else if (int fo = cond.fin_one(); fo >= 0) + { + acc_cond::mark_t fo_m = {(unsigned) fo}; + max_models(cond.remove(fo_m, true), colors - fo_m, out); + max_models(cond.remove(fo_m, false), colors, out); + } + } + } + + zielonka_tree::zielonka_tree(const acc_cond& cond) + { + const acc_cond::acc_code& code = cond.get_acceptance(); + auto used = code.used_sets(); + acc_cond negcond(cond.num_sets(), cond.get_acceptance().complement()); + + nodes_.emplace_back(); + nodes_[0].parent = 0; + nodes_[0].colors = used; + nodes_[0].level = 0; + + std::vector models; // This loop is a BFS over the increasing set of nodes. for (unsigned node = 0; node < nodes_.size(); ++node) { @@ -86,67 +111,12 @@ namespace spot if (node == 0) is_even_ = is_accepting; - // colors that do not appear in this node should - // be set to false in the acceptance. - bdd to_remove = bddtrue; - for (unsigned c: (colors ^ used).sets()) - to_remove &= !col_to_bdd[c]; - bdd cond = bdd_restrict(is_accepting ? negcond : poscond, to_remove); - - // These is where we will store the ordered list of models, as - // explained in the declation of that vector. + acc_cond c = (is_accepting ? negcond : cond).restrict_to(colors); models.clear(); + max_models(c, colors, models); - while (cond != bddfalse) - { - // Find one model of cond. If it has some don't cares - // variable, we interpret them as true, so in effect, we can - // start from a model where all colors are sets, and only - // unset those that are negative in the output of - // bdd_satone. - bdd one = bdd_satone(cond); - cond -= one; - acc_cond::mark_t curmodel = colors; - while (one != bddtrue) - { - unsigned v = bdd_to_col[bdd_var(one)]; - if (bdd_high(one) == bddfalse) - { - curmodel.clear(v); - one = bdd_low(one); - } - else - { - one = bdd_high(one); - } - } - // - unsigned sz = curmodel.count(); - if (sz == 0) - // ignore the empty set - continue; - auto iter = models.begin(); - while (iter != models.end()) - { - if (iter->size < sz) - // We have checked all larger models. - break; - if (curmodel.subset(iter->model)) - // curmodel is covered by iter->model. - goto donotinsert; - ++iter; - } - // insert the model - iter = models.insert(iter, {sz, curmodel}); - ++iter; - // erase all models it contains - models.erase(std::remove_if(iter, models.end(), - [&](auto& mod) { - return mod.model.subset(curmodel); - }), models.end()); - donotinsert:; - } - if (models.empty()) // This is a leaf of the tree. + unsigned num_children = models.size(); + if (num_children == 0) // This is a leaf of the tree. { if (num_branches_++ == 0) one_branch_ = node; @@ -154,7 +124,6 @@ namespace spot } unsigned first = nodes_.size(); nodes_[node].first_child = first; - unsigned num_children = models.size(); nodes_.reserve(first + num_children); for (auto& m: models) nodes_.push_back({node, static_cast(nodes_.size() + 1), diff --git a/tests/python/_zlktree.ipynb b/tests/python/_zlktree.ipynb index 00da76696..637c7813f 100644 --- a/tests/python/_zlktree.ipynb +++ b/tests/python/_zlktree.ipynb @@ -126,7 +126,7 @@ "\n", "8\n", "\n", - "{3}\n", + "{1}\n", "<8>\n", "\n", "\n", @@ -139,7 +139,7 @@ "\n", "9\n", "\n", - "{1}\n", + "{3}\n", "<9>\n", "\n", "\n", @@ -152,7 +152,7 @@ "\n", "10\n", "\n", - "{3}\n", + "{1}\n", "<10>\n", "\n", "\n", @@ -165,7 +165,7 @@ "\n", "11\n", "\n", - "{1}\n", + "{3}\n", "<11>\n", "\n", "\n", @@ -191,7 +191,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -286,7 +286,7 @@ { "data": { "text/plain": [ - "(9, 2)" + "(8, 3)" ] }, "execution_count": 6, @@ -307,7 +307,7 @@ { "data": { "text/plain": [ - "(9, 3)" + "(8, 2)" ] }, "execution_count": 7, @@ -328,7 +328,7 @@ { "data": { "text/plain": [ - "(8, 3)" + "(9, 2)" ] }, "execution_count": 8, @@ -755,7 +755,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -1111,7 +1111,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -1247,7 +1247,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -1358,7 +1358,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -1421,7 +1421,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -1484,7 +1484,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -2587,7 +2587,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "execution_count": 24, @@ -3974,7 +3974,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f14dc2662a0> >" + " *' at 0x7fd0ba759870> >" ] }, "execution_count": 38, @@ -4058,7 +4058,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "execution_count": 40, @@ -4181,7 +4181,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f14dc266720> >" + " *' at 0x7fd0ba764240> >" ] }, "execution_count": 41, @@ -4329,7 +4329,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f14dc29b750> >" + " *' at 0x7fd0ba764750> >" ] }, "metadata": {}, @@ -4483,7 +4483,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f14dc29b3f0> >" + " *' at 0x7fd0ba7646c0> >" ] }, "metadata": {}, @@ -4629,7 +4629,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f14dc29b2a0> >" + " *' at 0x7fd0ba759bd0> >" ] }, "metadata": {}, @@ -4881,7 +4881,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "execution_count": 48, @@ -5015,7 +5015,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f14dc27abd0> >" + " *' at 0x7fd0ba747c90> >" ] }, "execution_count": 50, @@ -5406,7 +5406,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f14dc295360> >" + " *' at 0x7fd0b9cfb570> >" ] }, "execution_count": 51, @@ -5790,7 +5790,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f14dc295420> >" + " *' at 0x7fd0b9cfb840> >" ] }, "execution_count": 52, @@ -5874,7 +5874,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f14dc295960> >" + " *' at 0x7fd0b9cfbc90> >" ] }, "execution_count": 53, @@ -5996,7 +5996,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f14dc295ba0> >" + " *' at 0x7fd0b9cfb5a0> >" ] }, "execution_count": 56,