From b7825552f8bd3c43d4340335b28420956ba68104 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 7 Feb 2022 16:10:40 +0100
Subject: [PATCH 01/18] remove uses of unary_function and binary_function

These were deprecated in C++11, and are supposed to be removed from
C++17, however gcc-snapshot just started warning about those.

* spot/misc/bddlt.hh, spot/misc/hash.hh, spot/misc/ltstr.hh,
spot/twa/taatgba.hh, spot/twaalgos/ltl2tgba_fm.cc: Here.
---
 spot/misc/bddlt.hh           | 11 ++++-------
 spot/misc/hash.hh            |  8 +++-----
 spot/misc/ltstr.hh           |  5 ++---
 spot/twa/taatgba.hh          |  8 +++-----
 spot/twaalgos/ltl2tgba_fm.cc |  7 +++----
 5 files changed, 15 insertions(+), 24 deletions(-)

diff --git a/spot/misc/bddlt.hh b/spot/misc/bddlt.hh
index 327fcd00a..46e24ed33 100644
--- a/spot/misc/bddlt.hh
+++ b/spot/misc/bddlt.hh
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2014, 2017, 2021 Laboratoire de Recherche et
+// Copyright (C) 2011, 2014, 2017, 2021, 2022 Laboratoire de Recherche et
 // Developpement de l'Epita (LRDE).
 // Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -33,8 +33,7 @@ namespace spot
   /// This comparison function use BDD ids for efficiency.  An
   /// algorithm depending on this order may return different results
   /// depending on how the BDD library has been used before.
