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

zlktree: implement ACD and its transform

Browse source 
A quick and dirty implementation of the Alternating Cycle
Decomposition of the casares.21.icalp paper.

* spot/twaalgos/genem.cc, spot/twaalgos/genem.hh
(maximal_accepting_loops_for_scc): New function.
* spot/twaalgos/sccinfo.cc,
spot/twaalgos/sccinfo.hh (scc_and_mark_filter): Add a possibility to
specify a mask of transition to filter.
* spot/twaalgos/zlktree.hh, spot/twaalgos/zlktree.cc (acd): New class.
(acd_transform): New function.
* python/spot/__init__.py: Add SVG rendering for acd.
* tests/python/_zlktree.ipynb: Play with acd and acd_transform.
* tests/python/toparity.py: Add more tests to compare the
sizes of acd_transform and to_parity.
* NEWS: Mention this new feature.
This commit is contained in:
Alexandre Duret-Lutz 2021-08-09 15:22:17 +02:00
parent 8c5bb6c2eb
commit 26f2179805
10 changed files with 4657 additions and 144 deletions
Download patch file Download diff file Expand all files Collapse all files

12
NEWS
View file

@ -232,9 +232,15 @@ New in spot 2.9.8.dev (not yet released)
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. This is based on
a paper by Casares et al. (ICALP'21). Its python binding will
display the tree graphically.
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.
Python:

8
python/spot/__init__.py
View file

@ -436,6 +436,14 @@ class zielonka_tree:
self.dot(ostr)
return _ostream_to_svg(ostr)
@_extend(acd)
class acd:
def _repr_svg_(self):
"""Output the ACD as SVG"""
ostr = ostringstream()
self.dot(ostr)
return _ostream_to_svg(ostr)
def automata(*sources, timeout=None, ignore_abort=True,
trust_hoa=True, no_sid=False, debug=False,

111
spot/twaalgos/genem.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2017-2020 Laboratoire de Recherche et Developpement
// Copyright (C) 2017-2021 Laboratoire de Recherche et Developpement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -44,55 +44,82 @@ namespace spot
namespace
{
template <bool EarlyStop, typename Extra>
static bool
is_scc_empty(const scc_info& si, unsigned scc,
const acc_cond& autacc, twa_run_ptr run,
const acc_cond& autacc, Extra extra,
acc_cond::mark_t tocut = {});
static bool
scc_split_check(const scc_info& si, unsigned scc, const acc_cond& acc,
twa_run_ptr run, acc_cond::mark_t tocut)
{
scc_and_mark_filter filt(si, scc, tocut);
filt.override_acceptance(acc);
scc_info upper_si(filt, scc_info_options::STOP_ON_ACC);
template <bool EarlyStop, typename Extra>
static bool
scc_split_check_filtered(const scc_info& upper_si, const acc_cond& acc,
Extra extra, acc_cond::mark_t tocut)
{
if constexpr (EarlyStop)
{
const int accepting_scc = upper_si.one_accepting_scc();
if (accepting_scc >= 0)
{
if (run)
upper_si.get_accepting_run(accepting_scc, run);
if (extra)
upper_si.get_accepting_run(accepting_scc, extra);
return false;
}
if (!acc.uses_fin_acceptance())
return true;
}
unsigned nscc = upper_si.scc_count();
for (unsigned scc = 0; scc < nscc; ++scc)
if (!is_scc_empty(upper_si, scc, acc, run, tocut))
if (!is_scc_empty<EarlyStop, Extra>(upper_si, scc, acc, extra, tocut))
if constexpr (EarlyStop)
return false;
return true;
}
template <bool EarlyStop, typename Extra>
static bool
scc_split_check(const scc_info& si, unsigned scc, const acc_cond& acc,
Extra extra, acc_cond::mark_t tocut)
{
scc_and_mark_filter filt(si, scc, tocut);
filt.override_acceptance(acc);
scc_info upper_si(filt, EarlyStop
? scc_info_options::STOP_ON_ACC
: scc_info_options::TRACK_STATES);
return scc_split_check_filtered<EarlyStop>(upper_si, acc, extra, tocut);
}
template <bool EarlyStop, typename Extra>
static bool
is_scc_empty(const scc_info& si, unsigned scc,
const acc_cond& autacc, twa_run_ptr run,
const acc_cond& autacc, Extra extra,
acc_cond::mark_t tocut)
{
if (si.is_rejecting_scc(scc))
return true;
if constexpr (!EarlyStop)
if (si.is_maximally_accepting_scc(scc))
{
extra(si, scc);
return false;
}
acc_cond::mark_t sets = si.acc_sets_of(scc);
acc_cond acc = autacc.restrict_to(sets);
acc = acc.remove(si.common_sets_of(scc), false);
if (SPOT_LIKELY(genem_version == spot29))
if (SPOT_LIKELY(genem_version == spot29 || !EarlyStop))
do
{
acc_cond::acc_code rest = acc_cond::acc_code::f();
if (EarlyStop)
{
for (const acc_cond& disjunct: acc.top_disjuncts())
if (acc_cond::mark_t fu = disjunct.fin_unit())
{
if (!scc_split_check
(si, scc, disjunct.remove(fu, true), run, fu))
if (!scc_split_check<EarlyStop, Extra>
(si, scc, disjunct.remove(fu, true), extra, fu))
if constexpr (EarlyStop)
return false;
}
else
@ -101,13 +128,22 @@ namespace spot
}
if (rest.is_f())
break;
}
else
{
rest = acc.get_acceptance();
if (acc_cond::mark_t fu = rest.fin_unit())
return scc_split_check<EarlyStop, Extra>
(si, scc, rest.remove(fu, true), extra, fu);
}
acc_cond subacc(acc.num_sets(), std::move(rest));
int fo = subacc.fin_one();
assert(fo >= 0);
// Try to accept when Fin(fo) == true
acc_cond::mark_t fo_m = {(unsigned) fo};
if (!scc_split_check
(si, scc, subacc.remove(fo_m, true), run, fo_m))
if (!scc_split_check<EarlyStop, Extra>
(si, scc, subacc.remove(fo_m, true), extra, fo_m))
if constexpr (EarlyStop)
return false;
// Try to accept when Fin(fo) == false
acc = subacc.force_inf(fo_m);
@ -118,8 +154,9 @@ namespace spot
for (const acc_cond& disjunct: acc.top_disjuncts())
if (acc_cond::mark_t fu = disjunct.fin_unit())
{
if (!scc_split_check
(si, scc, disjunct.remove(fu, true), run, fu))
if (!scc_split_check<EarlyStop, Extra>
(si, scc, disjunct.remove(fu, true), extra, fu))
if constexpr (EarlyStop)
return false;
}
else
@ -129,12 +166,14 @@ namespace spot
assert(fo >= 0);
// Try to accept when Fin(fo) == true
acc_cond::mark_t fo_m = {(unsigned) fo};
if (!scc_split_check
(si, scc, disjunct.remove(fo_m, true), run, fo_m))
if (!scc_split_check<EarlyStop, Extra>
(si, scc, disjunct.remove(fo_m, true), extra, fo_m))
if constexpr (EarlyStop)
return false;
// Try to accept when Fin(fo) == false
if (!is_scc_empty(si, scc, disjunct.force_inf(fo_m),
run, tocut))
if (!is_scc_empty<EarlyStop, Extra>
(si, scc, disjunct.force_inf(fo_m), extra, tocut))
if constexpr (EarlyStop)
return false;
}
}
@ -177,7 +216,7 @@ namespace spot
unsigned nscc = si.scc_count();
for (unsigned scc = 0; scc < nscc; ++scc)
if (!is_scc_empty(si, scc, aut_acc, run))
if (!is_scc_empty<true, twa_run_ptr>(si, scc, aut_acc, run))
return false;
return true;
}
@ -215,7 +254,8 @@ namespace spot
{
if (si.is_accepting_scc(scc))
return false;
return is_scc_empty(si, scc, si.get_aut()->acc(), nullptr);
return is_scc_empty<true, twa_run_ptr>
(si, scc, si.get_aut()->acc(), nullptr);
}
bool
@ -224,7 +264,24 @@ namespace spot
{
if (si.is_trivial(scc))
return true;
return scc_split_check(si, scc, forced_acc, nullptr, {});
return scc_split_check<true, twa_run_ptr>
(si, scc, forced_acc, nullptr, {});
}
bool
maximal_accepting_loops_for_scc(const scc_info& si, unsigned scc,
const acc_cond& forced_acc,
const std::vector<bool>& keep,
std::function<void(const scc_info&,
unsigned)> callback)
{
if (si.is_trivial(scc))
return false;
scc_and_mark_filter filt(si, scc, {}, keep);
filt.override_acceptance(forced_acc);
scc_info upper_si(filt, scc_info_options::TRACK_STATES);
return !scc_split_check_filtered<false>(upper_si, forced_acc, callback, {});
}
}

23
spot/twaalgos/genem.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2017-2020 Laboratoire de Recherche et Developpement
// Copyright (C) 2017-2021 Laboratoire de Recherche et Developpement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -62,6 +62,27 @@ namespace spot
generic_emptiness_check_for_scc(const scc_info& si, unsigned scc,
const acc_cond& forced_acc);
#ifndef SWIG
/// \ingroup emptiness_check_algorithms
/// \brief Compute set of maximal accepting loops in one SCC,
/// for any acceptance condition.
///
/// This computes all maximal subsets of the edges of an SCC
/// that form accepting (sub) SCCs. For each such subset, the
/// \a callback function is called with `(si, num)`, such that
/// `si->inner_edges_of(num)` lists the relevant edges.
///
/// The search is restricted to a set of edges of the given SCC
/// for which \a keep (an array indexed by edge numbers) is true.
///
/// Returns false iff no accepting loop where found.
SPOT_API bool
maximal_accepting_loops_for_scc(const scc_info& si, unsigned scc,
const acc_cond& forced_acc,
const std::vector<bool>& keep,
std::function<void(const scc_info&,
unsigned)> callback);
#endif
/// \ingroup emptiness_check_algorithms
///

28
spot/twaalgos/sccinfo.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2014-2020 Laboratoire de Recherche et Développement
// Copyright (C) 2014-2021 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -854,6 +854,16 @@ namespace spot
return res;
}
scc_info::edge_filter_choice
scc_and_mark_filter::filter_mark_
(const twa_graph::edge_storage_t& e, unsigned, void* data)
{
auto& d = *reinterpret_cast<scc_and_mark_filter*>(data);
if (d.cut_sets_ & e.acc)
return scc_info::edge_filter_choice::cut;
return scc_info::edge_filter_choice::keep;
}
scc_info::edge_filter_choice
scc_and_mark_filter::filter_scc_and_mark_
(const twa_graph::edge_storage_t& e, unsigned dst, void* data)
@ -867,13 +877,19 @@ namespace spot
}
scc_info::edge_filter_choice
scc_and_mark_filter::filter_mark_
scc_and_mark_filter::filter_scc_and_mark_and_edges_
(const twa_graph::edge_storage_t& e, unsigned, void* data)
{
auto& d = *reinterpret_cast<scc_and_mark_filter*>(data);
if (d.cut_sets_ & e.acc)
return scc_info::edge_filter_choice::cut;
return scc_info::edge_filter_choice::keep;
auto* si = d.lower_si_;
if (si->scc_of(e.dst) != si->scc_of(e.src))
return edge_filter_choice::ignore;
if (auto f = si->get_filter())
if (auto choice = f(e, e.dst, si->get_filter_data());
choice != edge_filter_choice::keep)
return choice;
if (!(*d.keep_)[d.aut_->edge_number(e)] || (d.cut_sets_ & e.acc))
return edge_filter_choice::cut;
return edge_filter_choice::keep;
}
}

