merge

The previous implementation was wrong and led to segfaults when sorting
large expansions

.gitignore

@@ -82,3 +82,4 @@ GTAGS
 *.dsc
 *.gcov
 spot.spec
+default.nix

Makefile.am

@@ -65,7 +65,8 @@ EXTRA_DIST = HACKING ChangeLog.1 tools/gitlog-to-changelog	\
 	     tools/help2man tools/man2html.pl			\
 	     tools/test-driver-teamcity $(UTF8) $(DEBIAN)	\
 	     m4/gnulib-cache.m4 .dir-locals.el			\
-	     spot.spec spot.spec.in README.ltsmin
+	     spot.spec spot.spec.in README.ltsmin		\
+	     default.nix default.nix.in
 
 dist-hook: gen-ChangeLog
 
@@ -111,3 +112,6 @@ deb: dist
 
 spot.spec: configure.ac spot.spec.in
 	sed 's/[@]VERSION[@]/$(VERSION)/;s/[@]GITPATCH[@]/@@@$(GITPATCH)/;s/@@@\.//' spot.spec.in > $@.tmp && mv $@.tmp $@
+
+default.nix: configure.ac default.nix.in
+	sed 's/[@]VERSION[@]/$(VERSION)/' default.nix.in > $@.tmp && mv $@.tmp $@

default.nix.in

@@ -0,0 +1,35 @@
+# -*- mode: nix; coding: utf-8 -*-
+# Copyright (C) 2022 Laboratoire de Recherche et Développement de l'Epita
+# (LRDE).
+#
+# This file is part of Spot, a model checking library.
+#
+# Spot is free software; you can redistribute it and/or modify it
+# under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 3 of the License, or
+# (at your option) any later version.
+#
+# Spot is distributed in the hope that it will be useful, but WITHOUT
+# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+# License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+{ pkgs ? import <nixpkgs> {} }:
+let
+  version = "@VERSION@";
+in
+pkgs.stdenv.mkDerivation {
+  inherit version;
+  pname = "spot";
+
+  buildInputs = [
+    pkgs.python3
+  ];
+
+  src = ./.;
+
+  enableParallelBuilding = true;
+}

flake.lock

