From ebe03cf3d06398f96c49258f958d587c6eac26e3 Mon Sep 17 00:00:00 2001
From: Alexandre Lewkowicz <lewkow_a@epita.fr>
Date: Thu, 28 May 2015 10:53:48 +0200
Subject: [PATCH] safra: Fix nesting comparision

* src/tests/safra.cc:  Output error message for wrong ltl formula.
* src/twaalgos/safra.cc:  Default comparision of vector does not
correspond to the desired comparision.
---
 src/tests/safra.cc    |  3 +++
 src/twaalgos/safra.cc | 27 ++++++++++++++++++++++-----
 2 files changed, 25 insertions(+), 5 deletions(-)

diff --git a/src/tests/safra.cc b/src/tests/safra.cc
index 747cd5530..6faf8b9f1 100644
--- a/src/tests/safra.cc
+++ b/src/tests/safra.cc
@@ -27,6 +27,7 @@
 #include "ltlparse/public.hh"
 #include "twaalgos/dotty.hh"
 #include "twaalgos/hoa.hh"
+#include "twaalgos/degen.hh"
 
 
 int main(int argc, char* argv[])
@@ -42,6 +43,8 @@ int main(int argc, char* argv[])
       const spot::ltl::formula* f =
       spot::ltl::parse(input, pel, spot::ltl::default_environment::instance(),
                        false);
+      if (spot::ltl::format_parse_errors(std::cerr, input, pel))
+        return 2;
       spot::translator trans(dict);
       trans.set_pref(spot::postprocessor::Deterministic);
       auto tmp = trans.run(f);
diff --git a/src/twaalgos/safra.cc b/src/twaalgos/safra.cc
index f26484258..345820226 100644
--- a/src/twaalgos/safra.cc
+++ b/src/twaalgos/safra.cc
@@ -28,6 +28,21 @@ namespace spot
 {
   namespace
   {
+    // Returns true if lhs has a smaller nesting pattern than rhs
+    // If lhs and rhs are the same, return false.
+    bool nesting_cmp(const std::vector<node_helper::brace_t>& lhs,
+                     const std::vector<node_helper::brace_t>& rhs)
+    {
+      size_t m = std::min(lhs.size(), rhs.size());
+      size_t i = 0;
+      for (; i < m; ++i)
+        {
+          if (lhs[i] < rhs[i])
+            return true;
+        }
+      return lhs.size() > rhs.size();
+    }
+
     // Used to remove all acceptance whos value is above max_acc
     void remove_dead_acc(twa_graph_ptr& aut, unsigned max_acc)
     {
@@ -91,7 +106,10 @@ namespace spot
       {
         if (nb_braces_[i] == 0)
           {
-            red = std::min(red, 2 * i + 1);
+            // It is impossible to emit red == -1 as those transitions would
+            // lead us in a sink states which are not created here.
+            assert(i >= 1);
+            red = std::min(red, 2 * i - 1);
             // Step A3: Brackets that do not contain any nodes emit red
             is_green_[i] = false;
           }
@@ -187,9 +205,9 @@ namespace spot
     auto i = nodes_.emplace(dst, copy);
     if (!i.second)
       {
-        // Step A2: Remove all occurrences whos nesting pattern (i-e  braces_)
-        // is smaller
-        if (copy > i.first->second)
+        // Step A2: Only keep the smallest nesting pattern (i-e  braces_) for
+        // identical nodes.  Nesting_cmp returnes true if copy is smaller
+        if (nesting_cmp(copy, i.first->second))
           {
             // Remove brace count of replaced node
             for (auto b: i.first->second)
@@ -301,7 +319,6 @@ namespace spot
             deltas[t.cond] = std::make_pair(prev, bddnums.size());
           }
       }
-    unsigned nc = bdd2num.size();
 
     auto res = make_twa_graph(aut->get_dict());
     res->copy_ap_of(aut);