diff --git a/.gitignore b/.gitignore
index 155a9b5e7..73745a48f 100644
--- a/.gitignore
+++ b/.gitignore
@@ -82,3 +82,4 @@ GTAGS
*.dsc
*.gcov
spot.spec
+default.nix
diff --git a/Makefile.am b/Makefile.am
index e198a977c..a5d842b4c 100644
--- a/Makefile.am
+++ b/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 $@
diff --git a/default.nix.in b/default.nix.in
new file mode 100644
index 000000000..8101e4f74
--- /dev/null
+++ b/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 .
+
+{ pkgs ? import {} }:
+let
+ version = "@VERSION@";
+in
+pkgs.stdenv.mkDerivation {
+ inherit version;
+ pname = "spot";
+
+ buildInputs = [
+ pkgs.python3
+ ];
+
+ src = ./.;
+
+ enableParallelBuilding = true;
+}
diff --git a/flake.lock b/flake.lock
new file mode 100644
index 000000000..dd215f1c6
--- /dev/null
+++ b/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
+}
diff --git a/flake.nix b/flake.nix
new file mode 100644
index 000000000..f0f3f95b5
--- /dev/null
+++ b/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
+ ]))
+ ];
+ };
+ });
+}
diff --git a/python/spot/impl.i b/python/spot/impl.i
index ee2c6a81e..a435758f6 100644
--- a/python/spot/impl.i
+++ b/python/spot/impl.i
@@ -89,6 +89,7 @@
#include
#include
#include
+#include
#include
#include
#include
@@ -638,6 +639,7 @@ namespace std {
%include
%include
%include
+%include
%include
%include
%include
diff --git a/spot/tl/Makefile.am b/spot/tl/Makefile.am
index abb431267..f2ff0fcad 100644
--- a/spot/tl/Makefile.am
+++ b/spot/tl/Makefile.am
@@ -32,7 +32,7 @@ tl_HEADERS = \
dot.hh \
environment.hh \
exclusive.hh \
- expansions.hh \
+ expansions2.hh \
formula.hh \
hierarchy.hh \
length.hh \
@@ -60,6 +60,7 @@ libtl_la_SOURCES = \
dot.cc \
exclusive.cc \
expansions.cc \
+ expansions2.cc \
formula.cc \
hierarchy.cc \
length.cc \
diff --git a/spot/tl/expansions.cc b/spot/tl/expansions.cc
index 756af4082..402236ea6 100644
--- a/spot/tl/expansions.cc
+++ b/spot/tl/expansions.cc
@@ -18,9 +18,11 @@
// along with this program. If not, see .
#include "config.h"
+#include
#include
#include
#include
+#include
#include
#include
#include
@@ -278,11 +280,11 @@ namespace spot
bdd dest_bdd = bdd_restrict(exp_, letter);
formula dest = bdd_to_sere(dest_bdd);
- #ifndef NDEBUG
- // make sure it didn't exist before
- auto it = std::find(res.begin(), res.end(), {letter, dest});
- SPOT_ASSERT(it == res.end());
- #endif
+ // #ifndef NDEBUG
+ // // make sure it didn't exist before
+ // auto it = std::find(res.begin(), res.end(), {letter, dest});
+ // SPOT_ASSERT(it == res.end());
+ // #endif
res.push_back({letter, dest});
}
@@ -338,7 +340,7 @@ namespace spot
expansion_t res;
- for (const auto [prefix, suffix] : unique_map)
+ for (const auto& [prefix, suffix] : unique_map)
{
if (!suffix.is(op::OrRat))
{
@@ -435,17 +437,22 @@ namespace spot
}
exp.clear();
- for (const auto [suffix, prefix] : unique_map)
+ for (const auto& [suffix, prefix] : unique_map)
{
exp.push_back({prefix, suffix});
}
}
- if (opts & exp_opts::expand_opt::UniquePrefix)
+ if (opts & exp_opts::expand_opt::UniquePrefix
+ || opts & exp_opts::expand_opt::UniquePrefixSeenOpt
+ || opts & exp_opts::expand_opt::UniquePrefixSeenCountOpt)
{
- exp = unique_prefix(exp);
- //exp = unique_prefix_seen(exp, seen);
- //exp = unique_prefix_count(exp, seen);
+ if (opts & exp_opts::expand_opt::UniquePrefixSeenOpt)
+ exp = unique_prefix_seen(exp, seen);
+ else if (opts & exp_opts::expand_opt::UniquePrefixSeenCountOpt)
+ exp = unique_prefix_count(exp, seen);
+ else
+ exp = unique_prefix(exp);
}
if (opts & exp_opts::expand_opt::UniqueSuffixPost)
@@ -462,7 +469,7 @@ namespace spot
}
exp.clear();
- for (const auto [suffix, prefix] : unique_map)
+ for (const auto& [suffix, prefix] : unique_map)
{
exp.push_back({prefix, suffix});
}
@@ -490,6 +497,18 @@ namespace spot
}
exp = exp_new;
}
+
+ // sort and remove duplicates from expansion to canonicalize it for
+ // eventual signature use
+ if (exp.size() >= 2)
+ {
+ std::sort(exp.begin(), exp.end(),
+ [](const auto& lhs, const auto& rhs) {
+ return std::make_pair(lhs.first.id(), lhs.second.id())
+ < std::make_pair(rhs.first.id(), rhs.second.id());
+ });
+ exp.erase(std::unique(exp.begin(), exp.end()), exp.end());
+ }
}
}
@@ -717,7 +736,10 @@ namespace spot
if ((li & kj) != bddfalse)
res.push_back({li & kj, fj});
}
- res.push_back({li, formula::Fusion({ei, F})});
+
+ formula ei_fusion_F = formula::Fusion({ei, F});
+ if (!ei_fusion_F.is(op::ff))
+ res.push_back({li, ei_fusion_F});
}
finalize(res, opts, d, seen);
@@ -817,7 +839,7 @@ namespace spot
struct signature_hash
{
std::size_t
- operator() (const std::pair& sig) const
+ operator() (const std::pair& sig) const noexcept
{
size_t hash = std::hash()(sig.first);
diff --git a/spot/tl/expansions.hh b/spot/tl/expansions.hh
index 036ac945a..9db8d2c8d 100644
--- a/spot/tl/expansions.hh
+++ b/spot/tl/expansions.hh
@@ -47,6 +47,8 @@ namespace spot
Determinize = 256,
UniquePrefixSeenOpt = 512,
UniqueSuffixPost = 1024,
+ UniquePrefixSeenCountOpt = 2048,
+ TransitionBased = 4096,
};
};
diff --git a/spot/tl/expansions2.cc b/spot/tl/expansions2.cc
new file mode 100644
index 000000000..d80e5ffa3
--- /dev/null
+++ b/spot/tl/expansions2.cc
@@ -0,0 +1,943 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2021 Laboratoire de Recherche et Développement de
+// l'Epita (LRDE).
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 3 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program. If not, see .
+
+#include "config.h"
+#include
+#include
+#include
+#include
+#include
+#include
+#include
+#include
+
+namespace spot
+{
+ namespace
+ {
+ // FIXME: could probably just return a map directly
+ static std::vector
+ formula_aps(formula f)
+ {
+ auto res = std::unordered_set();
+
+ 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 final;
+ std::vector 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 disj;
+ for (unsigned n = 0; n < s; ++n)
+ {
+ std::vector 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 formula2bdd_;
+ std::map 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 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 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 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* seen)
+ {
+ std::map 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 merge;
+ std::vector 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* 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* 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* 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* 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 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 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 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 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* seen)
+ {
+ using exp_t = expansion_t;
+
+ if (f.is_boolean())
+ {
+ auto f_bdd = formula_to_bdd(f, d, owner);
+
+ if (f_bdd == bddfalse)
+ return {};
+
+ return {{f_bdd, formula::eword()}};
+ }
+
+ auto rec = [&d, owner, opts, seen](formula f){
+ return expansion2(f, d, owner, exp_opts::None, seen);
+ };
+
+
+ switch (f.kind())
+ {
+ case op::ff:
+ case op::tt:
+ case op::ap:
+ SPOT_UNREACHABLE();
+
+ case op::eword:
+ // return {{bddfalse, formula::ff()}};
+ return {};
+
+ case op::Concat:
+ {
+ auto exps = rec(f[0]);
+
+ exp_t res;
+ for (const auto& [bdd_l, form] : exps)
+ {
+ res.push_back({bdd_l, formula::Concat({form, f.all_but(0)})});
+ }
+
+ if (f[0].accepts_eword())
+ {
+ auto exps_rest = rec(f.all_but(0));
+ for (const auto& [bdd_l, form] : exps_rest)
+ {
+ res.push_back({bdd_l, form});
+ }
+ }
+
+ finalize(res, opts, d, seen);
+ return res;
+ }
+
+ case op::FStar:
+ {
+ formula E = f[0];
+
+ if (f.min() == 0 && f.max() == 0)
+ return {{bddtrue, formula::eword()}};
+
+ auto min = f.min() == 0 ? 0 : (f.min() - 1);
+ auto max = f.max() == formula::unbounded()
+ ? formula::unbounded()
+ : (f.max() - 1);
+
+ auto E_i_j_minus = formula::FStar(E, min, max);
+
+ auto exp = rec(E);
+ exp_t res;
+ for (const auto& [li, ei] : exp)
+ {
+ res.push_back({li, formula::Fusion({ei, E_i_j_minus})});
+
+ if (ei.accepts_eword() && f.min() != 0)
+ {
+ for (const auto& [ki, fi] : rec(E_i_j_minus))
+ {
+ // FIXME: build bdd once
+ if ((li & ki) != bddfalse)
+ res.push_back({li & ki, fi});
+ }
+ }
+ }
+ if (f.min() == 0)
+ res.push_back({bddtrue, formula::eword()});
+
+ finalize(res, opts, d, seen);
+ return res;
+ }
+
+ case op::Star:
+ {
+ auto min = f.min() == 0 ? 0 : (f.min() - 1);
+ auto max = f.max() == formula::unbounded()
+ ? formula::unbounded()
+ : (f.max() - 1);
+
+ auto exps = rec(f[0]);
+
+ exp_t res;
+ for (const auto& [bdd_l, form] : exps)
+ {
+ res.push_back({bdd_l, formula::Concat({form, formula::Star(f[0], min, max)})});
+ }
+
+ finalize(res, opts, d, seen);
+ return res;
+ }
+
+ case op::AndNLM:
+ {
+ formula rewrite = rewrite_and_nlm(f);
+ auto res = rec(rewrite);
+ finalize(res, opts, d, seen);
+ return res;
+ }
+
+ case op::first_match:
+ {
+ auto exps = rec(f[0]);
+
+ exp_t res;
+ for (const auto& [bdd_l, form] : exps)
+ {
+ res.push_back({bdd_l, form});
+ }
+
+ // determinize
+ bdd or_labels = bddfalse;
+ bdd support = bddtrue;
+ bool is_det = true;
+ for (const auto& [l, _] : res)
+ {
+ support &= bdd_support(l);
+ if (is_det)
+ is_det = !bdd_have_common_assignment(l, or_labels);
+ or_labels |= l;
+ }
+
+ if (is_det)
+ {
+ for (auto& [_, dest] : res)
+ dest = formula::first_match(dest);
+ finalize(res, opts, d, seen);
+ return res;
+ }
+
+ exp_t res_det;
+ std::vector dests;
+ for (bdd l: minterms_of(or_labels, support))
+ {
+ for (const auto& [ndet_label, ndet_dest] : res)
+ {
+ if (bdd_implies(l, ndet_label))
+ dests.push_back(ndet_dest);
+ }
+ formula or_dests = formula::OrRat(dests);
+ res_det.push_back({l, or_dests});
+ dests.clear();
+ }
+
+ for (auto& [_, dest] : res_det)
+ dest = formula::first_match(dest);
+ finalize(res_det, opts, d, seen);
+ return res_det;
+ }
+
+ case op::Fusion:
+ {
+ exp_t res;
+ formula E = f[0];
+ formula F = f.all_but(0);
+
+ exp_t Ei = rec(E);
+ // TODO: std::option
+ exp_t Fj = rec(F);
+
+ for (const auto& [li, ei] : Ei)
+ {
+ if (ei.accepts_eword())
+ {
+ for (const auto& [kj, fj] : Fj)
+ if ((li & kj) != bddfalse)
+ res.push_back({li & kj, fj});
+ }
+ res.push_back({li, formula::Fusion({ei, F})});
+ }
+
+ finalize(res, opts, d, seen);
+ return res;
+ }
+
+ case op::AndRat:
+ {
+ exp_t res;
+ for (const auto& sub_f : f)
+ {
+ auto exps = rec(sub_f);
+
+ if (exps.empty())
+ {
+ // op::AndRat: one of the expansions was empty (the only
+ // edge was `false`), so the AndRat is empty as
+ // well
+ res.clear();
+ break;
+ }
+
+ if (res.empty())
+ {
+ res = std::move(exps);
+ continue;
+ }
+
+ exp_t new_res;
+ bool inserted = false;
+ for (const auto& [l_key, l_val] : exps)
+ {
+ for (const auto& [r_key, r_val] : res)
+ {
+ if ((l_key & r_key) != bddfalse)
+ {
+ new_res.push_back({l_key & r_key, formula::multop(f.kind(), {l_val, r_val})});
+ inserted = true;
+ }
+ }
+ }
+
+ if (!inserted)
+ {
+ // all prefix conjuctions led to bddfalse, And is empty
+ res.clear();
+ break;
+ }
+
+ res = std::move(new_res);
+ }
+
+ finalize(res, opts, d, seen);
+ return res;
+ }
+
+ case op::OrRat:
+ {
+ exp_t res;
+ for (const auto& sub_f : f)
+ {
+ auto exps = rec(sub_f);
+ if (exps.empty())
+ continue;
+
+ if (res.empty())
+ {
+ res = std::move(exps);
+ continue;
+ }
+
+ for (const auto& [label, dest] : exps)
+ res.push_back({label, dest});
+ }
+
+ finalize(res, opts, d, seen);
+ return res;
+ }
+
+ default:
+ std::cerr << "unimplemented kind "
+ << static_cast(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()(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();
+ auto signature2state = std::unordered_map();
+ auto seen = std::unordered_set();
+ 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();
+ 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>();
+ todo.push_back({f, init_state});
+
+ auto state_names = new std::vector();
+ 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;
+ }
+}
diff --git a/spot/tl/expansions2.hh b/spot/tl/expansions2.hh
new file mode 100644
index 000000000..e517bb87a
--- /dev/null
+++ b/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 .
+
+#pragma once
+
+#include