@@ -0,0 +1,61 @@
+{
+  "nodes": {
+    "flake-utils": {
+      "inputs": {
+        "systems": "systems"
+      },
+      "locked": {
+        "lastModified": 1731533236,
+        "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=",
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b",
+        "type": "github"
+      },
+      "original": {
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "type": "github"
+      }
+    },
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1741196730,
+        "narHash": "sha256-0Sj6ZKjCpQMfWnN0NURqRCQn2ob7YtXTAOTwCuz7fkA=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "48913d8f9127ea6530a2a2f1bd4daa1b8685d8a3",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "ref": "nixos-24.11",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "root": {
+      "inputs": {
+        "flake-utils": "flake-utils",
+        "nixpkgs": "nixpkgs"
+      }
+    },
+    "systems": {
+      "locked": {
+        "lastModified": 1681028828,
+        "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
+        "owner": "nix-systems",
+        "repo": "default",
+        "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-systems",
+        "repo": "default",
+        "type": "github"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}

flake.nix

@@ -0,0 +1,214 @@
+{
+  inputs = {
+    nixpkgs.url = "github:NixOS/nixpkgs/nixos-24.11";
+    flake-utils.url = "github:numtide/flake-utils";
+  };
+  outputs = { self, nixpkgs, flake-utils, ... }:
+    flake-utils.lib.eachSystem
+      [
+        "x86_64-linux"
+      ]
+
+      (system:
+        let
+          pkgs = import nixpkgs { inherit system; };
+          lib = pkgs.lib;
+
+          mkSpotApps = appNames:
+            pkgs.lib.genAttrs appNames
+              (name: flake-utils.lib.mkApp {
+                drv = self.packages.${system}.spot;
+                name = name;
+              });
+
+          spotPackage =
+            let
+              inherit (builtins)
+                filter
+                head
+                isString
+                match
+                readFile
+                split
+              ;
+
+              # NOTE: Maintaining the version separately would be a pain, and we
+              # can't have a flake.nix.in with a @VERSION@ because it would make
+              # the flake unusable without running autoconf first, defeating some
+              # of its purpose.
+              #
+              # So let's get it the hard way instead :)
+              extractVersionRegex = ''^AC_INIT\(\[spot], \[([^]]+)], \[spot@lrde\.epita\.fr]\)$'';
+              getLines = (fileContent:
+                filter isString (split "\n" fileContent)
+              );
+              findVersionLine = (lines:
+                lib.lists.findFirst
+                  (l: lib.strings.hasPrefix "AC_INIT(" l)
+                  null
+                  lines
+              );
+              getVersion = (file:
+                let
+                  lines = getLines (readFile file);
+                  versionLine = findVersionLine lines;
+                  version = head (match extractVersionRegex versionLine);
+                in
+                  version
+              );
+            in
+              {
+                lib,
+                pkgs,
+                stdenv,
+                # FIXME: do we want this flag?
+                buildOrgDoc ? false,
+                # Whether to enable Spot's Python 3 bindings
+                enablePython ? false
+              }:
+              stdenv.mkDerivation {
+                pname = "spot";
+                version = getVersion ./configure.ac;
+
+                src = self;
+
+                enableParallelBuilding = true;
+
+                # NOTE: Nix enables a lot of hardening flags by default, some of
+                # these probably harm performance so I've disabled everything
+                # (haven't benchmarked with vs without these, though).
+                hardeningDisable = [ "all" ];
+
+                # NOTE: mktexpk fails without a HOME set
+                preBuild = ''
+                  export HOME=$TMPDIR
+                  patchShebangs tools
+                '' + (if buildOrgDoc then ''
+                ln -s ${pkgs.plantuml}/lib/plantuml.jar doc/org/plantuml.jar
+              '' else ''
+                  touch doc/org-stamp
+                '');
+
+                configureFlags = [
+                  "--disable-devel"
+                  "--enable-optimizations"
+                ] ++ lib.optional (!enablePython) [
+                  "--disable-python"
+                ];
+
+                nativeBuildInputs = with pkgs; [
+                  autoreconfHook
+
+                  autoconf
+                  automake
+                  bison
+                  flex
+                  libtool
+                  perl
+                ] ++ lib.optional buildOrgDoc [
+                  graphviz
+                  groff
+                  plantuml
+                  pdf2svg
+                  R
+                ] ++ lib.optional enablePython [
+                  python3
+                  swig4
+                ];
+
+                buildInputs = with pkgs; [
+                  # should provide the minimum amount of packages necessary for
+                  # building tl.pdf
+                  (texlive.combine {
+                    inherit (texlive)
+                      scheme-basic
+                      latexmk
+
+                      booktabs
+                      cm-super
+                      doi
+                      doublestroke
+                      etoolbox
+                      koma-script
+                      mathabx-type1
+                      mathpazo
+                      metafont
+                      microtype
+                      nag
+                      pgf
+                      standalone
+                      stmaryrd
+                      tabulary
+                      todonotes
+                      wasy-type1
+                      wasysym
+                    ;
+                  })
+                ];
+              };
+        in
+          {
+            defaultPackage = self.packages.${system}.spot;
+
+            packages = {
+              # binaries + library only
+              spot = pkgs.callPackage spotPackage {};
+
+              # NOTE: clang build is broken on Nix when linking to stdlib++, using
+              #       libcxx instead. See:
+              #       https://github.com/NixOS/nixpkgs/issues/91285
+              spotClang = pkgs.callPackage spotPackage {
+                stdenv = pkgs.llvmPackages.libcxxStdenv;
+              };
+
+              spotWithOrgDoc = pkgs.callPackage spotPackage {
+                buildOrgDoc = true;
+              };
+
+              spotWithPython = pkgs.python3Packages.toPythonModule (
+                pkgs.callPackage spotPackage {
+                  enablePython = true;
+                }
+              );
+
+              spotFull = pkgs.python3Packages.toPythonModule (
+                pkgs.callPackage spotPackage {
+                  buildOrgDoc = true; enablePython = true;
+                }
+              );
+            };
+
+            apps = mkSpotApps [
+              "autcross"
+              "autfilt"
+              "dstar2tgba"
+              "genaut"
+              "genltl"
+              "ltl2tgba"
+              "ltl2tgta"
+              "ltlcross"
+              "ltldo"
+              "ltlfilt"
+              "ltlgrind"
+              "ltlmix"
+              "ltlsynt"
+              "randaut"
+              "randltl"
+            ];
+
+            devShell = pkgs.mkShell {
+              name = "spot-dev";
+              inputsFrom = [ self.packages.${system}.spotFull ];
+              buildInputs = [
+                pkgs.gdb
+                pkgs.clang-tools # for clangd
+                pkgs.bear
+
+                (pkgs.python3.withPackages (p: [
+                  p.jupyter
+                  p.ipython # otherwise ipython module isn't found when running ipynb tests
+                ]))
+              ];
+            };
+          });
+}

python/spot/impl.i

@@ -89,6 +89,7 @@
 #include <spot/tl/derive.hh>
 #include <spot/tl/dot.hh>
 #include <spot/tl/expansions.hh>
+#include <spot/tl/expansions2.hh>
 #include <spot/tl/nenoform.hh>
 #include <spot/tl/print.hh>
 #include <spot/tl/simplify.hh>
@@ -638,6 +639,7 @@ namespace std {
 %include <spot/tl/contain.hh>
 %include <spot/tl/derive.hh>
 %include <spot/tl/expansions.hh>
+%include <spot/tl/expansions2.hh>
 %include <spot/tl/dot.hh>
 %include <spot/tl/nenoform.hh>
 %include <spot/tl/sonf.hh>

spot/tl/Makefile.am

@@ -32,7 +32,7 @@ tl_HEADERS =					\
   dot.hh					\
   environment.hh				\
   exclusive.hh					\
-  expansions.hh					\
+  expansions2.hh					\
   formula.hh					\
   hierarchy.hh					\
   length.hh					\
@@ -60,6 +60,7 @@ libtl_la_SOURCES =				\
   dot.cc					\
   exclusive.cc					\
   expansions.cc					\
+  expansions2.cc					\
   formula.cc					\
   hierarchy.cc					\
   length.cc					\

spot/tl/expansions.cc

@@ -18,9 +18,11 @@
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 #include "config.h"
+#include <algorithm>
 #include <spot/misc/minato.hh>
 #include <spot/priv/robin_hood.hh>
 #include <spot/tl/expansions.hh>
+#include <spot/tl/formula.hh>
 #include <spot/twa/bdddict.hh>
 #include <spot/twa/formula2bdd.hh>
 #include <spot/twaalgos/remprop.hh>
@@ -278,11 +280,11 @@ namespace spot
           bdd dest_bdd = bdd_restrict(exp_, letter);
           formula dest = bdd_to_sere(dest_bdd);
 
-          #ifndef NDEBUG
-          // make sure it didn't exist before
-          auto it = std::find(res.begin(), res.end(), {letter, dest});
-          SPOT_ASSERT(it == res.end());
-          #endif
+          // #ifndef NDEBUG
+          // // make sure it didn't exist before
+          // auto it = std::find(res.begin(), res.end(), {letter, dest});
+          // SPOT_ASSERT(it == res.end());
+          // #endif
 
           res.push_back({letter, dest});
         }
@@ -338,7 +340,7 @@ namespace spot
 
       expansion_t res;
 
-      for (const auto [prefix, suffix] : unique_map)
+      for (const auto& [prefix, suffix] : unique_map)
       {
         if (!suffix.is(op::OrRat))
         {
@@ -435,17 +437,22 @@ namespace spot
         }
 
         exp.clear();
-        for (const auto [suffix, prefix] : unique_map)
+        for (const auto& [suffix, prefix] : unique_map)
         {
           exp.push_back({prefix, suffix});
         }
       }
 
-      if (opts & exp_opts::expand_opt::UniquePrefix)
+      if (opts & exp_opts::expand_opt::UniquePrefix
+          || opts & exp_opts::expand_opt::UniquePrefixSeenOpt
+          || opts & exp_opts::expand_opt::UniquePrefixSeenCountOpt)
       {
-        exp = unique_prefix(exp);
-        //exp = unique_prefix_seen(exp, seen);
-        //exp = unique_prefix_count(exp, seen);
+        if (opts & exp_opts::expand_opt::UniquePrefixSeenOpt)
+          exp = unique_prefix_seen(exp, seen);
+        else if (opts & exp_opts::expand_opt::UniquePrefixSeenCountOpt)
+          exp = unique_prefix_count(exp, seen);
+        else
+          exp = unique_prefix(exp);
       }
 
       if (opts & exp_opts::expand_opt::UniqueSuffixPost)
@@ -462,7 +469,7 @@ namespace spot
         }
 
         exp.clear();
