merge

* flake.nix, flake.lock: here

.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 $@

bin/common_post.cc

@@ -231,7 +231,14 @@ parse_opt_post(int key, char* arg, struct argp_state*)
         if (arg)
           type = XARGMATCH(key == 'P' ? "--parity" : "--colored-parity",
                            arg, parity_args, parity_types);
-        else
+        else if (!(type & spot::postprocessor::Parity))
+          // If no argument was given, we just require Parity.
+          // However, if a Parity condition was already set before,
+          // don't overwrite it.  This way if someone mistakenly write
+          // `--parity='max even' --colored` without realizing that
+          // `--colored` is just the abbreviation for
+          // `--colored-parity=...` with the default argument, we
+          // won't reset the 'max even' setting.
           type = spot::postprocessor::Parity;
         if (key == 'p')
           colored = spot::postprocessor::Colored;

bin/ltlsynt.cc

@@ -91,17 +91,15 @@ static const argp_option options[] =
     /**************************************************/
     { nullptr, 0, nullptr, 0, "Fine tuning:", 10 },
     { "algo", OPT_ALGO, "sd|ds|ps|lar|lar.old|acd", 0,
-      "choose the algorithm for synthesis:"
-      " \"sd\": translate to tgba, split, then determinize;"
-      " \"ds\": translate to tgba, determinize, then split;"
-      " \"ps\": translate to dpa, then split;"
-      " \"lar\": translate to a deterministic automaton with arbitrary"
-      " acceptance condition, then use LAR to turn to parity,"
-      " then split (default);"
-      " \"lar.old\": old version of LAR, for benchmarking;"
-      " \"acd\": translate to a deterministic automaton with arbitrary"
-      " acceptance condition, then use ACD to turn to parity,"
-      " then split.\n", 0 },
+      "choose the algorithm for synthesis:\n"
+      "  sd: translate to TGBA, split, determinize\n"
+      "  ds: translate to TGBA, determinize, split\n"
+      "  ps: translate to DPA, split\n"
+      "  lar: translate to a deterministic TELA, convert to DPA"
+      " with LAR, split (default)\n"
+      "  lar.old: old version of LAR, for benchmarking;\n"
+      "  acd: translate to a deterministic TELA, convert to DPA"
+      " with ACD, split", 0 },
     { "bypass", OPT_BYPASS, "yes|no", 0,
       "whether to try to avoid to construct a parity game "
       "(enabled by default)", 0},

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

@@ -86,7 +86,10 @@
 
 #include <spot/tl/apcollect.hh>
 #include <spot/tl/contain.hh>
+#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>
@@ -162,6 +165,7 @@
 #include <spot/twaalgos/stutter.hh>
 #include <spot/twaalgos/synthesis.hh>
 #include <spot/twaalgos/translate.hh>
+#include <spot/twaalgos/translate_aa.hh>
 #include <spot/twaalgos/toweak.hh>
 #include <spot/twaalgos/hoa.hh>
 #include <spot/twaalgos/dtwasat.hh>
@@ -544,6 +548,8 @@ namespace std {
   %template(vectorofvectorofformulas) vector<vector<spot::formula>>;
   %template(setunsigned) set<unsigned>;
   %template(relabeling_map) map<spot::formula, spot::formula>;
+  %template(pair_formula) pair<spot::formula, spot::formula>;
+  %template(vector_pair_formula) vector<pair<spot::formula, spot::formula>>;
 }
 
 %include <spot/tl/environment.hh>