35
spot/twaalgos/sccinfo.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2014-2020 Laboratoire de Recherche et Développement
// Copyright (C) 2014-2021 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -525,7 +525,7 @@ namespace spot
return filter_;
}
const void* get_filter_data() const
void* get_filter_data() const
{
return filter_data_;
}
@ -668,6 +668,13 @@ namespace spot
return node(scc).is_rejecting();
}
/// \brief Whether a cycle going through all edges of the SCC is
/// accepting.
bool is_maximally_accepting_scc(unsigned scc) const
{
return aut_->acc().accepting(acc_sets_of(scc));
}
/// \brief Study the SCCs that are currently reported neither as
/// accepting nor as rejecting because of the presence of Fin sets
///
@ -785,13 +792,19 @@ namespace spot
const_twa_graph_ptr aut_;
acc_cond old_acc_;
bool restore_old_acc_ = false;
const std::vector<bool>* keep_ = nullptr;
static scc_info::edge_filter_choice
filter_scc_and_mark_(const twa_graph::edge_storage_t& e,
unsigned dst, void* data);
static scc_info::edge_filter_choice
filter_mark_(const twa_graph::edge_storage_t& e, unsigned, void* data);
static scc_info::edge_filter_choice
filter_scc_and_mark_and_edges_(const twa_graph::edge_storage_t& e,
unsigned dst, void* data);
public:
/// \brief Specify how to restrict scc_info to some SCC and acceptance sets
///
@ -805,14 +818,27 @@ namespace spot
aut_(lower_si_->get_aut()), old_acc_(aut_->get_acceptance())
{
auto f = lower_si.get_filter();
if (f == &filter_mark_ || f == &filter_scc_and_mark_)
if (f == &filter_mark_
|| f == &filter_scc_and_mark_
|| f == &filter_scc_and_mark_and_edges_)
{
const void* data = lower_si.get_filter_data();
auto& d = *reinterpret_cast<const scc_and_mark_filter*>(data);
cut_sets_ |= d.cut_sets_;
if (f == &filter_scc_and_mark_and_edges_)
keep_ = d.keep_;
}
}
scc_and_mark_filter(const scc_info& lower_si,
unsigned lower_scc,
acc_cond::mark_t cut_sets,
const std::vector<bool>& keep)
: scc_and_mark_filter(lower_si, lower_scc, cut_sets)
{
keep_ = &keep;
}
/// \brief Specify how to restrict scc_info to some acceptance sets
///
/// \param aut the automaton to filter
@ -857,6 +883,8 @@ namespace spot
scc_info::edge_filter get_filter() const
{
if (keep_)
return filter_scc_and_mark_and_edges_;
if (lower_si_)
return filter_scc_and_mark_;
if (cut_sets_)
@ -865,7 +893,6 @@ namespace spot
}
};
/// \brief Dump the SCC graph of \a aut on \a out.
///
/// If \a sccinfo is not given, it will be computed.

