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

zlktree: use a cache in the construction of zielonka_tree

Browse source 
This largely speeds up the computation for conditions
like "Rabin n" sharing a lot of subtrees.

Also implement options to stop the construction if the shape is wrong.

* spot/twaalgos/zlktree.cc, spot/twaalgos/zlktree.hh: Implement the
cache and the options.
* tests/python/zlktree.ipynb, tests/python/zlktree.py: New tests.
This commit is contained in:
Alexandre Duret-Lutz 2022-05-20 16:51:16 +02:00
parent f784e40548
commit b11208440b
5 changed files with 517 additions and 151 deletions
Download patch file Download diff file Expand all files Collapse all files

74
spot/twaalgos/zlktree.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2021 Laboratoire de Recherche et Developpement de
// Copyright (C) 2021, 2022 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -109,7 +109,8 @@ namespace spot
}
}
zielonka_tree::zielonka_tree(const acc_cond& cond)
zielonka_tree::zielonka_tree(const acc_cond& cond,
zielonka_tree_options opt)
{
const acc_cond::acc_code& code = cond.get_acceptance();
auto all = cond.all_sets();
@ -120,11 +121,47 @@ namespace spot
nodes_[0].colors = all;
nodes_[0].level = 0;
robin_hood::unordered_node_map<acc_cond::mark_t, unsigned> nmap;
std::vector<size_model> models;
// This loop is a BFS over the increasing set of nodes.
for (unsigned node = 0; node < nodes_.size(); ++node)
{
acc_cond::mark_t colors = nodes_[node].colors;
unsigned nextlvl = nodes_[node].level + 1;
// Have we already seen this combination of colors previously?
// If yes, simply copy the children.
if (auto p = nmap.emplace(colors, node); !p.second)
{
unsigned fc = nodes_[p.first->second].first_child;
if (!fc) // this is a leaf
{
++num_branches_;
continue;
}
if (!!(opt & zielonka_tree_options::MERGE_SUBTREES))
{
nodes_[node].first_child = fc;
continue;
}
unsigned child = fc;
unsigned first = nodes_.size();
nodes_[node].first_child = first;
do
{
auto& c = nodes_[child];
child = c.next_sibling;
nodes_.push_back({node, static_cast<unsigned>(nodes_.size() + 1),
0, nextlvl, c.colors});
}
while (child != fc);
nodes_.back().next_sibling = first;
// We do not have to test the shape since this is the second time
// we see these colors;
continue;
}
bool is_accepting = code.accepting(colors);
if (node == 0)
is_even_ = is_accepting;
@ -145,15 +182,32 @@ namespace spot
nodes_.reserve(first + num_children);
for (auto& m: models)
nodes_.push_back({node, static_cast<unsigned>(nodes_.size() + 1),
0, nodes_[node].level + 1, m.model});
0, nextlvl, m.model});
nodes_.back().next_sibling = first;
if (num_children > 1)
{
bool abort = false;
if (is_accepting)
has_rabin_shape_ = false;
{
has_rabin_shape_ = false;
if (!!(opt & zielonka_tree_options::ABORT_WRONG_SHAPE)
&& !!(opt & zielonka_tree_options::CHECK_RABIN))
abort = true;
}
else
has_streett_shape_ = false;
{
has_streett_shape_ = false;
if (!!(opt & zielonka_tree_options::ABORT_WRONG_SHAPE)
&& !!(opt & zielonka_tree_options::CHECK_STREETT))
abort = true;
}
if (abort)
{
nodes_.clear();
num_branches_ = 0;
return;
}
}
}
@ -523,14 +577,18 @@ namespace spot
do
{
auto& c = nodes_[child];
// We have to read anything we need from C
// before emplace_back, which may reallocate.
acc_cond::mark_t colors = c.colors;
unsigned minstate = c.minstate;
child = c.next_sibling;
nodes_.emplace_back(c.edges, c.states);
auto& n = nodes_.back();
n.parent = node;
n.level = lvl + 1;
n.scc = ref.scc;
n.colors = c.colors;
n.minstate = c.minstate;
child = c.next_sibling;
n.colors = colors;
n.minstate = minstate;
}
while (child != fc);
chain_children(node, before, nodes_.size());

67
spot/twaalgos/zlktree.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2021 Laboratoire de Recherche et Developpement de
// Copyright (C) 2021, 2022 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -28,6 +28,68 @@
namespace spot
{
/// \ingroup twa_acc_transform
/// \brief Options to alter the behavior of acd
enum class zielonka_tree_options
{
/// Build the ZlkTree, without checking its shape.
NONE = 0,
/// Check if the ZlkTree has Rabin shape.
/// This actually has no effect unless ABORT_WRONG_SHAPE is set,
/// because zielonka_tree always check the shape.
CHECK_RABIN = 1,
/// Check if the ZlkTree has Streett shape.
/// This actually has no effect unless ABORT_WRONG_SHAPE is set,
/// because zielonka_tree always check the shape.
CHECK_STREETT = 2,
/// Check if the ZlkTree has Parity shape
/// This actually has no effect unless ABORT_WRONG_SHAPE is set,
/// because zielonka_tree always check the shape.
CHECK_PARITY = CHECK_RABIN | CHECK_STREETT,
/// Abort the construction of the ZlkTree if it does not have the
/// shape that is tested. When that happens, num_branches() is set
/// to 0.
ABORT_WRONG_SHAPE = 4,
/// Fuse identical substree. This cannot be used with
/// zielonka_tree_transform(). However it saves memory if the
/// only use of the zielonka_tree to check the shape.
MERGE_SUBTREES = 8,
};
#ifndef SWIG
inline
bool operator!(zielonka_tree_options me)
{
return me == zielonka_tree_options::NONE;
}
inline
zielonka_tree_options operator&(zielonka_tree_options left,
zielonka_tree_options right)
{
typedef std::underlying_type_t<zielonka_tree_options> ut;
return static_cast<zielonka_tree_options>(static_cast<ut>(left)
& static_cast<ut>(right));
}
inline
zielonka_tree_options operator|(zielonka_tree_options left,
zielonka_tree_options right)
{
typedef std::underlying_type_t<zielonka_tree_options> ut;
return static_cast<zielonka_tree_options>(static_cast<ut>(left)
| static_cast<ut>(right));
}
inline
zielonka_tree_options operator-(zielonka_tree_options left,
zielonka_tree_options right)
{
typedef std::underlying_type_t<zielonka_tree_options> ut;
return static_cast<zielonka_tree_options>(static_cast<ut>(left)
& ~static_cast<ut>(right));
}
#endif
/// \ingroup twa_acc_transform
/// \brief Zielonka Tree implementation
///
@ -41,7 +103,8 @@ namespace spot
{
public:
/// \brief Build a Zielonka tree from the acceptance condition.
zielonka_tree(const acc_cond& cond);
zielonka_tree(const acc_cond& cond,
zielonka_tree_options opt = zielonka_tree_options::NONE);
/// \brief The number of branches in the Zielonka tree.
///