@@ -631,6 +637,9 @@ namespace std {
 
 %include <spot/tl/apcollect.hh>
 %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>
@@ -788,6 +797,7 @@ def state_is_accepting(self, src) -> "bool":
 %include <spot/twaalgos/stutter.hh>
 %include <spot/twaalgos/synthesis.hh>
 %include <spot/twaalgos/translate.hh>
+%include <spot/twaalgos/translate_aa.hh>
 %include <spot/twaalgos/toweak.hh>
 %include <spot/twaalgos/hoa.hh>
 %include <spot/twaalgos/dtwasat.hh>

spot.spec.in

@@ -38,6 +38,7 @@ logic (LTL & PSL).
 %{_bindir}/ltldo
 %{_bindir}/ltlfilt
 %{_bindir}/ltlgrind
+%{_bindir}/ltlmix
 %{_bindir}/ltlsynt
 %{_bindir}/randaut
 %{_bindir}/randltl
@@ -52,11 +53,12 @@ logic (LTL & PSL).
 %{_mandir}/man1/ltldo.1*
 %{_mandir}/man1/ltlfilt.1*
 %{_mandir}/man1/ltlgrind.1*
+%{_mandir}/man1/ltlmix.1*
 %{_mandir}/man1/ltlsynt.1*
 %{_mandir}/man1/randaut.1*
 %{_mandir}/man1/randltl.1*
-%{_mandir}/man7/spot-x.7*
 %{_mandir}/man7/spot.7*
+%{_mandir}/man7/spot-x.7*
 %license COPYING
 %doc AUTHORS COPYING NEWS README THANKS
 

spot/graph/graph.hh

@@ -557,10 +557,11 @@ namespace spot
     {
       std::map<std::vector<unsigned>, unsigned> uniq_;
       G& g_;
+      unsigned acc_sink_;
     public:
 
-      univ_dest_mapper(G& graph)
-        : g_(graph)
+      univ_dest_mapper(G& graph, unsigned sink = -1u)
+        : g_(graph), acc_sink_(sink)
       {
       }
 
@@ -570,6 +571,9 @@ namespace spot
         std::vector<unsigned> tmp(begin, end);
         std::sort(tmp.begin(), tmp.end());
         tmp.erase(std::unique(tmp.begin(), tmp.end()), tmp.end());
+        if (acc_sink_ != -1u && tmp.size() > 1)
+          tmp.erase(std::remove(tmp.begin(), tmp.end(), acc_sink_),
+                    tmp.end());
         auto p = uniq_.emplace(tmp, 0);
         if (p.second)
           p.first->second = g_.new_univ_dests(tmp.begin(), tmp.end());

spot/tl/Makefile.am

@@ -28,9 +28,11 @@ tl_HEADERS =					\
   declenv.hh					\
   defaultenv.hh					\
   delta2.hh					\
+  derive.hh					\
   dot.hh					\
   environment.hh				\
   exclusive.hh					\
+  expansions2.hh					\
   formula.hh					\
   hierarchy.hh					\
   length.hh					\
@@ -54,8 +56,11 @@ libtl_la_SOURCES =				\
   declenv.cc					\
   defaultenv.cc					\
   delta2.cc					\
+  derive.cc					\
   dot.cc					\
   exclusive.cc					\
+  expansions.cc					\
+  expansions2.cc					\
   formula.cc					\
   hierarchy.cc					\
   length.cc					\

spot/tl/derive.cc

@@ -0,0 +1,589 @@
+// -*- 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 <spot/priv/robin_hood.hh>
+#include <spot/tl/derive.hh>
+#include <spot/twa/bdddict.hh>
+#include <spot/twa/formula2bdd.hh>
+#include <spot/twaalgos/remprop.hh>
+
+namespace spot
+{
+  namespace
+  {
+    static std::pair<bdd, bdd>
+    first(formula f, const bdd_dict_ptr& d, void* owner)
+    {
+      if (f.is_boolean())
+        {
+          bdd res = formula_to_bdd(f, d, owner);
+          return { res, bdd_support(res) };
+        }
+
+      switch (f.kind())
+      {
+        // handled by is_boolean above
+        case op::ff:
+        case op::tt:
+        case op::ap:
+        case op::And:
+        case op::Or:
+          SPOT_UNREACHABLE();
+
+        case op::eword:
+          return { bddfalse, bddtrue };
+
+        case op::OrRat:
+          {
+            bdd res = bddfalse;
+            bdd support = bddtrue;
+            for (auto subformula : f)
+              {
+                auto [r, sup] = first(subformula, d, owner);
+                res |= r;
+                support &= sup;
+              }
+            return { res, support };
+          }
+
+        case op::AndRat:
+          {
+            bdd res = bddtrue;
+            bdd support = bddtrue;
+            for (auto subformula : f)
+              {
+                auto [r, sup] = first(subformula, d, owner);
+                res &= r;
+                support &= sup;
+              }
+            return { res, support };
+          }
+
+        case op::AndNLM:
+          return first(rewrite_and_nlm(f), d, owner);
+
+        case op::Concat:
+          {
+            auto [res, support] = first(f[0], d, owner);
+
+            if (f[0].accepts_eword())
+              {
+                auto [r, sup] = first(f.all_but(0), d, owner);
+                res |= r;
+                support &= sup;
+              }
+
+            return { res, support };
+          }
+
+        case op::Fusion:
+          {
+            auto [res, support] = first(f[0], d, owner);
+
+            // this should be computed only if f[0] recognizes words of size 1
+            // or accepts eword ?
+            auto p = first(f.all_but(0), d, owner);
+
+            return { res, support & p.second };
+          }
+
+        case op::Star:
+        case op::first_match:
+          return first(f[0], d, owner);
+
+        case op::FStar:
+          {
+            auto [res, support] = first(f[0], d, owner);
+
+            if (f.min() == 0)
+              res = bddtrue;
+
+            return { res, support };
+          }
+
+        default:
+          std::cerr << "unimplemented kind "
+                    << static_cast<int>(f.kind())
+                    << std::endl;
+          SPOT_UNIMPLEMENTED();
+      }
+
+      return { bddfalse, bddtrue };
+    }
+
+    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));
+  }
+
+  twa_graph_ptr
+  derive_finite_automaton_with_first(formula f, bdd_dict_ptr bdd_dict,
+                                     bool deterministic, derive_opts options)
+  {
+    auto aut = make_twa_graph(bdd_dict);
+
+    aut->prop_state_acc(true);
+    const auto acc_mark = aut->set_buchi();
+
+    auto formula2state = robin_hood::unordered_map<formula, unsigned>();
+
+    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 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 derivative) -> unsigned
+      {
+        unsigned dst;
+        auto it = formula2state.find(derivative);
+        if (it != formula2state.end())
+        {
+          dst = it->second;
+        }
+        else
+        {
+          dst = aut->new_state();
+          todo.push_back({derivative, dst});
+          formula2state.insert({derivative, dst});
+          std::ostringstream ss;
+          ss << derivative;
+          state_names->push_back(ss.str());
+        }
+
+        return dst;
+      };
+
+    while (!todo.empty())
+      {
+        auto [curr_f, curr_state] = todo[todo.size() - 1];
+        todo.pop_back();
+
+        auto curr_acc_mark = curr_f.accepts_eword()
+          ? acc_mark
+          : acc_cond::mark_t();
+
+        auto [firsts, firsts_support] = first(curr_f, bdd_dict, aut.get());
+        for (const bdd one : minterms_of(firsts, firsts_support))
+          {
+            formula derivative =
+              partial_derivation(curr_f, one, bdd_dict, aut.get(), options);
+
+            // no transition possible from this letter
+            if (derivative.is(op::ff))
+              continue;
+
+            // either the formula isn't an OrRat, or if it is we consider it as
+            // as a whole to get a deterministic automaton
+            if (deterministic || !derivative.is(op::OrRat))
+              {
+                auto dst = find_dst(derivative);
+                aut->new_edge(curr_state, dst, one, curr_acc_mark);
+                continue;
+              }
+
+            // formula is an OrRat and we want a non deterministic automaton,
+            // so consider each child as a destination
+            for (const auto& subformula : derivative)
+              {
+                auto dst = find_dst(subformula);
+                aut->new_edge(curr_state, dst, one, curr_acc_mark);
+              }
+          }
+
+        // if state has no transitions and should be accepting, create
+        // artificial transition
+        if (aut->get_graph().state_storage(curr_state).succ == 0
+            && curr_f.accepts_eword())
+          aut->new_edge(curr_state, curr_state, bddfalse, acc_mark);
+      }
+
+    aut->set_named_prop("state-names", state_names);
+
+    aut->merge_edges();
+
+    return aut;
+  }
+
+  twa_graph_ptr
+  derive_finite_automaton(formula f, bool deterministic)
+  {
+    auto bdd_dict = make_bdd_dict();
+    auto aut = make_twa_graph(bdd_dict);
+
+    aut->prop_state_acc(true);
+    const auto acc_mark = aut->set_buchi();
+
+    auto formula2state = robin_hood::unordered_map<formula, unsigned>();
+
+    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);
+    bdd all_aps = aut->ap_vars();
+
+    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 derivative) -> unsigned
+      {
+        unsigned dst;
+        auto it = formula2state.find(derivative);
+        if (it != formula2state.end())
+        {
+          dst = it->second;
+        }
+        else
+        {
+          dst = aut->new_state();
+          todo.push_back({derivative, dst});
+          formula2state.insert({derivative, dst});
+          std::ostringstream ss;
+          ss << derivative;
+          state_names->push_back(ss.str());
+        }
+
+        return dst;
+      };
+
+    while (!todo.empty())
+      {
+        auto [curr_f, curr_state] = todo[todo.size() - 1];
+        todo.pop_back();
+
+        auto curr_acc_mark = curr_f.accepts_eword()
+          ? acc_mark
+          : acc_cond::mark_t();
+
+        for (const bdd one : minterms_of(bddtrue, all_aps))
+          {
+            formula derivative =
+              partial_derivation(curr_f, one, bdd_dict, aut.get());
+
+            // no transition possible from this letter
+            if (derivative.is(op::ff))
+              continue;
+
+            // either the formula isn't an OrRat, or if it is we consider it as
+            // as a whole to get a deterministic automaton
+            if (deterministic || !derivative.is(op::OrRat))
+              {
+                auto dst = find_dst(derivative);
+                aut->new_edge(curr_state, dst, one, curr_acc_mark);
+                continue;
+              }
+
+            // formula is an OrRat and we want a non deterministic automaton,
+            // so consider each child as a destination
+            for (const auto& subformula : derivative)
+              {
+                auto dst = find_dst(subformula);
+                aut->new_edge(curr_state, dst, one, curr_acc_mark);
+              }
+          }
+
+        // if state has no transitions and should be accepting, create
+        // artificial transition
+        if (aut->get_graph().state_storage(curr_state).succ == 0
+            && curr_f.accepts_eword())
+          aut->new_edge(curr_state, curr_state, bddfalse, acc_mark);
+      }
+
+    aut->set_named_prop("state-names", state_names);
+
+    aut->merge_edges();
+
+    return aut;
+  }
+
+  twa_graph_ptr
+  derive_automaton_with_first(formula f, bdd_dict_ptr bdd_dict,
+                              bool deterministic)
+  {
+    auto finite = derive_finite_automaton_with_first(f, bdd_dict,
+                                                     deterministic);
+
+    return from_finite(finite);
+  }
+
+  twa_graph_ptr
+  derive_automaton(formula f, bool deterministic)
+  {
+    auto finite = derive_finite_automaton(f, deterministic);
+
+    return from_finite(finite);
+  }
+
+  formula
+  partial_derivation(formula f, const bdd var, const bdd_dict_ptr& d,
+                     void* owner, derive_opts options)
+  {
+    if (f.is_boolean())
+      {
+        auto f_bdd = formula_to_bdd(f, d, owner);
+
+        if (bdd_implies(var, f_bdd))
+            return formula::eword();
+
+        return formula::ff();
+      }
+
+    switch (f.kind())
+      {
+        // handled by is_boolean above
+        case op::ff:
+        case op::tt:
+        case op::ap:
+          SPOT_UNREACHABLE();
+
+        case op::eword:
+          return formula::ff();
+
+        // d(E.F) = { d(E).F } U { c(E).d(F) }
+        case op::Concat:
+          {
+            formula E = f[0];
+            formula F = f.all_but(0);
+
+            formula d_E = partial_derivation(E, var, d, owner, options);
+
+            formula res;
+
+            if (options.concat_star_distribute && d_E.is(op::OrRat))
+              {
+                std::vector<formula> distributed;
+                for (auto g : d_E)
+                  {
+                    distributed.push_back(formula::Concat({g, F}));
+                  }
+
+                res = formula::OrRat(distributed);
+              }
+            else
+              {
+                res =
+                  formula::Concat({ partial_derivation(E, var, d, owner, options), F });
+              }
+
+
+            if (E.accepts_eword())
+                res = formula::OrRat(
+                        { res, partial_derivation(F, var, d, owner, options) });
+
+            return res;
+          }
+
+        // d(E*) = d(E).E*
+        // d(E[*i..j]) = d(E).E[*(i-1)..(j-1)]
+        case op::Star:
+          {
+            auto min = f.min() == 0 ? 0 : (f.min() - 1);
+            auto max = f.max() == formula::unbounded()
+                         ? formula::unbounded()
+                         : (f.max() - 1);
+
+            formula d_E = partial_derivation(f[0], var, d, owner, options);
+
+            if (options.concat_star_distribute && !f[0].is_finite() && d_E.is(op::OrRat))
+              {
+                std::vector<formula> distributed;
+                for (auto g : d_E)
+                  {
+                    distributed.push_back(formula::Concat({g, formula::Star(f[0], min, max)}));
+                  }
+
+                return formula::OrRat(distributed);
+              }
+
+            return formula::Concat({ d_E, formula::Star(f[0], min, max) });
+          }
+
+        // d(E[:*i..j]) = E:E[:*(i-1)..(j-1)] + (eword if i == 0 or c(d(E)))
+        case op::FStar:
+          {
+            formula E = f[0];
+
+            if (f.min() == 0 && f.max() == 0)
+              return formula::tt();
+
+            auto d_E = partial_derivation(E, var, d, owner, options);
+
+            auto min = f.min() == 0 ? 0 : (f.min() - 1);
+            auto max = f.max() == formula::unbounded()
+                         ? formula::unbounded()
+                         : (f.max() - 1);
+
+            auto results = std::vector<formula>();
+
+            auto E_i_j_minus = formula::FStar(E, min, max);
+            results.push_back(formula::Fusion({ d_E, E_i_j_minus }));
+
+            if (d_E.accepts_eword())
+              results.push_back(d_E);
+
+            if (f.min() == 0)
+              results.push_back(formula::eword());
+
+            return formula::OrRat(std::move(results));
+          }
+
+        // d(E && F) = d(E) && d(F)
+        // d(E + F) = {d(E)} U {d(F)}
+        case op::AndRat:
+        case op::OrRat:
+          {
+            std::vector<formula> subderivations;
+            for (auto subformula : f)
+              {
+                auto subderivation =
+                  partial_derivation(subformula, var, d, owner, options);
+                subderivations.push_back(subderivation);
+              }
+            return formula::multop(f.kind(), std::move(subderivations));
+          }
+
+        case op::AndNLM:
+          {
+            formula rewrite = rewrite_and_nlm(f);
+            return partial_derivation(rewrite, var, d, owner, options);
+          }
+
+        // d(E:F) = {d(E):F} U {c(d(E)).d(F)}
+        case op::Fusion:
+          {
+            formula E = f[0];
+            formula F = f.all_but(0);
+
+            auto d_E = partial_derivation(E, var, d, owner, options);
+            auto res = formula::Fusion({ d_E, F });
+
+            if (d_E.accepts_eword())
+              res =
+                formula::OrRat({ res, partial_derivation(F, var, d, owner, options) });
+
+            return res;
+          }
+
+        case op::first_match:
+          {
+            formula E = f[0];
+            auto d_E = partial_derivation(E, var, d, owner, options);
+            // if d_E.accepts_eword(), first_match(d_E) will return eword
+            return formula::first_match(d_E);
+          }
+
+        default:
+          std::cerr << "unimplemented kind "
+                    << static_cast<int>(f.kind())
+                    << std::endl;
+          SPOT_UNIMPLEMENTED();
+      }
+    return formula::ff();
+  }
+}