-        for (const auto [suffix, prefix] : unique_map)
+        for (const auto& [suffix, prefix] : unique_map)
         {
           exp.push_back({prefix, suffix});
         }
@@ -490,6 +497,18 @@ namespace spot
             }
           exp = exp_new;
         }
+
+      // sort and remove duplicates from expansion to canonicalize it for
+      // eventual signature use
+      if (exp.size() >= 2)
+        {
+          std::sort(exp.begin(), exp.end(),
+                    [](const auto& lhs, const auto& rhs) {
+                         return std::make_pair(lhs.first.id(), lhs.second.id())
+                           < std::make_pair(rhs.first.id(), rhs.second.id());
+                    });
+          exp.erase(std::unique(exp.begin(), exp.end()), exp.end());
+        }
     }
   }
 
@@ -717,7 +736,10 @@ namespace spot
                         if ((li & kj) != bddfalse)
                           res.push_back({li & kj, fj});
                   }
-                res.push_back({li, formula::Fusion({ei, F})});
+
+                formula ei_fusion_F = formula::Fusion({ei, F});
+                if (!ei_fusion_F.is(op::ff))
+                  res.push_back({li, ei_fusion_F});
               }
 
             finalize(res, opts, d, seen);
@@ -817,7 +839,7 @@ namespace spot
   struct signature_hash
   {
     std::size_t
-    operator() (const std::pair<bool, expansion_t>& sig) const
+    operator() (const std::pair<bool, expansion_t>& sig) const noexcept
     {
       size_t hash = std::hash<bool>()(sig.first);
 

spot/tl/expansions.hh

@@ -47,6 +47,8 @@ namespace spot
       Determinize = 256,
       UniquePrefixSeenOpt = 512,
       UniqueSuffixPost = 1024,
+      UniquePrefixSeenCountOpt = 2048,
+      TransitionBased = 4096,
     };
   };
 

spot/tl/expansions2.cc

