From 4ab97a68419e544cc11b0eb761480966ff5a6cf3 Mon Sep 17 00:00:00 2001
From: Antoine Martin <amartin@lrde.epita.fr>
Date: Fri, 18 Mar 2022 19:27:19 +0100
Subject: [PATCH] derive: extract AndNLM rewriting

---
 spot/tl/derive.cc            | 55 ++++++++++++++++++++++++++++++++++++
 spot/tl/derive.hh            |  3 ++
 spot/twaalgos/ltl2tgba_fm.cc | 51 ++-------------------------------
 3 files changed, 60 insertions(+), 49 deletions(-)

diff --git a/spot/tl/derive.cc b/spot/tl/derive.cc
index 699c8634f..a24fbac53 100644
--- a/spot/tl/derive.cc
+++ b/spot/tl/derive.cc
@@ -48,6 +48,61 @@ namespace spot
     }
   }
 
+  formula
+  rewrite_and_nlm(formula f)
+  {
+    unsigned s = f.size();
+    std::vector<formula> final;
+    std::vector<formula> non_final;
+
+    for (auto g: f)
+      if (g.accepts_eword())
+        final.emplace_back(g);
+      else
+        non_final.emplace_back(g);
+
+    if (non_final.empty())
+      // (a* & b*);c = (a*|b*);c
+      return formula::OrRat(std::move(final));
+    if (!final.empty())
+    {
+      // let F_i be final formulae
+      //     N_i be non final formula
+      // (F_1 & ... & F_n & N_1 & ... & N_m)
+      // =   (F_1 | ... | F_n);[*] && (N_1 & ... & N_m)
+      //   | (F_1 | ... | F_n) && (N_1 & ... & N_m);[*]
+      formula f = formula::OrRat(std::move(final));
+      formula n = formula::AndNLM(std::move(non_final));
+      formula t = formula::one_star();
+      formula ft = formula::Concat({f, t});
+      formula nt = formula::Concat({n, t});
+      formula ftn = formula::AndRat({ft, n});
+      formula fnt = formula::AndRat({f, nt});
+      return formula::OrRat({ftn, fnt});
+    }
+    // No final formula.
+    // Translate N_1 & N_2 & ... & N_n into
+    //   N_1 && (N_2;[*]) && ... && (N_n;[*])
+    // | (N_1;[*]) && N_2 && ... && (N_n;[*])
+    // | (N_1;[*]) && (N_2;[*]) && ... && N_n
+    formula star = formula::one_star();
+    std::vector<formula> disj;
+    for (unsigned n = 0; n < s; ++n)
+    {
+      std::vector<formula> conj;
+      for (unsigned m = 0; m < s; ++m)
+      {
+        formula g = f[m];
+        if (n != m)
+          g = formula::Concat({g, star});
+        conj.emplace_back(g);
+      }
+      disj.emplace_back(formula::AndRat(std::move(conj)));
+    }
+    return formula::OrRat(std::move(disj));
+  }
+
+
   twa_graph_ptr
   derive_finite_automaton(formula f, bool deterministic)
   {
diff --git a/spot/tl/derive.hh b/spot/tl/derive.hh
index 410a24e37..247f85b59 100644
--- a/spot/tl/derive.hh
+++ b/spot/tl/derive.hh
@@ -40,4 +40,7 @@ namespace spot
 
   SPOT_API twa_graph_ptr
   derive_finite_automaton(formula f, bool deterministic = true);
+
+  SPOT_API formula
+  rewrite_and_nlm(formula f);
 }
diff --git a/spot/twaalgos/ltl2tgba_fm.cc b/spot/twaalgos/ltl2tgba_fm.cc
index a3f0f2aa3..9c7674b0f 100644
--- a/spot/twaalgos/ltl2tgba_fm.cc
+++ b/spot/twaalgos/ltl2tgba_fm.cc
@@ -19,6 +19,7 @@
 #include "config.h"
 #include <spot/misc/bddlt.hh>
 #include <spot/misc/minato.hh>
+#include <spot/tl/derive.hh>
 #include <spot/tl/print.hh>
 #include <spot/tl/apcollect.hh>
 #include <spot/tl/mark.hh>
@@ -748,55 +749,7 @@ namespace spot
             SPOT_UNREACHABLE();
           case op::AndNLM:
             {
-              unsigned s = f.size();
-              vec final;
-              vec non_final;
-
-              for (auto g: f)
-                if (g.accepts_eword())
-                  final.emplace_back(g);
-                else
-                  non_final.emplace_back(g);
-
-              if (non_final.empty())
-                // (a* & b*);c = (a*|b*);c
-                return recurse_and_concat(formula::OrRat(std::move(final)));
-              if (!final.empty())
-                {
-                  // let F_i be final formulae
-                  //     N_i be non final formula
-                  // (F_1 & ... & F_n & N_1 & ... & N_m)
-                  // =   (F_1 | ... | F_n);[*] && (N_1 & ... & N_m)
-                  //   | (F_1 | ... | F_n) && (N_1 & ... & N_m);[*]
-                  formula f = formula::OrRat(std::move(final));
-                  formula n = formula::AndNLM(std::move(non_final));
-                  formula t = formula::one_star();
-                  formula ft = formula::Concat({f, t});
-                  formula nt = formula::Concat({n, t});
-                  formula ftn = formula::AndRat({ft, n});
-                  formula fnt = formula::AndRat({f, nt});
-                  return recurse_and_concat(formula::OrRat({ftn, fnt}));
-                }
-              // No final formula.
-              // Translate N_1 & N_2 & ... & N_n into
-              //   N_1 && (N_2;[*]) && ... && (N_n;[*])
-              // | (N_1;[*]) && N_2 && ... && (N_n;[*])
-              // | (N_1;[*]) && (N_2;[*]) && ... && N_n
-              formula star = formula::one_star();
-              vec disj;
-              for (unsigned n = 0; n < s; ++n)
-                {
-                  vec conj;
-                  for (unsigned m = 0; m < s; ++m)
-                    {
-                      formula g = f[m];
-                      if (n != m)
-                        g = formula::Concat({g, star});
-                      conj.emplace_back(g);
-                    }
-                  disj.emplace_back(formula::AndRat(std::move(conj)));
-                }
-              return recurse_and_concat(formula::OrRat(std::move(disj)));
+              return recurse_and_concat(rewrite_and_nlm(f));
             }
           case op::AndRat:
             {