From 2c267cac4048a5e6d54321883fe6b50868c1c834 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 22 Jul 2020 16:23:34 +0200
Subject: [PATCH 01/17] simplify: fix handling of keep_top_xor

Under that option, !(a ^ b) was converted
to (!a <=> !b) instead of simply (a <=> b).

* spot/tl/simplify.cc (equiv_or_xor): Improve
rewriting.
* tests/core/ltl2tgba2.test, tests/python/simstate.py: Adjust test
cases.
---
 NEWS                      |  9 ++++++---
 spot/tl/simplify.cc       | 16 ++++++++--------
 tests/core/ltl2tgba2.test |  4 ++--
 tests/python/simstate.py  |  6 +++---
 4 files changed, 19 insertions(+), 16 deletions(-)

diff --git a/NEWS b/NEWS
index 2fa5dcaa6..82a4901f6 100644
--- a/NEWS
+++ b/NEWS
@@ -1,19 +1,22 @@
 New in spot 2.9.3.dev  (not yet released)
 
-  Nothing yet.
+  Bugs fixed:
+
+  - Handle xor and <-> in a more natural way when translating
+    LTL formulas to generic acceptancee conditions.
 
 New in spot 2.9.3 (2020-07-22)
 
   Bug fixed:
 
-  - Completely fix the ltlcross issue mentionned in previous release.
+  - Completely fix the ltlcross issue mentioned in previous release.
 
 New in spot 2.9.2 (2020-07-21)
 
   Bugs fixed:
 
   - ltlcross --csv=... --product=N with N>0 could output spurious
-    diagnosics claiming that words were rejected when evaluating
+    diagnostics claiming that words were rejected when evaluating
     the automaton on state-space.
 
   - spot::scc_info::determine_unknown_acceptance() now also update the