442
spot/twaalgos/zlktree.cc
View file

@ -19,9 +19,9 @@
#include "config.h"
#include <iostream>
#include <spot/twaalgos/zlktree.hh>
#include <spot/twaalgos/sccinfo.hh>
#include <deque>
#include <spot/twaalgos/zlktree.hh>
#include <spot/twaalgos/genem.hh>
#include "spot/priv/bddalloc.hh"
namespace spot
@ -168,7 +168,7 @@ namespace spot
else
has_streett_shape_ = false;
}
};
}
}
void zielonka_tree::dot(std::ostream& os) const
@ -203,7 +203,7 @@ namespace spot
{
if (SPOT_UNLIKELY(nodes_.size() < branch || nodes_[branch].first_child))
throw std::runtime_error
("zielonka_tree::next_branch(): incorrect branch number");
("zielonka_tree::step(): incorrect branch number");
if (!colors)
return {branch, nodes_[branch].level + 1};
@ -230,8 +230,9 @@ namespace spot
namespace
{
// A state in the zielonka_tree_transform output corresponds to a
// state in the input associated to a branch of the tree.
// A state in the zielonka_tree_transform or acd_transform outputs
// corresponds to a state in the input associated to a branch of
// the tree.
typedef std::pair<unsigned, unsigned> zlk_state;
struct zlk_state_hash
@ -347,4 +348,433 @@ namespace spot
return res;
}
void acd::report_invalid_scc_number(unsigned num, const char* fn)
{
throw std::runtime_error(std::string(fn) +
"(): SCC number " + std::to_string(num)
+ " 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)
: acd(scc_info(aut))
{
}
acd::acd(const scc_info& si)
: trees_(si.scc_count())
{
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());
// 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
// used.
int max_level_of_even_tree = -1;
int max_level_of_odd_tree = -1;
for (unsigned scc = 0; scc < scc_count; ++scc)
{
if ((trees_[scc].trivial = si.is_trivial(scc)))
continue;
unsigned root = nodes_.size();
trees_[scc].root = root;
bool is_even = si.is_maximally_accepting_scc(scc);
trees_[scc].is_even = is_even;
nodes_.emplace_back();
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))
{
n.edges[aut->edge_number(e)] = true;
n.states[e.src] = true;
}
}
// This loop is a BFS over the increasing set of nodes.
for (unsigned node = 0; node < nodes_.size(); ++node)
{
unsigned scc = nodes_[node].scc;
unsigned lvl = nodes_[node].level;
bool accepting_node = (lvl & 1) != trees_[scc].is_even;
auto callback = [&](scc_info si, unsigned siscc)
{
nodes_.emplace_back();
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;
n.states[e.src] = true;
}
};
unsigned before_size = nodes_.size();
maximal_accepting_loops_for_scc(si, scc,
accepting_node ? negacc : posacc,
nodes_[node].edges, callback);
unsigned after_size = nodes_.size();
unsigned children = after_size - before_size;
// Chain the children together, and connect them to the parent
for (unsigned child = before_size; child < after_size; ++child)
{
unsigned next = child + 1;
if (next == after_size)
{
next = before_size;
nodes_[node].first_child = before_size;
}
nodes_[child].next_sibling = next;
}
if (children == 0)
{
// this node is a leaf.
if (trees_[scc].is_even)
max_level_of_even_tree = lvl;
else
max_level_of_odd_tree = lvl;
}
else if (children > 1)
{
if (accepting_node)
has_rabin_shape_ = false;
else
has_streett_shape_ = false;
}
}
// Now we decide if the ACD corresponds to a "min even" or "max
// even" parity. We want to minimize the number of colors
// introduced (because of Spot's limitation to a fixed number of
// those), so the parity of the tallest tree will give the parity
// of the ACD.
bool is_even = is_even_ = max_level_of_even_tree >= max_level_of_odd_tree;
// add one to the level of each node belonging to a tree of the
// opposite parity
for (auto& node: nodes_)
{
unsigned scc = node.scc;
if (trees_[scc].is_even != is_even)
++node.level;
trees_[scc].max_level = std::max(trees_[scc].max_level, node.level);
}
}
unsigned acd::leftmost_branch_(unsigned n, unsigned state)
{
loop:
unsigned first_child = nodes_[n].first_child;
if (first_child == 0) // no children
return n;
unsigned child = first_child;
do
{
if (nodes_[child].states[state])
{
n = child;
goto loop;
}
child = nodes_[child].next_sibling;
}
while (child != first_child);
return n;
}
unsigned acd::first_branch(unsigned s, unsigned scc)
{
if (scc > trees_.size())
report_invalid_scc_number(scc, "first_branch");
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));
return leftmost_branch_(n, s);
}
std::pair<unsigned, unsigned>
acd::step(unsigned branch, unsigned edge)
{
if (SPOT_UNLIKELY(nodes_.size() < branch))
throw std::runtime_error("acd::step(): incorrect branch number");
unsigned child = 0;
unsigned obranch = branch;
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));
child = branch;
branch = parent;
}
unsigned lvl = nodes_[branch].level;
unsigned dst = aut_->edge_storage(edge).dst;
if (child != 0)
{
unsigned start_child = child;
// find the next children that contains dst.
do
{
child = nodes_[child].next_sibling;
if (nodes_[child].states[dst])
return {leftmost_branch_(child, dst), lvl};
}
while (child != start_child);
return { branch, lvl };
}
else
{
return { leftmost_branch_(branch, dst), lvl };
}
}
void acd::dot(std::ostream& os) const
{
os << "digraph acd {\n labelloc=\"t\"\n label=\"\n"
<< (is_even_ ? "min even\"" : "min odd\"\n");
unsigned ns = nodes_.size();
for (unsigned n = 0; n < ns; ++n)
{
acc_cond::mark_t m = {};
os << " " << n << " [label=\"";
unsigned scc = nodes_[n].scc;
// The top of each tree has level 0 or 1, depending on whether
// the tree's parity matches the overall ACD parity.
if (nodes_[n].level == (trees_[scc].is_even != is_even_))
os << "SCC #" << scc << '\n';
// Prints the indices that are true in edges. To save space,
// we print span of 3 or more elements as start-end.
auto& edges = nodes_[n].edges;
unsigned nedges = edges.size();
bool lastval = false;
unsigned lastchange = 0;
const char* sep = "T: ";
for (unsigned n = 1; n <= nedges; ++n)
{
bool val = n < nedges ? edges[n] : false;
if (val != lastval)
{
if (lastval)
switch (n - lastchange)
{
case 1:
break;
case 2:
os << ',' << n - 1;
break;
default:
os << '-' << n - 1;
break;
}
else
os << sep << n;
lastval = val;
lastchange = n;
sep = ",";
}
if (val)
m |= aut_->edge_data(n).acc;
}
unsigned first_child = nodes_[n].first_child;
os << '\n' << m;
auto& states = nodes_[n].states;
unsigned nstates = states.size();
sep = "\nQ: ";
for (unsigned n = 0; n <= nstates; ++n)
{
bool val = n < nstates ? states[n] : false;
if (val != lastval)
{
if (lastval)
switch (n - lastchange)
{
case 1:
break;
case 2:
os << ',' << n - 1;
break;
default:
os << '-' << n - 1;
break;
}
else
os << sep << n;
lastval = val;
lastchange = n;
sep = ",";
}
}
os << "\nlvl: " << nodes_[n].level;
if (!first_child)
os << "\n<" << n << '>';
os << "\", shape="
<< (((nodes_[n].level & 1) ^ is_even_) ? "ellipse" : "box")
<< "]\n";
if (first_child)
{
unsigned child = first_child;
do
{
os << " " << n << " -> " << child << '\n';
child = nodes_[child].next_sibling;
}
while (child != first_child);
}
}
os << "}\n";
}
twa_graph_ptr
acd_transform(const const_twa_graph_ptr& a, bool colored)
{
auto res = make_twa_graph(a->get_dict());
res->copy_ap_of(a);
scc_info si(a, scc_info_options::TRACK_STATES);
acd theacd(si);
// If we desire non-colored output, we can omit the maximal
// color of each SCC if it has the same parity as max_level.
unsigned max_level = 0;
if (!colored)
{
unsigned ns = si.scc_count();
for (unsigned n = 0; n < ns; ++n)
max_level = std::max(max_level, theacd.scc_max_level(n));
}
bool max_level_is_odd = max_level & 1;
// Preserve determinism, and stutter-invariance.
// state-based acceptance is lost,
// inherently-weak automata become weak.
res->prop_copy(a, { false, false, true, true, true, true });
auto orig_states = new std::vector<unsigned>();
auto branches = new std::vector<unsigned>();
unsigned ns = a->num_states();
orig_states->reserve(ns); // likely more are needed.
res->set_named_prop("original-states", orig_states);
res->set_named_prop("degen-levels", branches);
// Associate each zlk_state to its number.
typedef std::unordered_map<zlk_state, unsigned, zlk_state_hash> zs2num_map;
zs2num_map zs2num;
// Queue of states to be processed.
std::deque<zlk_state> todo;
auto new_state = [&](zlk_state zs)
{
if (auto i = zs2num.find(zs); i != zs2num.end())
return i->second;
unsigned ns = res->new_state();
zs2num[zs] = ns;
todo.emplace_back(zs);
unsigned orig = zs.first;
assert(ns == orig_states->size());
orig_states->emplace_back(orig);
branches->emplace_back(zs.second);
return ns;
};
unsigned init = a->get_init_state_number();
zlk_state s(init, theacd.first_branch(init, si.scc_of(init)));
new_state(s);
unsigned max_color = 0;
bool is_even = theacd.is_even();
while (!todo.empty())
{
s = todo.front();
todo.pop_front();
int src = zs2num[s];
unsigned branch = s.second;
unsigned src_scc = si.scc_of(s.first);
unsigned scc_max_lvl = theacd.scc_max_level(src_scc);
bool scc_max_lvl_can_be_omitted = (scc_max_lvl & 1) == max_level_is_odd;
for (auto& i: a->out(s.first))
{
unsigned newbranch;
unsigned prio;
unsigned dst_scc = si.scc_of(i.dst);
if (dst_scc != src_scc)
{
newbranch = theacd.first_branch(i.dst, dst_scc);
prio = 0;
}
else
{
std::tie(newbranch, prio) =
theacd.step(branch, a->edge_number(i));
}
zlk_state d(i.dst, newbranch);
unsigned dst = new_state(d);
if (!colored && ((dst_scc != src_scc)
|| (scc_max_lvl_can_be_omitted
&& scc_max_lvl == prio)))
{
res->new_edge(src, dst, i.cond);
}
else
{
max_color = std::max(max_color, prio);
res->new_edge(src, dst, i.cond, {prio});
}
}
}
if (!colored && max_level == 0)
res->set_acceptance(0, acc_cond::acc_code::t());
else
res->set_acceptance(max_color + 1,
acc_cond::acc_code::parity_min(!is_even,
max_color + 1));
// compose original-states with the any previously existing one.
if (auto old_orig_states =
a->get_named_prop<std::vector<unsigned>>("original-states"))
for (auto& s: *orig_states)
s = (*old_orig_states)[s];
// An inherently-weak input necessarily becomes weak.
if (a->prop_inherently_weak())
res->prop_weak(true);
return res;
}
}