@@ -0,0 +1,943 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2021 Laboratoire de Recherche et Développement de
+// l'Epita (LRDE).
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 3 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+#include "config.h"
+#include <algorithm>
+#include <spot/misc/minato.hh>
+#include <spot/priv/robin_hood.hh>
+#include <spot/tl/expansions2.hh>
+#include <spot/tl/formula.hh>
+#include <spot/twa/bdddict.hh>
+#include <spot/twa/formula2bdd.hh>
+#include <spot/twaalgos/remprop.hh>
+
+namespace spot
+{
+  namespace
+  {
+    // FIXME: could probably just return a map directly
+    static std::vector<std::string>
+    formula_aps(formula f)
+    {
+      auto res = std::unordered_set<std::string>();
+
+      f.traverse([&res](formula f)
+      {
+        if (f.is(op::ap))
+        {
+          res.insert(f.ap_name());
+          return true;
+        }
+
+        return false;
+      });
+
+      return std::vector(res.begin(), res.end());
+    }
+
+    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));
+    }
+
+    class bdd_finalizer
+    {
+      public:
+        int encode(formula f)
+          {
+            bool is_anon = false;
+            int var_num;
+            auto it = formula2bdd_.find(f);
+            if (it != formula2bdd_.end())
+            {
+              var_num = it->second;
+            }
+            else
+            {
+              if (opt_sigma_star_ && (f.is(op::Star)
+                                      && f[0].is(op::tt)
+                                      && f.min() == 0
+                                      && f.max() == formula::unbounded()))
+                {
+                  var_num = bddtrue.id();
+                }
+              else if (opt_bdd_encode_ && (f.is(op::AndRat) || f.is(op::OrRat)))
+                {
+                  bdd var = f.is(op::AndRat) ? bdd(bddtrue) : bdd(bddfalse);
+                  for (const auto& sub_f : f)
+                    {
+                      int bddid = encode(sub_f);
+                      bdd subvar = bdd_ithvar(bddid);
+                      var = f.is(op::AndRat) ? var & subvar : var | subvar;
+                    }
+                  var_num = var.id();
+                }
+              else
+                {
+                  var_num = d_->register_anonymous_variables(1, this);
+                  is_anon = true;
+                }
+
+              formula2bdd_.insert({f, var_num});
+              bdd2formula_.insert({var_num, f});
+            }
+
+            bdd var = bdd_ithvar(var_num);
+
+            if (is_anon)
+              anon_set_ &= var;
+
+            return var_num;
+          }
+
+        bdd_finalizer(expansion_t& exp, bdd_dict_ptr d, bool opt_sigma_star, bool opt_bdd_encode)
+          : anon_set_(bddtrue)
+          , d_(d)
+          , opt_sigma_star_(opt_sigma_star)
+          , opt_bdd_encode_(opt_bdd_encode)
+        {
+          for (const auto& [prefix, suffix] : exp)
+          {
+            int var_num = encode(suffix);
+            bdd var = bdd_ithvar(var_num);
+            exp_ |= prefix & var;
+          }
+        }
+
+        ~bdd_finalizer()
+        {
+          d_->unregister_all_my_variables(this);
+        }
+
+        expansion_t
+        simplify(exp_opts::expand_opt opts);
+
+      private:
+        bdd exp_;
+        bdd anon_set_;
+        std::map<formula, int> formula2bdd_;
+        std::map<int, formula> bdd2formula_;
+        bdd_dict_ptr d_;
+        bool opt_sigma_star_;
+        bool opt_bdd_encode_;
+
+        formula var_to_formula(int var);
+        formula conj_bdd_to_sere(bdd b);
+        formula bdd_to_sere(bdd b);
+    };
+
+    formula
+    bdd_finalizer::var_to_formula(int var)
+    {
+      formula f = bdd2formula_[var];
+      assert(f);
+      return f;
+    }
+
+    formula
+    bdd_finalizer::bdd_to_sere(bdd f)
+    {
+      if (f == bddfalse)
+        return formula::ff();
+
+      std::vector<formula> v;
+      minato_isop isop(f);
+      bdd cube;
+      while ((cube = isop.next()) != bddfalse)
+        v.emplace_back(conj_bdd_to_sere(cube));
+      return formula::OrRat(std::move(v));
+    }
+
+    formula
+    bdd_finalizer::conj_bdd_to_sere(bdd b)
+    {
+      if (b == bddtrue)
+        {
+          if (opt_sigma_star_){
+            return formula::Star(formula::tt(), 0, formula::unbounded());
+          } else {
+            return formula::tt();
+          }
+        }
+      if (b == bddfalse)
+        return formula::ff();
+
+      // Unroll the first loop of the next do/while loop so that we
+      // do not have to create v when b is not a conjunction.
+      formula res = var_to_formula(bdd_var(b));
+      bdd high = bdd_high(b);
+      if (high == bddfalse)
+      {
+        res = formula::Not(res);
+        b = bdd_low(b);
+      }
+      else
+      {
+        assert(bdd_low(b) == bddfalse);
+        b = high;
+      }
+      if (b == bddtrue)
+        return res;
+      std::vector<formula> v{std::move(res)};
+      do
+      {
+        res = var_to_formula(bdd_var(b));
+        high = bdd_high(b);
+        if (high == bddfalse)
+        {
+          res = formula::Not(res);
+          b = bdd_low(b);
+        }
+        else
+        {
+          assert(bdd_low(b) == bddfalse);
+          b = high;
+        }
+        assert(b != bddfalse);
+        v.emplace_back(std::move(res));
+      }
+      while (b != bddtrue);
+      return formula::multop(op::AndRat, std::move(v));
+    }
+
+    expansion_t
+    bdd_finalizer::simplify(exp_opts::expand_opt opts)
+    {
+      expansion_t res;
+
+      if (opts & exp_opts::expand_opt::BddMinterm)
+      {
+        bdd prop_set = bdd_exist(bdd_support(exp_), anon_set_);
+        bdd or_labels = bdd_exist(exp_, anon_set_);
+        // TODO: check are_equivalent avec or_labels/exp_ en premier argument
+        for (bdd letter: minterms_of(or_labels, prop_set))
+        {
+          bdd dest_bdd = bdd_restrict(exp_, letter);
+          formula dest = bdd_to_sere(dest_bdd);
+
+          // #ifndef NDEBUG
+          // // make sure it didn't exist before
+          // auto it = std::find(res.begin(), res.end(), {letter, dest});
+          // SPOT_ASSERT(it == res.end());
+          // #endif
+
+          res.push_back({letter, dest});
+        }
+      }
+      else // BddIsop
+      {
+        minato_isop isop(exp_);
+        bdd cube;
+        while ((cube = isop.next()) != bddfalse)
+        {
+          bdd letter = bdd_exist(cube, anon_set_);
+          bdd suffix = bdd_existcomp(cube, anon_set_);
+          formula dest = conj_bdd_to_sere(suffix);
+
+          res.push_back({letter, dest});
+        }
+      }
+
+      return res;
+    }
+
+    expansion_t
+    unique_prefix(const expansion_t& exp)
+    {
+      std::map<bdd, formula, bdd_less_than> unique_map;
+      for (const auto& [prefix, suffix] : exp)
+      {
+        auto res = unique_map.insert({prefix, suffix});
+        if (!res.second)
+        {
+          auto it = res.first;
+          it->second = formula::OrRat({it->second, suffix});
+        }
+      }
+
+      expansion_t res(unique_map.begin(), unique_map.end());
+      return res;
+    }
+
+    expansion_t
+    unique_prefix_seen(const expansion_t& exp, std::unordered_set<formula>* seen)
+    {
+      std::map<bdd, formula, bdd_less_than> unique_map;
+      for (const auto& [prefix, suffix] : exp)
+      {
+        auto res = unique_map.insert({prefix, suffix});
+        if (!res.second)
+        {
+          auto it = res.first;
+          it->second = formula::OrRat({it->second, suffix});
+        }
+      }
+
+      expansion_t res;
+
+      for (const auto& [prefix, suffix] : unique_map)
+      {
+        if (!suffix.is(op::OrRat))
+        {
+          res.push_back({prefix, suffix});
+          continue;
+        }
+
+        std::vector<formula> merge;
+        std::vector<formula> single;
+
+        for (const auto& sub_f : suffix)
+          {
+            if (seen->find(sub_f) != seen->end())
+              {
+                single.push_back(sub_f);
+              }
+            else
+              {
+                merge.push_back(sub_f);
+              }
+          }
+
+        for (const auto& sub_f : single)
+          res.push_back({prefix, sub_f});
+
+        if (!merge.empty())
+          res.push_back({prefix, formula::OrRat(merge)});
+      }
+
+      return res;
+    }
+
+    size_t count_new(const expansion_t& exp, std::unordered_set<formula>* seen)
+    {
+      size_t count = 0;
+      for (const auto& [_, suffix] : exp)
+      {
+        if (seen->find(suffix) == seen->end())
+          count++;
+      }
+      return count;
+    }
+
+    const expansion_t&
+    find_smallest(const expansion_t& left,
+                  const expansion_t& right,
+                  std::unordered_set<formula>* seen)
+    {
+      size_t left_new = count_new(left, seen);
+      size_t right_new = count_new(right, seen);
+
+      if (left_new < right_new)
+        return left;
+
+      if (left_new == right_new && left.size() > right.size())
+        return right;
+
+      return right;
+    }
+
+    expansion_t
+    unique_prefix_count(const expansion_t& exp, std::unordered_set<formula>* seen)
+    {
+      expansion_t up = unique_prefix(exp);
+      expansion_t up_seen = unique_prefix_seen(exp, seen);
+
+      const expansion_t& maybe_smallest = find_smallest(exp, up, seen);
+      const expansion_t& smallest = find_smallest(maybe_smallest, up_seen, seen);
+
+      return smallest;
+    }
+
+    void
+    finalize(expansion_t& exp, exp_opts::expand_opt opts, bdd_dict_ptr d, std::unordered_set<formula>* seen)
+    {
+      if (opts & (exp_opts::expand_opt::BddIsop
+                  | exp_opts::expand_opt::BddMinterm))
+      {
+        bdd_finalizer bddf(exp, d, opts & exp_opts::expand_opt::BddSigmaStar, opts & exp_opts::expand_opt::BddEncode);
+        exp = bddf.simplify(opts);
+      }
+
+      if (opts & exp_opts::expand_opt::UniqueSuffixPre)
+      {
+        std::map<formula, bdd> unique_map;
+        for (const auto& [prefix, suffix] : exp)
+        {
+          auto res = unique_map.insert({suffix, prefix});
+          if (!res.second)
+          {
+            auto it = res.first;
+            it->second |= prefix;
+          }
+        }
+
+        exp.clear();
+        for (const auto& [suffix, prefix] : unique_map)
+        {
+          exp.push_back({prefix, suffix});
+        }
+      }
+
+      if (opts & exp_opts::expand_opt::UniquePrefix
+          || opts & exp_opts::expand_opt::UniquePrefixSeenOpt
+          || opts & exp_opts::expand_opt::UniquePrefixSeenCountOpt)
+      {
+        if (opts & exp_opts::expand_opt::UniquePrefixSeenOpt)
+          exp = unique_prefix_seen(exp, seen);
+        else if (opts & exp_opts::expand_opt::UniquePrefixSeenCountOpt)
+          exp = unique_prefix_count(exp, seen);
+        else
+          exp = unique_prefix(exp);
+      }
+
+      if (opts & exp_opts::expand_opt::UniqueSuffixPost)
+      {
+        std::map<formula, bdd> unique_map;
+        for (const auto& [prefix, suffix] : exp)
+        {
+          auto res = unique_map.insert({suffix, prefix});
+          if (!res.second)
+          {
+            auto it = res.first;
+            it->second |= prefix;
+          }
+        }
+
+        exp.clear();
+        for (const auto& [suffix, prefix] : unique_map)
+        {
+          exp.push_back({prefix, suffix});
+        }
+      }
+
+      if (opts & exp_opts::expand_opt::Determinize)
+        {
+          expansion_t exp_new;
+
+          bdd props = bddtrue;
+          for (const auto& [prefix, _] : exp)
+            props &= bdd_support(prefix);
+
+          std::vector<formula> dests;
+          for (bdd letter : minterms_of(bddtrue, props))
+            {
+              for (const auto& [prefix, suffix] : exp)
+                {
+                  if (bdd_implies(letter, prefix))
+                    dests.push_back(suffix);
+                }
+              formula or_dests = formula::OrRat(dests);
+              exp_new.push_back({letter, or_dests});
+              dests.clear();
+            }
+          exp = exp_new;
+        }
+
+      // sort expansion to canonicalize it for eventual signature use
+      if (exp.size() >= 2)
+        {
+          std::sort(exp.begin(), exp.end(),
+                    [](const auto& lhs, const auto& rhs) {
+                         return std::make_pair(lhs.first.id(), lhs.second.id())
+                           < std::make_pair(rhs.first.id(), rhs.second.id());
+                    });
+          exp.erase(std::unique(exp.begin(), exp.end()), exp.end());
+        }
+    }
+  }
+
+  formula
+  expansion_to_formula2(expansion_t e, bdd_dict_ptr& d)
+  {
+    std::vector<formula> res;
+
+    for (const auto& [key, val] : e)
+      {
+        formula prefix = bdd_to_formula(key, d);
+        res.push_back(formula::Concat({prefix, val}));
+      }
+
+    return formula::OrRat(res);
+  }
+
+  expansion_t
+  expansion2(formula f, const bdd_dict_ptr& d, void *owner, exp_opts::expand_opt opts, std::unordered_set<formula>* seen)
+  {
+    using exp_t = expansion_t;
+
+    if (f.is_boolean())
+      {
+        auto f_bdd = formula_to_bdd(f, d, owner);
+
+        if (f_bdd == bddfalse)
+          return {};
+
+        return {{f_bdd, formula::eword()}};
+      }
+
+    auto rec = [&d, owner, opts, seen](formula f){
+      return expansion2(f, d, owner, exp_opts::None, seen);
+    };
+
+
+    switch (f.kind())
+      {
+        case op::ff:
+        case op::tt:
+        case op::ap:
+          SPOT_UNREACHABLE();
+
+        case op::eword:
+          // return {{bddfalse, formula::ff()}};
+          return {};
+
+        case op::Concat:
+          {
+            auto exps = rec(f[0]);
+
+            exp_t res;
+            for (const auto& [bdd_l, form] : exps)
+              {
+                res.push_back({bdd_l, formula::Concat({form, f.all_but(0)})});
+              }
+
+            if (f[0].accepts_eword())
+              {
+                auto exps_rest = rec(f.all_but(0));
+                for (const auto& [bdd_l, form] : exps_rest)
+                  {
+                    res.push_back({bdd_l, form});
+                  }
+              }
+
+            finalize(res, opts, d, seen);
+            return res;
+          }
+
+        case op::FStar:
+          {
+            formula E = f[0];
+
+            if (f.min() == 0 && f.max() == 0)
+              return {{bddtrue, formula::eword()}};
+
+            auto min = f.min() == 0 ? 0 : (f.min() - 1);
+            auto max = f.max() == formula::unbounded()
+                         ? formula::unbounded()
+                         : (f.max() - 1);
+
+            auto E_i_j_minus = formula::FStar(E, min, max);
+
+            auto exp = rec(E);
+            exp_t res;
+            for (const auto& [li, ei] : exp)
+              {
+                res.push_back({li, formula::Fusion({ei, E_i_j_minus})});
+
+                if (ei.accepts_eword() && f.min() != 0)
+                  {
+                    for (const auto& [ki, fi] : rec(E_i_j_minus))
+                      {
+                        // FIXME: build bdd once
+                        if ((li & ki) != bddfalse)
+                          res.push_back({li & ki, fi});
+                      }
+                  }
+              }
+            if (f.min() == 0)
+              res.push_back({bddtrue, formula::eword()});
+
+            finalize(res, opts, d, seen);
+            return res;
+          }
+
+        case op::Star:
+          {
+            auto min = f.min() == 0 ? 0 : (f.min() - 1);
+            auto max = f.max() == formula::unbounded()
+                         ? formula::unbounded()
+                         : (f.max() - 1);
+
+            auto exps = rec(f[0]);
+
+            exp_t res;
+            for (const auto& [bdd_l, form] : exps)
+              {
+                res.push_back({bdd_l, formula::Concat({form, formula::Star(f[0], min, max)})});
+              }
+
+            finalize(res, opts, d, seen);
+            return res;
+          }
+
+        case op::AndNLM:
+          {
+            formula rewrite = rewrite_and_nlm(f);
+            auto res = rec(rewrite);
+            finalize(res, opts, d, seen);
+            return res;
+          }
+
+        case op::first_match:
+          {
+            auto exps = rec(f[0]);
+
+            exp_t res;
+            for (const auto& [bdd_l, form] : exps)
+              {
+                res.push_back({bdd_l, form});
+              }
+
+            // determinize
+            bdd or_labels = bddfalse;
+            bdd support = bddtrue;
+            bool is_det = true;
+            for (const auto& [l, _] : res)
+              {
+                support &= bdd_support(l);
+                if (is_det)
+                  is_det = !bdd_have_common_assignment(l, or_labels);
+                or_labels |= l;
+              }
+
+            if (is_det)
+              {
+                for (auto& [_, dest] : res)
+                  dest = formula::first_match(dest);
+                finalize(res, opts, d, seen);
+                return res;
+              }
+
+            exp_t res_det;
+            std::vector<formula> dests;
+            for (bdd l: minterms_of(or_labels, support))
+              {
+                for (const auto& [ndet_label, ndet_dest] : res)
+                  {
+                    if (bdd_implies(l, ndet_label))
+                      dests.push_back(ndet_dest);
+                  }
+                formula or_dests = formula::OrRat(dests);
+                res_det.push_back({l, or_dests});
+                dests.clear();
+              }
+
+            for (auto& [_, dest] : res_det)
+              dest = formula::first_match(dest);
+            finalize(res_det, opts, d, seen);
+            return res_det;
+          }
+
+        case op::Fusion:
+          {
+            exp_t res;
+            formula E = f[0];
+            formula F = f.all_but(0);
+
+            exp_t Ei = rec(E);
+            // TODO: std::option
+            exp_t Fj = rec(F);
+
+            for (const auto& [li, ei] : Ei)
+              {
+                if (ei.accepts_eword())
+                  {
+                    for (const auto& [kj, fj] : Fj)
+                        if ((li & kj) != bddfalse)
+                          res.push_back({li & kj, fj});
+                  }
+                res.push_back({li, formula::Fusion({ei, F})});
+              }
+
+            finalize(res, opts, d, seen);
+            return res;
+          }
+
+        case op::AndRat:
+          {
+            exp_t res;
+            for (const auto& sub_f : f)
+              {
+                auto exps = rec(sub_f);
+
+                if (exps.empty())
+                  {
+                    // op::AndRat: one of the expansions was empty (the only
+                    //             edge was `false`), so the AndRat is empty as
+                    //             well
+                    res.clear();
+                    break;
+                  }
+
+                if (res.empty())
+                  {
+                    res = std::move(exps);
+                    continue;
+                  }
+
+                exp_t new_res;
+                bool inserted = false;
+                for (const auto& [l_key, l_val] : exps)
+                  {
+                    for (const auto& [r_key, r_val] : res)
+                      {
+                        if ((l_key & r_key) != bddfalse)
+                          {
+                            new_res.push_back({l_key & r_key, formula::multop(f.kind(), {l_val, r_val})});
+                            inserted = true;
+                          }
+                      }
+                  }
+
+                if (!inserted)
+                  {
+                    // all prefix conjuctions led to bddfalse, And is empty
+                    res.clear();
+                    break;
+                  }
+
+                res = std::move(new_res);
+              }
+
+            finalize(res, opts, d, seen);
+            return res;
+          }
+
+        case op::OrRat:
+          {
+            exp_t res;
+            for (const auto& sub_f : f)
+              {
+                auto exps = rec(sub_f);
+                if (exps.empty())
+                  continue;
+
+                if (res.empty())
+                  {
+                    res = std::move(exps);
+                    continue;
+                  }
+
+                for (const auto& [label, dest] : exps)
+                  res.push_back({label, dest});
+              }
+
+            finalize(res, opts, d, seen);
+            return res;
+          }
+
+        default:
+          std::cerr << "unimplemented kind "
+                    << static_cast<int>(f.kind())
+                    << std::endl;
+          SPOT_UNIMPLEMENTED();
+      }
+
+    return {};
+  }
+
+  twa_graph_ptr
+  expand_automaton2(formula f, bdd_dict_ptr d, exp_opts::expand_opt opts)
+  {
+    auto finite = expand_finite_automaton2(f, d, opts);
+    return from_finite(finite);
+  }
+
+  struct signature_hash
+  {
+    std::size_t
+    operator() (const expansion_t& sig) const noexcept
+    {
+      size_t hash = 0;
+
+      for (const auto& keyvalue : sig)
+        {
+          hash ^= (bdd_hash()(keyvalue.first) ^ std::hash<formula>()(keyvalue.second))
+            + 0x9e3779b9 + (hash << 6) + (hash >> 2);
+        }
+
+      return hash;
+    }
+  };
+
+  twa_graph_ptr
+  expand_finite_automaton2(formula f, bdd_dict_ptr d, exp_opts::expand_opt opts)
+  {
+    bool signature_merge = opts & exp_opts::expand_opt::SignatureMerge;
+
+    auto aut = make_twa_graph(d);
+
+    aut->prop_state_acc(false);
+    const auto acc_mark = aut->set_buchi();
+
+    auto formula2state = robin_hood::unordered_map<formula, unsigned>();
+    auto signature2state = std::unordered_map<expansion_t, unsigned, signature_hash>();
+    auto seen = std::unordered_set<formula>();
+    seen.insert(f);
+
+    unsigned init_state = aut->new_state();
+    aut->set_init_state(init_state);
+    formula2state.insert({ f, init_state });
+
+
+    auto f_aps = formula_aps(f);
+    for (auto& ap : f_aps)
+        aut->register_ap(ap);
+
+    auto formula2signature = robin_hood::unordered_map<formula, expansion_t>();
+    auto get_signature = [&](const formula& form) -> expansion_t
+      {
+        auto it = formula2signature.find(form);
+        if (it != formula2signature.end())
+          {
+            return it->second;
+          }
+        auto exp = expansion2(form, d, aut.get(), opts, &seen);
+        formula2signature.insert({form, exp});
+        return exp;
+      };
+
+    if (signature_merge)
+      signature2state.insert({ get_signature(f), init_state});
+
+    auto todo = std::vector<std::pair<formula, unsigned>>();
+    todo.push_back({f, init_state});
+
+    auto state_names = new std::vector<std::string>();
+    std::ostringstream ss;
+    ss << f;
+    state_names->push_back(ss.str());
+
+    auto find_dst = [&](formula suffix) -> unsigned
+      {
+        unsigned dst;
+        auto it = formula2state.find(suffix);
+        if (it != formula2state.end())
+        {
+          dst = it->second;
+        }
+        else
+        {
+          if (signature_merge)
+            {
+              auto exp = get_signature(suffix);
+
+              auto it2 = signature2state.find(exp);
+              if (it2 != signature2state.end())
+                {
+                  formula2state.insert({suffix, it2->second});
+                  return it2->second;
+                }
+            }
+
+          dst = aut->new_state();
+          todo.push_back({suffix, dst});
+          seen.insert(suffix);
+
+          formula2state.insert({suffix, dst});
+          if (signature_merge)
+            signature2state.insert({get_signature(suffix), dst});
+
+          std::ostringstream ss;
+          ss << suffix;
+          state_names->push_back(ss.str());
+        }
+
+        return dst;
+      };
+
+    while (!todo.empty())
+      {
+        auto [curr_f, curr_state] = todo[todo.size() - 1];
+        todo.pop_back();
+
+
+        auto exp = get_signature(curr_f);
+
+        for (const auto& [letter, suffix] : exp)
+          {
+            if (suffix.is(op::ff))
+              // TODO ASSERT NOT
+              continue;
+
+            auto dst = find_dst(suffix);
+
+            auto curr_acc_mark = suffix.accepts_eword() ? acc_mark : acc_cond::mark_t();
+            aut->new_edge(curr_state, dst, letter, curr_acc_mark);
+          }
+      }
+
+    aut->set_named_prop("state-names", state_names);
+
+    if ((opts & exp_opts::MergeEdges)
+        && !(opts & exp_opts::UniqueSuffixPre || opts & exp_opts::UniqueSuffixPost))
+      aut->merge_edges();
+
+    return aut;
+  }
+}

