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

zlktree: cleanup the interface, and add interactive ACD

Browse source 
* tests/python/_zlktree.ipynb: Remove and replace by...
* tests/python/zlktree.ipynb: ... this more documented notebook.
* tests/Makefile.am: Adjust.
* doc/org/tut.org, NEWS: Mention zlktree.ipynb.
* spot/twaalgos/zlktree.hh, spot/twaalgos/zlktree.cc,
python/spot/__init__.py: Cleanup interface, and add support for
interactive display.
This commit is contained in:
Alexandre Duret-Lutz 2021-09-03 22:20:20 +02:00
parent dc17762e14
commit 5c5790039b
8 changed files with 6754 additions and 6130 deletions
Download patch file Download diff file Expand all files Collapse all files

16
NEWS
View file

@ -239,16 +239,12 @@ New in spot 2.9.8.dev (not yet released)
Additionally, this function now returns the number of states that
have been merged (and therefore removed from the automaton).
- spot::zielonka_tree is a new class that can be constructed from
any acceptance condition to help paritizing it.
spot::zielonka_tree_transform() will paritize an automaton using
the Zielong Tree of its acceptance. Similarly, spot::acd class
implement the Alternating Cycle Decomposition of any automaton.
The spot::acd_transform() function uses it to paritize any
automaton optimally. These two transformations are based on a
paper by Casares et al. (ICALP'21). The python bindings for
spot.zielonka_tree and spot.acd will display those structure
graphically, making it easier to explore those concepts.
- spot::zielonka_tree and spot::acd are new class that implement the
Zielonka Tree and Alternatic Cycle Decomposition, based on a paper
by Casares et al. (ICALP'21). Those structures can be used to
paritize any automaton, and more. The graphical rendering of ACD
in Jupyter notebooks is Spot's first interactive output. See
https://spot.lrde.epita.fr/ipynb/zlktree.html for more.
Python:

1
doc/org/tut.org
View file

@ -91,6 +91,7 @@ real notebooks instead.
- [[https://spot.lrde.epita.fr/ipynb/stutter-inv.html][=stutter-inv.ipynb=]] working with stutter-invariant formulas properties.
- [[https://spot.lrde.epita.fr/ipynb/satmin.html][=satmin.ipynb=]] Python interface for [[file:satmin.org][SAT-based minimization of deterministic ω-automata]].
- [[https://spot.lrde.epita.fr/ipynb/twagraph-internals.html][=twagraph-internals.ipynb=]] Inner workings of the =twa_graph= class.
- [[https://spot.lrde.epita.fr/ipynb/zlktree.html][=zlktree.ipynb=]] demonstration of Zielonka Trees and ACD
# LocalWords: utf html bdd IPython ipynb io randaut accparse acc
# LocalWords: cond randltl genltl genaut scc testingaut ltsmin dve

71
python/spot/__init__.py
View file

@ -436,14 +436,81 @@ class zielonka_tree:
self.dot(ostr)
return _ostream_to_svg(ostr)
_acdnum = 0
@_extend(acd)
class acd:
def _repr_svg_(self):
def _repr_svg_(self, id=None):
"""Output the ACD as SVG"""
ostr = ostringstream()
self.dot(ostr)
self.dot(ostr, id)
return _ostream_to_svg(ostr)
def _repr_html_(self):
global _acdnum
num = _acdnum
_acdnum += 1
style = '''
.acdhigh ellipse,.acdacc ellipse,.acdacc path,.acdacc polygon{stroke:green;}
.acdhigh polygon,.acdrej ellipse,.acdrej path,.acdrej polygon{stroke:red;}
.acdbold ellipse,.acdbold polygon,.acdbold path{stroke-width:2;}
.acdrej polygon{fill:red;}
.acdacc polygon{fill:green;}
'''
js = '''
function acd{num}_clear(){{
$("#acd{num} .node,#acdaut{num} .node,#acdaut{num} .edge")
.removeClass("acdhigh acdbold acdacc acdrej");
}};
function acd{num}_state(state){{
acd{num}_clear();
$("#acd{num} .acdS" + state).addClass("acdhigh acdbold");
$("#acdaut{num} #S" + state).addClass("acdbold");
}};
function acd{num}_edge(edge){{
acd{num}_clear();
var theedge = $('#acdaut{num} #E' + edge)
var classList = theedge.attr('class').split(/\s+/);
$.each(classList, function(index, item) {{
if (item.startsWith('acdN')) {{
$("#acd{num} #" + item.substring(3)).addClass("acdhigh acdbold");
}}
}});
theedge.addClass("acdbold");
}};
function acd{num}_node(node, acc){{
acd{num}_clear();
$("#acdaut{num} .acdN" + node).addClass(acc
? "acdacc acdbold"
: "acdrej acdbold");
$("#acd{num} #N" + node).addClass("acdbold acdhigh");
}};'''.format(num=num)
me = 0
for n in range(self.node_count()):
for e in self.edges_of_node(n):
me = max(e, me)
js += '$("#acdaut{num} #E{e}").addClass("acdN{n}");'\
.format(num=num, e=e, n=n)
for e in range(1, me + 1):
js += '$("#acdaut{num} #E{e}")'\
'.click(function(){{acd{num}_edge({e});}});'\
.format(num=num, e=e)
for s in range(self.get_aut().num_states()):
js += '$("#acdaut{num} #S{s}")'\
'.click(function(){{acd{num}_state({s});}});'\
.format(num=num, s=s)
for n in range(self.node_count()):
v = int(self.node_acceptance(n))
js += '$("#acd{num} #N{n}")'\
'.click(function(){{acd{num}_node({n}, {v});}});'\
.format(num=num, n=n, v=v)
html = '<style>{}</style><div>{}</div><div>{}</div><script>{}</script>'\
.format(style,
self.get_aut().show('.i(acdaut{})'.format(num)).data,
self._repr_svg_("acd{}".format(num)),
js);
return html
def automata(*sources, timeout=None, ignore_abort=True,
trust_hoa=True, no_sid=False, debug=False,

102
spot/twaalgos/zlktree.cc
View file

@ -22,6 +22,7 @@
#include <deque>
#include <spot/twaalgos/zlktree.hh>
#include <spot/twaalgos/genem.hh>
#include <spot/misc/escape.hh>
namespace spot
{
@ -138,6 +139,9 @@ namespace spot
has_streett_shape_ = false;
}
}
bool empty_is_accepting = code.accepting(acc_cond::mark_t{});
empty_is_even_ = empty_is_accepting == is_even_;
}
void zielonka_tree::dot(std::ostream& os) const
@ -175,8 +179,10 @@ namespace spot
("zielonka_tree::step(): incorrect branch number");
if (!colors)
return {branch, nodes_[branch].level + 1};
{
unsigned lvl = nodes_[branch].level;
return {branch, lvl + ((lvl & 1) == empty_is_even_)};
}
unsigned child = 0;
for (;;)
{
@ -325,17 +331,6 @@ namespace spot
+ " is too large");
}
std::pair<unsigned, unsigned>
acd::step(unsigned branch, unsigned edge) const
{
if (SPOT_UNLIKELY(nodes_.size() < branch || nodes_[branch].first_child))
throw std::runtime_error
("acd::next_branch(): incorrect branch number");
// FIXME
(void)edge;
return {branch, 0};
}
acd::acd(const const_twa_graph_ptr& aut)
: si_(new scc_info(aut)), own_si_(true), trees_(si_->scc_count())
{
@ -485,7 +480,7 @@ namespace spot
}
}
unsigned acd::leftmost_branch_(unsigned n, unsigned state)
unsigned acd::leftmost_branch_(unsigned n, unsigned state) const
{
loop:
unsigned first_child = nodes_[n].first_child;
@ -507,42 +502,45 @@ namespace spot
}
unsigned acd::first_branch(unsigned s, unsigned scc)
unsigned acd::first_branch(unsigned s) const
{
if (scc > trees_.size())
report_invalid_scc_number(scc, "first_branch");
if (SPOT_UNLIKELY(aut_->num_states() < s))
throw std::runtime_error("first_branch(): unknown state " +
std::to_string(s));
unsigned scc = si_->scc_of(s);
if (trees_[scc].trivial) // the branch is irrelevant for transiant SCCs
return 0;
unsigned n = trees_[scc].root;
if (SPOT_UNLIKELY(!nodes_[n].states[s]))
throw std::runtime_error("first_branch(): state " +
std::to_string(s) + " not found in SCC " +
std::to_string(scc));
assert(nodes_[n].states[s]);
return leftmost_branch_(n, s);
}
std::pair<unsigned, unsigned>
acd::step(unsigned branch, unsigned edge)
acd::step(unsigned branch, unsigned edge) const
{
if (SPOT_UNLIKELY(nodes_.size() < branch))
throw std::runtime_error("acd::step(): incorrect branch number");
if (SPOT_UNLIKELY(nodes_[branch].edges.size() < edge))
throw std::runtime_error("acd::step(): incorrect edge number");
unsigned child = 0;
unsigned obranch = branch;
unsigned dst = aut_->edge_storage(edge).dst;
while (!nodes_[branch].edges[edge])
{
unsigned parent = nodes_[branch].parent;
if (SPOT_UNLIKELY(branch == parent))
throw std::runtime_error("acd::step(): edge " +
std::to_string(edge) +
" is not on branch " +
std::to_string(obranch));
{
// We are changing SCC, so the level emitted does not
// matter.
assert(si_->scc_of(aut_->edge_storage(edge).src)
!= si_->scc_of(dst));
return { first_branch(dst), 0 };
}
child = branch;
branch = parent;
}
unsigned lvl = nodes_[branch].level;
unsigned dst = aut_->edge_storage(edge).dst;
if (child != 0)
{
unsigned start_child = child;
@ -562,10 +560,14 @@ namespace spot
}
}
void acd::dot(std::ostream& os) const
void acd::dot(std::ostream& os, const char* id) const
{
os << "digraph acd {\n labelloc=\"t\"\n label=\"\n"
<< (is_even_ ? "min even\"" : "min odd\"\n");
if (id)
escape_str(os << " id=\"", id)
// fill the node so that the entire node is clickable
<< "\"\n node [id=\"N\\N\", style=filled, fillcolor=white]\n";
unsigned ns = nodes_.size();
for (unsigned n = 0; n < ns; ++n)
{
@ -642,9 +644,22 @@ namespace spot
os << "\nlvl: " << nodes_[n].level;
if (!first_child)
os << "\n<" << n << '>';
// use a fillcolor so that the entire node is clickable
os << "\", shape="
<< (((nodes_[n].level & 1) ^ is_even_) ? "ellipse" : "box")
<< "]\n";
<< (((nodes_[n].level & 1) ^ is_even_) ? "ellipse" : "box");
if (id)
{
os << " class=\"";
const char* sep = "";
for (unsigned n = 0; n < nstates; ++n)
if (states[n] && si_->scc_of(n) == scc)
{
os << sep << "acdS" << n << '\n';
sep = " ";
}
os << '\"';
}
os << "]\n";
if (first_child)
{
unsigned child = first_child;
@ -659,6 +674,27 @@ namespace spot
os << "}\n";
}
bool acd::node_acceptance(unsigned n) const
{
if (SPOT_UNLIKELY(nodes_.size() < n))
throw std::runtime_error("acd::node_acceptance(): unknown node");
return (nodes_[n].level & 1) ^ is_even_;
}
std::vector<unsigned> acd::edges_of_node(unsigned n) const
{
if (SPOT_UNLIKELY(nodes_.size() < n))
throw std::runtime_error("acd::edges_of_node(): unknown node");
std::vector<unsigned> res;
unsigned scc = nodes_[n].scc;
auto& edges = nodes_[n].edges;
unsigned nedges = edges.size();
for (unsigned e = 1; e < nedges; ++e)
if (edges[e] && si_->scc_of(aut_->edge_storage(e).dst) == scc)
res.push_back(e);
return res;
}
twa_graph_ptr
acd_transform(const const_twa_graph_ptr& a, bool colored)
{
@ -714,7 +750,7 @@ namespace spot
};
unsigned init = a->get_init_state_number();
zlk_state s(init, theacd.first_branch(init, si.scc_of(init)));
zlk_state s(init, theacd.first_branch(init));
new_state(s);
unsigned max_color = 0;
bool is_even = theacd.is_even();
@ -734,7 +770,7 @@ namespace spot
unsigned dst_scc = si.scc_of(i.dst);
if (dst_scc != src_scc)
{
newbranch = theacd.first_branch(i.dst, dst_scc);
newbranch = theacd.first_branch(i.dst);
prio = 0;
}
else

60
spot/twaalgos/zlktree.hh
View file

@ -71,10 +71,12 @@ namespace spot
/// definition since it allows a set of colors to be processed,
/// and not exactly one color. When multiple colors are given,
/// the minimum corresponding level is returned. When no color is
/// given, the branch is not changed and the level returned is one
/// more than the depth of that branch (this is as if the tree add
/// another layer of leaves labeled by the empty sets, that do not
/// store for simplicity).
/// given, the branch is not changed and the level returned might
/// be one more than the depth of that branch (as if the tree had
/// another layer of leaves labeled by the empty sets, that we
/// do not store). Whether the depth for no color is the depth
/// of the node or one more depend on whether the absence of
/// color had the same parity has the current node.
std::pair<unsigned, unsigned>
step(unsigned branch, acc_cond::mark_t colors) const;
@ -127,6 +129,7 @@ namespace spot
unsigned one_branch_ = 0;
unsigned num_branches_ = 0;
bool is_even_;
bool empty_is_even_;
bool has_rabin_shape_ = true;
bool has_streett_shape_ = true;
};
@ -164,19 +167,34 @@ namespace spot
~acd();
/// \brief Walk through the ACD.
/// \brief Step through the ACD.
///
/// Given a \a branch number, and an edge, this returns
/// a pair (new branch, level), as needed in definition 4.6 of
/// \cite casares.21.icalp (or definition 4.20 in the full version).
/// We do not have to specify any SCC, because the branch number are
/// different in each SCC.
///
/// The level correspond to the priority of a minimum parity acceptance
/// condition, with the parity odd/even as specified by is_even().
std::pair<unsigned, unsigned>
step(unsigned branch, unsigned edge) const;
/// \brief Return the list of edges covered by node n of the ACD.
///
/// This is mostly used for interactive display.
std::vector<unsigned> edges_of_node(unsigned n) const;
/// \brief Return the number of nodes in the the ACD forest.
unsigned node_count() const
{
return nodes_.size();
}
/// Tell whether a node store accepting or rejecting cycles.
///
/// This is mostly used for interactive display.
bool node_acceptance(unsigned n) const;
/// \brief Whether the ACD corresponds to a min even or min odd
/// parity acceptance in SCC \a scc.
bool is_even(unsigned scc) const
@ -198,20 +216,9 @@ namespace spot
}
/// \brief Return the first branch for \a state
///
/// \a scc should correspond to the SCC containing \a state.
/// (this class does not store the scc_info passed at construction)
unsigned first_branch(unsigned state, unsigned scc);
unsigned first_branch(unsigned state) const;
/// \brief Step into the ACD
///
/// Given an edge \a edge on branch \a branch,
/// return a pair (new branch, level) giving the proirity (\a level) to
/// emit, and the branch of the destination state.
std::pair<unsigned, unsigned>
step(unsigned branch, unsigned edge);
unsigned scc_max_level(unsigned scc)
unsigned scc_max_level(unsigned scc) const
{
if (scc >= scc_count_)
report_invalid_scc_number(scc, "scc_max_level");
@ -244,8 +251,17 @@ namespace spot
return has_streett_shape() && has_rabin_shape();
}
/// \brief Return the automaton on which the ACD is defined.
const const_twa_graph_ptr get_aut() const
{
return aut_;
}
/// \brief Render the ACD as in GraphViz format.
void dot(std::ostream&) const;
///
/// If \a id is given, it is used to give the graph an id, and,
/// all nodes will get ids as well.
void dot(std::ostream&, const char* id = nullptr) const;
private:
const scc_info* si_;
@ -312,7 +328,7 @@ namespace spot
void build_();
// leftmost branch of \a node that contains \a state
unsigned leftmost_branch_(unsigned node, unsigned state);
unsigned leftmost_branch_(unsigned node, unsigned state) const;
#ifndef SWIG
[[noreturn]] static

2
tests/Makefile.am
View file

@ -449,7 +449,7 @@ TESTS_python = \
python/twagraph.py \
python/toweak.py \
python/_word.ipynb \
python/_zlktree.ipynb \
python/zlktree.ipynb \
$(TESTS_ipython)
endif

6062
tests/python/_zlktree.ipynb
View file

File diff suppressed because it is too large Load diff

6570
tests/python/zlktree.ipynb Normal file
View file

File diff suppressed because one or more lines are too long