spot/tl/derive.hh

@@ -0,0 +1,60 @@
+// -*- 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 <vector>
+
+#include <bddx.h>
+
+#include <spot/tl/formula.hh>
+#include <spot/twa/bdddict.hh>
+#include <spot/twa/twagraph.hh>
+
+namespace spot
+{
+
+  struct derive_opts
+  {
+    bool concat_star_distribute = true;
+  };
+
+  /// \ingroup tl_misc
+  /// \brief Produce a SERE formula's partial derivative
+  SPOT_API formula
+  partial_derivation(formula f, const bdd var, const bdd_dict_ptr& d,
+                     void* owner, derive_opts options = {});
+
+  SPOT_API twa_graph_ptr
+  derive_automaton(formula f, bool deterministic = true);
+
+  SPOT_API twa_graph_ptr
+  derive_automaton_with_first(formula f, bdd_dict_ptr bdd_dict,
+                              bool deterministic = true);
+
+  SPOT_API twa_graph_ptr
+  derive_finite_automaton(formula f, bool deterministic = true);
+
+  SPOT_API twa_graph_ptr
+  derive_finite_automaton_with_first(formula f, bdd_dict_ptr bdd_dict,
+                                     bool deterministic = true, derive_opts options = {});
+
+  SPOT_API formula
+  rewrite_and_nlm(formula f);
+}

spot/tl/expansions.cc