159
spot/twaalgos/zlktree.hh
View file

@ -20,7 +20,9 @@
#pragma once
#include <iosfwd>
#include <deque>
#include <spot/twa/twagraph.hh>
#include <spot/twaalgos/sccinfo.hh>
namespace spot
{
@ -59,8 +61,8 @@ namespace spot
/// \brief Walk through the Zielonka tree.
///
/// Given a \a branch number, and a set of \a colors, this returns
/// a pair (new branch, level), as needed in definition 3.7 of
/// \cite casares.21.icalp
/// a pair (new branch, level), as needed in definition 3.3 of
/// \cite casares.21.icalp (or definition 3.7 in the full version).
///
/// The level correspond to the priority of a minimum parity acceptance
/// condition, with the parity odd/even as specified by is_even().
@ -142,4 +144,157 @@ namespace spot
/// has exactly one color.
SPOT_API
twa_graph_ptr zielonka_tree_transform(const const_twa_graph_ptr& aut);
/// \ingroup twa_acc_transform
/// \brief Alternating Cycle Decomposition implementation
///
/// This class implements an Alternating Cycle Decomposition
/// similar to what is described in \cite casares.21.icalp
///
/// The differences is that this ACD is built from Emerson-Lei
/// acceptance conditions, and can be "walked through" with multiple
/// colors at once.
class SPOT_API acd
{
public:
/// \brief Build a Alternating Cycle Decomposition an SCC decomposition
acd(const scc_info& si);
acd(const const_twa_graph_ptr& aut);
/// \brief Walk 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 Whether the ACD corresponds to a min even or min odd
/// parity acceptance in SCC \a scc.
bool is_even(unsigned scc) const
{
if (scc >= scc_count_)
report_invalid_scc_number(scc, "is_even");
return trees_[scc].is_even;
}
/// \brief Whether the ACD globally corresponds to a min even or
/// min odd parity acceptance.
///
/// The choice between even or odd is determined by the parity
/// of the tallest tree of the ACD. In case two tree of opposite
/// parity share the tallest height, then even parity is favored.
bool is_even() const
{
return is_even_;
}
/// \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);
/// \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)
{
if (scc >= scc_count_)
report_invalid_scc_number(scc, "scc_max_level");
return trees_[scc].max_level;
}
/// \brief Whether the ACD has Rabin shape.
///
/// The ACD has Rabin shape of all accepting (round) nodes have
/// at most one child.
bool has_rabin_shape() const
{
return has_rabin_shape_;
}
/// \brief Whether the ACD has Streett shape.
///
/// The ACD has Streett shape of all rejecting (square) nodes have
/// at most one child.
bool has_streett_shape() const
{
return has_streett_shape_;
}
/// \brief Whether the ACD has parity shape.
///
/// The ACD has parity shape of all nodes have at most one child.
bool has_parity_shape() const
{
return has_streett_shape() && has_rabin_shape();
}
/// \brief Render the ACD as in GraphViz format.
void dot(std::ostream&) const;
private:
struct acd_node
{
unsigned parent;
unsigned next_sibling = 0;
unsigned first_child = 0;
unsigned level;
unsigned scc;
std::vector<bool> edges;
std::vector<bool> states;
};
std::deque<acd_node> nodes_;
struct scc_data
{
bool trivial;
unsigned root = 0;
bool is_even;
unsigned max_level = 0;
};
std::vector<scc_data> trees_;
unsigned scc_count_;
const_twa_graph_ptr aut_;
bool is_even_;
bool has_rabin_shape_ = true;
bool has_streett_shape_ = true;
// leftmost branch of \a node that contains \a state
unsigned leftmost_branch_(unsigned node, unsigned state);
#ifndef SWIG
[[noreturn]] static
void report_invalid_scc_number(unsigned num, const char* fn);
#endif
};
/// \ingroup twa_acc_transform
/// \brief Paritize an automaton using ACD.
///
/// This corresponds to the application of Section 4 of
/// \cite casares.21.icalp
///
/// The resulting automaton has a parity acceptance that is either
/// "min odd" or "min even", depending on the original acceptance.
///
/// If \a colored is set, each output transition will have exactly
/// one color, and the output automaton will use at most n+1 colors
/// if the input has n colors. If \colored is unsed (the default),
/// output transitions will use at most one color, and output
/// automaton will use at most n colors.
SPOT_API
twa_graph_ptr acd_transform(const const_twa_graph_ptr& aut,
bool colored = false);
}