diff --git a/spot/tl/simplify.cc b/spot/tl/simplify.cc
index 24f94d5eb..2848c3e9e 100644
--- a/spot/tl/simplify.cc
+++ b/spot/tl/simplify.cc
@@ -431,12 +431,12 @@ namespace spot
       if (equiv)
         {
           // Rewrite a<=>b as (a&b)|(!a&!b)
-          auto recurse_f1_true = rec(f1, true);
-          auto recurse_f2_true = rec(f2, true);
-          if (!deep && c->options.keep_top_xor)
-            return formula::Equiv(recurse_f1_true, recurse_f2_true);
           auto recurse_f1_false = rec(f1, false);
           auto recurse_f2_false = rec(f2, false);
+          if (!deep && c->options.keep_top_xor)
+            return formula::Equiv(recurse_f1_false, recurse_f2_false);
+          auto recurse_f1_true = rec(f1, true);
+          auto recurse_f2_true = rec(f2, true);
           auto left = formula::And({recurse_f1_false, recurse_f2_false});
           auto right = formula::And({recurse_f1_true, recurse_f2_true});
           return formula::Or({left, right});
@@ -444,12 +444,12 @@ namespace spot
       else
         {
           // Rewrite a^b as (a&!b)|(!a&b)
-          auto recurse_f1_true = rec(f1, true);
-          auto recurse_f2_true = rec(f2, true);
-          if (!deep && c->options.keep_top_xor)
-            return formula::Xor(recurse_f1_true, recurse_f2_true);
           auto recurse_f1_false = rec(f1, false);
           auto recurse_f2_false = rec(f2, false);
+          if (!deep && c->options.keep_top_xor)
+            return formula::Xor(recurse_f1_false, recurse_f2_false);
+          auto recurse_f1_true = rec(f1, true);
+          auto recurse_f2_true = rec(f2, true);
           auto left = formula::And({recurse_f1_false, recurse_f2_true});
           auto right = formula::And({recurse_f1_true, recurse_f2_false});
           return formula::Or({left, right});
diff --git a/tests/core/ltl2tgba2.test b/tests/core/ltl2tgba2.test
index 22c7c215c..1878e3efd 100755
--- a/tests/core/ltl2tgba2.test
+++ b/tests/core/ltl2tgba2.test
@@ -453,9 +453,9 @@ test 1,3,2 = `ltl2tgba -G -D "(GFp0 | FGp1)" --stats=%s,%e,%a`
 
 # Handling of Xor and <-> by ltl-split and -D -G.
 res=`ltl2tgba -D -G 'X((Fa & Fb & Fc & Fd) <-> GFe)' --stats='%s %g'`
-test "$res" = "17 (Inf(0) & Fin(1)) | (Fin(0) & Inf(1))"
-res=`ltl2tgba -D -G 'X((Fa & Fb & Fc & Fd) ^ GFe)' --stats='%s %g'`
 test "$res" = "17 (Inf(0)&Inf(1)) | (Fin(0) & Fin(1))"
+res=`ltl2tgba -D -G 'X((Fa & Fb & Fc & Fd) ^ GFe)' --stats='%s %g'`
+test "$res" = "17 (Inf(0) & Fin(1)) | (Fin(0) & Inf(1))"
 ltlcross 'ltl2tgba -D -G' 'ltl2tgba -G' -f '(Fa & Fb & Fc & Fd) ^ GFe'
 
 f='G(p1 | G!p0) M Xp1'
diff --git a/tests/python/simstate.py b/tests/python/simstate.py
index 1be3d9a94..8e5e1c712 100644
--- a/tests/python/simstate.py
+++ b/tests/python/simstate.py
@@ -178,13 +178,13 @@ b.copy_state_names_from(a)
 assert b.to_str() == """HOA: v1
 States: 1
 Start: 0
-AP: 2 "p1" "p0"
+AP: 2 "p0" "p1"
 acc-name: Buchi
 Acceptance: 1 Inf(0)
 properties: trans-labels explicit-labels trans-acc complete
 properties: deterministic stutter-invariant
 --BODY--
 State: 0 "[1,7]"
-[!0] 0 {0}
-[0] 0
+[!1] 0 {0}
+[1] 0
 --END--"""

From 50a33cbc8c5b30f3354a3857b213f0fe76cd2c67 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 23 Jul 2020 15:46:21 +0200
Subject: [PATCH 02/17] org: fix shadow of hierarchy figure

* doc/org/hierarchy.tex: Draw the shadow manually, so that it is part
of the bounding box when we extract the SVG.
---
 doc/org/hierarchy.tex | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

diff --git a/doc/org/hierarchy.tex b/doc/org/hierarchy.tex
index 71607fea4..fd9b430cf 100644
--- a/doc/org/hierarchy.tex
+++ b/doc/org/hierarchy.tex
@@ -1,16 +1,16 @@
 \documentclass{standalone}
 \usepackage{tikz}
-\usetikzlibrary{shadows}
 \def\F{\mathsf{F}} % in future
 \def\G{\mathsf{G}} % globally
-
-\begin{document}
-
 \def\mycyan{cyan!30}
 \def\mypink{magenta!30}
+\begin{document}
+\noindent
 \scalebox{1.2}{
- \begin{tikzpicture}[scale=.9]
-    \draw[drop shadow,fill=white] (0,0) rectangle (6,7);
+  \begin{tikzpicture}[scale=.9]
+    %Let's draw the shadow ourselves, so that it is included in the bounding box
+    \path[fill=black!50,opacity=.5,xshift=.5ex,yshift=-.5ex] (0,0) rectangle (6,7);
+    \draw[fill=white] (0,0) rectangle (6,7);
 
     \path[fill=\mycyan,fill opacity=.4] (0,6.5) -- (6,3) -- (6,0) -- (0,0);
     \path[fill=\mycyan,fill opacity=.5] (0,3) -- (4.5,0) -- (0,0);
@@ -37,7 +37,8 @@
     \node[above,red] at (saf.north) {\tt S};
     \node[above,red] at (gua.north) {\tt G};
     \node[above,red] at (3,0.3) {\tt B};
-  \end{tikzpicture}}
+  \end{tikzpicture}
+}
 \end{document}
 %%% Local Variables:
 %%% mode: latex

From 94eca2ca7dc24f80790772f1c344d866fd0c9cca Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 24 Jul 2020 15:39:24 +0200
Subject: [PATCH 03/17] * spot/twaalgos/toparity.hh: Improve documentation.

---
 spot/twaalgos/toparity.hh | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/spot/twaalgos/toparity.hh b/spot/twaalgos/toparity.hh
index a97fda0e6..3c935f095 100644
--- a/spot/twaalgos/toparity.hh
+++ b/spot/twaalgos/toparity.hh
@@ -90,8 +90,9 @@ namespace spot
   /// \brief Take an automaton with any acceptance condition and return an
   /// equivalent parity automaton.
   ///
-  /// The parity condition of the returned automaton is either max even or
-  /// max odd.
+  /// If the input is already a parity automaton of any kind, it is
+  /// returned unchanged.  Otherwise a new parity automaton with max
+  /// odd or max even condition is created.
   ///
   /// This procedure combines many strategies in an attempt to produce
   /// the smallest possible parity automaton.  Some of the strategies

From 1a7f471a028649c49ac893b92a156760f8dad128 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 27 Jul 2020 10:26:17 +0200
Subject: [PATCH 04/17] * tests/python/ipnbdoctest.py: Ignore matplotlib font
 cache messages.

---
 tests/python/ipnbdoctest.py | 30 +++++++++++++++++++++++-------
 1 file changed, 23 insertions(+), 7 deletions(-)

diff --git a/tests/python/ipnbdoctest.py b/tests/python/ipnbdoctest.py
index 5d7d00d10..cdf4a4407 100755
--- a/tests/python/ipnbdoctest.py
+++ b/tests/python/ipnbdoctest.py
@@ -180,21 +180,41 @@ def canonical_dict(dict, ignores):
     return dict
 
 
+def keep_dict(dict):
+    # pandas imports Matplotlib, which can display a message about building the
+    # the font cache if it does not exist, and if doing so takes more than 5
+    # seconds.   Just ignore those.
+    if ('name' in dict and dict['name'] == 'stderr' and
+        type(dict['text']) is str and
+        dict['text'].startswith("Matplotlib is building the font cache")):
+        return False
+    return True
+
+
 def compare_outputs(ref, test, ignores=[]):
     '''Check that two lists of outputs are equivalent and report the
     result.'''
 
+    cref = [canonical_dict(d, ignores) for d in ref if keep_dict(d)]
+    ctest = [canonical_dict(d, ignores) for d in test if keep_dict(d)]
+
+    ok = True
+
+    if len(cref) != len(ctest):
+        print("output length mismatch (expected {}, got {})".format(
+            len(cref), len(ctest)))
+        ok = False
     # There can be several outputs.  For instance wnen the cell both
     # prints a result (goes to "stdout") and displays an automaton
     # (goes to "data").
-    exp = pprint.pformat([canonical_dict(d, ignores) for d in ref],  width=132)
-    eff = pprint.pformat([canonical_dict(d, ignores) for d in test], width=132)
+    exp = pprint.pformat(cref, width=132)
+    eff = pprint.pformat(ctest, width=132)
     if exp[:-1] != '\n':
         exp += '\n'
     if eff[:-1] != '\n':
         eff += '\n'
     if exp == eff:
-        return True
+        return ok
     else:
         print(''.join(diff(exp.splitlines(1), eff.splitlines(1),
                            fromfile='expected', tofile='effective')))
@@ -296,10 +316,6 @@ def test_notebook(ipynb):
             continue
 
         failed = False
-        if len(outs) != len(cell.outputs):
-            print("output length mismatch (expected {}, got {})".format(
-                  len(cell.outputs), len(outs)))
-            failed = True
         if not compare_outputs(cell.outputs, outs):
             failed = True
         print("cell %d: " % i, end="")

From b013077af3d583b9421e1c6e26bac9bfe4794fe6 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 27 Jul 2020 17:05:58 +0200
Subject: [PATCH 05/17] doc: improve css

* doc/org/spot.css: Display input and output closer and separate them
with dash.
---
 doc/org/spot.css | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/doc/org/spot.css b/doc/org/spot.css
index c6c5e813e..b4ab9c1e5 100644
--- a/doc/org/spot.css
+++ b/doc/org/spot.css
@@ -16,9 +16,12 @@ body a{color:#008181}
 .outline-2 h2{border-bottom-style:solid;border-color:#ffe35e}
 .outline-3 h3{position:relative;z-index:1}
 .outline-3 h3:before{content:"";position:absolute;z-index:-1;left:-.2em;bottom:-.05em;height:1.2em;width:1.2em;background-color:#ffe35e;border-radius:5px}
-pre.src{padding-top:8px;border-left-style:solid;border-color:#00adad;overflow:auto}
-pre.src-hoa{padding-top:8px;border-left-style:solid;border-color:#d70079;overflow:auto}
-pre.example{border-left-style:solid;border-color:#d70079}
+pre.src{padding-top:8px;border-left-style:solid;border-color:#00adad;overflow:auto;margin-top:0;margin-bottom:0}
+pre.src-hoa{border-color:#d70079}
+pre.example{border-left-style:solid;border-color:#d70079;margin-top:0;margin-bottom:0;position:relative;z-index:2}
+div.org-src-container+pre.example{border-top-width:1px;border-top-color:#ddd;border-top-style:dashed}
+div.org-src-container+div.org-src-container pre.src{border-top-width:1px;border-top-color:#ddd;border-top-style:dashed}
+div.org-src-container {margin-top:0;margin-bottom:0;position:relative;z-index:1}
 pre.src-text{border-left-style:solid;border-color:#d70079}
 pre.src:before{border:none;border-bottom-style:solid;border-color:#00adad;top:0px;}
 pre.src-python:before{content:'Python'}
@@ -40,6 +43,8 @@ table.csv-table th div span{text-align:left;writing-mode:vertical-lr;transform:r
 #table-of-contents{border:1px solid #ffd300}
 #org-div-home-and-up{visibility:hidden}
 #spotlogo{width:2cm;position:absolute;top:0px;left:0px;z-index:-1}
+pre.src{word-wrap:break-word;white-space:pre-wrap}
+pre.example{word-wrap:break-word;white-space:pre-wrap}
 }
 thead tr{background:#ffe35e}
 #content tbody:nth-child(odd) tr:nth-child(even){background:#fff0a6}

From c49506eea7f68e235daa802d7cbcce149cd4354b Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 27 Jul 2020 21:47:28 +0200
Subject: [PATCH 06/17] * debian/copyright: Replace MIT by Expat.

---
 debian/copyright | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/debian/copyright b/debian/copyright
index 669d5abd2..ae2340f5f 100644
--- a/debian/copyright
+++ b/debian/copyright
@@ -165,7 +165,7 @@ License: GPL-3+
 
 Files: picosat/*
 Copyright: 2006 - 2015, Armin Biere, Johannes Kepler University.
-License: MIT style
+License: Expat
  Permission is hereby granted, free of charge, to any person obtaining a copy
  of this software and associated documentation files (the "Software"), to
  deal in the Software without restriction, including without limitation the
@@ -186,7 +186,7 @@ License: MIT style
 
 Files: spot/priv/robin_hood.hh
 Copyright: 2018-2019 Martin Ankerl
-License: MIT
+License: Expat
  Permission is hereby granted, free of charge, to any person obtaining a copy
  of this software and associated documentation files (the "Software"), to deal
  in the Software without restriction, including without limitation the rights

From d308728b41531ba0664abdbfb1ad4794d6128fbd Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 28 Jul 2020 10:30:45 +0200
Subject: [PATCH 07/17] argp: fix handling of very long options in --help

* lib/argp-help.c (hol_entry_help): Handle cases with option
description is larger than RMARGIN.
---
 lib/argp-help.c | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/lib/argp-help.c b/lib/argp-help.c
index 02faa60f7..550dfd98d 100644
--- a/lib/argp-help.c
+++ b/lib/argp-help.c
@@ -1186,7 +1186,11 @@ hol_entry_help (struct hol_entry *entry, const struct argp_state *state,
           __argp_fmtstream_set_lmargin (stream, uparams.opt_doc_col);
           __argp_fmtstream_set_wmargin (stream, uparams.opt_doc_col);
 
-          if (col > (unsigned int) (uparams.opt_doc_col + 3))
+          /* Put the description on a new line if it cannot start
+             within 3 columns of OPT_DOC_COL.  Note that if the option
+             specification went past RMARGIN, then COL has been reset
+             to 0. */
+          if (col > (unsigned int) (uparams.opt_doc_col + 3) || col == 0)
             __argp_fmtstream_putc (stream, '\n');
           else if (col >= (unsigned int) uparams.opt_doc_col)
             __argp_fmtstream_puts (stream, "   ");

From 9e6a99dcac8977a5c2c5d1c621b16acc7e19bee2 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 28 Jul 2020 22:08:47 +0200
Subject: [PATCH 08/17] * spot/misc/satsolver.hh: Typo in comment.

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

diff --git a/spot/misc/satsolver.hh b/spot/misc/satsolver.hh
index 51d931373..03a75fa02 100644
--- a/spot/misc/satsolver.hh
+++ b/spot/misc/satsolver.hh
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013, 2017, 2018 Laboratoire de Recherche et
+// Copyright (C) 2013, 2017-2018, 2020 Laboratoire de Recherche et
 // Développement de l'Epita.
 //
 // This file is part of Spot, a model checking library.
@@ -167,7 +167,7 @@ namespace spot
     PicoSAT* psat_;
 
     // The next 2 pointers will be initialized if SPOT_XCNF env var
-    // is set. This recquires SPOT_SATSOLVER to be set as well.
+    // is set. This requires SPOT_SATSOLVER to be set as well.
     std::ofstream* xcnf_tmp_;
     std::ofstream* xcnf_stream_;
     std::string path_;

From fde9a303c4af3b1274b1846e40465b2ac5563278 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 29 Jul 2020 14:43:55 +0200
Subject: [PATCH 09/17] to_parity: minor fixes

* spot/twaalgos/toparity.cc: Do not call prpagate_marks_here twice if
the automaton was not degeneralized.
* spot/twaalgos/toparity.hh: Typo in comment.
---
 spot/twaalgos/toparity.cc | 3 ++-
 spot/twaalgos/toparity.hh | 2 +-
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/spot/twaalgos/toparity.cc b/spot/twaalgos/toparity.cc
index 31d7b190b..0b46e6224 100644
--- a/spot/twaalgos/toparity.cc
+++ b/spot/twaalgos/toparity.cc
@@ -1583,7 +1583,8 @@ run()
         if (options.propagate_col)
         {
             propagate_marks_here(sub_automaton);
-            propagate_marks_here(deg);
+            if (deg != sub_automaton)
+              propagate_marks_here(deg);
         }
 
         std::map<unsigned, car_state> state2car_sub, state2car_deg;
diff --git a/spot/twaalgos/toparity.hh b/spot/twaalgos/toparity.hh
index 3c935f095..7d2701581 100644
--- a/spot/twaalgos/toparity.hh
+++ b/spot/twaalgos/toparity.hh
@@ -49,7 +49,7 @@ namespace spot
     /// get a better result if we don't apply partial_degeneralize.
     bool force_degen = true;
     /// If \c scc_acc_clean is true, to_parity() will ignore colors
-    /// no occoring in an SCC while processing this SCC.
+    /// not occurring in an SCC while processing this SCC.
     bool acc_clean = true;
     /// If \c parity_equiv is true, to_parity() will check if there
     /// exists a permutations of colors such that the acceptance

From ceced82c5cd3962315aa2a71db1fad5fbd0dfec5 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 29 Jul 2020 15:17:47 +0200
Subject: [PATCH 10/17] * debian/rules (fix-js): Adjust to newer MathJax URL.

---
 debian/rules | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/debian/rules b/debian/rules
index 647c49429..bd2565cd8 100755
--- a/debian/rules
+++ b/debian/rules
@@ -105,5 +105,5 @@ fix-js:
 	perl -pi -e 's|http://orgmode.org/mathjax/MathJax.js|file:///usr/share/javascript/mathjax/MathJax.js|' doc/userdoc/*.html
 	perl -pi -e 's|https://cdnjs.cloudflare.com/ajax/libs/require.js/.*/require.min.js|file:///usr/share/javascript/requirejs/require.min.js|' tests/python/*.html
 	perl -pi -e 's|https://cdn.mathjax.org/mathjax/.*/MathJax.js|file:///usr/share/javascript/mathjax/MathJax.js|' tests/python/*.html doc/userdoc/*.html
-	perl -pi -e 's|https://cdnjs.cloudflare.com/ajax/libs/mathjax/.*/MathJax.js|file:///usr/share/javascript/mathjax/MathJax.js|' tests/python/*.html doc/userdoc/*.html
+	perl -pi -e 's,https://cdnjs.cloudflare.com/ajax/libs/mathjax/.*/(?:MathJax|latest).js,file:///usr/share/javascript/mathjax/MathJax.js,' tests/python/*.html doc/userdoc/*.html
 	perl -pi -e 's|https://cdnjs.cloudflare.com/ajax/libs/jquery/2.0.3/jquery.min.js|file:///usr/share/javascript/jquery/jquery.min.js|' tests/python/*.html

From fd437d62f896e94f6b29ebe8ec2f5b27b1a914b7 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 29 Jul 2020 21:28:01 +0200
Subject: [PATCH 11/17] help2man: allow line breaks in long lists of options

* tools/help2man: Add \: after | when listing optional arguments.
This should fix a lintian warning about unbreakable long line.
---
 tools/help2man | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/tools/help2man b/tools/help2man
index 8ee878782..bf1f075cb 100755
--- a/tools/help2man
+++ b/tools/help2man
@@ -750,7 +750,8 @@ sub get_option_value
 }
 
 # Convert option dashes to \- to stop nroff from hyphenating 'em, and
-# embolden.  Option arguments get italicised.
+# embolden.  Option arguments get italicized. \: in front of | allow
+# linebreaks.
 sub convert_option
 {
     local $_ = '\fB' . shift;
@@ -758,7 +759,7 @@ sub convert_option
     s/-/\x83/g;
     if (s/\[=(.*)\]$/\\fR[=\\fI$1\\fR]/)
     {
-	s/\|/\\fR|\\fI/g;
+	s/\|/\\fR|\\:\\fI/g;
     }
     else
     {

From af108d05565d3af066458f876d0d58948852f4cb Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 31 Jul 2020 12:05:32 +0200
Subject: [PATCH 12/17] * doc/org/ioltl.org: Document prefix operators.

---
 doc/org/ioltl.org | 52 ++++++++++++++++++++++++++++++++++++-----------
 1 file changed, 40 insertions(+), 12 deletions(-)

diff --git a/doc/org/ioltl.org b/doc/org/ioltl.org
index 641a19ef2..696a50c19 100644
--- a/doc/org/ioltl.org
+++ b/doc/org/ioltl.org
@@ -40,6 +40,11 @@ contains column headers).  We have [[file:csv.org][examples of reading or writin
 files on a separate page]].
 
 ** Default parser
+   :PROPERTIES:
+   :CUSTOM_ID: infix
+   :END:
+
+
 
 Spot's default LTL parser is able to parse the syntaxes of many tools,
 such as [[http://spinroot.com][Spin]], [[http://vlsi.colorado.edu/~rbloem/wring.html][Wring]], [[http://goal.im.ntu.edu.tw][Goal]], etc.  For instance here are the preferred ways
@@ -75,6 +80,9 @@ should not try to interpret.  For instance:
 : "a < b" U "process[2]@ok"
 
 ** Lenient mode
+   :PROPERTIES:
+   :CUSTOM_ID: lenient
+   :END:
 
 In version 6, Spin extended its syntax to support arbitrary atomic expression
 in LTL formulas. The previous formula would be written simply:
@@ -122,6 +130,9 @@ ltlfilt --lenient -f '(a U b U) U c'
 Here =a U b U= was taken as an atomic proposition.
 
 ** Prefix parser
+   :PROPERTIES:
+   :CUSTOM_ID: prefix
+   :END:
 
 The prefix syntax used by tools such as [[http://www.tcs.hut.fi/Software/maria/tools/lbt/][LBT]], [[http://www.tcs.hut.fi/Software/lbtt/][LBTT]], [[http://tcs.legacy.ics.tkk.fi/users/tlatvala/scheck/][scheck]] or [[http://www.ltl2dstar.de][ltl2dstar]]
 requires a different parser.  For these tools, the above example
@@ -130,9 +141,31 @@ propositions must start with =p= and be followed by a number).  Spot's
 =--lbt-input= option can be used to activate the parser for this
 syntax.
 
+The following operators are supported:
+
+| syntax | meaning        |
+|--------+----------------|
+|  <c>   | <l>            |
+|  =t=   | true           |
+|  =f=   | false          |
+|  =!=   | not            |
+|  =&=   | and            |
+| \vert  | or             |
+|  =^=   | xor            |
+|  =i=   | implies        |
+|  =e=   | equivalent     |
+|  =X=   | next           |
+|  =F=   | eventually     |
+|  =G=   | globally       |
+|  =U=   | strong until   |
+|  =V=   | weak release   |
+|  =M=   | strong release |
+|  =W=   | weak until     |
+|--------+----------------|
+
 As an extension to LBT's syntax, alphanumeric atomic propositions that
 follow the "=p= + number" rule will be accepted if they do not
-conflict with one of the operator (e.g., =i=, the implies operator,
+conflict with one of the operators (e.g., =i=, the /implies/ operator,
 cannot be used as an atomic proposition).  Also any atomic proposition
 may be double-quoted.  These extensions are compatible with the syntax
 used by [[http://www.ltl2dstar.de][ltl2dstar]].
@@ -141,11 +174,15 @@ used by [[http://www.ltl2dstar.de][ltl2dstar]].
 
 
 * Common output options
+   :PROPERTIES:
+   :CUSTOM_ID: output-options
+   :END:
 
 All tools that output LTL/PSL formulas implement the following options:
 
 #+BEGIN_SRC sh :exports results
-genltl --help | sed -n '/Output options:/,/^$/p' | sed '1d;$d'
+ltlfilt --help | sed -n '/Output options:/,/^$/p' |
+  sed '1d;$d;/--.*count/d;/--quiet/d'
 #+END_SRC
 #+RESULTS:
 #+begin_example
@@ -157,13 +194,9 @@ genltl --help | sed -n '/Output options:/,/^$/p' | sed '1d;$d'
                              "%f")
   -l, --lbt                  output in LBT's syntax
       --latex                output using LaTeX macros
-      --negative, --negated  output the negated versions of all formulas
   -o, --output=FORMAT        send output to a file named FORMAT instead of
                              standard output.  The first formula sent to a file
                              truncates it unless FORMAT starts with '>>'.
-      --positive             output the positive versions of all formulas (done
-                             by default, unless --negative is specified without
-                             --positive)
   -p, --full-parentheses     output fully-parenthesized formulas
   -s, --spin                 output in Spin's syntax
       --spot                 output in Spot's syntax (default)
@@ -220,7 +253,7 @@ the above =%=-sequences.
 For instance the following invocation of [[file:randltl.org][=randltl=]] will create 5
 random formulas, but in 5 different files:
 
-#+BEGIN_SRC sh
+#+BEGIN_SRC sh :epilogue "rm -f example-*.ltl"
 randltl -n5 a b -o example-%L.ltl
 wc -l example-*.ltl
 #+END_SRC
@@ -232,11 +265,6 @@ wc -l example-*.ltl
 :  1 example-5.ltl
 :  5 total
 
-#+BEGIN_SRC sh :results silent :exports results
-rm -f example-*.ltl
-#+END_SRC
-#+RESULTS:
-
 Option =-0= is useful if the list of formulas is passed to =xargs=.
 =xargs= normally splits its input on white space (which are frequent
 in LTL formulas), but you can use =xargs -0= to split the input on

From 149fbb73bff83496293eb4e495b018f840324710 Mon Sep 17 00:00:00 2001
From: Florian Renkin <frenkin@lrde.epita.fr>
Date: Tue, 1 Sep 2020 17:19:44 +0200
Subject: [PATCH 13/17] configure.ac: Correct warning message

configure.ac used unintialized variable when he printed message
for enable-max-accsets

* configure.ac: here.
---
 configure.ac | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/configure.ac b/configure.ac
index 93ca2b24b..db009f093 100644
--- a/configure.ac
+++ b/configure.ac
@@ -71,7 +71,7 @@ then
   AC_DEFINE_UNQUOTED([MAX_ACCSETS], [$enable_max_accsets],
     [The maximal number of acceptance sets supported (also known as acceptance marks)])
 else
-  AC_ERROR([The argument of --enable-max-accsets must be a multiple of $default_nb_acc])
+  AC_ERROR([The argument of --enable-max-accsets must be a multiple of $default_max_accsets])
 fi
 
 # Activate C11 for gnulib tests

From 33a79a34d334e1d23c9f812473840125381e046c Mon Sep 17 00:00:00 2001
From: Florian Renkin <frenkin@lrde.epita.fr>
Date: Tue, 1 Sep 2020 17:25:31 +0200
Subject: [PATCH 14/17] Fix typo

* NEWS, spot/graph/graph.hh: here.
---
 NEWS                | 2 +-
 spot/graph/graph.hh | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/NEWS b/NEWS
index 82a4901f6..0edbfaf5e 100644
--- a/NEWS
+++ b/NEWS
@@ -78,7 +78,7 @@ New in spot 2.9.1 (2020-07-15)
 
   - simplify_acceptance() missed some patterns it should have been
     able to simplify.  For instance Fin(0)&(Fin(1)|Fin(2)|Fin(4))
-    should simplify to Fin(1)|Fin(2)|Fin(4) adter adding {1,2,4} to
+    should simplify to Fin(1)|Fin(2)|Fin(4) after adding {1,2,4} to
     every place where 0 occur, and then the acceptance would be
     renumbered to Fin(0)|Fin(1)|Fin(2).  This is now fixed.
 
diff --git a/spot/graph/graph.hh b/spot/graph/graph.hh
index e247e44ec..87bb063fd 100644
--- a/spot/graph/graph.hh
+++ b/spot/graph/graph.hh
@@ -861,7 +861,7 @@ namespace spot
       return &ss - &states_.front();
     }
 
-    /// Conveart a storage reference into an edge number
+    /// Convert a storage reference into an edge number
     edge index_of_edge(const edge_storage_t& tt) const
     {
       SPOT_ASSERT(!edges_.empty());

From b0f8170055c8a8098694b4450bf9dae932f4f0ab Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 3 Sep 2020 14:45:07 +0200
Subject: [PATCH 15/17] * .gitlab-ci.yml: Update docker images, for buildenv#1.

---
 .gitlab-ci.yml | 26 +++++++++++++-------------
 1 file changed, 13 insertions(+), 13 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 99ae85a33..11ae8fb7b 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -8,7 +8,7 @@ debian-stable-gcc:
     - branches
   except:
     - /wip/
-  image: registry.lrde.epita.fr/spot-debuild:stable
+  image: gitlab-registry.lrde.epita.fr/spot/buildenv/debian:stable
   script:
     - autoreconf -vfi
     - ./configure --enable-max-accsets=256
@@ -27,7 +27,7 @@ debian-unstable-gcc-coverage:
     - branches
   except:
     - /wip/
-  image: registry.lrde.epita.fr/spot-debuild
+  image: gitlab-registry.lrde.epita.fr/spot/buildenv/debian
   script:
     - autoreconf -vfi
     - ./configure CXX='g++ --coverage' --enable-devel --disable-static --enable-doxygen
@@ -54,7 +54,7 @@ debian-gcc-snapshot:
     - branches
   except:
     - /wip/
-  image: registry.lrde.epita.fr/spot-debuild
+  image: gitlab-registry.lrde.epita.fr/spot/buildenv/debian
   script:
     - export PATH="/usr/lib/gcc-snapshot/bin:$PATH" LD_LIBRARY_PATH="/usr/lib/gcc-snapshot/lib:$LD_LIBRARY_PATH"
     - autoreconf -vfi
@@ -77,7 +77,7 @@ alpine-gcc:
     - branches
   except:
     - /wip/
-  image: registry.lrde.epita.fr/spot-alpine
+  image: gitlab-registry.lrde.epita.fr/spot/buildenv/alpine
   script:
     - autoreconf -vfi
     - ./configure
@@ -96,7 +96,7 @@ arch-clang:
     - branches
   except:
     - /wip/
-  image: registry.lrde.epita.fr/spot-arch
+  image: gitlab-registry.lrde.epita.fr/spot/buildenv/arch
   script:
     - autoreconf -vfi
     - ./configure --prefix ~/install_dir CC='clang -Qunused-arguments' CXX='clang++ -Qunused-arguments' --enable-devel --enable-c++17 --enable-doxygen
@@ -114,7 +114,7 @@ arch-gcc-glibcxxdebug:
     - branches
   except:
     - /wip/
-  image: registry.lrde.epita.fr/spot-arch
+  image: gitlab-registry.lrde.epita.fr/spot/buildenv/arch
   script:
     - autoreconf -vfi
     - ./configure --enable-devel --enable-c++17 --enable-glibcxx-debug
@@ -132,7 +132,7 @@ mingw-shared:
     - branches
   except:
     - /wip/
-  image: registry.lrde.epita.fr/spot-debuild
+  image: gitlab-registry.lrde.epita.fr/spot/buildenv/debian
   script:
     - autoreconf -vfi
     - ./configure CC=i686-w64-mingw32-gcc CXX=i686-w64-mingw32-g++-posix --host i686-w64-mingw32 --disable-python
@@ -150,7 +150,7 @@ mingw-static:
     - branches
   except:
     - /wip/
-  image: registry.lrde.epita.fr/spot-debuild
+  image: gitlab-registry.lrde.epita.fr/spot/buildenv/debian
   script:
     - mkdir install_dir
     - autoreconf -vfi
@@ -177,8 +177,8 @@ debpkg-stable:
     - next
     - stable
   script:
-    - docker pull registry.lrde.epita.fr/spot-debuild:stable
-    - docker pull registry.lrde.epita.fr/spot-debuild-i386:stable
+    - docker pull gitlab-registry.lrde.epita.fr/spot/buildenv/debian:stable
+    - docker pull gitlab-registry.lrde.epita.fr/spot/buildenv/debian-i386:stable
     - vol=spot-stable-$CI_COMMIT_SHA
     - docker volume create $vol
     - exitcode=0
@@ -201,8 +201,8 @@ debpkg-unstable:
     - /-deb$/
     - next
   script:
-    - docker pull registry.lrde.epita.fr/spot-debuild
-    - docker pull registry.lrde.epita.fr/spot-debuild-i386
+    - docker pull gitlab-registry.lrde.epita.fr/spot/buildenv/debian
+    - docker pull gitlab-registry.lrde.epita.fr/spot/buildenv/debian-i386
     - vol=spot-unstable-$CI_COMMIT_SHA
     - docker volume create $vol
     - exitcode=0
@@ -226,7 +226,7 @@ rpm-pkg:
     - master
     - next
     - stable
-  image: registry.lrde.epita.fr/spot-rpm
+  image: gitlab-registry.lrde.epita.fr/spot/buildenv/fedora
   script:
     - autoreconf -vfi
     - ./configure

From b956bfe90f91275974e292e37e7793a398f6d72d Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 7 Sep 2020 10:50:01 +0200
Subject: [PATCH 16/17] Release Spot 2.9.4

* NEWS, configure.ac, doc/org/setup.org: Bump to version 2.9.4.
---
 NEWS              |  6 ++++--
 configure.ac      |  2 +-
 doc/org/setup.org | 10 +++++-----
 3 files changed, 10 insertions(+), 8 deletions(-)

diff --git a/NEWS b/NEWS
index 0edbfaf5e..cb523ba24 100644
--- a/NEWS
+++ b/NEWS
@@ -1,9 +1,11 @@
-New in spot 2.9.3.dev  (not yet released)
+New in spot 2.9.4 (2020-09-07)
 
   Bugs fixed:
 
   - Handle xor and <-> in a more natural way when translating
-    LTL formulas to generic acceptancee conditions.
+    LTL formulas to generic acceptance conditions.
+
+  - Multiple typos in documentation, --help texts, or error messages.
 
 New in spot 2.9.3 (2020-07-22)
 
diff --git a/configure.ac b/configure.ac
index db009f093..b9a9e48fa 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.63])
-AC_INIT([spot], [2.9.3.dev], [spot@lrde.epita.fr])
+AC_INIT([spot], [2.9.4], [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 cc9773d9f..8a3339fb2 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.9.3
-#+MACRO: LASTRELEASE 2.9.3
-#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.9.3.tar.gz][=spot-2.9.3.tar.gz=]]
-#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-9-3/NEWS][summary of the changes]]
-#+MACRO: LASTDATE 2020-07-22
+#+MACRO: SPOTVERSION 2.9.4
+#+MACRO: LASTRELEASE 2.9.4
+#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.9.4.tar.gz][=spot-2.9.4.tar.gz=]]
+#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-9-4/NEWS][summary of the changes]]
+#+MACRO: LASTDATE 2020-09-07
 
 #+ATTR_HTML: :id spotlogo
 [[file:spot2.svg]]

From 9a3c809f10c851a27567d366d2fec077440805e9 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 7 Sep 2020 10:56:01 +0200
Subject: [PATCH 17/17] * NEWS, configure.ac: Bump version to 2.9.4.dev.

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

diff --git a/NEWS b/NEWS
index cb523ba24..35a8b0d11 100644
--- a/NEWS
+++ b/NEWS
@@ -1,3 +1,7 @@
+New in spot 2.9.4.dev  (not yet released)
+
+  Nothing yet.
+
 New in spot 2.9.4 (2020-09-07)
 
   Bugs fixed:
diff --git a/configure.ac b/configure.ac
index b9a9e48fa..d194deb9e 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.63])
-AC_INIT([spot], [2.9.4], [spot@lrde.epita.fr])
+AC_INIT([spot], [2.9.4.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])