alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

acd: remove redundant nodes

Browse source 
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.
This commit is contained in:
Alexandre Duret-Lutz 2021-09-05 16:56:54 +02:00
parent d5b641a7dc
commit 170d839c4b
3 changed files with 1679 additions and 892 deletions
Download patch file Download diff file Expand all files Collapse all files

65
spot/twaalgos/zlktree.cc
View file

@ -20,9 +20,11 @@
#include "config.h"
#include <iostream>
#include <deque>
#include <memory>
#include <spot/twaalgos/zlktree.hh>
#include <spot/twaalgos/genem.hh>
#include <spot/misc/escape.hh>
#include <spot/misc/bitvect.hh>
namespace spot
{
@ -405,6 +407,13 @@ namespace spot
}
}
struct size_model
{
unsigned size;
std::unique_ptr<bitvect> trans;
};
std::vector<size_model> 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<bitvect>(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;