3849
tests/python/_zlktree.ipynb
View file

File diff suppressed because it is too large Load diff

36
tests/python/toparity.py
View file

@ -88,11 +88,13 @@ options = [
rab_to_buchi_opt,
use_car_opt,
all_opt,
None, # acd_transform
]
def test(aut, expected_num_states=[], full=True):
for (opt, expected_num) in zip_longest(options, expected_num_states):
if opt is not None:
p1 = spot.to_parity(aut,
search_ex = opt.search_ex,
use_last = opt.use_last,
@ -106,15 +108,17 @@ def test(aut, expected_num_states=[], full=True):
propagate_col = opt.propagate_col,
pretty_print = opt.pretty_print,
)
else:
p1 = spot.acd_transform(aut)
p1st, p1ed, p1se = p1.num_states(), p1.num_edges(), p1.num_sets()
if opt.parity_prefix is False:
if opt is not None and opt.parity_prefix is False:
# Reduce the number of colors to help are_equivalent
spot.reduce_parity_here(p1)
assert spot.are_equivalent(aut, p1)
if expected_num is not None:
print(p1.num_states(), expected_num)
assert p1.num_states() == expected_num
if full:
if full and opt is not None:
# Make sure passing opt is the same as setting
# each argument individually
p2 = spot.to_parity(aut, opt)
@ -200,7 +204,7 @@ State: 13
[0&1] 5
[!0&!1] 10 {0 1 3 5}
[0&!1] 13 {1 3}
--END--"""), [35, 30, 23, 32, 31, 28, 22])
--END--"""), [35, 30, 23, 32, 31, 28, 22, 21])
test(spot.automaton("""
HOA: v1
@ -218,7 +222,7 @@ State: 1
[0&!1] 1 {4}
[!0&1] 1 {0 1 2 3}
[!0&!1] 1 {0 3}
--END--"""), [7, 5, 3, 6, 5, 5, 3])
--END--"""), [7, 5, 3, 6, 5, 5, 3, 3])
test(spot.automaton("""HOA: v1
States: 2
@ -234,13 +238,13 @@ State: 0
State: 1
[0&1] 1 {2 3 4}
[!0&!1] 0 {1 2}
--END--"""), [9, 3, 2, 3, 3, 3, 2])
--END--"""), [9, 3, 2, 3, 3, 3, 2, 2])
for i,f in enumerate(spot.randltl(10, 400)):
test(spot.translate(f, "det", "G"), full=(i<100))
for f in spot.randltl(5, 2500):
test(spot.translate(f), full=False)
#for i,f in enumerate(spot.randltl(10, 400)):
# test(spot.translate(f, "det", "G"), full=(i<100))
#
#for f in spot.randltl(5, 2500):
# test(spot.translate(f), full=False)
test(spot.automaton("""
@ -274,7 +278,7 @@ State: 3
[!0&1] 2 {1 4}
[0&1] 3 {0}
--END--
"""), [80, 47, 104, 104, 102, 29, 6])
"""), [80, 47, 104, 104, 102, 29, 6, 6])
test(spot.automaton("""
HOA: v1
@ -308,7 +312,7 @@ State: 4
[0&!1] 4
[0&1] 4 {1 2 4}
--END--
"""), [9, 6, 7, 7, 6, 6, 6])
"""), [9, 6, 7, 7, 6, 6, 6, 6])
test(spot.automaton("""
HOA: v1
@ -330,7 +334,7 @@ State: 1
[0&!1] 1 {2 3}
[0&1] 1 {1 2 4}
--END--
"""), [11, 3, 2, 3, 3, 3, 2])
"""), [11, 3, 2, 3, 3, 3, 2, 2])
# Tests both the old and new version of to_parity
@ -361,7 +365,7 @@ explicit-labels trans-acc --BODY-- State: 0 [0&1] 2 {4 5} [0&1] 4 {0 4}
p = spot.to_parity_old(a, True)
assert p.num_states() == 22
assert spot.are_equivalent(a, p)
test(a, [8, 6, 6, 6, 6, 6, 6])
test(a, [8, 6, 6, 6, 6, 6, 6, 6])
# Force a few edges to false, to make sure to_parity() is OK with that.
for e in a.out(2):
@ -375,7 +379,7 @@ for e in a.out(3):
p = spot.to_parity_old(a, True)
assert p.num_states() == 22
assert spot.are_equivalent(a, p)
test(a, [7, 6, 6, 6, 6, 6, 6])
test(a, [7, 6, 6, 6, 6, 6, 6, 6])
for f in spot.randltl(4, 400):
d = spot.translate(f, "det", "G")
@ -391,4 +395,4 @@ for f in spot.randltl(5, 2000):
a = spot.translate('!(GFa -> (GFb & GF(!b & !Xb)))', 'gen', 'det')
b = spot.to_parity_old(a, True)
assert a.equivalent_to(b)
test(a, [7, 7, 3, 7, 7, 7, 3])
test(a, [7, 7, 3, 7, 7, 7, 3, 3])