spot/tl/expansions2.hh

@@ -0,0 +1,45 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2021 Laboratoire de Recherche et Développement de
+// l'Epita (LRDE).
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 3 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+#pragma once
+
+#include <map>
+
+#include <bddx.h>
+
+#include <spot/misc/bddlt.hh>
+#include <spot/tl/expansions.hh>
+#include <spot/tl/formula.hh>
+#include <spot/twa/bdddict.hh>
+#include <spot/twa/twagraph.hh>
+
+namespace spot
+{
+  SPOT_API expansion_t
+  expansion2(formula f, const bdd_dict_ptr& d, void *owner, exp_opts::expand_opt opts, std::unordered_set<formula>* seen = nullptr);
+
+  SPOT_API twa_graph_ptr
+  expand_automaton2(formula f, bdd_dict_ptr d, exp_opts::expand_opt opts);
+
+  SPOT_API twa_graph_ptr
+  expand_finite_automaton2(formula f, bdd_dict_ptr d, exp_opts::expand_opt opts);
+
+  SPOT_API formula
+  expansion_to_formula2(expansion_t e, bdd_dict_ptr& d);
+}

spot/twaalgos/ltl2tgba_fm.cc

@@ -24,6 +24,7 @@
 #include <spot/tl/apcollect.hh>
 #include <spot/tl/mark.hh>
 #include <spot/tl/nenoform.hh>
