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

zlktree: share bitvectors in ACD

Browse source 
Improve the memory usage of the acd class by sharing state-vectors and
edges-vectors.

* spot/twaalgos/zlktree.cc, spot/twaalgos/zlktree.hh: Share the
vectors during the construction, and adjust the dot output to take
this into account.
This commit is contained in:
Alexandre Duret-Lutz 2021-08-30 11:07:53 +02:00
parent 26f2179805
commit 49b5d570e7
2 changed files with 93 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

63
spot/twaalgos/zlktree.cc
View file

@ -368,20 +368,51 @@ namespace spot
}
acd::acd(const const_twa_graph_ptr& aut)
: acd(scc_info(aut))
: si_(new scc_info(aut)), own_si_(true), trees_(si_->scc_count())
{
build_();
}
acd::acd(const scc_info& si)
: trees_(si.scc_count())
: si_(&si), own_si_(false), trees_(si_->scc_count())
{
unsigned scc_count = scc_count_ = si.scc_count();
const_twa_graph_ptr aut = aut_ = si.get_aut();
build_();
}
acd::~acd()
{
if (own_si_)
delete si_;
}
void acd::build_()
{
unsigned scc_count = scc_count_ = si_->scc_count();
const_twa_graph_ptr aut = aut_ = si_->get_aut();
unsigned nedges = aut->get_graph().edge_vector().size();
unsigned nstates = aut->num_states();
acc_cond posacc = aut->acc();
acc_cond negacc(posacc.num_sets(), posacc.get_acceptance().complement());
// The bitvectors store edge and state-vectors that are shared
// among the different trees.
auto allocate_vectors_maybe = [&](unsigned n)
{
if (bitvectors.size() > 2 * n)
return;
bitvectors.emplace_back(nedges, false);
bitvectors.emplace_back(nstates, false);
};
auto edge_vector = [&] (unsigned n) -> std::vector<bool>&
{
return bitvectors[2 * n];
};
auto state_vector = [&] (unsigned n) -> std::vector<bool>&
{
return bitvectors[2 * n + 1];
};
allocate_vectors_maybe(0);
// Remember the max level since of each tree of different parity.
// We will use that to decide if the output should have parity
// "min even" or "min odd" so as to minimize the number of colors
@ -391,20 +422,19 @@ namespace spot
for (unsigned scc = 0; scc < scc_count; ++scc)
{
if ((trees_[scc].trivial = si.is_trivial(scc)))
if ((trees_[scc].trivial = si_->is_trivial(scc)))
continue;
trees_[scc].num_nodes = 1;
unsigned root = nodes_.size();
trees_[scc].root = root;
bool is_even = si.is_maximally_accepting_scc(scc);
bool is_even = si_->is_maximally_accepting_scc(scc);
trees_[scc].is_even = is_even;
nodes_.emplace_back();
nodes_.emplace_back(edge_vector(0), state_vector(0));
auto& n = nodes_.back();
n.parent = root;
n.level = 0;
n.scc = scc;
n.edges.resize(nedges);
n.states.resize(nstates);
for (auto& e: si.inner_edges_of(scc))
for (auto& e: si_->inner_edges_of(scc))
{
n.edges[aut->edge_number(e)] = true;
n.states[e.src] = true;
@ -420,13 +450,13 @@ namespace spot
auto callback = [&](scc_info si, unsigned siscc)
{
nodes_.emplace_back();
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;
n.edges.resize(nedges);
n.states.resize(nstates);
for (auto& e: si.inner_edges_of(siscc))
{
n.edges[aut->edge_number(e)] = true;
@ -435,7 +465,7 @@ namespace spot
};
unsigned before_size = nodes_.size();
maximal_accepting_loops_for_scc(si, scc,
maximal_accepting_loops_for_scc(*si_, scc,
accepting_node ? negacc : posacc,
nodes_[node].edges, callback);
unsigned after_size = nodes_.size();
@ -586,7 +616,8 @@ namespace spot
const char* sep = "T: ";
for (unsigned n = 1; n <= nedges; ++n)
{
bool val = n < nedges ? edges[n] : false;
bool val = n < nedges && edges[n]
&& si_->scc_of(aut_->edge_storage(n).dst) == scc;
if (val != lastval)
{
if (lastval)
@ -617,7 +648,7 @@ namespace spot
sep = "\nQ: ";
for (unsigned n = 0; n <= nstates; ++n)
{
bool val = n < nstates ? states[n] : false;
bool val = n < nstates && states[n] && si_->scc_of(n) == scc;
if (val != lastval)
{
if (lastval)

52
spot/twaalgos/zlktree.hh
View file

@ -162,6 +162,8 @@ namespace spot
acd(const scc_info& si);
acd(const const_twa_graph_ptr& aut);
~acd();
/// \brief Walk through the ACD.
///
/// Given a \a branch number, and an edge, this returns
@ -246,6 +248,20 @@ namespace spot
void dot(std::ostream&) const;
private:
const scc_info* si_;
bool own_si_ = false;
// This structure is used to represent one node in the ACD forest.
// The tree use a left-child / right-sibling representation
// (called here first_child, next_sibling). Each node
// additionally store a level (depth in the ACD, adjusted at the
// end of the construction so that all node on the same level have
// the same parity), the SCC (which is also it's tree number), and
// some bit vectors representing the edges and states of that
// node. Those bit vectors are as large as the original
// automaton, and they are shared among nodes from the different
// trees of the ACD forest (since each tree correspond to a
// different SCC, they cannot share state or edges).
struct acd_node
{
unsigned parent;
@ -253,24 +269,48 @@ namespace spot
unsigned first_child = 0;
unsigned level;
unsigned scc;
std::vector<bool> edges;
std::vector<bool> states;
std::vector<bool>& edges;
std::vector<bool>& states;
acd_node(std::vector<bool>& e, std::vector<bool>& s) noexcept
: edges(e), states(s)
{
}
};
// We store the nodes in a deque so that their addresses do not
// change.
std::deque<acd_node> nodes_;
// Likewise for bitvectors: this is the support for all edge vectors
// and state vectors used in acd_node.
std::deque<std::vector<bool>> bitvectors;
// Information about a tree of the ACD. Each tree correspond
// to an SCC.
struct scc_data
{
bool trivial;
unsigned root = 0;
bool is_even;
unsigned max_level = 0;
bool trivial; // whether the SCC is trivial we do
// not store any node for trivial
// SCCs.
unsigned root = 0; // root node of a non-trivial SCC.
bool is_even; // parity of the tree, used at the end
// of the construction to adjust
// levels.
unsigned max_level = 0; // Maximum level for this SCC.
unsigned num_nodes = 0; // Number of node in this tree. This
// is only used to share bitvectors
// between SCC: node with the same
// "rank" in each tree share the same
// bitvectors.
};
std::vector<scc_data> trees_;
unsigned scc_count_;
const_twa_graph_ptr aut_;
// Information about the overall ACD.
bool is_even_;
bool has_rabin_shape_ = true;
bool has_streett_shape_ = true;
// Build the ACD structure. Called by the constructors.
void build_();
// leftmost branch of \a node that contains \a state
unsigned leftmost_branch_(unsigned node, unsigned state);