From 514ef110f254b5dacf182c6702bc8451ee34f078 Mon Sep 17 00:00:00 2001
From: Antoine Martin <amartin@lrde.epita.fr>
Date: Fri, 10 Oct 2025 16:49:34 +0200
Subject: [PATCH] translate_aa: Factorize sere translation choice

* spot/twaalgos/translate_aa.cc: Here.
---
 spot/twaalgos/translate_aa.cc | 48 ++++++++++++-----------------------
 1 file changed, 16 insertions(+), 32 deletions(-)

diff --git a/spot/twaalgos/translate_aa.cc b/spot/twaalgos/translate_aa.cc
index 15633b4ec..799a7e6f3 100644
--- a/spot/twaalgos/translate_aa.cc
+++ b/spot/twaalgos/translate_aa.cc
@@ -34,6 +34,20 @@ namespace spot
 {
   namespace
   {
+    twa_graph_ptr sere_aa_translate(formula f, const bdd_dict_ptr& dict)
+    {
+      // old bdd method
+      if (sere_aa_translation_options() == 0)
+        return sere_to_tgba(f, dict, true);
+
+      // derivation
+      if (sere_aa_translation_options() == 1)
+        return derive_finite_automaton_with_first(f, dict);
+
+      // linear form
+      return expand_finite_automaton(f, dict, exp_opts::expand_opt::None);
+    }
+
     struct ltl_to_aa_builder
     {
       ltl_to_aa_builder(twa_graph_ptr aut, unsigned accepting_sink)
@@ -289,22 +303,7 @@ namespace spot
           {
             unsigned rhs_init = recurse(f[1]);
             const auto& dict = aut_->get_dict();
-            twa_graph_ptr sere_aut;
-            if (sere_aa_translation_options() == 0)
-              {
-                // old bdd method
-                sere_aut = sere_to_tgba(f[0], dict, true);
-              }
-            else if (sere_aa_translation_options() == 1)
-              {
-                // derivation
-                sere_aut = derive_finite_automaton_with_first(f[0], dict);
-              }
-            else
-              {
-                // linear form
-                sere_aut = expand_finite_automaton(f[0], dict, exp_opts::expand_opt::None);
-              }
+            twa_graph_ptr sere_aut = sere_aa_translate(f[0], dict);
 
             // TODO: this should be a std::vector<bool> !
             std::vector<unsigned> acc_states;
@@ -345,22 +344,7 @@ namespace spot
           {
             unsigned rhs_init = recurse(f[1]);
             const auto& dict = aut_->get_dict();
-            twa_graph_ptr sere_aut;
-            if (sere_aa_translation_options() == 0)
-              {
-                // old bdd method
-                sere_aut = sere_to_tgba(f[0], dict, true);
-              }
-            else if (sere_aa_translation_options() == 1)
-              {
-                // derivation
-                sere_aut = derive_finite_automaton_with_first(f[0], dict);
-              }
-            else
-              {
-                // linear form
-                sere_aut = expand_finite_automaton(f[0], dict, exp_opts::expand_opt::None);
-              }
+            twa_graph_ptr sere_aut = sere_aa_translate(f[0], dict);
 
             // DFA recognizes the empty language, so {0} []-> rhs is always true
             unsigned ns = sere_aut->num_states();