+#include <spot/tl/expansions.hh>
 #include <cassert>
 #include <memory>
 #include <utility>
@@ -101,15 +102,14 @@ namespace spot
     class ratexp_to_dfa final
     {
       typedef twa_graph::namer<formula> namer;
+      // Use robin_hood::pair because std::pair is not no-throw constructible
+      typedef robin_hood::pair<twa_graph_ptr, const namer*> labelled_aut;
     public:
       ratexp_to_dfa(translate_dict& dict, bool disable_scc_trimming = false);
 
       std::vector<std::pair<bdd, formula>> succ(formula f);
       ~ratexp_to_dfa();
 
-    protected:
-      // Use robin_hood::pair because std::pair is not no-throw constructible
-      typedef robin_hood::pair<twa_graph_ptr, const namer*> labelled_aut;
       labelled_aut translate(formula f);
 
     private:
@@ -224,6 +224,7 @@ namespace spot
       int
       register_proposition(formula f)
       {
+        // TODO: call this in expansions
         int num = dict->register_proposition(f, this);
         var_set &= bdd_ithvar(num);
         return num;
@@ -887,8 +888,22 @@ namespace spot
       bdd res;
       if (!f.is_boolean())
         {
-          ratexp_trad_visitor v(dict, to_concat);
-          res = v.visit(f);
+          if (sere_translation_options() == 0)
+            {
+              ratexp_trad_visitor v(dict, to_concat);
+              res = v.visit(f);
+            }
+          else // version expansion
+            {
+              res = bddfalse;
+              for (auto [label, succ]: expansion(f, dict.dict, &dict, exp_opts::expand_opt::None, nullptr))
+                {
+                  if (to_concat)
+                    succ = formula::Concat({succ, to_concat});
+                  int x = dict.register_next_variable(succ);
+                  res |= label & bdd_ithvar(x);
+                }
+            }
         }
       else
         {
@@ -2191,6 +2206,10 @@ namespace spot
   twa_graph_ptr
   sere_to_tgba(formula f, const bdd_dict_ptr& dict, bool disable_scc_trimming)
   {
+    // make sure we use bdd translation in this case
+    auto old_opt = sere_translation_options();
+    sere_translation_options("bdd");
+
     f = negative_normal_form(f);
 
     tl_simplifier* s = new tl_simplifier(dict);
@@ -2199,7 +2218,7 @@ namespace spot
     translate_dict d(a, s, false, false, false);
     ratexp_to_dfa sere2dfa(d, disable_scc_trimming);
 
-    auto [dfa, namer, state] = sere2dfa.succ(f);
+    auto [dfa, namer] = sere2dfa.translate(f);
 
     // language was empty, build an automaton with one non accepting state
     if (dfa == nullptr)
@@ -2245,6 +2264,38 @@ namespace spot
 
     res->set_named_prop("state-names", names);
 
+    // restore previous option
+    if (old_opt != 0)
+      sere_translation_options("expansion");
+
     return res;
   }
+
+  int sere_translation_options(const char* version)
+  {
+    static int pref = -1;
+    const char *env = nullptr;
+    if (!version && pref < 0)
+      version = env = getenv("SPOT_SERE_TRANSLATE_OPT");
+    if (version)
+      {
+        if (!strcasecmp(version, "bdd"))
+          pref = 0;
+        else if (!strcasecmp(version, "expansion"))
+          pref = 1;
+        else
+          {
+            const char* err = ("sere_translation_options(): argument"
+                              " should be one of {bdd,expansion}");
+            if (env)
+              err = "SPOT_SERE_TRANSLATE_OPT should be one of {bdd,expansion}";
+            throw std::runtime_error(err);
+          }
+      }
+    else if (pref < 0)
+      {
+        pref = 0;
+      }
+    return pref;
+  }
 }

spot/twaalgos/ltl2tgba_fm.hh

@@ -92,4 +92,6 @@ namespace spot
 
   SPOT_API twa_graph_ptr
   sere_to_tgba(formula f, const bdd_dict_ptr& dict, bool disable_scc_trimming = false);
+
+  SPOT_API int sere_translation_options(const char* version = nullptr);
 }

spot/twaalgos/translate_aa.cc

@@ -18,9 +18,14 @@
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 #include "config.h"
+
+#include <string.h>
+
 #include <spot/twaalgos/alternation.hh>
+#include <spot/twaalgos/ltl2tgba_fm.hh>
 #include <spot/twaalgos/translate_aa.hh>
 #include <spot/tl/derive.hh>
+#include <spot/tl/expansions.hh>
 #include <spot/tl/nenoform.hh>
 
 #include <iostream>
@@ -176,7 +181,6 @@ namespace spot
           {
             unsigned init_state = aut_->new_state();
 
-            outedge_combiner oe(aut_, accepting_sink_);
             bdd comb = bddtrue;
             for (const auto& sub_formula : f)
               {
@@ -285,7 +289,22 @@ namespace spot
           {
             unsigned rhs_init = recurse(f[1]);
             const auto& dict = aut_->get_dict();
-            twa_graph_ptr sere_aut = derive_finite_automaton_with_first(f[0], 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);
+              }
 
             // TODO: this should be a std::vector<bool> !
             std::vector<unsigned> acc_states;
@@ -326,7 +345,22 @@ namespace spot
           {
             unsigned rhs_init = recurse(f[1]);
             const auto& dict = aut_->get_dict();
-            twa_graph_ptr sere_aut = derive_finite_automaton_with_first(f[0], 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);
+              }
 
             // DFA recognizes the empty language, so {0} []-> rhs is always true
             unsigned ns = sere_aut->num_states();
@@ -482,4 +516,34 @@ namespace spot
 
     return aut;
   }
+
+  int sere_aa_translation_options(const char* version)
+  {
+    static int pref = -1;
+    const char *env = nullptr;
+    if (!version && pref < 0)
+      version = env = getenv("SPOT_SERE_AA_TRANSLATE_OPT");
+    if (version)
+      {
+        if (!strcasecmp(version, "bdd"))
+          pref = 0;
+        else if (!strcasecmp(version, "derive"))
+          pref = 1;
+        else if (!strcasecmp(version, "expansion"))
+          pref = 2;
+        else
+          {
+            const char* err = ("sere_aa_translation_options(): argument"
+                              " should be one of {bdd,derive,expansion}");
+            if (env)
+              err = "SPOT_SERE_AA_TRANSLATE_OPT should be one of {bdd,derive,expansion}";
+            throw std::runtime_error(err);
+          }
+      }
+    else if (pref < 0)
+      {
+        pref = 0;
+      }
+    return pref;
+  }
 }

spot/twaalgos/translate_aa.hh

@@ -29,4 +29,6 @@ namespace spot
 {
   SPOT_API twa_graph_ptr
   ltl_to_aa(formula f, bdd_dict_ptr& dict, bool purge_dead_states = false);
+
+  SPOT_API int sere_aa_translation_options(const char* version = nullptr);
 }

tests/Makefile.am

@@ -69,7 +69,6 @@ check_PROGRAMS = \
   core/cube \
   core/emptchk \
   core/equals \
-  core/expand \
   core/graph \
   core/kind \
   core/length \
@@ -112,7 +111,6 @@ core_bricks_SOURCES = core/bricks.cc
 core_checkpsl_SOURCES = core/checkpsl.cc
 core_checkta_SOURCES = core/checkta.cc
 core_emptchk_SOURCES  = core/emptchk.cc
-core_expand_SOURCES  = core/expand.cc
 core_graph_SOURCES = core/graph.cc
 core_ikwiad_SOURCES = core/ikwiad.cc
 core_intvcomp_SOURCES = core/intvcomp.cc