@@ -0,0 +1,966 @@
+// -*- 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/expansions.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 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());
+        }
+    }
+  }
+
+  formula
+  expansion_to_formula(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);
+  }
+
+  void print_expansion(const expansion_t& exp, const bdd_dict_ptr& dict)
+  {
+    for (const auto& [prefix, suffix] : exp)
+      {
+        std::cout << bdd_to_formula(prefix, dict) << ": " << suffix << std::endl;
+      }
+  }
+
+  std::vector<std::pair<formula, formula>>
+  expansion_simple(formula f)
+  {
+    int owner = 42;
+    auto d = make_bdd_dict();
+
+    auto exp = expansion(f, d, &owner, exp_opts::None);
+
+    std::vector<std::pair<formula, formula>> res;
+    for (const auto& [bdd, f] : exp)
+      res.push_back({bdd_to_formula(bdd, d), f});
+
+    d->unregister_all_my_variables(&owner);
+    return res;
+  }
+
+  expansion_t
+  expansion(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, seen](formula f){
+      return expansion(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});
+                  }
+
+                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);
+            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_automaton(formula f, bdd_dict_ptr d, exp_opts::expand_opt opts)
+  {
+    auto finite = expand_finite_automaton(f, d, opts);
+    return from_finite(finite);
+  }
+
+  struct signature_hash
+  {
+    std::size_t
+    operator() (const std::pair<bool, expansion_t>& sig) const noexcept
+    {
+      size_t hash = std::hash<bool>()(sig.first);
+
+      for (const auto& keyvalue : sig.second)
+        {
+          hash ^= (bdd_hash()(keyvalue.first) ^ std::hash<formula>()(keyvalue.second))
+            + 0x9e3779b9 + (hash << 6) + (hash >> 2);
+        }
+
+      return hash;
+    }
+  };
+
+  twa_graph_ptr
+  expand_finite_automaton(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(true);
+    const auto acc_mark = aut->set_buchi();
+
+    auto formula2state = robin_hood::unordered_map<formula, unsigned>();
+    auto signature2state = std::unordered_map<std::pair<bool, 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);
+
+    if (signature_merge)
+      signature2state.insert({ {f.accepts_eword(), expansion(f, d, aut.get(), opts, &seen)}, 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 = expansion(suffix, d, aut.get(), opts, &seen);
+              bool accepting = suffix.accepts_eword();
+              auto it2 = signature2state.find({accepting, 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({{suffix.accepts_eword(), expansion(suffix, d, aut.get(), opts, &seen)}, 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 curr_acc_mark= curr_f.accepts_eword()
+          ? acc_mark
+          : acc_cond::mark_t();
+
+        auto exp = expansion(curr_f, d, aut.get(), opts, &seen);
+
+        for (const auto& [letter, suffix] : exp)
+          {
+            if (suffix.is(op::ff))
+              // TODO ASSERT NOT
+              continue;
+
+            auto dst = find_dst(suffix);
+            aut->new_edge(curr_state, dst, letter, curr_acc_mark);
+          }
+
+        // if state has no transitions and should be accepting, create
+        // artificial transition
+        if (aut->get_graph().state_storage(curr_state).succ == 0
+            && curr_f.accepts_eword())
+          aut->new_edge(curr_state, curr_state, bddfalse, 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/expansions.hh

@@ -0,0 +1,72 @@
+// -*- 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/formula.hh>
+#include <spot/twa/bdddict.hh>
+#include <spot/twa/twagraph.hh>
+
+namespace spot
+{
+  using expansion_t = std::vector<std::pair<bdd, formula>>;
+
+  struct exp_opts
+  {
+    enum expand_opt {
+      None = 0,
+      UniqueSuffixPre = 1,
+      UniquePrefix = 2,
+      BddIsop = 4,
+      BddMinterm = 8,
+      BddSigmaStar = 16,
+      BddEncode = 32,
+      MergeEdges = 64,
+      SignatureMerge = 128,
+      Determinize = 256,
+      UniquePrefixSeenOpt = 512,
+      UniqueSuffixPost = 1024,
+      UniquePrefixSeenCountOpt = 2048,
+      TransitionBased = 4096,
+    };
+  };
+
+  SPOT_API std::vector<std::pair<formula, formula>>
+  expansion_simple(formula f);
+
+  SPOT_API expansion_t
+  expansion(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_automaton(formula f, bdd_dict_ptr d, exp_opts::expand_opt opts);
+
+  SPOT_API twa_graph_ptr
+  expand_finite_automaton(formula f, bdd_dict_ptr d, exp_opts::expand_opt opts);
+
+  SPOT_API formula
+  expansion_to_formula(expansion_t e, bdd_dict_ptr& d);
+
+  SPOT_API void
+  print_expansion(const expansion_t& exp, const bdd_dict_ptr& dict);
+}

spot/tl/expansions2.cc

@@ -0,0 +1,946 @@
+// -*- 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, 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});
+                  }
+
+                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);
+            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/twa/twagraph.cc

@@ -230,11 +230,15 @@ namespace spot
         // them.
       });
 
+      bool is_state_acc = this->prop_state_acc().is_true();
+
       unsigned out = 0;
       unsigned in = 1;
 
       // Skip any leading false edge.
-      while (in < tend && trans[in].cond == bddfalse)
+      while (in < tend
+             && trans[in].cond == bddfalse
+             && (!is_state_acc || trans[in].src != trans[in].dst))
         ++in;
       if (in < tend)
         {
@@ -243,7 +247,9 @@ namespace spot
             trans[out] = trans[in];
           for (++in; in < tend; ++in)
             {
-              if (trans[in].cond == bddfalse) // Unusable edge
+              if (trans[in].cond == bddfalse
+                  && (!is_state_acc
+                      || trans[in].src != trans[in].dst)) // Unusable edge
                 continue;
               // Merge edges with the same source, destination, and
               // colors.  (We test the source last, because this is the

spot/twaalgos/Makefile.am

@@ -99,6 +99,7 @@ twaalgos_HEADERS = \
   totgba.hh \
   toweak.hh \
   translate.hh \
+  translate_aa.hh \
   word.hh \
   zlktree.hh
 
@@ -177,6 +178,7 @@ libtwaalgos_la_SOURCES = \
   totgba.cc \
   toweak.cc \
   translate.cc \
+  translate_aa.cc \
   word.cc \
   zlktree.cc
 

spot/twaalgos/alternation.cc

@@ -28,8 +28,8 @@
 
 namespace spot
 {
-  outedge_combiner::outedge_combiner(const twa_graph_ptr& aut)
-    : aut_(aut), vars_(bddtrue)
+  outedge_combiner::outedge_combiner(const twa_graph_ptr& aut, unsigned sink)
+    : aut_(aut), vars_(bddtrue), acc_sink_(sink)
   {
   }
 
@@ -38,7 +38,8 @@ namespace spot
     aut_->get_dict()->unregister_all_my_variables(this);
   }
 
-  bdd outedge_combiner::operator()(unsigned st)
+  bdd outedge_combiner::operator()(unsigned st, const std::vector<unsigned>& dst_filter,
+                                   bool remove_original_edges)
   {
     const auto& dict = aut_->get_dict();
     bdd res = bddtrue;
@@ -47,9 +48,27 @@ namespace spot
         bdd res2 = bddfalse;
         for (auto& e: aut_->out(d1))
           {
+            // handle edge filtering
+            if (!dst_filter.empty())
+              {
+                // if any edge destination is an accepting state in the SERE
+                // automaton, handle the edge, otherwise skip it
+                auto univ_dests = aut_->univ_dests(e.dst);
+                if (std::all_of(univ_dests.begin(), univ_dests.end(),
+                                [&](unsigned dst)
+                                {
+                                  return std::find(dst_filter.begin(), dst_filter.end(), dst)
+                                    == dst_filter.end();
+                                }))
+                  continue;
+              }
+
             bdd out = bddtrue;
             for (unsigned d: aut_->univ_dests(e.dst))
               {
+                if (d == acc_sink_)
+                  continue;
+
                 auto p = state_to_var.emplace(d, 0);
                 if (p.second)
                   {
@@ -61,7 +80,11 @@ namespace spot
                 out &= bdd_ithvar(p.first->second);
               }
             res2 |= e.cond & out;
+
+            if (remove_original_edges)
+              e.cond = bddfalse;
           }
+
         res &= res2;
       }
     return res;
@@ -78,7 +101,17 @@ namespace spot
       {
         bdd cond = bdd_exist(cube, vars_);
         bdd dest = bdd_existcomp(cube, vars_);
-        while (dest != bddtrue)
+
+        if (dest == bddtrue)
+          {
+            // if dest is bddtrue then the accepting sink is the only
+            // destination for this edge, in that case don't filter it out
+            assert(acc_sink_ != -1u);
+            aut_->new_edge(st, acc_sink_, cond);
+            continue;
+          }
+
+        do
           {
             assert(bdd_low(dest) == bddfalse);
             auto it = var_to_state.find(bdd_var(dest));
@@ -86,6 +119,8 @@ namespace spot
             univ_dest.push_back(it->second);
             dest = bdd_high(dest);
           }
+        while  (dest != bddtrue);
+
         std::sort(univ_dest.begin(), univ_dest.end());
         aut_->new_univ_edge(st, univ_dest.begin(), univ_dest.end(), cond);
         univ_dest.clear();

spot/twaalgos/alternation.hh

@@ -49,10 +49,12 @@ namespace spot
     std::map<unsigned, int> state_to_var;
     std::map<int, unsigned> var_to_state;
     bdd vars_;
+    unsigned acc_sink_;
   public:
-    outedge_combiner(const twa_graph_ptr& aut);
+    outedge_combiner(const twa_graph_ptr& aut, unsigned sink = -1u);
     ~outedge_combiner();
-    bdd operator()(unsigned st);
+    bdd operator()(unsigned st, const std::vector<unsigned>& dst_filter = std::vector<unsigned>(),
+                   bool remove_original_edges = false);
     void new_dests(unsigned st, bdd out) const;
   };
 

spot/twaalgos/ltl2tgba_fm.cc

@@ -19,9 +19,12 @@
 #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>
+#include <spot/tl/nenoform.hh>
+#include <spot/tl/expansions.hh>
 #include <cassert>
 #include <memory>
 #include <utility>
@@ -99,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);
+      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:
@@ -115,6 +117,7 @@ namespace spot
       typedef robin_hood::unordered_node_map<formula, labelled_aut> f2a_t;
       std::vector<labelled_aut> automata_;
       f2a_t f2a_;
+      bool disable_scc_trimming_;
     };
 
     // Helper dictionary.  We represent formulae using BDDs to
@@ -221,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;
@@ -747,55 +751,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:
             {
@@ -932,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
         {
@@ -948,8 +918,9 @@ namespace spot
     }
 
 
-    ratexp_to_dfa::ratexp_to_dfa(translate_dict& dict)
+    ratexp_to_dfa::ratexp_to_dfa(translate_dict& dict, bool disable_scc_trimming)
       : dict_(dict)
+      , disable_scc_trimming_(disable_scc_trimming)
     {
     }
 
@@ -1002,6 +973,12 @@ namespace spot
             }
         }
 
+      if (disable_scc_trimming_)
+        {
+          automata_.emplace_back(a, namer);
+          return labelled_aut(a, namer);
+        }
+
       // The following code trims the automaton in a crude way by
       // eliminating SCCs that are not coaccessible.  It does not
       // actually remove the states, it simply marks the corresponding
@@ -2226,4 +2203,99 @@ namespace spot
     return a;
   }
 
+  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);
+    twa_graph_ptr a = make_twa_graph(dict);
+
+    translate_dict d(a, s, false, false, false);
+    ratexp_to_dfa sere2dfa(d, disable_scc_trimming);
+
+    auto [dfa, namer] = sere2dfa.translate(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();
+    auto names = new std::vector<std::string>(sn);
+    for (size_t i = 0; i < sn; ++i)
+      {
+        formula g = namer->state_to_name[i];
+        (*names)[i] = str_psl(g);
+        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;
+              }
+          }
+      }
+
+    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

@@ -89,4 +89,9 @@ 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, bool disable_scc_trimming = false);
+
+  SPOT_API int sere_translation_options(const char* version = nullptr);
 }

