diff --git a/.gitignore b/.gitignore
index 73745a48f..155a9b5e7 100644
--- a/.gitignore
+++ b/.gitignore
@@ -82,4 +82,3 @@ GTAGS
*.dsc
*.gcov
spot.spec
-default.nix
diff --git a/Makefile.am b/Makefile.am
index a5d842b4c..e198a977c 100644
--- a/Makefile.am
+++ b/Makefile.am
@@ -65,8 +65,7 @@ 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 \
- default.nix default.nix.in
+ spot.spec spot.spec.in README.ltsmin
dist-hook: gen-ChangeLog
@@ -112,6 +111,3 @@ 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
deleted file mode 100644
index 8101e4f74..000000000
--- a/default.nix.in
+++ /dev/null
@@ -1,35 +0,0 @@
-# -*- 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
deleted file mode 100644
index dd215f1c6..000000000
--- a/flake.lock
+++ /dev/null
@@ -1,61 +0,0 @@
-{
- "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
deleted file mode 100644
index f0f3f95b5..000000000
--- a/flake.nix
+++ /dev/null
@@ -1,214 +0,0 @@
-{
- 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 a435758f6..ee2c6a81e 100644
--- a/python/spot/impl.i
+++ b/python/spot/impl.i
@@ -89,7 +89,6 @@
#include
#include
#include
-#include
#include
#include
#include
@@ -639,7 +638,6 @@ namespace std {
%include
%include
%include
-%include
%include
%include
%include
diff --git a/spot/tl/Makefile.am b/spot/tl/Makefile.am
index f2ff0fcad..abb431267 100644
--- a/spot/tl/Makefile.am
+++ b/spot/tl/Makefile.am
@@ -32,7 +32,7 @@ tl_HEADERS = \
dot.hh \
environment.hh \
exclusive.hh \
- expansions2.hh \
+ expansions.hh \
formula.hh \
hierarchy.hh \
length.hh \
@@ -60,7 +60,6 @@ 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 402236ea6..756af4082 100644
--- a/spot/tl/expansions.cc
+++ b/spot/tl/expansions.cc
@@ -18,11 +18,9 @@
// along with this program. If not, see .
#include "config.h"
-#include
#include
#include
#include
-#include
#include
#include
#include
@@ -280,11 +278,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});
}
@@ -340,7 +338,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))
{
@@ -437,22 +435,17 @@ 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
- || opts & exp_opts::expand_opt::UniquePrefixSeenOpt
- || opts & exp_opts::expand_opt::UniquePrefixSeenCountOpt)
+ if (opts & exp_opts::expand_opt::UniquePrefix)
{
- 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);
+ exp = unique_prefix(exp);
+ //exp = unique_prefix_seen(exp, seen);
+ //exp = unique_prefix_count(exp, seen);
}
if (opts & exp_opts::expand_opt::UniqueSuffixPost)
@@ -469,7 +462,7 @@ namespace spot
}
exp.clear();
- for (const auto& [suffix, prefix] : unique_map)
+ for (const auto [suffix, prefix] : unique_map)
{
exp.push_back({prefix, suffix});
}
@@ -497,18 +490,6 @@ 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());
- }
}
}
@@ -736,10 +717,7 @@ namespace spot
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});
+ res.push_back({li, formula::Fusion({ei, F})});
}
finalize(res, opts, d, seen);
@@ -839,7 +817,7 @@ namespace spot
struct signature_hash
{
std::size_t
- operator() (const std::pair& sig) const noexcept
+ operator() (const std::pair& sig) const
{
size_t hash = std::hash()(sig.first);
diff --git a/spot/tl/expansions.hh b/spot/tl/expansions.hh
index 9db8d2c8d..036ac945a 100644
--- a/spot/tl/expansions.hh
+++ b/spot/tl/expansions.hh
@@ -47,8 +47,6 @@ namespace spot
Determinize = 256,
UniquePrefixSeenOpt = 512,
UniqueSuffixPost = 1024,
- UniquePrefixSeenCountOpt = 2048,
- TransitionBased = 4096,
};
};
diff --git a/spot/tl/expansions2.cc b/spot/tl/expansions2.cc
deleted file mode 100644
index d80e5ffa3..000000000
--- a/spot/tl/expansions2.cc
+++ /dev/null
@@ -1,943 +0,0 @@
-// -*- 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
deleted file mode 100644
index e517bb87a..000000000
--- a/spot/tl/expansions2.hh
+++ /dev/null
@@ -1,45 +0,0 @@
-// -*- 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