diff --git a/NEWS b/NEWS
index 6f4d7d37f..a425a352d 100644
--- a/NEWS
+++ b/NEWS
@@ -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:
diff --git a/doc/org/tut.org b/doc/org/tut.org
index ba8f893b5..d3bd313c8 100644
--- a/doc/org/tut.org
+++ b/doc/org/tut.org
@@ -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
diff --git a/python/spot/__init__.py b/python/spot/__init__.py
index 4c8a419dc..25ca26138 100644
--- a/python/spot/__init__.py
+++ b/python/spot/__init__.py
@@ -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 = '
{}
{}
'\
+ .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,
diff --git a/spot/twaalgos/zlktree.cc b/spot/twaalgos/zlktree.cc
index 1641d76b9..105bfe19d 100644
--- a/spot/twaalgos/zlktree.cc
+++ b/spot/twaalgos/zlktree.cc
@@ -22,6 +22,7 @@
#include
#include
#include
+#include
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
- 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
- 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 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 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
diff --git a/spot/twaalgos/zlktree.hh b/spot/twaalgos/zlktree.hh
index 3d395541d..8222a8335 100644
--- a/spot/twaalgos/zlktree.hh
+++ b/spot/twaalgos/zlktree.hh
@@ -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
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
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 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
- 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
diff --git a/tests/Makefile.am b/tests/Makefile.am
index 02ec0b893..a6c454bb9 100644
--- a/tests/Makefile.am
+++ b/tests/Makefile.am
@@ -449,7 +449,7 @@ TESTS_python = \
python/twagraph.py \
python/toweak.py \
python/_word.ipynb \
- python/_zlktree.ipynb \
+ python/zlktree.ipynb \
$(TESTS_ipython)
endif
diff --git a/tests/python/_zlktree.ipynb b/tests/python/_zlktree.ipynb
deleted file mode 100644
index 637c7813f..000000000
--- a/tests/python/_zlktree.ipynb
+++ /dev/null
@@ -1,6062 +0,0 @@
-{
- "cells": [
- {
- "cell_type": "code",
- "execution_count": 1,
- "id": "found-hurricane",
- "metadata": {},
- "outputs": [],
- "source": [
- "import spot\n",
- "spot.setup()"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 2,
- "id": "colonial-testimony",
- "metadata": {},
- "outputs": [
- {
- "data": {
- "image/svg+xml": [
- "\n",
- "\n",
- "\n",
- "\n",
- "\n"
- ],
- "text/plain": [
- " >"
- ]
- },
- "metadata": {},
- "output_type": "display_data"
- },
- {
- "data": {
- "text/plain": [
- "(6, 7, False, False, False)"
- ]
- },
- "execution_count": 2,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "c = spot.acc_cond('Fin(0)&Inf(1)&(Inf(2)|Fin(3)) | (Inf(0)|Fin(1))&Fin(2)&Inf(3)')\n",
- "t = spot.zielonka_tree(c); display(t)\n",
- "t.num_branches(), t.first_branch(), t.has_rabin_shape(), t.has_streett_shape(), t.has_parity_shape()"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 3,
- "id": "incorrect-protection",
- "metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "(7, 3)"
- ]
- },
- "execution_count": 3,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "t.step(7, [3])"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 4,
- "id": "rolled-command",
- "metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "(7, 2)"
- ]
- },
- "execution_count": 4,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "t.step(7, [2])"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 5,
- "id": "affecting-border",
- "metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "(8, 1)"
- ]
- },
- "execution_count": 5,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "t.step(7, [1])"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 6,
- "id": "accepting-clerk",
- "metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "(8, 3)"
- ]
- },
- "execution_count": 6,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "t.step(8, [1])"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 7,
- "id": "flexible-country",
- "metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "(8, 2)"
- ]
- },
- "execution_count": 7,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "t.step(9, [1])"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 8,
- "id": "continental-sessions",
- "metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "(9, 2)"
- ]
- },
- "execution_count": 8,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "t.step(8, [3])"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 9,
- "id": "expired-asian",
- "metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "(10, 0)"
- ]
- },
- "execution_count": 9,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "t.step(8, [0])"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 10,
- "id": "binary-republic",
- "metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "(7, 0)"
- ]
- },
- "execution_count": 10,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "t.step(10, [0,2])"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 11,
- "id": "starting-liechtenstein",
- "metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "(10, 0)"
- ]
- },
- "execution_count": 11,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "t.step(7, [0,2])"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 12,
- "id": "forced-canyon",
- "metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "(7, 4)"
- ]
- },
- "execution_count": 12,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "t.step(7, [])"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 13,
- "id": "floppy-chassis",
- "metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "(6, (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)) | (Fin(4) & Inf(5)))\n"
- ]
- },
- {
- "data": {
- "image/svg+xml": [
- "\n",
- "\n",
- "\n",
- "\n",
- "\n"
- ],
- "text/plain": [
- " >"
- ]
- },
- "metadata": {},
- "output_type": "display_data"
- },
- {
- "data": {
- "text/plain": [
- "(6, 19, True, False, False)"
- ]
- },
- "execution_count": 13,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "c = spot.acc_cond('Rabin 3')\n",
- "print(c)\n",
- "t = spot.zielonka_tree(c)\n",
- "display(t)\n",
- "t.num_branches(), t.first_branch(), t.has_rabin_shape(), t.has_streett_shape(), t.has_parity_shape()"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 14,
- "id": "acquired-rogers",
- "metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "(6, (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)) & (Fin(4) | Inf(5)))\n"
- ]
- },
- {
- "data": {
- "image/svg+xml": [
- "\n",
- "\n",
- "\n",
- "\n",
- "\n"
- ],
- "text/plain": [
- " >"
- ]
- },
- "metadata": {},
- "output_type": "display_data"
- },
- {
- "data": {
- "text/plain": [
- "(6, 19, False, True, False)"
- ]
- },
- "execution_count": 14,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "c = spot.acc_cond('Streett 3')\n",
- "print(c)\n",
- "t = spot.zielonka_tree(c)\n",
- "display(t)\n",
- "t.num_branches(), t.first_branch(), t.has_rabin_shape(), t.has_streett_shape(), t.has_parity_shape()"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 15,
- "id": "minimal-douglas",
- "metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "(5, (Inf(0) & Fin(1)) | (Inf(2) & Fin(3) & Fin(4)))\n"
- ]
- },
- {
- "data": {
- "image/svg+xml": [
- "\n",
- "\n",
- "\n",
- "\n",
- "\n"
- ],
- "text/plain": [
- " >"
- ]
- },
- "metadata": {},
- "output_type": "display_data"
- },
- {
- "data": {
- "text/plain": [
- "(2, 5, True, False, False)"
- ]
- },
- "execution_count": 15,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "c = spot.acc_cond('Inf(0)&Fin(1) | (Inf(2)&Fin(3)&Fin(4))')\n",
- "print(c)\n",
- "t = spot.zielonka_tree(c)\n",
- "display(t)\n",
- "t.num_branches(), t.first_branch(), t.has_rabin_shape(), t.has_streett_shape(), t.has_parity_shape()"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 16,
- "id": "tired-thumbnail",
- "metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "(5, Fin(4) & (Inf(3) | (Fin(2) & (Inf(1) | Fin(0)))))\n"
- ]
- },
- {
- "data": {
- "image/svg+xml": [
- "\n",
- "\n",
- "\n",
- "\n",
- "\n"
- ],
- "text/plain": [
- " >"
- ]
- },
- "metadata": {},
- "output_type": "display_data"
- },
- {
- "data": {
- "text/plain": [
- "(1, 4, True, True, True)"
- ]
- },
- "execution_count": 16,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "c = spot.acc_cond('parity max odd 5')\n",
- "print(c)\n",
- "t = spot.zielonka_tree(c)\n",
- "display(t)\n",
- "t.num_branches(), t.first_branch(), t.has_rabin_shape(), t.has_streett_shape(), t.has_parity_shape()"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 17,
- "id": "structured-palace",
- "metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "(0, f)\n"
- ]
- },
- {
- "data": {
- "image/svg+xml": [
- "\n",
- "\n",
- "\n",
- "\n",
- "\n"
- ],
- "text/plain": [
- " >"
- ]
- },
- "metadata": {},
- "output_type": "display_data"
- },
- {
- "data": {
- "text/plain": [
- "(1, 0, True, True, True)"
- ]
- },
- "execution_count": 17,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "c = spot.acc_cond('f')\n",
- "print(c)\n",
- "t = spot.zielonka_tree(c)\n",
- "display(t)\n",
- "t.num_branches(), t.first_branch(), t.has_rabin_shape(), t.has_streett_shape(), t.has_parity_shape()"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 18,
- "id": "plain-modern",
- "metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "(0, t)\n"
- ]
- },
- {
- "data": {
- "image/svg+xml": [
- "\n",
- "\n",
- "\n",
- "\n",
- "\n"
- ],
- "text/plain": [
- " >"
- ]
- },
- "metadata": {},
- "output_type": "display_data"
- },
- {
- "data": {
- "text/plain": [
- "(1, 0, True, True, True)"
- ]
- },
- "execution_count": 18,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "c = spot.acc_cond('t')\n",
- "print(c)\n",
- "t = spot.zielonka_tree(c)\n",
- "display(t)\n",
- "t.num_branches(), t.first_branch(), t.has_rabin_shape(), t.has_streett_shape(), t.has_parity_shape()"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 19,
- "id": "interesting-seller",
- "metadata": {},
- "outputs": [],
- "source": [
- "a = spot.automaton(\"\"\"HOA: v1 name: \"(FGp0 & ((XFp0 & F!p1) | F(Gp1 &\n",
- "XG!p0))) | G(F!p0 & (XFp0 | F!p1) & F(Gp1 | G!p0))\" States: 14 Start:\n",
- "0 AP: 2 \"p1\" \"p0\" Acceptance: 6 (Fin(0) & Fin(1)) | ((Fin(4)|Fin(5)) &\n",
- "(Inf(2)&Inf(3))) properties: trans-labels explicit-labels trans-acc\n",
- "complete properties: deterministic --BODY-- State: 0 [!0] 1 [0] 2\n",
- "State: 1 [!0&!1] 1 {0 1 2 3 5} [0&!1] 3 [!0&1] 4 [0&1] 5 State: 2\n",
- "[0&!1] 2 {1} [!0&1] 4 [!0&!1] 6 [0&1] 7 State: 3 [0&!1] 3 {1 3} [!0&1]\n",
- "4 [!0&!1] 6 {0 1 2 3 5} [0&1] 8 State: 4 [!0&!1] 4 {1 2 3 5} [!0&1] 4\n",
- "{2 4 5} [0&!1] 5 {1 3} [0&1] 5 {4} State: 5 [!0&1] 4 {2 4 5} [0&!1] 5\n",
- "{1 3} [0&1] 8 {2 4} [!0&!1] 9 {1 2 3 5} State: 6 [0&!1] 3 {1 3} [!0&1]\n",
- "4 [0&1] 5 [!0&!1] 10 State: 7 [!0&1] 4 [0&!1] 7 {1 3} [!0&!1] 11 [0&1]\n",
- "12 {0 4} State: 8 [!0&1] 4 {2 4 5} [0&1] 5 {4} [0&!1] 8 {1 3} [!0&!1]\n",
- "11 {1 3 5} State: 9 [!0&1] 4 {2 4 5} [0&!1] 5 {1 3} [0&1] 5 {4}\n",
- "[!0&!1] 11 {1 3 5} State: 10 [!0&1] 4 [0&1] 8 [!0&!1] 10 {0 1 2 3 5}\n",
- "[0&!1] 13 {1 2 3} State: 11 [!0&1] 4 {2 4 5} [0&!1] 8 {1 2 3} [0&1] 8\n",
- "{2 4} [!0&!1] 11 {1 2 3 5} State: 12 [!0&1] 4 [0&1] 7 {0 2 4} [!0&!1]\n",
- "9 [0&!1] 12 {1 3} State: 13 [!0&1] 4 [0&1] 5 [!0&!1] 10 {0 1 3 5}\n",
- "[0&!1] 13 {1 3} --END--\"\"\")"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 20,
- "id": "headed-tampa",
- "metadata": {},
- "outputs": [],
- "source": [
- "b = spot.zielonka_tree_transform(a)"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 21,
- "id": "finite-works",
- "metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "33"
- ]
- },
- "execution_count": 21,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "b.num_states()"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 22,
- "id": "numerical-education",
- "metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "True"
- ]
- },
- "execution_count": 22,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "a.equivalent_to(b)"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 23,
- "id": "useful-helicopter",
- "metadata": {},
- "outputs": [
- {
- "data": {
- "image/svg+xml": [
- "\n",
- "\n",
- "\n",
- "\n",
- "\n"
- ],
- "text/plain": [
- ""
- ]
- },
- "execution_count": 23,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "a.show('.s#')"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 24,
- "id": "imported-wheel",
- "metadata": {
- "scrolled": false
- },
- "outputs": [
- {
- "data": {
- "image/svg+xml": [
- "\n",
- "\n",
- "\n",
- "\n",
- "\n"
- ],
- "text/plain": [
- " >"
- ]
- },
- "execution_count": 24,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "acda = spot.acd(a); acda"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 25,
- "id": "surprised-column",
- "metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "6"
- ]
- },
- "execution_count": 25,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "acda.first_branch(4, 0)"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 26,
- "id": "multiple-minneapolis",
- "metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "(6, 1)"
- ]
- },
- "execution_count": 26,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "acda.step(6, 16)"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 27,
- "id": "addressed-desire",
- "metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "(6, 1)"
- ]
- },
- "execution_count": 27,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "acda.step(6, 18)"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 28,
- "id": "published-pollution",
- "metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "(17, 0)"
- ]
- },
- "execution_count": 28,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "acda.step(6, 17)"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 29,
- "id": "excessive-locking",
- "metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "(8, 1)"
- ]
- },
- "execution_count": 29,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "acda.step(17, 22)"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 30,
- "id": "premier-declaration",
- "metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "(17, 1)"
- ]
- },
- "execution_count": 30,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "acda.step(8, 36)"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 31,
- "id": "modular-metro",
- "metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "3"
- ]
- },
- "execution_count": 31,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "acda.first_branch(1, 3)"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 32,
- "id": "solved-distinction",
- "metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "(3, 1)"
- ]
- },
- "execution_count": 32,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "acda.step(3, 3)"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 33,
- "id": "diagnostic-anthony",
- "metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "21\n",
- "2\n"
- ]
- }
- ],
- "source": [
- "b = spot.acd_transform(a); print(b.num_states()); print(b.num_sets())"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 34,
- "id": "large-shooting",
- "metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "(False, False)"
- ]
- },
- "execution_count": 34,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "acda.has_parity_shape(), acda.has_streett_shape()"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 35,
- "id": "known-plain",
- "metadata": {},
- "outputs": [
- {
- "data": {
- "image/svg+xml": [
- "\n",
- "\n",
- "\n",
- "\n",
- "\n"
- ],
- "text/plain": [
- ""
- ]
- },
- "execution_count": 35,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "b.show('.s')"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 36,
- "id": "stock-physics",
- "metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "True"
- ]
- },
- "execution_count": 36,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "a.equivalent_to(b)"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 37,
- "id": "criminal-northwest",
- "metadata": {},
- "outputs": [
- {
- "data": {
- "image/svg+xml": [
- "\n",
- "\n",
- "\n",
- "\n",
- "\n"
- ],
- "text/plain": [
- ""
- ]
- },
- "execution_count": 37,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "c = spot.automaton(\"\"\"\n",
- "HOA: v1\n",
- "States: 2\n",
- "Start: 0\n",
- "AP: 2 \"p1\" \"p0\"\n",
- "Acceptance: 5 (Fin(0) & (Fin(3)|Fin(4)) & (Inf(1)&Inf(2))) | Inf(3)\n",
- "properties: trans-labels explicit-labels trans-acc complete\n",
- "properties: deterministic stutter-invariant\n",
- "--BODY--\n",
- "State: 0\n",
- "[0&!1] 0 {2 3}\n",
- "[!0&!1] 0 {2 3 4}\n",
- "[!0&1] 1\n",
- "[0&1] 1 {2 4}\n",
- "State: 1\n",
- "[!0&!1] 0 {0 2 3 4}\n",
- "[!0&1] 1 {1}\n",
- "[0&!1] 1 {2 3}\n",
- "[0&1] 1 {1 2 4}\n",
- "--END--\n",
- "\"\"\"); c.show(\".#\")"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 38,
- "id": "balanced-investing",
- "metadata": {},
- "outputs": [
- {
- "data": {
- "image/svg+xml": [
- "\n",
- "\n",
- "\n",
- "\n",
- "\n"
- ],
- "text/plain": [
- " *' at 0x7fd0ba759870> >"
- ]
- },
- "execution_count": 38,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "d = spot.zielonka_tree_transform(c); d"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 39,
- "id": "nutritional-rugby",
- "metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "True"
- ]
- },
- "execution_count": 39,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "c.equivalent_to(d)"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 40,
- "id": "criminal-marking",
- "metadata": {},
- "outputs": [
- {
- "data": {
- "image/svg+xml": [
- "\n",
- "\n",
- "\n",
- "\n",
- "\n"
- ],
- "text/plain": [
- " >"
- ]
- },
- "execution_count": 40,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "spot.acd(c)"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 41,
- "id": "unusual-dependence",
- "metadata": {
- "scrolled": true
- },
- "outputs": [
- {
- "data": {
- "image/svg+xml": [
- "\n",
- "\n",
- "\n",
- "\n",
- "\n"
- ],
- "text/plain": [
- " *' at 0x7fd0ba764240> >"
- ]
- },
- "execution_count": 41,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "d = spot.acd_transform(c); d"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 42,
- "id": "surgical-window",
- "metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "True"
- ]
- },
- "execution_count": 42,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "c.equivalent_to(d)"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 43,
- "id": "attractive-tradition",
- "metadata": {},
- "outputs": [
- {
- "data": {
- "image/svg+xml": [
- "\n",
- "\n",
- "\n",
- "\n",
- "\n"
- ],
- "text/plain": [
- " *' at 0x7fd0ba764750> >"
- ]
- },
- "metadata": {},
- "output_type": "display_data"
- },
- {
- "data": {
- "image/svg+xml": [
- "\n",
- "\n",
- "\n",
- "\n",
- "\n"
- ],
- "text/plain": [
- " *' at 0x7fd0ba7646c0> >"
- ]
- },
- "metadata": {},
- "output_type": "display_data"
- },
- {
- "data": {
- "image/svg+xml": [
- "\n",
- "\n",
- "\n",
- "\n",
- "\n"
- ],
- "text/plain": [
- " *' at 0x7fd0ba759bd0> >"
- ]
- },
- "metadata": {},
- "output_type": "display_data"
- }
- ],
- "source": [
- "e = spot.translate('!(GFa -> (GFb & GF(!b & !Xb)))', 'gen', 'det')\n",
- "f = spot.zielonka_tree_transform(e)\n",
- "f2 = spot.acd_transform(e)\n",
- "display(e,f,f2)"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 44,
- "id": "conventional-aircraft",
- "metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "True"
- ]
- },
- "execution_count": 44,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "e.equivalent_to(f)"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 45,
- "id": "unavailable-making",
- "metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "True"
- ]
- },
- "execution_count": 45,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "e.equivalent_to(f2)"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 46,
- "id": "hispanic-europe",
- "metadata": {},
- "outputs": [],
- "source": [
- "a = spot.translate('GFa -> GF(b & Xb)', 'det', 'gen')"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 47,
- "id": "junior-basis",
- "metadata": {},
- "outputs": [
- {
- "data": {
- "image/svg+xml": [
- "\n",
- "\n",
- "\n",
- "\n",
- "\n"
- ],
- "text/plain": [
- ""
- ]
- },
- "execution_count": 47,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "a.show(\".#\")"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 48,
- "id": "vietnamese-explorer",
- "metadata": {},
- "outputs": [
- {
- "data": {
- "image/svg+xml": [
- "\n",
- "\n",
- "\n",
- "\n",
- "\n"
- ],
- "text/plain": [
- " >"
- ]
- },
- "execution_count": 48,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "theacd = spot.acd(a); theacd"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 49,
- "id": "miniature-attitude",
- "metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "True"
- ]
- },
- "execution_count": 49,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "theacd.has_parity_shape()"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 50,
- "id": "refined-clerk",
- "metadata": {},
- "outputs": [
- {
- "data": {
- "image/svg+xml": [
- "\n",
- "\n",
- "\n",
- "\n",
- "\n"
- ],
- "text/plain": [
- " *' at 0x7fd0ba747c90> >"
- ]
- },
- "execution_count": 50,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "spot.acd_transform(a)"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 51,
- "id": "foster-origin",
- "metadata": {},
- "outputs": [
- {
- "data": {
- "image/svg+xml": [
- "\n",
- "\n",
- "\n",
- "\n",
- "\n"
- ],
- "text/plain": [
- " *' at 0x7fd0b9cfb570> >"
- ]
- },
- "execution_count": 51,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "af = spot.translate('X(p3 | (p4 <-> p8)) R ((Gp4 R p6) W p8)', 'det', 'gen')\n",
- "af"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 52,
- "id": "nuclear-graduation",
- "metadata": {},
- "outputs": [
- {
- "data": {
- "image/svg+xml": [
- "\n",
- "\n",
- "\n",
- "\n",
- "\n"
- ],
- "text/plain": [
- " *' at 0x7fd0b9cfb840> >"
- ]
- },
- "execution_count": 52,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "spot.acd_transform(af)"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 53,
- "id": "german-vienna",
- "metadata": {},
- "outputs": [
- {
- "data": {
- "image/svg+xml": [
- "\n",
- "\n",
- "\n",
- "\n",
- "\n"
- ],
- "text/plain": [
- " *' at 0x7fd0b9cfbc90> >"
- ]
- },
- "execution_count": 53,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "# inherently weak automata become weak\n",
- "w = spot.automaton(\"\"\"HOA: v1\n",
- "States: 2\n",
- "Start: 1\n",
- "AP: 1 \"a\"\n",
- "Acceptance: 2 Inf(0) | Inf(1)\n",
- "properties: trans-labels explicit-labels trans-acc colored complete\n",
- "properties: deterministic inherently-weak\n",
- "--BODY--\n",
- "State: 0\n",
- "[t] 1 {0}\n",
- "State: 1\n",
- "[0] 0 {1}\n",
- "[!0] 1 {0}\n",
- "--END--\"\"\"); w"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 54,
- "id": "chemical-primary",
- "metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "(spot.trival_maybe(), spot.trival(True))"
- ]
- },
- "execution_count": 54,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "w.prop_weak(), w.prop_inherently_weak()"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 55,
- "id": "hispanic-floor",
- "metadata": {},
- "outputs": [],
- "source": [
- "w2 = spot.acd_transform(w)"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 56,
- "id": "bacterial-wiring",
- "metadata": {},
- "outputs": [
- {
- "data": {
- "image/svg+xml": [
- "\n",
- "\n",
- "\n",
- "\n",
- "\n"
- ],
- "text/plain": [
- " *' at 0x7fd0b9cfb5a0> >"
- ]
- },
- "execution_count": 56,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "w2"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 57,
- "id": "central-london",
- "metadata": {},
- "outputs": [
- {
- "data": {
- "text/plain": [
- "(spot.trival(True), spot.trival(True))"
- ]
- },
- "execution_count": 57,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "w2.prop_weak(), w2.prop_inherently_weak()"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": null,
- "id": "adjusted-cause",
- "metadata": {},
- "outputs": [],
- "source": []
- }
- ],
- "metadata": {
- "kernelspec": {
- "display_name": "Python 3",
- "language": "python",
- "name": "python3"
- },
- "language_info": {
- "codemirror_mode": {
- "name": "ipython",
- "version": 3
- },
- "file_extension": ".py",
- "mimetype": "text/x-python",
- "name": "python",
- "nbconvert_exporter": "python",
- "pygments_lexer": "ipython3",
- "version": "3.9.2"
- }
- },
- "nbformat": 4,
- "nbformat_minor": 5
-}
diff --git a/tests/python/zlktree.ipynb b/tests/python/zlktree.ipynb
new file mode 100644
index 000000000..9e4f7f637
--- /dev/null
+++ b/tests/python/zlktree.ipynb
@@ -0,0 +1,6570 @@
+{
+ "cells": [
+ {
+ "cell_type": "code",
+ "execution_count": 1,
+ "id": "found-hurricane",
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ "import spot\n",
+ "spot.setup()"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "fb656100",
+ "metadata": {},
+ "source": [
+ "This notebook demonstrates the implementation of Zielonka Tree and ACD (Alternating Cycle Decomposition)\n",
+ "in Spot. \n",
+ "\n",
+ "These two structures are used to decompose an acceptance condition (or automaton) into trees that alternate accepting and rejecting elements in order to help converting an automaton to parity acceptance. Spot implements those structures, includes some display code to better explore them iteractively, and finally use them to implement a transformation to parity acceptance.\n",
+ "\n",
+ "For a formal tratement of these, in a slightly different formalism, see [Optimal Transformations of Games and Automata Using Muller Conditions](https://arxiv.org/abs/2011.13041) by Casares, Colcombet, and Fijalkow. In Spot those definitions have been adapted to use Emerson-Lei acceptance, and support transitions labeled by multiple colors (the main differences are for the Zielonka Tree, the ACD is almost identical)."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "4e8b5d3f",
+ "metadata": {},
+ "source": [
+ "# Zielonka Tree\n",
+ "\n",
+ "The Zielonka tree is built from an acceptance formula and is labeled by sets of colors. The root contains all colors used in the formula. If seing infinitely all colors of one node would satisfy the acceptance condition, we say that the node is accepting and draw it with an ellipse, otherwise is is rejecting and drawn with a rectangle. The children of an accepting (resp. rejecting) node, are the largest subsets of colors that are rejecting (resp. accepting).\n",
+ "\n",
+ "Here is an example:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 2,
+ "id": "b330dcc5",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text/plain": [
+ " >"
+ ]
+ },
+ "execution_count": 2,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "c = spot.acc_cond('Fin(0)&Inf(1)&(Inf(2)|Fin(3)) | (Inf(0)|Fin(1))&Fin(2)&Inf(3)')\n",
+ "t = spot.zielonka_tree(c)\n",
+ "t"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "d7629725",
+ "metadata": {},
+ "source": [
+ "Above we can see that `{0,1,2,3}` is a rejecting root, but it has two accepting maximal subsets: `{1,2,3}` and `{0,1,3}`. Similarly, `{1,2,3}` has two rejecting maximal subsets: `{2,3}` and `{1,3}`.\n",
+ "\n",
+ "The leaves of this tree have some additional numbers in angle brackets: those are the node numbers. Each node has a number (it can be seen by hovering over it with the mouse), but those leaf numbers play a particular role when the tree is used to paritize an automaton.\n",
+ "\n",
+ "This tree is also layered: all nodes in each layers are alternatively rejecting and accepting. Layers are numbered incrementally from 0 at the root. In this example, leaves are in layer 3. Since it is conventional to put the root at the top, we will say that a node is high in the tree when it has a small level.\n",
+ "\n",
+ "In this example, odd levels are accepting: we say the tree is odd. On another example, it could be the other way arround. The `is_even()` method tells us which way it is."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 3,
+ "id": "ef1a0061",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "False"
+ ]
+ },
+ "execution_count": 3,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "t.is_even()"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "15fbd4e6",
+ "metadata": {},
+ "source": [
+ "The number of leaves, and the number of the left-most leaf can be found with the following functions:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 4,
+ "id": "ad093868",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "(6, 7)"
+ ]
+ },
+ "execution_count": 4,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "t.num_branches(), t.first_branch()"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "de4cdc45",
+ "metadata": {},
+ "source": [
+ "The `step()` methods takes one leaf L, one set of colors S, and returns a pair: (leaf, level).\n",
+ "It works as follows: starting from node L, it walks up the tree until it has seen all colors in S, and then return the left-most leaf of the *next* branch of the node it has seen (assuming branches are ordered circularly from left to right). The level returned is that of the highest node seen.\n",
+ "\n",
+ "We refer to the process performed by `step(L,S)` as *reading S from L*. \n",
+ "\n",
+ "For instance reading `[3]` from 7 does not change the leaf, since that leaf is already labeled by `{3}`. The level emitted is 3, since that's the level of 7."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 5,
+ "id": "f4795cff",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "(7, 3)"
+ ]
+ },
+ "execution_count": 5,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "t.step(7, [3])"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "4c3bf70b",
+ "metadata": {},
+ "source": [
+ "Reading `[3]` from 8, would however move to leave 9 and emit level 2. Indeed, color 3 is not recognized by 8, so we move up to node 4 (the one labelled by `{1,3}`), emit its level (2), and go down to the left-most leaf of the next branch."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 6,
+ "id": "27899524",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "(9, 2)"
+ ]
+ },
+ "execution_count": 6,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "t.step(8, [3])"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "0d865f30",
+ "metadata": {},
+ "source": [
+ "If we read `[0,2]` from 9, we will have to go all the way up to the root (emitting 0) and then down to leaf 10:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 7,
+ "id": "94d01547",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "(10, 0)"
+ ]
+ },
+ "execution_count": 7,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "t.step(9, [0,2])"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "8b6b3928",
+ "metadata": {},
+ "source": [
+ "Now, let's take this a *step* further, and chain multiple steps, by reading a sequence of Sᵢ and producing a sequence of levels."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 8,
+ "id": "43b17b85",
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ "def steps(tree, leaf, seq_of_s):\n",
+ " seq_of_lvl = []\n",
+ " for s in seq_of_s:\n",
+ " leaf, lvl = tree.step(leaf, s)\n",
+ " seq_of_lvl.append(lvl)\n",
+ " return leaf, seq_of_lvl"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 9,
+ "id": "1d411142",
+ "metadata": {},
+ "outputs": [
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "(10, [1, 0, 2, 2, 1, 1, 3, 1, 1, 3, 1, 1])\n",
+ "(9, [1, 2, 2, 2, 2, 2, 2, 2])\n"
+ ]
+ }
+ ],
+ "source": [
+ "print(steps(t, 7, [[1],[0],[3],[1],[0],[3],[1],[0],[3],[1],[0],[3]]))\n",
+ "print(steps(t, 7, [[1],[3],[1],[3],[1],[3],[1],[3]]))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "656e05f4",
+ "metadata": {},
+ "source": [
+ "If we imagine an run looping on tree transitions labeled by `[1]`, `[0]`, `[3]`, we know (from the original acceptance condition) that it should be accepting. Infinite repetition of the `step()` procedure will emit many levels, but the smallest level we see infinitely often is `1`. It corresponds to node 2, labeled by `{0,1,3}`: this is the highest node we visit infinitely often while steping through this tree in a loop.\n",
+ "\n",
+ "Similarly, a loop of two transitions labeled by `[1]` and `[3]` should be rejecting. Stepping through the tree will emit infinitely many 2, a rejecting level."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "5c7014e9",
+ "metadata": {},
+ "source": [
+ "All of this can be used to transform an automaton with arbitrary acceptance into a parity automaton, where the emitted levels will correspond to the priorities of the parity automaton.\n",
+ "\n",
+ "The states of the new automaton will be pairs of states of the form `(original state, leaf)`. If the input edge `(src,dst)` has colors `S`, then the output edge `((src,leaf),(dst,nextleaf))` will have priority `L` where `L` and `nextleaf` are computed as `(nextleaf,L)=t.step(leaf, S)`. The leaf used for the initial state does not really matter, we use the left-most one."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "2750cb1d",
+ "metadata": {},
+ "source": [
+ "Let's create a random automaton with this example acceptance condition, and paritize it:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 10,
+ "id": "0b9511da",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text/plain": [
+ " *' at 0x7fa2681f9db0> >"
+ ]
+ },
+ "execution_count": 10,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "a1 = spot.automaton(\"randaut -Q4 --colored -e.7 -A '{}' 2 |\".format(c.get_acceptance()))\n",
+ "a1"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 11,
+ "id": "499c26d8",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text/plain": [
+ " *' at 0x7fa2681f96f0> >"
+ ]
+ },
+ "execution_count": 11,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "p1 = spot.zielonka_tree_transform(a1)\n",
+ "p1.copy_state_names_from(a1)\n",
+ "p1"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "ea452913",
+ "metadata": {},
+ "source": [
+ "Here the parity automaton output has as many proprities as there are levels in the Zielonka tree.\n",
+ "\n",
+ "The call to `copy_state_names_from()` above causes the states to be labeled by strings of the form `orig#leaf` when `orig` is the original state number, and `leaf` is a leaf of the Zielonka tree.\n",
+ "\n",
+ "Since this notebook is part of our test-suite, let us also make sure those automata are equivalent. "
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 12,
+ "id": "934e5cd5",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "True"
+ ]
+ },
+ "execution_count": 12,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "spot.are_equivalent(p1, a1)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "da8d9e97",
+ "metadata": {},
+ "source": [
+ "Note that `a1` above was generated as a so-called \"colored\" automaton, i.e., each edge has exactly one color. But the transformation also works when edges have arbitrary and possibly empty subsets of colors. In that case, reading a transition without color may emit a level that is not in the Zielonka tree, as if an additional imaginary layer labeled with the empty set was below the tree: we do not store this level for simplicity, but the `step()` function is aware of that."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 13,
+ "id": "87eb80e1",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text/plain": [
+ " *' at 0x7fa2681f98d0> >"
+ ]
+ },
+ "execution_count": 13,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "a2 = spot.automaton(\"randaut -Q3 -e.8 --seed=4 -A '{}' 2 |\".format(c.get_acceptance()))\n",
+ "a2"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 14,
+ "id": "201acd7e",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text/plain": [
+ " *' at 0x7fa268204300> >"
+ ]
+ },
+ "execution_count": 14,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "p2 = spot.zielonka_tree_transform(a2)\n",
+ "p2.copy_state_names_from(a2)\n",
+ "p2"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "9bf70138",
+ "metadata": {},
+ "source": [
+ "The shape of the Zielonka tree (and later of the ACD), can also tell us if the acceptance condition can be converted into Rabin/Streett/parity without changing the automaton structure. This follows from the following properties:\n",
+ "\n",
+ "- an automaton is Rabin-type iff the union of any two accepting cycle is necessarily accepting\n",
+ "- an automaton is Streett-type iff the union of two rejecting cycle is necessarily rejecting\n",
+ "- an automaton is parity-type iff it is Rabin-type and Streett-type\n",
+ "\n",
+ "Here, X-type means that the acceptance condition of the automaton can be changed into X without changing the transition structure (just by coloring it differently). The Zielonka tree does not really look at the automaton, however its shape can still implies some typeness:\n",
+ "\n",
+ "- an automaton is Rabin-type if (not iff) accepting nodes of the Zielonka tree have at most one child\n",
+ "- an automaton is Street-type if (not iff) rejecting nodes of the Zielonka tree have at most one child\n",
+ "\n",
+ "The following methods provide this information:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 15,
+ "id": "25ae5666",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "(False, False, False)"
+ ]
+ },
+ "execution_count": 15,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "t.has_rabin_shape(), t.has_streett_shape(), t.has_parity_shape()"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "147a71a6",
+ "metadata": {},
+ "source": [
+ "Let's look at some examples:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 16,
+ "id": "e24c005d",
+ "metadata": {
+ "scrolled": false
+ },
+ "outputs": [
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "(Fin(0) & Inf(1)) | (Fin(2) & Inf(3)) | (Fin(4) & Inf(5)) : True False False\n"
+ ]
+ },
+ {
+ "data": {
+ "image/svg+xml": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text/plain": [
+ " >"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "(Fin(0) | Inf(1)) & (Fin(2) | Inf(3)) & (Fin(4) | Inf(5)) : False True False\n"
+ ]
+ },
+ {
+ "data": {
+ "image/svg+xml": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text/plain": [
+ " >"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "Fin(0) & (Inf(1) | (Fin(2) & (Inf(3) | Fin(4)))) : True True True\n"
+ ]
+ },
+ {
+ "data": {
+ "image/svg+xml": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text/plain": [
+ " >"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "(Inf(0) & Fin(1)) | (Inf(2) & Fin(3) & Fin(4)) : True False False\n"
+ ]
+ },
+ {
+ "data": {
+ "image/svg+xml": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text/plain": [
+ " >"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "f : True True True\n"
+ ]
+ },
+ {
+ "data": {
+ "image/svg+xml": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text/plain": [
+ " >"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "t : True True True\n"
+ ]
+ },
+ {
+ "data": {
+ "image/svg+xml": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text/plain": [
+ " >"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "for ct in ('Rabin 3', 'Streett 3', 'parity min odd 5', \n",
+ " 'Inf(0)&Fin(1) | (Inf(2)&Fin(3)&Fin(4))', 'f', 't'):\n",
+ " cond = spot.acc_cond(ct)\n",
+ " tcond = spot.zielonka_tree(cond)\n",
+ " print(cond.get_acceptance(), \":\", tcond.has_rabin_shape(), \n",
+ " tcond.has_streett_shape(), tcond.has_parity_shape());\n",
+ " display(tcond)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "75838579",
+ "metadata": {},
+ "source": [
+ "# Alternating Cycle Decomposition\n",
+ "\n",
+ "We now turn to the ACD, which extends the Zielonka tree to take the automaton structure into account. Instead of storing subsets of colors, it stores SCCs (not necessarily maximal). In Spot, those SCCs are stored as bitvectors of edges. The principle is similar: instead of one tree, we are building a forest, with one root per non-trivial maximal SCC. The root of each tree is labeled by all the transitions in this maximal SCC: if such a huge cycle is accepting the node is said accepting and drawn as an ellipse, otherwise it is rejecting and drawn as a rectangle. For children, we look for maximal subsets of cycles that can be rejecting (if the parent was accepting), or accepting (if the parent was rejecting). \n",
+ "\n",
+ "In other words all nodes correspond to SCCs that may not be maximal from a graph point of view, but that are maximal with respect to their accepting or rejecting status: adding more cycles to it would change that status."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 17,
+ "id": "ea3488b1",
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ "a3 = spot.automaton(\"\"\"HOA: v1 name: \"(FGp0 & ((XFp0 & F!p1) | F(Gp1 &\n",
+ "XG!p0))) | G(F!p0 &\\n(XFp0 | F!p1) & F(Gp1 | G!p0))\" States: 10 Start:\n",
+ "0 AP: 2 \"p0\" \"p1\" Acceptance: 6 (Fin(0) & Fin(1)) | ((Fin(4)|Fin(5)) &\n",
+ "(Inf(2)&Inf(3))) properties: trans-labels explicit-labels trans-acc\n",
+ "complete properties: deterministic --BODY-- State: 0 [!0&!1] 0 {0 1 2\n",
+ "3 5} [!0&1] 1 [0&!1] 2 [0&1] 3 State: 1 [!0&1] 1 {1 3} [0&!1] 2\n",
+ "[!0&!1] 4 {0 1 2 3 5} [0&1] 5 State: 2 [!0&!1] 2 {1 2 3 5} [0&!1] 2 {2\n",
+ "4 5} [!0&1] 3 {1 3} [0&1] 3 {4} State: 3 [0&!1] 2 {2 4 5} [!0&1] 3 {1\n",
+ "3} [0&1] 5 {2 4} [!0&!1] 6 {1 2 3 5} State: 4 [!0&1] 1 {1 3} [0&!1] 2\n",
+ "[0&1] 3 [!0&!1] 7 State: 5 [0&!1] 2 {2 4 5} [0&1] 3 {4} [!0&1] 5 {1 3}\n",
+ "[!0&!1] 8 {1 3 5} State: 6 [0&!1] 2 {2 4 5} [!0&1] 3 {1 3} [0&1] 3 {4}\n",
+ "[!0&!1] 8 {1 3 5} State: 7 [0&!1] 2 [0&1] 5 [!0&!1] 7 {0 1 2 3 5}\n",
+ "[!0&1] 9 {1 2 3} State: 8 [0&!1] 2 {2 4 5} [!0&1] 5 {1 2 3} [0&1] 5 {2\n",
+ "4} [!0&!1] 8 {1 2 3 5} State: 9 [0&!1] 2 [0&1] 3 [!0&!1] 7 {0 1 3 5}\n",
+ "[!0&1] 9 {1 3} --END--\"\"\")"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "cb546bc2",
+ "metadata": {},
+ "source": [
+ "Here is the ACD for automaton `a3`, displayed below a copy of the automaton. Note that the automaton and ACD are linked interactively: you may click on nodes of the ACD to highlight the cycles it stores, and you may click on a state or an edge in the automaton to highlight to relevant ACD nodes (it is easier to click on edge labels than on edges)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 18,
+ "id": "fad721c0",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text/html": [
+ "
\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "
\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "
"
+ ],
+ "text/plain": [
+ " >"
+ ]
+ },
+ "execution_count": 18,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "theacd = spot.acd(a3); theacd"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "0f2f00c4",
+ "metadata": {},
+ "source": [
+ "The nodes of the ACD represent various bits of informations. First, the root of each tree shows the number of the maximal SCC (as computed by `spot.scc_info`). Trivial maximal SCCs (without cycles) are omitted from the construction.\n",
+ "\n",
+ "The numbers after `T:` list the edges that belong to the strongly connected component. The numbers are simply the indices of those edges in the automaton. Between braces are the colors covered by all those edges, to decide if a cycle formed by all these edges would be accepting. The numbers after `Q:` are the states touched by those edges. `lvl:` indicates the level of each node. Since some trees can have accepting roots while others have rejecting roots, the levels of some tree have been shifted down (i.e., the root start at levl 1 instead of 0) to ensure that all trees use the same parity. The parity of the decomposition (i.e., whether even levels are accepting) is indicated by the `is_even()` method."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 19,
+ "id": "859a993a",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "False"
+ ]
+ },
+ "execution_count": 19,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "theacd.is_even()"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "3a3db431",
+ "metadata": {},
+ "source": [
+ "Finally, the leaves have their node number indicated between angle brackets, but again, node numbers can be obtained by hovering over the node with the mouse. This construction may step in more that just those indicated leaves because it will consider subtrees of the ACD.\n",
+ "\n",
+ "For each state of the original automaton, there exists a subtree in the ACD formed by all the node whose `Q:` contain that state. In the display of `theacd` above, you can click on any state of the input automaton to highlight the corresponding subtree of the ACD."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "6595333d",
+ "metadata": {},
+ "source": [
+ "The `step()` method works similarly to Zielonka trees, except it uses edge number instead of colors. It is given a node of the ACD and the number of an edge whose source state touched belong to `Q:` in the current node. Then it walks up the tree until it finds a node that contains the given edge, emit the level of that node, and returns the left-most node of the next-branch in the sub-tree associated to the destination state.\n",
+ "\n",
+ "For instance, let's consider the edges 2->3 and 3->2 in `a1`. There are actually two edges going from 2 to 3. Hovering above those arrows tells us the number of these edges:\n",
+ " - 2->3 with {1,3} is edge 11\n",
+ " - 2->3 with {4} is edge 12\n",
+ " - 3->2 with {2,4,5} is edge 13\n",
+ " \n",
+ "Let us assume we are in node 4 of the ACD (a node that contains state 2) and want to step through edges 12 and 13:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 20,
+ "id": "a8bd0844",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "(4, 1)"
+ ]
+ },
+ "execution_count": 20,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "theacd.step(4, 12)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 21,
+ "id": "93116a05",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "(4, 1)"
+ ]
+ },
+ "execution_count": 21,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "theacd.step(4, 13)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "1c6d4fe9",
+ "metadata": {},
+ "source": [
+ "In both case, we stay in node 4 and emit level 1, this is the level of node 4, which contains both edges.\n",
+ "\n",
+ "If we were to iterate through edges 11 and 13 instead, the story would be different:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 22,
+ "id": "23940b6a",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "(12, 0)"
+ ]
+ },
+ "execution_count": 22,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "theacd.step(4, 11)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 23,
+ "id": "de7cbd02",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "(7, 0)"
+ ]
+ },
+ "execution_count": 23,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "theacd.step(12, 13)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 24,
+ "id": "8b0305d4",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "(13, 0)"
+ ]
+ },
+ "execution_count": 24,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "theacd.step(7, 11)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 25,
+ "id": "4f0a10f5",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "(4, 0)"
+ ]
+ },
+ "execution_count": 25,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "theacd.step(13, 13)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "ad201f45",
+ "metadata": {
+ "slideshow": {
+ "slide_type": "slide"
+ }
+ },
+ "source": [
+ "And then it would loop again. \n",
+ "\n",
+ "Let's consider the first step. Node 4 does not contains edge 11, so we move up the tree until we find node 0 that contains it, and emit level 0. Then the destination of edge 11 is 3, so we consider the subtree associated to 3 (clicking on state 3 shows us this is the tree that has nodes 4,7,13 as leaves) and return the left-most node of the next branch: 12.\n",
+ "\n",
+ "When we read edge 13 from node 12, go all the way up to node 0 again, and consider the left-most node of the next branch in the tree for the destination 2: that's node 7."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "04d7cc51",
+ "metadata": {},
+ "source": [
+ "The initial node we use to start this process can be any node that contains this state. The `first_branch(s)` method returns the left-most node containing state `s`."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 26,
+ "id": "2bd04c1f",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "4"
+ ]
+ },
+ "execution_count": 26,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "theacd.first_branch(2)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "1015abb6",
+ "metadata": {},
+ "source": [
+ "This `first_branch()` method is actually being used when `step()` is used to take an edge between two SCCs. In that case the edge does not appear in the ACD, and `step()` will return the `first_branch()` for its destination, and level 0."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "b89a6186",
+ "metadata": {},
+ "source": [
+ "An automaton can be paritized using ACD following a procedure similar to Zielonka tree, with this more complex stepping process."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 27,
+ "id": "e28035e8",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text/plain": [
+ " *' at 0x7fa2681f9d20> >"
+ ]
+ },
+ "execution_count": 27,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "p3 = spot.acd_transform(a3, True)\n",
+ "p3.copy_state_names_from(a3)\n",
+ "p3"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "f039aeaa",
+ "metadata": {},
+ "source": [
+ "Note how the loops `2#4 → 3#4 → 2#4` and `2#4 → 3#12 → 2#7 → 3#13 → 2#4` corresponds to the two cycles stepped though before."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 28,
+ "id": "numerical-education",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "True"
+ ]
+ },
+ "execution_count": 28,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "a3.equivalent_to(p3)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "07aaab3a",
+ "metadata": {},
+ "source": [
+ "By default, the construction will try to save colors by not emitting colors between SCCs, and not emitting colors for the largest level of an SCC when the parity allows it. So this automaton can actually be paritized with two colors:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 29,
+ "id": "3e239a0c",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text/plain": [
+ " *' at 0x7fa2682f4c60> >"
+ ]
+ },
+ "execution_count": 29,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "p3 = spot.acd_transform(a3) # second argument defaults to False\n",
+ "p3.copy_state_names_from(a3)\n",
+ "assert a3.equivalent_to(p3)\n",
+ "p3\n"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "f14ee428",
+ "metadata": {},
+ "source": [
+ "This transformation can have substantiually fewer states than the one based on Zielonka tree, because the branches are actually restricted to only those that matter for a given state."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 30,
+ "id": "4f62e612",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "15"
+ ]
+ },
+ "execution_count": 30,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "p3.num_states()"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 31,
+ "id": "20f2a45c",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "27"
+ ]
+ },
+ "execution_count": 31,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "spot.zielonka_tree_transform(a3).num_states()"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "e3d0ff64",
+ "metadata": {},
+ "source": [
+ "We can decide Rabin, Streett, and parity-typeness with the following methods. However building the entire ACD to decide that is a bit overkill, especially in case of a negative answer."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 32,
+ "id": "2d0bbc0b",
+ "metadata": {},
+ "outputs": [
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "False False False\n"
+ ]
+ }
+ ],
+ "source": [
+ "print(theacd.has_rabin_shape(), theacd.has_streett_shape(), theacd.has_parity_shape())"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "15f094c0",
+ "metadata": {},
+ "source": [
+ "# More examples\n",
+ "\n",
+ "These additional examples also contribute to our test suite."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 33,
+ "id": "criminal-northwest",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text/plain": [
+ " *' at 0x7fa268211ae0> >"
+ ]
+ },
+ "execution_count": 33,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "c = spot.automaton(\"\"\"\n",
+ "HOA: v1\n",
+ "States: 2\n",
+ "Start: 0\n",
+ "AP: 2 \"p1\" \"p0\"\n",
+ "Acceptance: 5 (Fin(0) & (Fin(3)|Fin(4)) & (Inf(1)&Inf(2))) | Inf(3)\n",
+ "properties: trans-labels explicit-labels trans-acc complete\n",
+ "properties: deterministic stutter-invariant\n",
+ "--BODY--\n",
+ "State: 0\n",
+ "[0&!1] 0 {2 3}\n",
+ "[!0&!1] 0 {2 3 4}\n",
+ "[!0&1] 1\n",
+ "[0&1] 1 {2 4}\n",
+ "State: 1\n",
+ "[!0&!1] 0 {0 2 3 4}\n",
+ "[!0&1] 1 {1}\n",
+ "[0&!1] 1 {2 3}\n",
+ "[0&1] 1 {1 2 4}\n",
+ "--END--\n",
+ "\"\"\"); c"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 34,
+ "id": "63c7c062",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text/plain": [
+ " >"
+ ]
+ },
+ "execution_count": 34,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "spot.zielonka_tree(c.acc())"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 35,
+ "id": "balanced-investing",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text/plain": [
+ " *' at 0x7fa2682117b0> >"
+ ]
+ },
+ "execution_count": 35,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "d = spot.zielonka_tree_transform(c); d"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 36,
+ "id": "nutritional-rugby",
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ "assert c.equivalent_to(d)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 37,
+ "id": "criminal-marking",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text/html": [
+ "