spot/twaalgos/remprop.cc

@@ -245,4 +245,51 @@ namespace spot
 
   }
 
+  twa_graph_ptr from_finite(const_twa_graph_ptr aut, const char* alive)
+  {
+    twa_graph_ptr res =
+      make_twa_graph(aut,
+                     { true, false, true, false, false, false });
+
+    if (aut->get_named_prop<std::vector<std::string>>("state-names"))
+      res->copy_state_names_from(aut);
+    auto* names = res->get_named_prop<std::vector<std::string>>("state-names");
+
+    unsigned alive_sink = res->new_state();
+    if (names != nullptr)
+      names->push_back("sink");
+    auto acc = res->acc().all_sets();
+    auto alive_bdd = bdd_ithvar(res->register_ap(alive));
+    res->new_edge(alive_sink, alive_sink, !alive_bdd, acc);
+
+    unsigned ns = res->num_states();
+    for (unsigned s = 0; s < ns; ++s)
+      {
+        if (s == alive_sink)
+          continue;
+
+        bool was_acc = res->state_is_accepting(s);
+
+        // erase accepting marks, require alive on non-accepting transition,
+        // and remove self-loop edges used to mark acceptance
+        auto i = res->out_iteraser(s);
+        while (i)
+          {
+            if (i->src == i->dst && i->cond == bddfalse)
+              {
+                i.erase();
+                continue;
+              }
+
+            i->cond &= alive_bdd;
+            i->acc = {};
+            ++i;
+          }
+
+        if (was_acc)
+          res->new_edge(s, alive_sink, !alive_bdd);
+      }
+
+    return res;
+  }
 }

spot/twaalgos/remprop.hh

@@ -53,5 +53,8 @@ namespace spot
   SPOT_API twa_graph_ptr
   to_finite(const_twa_graph_ptr aut, const char* alive = "alive");
 
+  /// \brief The opposite of the to_finite operation
+  SPOT_API twa_graph_ptr
+  from_finite(const_twa_graph_ptr aut, const char* alive = "alive");
 
 }

spot/twaalgos/translate_aa.cc

