From e01d9237b2f3f5ab4b0b3ec60ec2e955ed211c1f Mon Sep 17 00:00:00 2001
From: Antoine Martin <amartin@lrde.epita.fr>
Date: Thu, 10 Mar 2022 15:45:50 +0100
Subject: [PATCH] twaalgos: extract internal sere2dfa

---
 spot/twaalgos/ltl2tgba_fm.cc | 56 ++++++++++++++++++++++++++++++++++++
 spot/twaalgos/ltl2tgba_fm.hh |  3 ++
 2 files changed, 59 insertions(+)

diff --git a/spot/twaalgos/ltl2tgba_fm.cc b/spot/twaalgos/ltl2tgba_fm.cc
index 09e88acae..a3f0f2aa3 100644
--- a/spot/twaalgos/ltl2tgba_fm.cc
+++ b/spot/twaalgos/ltl2tgba_fm.cc
@@ -22,6 +22,7 @@
 #include <spot/tl/print.hh>
 #include <spot/tl/apcollect.hh>
 #include <spot/tl/mark.hh>
+#include <spot/tl/nenoform.hh>
 #include <cassert>
 #include <memory>
 #include <utility>
@@ -2226,4 +2227,59 @@ namespace spot
     return a;
   }
 
+  twa_graph_ptr
+  sere_to_tgba(formula f, const bdd_dict_ptr& dict)
+  {
+    f = negative_normal_form(f);
+
+    tl_simplifier* s = new tl_simplifier(dict);
+    twa_graph_ptr a = make_twa_graph(dict);
+
+    translate_dict d(a, s, false, false, false);
+    ratexp_to_dfa sere2dfa(d);
+
+    auto [dfa, namer, state] = sere2dfa.succ(f);
+
+    // language was empty, build an automaton with one non accepting state
+    if (dfa == nullptr)
+      {
+        auto res = make_twa_graph(dict);
+        res->set_init_state(res->new_state());
+        res->prop_universal(true);
+        res->prop_complete(false);
+        res->prop_stutter_invariant(true);
+        res->prop_terminal(true);
+        res->prop_state_acc(true);
+        return res;
+      }
+
+    auto res = make_twa_graph(dfa, {false, false, true, false, false, false});
+
+    // HACK: translate_dict registers the atomic propositions in the "final"
+    // automaton that would be produced by a full translation, not in the
+    // intermediate automaton we're interested in. We can copy them from the
+    // resulting automaton.
+    res->copy_ap_of(a);
+
+    res->prop_state_acc(true);
+    const auto acc_mark = res->set_buchi();
+
+    size_t sn = namer->state_to_name.size();
+    for (size_t i = 0; i < sn; ++i)
+      {
+        formula g = namer->state_to_name[i];
+        if (g.accepts_eword())
+          {
+            if (res->get_graph().state_storage(i).succ == 0)
+              res->new_edge(i, i, bddfalse, acc_mark);
+            else
+              {
+                for (auto& e : res->out(i))
+                  e.acc = acc_mark;
+              }
+          }
+      }
+
+    return res;
+  }
 }
diff --git a/spot/twaalgos/ltl2tgba_fm.hh b/spot/twaalgos/ltl2tgba_fm.hh
index 717ae6b1b..7dba4aee0 100644
--- a/spot/twaalgos/ltl2tgba_fm.hh
+++ b/spot/twaalgos/ltl2tgba_fm.hh
@@ -89,4 +89,7 @@ namespace spot
                  bool unambiguous = false,
                  const output_aborter* aborter = nullptr,
                  bool label_with_ltl = false);
+
+  SPOT_API twa_graph_ptr
+  sere_to_tgba(formula f, const bdd_dict_ptr& dict);
 }