-  struct bdd_less_than :
-    public std::binary_function<const bdd&, const bdd&, bool>
+  struct bdd_less_than
   {
     bool
     operator()(const bdd& left, const bdd& right) const
@@ -50,8 +49,7 @@ namespace spot
   /// long as the variable order is the same, the output of this
   /// comparison will be stable and independent on previous BDD
   /// operations.
-  struct bdd_less_than_stable :
-    public std::binary_function<const bdd&, const bdd&, bool>
+  struct bdd_less_than_stable
   {
     bool
     operator()(const bdd& left, const bdd& right) const
@@ -62,8 +60,7 @@ namespace spot
 
   /// \ingroup misc_tools
   /// \brief Hash functor for BDDs.
-  struct bdd_hash :
-    public std::unary_function<const bdd&, size_t>
+  struct bdd_hash
   {
     size_t
     operator()(const bdd& b) const noexcept
diff --git a/spot/misc/hash.hh b/spot/misc/hash.hh
index b99c4ab53..cad845a68 100644
--- a/spot/misc/hash.hh
+++ b/spot/misc/hash.hh
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2008, 2011, 2014, 2015-2018, 2021 Laboratoire de
+// Copyright (C) 2008, 2011, 2014, 2015-2018, 2021, 2022 Laboratoire de
 // Recherche et Développement de l'Epita (LRDE).
 // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de
 // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@@ -36,8 +36,7 @@ namespace spot
   /// \ingroup hash_funcs
   /// \brief A hash function for pointers.
   template <class T>
-  struct ptr_hash :
-    public std::unary_function<const T*, size_t>
+  struct ptr_hash
   {
     // A default constructor is needed if the ptr_hash object is
     // stored in a const member.  This occur with the clang version
@@ -59,8 +58,7 @@ namespace spot
   /// \ingroup hash_funcs
   /// \brief A hash function that returns identity
   template<typename T>
-  struct identity_hash:
-    public std::unary_function<const T&, size_t>
+  struct identity_hash
   {
     // A default constructor is needed if the identity_hash object is
     // stored in a const member.
diff --git a/spot/misc/ltstr.hh b/spot/misc/ltstr.hh
index 25b561b3b..15f7d11ef 100644
--- a/spot/misc/ltstr.hh
+++ b/spot/misc/ltstr.hh
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2015 Laboratoire de Recherche et Développement
+// Copyright (C) 2015, 2022 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE)
 // Copyright (C) 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -39,8 +39,7 @@ namespace spot
   /// \code
   ///   std::map<const char*, int, spot::state_ptr_less_than> seen;
   /// \endcode
-  struct char_ptr_less_than:
-    public std::binary_function<const char*, const char*, bool>
+  struct char_ptr_less_than
   {
     bool
     operator()(const char* left, const char* right) const
diff --git a/spot/twa/taatgba.hh b/spot/twa/taatgba.hh
index 9daa4975d..6a5b1c470 100644
--- a/spot/twa/taatgba.hh
+++ b/spot/twa/taatgba.hh
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2011-2019 Laboratoire de Recherche et Développement de
-// l'Epita (LRDE).
+// Copyright (C) 2009, 2011-2019, 2022 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -121,9 +121,7 @@ namespace spot
                                std::vector<taa_tgba::transition*>,
                                state_ptr_hash, state_ptr_equal> seen_map;
 
-    struct distance_sort :
-      public std::binary_function<const iterator_pair&,
-                                  const iterator_pair&, bool>
+    struct distance_sort
     {
       bool
       operator()(const iterator_pair& lhs, const iterator_pair& rhs) const
diff --git a/spot/twaalgos/ltl2tgba_fm.cc b/spot/twaalgos/ltl2tgba_fm.cc
index 9ad149c1c..3566abc97 100644
--- a/spot/twaalgos/ltl2tgba_fm.cc
+++ b/spot/twaalgos/ltl2tgba_fm.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2008-2019, 2021 Laboratoire de Recherche et Développement
-// de l'Epita (LRDE).
+// Copyright (C) 2008-2019, 2021-2022 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 // Copyright (C) 2003-2006 Laboratoire d'Informatique de Paris 6
 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
 // Pierre et Marie Curie.
@@ -199,8 +199,7 @@ namespace spot
         }
       };
 
-      struct flagged_formula_hash:
-        public std::unary_function<flagged_formula, size_t>
+      struct flagged_formula_hash
       {
         size_t
         operator()(const flagged_formula& that) const

From 64020279cb9393d7783d72c2c8ae9bcb19923301 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sun, 13 Feb 2022 18:37:34 +0100
Subject: [PATCH 02/18] reduce_parity: fix to work on automata with deleted
 edges

* spot/twaalgos/parity.cc (reduce_parity): Use the
size of the edge vector to initialize piprime1 and piprime2,
not the number of edges.
* tests/python/parity.py: Add test case, based on a report
by Yann Thierry-Mieg.
---
 NEWS                    |  5 +++++
 spot/twaalgos/parity.cc |  9 +++++----
 tests/python/parity.py  | 16 +++++++++++++++-
 3 files changed, 25 insertions(+), 5 deletions(-)

diff --git a/NEWS b/NEWS
index 6d5fd9fc3..99a239a81 100644
--- a/NEWS
+++ b/NEWS
@@ -2,6 +2,11 @@ New in spot 2.10.4.dev  (net yet released)
 
   Nothing yet.
 
+  Bugs fixed:
+
+  - reduce_parity() produced incorrect results when applied to
+    automata with deleted edges.
+
 New in spot 2.10.4  (2022-02-01)
 
   Bug fixed:
diff --git a/spot/twaalgos/parity.cc b/spot/twaalgos/parity.cc
index 35ec10a90..94c7bd922 100644
--- a/spot/twaalgos/parity.cc
+++ b/spot/twaalgos/parity.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2016, 2018, 2019 Laboratoire de Recherche et Développement
-// de l'Epita (LRDE).
+// Copyright (C) 2016, 2018, 2019, 2022 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -465,8 +465,9 @@ namespace spot
     // using k=0 or k=1.
     //
     // -2 means the edge was never assigned a color.
-    std::vector<int> piprime1(aut->num_edges() + 1, -2); // k=1
-    std::vector<int> piprime2(aut->num_edges() + 1, -2); // k=0
+    unsigned evs = aut->edge_vector().size();
+    std::vector<int> piprime1(evs, -2); // k=1
+    std::vector<int> piprime2(evs, -2); // k=0
     bool sba = aut->prop_state_acc().is_true();
 
     auto rec =
diff --git a/tests/python/parity.py b/tests/python/parity.py
index dfeb24d3d..b0389c40e 100644
--- a/tests/python/parity.py
+++ b/tests/python/parity.py
@@ -1,6 +1,6 @@
 #!/usr/bin/python3
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2018, 2019 Laboratoire de Recherche et Développement de
+# Copyright (C) 2018, 2019, 2022 Laboratoire de Recherche et Développement de
 # l'EPITA.
 #
 # This file is part of Spot, a model checking library.
@@ -155,3 +155,17 @@ except RuntimeError as e:
   assert "invalid state number" in str(e)
 else:
   report_missing_exception()
+
+
+a = spot.automaton("""HOA: v1 name: "F(!p0 | X!p1)" States: 3
+Start: 1 AP: 2 "p0" "p1" acc-name: Buchi Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels trans-acc complete
+properties: deterministic terminal --BODY-- State: 0 [t] 0 {0} State:
+1 [!0] 0 [0] 2 State: 2 [!0 | !1] 0 [0&1] 2 --END--""")
+# Erase the first edge of state 1
+oi = a.out_iteraser(1)
+oi.erase()
+# postprocess used to call reduce_parity that did not
+# work correctly on automata with deleted edges.
+sm = a.postprocess("gen", "small")
+assert sm.num_states() == 3

From 7d9fddadceb51b512e294eed7f088aff9e78a4ad Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 16 Feb 2022 11:42:06 +0100
Subject: [PATCH 03/18] work around an issue in Flex 2.6.4

The fallback definition of SIZE_MAX supplied by flex was not
preprocessor friendly and prevented robin_hood.hh from doing "#if
SIZE_MAX == UINT64_MAX", as observed by Marc Espie on OpenBSD.

* spot/parseaut/scanaut.ll, spot/parsetl/scantl.ll: Define
__STDC_VERSION__ just so that the code generated by Flex
include <inttypes.h>.
* NEWS: Mention the bug.
* THANKS: Add Marc.
---
 NEWS                     |  3 +++
 THANKS                   |  1 +
 spot/parseaut/scanaut.ll |  8 ++++++++
 spot/parsetl/scantl.ll   | 12 ++++++++++--
 4 files changed, 22 insertions(+), 2 deletions(-)

diff --git a/NEWS b/NEWS
index 99a239a81..f2b95e7ba 100644
--- a/NEWS
+++ b/NEWS
@@ -7,6 +7,9 @@ New in spot 2.10.4.dev  (net yet released)
   - reduce_parity() produced incorrect results when applied to
     automata with deleted edges.
 
+  - work around a portability issue in Flex 2.6.4 preventing
+    compilation on OpenBSD.
+
 New in spot 2.10.4  (2022-02-01)
 
   Bug fixed:
diff --git a/THANKS b/THANKS
index 193dccaf7..9eb566483 100644
--- a/THANKS
+++ b/THANKS
@@ -31,6 +31,7 @@ Joachim Klein
 Juan Tzintzun
 Juraj Major
 Kristin Y. Rozier
+Marc Espie
 Martin Dieguez Lodeiro
 Matthias Heizmann
 Maxime Bouton
diff --git a/spot/parseaut/scanaut.ll b/spot/parseaut/scanaut.ll
index c1c4fb44f..bf35810ed 100644
--- a/spot/parseaut/scanaut.ll
+++ b/spot/parseaut/scanaut.ll
@@ -26,6 +26,14 @@
 /* %option debug */
 %top{
 #include "config.h"
+/* Flex 2.6.4's test for <inttypes.h> relies on __STDC_VERSION__
+   which is undefined in C++.   So without that, it will define
+   its own integer types, including a broken SIZE_MAX definition.
+   So let's define __STDC_VERSION__ to make sure <inttypes.h> gets
+   included. */
+#if HAVE_INTTYPES_H && !(defined __STDC_VERSION__)
+#  define __STDC_VERSION__ 199901L
+#endif
 }
 %{
 #include <string>
diff --git a/spot/parsetl/scantl.ll b/spot/parsetl/scantl.ll
index ff15685f8..554c28298 100644
--- a/spot/parsetl/scantl.ll
+++ b/spot/parsetl/scantl.ll
@@ -1,6 +1,6 @@
 /* -*- coding: utf-8 -*-
-** Copyright (C) 2010-2015, 2017-2019, 2021, Laboratoire de Recherche
-** et Développement de l'Epita (LRDE).
+** Copyright (C) 2010-2015, 2017-2019, 2021-2022, Laboratoire de
+** Recherche et Développement de l'Epita (LRDE).
 ** Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6
 ** (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
 ** Pierre et Marie Curie.
@@ -28,6 +28,14 @@
 
 %top{
 #include "config.h"
+/* Flex 2.6.4's test for <inttypes.h> relies on __STDC_VERSION__
+   which is undefined in C++.   So without that, it will define
+   its own integer types, including a broken SIZE_MAX definition.
+   So let's define __STDC_VERSION__ to make sure <inttypes.h> gets
+   included. */
+#if HAVE_INTTYPES_H && !(defined __STDC_VERSION__)
+#  define __STDC_VERSION__ 199901L
+#endif
 }
 %{
 #include <cstdlib>

From 7149e5a34d4dc5374f81833e2f49f77c3a214e1e Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 3 Mar 2022 09:10:53 +0100
Subject: [PATCH 04/18] * .gitlab-ci.yml (alpine-gcc): Fix path for logs.

---
 .gitlab-ci.yml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 583774da0..3c66af0b7 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -115,8 +115,9 @@ alpine-gcc:
   artifacts:
     when: always
     paths:
-      - tests/*/*.log
+      - ./spot-*/_build/sub/tests/*/*.log
       - ./*.log
+      - ./*.tar.gz
 
 arch-clang:
   stage: build

From d61d6e5e2fa91046a20acad8820c88d2448a408e Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 3 Mar 2022 18:01:11 +0100
Subject: [PATCH 05/18] tests: avoid seq

Partial fix for #501.

* tests/core/prodchain.test: Hardcode the seq output.
* tests/core/bricks.test: Use $AWK instead of seq.
* tests/core/defs.in: Define $AWK.
* NEWS: Mention the bug.
---
 NEWS                      |  3 +++
 tests/core/bricks.test    | 11 ++++++-----
 tests/core/defs.in        |  3 ++-
 tests/core/prodchain.test |  5 +++--
 4 files changed, 14 insertions(+), 8 deletions(-)

diff --git a/NEWS b/NEWS
index f2b95e7ba..7f3429991 100644
--- a/NEWS
+++ b/NEWS
@@ -10,6 +10,9 @@ New in spot 2.10.4.dev  (net yet released)
   - work around a portability issue in Flex 2.6.4 preventing
     compilation on OpenBSD.
 
+  - Do not use the seq command in test cases, it is not available
+    everywhere.
+
 New in spot 2.10.4  (2022-02-01)
 
   Bug fixed:
diff --git a/tests/core/bricks.test b/tests/core/bricks.test
index b98c7e856..37ff57cb0 100644
--- a/tests/core/bricks.test
+++ b/tests/core/bricks.test
@@ -1,7 +1,7 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2020 Laboratoire de Recherche et Développement de
-# l'Epita (LRDE).
+# Copyright (C) 2020, 2022 Laboratoire de Recherche et Développement
+# de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -21,12 +21,13 @@
 . ./defs
 set -e
 
-seq 0 1999 > expected
+# The seq command is not always available, but we assume awk is.
+$AWK 'BEGIN{for(x=0;x<2000;++x) print x;}' >expected
 
 ../bricks > stdout
 
-cat stdout | head -n 2000 | awk '{print $2}' | sed 's/{//g' | \
-    awk -F',' '{print $1}' | sort -n > map
+cat stdout | head -n 2000 | $AWK '{print $2}' | sed 's/{//g' | \
+    $AWK -F',' '{print $1}' | sort -n > map
 
 diff expected map
 
diff --git a/tests/core/defs.in b/tests/core/defs.in
index 7df6fdf77..d06a3b67d 100644
--- a/tests/core/defs.in
+++ b/tests/core/defs.in
@@ -1,5 +1,5 @@
 # -*- mode: shell-script; coding: utf-8 -*-
-# Copyright (C) 2009, 2010, 2012, 2013, 2015 Laboratoire de Recherche
+# Copyright (C) 2009, 2010, 2012, 2013, 2015, 2022 Laboratoire de Recherche
 # et Développement de l'Epita (LRDE).
 # Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -57,6 +57,7 @@ case $srcdir in
   *) srcdir=../$srcdir
 esac
 
+AWK='@AWK@'
 DOT='@DOT@'
 LBTT="@LBTT@"
 LBTT_TRANSLATE="@LBTT_TRANSLATE@"
diff --git a/tests/core/prodchain.test b/tests/core/prodchain.test
index b5037782f..0a7f1a1d9 100755
--- a/tests/core/prodchain.test
+++ b/tests/core/prodchain.test
@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2018 Laboratoire de Recherche et Développement
+# Copyright (C) 2018, 2022 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -23,7 +23,8 @@ set -e
 
 set x
 shift
-for i in `seq 1 42`; do
+for i in 01 02 03 04 05 06 07 08 09 10 11 12 13 14 15 16 17 18 19 20 21 \
+         22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42; do
   ltl2tgba "{a[*$i]}[]->GFb" > $i.hoa
 done
 for i in *.hoa; do

From 734de00bfd54de20ac142aabb90f1fca0cde0d7d Mon Sep 17 00:00:00 2001
From: Antoine Martin <amartin@lrde.epita.fr>
Date: Thu, 10 Mar 2022 15:49:46 +0100
Subject: [PATCH 06/18] tests: don't wipe python environment

* tests/run.in: keep original PYTHONPATH contents
* NEWS: mention the bug
---
 NEWS         | 3 +++
 tests/run.in | 9 ++++++---
 2 files changed, 9 insertions(+), 3 deletions(-)

diff --git a/NEWS b/NEWS
index 7f3429991..301711588 100644
--- a/NEWS
+++ b/NEWS
@@ -13,6 +13,9 @@ New in spot 2.10.4.dev  (net yet released)
   - Do not use the seq command in test cases, it is not available
     everywhere.
 
+  - Do not erase the previous contents of the PYTHONPATH environment
+    variable when running tests, prepend to it instead.
+
 New in spot 2.10.4  (2022-02-01)
 
   Bug fixed:
diff --git a/tests/run.in b/tests/run.in
index d14bf52a9..7eaa7732c 100755
--- a/tests/run.in
+++ b/tests/run.in
@@ -104,18 +104,21 @@ export srcdir
 
 case $1 in
   *.ipynb)
-    PYTHONPATH=$pypath DYLD_LIBRARY_PATH=$modpath:$DYLD_LIBRARY_PATH \
+    PYTHONPATH=$pypath:$PYTHONPATH \
+    DYLD_LIBRARY_PATH=$modpath:$DYLD_LIBRARY_PATH \
     PYTHONIOENCODING=utf-8:surrogateescape \
     exec $PREFIXCMD @PYTHON@ @abs_srcdir@/python/ipnbdoctest.py "$@";;
   *.py)
-    PYTHONPATH=$pypath DYLD_LIBRARY_PATH=$modpath:$DYLD_LIBRARY_PATH \
+    PYTHONPATH=$pypath:$PYTHONPATH \
+    DYLD_LIBRARY_PATH=$modpath:$DYLD_LIBRARY_PATH \
     exec $PREFIXCMD @PYTHON@ "$@";;
   *.test)
     exec sh -x "$@";;
   *.pl)
     exec $PERL "$@";;
   *python*|*jupyter*|*pypy*)
-    PYTHONPATH=$pypath DYLD_LIBRARY_PATH=$modpath:$DYLD_LIBRARY_PATH \
+    PYTHONPATH=$pypath:$PYTHONPATH \
+    DYLD_LIBRARY_PATH=$modpath:$DYLD_LIBRARY_PATH \
     exec $PREFIXCMD "$@";;
   *)
     echo "Unknown extension" >&2

From 2aecf9a79e64c55e8cac803591f73d93552a46e4 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 10 Mar 2022 10:53:18 +0100
Subject: [PATCH 07/18] fix typos and make formula_from_bdd more usable in
 Python

* python/spot/impl.i (formula_from_bdd): Instantiate for twa_graph.
* spot/twa/twa.hh (register_aps_from_dict): Typo in exception.
* tests/python/except.py: More tests for the above.
* tests/python/bdddict.py: Typo in comment.
---
 python/spot/impl.i      |  2 ++
 spot/twa/twa.hh         |  4 ++--
 tests/python/bdddict.py |  4 ++--
 tests/python/except.py  | 38 +++++++++++++++++++++++++++++++++++++-
 4 files changed, 43 insertions(+), 5 deletions(-)

diff --git a/python/spot/impl.i b/python/spot/impl.i
index 12cae6311..21a9a68b8 100644
--- a/python/spot/impl.i
+++ b/python/spot/impl.i
@@ -530,6 +530,8 @@ namespace std {
 %include <spot/twa/bdddict.hh>
 %include <spot/twa/bddprint.hh>
 %include <spot/twa/formula2bdd.hh>
+%template(formula_to_bdd) spot::formula_to_bdd<spot::twa_graph>;
+
 %include <spot/twa/fwd.hh>
  /* These operators may raise exceptions, and we do not
     want Swig4 to convert those exceptions to NotImplemented. */
diff --git a/spot/twa/twa.hh b/spot/twa/twa.hh
index cb1e208ec..819a90962 100644
--- a/spot/twa/twa.hh
+++ b/spot/twa/twa.hh
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2011, 2013-2021 Laboratoire de Recherche et
+// Copyright (C) 2009, 2011, 2013-2022 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 // Copyright (C) 2003-2005 Laboratoire d'Informatique de Paris 6
 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
@@ -761,7 +761,7 @@ namespace spot
     void register_aps_from_dict()
     {
       if (!aps_.empty())
-        throw std::runtime_error("register_ap_from_dict() may not be"
+        throw std::runtime_error("register_aps_from_dict() may not be"
                                  " called on an automaton that has already"
                                  " registered some AP");
       auto& m = get_dict()->bdd_map;
diff --git a/tests/python/bdddict.py b/tests/python/bdddict.py
index d6222b58f..45c505385 100644
--- a/tests/python/bdddict.py
+++ b/tests/python/bdddict.py
@@ -17,8 +17,8 @@
 # You should have received a copy of the GNU General Public License
 # along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
-# Make sure we can leep track of BDD association in Python using bdd_dict, as
-# discussed in issue #372.
+# Make sure we can keep track of BDD association in Python using bdd_dict, as
+# discussed in (deleted???) issue #372.
 
 # CPython use reference counting, so that automata are destructed
 # when we expect them to be.   However other implementations like
diff --git a/tests/python/except.py b/tests/python/except.py
index ef6ec3cc5..76ae88b0a 100644
--- a/tests/python/except.py
+++ b/tests/python/except.py
@@ -1,5 +1,5 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2018-2021 Laboratoire de Recherche et Développement de
+# Copyright (C) 2018-2022 Laboratoire de Recherche et Développement de
 # l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -24,6 +24,8 @@
 
 import spot
 import buddy
+from unittest import TestCase
+tc = TestCase()
 
 
 def report_missing_exception():
@@ -278,3 +280,37 @@ except OverflowError as e:
     assert "reversed" in str(e)
 else:
     report_missing_exception()
+
+
+a = spot.make_twa_graph()
+s = a.new_state()
+b = spot.formula_to_bdd("a & b", a.get_dict(), a)
+a.new_edge(s, s, b, [])
+try:
+    print(a.to_str('hoa'))
+except RuntimeError as e:
+    tc.assertIn("unregistered atomic propositions", str(e))
+else:
+    report_missing_exception()
+
+a.register_aps_from_dict()
+tc.assertEqual(a.to_str('hoa'), """HOA: v1
+States: 1
+Start: 0
+AP: 2 "a" "b"
+acc-name: all
+Acceptance: 0 t
+properties: trans-labels explicit-labels state-acc deterministic
+--BODY--
+State: 0
+[0&1] 0
+--END--""")
+
+try:
+    a.register_aps_from_dict()
+except RuntimeError as e:
+    se = str(e)
+    tc.assertIn("register_aps_from_dict", se)
+    tc.assertIn("already registered", se)
+else:
+    report_missing_exception()

From 968ef0f7b89431f44f6c90c4ed5b2c7b92bb345a Mon Sep 17 00:00:00 2001
From: Florian Renkin <frenkin@lrde.epita.fr>
Date: Tue, 15 Mar 2022 14:01:25 +0100
Subject: [PATCH 08/18] ltlsynt: typo in help

* bin/ltlsynt.cc: here
---
 bin/ltlsynt.cc | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc
index 57b67bcc0..c6e53258c 100644
--- a/bin/ltlsynt.cc
+++ b/bin/ltlsynt.cc
@@ -65,7 +65,7 @@ static const argp_option options[] =
       "comma-separated list of controllable (a.k.a. output) atomic"
       " propositions", 0},
     { "ins", OPT_INPUT, "PROPS", 0,
-      "comma-separated list of controllable (a.k.a. output) atomic"
+      "comma-separated list of uncontrollable (a.k.a. input) atomic"
       " propositions", 0},
     /**************************************************/
     { nullptr, 0, nullptr, 0, "Fine tuning:", 10 },

From 96e051d2bb971ebecb27b21db3ea1d9c65a9f3bd Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 22 Mar 2022 12:18:25 +0100
Subject: [PATCH 09/18] graph: fix invalid read

Reported by Florian Renkin.

* spot/graph/graph.hh (sort_edges_of): Fix invalid read when sorting a
state without successor.  Seen on core/tgbagraph.test.
---
 spot/graph/graph.hh | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

diff --git a/spot/graph/graph.hh b/spot/graph/graph.hh
index 75e0977b7..fa276131d 100644
--- a/spot/graph/graph.hh
+++ b/spot/graph/graph.hh
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014-2018, 2020, 2021 Laboratoire de Recherche et
+// Copyright (C) 2014-2018, 2020-2022 Laboratoire de Recherche et
 // Développement de l'Epita.
 //
 // This file is part of Spot, a model checking library.
@@ -1243,14 +1243,19 @@ namespace spot
       //dump_storage(std::cerr);
       auto pi = [&](unsigned t1, unsigned t2)
           {return p(edges_[t1], edges_[t2]); };
+
+      // Sort the outgoing edges of each selected state according
+      // to predicate p.  Do that in place.
       std::vector<unsigned> sort_idx_;
-      for (unsigned i = 0; i < num_states(); ++i)
+      unsigned ns = num_states();
+      for (unsigned i = 0; i < ns; ++i)
         {
           if (to_sort_ptr && !(*to_sort_ptr)[i])
             continue;
-
-          sort_idx_.clear();
           unsigned t = states_[i].succ;
+          if (t == 0)
+            continue;
+          sort_idx_.clear();
           do
             {
                sort_idx_.push_back(t);

From 53118d9314783ce97a0069e14d390fba9f7f7eed Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 22 Mar 2022 12:22:48 +0100
Subject: [PATCH 10/18] * spot/twaalgos/gfguarantee.hh: Typos in comments.

---
 spot/twaalgos/gfguarantee.hh | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/spot/twaalgos/gfguarantee.hh b/spot/twaalgos/gfguarantee.hh
index 5124667f4..40cb16f97 100644
--- a/spot/twaalgos/gfguarantee.hh
+++ b/spot/twaalgos/gfguarantee.hh
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2018 Laboratoire de Recherche et Développement
+// Copyright (C) 2018, 2022 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -48,7 +48,7 @@ namespace spot
   /// \brief Convert GF(φ) into a (D)BA if φ is a guarantee property.
   ///
   /// If the formula \a gf has the form GΦ where Φ matches either F(φ)
-  /// or F(φ₁)|F(φ₂)|...|F(φₙ), we translate Φ into A_Φ and attempt to
+  /// or F(φ₁)&F(φ₂)&...&F(φₙ), we translate Φ into A_Φ and attempt to
   /// minimize it to a WDBA W_Φ.  If the resulting automaton is
   /// terminal, we then call g_f_terminal_inplace(W_Φ).  If \a
   /// deterministic is not set, we keep the minimized automaton only

From d1f49c721a45c58f24c085dfb14e3f70f1c7089d Mon Sep 17 00:00:00 2001
From: Florian Renkin <frenkin@lrde.epita.fr>
Date: Mon, 21 Mar 2022 10:46:42 +0100
Subject: [PATCH 11/18] ltlsynt: don't fail if --outs or --ins is set to empty

* bin/ltlsynt.cc: here
* tests/core/ltlsynt.test: add tests
---
 bin/ltlsynt.cc          | 58 +++++++++++++++++++++++------------------
 tests/core/ltlsynt.test |  8 ++++++
 2 files changed, 40 insertions(+), 26 deletions(-)

diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc
index c6e53258c..f5b2ade51 100644
--- a/bin/ltlsynt.cc
+++ b/bin/ltlsynt.cc
@@ -135,8 +135,8 @@ Exit status:\n\
   1   if the input problem is not realizable\n\
   2   if any error has been reported";
 
-static std::vector<std::string> all_output_aps;
-static std::vector<std::string> all_input_aps;
+static std::optional<std::vector<std::string>> all_output_aps;
+static std::optional<std::vector<std::string>> all_input_aps;
 
 static const char* opt_csv = nullptr;
 static bool opt_print_pg = false;
@@ -577,12 +577,12 @@ namespace
   class ltl_processor final : public job_processor
   {
   private:
-    std::vector<std::string> input_aps_;
-    std::vector<std::string> output_aps_;
+    std::optional<std::vector<std::string>> input_aps_;
+    std::optional<std::vector<std::string>> output_aps_;
 
   public:
-    ltl_processor(std::vector<std::string> input_aps_,
-                  std::vector<std::string> output_aps_)
+    ltl_processor(std::optional<std::vector<std::string>> input_aps_,
+                  std::optional<std::vector<std::string>> output_aps_)
         : input_aps_(std::move(input_aps_)),
           output_aps_(std::move(output_aps_))
     {
@@ -592,11 +592,13 @@ namespace
                         const char* filename, int linenum) override
     {
       auto unknown_aps = [](spot::formula f,
-                            const std::vector<std::string>& known,
-                            const std::vector<std::string>* known2 = nullptr)
+                    const std::optional<std::vector<std::string>>& known,
+                    const std::optional<std::vector<std::string>>& known2 = {})
       {
         std::vector<std::string> unknown;
         std::set<spot::formula> seen;
+        // If we don't have --ins and --outs, we must not find an AP.
+        bool can_have_ap = known.has_value();
         f.traverse([&](const spot::formula& s)
         {
           if (s.is(spot::op::ap))
@@ -604,10 +606,11 @@ namespace
               if (!seen.insert(s).second)
                 return false;
               const std::string& a = s.ap_name();
-              if (std::find(known.begin(), known.end(), a) == known.end()
-                  && (!known2
+              if (!can_have_ap
+                  || (std::find(known->begin(), known->end(), a) == known->end()
+                  && (!known2.has_value()
                       || std::find(known2->begin(),
-                                   known2->end(), a) == known2->end()))
+                                   known2->end(), a) == known2->end())))
                 unknown.push_back(a);
             }
           return false;
@@ -617,30 +620,30 @@ namespace
 
       // Decide which atomic propositions are input or output.
       int res;
-      if (input_aps_.empty() && !output_aps_.empty())
+      if (!input_aps_.has_value() && output_aps_.has_value())
         {
-          res = solve_formula(f, unknown_aps(f, output_aps_), output_aps_);
+          res = solve_formula(f, unknown_aps(f, output_aps_), *output_aps_);
         }
-      else if (output_aps_.empty() && !input_aps_.empty())
+      else if (!output_aps_.has_value() && input_aps_.has_value())
         {
-          res = solve_formula(f, input_aps_, unknown_aps(f, input_aps_));
+          res = solve_formula(f, *input_aps_, unknown_aps(f, input_aps_));
         }
-      else if (output_aps_.empty() && input_aps_.empty())
+      else if (!output_aps_.has_value() && !input_aps_.has_value())
         {
-          for (const std::string& ap: unknown_aps(f, input_aps_, &output_aps_))
+          for (const std::string& ap: unknown_aps(f, input_aps_, output_aps_))
             error_at_line(2, 0, filename, linenum,
                           "one of --ins or --outs should list '%s'",
                           ap.c_str());
-          res = solve_formula(f, input_aps_, output_aps_);
+          res = solve_formula(f, *input_aps_, *output_aps_);
         }
       else
         {
-          for (const std::string& ap: unknown_aps(f, input_aps_, &output_aps_))
+          for (const std::string& ap: unknown_aps(f, input_aps_, output_aps_))
             error_at_line(2, 0, filename, linenum,
                           "both --ins and --outs are specified, "
                           "but '%s' is unlisted",
                           ap.c_str());
-          res = solve_formula(f, input_aps_, output_aps_);
+          res = solve_formula(f, *input_aps_, *output_aps_);
         }
 
       if (opt_csv)
@@ -671,23 +674,25 @@ parse_opt(int key, char *arg, struct argp_state *)
       break;
     case OPT_INPUT:
       {
+        all_input_aps.emplace(std::vector<std::string>{});
         std::istringstream aps(arg);
         std::string ap;
         while (std::getline(aps, ap, ','))
           {
             ap.erase(remove_if(ap.begin(), ap.end(), isspace), ap.end());
-            all_input_aps.push_back(str_tolower(ap));
+            all_input_aps->push_back(str_tolower(ap));
           }
         break;
       }
     case OPT_OUTPUT:
       {
+        all_output_aps.emplace(std::vector<std::string>{});
         std::istringstream aps(arg);
         std::string ap;
         while (std::getline(aps, ap, ','))
           {
             ap.erase(remove_if(ap.begin(), ap.end(), isspace), ap.end());
-            all_output_aps.push_back(str_tolower(ap));
+            all_output_aps->push_back(str_tolower(ap));
           }
         break;
       }
@@ -748,10 +753,11 @@ main(int argc, char **argv)
     check_no_formula();
 
     // Check if inputs and outputs are distinct
-    for (const std::string& ai : all_input_aps)
-      if (std::find(all_output_aps.begin(), all_output_aps.end(), ai)
-          != all_output_aps.end())
-        error(2, 0, "'%s' appears both in --ins and --outs", ai.c_str());
+    if (all_input_aps.has_value() && all_output_aps.has_value())
+      for (const std::string& ai : *all_input_aps)
+        if (std::find(all_output_aps->begin(), all_output_aps->end(), ai)
+            != all_output_aps->end())
+          error(2, 0, "'%s' appears both in --ins and --outs", ai.c_str());
 
     ltl_processor processor(all_input_aps, all_output_aps);
     if (int res = processor.run(); res == 0 || res == 1)
diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test
index 4d318dbae..99d1e92da 100644
--- a/tests/core/ltlsynt.test
+++ b/tests/core/ltlsynt.test
@@ -821,3 +821,11 @@ ltlsynt -f '!(F(a | b))' --outs=b, --decompose=yes \
                          --verbose --aiger 2> out || true
 sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx
 diff outx exp
+
+ltlsynt --ins="" -f "GFa"
+ltlsynt --outs="" -f "GFb" | grep "UNREALIZABLE"
+
+ltlsynt --outs="" -f "1"
+
+ltlsynt --outs="" --ins="" -f "GFa" 2>&1 | \
+  grep "both --ins and --outs are specified"
\ No newline at end of file

From 58f39ec2874c34a7f7e71c5fb683e89ab41ca095 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 25 Mar 2022 09:25:04 +0100
Subject: [PATCH 12/18] * doc/org/tut40.org: Clarify, as suggested by a CAV'22
 reviewer.

---
 doc/org/tut40.org | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/doc/org/tut40.org b/doc/org/tut40.org
index b68efe558..8d9b004da 100644
--- a/doc/org/tut40.org
+++ b/doc/org/tut40.org
@@ -144,9 +144,11 @@ states.
 
 We now look at how to create such a game in Python.
 
-Essentially, a game in Spot is just an automaton equiped with a
-special property to indicate the owner of each states.  So it can be
-created using the usual interface:
+Essentially, a game in Spot is just an automaton equiped with a [[file:concepts.org::#named-properties][named
+property "state-player"]] that hold a Boolean vector indicating the
+owner of each state.  The game can be created using the usual
+automaton interface, and the owners are set by calling
+=game.set_state_players()= with a vector of Boolean at the very end.
 
 #+NAME: build_game
 #+BEGIN_SRC python :exports code
@@ -173,7 +175,7 @@ created using the usual interface:
       todo = []
 
       # Create the state (i, j) for a player if it does not exist yet and
-      # returns the state's number in the game.
+      # return the state's number in the game.
       def get_game_state(player, i, j):
           orig_state = s_orig_states if player else d_orig_states
           if (i, j) in orig_state:

From add2fced4430e01304a2cfae1b81675c7fe8c51f Mon Sep 17 00:00:00 2001
From: Philipp Schlehuber-Caissier <philipp@lrde.epita.fr>
Date: Tue, 29 Mar 2022 15:51:31 +0200
Subject: [PATCH 13/18] Correct bug in zielonka

Optimization in Zielonka failed
under certain circumstances
todo: Devise a specialized test
for direct attr computation

* spot/twaalgos/game.cc: Correction
* tests/python/game.py: Test
---
 spot/twaalgos/game.cc |  46 ++++++---
 tests/python/game.py  | 212 +++++++++++++++++++++++++++++++++++++++++-
 2 files changed, 246 insertions(+), 12 deletions(-)

diff --git a/spot/twaalgos/game.cc b/spot/twaalgos/game.cc
index 9b8fdcee9..6bb62500d 100644
--- a/spot/twaalgos/game.cc
+++ b/spot/twaalgos/game.cc
@@ -309,16 +309,21 @@ namespace spot
       {
         auto scc_acc = info_->acc_sets_of(c_scc_idx_);
         // We will override all parities of edges leaving the scc
+        // Currently game is colored max odd
+        // So there is at least one color
         bool added[] = {false, false};
         unsigned par_pair[2];
         unsigned scc_new_par = std::max(scc_acc.max_set(), 1u);
+        bool player_color_larger;
         if (scc_new_par&1)
           {
+            player_color_larger = false;
             par_pair[1] = scc_new_par;
             par_pair[0] = scc_new_par+1;
           }
         else
           {
+            player_color_larger = true;
             par_pair[1] = scc_new_par+1;
             par_pair[0] = scc_new_par;
           }
@@ -331,6 +336,7 @@ namespace spot
         for (unsigned v : c_states())
           {
             assert(subgame_[v] == unseen_mark);
+            bool owner = (*owner_ptr_)[v];
             for (auto &e : arena_->out(v))
               {
                 // The outgoing edges are taken finitely often
@@ -342,14 +348,20 @@ namespace spot
                                                e.dst, e.acc);
                     if (w_.winner(e.dst))
                       {
-                        // Winning region of player -> odd
-                        e.acc = odd_mark;
+                        // Winning region off player ->
+                        // odd mark if player
+                        // else 1 (smallest loosing for env)
+                        e.acc = owner ? odd_mark
+                                      : acc_cond::mark_t({1});
                         added[1] = true;
                       }
                     else
                       {
-                        // Winning region of env -> even
-                        e.acc = even_mark;
+                        // Winning region of env ->
+                        // even mark for env,
+                        // else 0 (smallest loosing for player)
+                        e.acc = !owner ? even_mark
+                                       : acc_cond::mark_t({0});
                         added[0] = true;
                       }
                     // Replace with self-loop
@@ -360,13 +372,22 @@ namespace spot
 
         // Compute the attractors of the self-loops/transitions leaving scc
         // These can be directly added to the winning states
-        // Note: attractors can not intersect therefore the order in which
-        // they are computed does not matter
+        // To avoid disregarding edges in attr computation we
+        // need to start with the larger color
+        // Todo come up with a test for this
         unsigned dummy_rd;
 
-        for (bool p : {false, true})
-          if (added[p])
-            attr(dummy_rd, p, par_pair[p], true, par_pair[p]);
+        for (bool p : {player_color_larger,
+                       !player_color_larger})
+          {
+            if (added[p])
+              {
+                // Always take the larger,
+                // Otherwise states with an transition to a winning AND
+                // a loosing scc are treated incorrectly
+                attr(dummy_rd, p, par_pair[p], true, par_pair[p]);
+              }
+          }
 
         if (added[0] || added[1])
           // Fix "negative" strategy
@@ -379,8 +400,11 @@ namespace spot
 
       inline bool
       attr(unsigned &rd, bool p, unsigned max_par,
-           bool acc_par, unsigned min_win_par)
+           bool acc_par, unsigned min_win_par,
+           bool no_check=false)
       {
+        // In fix_scc, the attr computation is
+        // abused so we can not check ertain things
         // Computes the attractor of the winning set of player p within a
         // subgame given as rd.
         // If acc_par is true, max_par transitions are also accepting and
@@ -394,7 +418,7 @@ namespace spot
         // As proposed in Oink! / PGSolver
         // Needs the transposed graph however
 
-        assert((!acc_par) || (acc_par && (max_par&1) == p));
+        assert((no_check || !acc_par) || (acc_par && (max_par&1) == p));
         assert(!acc_par || (0 < min_win_par));
         assert((min_win_par <= max_par) && (max_par <= max_abs_par_));
 
diff --git a/tests/python/game.py b/tests/python/game.py
index 9d77c153d..f45bed532 100644
--- a/tests/python/game.py
+++ b/tests/python/game.py
@@ -1,6 +1,6 @@
 #!/usr/bin/python3
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2020 Laboratoire de Recherche et Développement de
+# Copyright (C) 2020, 2022 Laboratoire de Recherche et Développement de
 # l'EPITA.
 #
 # This file is part of Spot, a model checking library.
@@ -61,3 +61,213 @@ State: 7
 State: 8 {1}
 [0] 2
 --END--"""
+
+# Testing case where parity_game optimization
+# lead to wrong results
+si = spot.synthesis_info()
+
+game = spot.automaton("""HOA: v1
+States: 27
+Start: 7
+AP: 11 "a" "b" "c" "d" "e" "f" "g" "h" "i" "j" "k"
+acc-name: parity max odd 3
+Acceptance: 3 Fin(2) & (Inf(1) | Fin(0))
+properties: trans-labels explicit-labels trans-acc colored
+properties: deterministic
+spot-state-player: 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1
+controllable-AP: 0 1 2 3 4 5 6 7
+--BODY--
+State: 0
+[t] 8 {0}
+State: 1
+[8&9] 8 {0}
+[!8&!10 | !9&!10] 9 {0}
+[!8&10 | !9&10] 10 {0}
+State: 2
+[8&9] 8 {0}
+[!8&!10 | !9&!10] 11 {0}
+[!8&10 | !9&10] 12 {0}
+State: 3
+[8&9] 8 {0}
+[!9&!10] 13 {0}
+[!8&10 | !9&10] 14 {0}
+[!8&9&!10] 15 {0}
+State: 4
+[8&9] 8 {0}
+[!8&!10 | !9&!10] 16 {0}
+[!8&!9&10] 17 {0}
+[!8&9&10] 18 {0}
+[8&!9&10] 19 {0}
+State: 5
+[8&9] 8 {0}
+[!9&!10] 20 {0}
+[!8&10 | !9&10] 21 {0}
+[!8&9&!10] 22 {0}
+State: 6
+[8&9] 8 {0}
+[!8&!10 | !9&!10] 23 {0}
+[!8&!9&10] 24 {0}
+[!8&9&10] 25 {0}
+[8&!9&10] 26 {0}
+State: 7
+[8&9] 8 {0}
+[!9&!10] 13 {0}
+[!8&9&!10] 15 {0}
+[!8&!9&10] 17 {0}
+[!8&9&10] 18 {0}
+[8&!9&10] 19 {0}
+State: 8
+[!0&!1&2&!3&!4&5&!6&7 | !0&!1&2&!3&!4&5&6&!7 | !0&!1&2&!3&4&!5&!6&7 |
+!0&!1&2&!3&4&!5&6&!7 | !0&!1&2&3&!4&!5&!6&7 | !0&!1&2&3&!4&!5&6&!7 |
+!0&1&!2&!3&!4&5&!6&7 | !0&1&!2&!3&!4&5&6&!7 | !0&1&!2&!3&4&!5&!6&7 |
+!0&1&!2&!3&4&!5&6&!7 | !0&1&!2&3&!4&!5&!6&7 | !0&1&!2&3&!4&!5&6&!7 |
+0&!1&!2&!3&!4&5&!6&7 | 0&!1&!2&!3&!4&5&6&!7 | 0&!1&!2&!3&4&!5&!6&7 |
+ 0&!1&!2&!3&4&!5&6&!7 | 0&!1&!2&3&!4&!5&!6&7 | 0&!1&!2&3&!4&!5&6&!7] 0 {1}
+State: 9
+[!0&!1&2&!3&!4&5&!6&7 | !0&!1&2&!3&!4&5&6&!7 | !0&!1&2&!3&4&!5&!6&7 |
+!0&!1&2&!3&4&!5&6&!7 | !0&1&!2&!3&!4&5&!6&7 | !0&1&!2&!3&!4&5&6&!7 |
+!0&1&!2&!3&4&!5&!6&7 | !0&1&!2&!3&4&!5&6&!7 | 0&!1&!2&!3&!4&5&!6&7 |
+0&!1&!2&!3&!4&5&6&!7 | 0&!1&!2&!3&4&!5&!6&7 | 0&!1&!2&!3&4&!5&6&!7] 1 {2}
+[!0&!1&2&3&!4&!5&!6&7 | !0&!1&2&3&!4&!5&6&!7 | !0&1&!2&3&!4&!5&!6&7 |
+!0&1&!2&3&!4&!5&6&!7 | 0&!1&!2&3&!4&!5&!6&7 | 0&!1&!2&3&!4&!5&6&!7] 2 {2}
+State: 10
+[!0&!1&2&!3&!4&5&!6&7 | !0&!1&2&!3&!4&5&6&!7 | !0&!1&2&!3&4&!5&!6&7 |
+!0&!1&2&!3&4&!5&6&!7 | !0&1&!2&!3&!4&5&!6&7 | !0&1&!2&!3&!4&5&6&!7 |
+!0&1&!2&!3&4&!5&!6&7 | !0&1&!2&!3&4&!5&6&!7 | 0&!1&!2&!3&!4&5&!6&7 |
+0&!1&!2&!3&!4&5&6&!7 | 0&!1&!2&!3&4&!5&!6&7 | 0&!1&!2&!3&4&!5&6&!7] 0 {1}
+[!0&!1&2&3&!4&!5&!6&7 | !0&!1&2&3&!4&!5&6&!7 | !0&1&!2&3&!4&!5&!6&7 |
+!0&1&!2&3&!4&!5&6&!7 | 0&!1&!2&3&!4&!5&!6&7 | 0&!1&!2&3&!4&!5&6&!7] 2 {2}
+State: 11
+[!0&!1&2&!3&4&!5&!6&7 | !0&!1&2&!3&4&!5&6&!7 | !0&!1&2&3&!4&!5&!6&7 |
+!0&!1&2&3&!4&!5&6&!7 | !0&1&!2&!3&4&!5&!6&7 | !0&1&!2&!3&4&!5&6&!7 |
+!0&1&!2&3&!4&!5&!6&7 | !0&1&!2&3&!4&!5&6&!7 | 0&!1&!2&!3&4&!5&!6&7 |
+0&!1&!2&!3&4&!5&6&!7 | 0&!1&!2&3&!4&!5&!6&7 | 0&!1&!2&3&!4&!5&6&!7] 0 {1}
+[!0&!1&2&!3&!4&5&!6&7 | !0&!1&2&!3&!4&5&6&!7 | !0&1&!2&!3&!4&5&!6&7 |
+!0&1&!2&!3&!4&5&6&!7 | 0&!1&!2&!3&!4&5&!6&7 | 0&!1&!2&!3&!4&5&6&!7] 1 {2}
+State: 12
+[!0&!1&2&!3&!4&5&!6&7 | !0&!1&2&!3&!4&5&6&!7 | !0&1&!2&!3&!4&5&!6&7 |
+!0&1&!2&!3&!4&5&6&!7 | 0&!1&!2&!3&!4&5&!6&7 | 0&!1&!2&!3&!4&5&6&!7] 1 {2}
+[!0&!1&2&!3&4&!5&!6&7 | !0&!1&2&!3&4&!5&6&!7 | !0&!1&2&3&!4&!5&!6&7 |
+!0&!1&2&3&!4&!5&6&!7 | !0&1&!2&!3&4&!5&!6&7 | !0&1&!2&!3&4&!5&6&!7 |
+!0&1&!2&3&!4&!5&!6&7 | !0&1&!2&3&!4&!5&6&!7 | 0&!1&!2&!3&4&!5&!6&7 |
+0&!1&!2&!3&4&!5&6&!7 | 0&!1&!2&3&!4&!5&!6&7 | 0&!1&!2&3&!4&!5&6&!7] 2 {2}
+State: 13
+[!0&!1&2&!3&!4&5&6&!7 | !0&!1&2&!3&4&!5&6&!7 | !0&1&!2&!3&!4&5&!6&7 |
+!0&1&!2&!3&!4&5&6&!7 | !0&1&!2&!3&4&!5&!6&7 | !0&1&!2&!3&4&!5&6&!7 |
+0&!1&!2&!3&!4&5&!6&7 | 0&!1&!2&!3&!4&5&6&!7 | 0&!1&!2&!3&4&!5&!6&7 |
+0&!1&!2&!3&4&!5&6&!7] 1 {1}
+[!0&!1&2&3&!4&!5&6&!7 | !0&1&!2&3&!4&!5&!6&7 | !0&1&!2&3&!4&!5&6&!7 |
+0&!1&!2&3&!4&!5&!6&7 | 0&!1&!2&3&!4&!5&6&!7] 2 {1}
+[!0&!1&2&!3&!4&5&!6&7 | !0&!1&2&!3&4&!5&!6&7] 3 {1}
+[!0&!1&2&3&!4&!5&!6&7] 5 {1}
+State: 14
+[!0&!1&2&!3&!4&5&!6&7 | !0&!1&2&!3&!4&5&6&!7 | !0&!1&2&!3&4&!5&!6&7 |
+!0&!1&2&!3&4&!5&6&!7 | !0&1&!2&!3&!4&5&!6&7 | !0&1&!2&!3&!4&5&6&!7 |
+!0&1&!2&!3&4&!5&!6&7 | !0&1&!2&!3&4&!5&6&!7 | 0&!1&!2&!3&!4&5&!6&7 |
+0&!1&!2&!3&!4&5&6&!7 | 0&!1&!2&!3&4&!5&!6&7 | 0&!1&!2&!3&4&!5&6&!7] 0 {1}
+[!0&!1&2&3&!4&!5&!6&7 | !0&!1&2&3&!4&!5&6&!7 | !0&1&!2&3&!4&!5&!6&7 |
+!0&1&!2&3&!4&!5&6&!7 | 0&!1&!2&3&!4&!5&!6&7 | 0&!1&!2&3&!4&!5&6&!7] 2 {1}
+State: 15
+[!0&!1&2&!3&!4&5&6&!7 | !0&!1&2&!3&4&!5&6&!7 | !0&1&!2&!3&!4&5&!6&7 |
+!0&1&!2&!3&!4&5&6&!7 | !0&1&!2&!3&4&!5&!6&7 | !0&1&!2&!3&4&!5&6&!7 |
+0&!1&!2&!3&!4&5&!6&7 | 0&!1&!2&!3&!4&5&6&!7 | 0&!1&!2&!3&4&!5&!6&7 |
+0&!1&!2&!3&4&!5&6&!7] 1 {1}
+[!0&!1&2&3&!4&!5&6&!7 | !0&1&!2&3&!4&!5&!6&7 | !0&1&!2&3&!4&!5&6&!7 |
+0&!1&!2&3&!4&!5&!6&7 | 0&!1&!2&3&!4&!5&6&!7] 2 {1}
+[!0&!1&2&!3&!4&5&!6&7 | !0&!1&2&!3&4&!5&!6&7] 4 {1}
+[!0&!1&2&3&!4&!5&!6&7] 6 {1}
+State: 16
+[!0&!1&2&!3&!4&5&!6&7 | !0&!1&2&!3&!4&5&6&!7 | !0&!1&2&!3&4&!5&!6&7 |
+!0&!1&2&!3&4&!5&6&!7 | !0&1&!2&!3&!4&5&!6&7 | !0&1&!2&!3&!4&5&6&!7 |
+!0&1&!2&!3&4&!5&!6&7 | !0&1&!2&!3&4&!5&6&!7 | 0&!1&!2&!3&!4&5&!6&7 |
+0&!1&!2&!3&!4&5&6&!7 | 0&!1&!2&!3&4&!5&!6&7 | 0&!1&!2&!3&4&!5&6&!7] 1 {1}
+[!0&!1&2&3&!4&!5&!6&7 | !0&!1&2&3&!4&!5&6&!7 | !0&1&!2&3&!4&!5&!6&7 |
+!0&1&!2&3&!4&!5&6&!7 | 0&!1&!2&3&!4&!5&!6&7 | 0&!1&!2&3&!4&!5&6&!7] 2 {1}
+State: 17
+[!0&!1&2&!3&!4&5&!6&7 | !0&!1&2&!3&!4&5&6&!7 | !0&!1&2&!3&4&!5&!6&7 |
+!0&!1&2&!3&4&!5&6&!7 | !0&1&!2&!3&!4&5&!6&7 | !0&1&!2&!3&!4&5&6&!7 |
+!0&1&!2&!3&4&!5&!6&7 | !0&1&!2&!3&4&!5&6&!7 | 0&!1&!2&!3&!4&5&!6&7 |
+0&!1&!2&!3&!4&5&6&!7 | 0&!1&!2&!3&4&!5&!6&7 | 0&!1&!2&!3&4&!5&6&!7] 0 {1}
+[!0&!1&2&3&!4&!5&!6&7 | !0&!1&2&3&!4&!5&6&!7 | !0&1&!2&3&!4&!5&6&!7 |
+0&!1&!2&3&!4&!5&!6&7 | 0&!1&!2&3&!4&!5&6&!7] 2 {1}
+[!0&1&!2&3&!4&!5&!6&7] 6 {1}
+State: 18
+[!0&!1&2&!3&!4&5&!6&7 | !0&!1&2&!3&!4&5&6&!7 | !0&!1&2&!3&4&!5&!6&7 |
+!0&!1&2&!3&4&!5&6&!7 | !0&1&!2&!3&!4&5&!6&7 | !0&1&!2&!3&!4&5&6&!7 |
+!0&1&!2&!3&4&!5&!6&7 | !0&1&!2&!3&4&!5&6&!7 | 0&!1&!2&!3&!4&5&!6&7 |
+0&!1&!2&!3&!4&5&6&!7 | 0&!1&!2&!3&4&!5&!6&7 | 0&!1&!2&!3&4&!5&6&!7] 0 {1}
+[!0&!1&2&3&!4&!5&!6&7 | !0&!1&2&3&!4&!5&6&!7 | !0&1&!2&3&!4&!5&6&!7 |
+0&!1&!2&3&!4&!5&!6&7 | 0&!1&!2&3&!4&!5&6&!7] 2 {1}
+[!0&1&!2&3&!4&!5&!6&7] 5 {1}
+State: 19
+[!0&!1&2&!3&!4&5&!6&7 | !0&!1&2&!3&!4&5&6&!7 | !0&!1&2&!3&4&!5&!6&7 |
+!0&!1&2&!3&4&!5&6&!7 | !0&1&!2&!3&!4&5&!6&7 | !0&1&!2&!3&!4&5&6&!7 |
+!0&1&!2&!3&4&!5&!6&7 | !0&1&!2&!3&4&!5&6&!7 | 0&!1&!2&!3&!4&5&!6&7 |
+0&!1&!2&!3&!4&5&6&!7 | 0&!1&!2&!3&4&!5&!6&7 | 0&!1&!2&!3&4&!5&6&!7] 0 {1}
+[!0&!1&2&3&!4&!5&!6&7 | !0&!1&2&3&!4&!5&6&!7 | !0&1&!2&3&!4&!5&!6&7 |
+0&!1&!2&3&!4&!5&!6&7 | 0&!1&!2&3&!4&!5&6&!7] 2 {1}
+[!0&1&!2&3&!4&!5&6&!7] 6 {1}
+State: 20
+[!0&!1&2&!3&4&!5&!6&7 | !0&!1&2&!3&4&!5&6&!7 | !0&!1&2&3&!4&!5&!6&7 |
+!0&!1&2&3&!4&!5&6&!7 | !0&1&!2&!3&4&!5&!6&7 | !0&1&!2&!3&4&!5&6&!7 |
+!0&1&!2&3&!4&!5&!6&7 | !0&1&!2&3&!4&!5&6&!7 | 0&!1&!2&!3&4&!5&!6&7 |
+0&!1&!2&!3&4&!5&6&!7 | 0&!1&!2&3&!4&!5&!6&7 | 0&!1&!2&3&!4&!5&6&!7] 0 {1}
+[!0&!1&2&!3&!4&5&6&!7 | !0&1&!2&!3&!4&5&!6&7 | !0&1&!2&!3&!4&5&6&!7 |
+0&!1&!2&!3&!4&5&!6&7 | 0&!1&!2&!3&!4&5&6&!7] 1 {1}
+[!0&!1&2&!3&!4&5&!6&7] 3 {1}
+State: 21
+[!0&!1&2&!3&!4&5&!6&7 | !0&!1&2&!3&!4&5&6&!7 | !0&1&!2&!3&!4&5&!6&7 |
+!0&1&!2&!3&!4&5&6&!7 | 0&!1&!2&!3&!4&5&!6&7 | 0&!1&!2&!3&!4&5&6&!7] 1 {1}
+[!0&!1&2&!3&4&!5&!6&7 | !0&!1&2&!3&4&!5&6&!7 | !0&!1&2&3&!4&!5&!6&7 |
+!0&!1&2&3&!4&!5&6&!7 | !0&1&!2&!3&4&!5&!6&7 | !0&1&!2&!3&4&!5&6&!7 |
+!0&1&!2&3&!4&!5&!6&7 | !0&1&!2&3&!4&!5&6&!7 | 0&!1&!2&!3&4&!5&!6&7 |
+0&!1&!2&!3&4&!5&6&!7 | 0&!1&!2&3&!4&!5&!6&7 | 0&!1&!2&3&!4&!5&6&!7] 2 {1}
+State: 22
+[!0&!1&2&!3&4&!5&!6&7 | !0&!1&2&!3&4&!5&6&!7 | !0&!1&2&3&!4&!5&!6&7 |
+!0&!1&2&3&!4&!5&6&!7 | !0&1&!2&!3&4&!5&!6&7 | !0&1&!2&!3&4&!5&6&!7 |
+!0&1&!2&3&!4&!5&!6&7 | !0&1&!2&3&!4&!5&6&!7 | 0&!1&!2&!3&4&!5&!6&7 |
+0&!1&!2&!3&4&!5&6&!7 | 0&!1&!2&3&!4&!5&!6&7 | 0&!1&!2&3&!4&!5&6&!7] 0 {1}
+[!0&!1&2&!3&!4&5&6&!7 | !0&1&!2&!3&!4&5&!6&7 | !0&1&!2&!3&!4&5&6&!7 |
+0&!1&!2&!3&!4&5&!6&7 | 0&!1&!2&!3&!4&5&6&!7] 1 {1}
+[!0&!1&2&!3&!4&5&!6&7] 4 {1}
+State: 23
+[!0&!1&2&!3&4&!5&!6&7 | !0&!1&2&!3&4&!5&6&!7 | !0&!1&2&3&!4&!5&!6&7 |
+!0&!1&2&3&!4&!5&6&!7 | !0&1&!2&!3&4&!5&!6&7 | !0&1&!2&!3&4&!5&6&!7 |
+!0&1&!2&3&!4&!5&!6&7 | !0&1&!2&3&!4&!5&6&!7 | 0&!1&!2&!3&4&!5&!6&7 |
+0&!1&!2&!3&4&!5&6&!7 | 0&!1&!2&3&!4&!5&!6&7 | 0&!1&!2&3&!4&!5&6&!7] 0 {1}
+[!0&!1&2&!3&!4&5&!6&7 | !0&!1&2&!3&!4&5&6&!7 | !0&1&!2&!3&!4&5&!6&7 |
+!0&1&!2&!3&!4&5&6&!7 | 0&!1&!2&!3&!4&5&!6&7 | 0&!1&!2&!3&!4&5&6&!7] 1 {1}
+State: 24
+[!0&!1&2&!3&!4&5&!6&7 | !0&!1&2&!3&!4&5&6&!7 | !0&1&!2&!3&!4&5&6&!7 |
+0&!1&!2&!3&!4&5&!6&7 | 0&!1&!2&!3&!4&5&6&!7] 1 {1}
+[!0&!1&2&!3&4&!5&!6&7 | !0&!1&2&!3&4&!5&6&!7 | !0&!1&2&3&!4&!5&!6&7 |
+!0&!1&2&3&!4&!5&6&!7 | !0&1&!2&!3&4&!5&6&!7 | !0&1&!2&3&!4&!5&6&!7 |
+0&!1&!2&!3&4&!5&!6&7 | 0&!1&!2&!3&4&!5&6&!7 | 0&!1&!2&3&!4&!5&!6&7 |
+0&!1&!2&3&!4&!5&6&!7] 2 {1}
+[!0&1&!2&!3&!4&5&!6&7] 4 {1}
+[!0&1&!2&!3&4&!5&!6&7 | !0&1&!2&3&!4&!5&!6&7] 6 {1}
+State: 25
+[!0&!1&2&!3&!4&5&!6&7 | !0&!1&2&!3&!4&5&6&!7 | !0&1&!2&!3&!4&5&6&!7 |
+0&!1&!2&!3&!4&5&!6&7 | 0&!1&!2&!3&!4&5&6&!7] 1 {1}
+[!0&!1&2&!3&4&!5&!6&7 | !0&!1&2&!3&4&!5&6&!7 | !0&!1&2&3&!4&!5&!6&7 |
+!0&!1&2&3&!4&!5&6&!7 | !0&1&!2&!3&4&!5&6&!7 | !0&1&!2&3&!4&!5&6&!7 |
+0&!1&!2&!3&4&!5&!6&7 | 0&!1&!2&!3&4&!5&6&!7 | 0&!1&!2&3&!4&!5&!6&7 |
+0&!1&!2&3&!4&!5&6&!7] 2 {1}
+[!0&1&!2&!3&!4&5&!6&7] 3 {1}
+[!0&1&!2&!3&4&!5&!6&7 | !0&1&!2&3&!4&!5&!6&7] 5 {1}
+State: 26
+[!0&!1&2&!3&!4&5&!6&7 | !0&!1&2&!3&!4&5&6&!7 | !0&1&!2&!3&!4&5&!6&7 |
+0&!1&!2&!3&!4&5&!6&7 | 0&!1&!2&!3&!4&5&6&!7] 1 {1}
+[!0&!1&2&!3&4&!5&!6&7 | !0&!1&2&!3&4&!5&6&!7 | !0&!1&2&3&!4&!5&!6&7 |
+!0&!1&2&3&!4&!5&6&!7 | !0&1&!2&!3&4&!5&!6&7 | !0&1&!2&3&!4&!5&!6&7 |
+0&!1&!2&!3&4&!5&!6&7 | 0&!1&!2&!3&4&!5&6&!7 | 0&!1&!2&3&!4&!5&!6&7 |
+0&!1&!2&3&!4&!5&6&!7] 2 {1}
+[!0&1&!2&!3&!4&5&6&!7] 4 {1}
+[!0&1&!2&!3&4&!5&6&!7 | !0&1&!2&3&!4&!5&6&!7] 6 {1}
+--END--""")
+
+assert spot.solve_game(game, si)
+
+games = spot.split_edges(game)
+spot.set_state_players(games, spot.get_state_players(game))
+assert spot.solve_game(games, si)

From fa6912a5745ed02f883fba03406949080a5a997b Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 29 Mar 2022 11:13:19 +0200
Subject: [PATCH 14/18] debian: simplify LTO configuration to work around newer
 libtool

Libtool 2.4.7 breaks if AR_FLAGS contains a space. See
https://lists.gnu.org/archive/html/bug-libtool/2022-03/msg00009.html

* debian/rules: Use gcc-{nm,ar,ranlib} so we do not have to pass
the plugin explicitly.
---
 debian/rules | 22 +++++++++-------------
 1 file changed, 9 insertions(+), 13 deletions(-)

diff --git a/debian/rules b/debian/rules
index 0193e9a62..51daf21ed 100755
--- a/debian/rules
+++ b/debian/rules
@@ -20,20 +20,16 @@ include /usr/share/dpkg/default.mk
 %:
 	dh $@ --with=python3
 
-# Find the LTO plugin, which we need to pass to ar, nm, and ranlib.
-LTOPLUG := $(shell gcc -v 2>&1 | \
-  sed -n 's:COLLECT_LTO_WRAPPER=\(/.*/\)[^/]*:\1:p')liblto_plugin.so
-
 # ARFLAGS is for Automake
-# AR_FLAGS is for Libtool
-# These activate the LTO pluggin, but also remove the 'u' option
-# from ar, since its now ignored with Debian's default to 'D'.
-LTOSETUP =					    \
-  LDFLAGS='-fuse-linker-plugin'			    \
-  NM='nm --plugin $(LTOPLUG)'			    \
-  ARFLAGS='cr --plugin $(LTOPLUG)'		    \
-  AR_FLAGS='cr --plugin $(LTOPLUG)'		    \
-  RANLIB='ranlib --plugin $(LTOPLUG)'		    \
+# AR_FLAGS is for Libtool, (but libtool 2.4.7 will now use ARFLAGS as well)
+# The gcc-tools activate the LTO plugin.
+LTOSETUP =					\
+  LDFLAGS='-fuse-linker-plugin'			\
+  NM='gcc-nm'					\
+  AR='gcc-ar'					\
+  ARFLAGS='cr'					\
+  AR_FLAGS='cr'					\
+  RANLIB='gcc-ranlib'				\
   VALGRIND=false
 GCDADIR := $(shell pwd)/gcda
 

From 0f3ffd59cec1f152733c07458078f8a21ca1edc8 Mon Sep 17 00:00:00 2001
From: Florian Renkin <frenkin@lrde.epita.fr>
Date: Tue, 12 Apr 2022 11:21:14 +0200
Subject: [PATCH 15/18] ltlsynt: don't solve games when we want to display them

* bin/ltlsynt.cc: here
---
 bin/ltlsynt.cc | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc
index f5b2ade51..5ffa22f39 100644
--- a/bin/ltlsynt.cc
+++ b/bin/ltlsynt.cc
@@ -395,6 +395,8 @@ namespace
                      && "Env needs first turn");
             }
           print_game(arena);
+          if (want_game)
+            continue;
           if (!spot::solve_game(arena, *gi))
             {
               std::cout << "UNREALIZABLE" << std::endl;

From 385da8ebd0c8ec01c3e69c76830a7a1462996c74 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 2 May 2022 17:47:53 +0200
Subject: [PATCH 16/18] update NEWS for upcoming release

* NEWS: Here.
---
 NEWS | 19 ++++++++++++++++---
 1 file changed, 16 insertions(+), 3 deletions(-)

diff --git a/NEWS b/NEWS
index 301711588..f857fb97d 100644
--- a/NEWS
+++ b/NEWS
@@ -1,13 +1,20 @@
 New in spot 2.10.4.dev  (net yet released)
 
-  Nothing yet.
-
   Bugs fixed:
 
   - reduce_parity() produced incorrect results when applied to
     automata with deleted edges.
 
-  - work around a portability issue in Flex 2.6.4 preventing
+  - An optimization of Zielonka could result in incorrect results
+    in some cases.
+
+  - ltlsynt --print-pg incorrectly solved the game in addition to
+    printing it.
+
+  - ltlsynt would fail if only one of --ins or --outs was set, and
+    if it was set empty.
+
+  - Work around a portability issue in Flex 2.6.4 preventing
     compilation on OpenBSD.
 
   - Do not use the seq command in test cases, it is not available
@@ -16,6 +23,12 @@ New in spot 2.10.4.dev  (net yet released)
   - Do not erase the previous contents of the PYTHONPATH environment
     variable when running tests, prepend to it instead.
 
+  - Simplify Debian instructions for LTO build to work around newer
+    libtool version.
+
+  - Fix invalid read in digraph::sort_edges_of_(), currently unused in
+    Spot.
+
 New in spot 2.10.4  (2022-02-01)
 
   Bug fixed:

From c70a06ae0adbd16ca9f16f67b6892f7e4306a2e8 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 3 May 2022 08:59:17 +0200
Subject: [PATCH 17/18] Release Spot 2.10.5

* NEWS, configure.ac, doc/org/setup.org: Update.
---
 NEWS              |  2 +-
 configure.ac      |  2 +-
 doc/org/setup.org | 10 +++++-----
 3 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/NEWS b/NEWS
index f857fb97d..8f512fcb7 100644
--- a/NEWS
+++ b/NEWS
@@ -1,4 +1,4 @@
-New in spot 2.10.4.dev  (net yet released)
+New in spot 2.10.5  (2022-05-03)
 
   Bugs fixed:
 
diff --git a/configure.ac b/configure.ac
index 31002ccda..5815a2c13 100644
--- a/configure.ac
+++ b/configure.ac
@@ -21,7 +21,7 @@
 # along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 AC_PREREQ([2.69])
-AC_INIT([spot], [2.10.4.dev], [spot@lrde.epita.fr])
+AC_INIT([spot], [2.10.5], [spot@lrde.epita.fr])
 AC_CONFIG_AUX_DIR([tools])
 AC_CONFIG_MACRO_DIR([m4])
 AM_INIT_AUTOMAKE([1.11 gnu tar-ustar color-tests parallel-tests])
diff --git a/doc/org/setup.org b/doc/org/setup.org
index 3b8b1b404..c1b7e9235 100644
--- a/doc/org/setup.org
+++ b/doc/org/setup.org
@@ -1,11 +1,11 @@
 #+OPTIONS: H:2 num:nil toc:t html-postamble:nil ^:nil
 #+EMAIL: spot@lrde.epita.fr
 #+HTML_LINK_HOME: index.html
-#+MACRO: SPOTVERSION 2.10.4
-#+MACRO: LASTRELEASE 2.10.4
-#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.10.4.tar.gz][=spot-2.10.4.tar.gz=]]
-#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-10-4/NEWS][summary of the changes]]
-#+MACRO: LASTDATE 2022-02-01
+#+MACRO: SPOTVERSION 2.10.5
+#+MACRO: LASTRELEASE 2.10.5
+#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.10.5.tar.gz][=spot-2.10.5.tar.gz=]]
+#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-10-5/NEWS][summary of the changes]]
+#+MACRO: LASTDATE 2022-05-03
 
 #+ATTR_HTML: :id spotlogo
 [[file:spot2.svg]]

From 56666e0db592c3528ddf015f783a81bf77f74fb2 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 3 May 2022 09:01:03 +0200
Subject: [PATCH 18/18] * NEWS, configure.ac: Bump version to 2.10.5.dev.

---
 NEWS         | 4 ++++
 configure.ac | 2 +-
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/NEWS b/NEWS
index 8f512fcb7..031df5b71 100644
--- a/NEWS
+++ b/NEWS
@@ -1,3 +1,7 @@
+New in spot 2.10.5.dev  (not yet released)
+
+  Nothing yet.
+
 New in spot 2.10.5  (2022-05-03)
 
   Bugs fixed:
diff --git a/configure.ac b/configure.ac
index 5815a2c13..6527900ce 100644
--- a/configure.ac
+++ b/configure.ac
@@ -21,7 +21,7 @@
 # along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 AC_PREREQ([2.69])
-AC_INIT([spot], [2.10.5], [spot@lrde.epita.fr])
+AC_INIT([spot], [2.10.5.dev], [spot@lrde.epita.fr])
 AC_CONFIG_AUX_DIR([tools])
 AC_CONFIG_MACRO_DIR([m4])
 AM_INIT_AUTOMAKE([1.11 gnu tar-ustar color-tests parallel-tests])