Commit 8ae10f74 authored by Alexandre GBAGUIDI AISSE's avatar Alexandre GBAGUIDI AISSE
Browse files

twaalgos/cobuchi: Add dnf_to_dca()

* NEWS: Update news with all co-Büching functions.
* spot/twaalgos/cobuchi.hh: Declare it.
* spot/twaalgos/cobuchi.cc: Implement it.
parent 5f6a71d2
......@@ -13,6 +13,11 @@ New in spot 2.4.0.dev (not yet released)
have a Streett-like acceptance condition. It only works with
ω-automata having an acceptance in disjunctive normal form.
- autfilt learned --dca to convert a Streett-like automaton or an
automaton with an acceptance in disjunctive normal form to a
deterministic co-Büchi automaton using the new functions
[nsa-dnf]_to_dca() described below.
Library:
- Rename three methods of spot::scc_info. New names are clearer. The
......@@ -28,13 +33,14 @@ New in spot 2.4.0.dev (not yet released)
Streett-like automaton. This is used by the new option
'--streett-like' of autfilt.
- The new functions nsa_to_nca() and nra_to_nca() are able to convert
when possible respectively an automaton with a Streett-like
acceptance or a Rabin-like acceptance to an equivalent automaton
with a co-Büchi acceptance. Actually the resulting automaton will
always recognize at least the same language. It can recognize more
if the original language can not be expressed with a co-Büchi
acceptance condition.
- The new functions spot::nsa_to_[nca-dca]()
(or spot::dnf_to_[nca-dca]()) are able to convert when possible a
Streett-like automaton (or any automaton with an acceptance in DNF)
to an equivalent 'nca' (nondeterministic co-Büchi automaton) or
'dca' (deterministic co-Büchi automaton). Actually the resulting
automaton will always recognize at least the same language. It can
recognize more if the original language can not be expressed with
a co-Büchi acceptance condition.
Deprecation notices:
......
......@@ -566,6 +566,37 @@ namespace spot
}
twa_graph_ptr
dnf_to_dca(const const_twa_graph_ptr& aut, bool named_states)
{
debug << "DNF_to_dca" << std::endl;
const acc_cond::acc_code& code = aut->get_acceptance();
std::vector<acc_cond::rs_pair> pairs;
if (!code.is_dnf())
throw std::runtime_error("dnf_to_dca() only works with DNF (Rabin-like "
"included) acceptance condition");
// Get states that must be visited infinitely often in NCA.
vect_nca_info nca_info;
dnf_to_nca(aut, false, &nca_info);
#if DEBUG
debug << "PRINTING INFO" << std::endl;
for (unsigned i = 0; i < nca_info.size(); ++i)
debug << '<' << nca_info[i]->clause_num << ',' << nca_info[i]->state_num
<< ',' << nca_info[i]->all_dst << '>' << std::endl;
#endif
unsigned nb_copy = 0;
for (const auto& p : nca_info)
if (nb_copy < p->clause_num)
nb_copy = p->clause_num;
dca_breakpoint_cons dca(aut, &nca_info, nb_copy);
return dca.run(named_states);
}
twa_graph_ptr
to_dca(const const_twa_graph_ptr& aut, bool named_states)
{
......@@ -575,7 +606,7 @@ namespace spot
if (aut->acc().is_streett_like(pairs) || aut->acc().is_parity())
return nsa_to_dca(aut, named_states);
else if (code.is_dnf())
return dnf_to_nca(aut, named_states);
return dnf_to_dca(aut, named_states);
else
throw std::runtime_error("to_dca() only works with Streett-like, Parity "
"or any acceptance condition in DNF");
......
......@@ -129,6 +129,28 @@ namespace spot
SPOT_API twa_graph_ptr
nsa_to_dca(const const_twa_graph_ptr& aut, bool named_states = false);
/// \brief Converts an aut. with acceptance in DNF to a det. co-Büchi aut.
///
/// This function calls first nra_to_nca() in order to retrieve som
/// information and then runs a breakpoint construction. The algorithm is
/// described in section 4 of:
/** \verbatim
@Article{boker.2009.lcs,
author = {Udi Boker and Orna Kupferman},
title = {Co-Büching Them All},
booktitle = {Foundations of Software Science and Computational
Structures - 14th International Conference, FOSSACS 2011}
year = {2011},
pages = {184--198},
url = {\url{www.cs.huji.ac.il/~ornak/publications/fossacs11b.pdf}}
}
\endverbatim */
///
/// \a aut The automaton to convert.
/// \a named_states name each state for easier debugging.
SPOT_API twa_graph_ptr
dnf_to_dca(const const_twa_graph_ptr& aut, bool named_states = false);
/// \brief Converts any ω-automata to det. co-buchi (when possible)
///
/// The resulting automaton will always recognize at least the same language.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment