From 8ae10f744f262bc5434cae89eeba0ee8635ce5ab Mon Sep 17 00:00:00 2001
From: Alexandre GBAGUIDI AISSE <gbagui_a@epita.fr>
Date: Sat, 17 Jun 2017 22:16:22 +0200
Subject: [PATCH] twaalgos/cobuchi: Add dnf_to_dca()
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* NEWS: Update news with all co-Büching functions.
* spot/twaalgos/cobuchi.hh: Declare it.
* spot/twaalgos/cobuchi.cc: Implement it.
---
 NEWS                     | 20 +++++++++++++-------
 spot/twaalgos/cobuchi.cc | 33 ++++++++++++++++++++++++++++++++-
 spot/twaalgos/cobuchi.hh | 22 ++++++++++++++++++++++
 3 files changed, 67 insertions(+), 8 deletions(-)

diff --git a/NEWS b/NEWS
index 8b45690cb..a7a26b3fb 100644
--- a/NEWS
+++ b/NEWS
@@ -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:
 
diff --git a/spot/twaalgos/cobuchi.cc b/spot/twaalgos/cobuchi.cc
index b5f14680a..2cdc98aa6 100644
--- a/spot/twaalgos/cobuchi.cc
+++ b/spot/twaalgos/cobuchi.cc
@@ -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");
diff --git a/spot/twaalgos/cobuchi.hh b/spot/twaalgos/cobuchi.hh
index bf632b5d9..e2bec918b 100644
--- a/spot/twaalgos/cobuchi.hh
+++ b/spot/twaalgos/cobuchi.hh
@@ -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.