From ef3143f048c2e5a6a2b8052cda12a1fcc0e381ff Mon Sep 17 00:00:00 2001
From: Alexandre Lewkowicz <lewkow_a@epita.fr>
Date: Tue, 19 May 2015 16:32:00 +0200
Subject: [PATCH] safra: Output parity acceptance sets

* src/twaalgos/safra.cc, src/twaalgos/safra.hh:  Note that the created
automaton is not a true parity automaton as they are not handled yet
by Spot.
---
 src/twaalgos/safra.cc | 16 ++++++++++++----
 src/twaalgos/safra.hh |  4 +++-
 2 files changed, 15 insertions(+), 5 deletions(-)

diff --git a/src/twaalgos/safra.cc b/src/twaalgos/safra.cc
index 2f09eef37..e474fdd65 100644
--- a/src/twaalgos/safra.cc
+++ b/src/twaalgos/safra.cc
@@ -53,25 +53,29 @@ namespace spot
     for (auto& s: res)
       {
         safra_state& tmp = s.first;
-        tmp.finalize_construction();
+        s.first.color_ = tmp.finalize_construction();
       }
     return res;
   }
 
-  void safra_state::finalize_construction()
+  unsigned safra_state::finalize_construction()
   {
+    unsigned red = -1U;
+    unsigned green = -1U;
     std::vector<unsigned> rem_succ_of;
     assert(is_green_.size() == nb_braces_.size());
     for (unsigned i = 0; i < is_green_.size(); ++i)
       {
         if (nb_braces_[i] == 0)
           {
+            red = std::min(red, 2 * i + 1);
             // TODO We also emit Red = min(red, i)
             // Step A3: Brackets that do not contain any nodes emit red
             is_green_[i] = false;
           }
         else if (is_green_[i])
           {
+            green = std::min(green, 2 * i);
             // Step A4 Emit green
             rem_succ_of.emplace_back(i);
           }
@@ -109,6 +113,7 @@ namespace spot
         // it
         nn.disable_construction();
       }
+    return std::min(red, green);
   }
 
   void safra_state::node::renumber(const std::vector<unsigned>& decr_by)
@@ -317,11 +322,14 @@ namespace spot
 	    else
 	      {
                 dst_num = res->new_state();
-                s.first.print_debug(dst_num);
+                // s.first.print_debug(dst_num);
                 todo.push_back(s.first);
                 seen.insert(std::make_pair(s.first, dst_num));
               }
-	    res->new_transition(src_num, dst_num, s.second);
+            if (s.first.color_ != -1U)
+              res->new_transition(src_num, dst_num, s.second, {s.first.color_});
+            else
+              res->new_transition(src_num, dst_num, s.second);
           }
       }
     return res;
diff --git a/src/twaalgos/safra.hh b/src/twaalgos/safra.hh
index ec28c7779..4bc0f2bce 100644
--- a/src/twaalgos/safra.hh
+++ b/src/twaalgos/safra.hh
@@ -70,7 +70,8 @@ namespace spot
     // A new intermediate node is created with  src's braces and with dst as id
     // A merge is done if dst already existed in *this
     void update_succ(const node& src, unsigned dst, const acc_cond::mark_t acc);
-    void finalize_construction();
+    // Return the emitted color, red or green
+    unsigned finalize_construction();
     // A list of nodes similar to the ones of a
     // safra tree.  These are constructed in the same way as the powerset
     // algorithm.
@@ -80,6 +81,7 @@ namespace spot
     std::vector<size_t> nb_braces_;
     // A bitfield to know if a brace can emit green.
     std::vector<bool> is_green_;
+    unsigned color_;
   };
 
   SPOT_API twa_graph_ptr