@@ -0,0 +1,549 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2013-2018, 2020-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 <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>
+
+namespace spot
+{
+  namespace
+  {
+    struct ltl_to_aa_builder
+    {
+      ltl_to_aa_builder(twa_graph_ptr aut, unsigned accepting_sink)
+        : aut_(aut)
+        , accepting_sink_(accepting_sink)
+        , uniq_(aut_->get_graph(), accepting_sink)
+        , oe_(aut_, accepting_sink)
+      {
+      }
+
+      ~ltl_to_aa_builder()
+      {
+        aut_->get_dict()->unregister_all_my_variables(this);
+      }
+
+      twa_graph_ptr aut_;
+      unsigned accepting_sink_;
+      internal::univ_dest_mapper<twa_graph::graph_t> uniq_;
+      outedge_combiner oe_;
+
+      void add_self_loop(twa_graph::edge_storage_t const& e,
+                         unsigned init_state,
+                         acc_cond::mark_t acc)
+      {
+        if (e.dst == accepting_sink_)
+          {
+            // avoid creating a univ_dests vector if the only dest is an
+            // accepting sink, which can be simplified, only keeping the self
+            // loop
+            aut_->new_edge(init_state, init_state, e.cond, acc);
+            return;
+          }
+
+        auto dests = aut_->univ_dests(e);
+        std::vector<unsigned> new_dests(dests.begin(), dests.end());
+        new_dests.push_back(init_state);
+
+        unsigned dst = uniq_.new_univ_dests(new_dests.begin(),
+                                            new_dests.end());
+        aut_->new_edge(init_state, dst, e.cond, acc);
+      }
+
+      unsigned copy_sere_aut_to_res(twa_graph_ptr sere_aut,
+                                    std::map<unsigned, unsigned>& old_to_new,
+                                    std::vector<unsigned>* acc_states = nullptr,
+                                    bool use_accepting_sink = true)
+      {
+        unsigned ns = sere_aut->num_states();
+
+        // TODO: create all new states at once, keeping an initial offset (the
+        //       number of states already present in aut_)
+        aut_->copy_ap_of(sere_aut);
+        auto register_state = [&](unsigned st) -> unsigned {
+          auto p = old_to_new.emplace(st, 0);
+          if (p.second)
+          {
+            unsigned new_st = aut_->new_state();
+            p.first->second = new_st;
+            if (acc_states != nullptr && sere_aut->state_is_accepting(st))
+              acc_states->push_back(new_st);
+          }
+          return p.first->second;
+        };
+
+        for (unsigned st = 0; st < ns; ++st)
+          {
+            unsigned new_st = register_state(st);
+            for (const auto& e : sere_aut->out(st))
+              {
+                if (use_accepting_sink && sere_aut->state_is_accepting(e.dst))
+                  aut_->new_edge(new_st, accepting_sink_, e.cond);
+                else
+                  aut_->new_edge(new_st, register_state(e.dst), e.cond);
+              }
+          }
+
+        auto it = old_to_new.find(sere_aut->get_init_state_number());
+        assert(it != old_to_new.end());
+        return it->second;
+      }
+
+
+      unsigned recurse(formula f)
+      {
+        switch (f.kind())
+        {
+          case op::ff:
+            return aut_->new_state();
+
+          case op::tt:
+          {
+            unsigned init_state = aut_->new_state();
+            aut_->new_edge(init_state, accepting_sink_, bddtrue, {});
+            return init_state;
+          }
+
+          case op::ap:
+          case op::Not:
+          {
+            unsigned init_state = aut_->new_state();
+
+            bdd ap;
+            if (f.kind() == op::ap)
+              ap = bdd_ithvar(aut_->register_ap(f.ap_name()));
+            else
+              ap = bdd_nithvar(aut_->register_ap(f[0].ap_name()));
+
+            aut_->new_edge(init_state, accepting_sink_, ap, {});
+            return init_state;
+          }
+
+          // FIXME: is this right for LTLf?
+          case op::strong_X:
+          case op::X:
+          {
+            unsigned sub_init_state = recurse(f[0]);
+            unsigned new_init_state = aut_->new_state();
+            aut_->new_edge(new_init_state, sub_init_state, bddtrue, {});
+            return new_init_state;
+          }
+
+          case op::Or:
+          {
+            unsigned init_state = aut_->new_state();
+
+            for (const auto& sub_formula : f)
+              {
+                unsigned sub_init = recurse(sub_formula);
+                for (auto& e : aut_->out(sub_init))
+                  {
+                    unsigned dst = e.dst;
+                    if (aut_->is_univ_dest(e.dst))
+                      {
+                        auto dests = aut_->univ_dests(e);
+                        dst = uniq_.new_univ_dests(dests.begin(), dests.end());
+                      }
+                    aut_->new_edge(init_state, dst, e.cond, {});
+                  }
+              }
+
+            return init_state;
+          }
+
+          case op::And:
+          {
+            unsigned init_state = aut_->new_state();
+
+            bdd comb = bddtrue;
+            for (const auto& sub_formula : f)
+              {
+                unsigned sub_init = recurse(sub_formula);
+                comb &= oe_(sub_init);
+              }
+            oe_.new_dests(init_state, comb);
+
+            return init_state;
+          }
+
+          case op::U:
+          case op::W:
+          {
+            auto acc = f.kind() == op::U
+              ? acc_cond::mark_t{0}
+              : acc_cond::mark_t{};
+
+            unsigned init_state = aut_->new_state();
+
+            unsigned lhs_init = recurse(f[0]);
+            unsigned rhs_init = recurse(f[1]);
+
+            std::vector<unsigned> new_dests;
+            for (auto& e : aut_->out(lhs_init))
+              add_self_loop(e, init_state, acc);
+
+            for (auto& e : aut_->out(rhs_init))
+              {
+                unsigned dst = e.dst;
+                if (aut_->is_univ_dest(e.dst))
+                  {
+                    auto dests = aut_->univ_dests(e);
+                    dst = uniq_.new_univ_dests(dests.begin(), dests.end());
+                  }
+                aut_->new_edge(init_state, dst, e.cond, {});
+              }
+
+            return init_state;
+          }
+
+          case op::R:
+          case op::M:
+          {
+            auto acc = f.kind() == op::M
+              ? acc_cond::mark_t{0}
+              : acc_cond::mark_t{};
+
+            unsigned init_state = aut_->new_state();
+
+            unsigned lhs_init = recurse(f[0]);
+            unsigned rhs_init = recurse(f[1]);
+
+            for (auto& e : aut_->out(rhs_init))
+              add_self_loop(e, init_state, acc);
+
+            bdd comb = oe_(lhs_init);
+            comb &= oe_(rhs_init);
+            oe_.new_dests(init_state, comb);
+
+            return init_state;
+          }
+
+          // F(phi) = tt U phi
+          case op::F:
+          {
+            auto acc = acc_cond::mark_t{0};
+
+            // if phi is boolean then we can reuse its initial state (otherwise
+            // we can't because of potential self loops)
+            if (f[0].is_boolean())
+              {
+                unsigned init_state = recurse(f[0]);
+                aut_->new_edge(init_state, init_state, bddtrue, acc);
+                return init_state;
+              }
+
+            unsigned init_state = aut_->new_state();
+            unsigned sub_init = recurse(f[0]);
+
+            aut_->new_edge(init_state, init_state, bddtrue, acc);
+
+            for (auto& e : aut_->out(sub_init))
+              aut_->new_edge(init_state, e.dst, e.cond, {});
+
+            return init_state;
+          }
+
+          // G phi = ff R phi
+          case op::G:
+          {
+            unsigned init_state = aut_->new_state();
+
+            unsigned sub_init = recurse(f[0]);
+
+            // translate like R, but only the self loop part; `ff` cancels out
+            // the product of edges
+            std::vector<unsigned> new_dests;
+            for (auto& e : aut_->out(sub_init))
+              add_self_loop(e, init_state, {});
+
+            return init_state;
+          }
+
+          case op::EConcat:
+          {
+            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);
+              }
+
+            // TODO: this should be a std::vector<bool> !
+            std::vector<unsigned> acc_states;
+            std::map<unsigned, unsigned> old_to_new;
+            copy_sere_aut_to_res(sere_aut, old_to_new, &acc_states, false);
+
+            std::vector<unsigned> acc_edges;
+            unsigned ns = sere_aut->num_states();
+            for (unsigned st = 0; st < ns; ++st)
+              {
+                auto it = old_to_new.find(st);
+                assert(it != old_to_new.end());
+                unsigned new_st = it->second;
+
+                for (auto& e : aut_->out(new_st))
+                  {
+                    e.acc = acc_cond::mark_t{0};
+                    if (std::find(acc_states.begin(), acc_states.end(), e.dst)
+                        != acc_states.end())
+                      acc_edges.push_back(aut_->edge_number(e));
+                  }
+              }
+
+            for (unsigned i : acc_edges)
+              {
+                auto& e1 = aut_->edge_storage(i);
+                for (const auto& e2 : aut_->out(rhs_init))
+                  aut_->new_edge(e1.src, e2.dst, e1.cond & e2.cond);
+              }
+
+            auto it = old_to_new.find(sere_aut->get_init_state_number());
+            assert(it != old_to_new.end());
+
+            return it->second;
+          }
+
+          case op::UConcat:
+          {
+            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);
+              }
+
+            // DFA recognizes the empty language, so {0} []-> rhs is always true
+            unsigned ns = sere_aut->num_states();
+            bool has_accepting_state = false;
+            for (unsigned st = 0; st < ns && !has_accepting_state; ++st)
+              has_accepting_state = sere_aut->state_is_accepting(st);
+            if (!has_accepting_state)
+              return accepting_sink_;
+
+            std::map<unsigned, unsigned> old_to_new;
+            std::map<unsigned, int> state_to_var;
+            std::map<int, unsigned> var_to_state;
+            bdd vars = bddtrue;
+            bdd aps = sere_aut->ap_vars();
+            std::vector<unsigned> univ_dest;
+            // TODO: this should be a std::vector<bool> !
+            std::vector<unsigned> acc_states;
+
+            // registers a state in various maps and returns the index of the
+            // anonymous bdd var representing that state
+            auto register_state = [&](unsigned st) -> int {
+              auto p = state_to_var.emplace(st, 0);
+              if (p.second)
+              {
+                int v = dict->register_anonymous_variables(1, this);
+                p.first->second = v;
+
+                unsigned new_st = aut_->new_state();
+                old_to_new.emplace(st, new_st);
+                var_to_state.emplace(v, new_st);
+
+                if (sere_aut->state_is_accepting(st))
+                  acc_states.push_back(new_st);
+
+                vars &= bdd_ithvar(v);
+              }
+
+              return p.first->second;
+            };
+
+            aut_->copy_ap_of(sere_aut);
+            for (unsigned st = 0; st < ns; ++st)
+              {
+                register_state(st);
+
+                bdd sig = bddfalse;
+                for (const auto& e : sere_aut->out(st))
+                  {
+                    int st_bddi = register_state(e.dst);
+                    sig |= e.cond & bdd_ithvar(st_bddi);
+                  }
+
+                for (bdd cond : minterms_of(bddtrue, aps))
+                  {
+                    bdd dest = bdd_appex(sig, cond, bddop_and, aps);
+                    while (dest != bddfalse)
+                      {
+                        assert(bdd_high(dest) == bddtrue);
+                        auto it = var_to_state.find(bdd_var(dest));
+                        assert(it != var_to_state.end());
+                        univ_dest.push_back(it->second);
+                        dest = bdd_low(dest);
+                      }
+
+                    auto it = old_to_new.find(st);
+                    assert(it != old_to_new.end());
+                    unsigned src = it->second;
+
+                    unsigned dst = univ_dest.empty()
+                      ? accepting_sink_
+                      : (uniq_.new_univ_dests(univ_dest.begin(),
+                                              univ_dest.end()));
+
+                    aut_->new_edge(src, dst, cond, {});
+                    univ_dest.clear();
+                  }
+              }
+
+            for (unsigned st = 0; st < ns; ++st)
+              {
+                auto it = old_to_new.find(st);
+                assert(it != old_to_new.end());
+                unsigned new_st = it->second;
+
+                bdd comb = bddtrue;
+                comb &= oe_(new_st, acc_states, true);
+                if (comb != bddtrue)
+                  {
+                    comb &= oe_(rhs_init);
+                    oe_.new_dests(new_st, comb);
+                  }
+              }
+
+            auto it = old_to_new.find(sere_aut->get_init_state_number());
+            assert(it != old_to_new.end());
+
+            aut_->merge_edges();
+            return it->second;
+          }
+
+          case op::Closure:
+          {
+            twa_graph_ptr sere_aut =
+              derive_finite_automaton_with_first(f[0], aut_->get_dict());
+            std::map<unsigned, unsigned> old_to_new;
+            return copy_sere_aut_to_res(sere_aut, old_to_new);
+          }
+
+          case op::NegClosure:
+          case op::NegClosureMarked:
+          case op::eword:
+          case op::Xor:
+          case op::Implies:
+          case op::Equiv:
+          case op::EConcatMarked:
+          case op::OrRat:
+          case op::AndRat:
+          case op::AndNLM:
+          case op::Concat:
+          case op::Fusion:
+          case op::Star:
+          case op::FStar:
+          case op::first_match:
+            SPOT_UNREACHABLE();
+            return -1;
+        }
+
+        SPOT_UNREACHABLE();
+      }
+    };
+  }
+
+  twa_graph_ptr
+  ltl_to_aa(formula f, bdd_dict_ptr& dict, bool purge_dead_states)
+  {
+    f = negative_normal_form(f);
+
+    auto aut = make_twa_graph(dict);
+    aut->set_co_buchi();
+
+    unsigned accepting_sink = aut->new_state();
+    aut->new_edge(accepting_sink, accepting_sink, bddtrue, {});
+    auto builder = ltl_to_aa_builder(aut, accepting_sink);
+
+    unsigned init_state = builder.recurse(f);
+    aut->set_init_state(init_state);
+
+    if (purge_dead_states)
+      {
+        aut->purge_dead_states();
+        aut->merge_edges();
+      }
+
+    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

@@ -0,0 +1,34 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2010-2015, 2017, 2019-2020 Laboratoire de
+// Recherche et Développement de l'Epita (LRDE).
+// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
+// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
+// Université Pierre et Marie Curie.
+//
+// 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 <spot/tl/formula.hh>
+#include <spot/twa/twagraph.hh>
+
+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

@@ -76,6 +76,7 @@ check_PROGRAMS = \
   core/intvcomp \
   core/intvcmp2 \
   core/kripkecat \
+  core/ltl2aa \
   core/ltl2dot \
   core/ltl2text \
   core/ltlrel \
@@ -125,6 +126,7 @@ core_cube_SOURCES = core/cube.cc
 core_equals_SOURCES = core/equalsf.cc
 core_kind_SOURCES = core/kind.cc
 core_length_SOURCES = core/length.cc
+core_ltl2aa_SOURCES = core/ltl2aa.cc
 core_ltl2dot_SOURCES = core/readltl.cc
 core_ltl2dot_CPPFLAGS = $(AM_CPPFLAGS) -DDOTTY
 core_ltl2text_SOURCES = core/readltl.cc

tests/core/.gitignore

@@ -33,6 +33,7 @@ kripkecat
 length
 .libs
 ikwiad
+ltl2aa
 ltl2dot
 ltl2text
 ltlmagic

tests/core/expand.cc

@@ -0,0 +1,25 @@
+#include "config.h"
+
+#include <spot/tl/expansions.hh>
+#include <spot/tl/parse.hh>
+#include <spot/twa/formula2bdd.hh>
+#include <iostream>
+
+int main(int argc, char** argv)
+{
+  if (argc != 2)
+    return 1;
+
+  spot::formula f = spot::parse_infix_sere(argv[1]).f;
+  auto d = spot::make_bdd_dict();
+
+  auto m = spot::expansion(f, d, nullptr);
+
+  for (const auto& [bdd_l, form] : m)
+    std::cout << '[' << bdd_to_formula(bdd_l, d) << ']' << ": " << form << std::endl;
+  std::cout << "formula: " << expansion_to_formula(m, d) << std::endl;
+
+  d->unregister_all_my_variables(nullptr);
+
+  return 0;
+}

tests/core/ltl2aa.cc

@@ -0,0 +1,22 @@
+#include "config.h"
+
+#include <fstream>
+
+#include <spot/tl/formula.hh>
+#include <spot/tl/parse.hh>
+#include <spot/twaalgos/hoa.hh>
+#include <spot/twaalgos/translate_aa.hh>
+
+int main(int argc, char * argv[])
+{
+  if (argc < 3)
+    return 1;
+
+  spot::formula f = spot::parse_formula(argv[1]);
+  spot::bdd_dict_ptr d = spot::make_bdd_dict();
+  auto aut = ltl_to_aa(f, d, true);
+
+  std::ofstream out(argv[2]);
+  spot::print_hoa(out, aut);
+  return 0;
+}

tests/core/parity2.test

@@ -26,7 +26,19 @@ for x in P 'Pmin odd' 'Pmax even' p 'pmin odd' 'pmax even'; do
     autfilt --name=%M --high "-$x" >>res2
   ltl2tgba -D "-$x" FGa 'GFa & GFb' '(p0 W XXGp0) & GFp1 & FGp2' >>res3
   ltl2tgba FGa 'GFa & GFb' '(p0 W XXGp0) & GFp1 & FGp2' |
-    autfilt -D --name=%M --high "-$x" >>res4
+      autfilt -D --name=%M --high "-$x" >>res4
+  (
+      ## --colored is normally short for --colored-parity=any
+      ## But in case someone types something like
+      ##   --parity='max odd' --colored
+      ## let's make sure we handle it like --colored-parity='max odd'.
+      echo "=== -$x ==="
+      ltl2tgba FGa 'GFa & GFb' '(p0 W XXGp0) & GFp1 & FGp2' \
+               "-$x" --stats='%[]g'
+      echo "=== -$x --colored ==="
+      ltl2tgba FGa 'GFa & GFb' '(p0 W XXGp0) & GFp1 & FGp2' \
+               "-$x" --colored --stats='%[]g'
+  ) >> res5
 done
 
 cat >expected<<EOF
@@ -1423,6 +1435,58 @@ State: 4
 EOF
 diff expected4 res4
 
+cat >expected5 <<EOF
+=== -P ===
+co-Buchi
+Buchi
+Rabin 1
+=== -P --colored ===
+parity max even 2
+Streett 1
+parity min odd 3
+=== -Pmin odd ===
+co-Buchi
+Rabin 1
+Rabin 1
+=== -Pmin odd --colored ===
+Rabin 1
+parity min odd 3
+parity min odd 3
+=== -Pmax even ===
+parity max even 2
+Buchi
+parity max even 2
+=== -Pmax even --colored ===
+parity max even 2
+parity max even 3
+parity max even 4
+=== -p ===
+parity max even 2
+Streett 1
+parity min odd 3
+=== -p --colored ===
+parity max even 2
+Streett 1
+parity min odd 3
+=== -pmin odd ===
+Rabin 1
+parity min odd 3
+parity min odd 3
+=== -pmin odd --colored ===
+Rabin 1
+parity min odd 3
+parity min odd 3
+=== -pmax even ===
+parity max even 2
+parity max even 3
+parity max even 4
+=== -pmax even --colored ===
+parity max even 2
+parity max even 3
+parity max even 4
+EOF
+diff expected5 res5
+
 ltlcross 'ltl2tgba -P' 'ltl2tgba -P"odd max"' 'ltl2tgba -P"even min"' \
          'ltl2tgba -p' 'ltl2tgba -p"odd max"' 'ltl2tgba -p"even min"' \
          -f FGa -f 'GFa&GFb' -f 'GF(a <-> XXXb)' -f '(p0 W XXGp0) & GFp1 & FGp2'

tests/sanity/bin.test

@@ -52,6 +52,11 @@ do
             echo "bin/man/$manpage is not listed in man/Makefile.am"
             exit_status=2
         fi
+        if ! grep -q "%{_mandir}/man./$manpage\*\$" $top_srcdir/spot.spec.in;
+        then
+            echo "$manpage is not listed in spot.spec.in"
+            exit_status=2
+        fi
     fi
 
     case $binary in
@@ -74,7 +79,7 @@ do
             ;;
     esac
 
-    # All man pages
+    # All tools
     case $manpage in
         *.1)
             if ! test -f $top_srcdir/doc/org/$binary.org; then
@@ -94,8 +99,20 @@ do
                 echo "$binary does not occur in doc/org/arch.tex"
                 exit_status=2
             fi
+            if ! grep -q "%{_bindir}/$binary\$" $top_srcdir/spot.spec.in; then
+                echo "$binary does is not listed in spot.spec.in";
+                exit_status=2
+            fi
+
     esac
 
+    if test -f $top_srcdir/bin/.gitignore; then
+        if ! grep -q "^$binary\$" $top_srcdir/bin/.gitignore; then
+            echo "$binary is not listed in bin/.gitignore"
+            exit_status=2
+        fi
+    fi
+
     # Check --help text.  Set a high rmargin to workaround some
     # bug in argp where an extra line it sometimes added if the end
     # of the document string fall right into the rmargin.
@@ -107,6 +124,7 @@ do
         echo "bin/$binary --help has options after blank line;" \
              "missing section header?"
         cat help-err
+        exit_status=2
     fi
     rm -f help-$binary.tmp help-err