From fbb56759865e2961fc79c07ec6e0d8623c049438 Mon Sep 17 00:00:00 2001
From: Antoine Martin <amartin@lrde.epita.fr>
Date: Wed, 15 Oct 2025 14:24:08 +0200
Subject: [PATCH] translate_aa: expose lf-trans option

* spot/twaalgos/translate_aa.cc:
---
 spot/twaalgos/translate_aa.cc | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

diff --git a/spot/twaalgos/translate_aa.cc b/spot/twaalgos/translate_aa.cc
index 799a7e6f3..163afaf3b 100644
--- a/spot/twaalgos/translate_aa.cc
+++ b/spot/twaalgos/translate_aa.cc
@@ -26,6 +26,7 @@
 #include <spot/twaalgos/translate_aa.hh>
 #include <spot/tl/derive.hh>
 #include <spot/tl/expansions.hh>
+#include <spot/tl/expansions2.hh>
 #include <spot/tl/nenoform.hh>
 
 #include <iostream>
@@ -45,7 +46,11 @@ namespace spot
         return derive_finite_automaton_with_first(f, dict);
 
       // linear form
-      return expand_finite_automaton(f, dict, exp_opts::expand_opt::None);
+      if (sere_aa_translation_options() == 2)
+        return expand_finite_automaton(f, dict, exp_opts::expand_opt::None);
+
+      // linear form - trans-based
+      return expand_finite_automaton2(f, dict, exp_opts::expand_opt::None);
     }
 
     struct ltl_to_aa_builder
@@ -515,12 +520,14 @@ namespace spot
           pref = 1;
         else if (!strcasecmp(version, "lf"))
           pref = 2;
+        else if (!strcasecmp(version, "lft"))
+          pref = 3;
         else
           {
             const char* err = ("sere_aa_translation_options(): argument"
-                              " should be one of {bdd,derive,lf}");
+                              " should be one of {bdd,derive,lf,lft}");
             if (env)
-              err = "SPOT_SERE_AA_TRANSLATE_OPT should be one of {bdd,derive,expansion}";
+              err = "SPOT_SERE_AA_TRANSLATE_OPT should be one of {bdd,derive,lf,lft}";
             throw std::runtime_error(err);
           }
       }