From fe007b9de377e066720ceba3db256ddb0b6c3144 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 18 Jan 2021 18:19:23 +0100 Subject: [PATCH 01/12] * doc/org/setup.org: Fix last release date. --- doc/org/setup.org | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/org/setup.org b/doc/org/setup.org index f073eba38..268704e63 100644 --- a/doc/org/setup.org +++ b/doc/org/setup.org @@ -5,7 +5,7 @@ #+MACRO: LASTRELEASE 2.9.6 #+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.9.6.tar.gz][=spot-2.9.6.tar.gz=]] #+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-9-6/NEWS][summary of the changes]] -#+MACRO: LASTDATE 2020-11-19 +#+MACRO: LASTDATE 2021-01-18 #+ATTR_HTML: :id spotlogo [[file:spot2.svg]] From b6c4145599ac44b1d3aa5349dd265a22545bc662 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 20 Jan 2021 22:18:42 +0100 Subject: [PATCH 02/12] merge_edge: clarify documentation MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Reported by Florian Renkin. * spot/graph/graph.hh, spot/twa/twagraph.hh (merge_edge): Document that it is expected that state i can only be renamed as j if j≤i. --- spot/graph/graph.hh | 5 +++-- spot/twa/twagraph.hh | 9 ++++++--- 2 files changed, 9 insertions(+), 5 deletions(-) diff --git a/spot/graph/graph.hh b/spot/graph/graph.hh index 87bb063fd..bcd7045f0 100644 --- a/spot/graph/graph.hh +++ b/spot/graph/graph.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014-2018, 2020 Laboratoire de Recherche et +// Copyright (C) 2014-2018, 2020, 2021 Laboratoire de Recherche et // Développement de l'Epita. // // This file is part of Spot, a model checking library. @@ -1290,7 +1290,8 @@ namespace spot /// \brief Rename and remove states. /// /// \param newst A vector indicating how each state should be renumbered. - /// Use -1U to erase a state. + /// Use -1U to erase a state. All other numbers are expected to + /// satisfy newst[i] ≤ i for all i. /// \param used_states the number of states used (after renumbering) void defrag_states(std::vector&& newst, unsigned used_states) { diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh index d2dc9d739..d4cda0971 100644 --- a/spot/twa/twagraph.hh +++ b/spot/twa/twagraph.hh @@ -695,9 +695,12 @@ namespace spot /// digraph::defrag_state() that additionally deals with universal /// branching. /// - /// \param newst A vector indicating how each state should be renumbered. - /// Use -1U to erase a state. - /// \param used_states the number of states used (after renumbering) + /// \param newst A vector indicating how each state should be + /// renumbered. Use -1U to erase a state. Ignoring the + /// occurrences of -1U, the renumbering is expected to + /// satisfy newst[i] ≤ i for all i. + /// \param used_states the number of states used + /// (after renumbering) void defrag_states(std::vector&& newst, unsigned used_states); /// \brief Print the data structures used to represent the From 244e3a973165f1cb2e5bfe7f411ac6eeafd409cb Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 3 Feb 2021 12:20:42 +0100 Subject: [PATCH 03/12] fix eventual/universal properties for ->/<->/xor * spot/tl/formula.cc: Correctly set eventual and universal properties for ->, <->, and xor. This wasn't really relevant before, but there are now situation where those are not rewritten. * tests/core/kind.test: Adjust expected output. * tests/core/ltl2tgba2.test: New test case, reported by Florian Renkin. * NEWS: Mention the bug. --- NEWS | 3 +++ spot/tl/formula.cc | 14 ++++++++------ tests/core/kind.test | 8 ++++---- tests/core/ltl2tgba2.test | 11 +++++++++-- 4 files changed, 24 insertions(+), 12 deletions(-) diff --git a/NEWS b/NEWS index f1661b087..2f66c8270 100644 --- a/NEWS +++ b/NEWS @@ -2,6 +2,9 @@ New in spot 2.9.6.dev (not yet released) Nothing yet. + - Some formulas using ->, <->, or xor were not properly detected as + purely universal or pure eventualities. + New in spot 2.9.6 (2021-01-18) Build: diff --git a/spot/tl/formula.cc b/spot/tl/formula.cc index 05b295708..346d77fce 100644 --- a/spot/tl/formula.cc +++ b/spot/tl/formula.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015-2019 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2015-2019, 2021 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -1283,8 +1283,8 @@ namespace spot case op::Xor: case op::Equiv: props = children[0]->props & children[1]->props; - is_.eventual = false; - is_.universal = false; + // Preserve suspendable property + is_.eventual = is_.universal = is_.eventual && is_.universal; is_.sere_formula = is_.boolean; is_.sugar_free_boolean = false; is_.in_nenoform = false; @@ -1310,8 +1310,10 @@ namespace spot break; case op::Implies: props = children[0]->props & children[1]->props; - is_.eventual = false; - is_.universal = false; + is_.eventual = + children[0]->is_universal() && children[1]->is_eventual(); + is_.universal = + children[0]->is_eventual() && children[1]->is_universal(); is_.sere_formula = (children[0]->is_boolean() && children[1]->is_sere_formula()); is_.sugar_free_boolean = false; diff --git a/tests/core/kind.test b/tests/core/kind.test index db04fc6d2..d6413211a 100755 --- a/tests/core/kind.test +++ b/tests/core/kind.test @@ -1,7 +1,7 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2010-2012, 2015, 2017, 2019 Laboratoire de Recherche -# et Développement de l'Epita (LRDE). +# Copyright (C) 2010-2012, 2015, 2017, 2019, 2021 Laboratoire de +# Recherche et Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -47,8 +47,8 @@ a U (b U (c U d)),&!xfLPgopra a W (b W (c W d)),&!xfLPsopra a M (b M (c M d)),&!xfLPgopra Fa -> Fb,xLPopra -Ga -> Fb,xLPgopra -Fa -> Gb,xLPsopra +Ga -> Fb,xLPegopra +Fa -> Gb,xLPusopra (Ga|Fc) -> Fb,xLPopra (Ga|Fa) -> Gb,xLPopra {a;c*;b}|->!Xb,&fPsopra diff --git a/tests/core/ltl2tgba2.test b/tests/core/ltl2tgba2.test index 57fd57d44..26c29acc0 100755 --- a/tests/core/ltl2tgba2.test +++ b/tests/core/ltl2tgba2.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2009-2020 Laboratoire de Recherche et Développement de +# Copyright (C) 2009-2021 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 @@ -469,4 +469,11 @@ test "4,1" = `ltl2tgba -D -x wdba-minimize=2 "$f" --stats=%s,%d` test "4,0" = `ltl2tgba -D -x wdba-minimize=0 "$f" --stats=%s,%d` test "4,1" = `ltl2tgba -D --med "$f" --stats=%s,%d` -: +# This used to fail because ltl-split would not detect +# the (GFa <-> (GFb & GFc & GFd & GFe & GFf & GFg & GFh)) part +# as suspendable. +f='G((a -> X((!a U b) | G!a)) & (a -> X(G!a | (!a U c))) & (a -> X(G!a +| (!a U d))) & (a -> X(G!a | (!a U e))) & (a -> X(G!a | (!a U f))) & +(a -> X(G!a | (!a U g))) & (a -> X(G!a | (!a U h)))) & (GFa <-> (GFb & +GFc & GFd & GFe & GFf & GFg & GFh))' +test 128 = `ltl2tgba -G -D "$f" --stats=%s` From 4d23b7b770a1bac0ea35889d2da2f3fb690d5ffd Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 3 Feb 2021 17:10:41 +0100 Subject: [PATCH 04/12] work around a GraphViz 2.60.0 bug * spot/twa/twagraph.cc (dump_storage_as_dot): Prefer \n over a plain new line to work around GraphViz issue 1931, which was causing twagraph-internals.ipynb to fail in our test suite. --- spot/twa/twagraph.cc | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index 38e302c96..d652fdaa1 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -896,9 +896,14 @@ namespace spot if (!named_prop_.empty()) { - out << "namedprops [label=\"named properties:\n"; + // GraphiViz 2.46.0 has a bug where plain newlines in + // quoted strings are ignored. See + // https://gitlab.com/graphviz/graphviz/-/issues/1931 + // A workaround is to use emit \n instead of the + // actual new line. + out << "namedprops [label=\"named properties:\\n"; for (auto p: named_prop_) - escape_html(out, p.first) << '\n'; + escape_html(out, p.first) << "\\n"; out << "\"]\n"; } } From cad3d7706cd74e278286ce83ff8d2593005ad29a Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 18 Feb 2021 22:15:58 +0100 Subject: [PATCH 05/12] twagraph: improve doc MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Based on report by Michaël Cadilhac. * spot/graph/graph.hh, spot/twa/twagraph.hh (defrag_state): Clarify that only unreachable states are meant to be removed. * spot/twa/twagraph.hh (merge_edges): Typo in comment. Fixes #457. * THANKS: Add Michaël. --- THANKS | 1 + spot/graph/graph.hh | 17 +++++++++++++---- spot/twa/twagraph.hh | 22 +++++++++++++++------- 3 files changed, 29 insertions(+), 11 deletions(-) diff --git a/THANKS b/THANKS index 090f09bae..d492eb481 100644 --- a/THANKS +++ b/THANKS @@ -33,6 +33,7 @@ Kristin Y. Rozier Martin Dieguez Lodeiro Matthias Heizmann Maxime Bouton +Michaël Cadilhac Michael Tautschnig Michael Weber Mikuláš Klokočka diff --git a/spot/graph/graph.hh b/spot/graph/graph.hh index bcd7045f0..507bc849e 100644 --- a/spot/graph/graph.hh +++ b/spot/graph/graph.hh @@ -1289,10 +1289,19 @@ namespace spot /// \brief Rename and remove states. /// - /// \param newst A vector indicating how each state should be renumbered. - /// Use -1U to erase a state. All other numbers are expected to - /// satisfy newst[i] ≤ i for all i. - /// \param used_states the number of states used (after renumbering) + /// This method is used to remove some states that have been + /// previously detected to be unreachable in order to "defragment" + /// the state vector. When a state is removed, all its outgoing + /// transition are removed as well. Removing reachable states + /// should NOT be attempted, because the incoming edges will be + /// dangling. + /// + /// \param newst A vector indicating how each state should be + /// renumbered. Use -1U to erase an unreachable state. All other + /// numbers are expected to satisfy newst[i] ≤ i for all i. + /// + /// \param used_states the number of states used (after + /// renumbering) void defrag_states(std::vector&& newst, unsigned used_states) { SPOT_ASSERT(newst.size() >= states_.size()); diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh index d4cda0971..2ab481b42 100644 --- a/spot/twa/twagraph.hh +++ b/spot/twa/twagraph.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014-2020 Laboratoire de Recherche et Développement +// Copyright (C) 2014-2021 Laboratoire de Recherche et Développement // de l'Epita. // // This file is part of Spot, a model checking library. @@ -554,7 +554,7 @@ namespace spot /// /// In the first pass, edges that share their source, destination, /// and acceptance marks are merged into a single edge whose condition - /// is the conjunction of the conditions of the original edges. + /// is the disjunction of the conditions of the original edges. /// /// In the second pass, which is performed only on automata with /// Fin-less acceptance, edges with the same source, destination, @@ -695,12 +695,20 @@ namespace spot /// digraph::defrag_state() that additionally deals with universal /// branching. /// + /// This method is used to remove some states that have been + /// previously detected to be unreachable in order to "defragment" + /// the state vector. When a state is removed, all its outgoing + /// transition are removed as well. Removing reachable states + /// should NOT be attempted, because the incoming edges will be + /// dangling. + /// /// \param newst A vector indicating how each state should be - /// renumbered. Use -1U to erase a state. Ignoring the - /// occurrences of -1U, the renumbering is expected to - /// satisfy newst[i] ≤ i for all i. - /// \param used_states the number of states used - /// (after renumbering) + /// renumbered. Use -1U to mark an unreachable state for removal. + /// Ignoring the occurrences of -1U, the renumbering is expected + /// to satisfy newst[i] ≤ i for all i. + /// + /// \param used_states the number of states used after + /// renumbering. void defrag_states(std::vector&& newst, unsigned used_states); /// \brief Print the data structures used to represent the From 084964a9ff51246efd9046c9dd61d90ec802eecb Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 19 Feb 2021 15:58:49 +0100 Subject: [PATCH 06/12] autfilt: fix incorrect diagnostic * bin/autfilt.cc (OPT_KEEP_STATES): Mention the correct option. * tests/core/maskkeep.test: Test for it. * NEWS: Mention the bug. --- NEWS | 5 ++++- bin/autfilt.cc | 4 ++-- tests/core/maskkeep.test | 10 +++++++--- 3 files changed, 13 insertions(+), 6 deletions(-) diff --git a/NEWS b/NEWS index 2f66c8270..8622f8312 100644 --- a/NEWS +++ b/NEWS @@ -1,10 +1,13 @@ New in spot 2.9.6.dev (not yet released) - Nothing yet. + Bugs fixed: - Some formulas using ->, <->, or xor were not properly detected as purely universal or pure eventualities. + - autfilt --keep-states=... could incorrectly mention --mask-acc + when diagnosing errors. + New in spot 2.9.6 (2021-01-18) Build: diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 5cc3bda7e..49fcb04d5 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013-2020 Laboratoire de Recherche et Développement +// Copyright (C) 2013-2021 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -1011,7 +1011,7 @@ parse_opt(int key, char* arg, struct argp_state*) { if (res < 0) error(2, 0, "state ids should be non-negative:" - " --mask-acc=%ld", res); + " --keep-states=%ld", res); // We don't know yet how many states the automata contain. if (opt_keep_states.size() <= static_cast(res)) opt_keep_states.resize(res + 1, false); diff --git a/tests/core/maskkeep.test b/tests/core/maskkeep.test index 4fe4dbcf1..1188c1b67 100755 --- a/tests/core/maskkeep.test +++ b/tests/core/maskkeep.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement +# Copyright (C) 2015, 2016, 2021 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -109,5 +109,9 @@ run 0 autfilt --keep-states=1,2,0 input1 -H >output diff output expect4 # Errors -run 2 autfilt --keep-states=a3 input1 -run 2 autfilt --keep-states=3-2 input1 +run 2 autfilt --keep-states=a3 input1 2> error +cat error +grep 'failed to parse' error +run 2 autfilt --keep-states=3-2 input1 2> error +cat error +grep 'non-negative: --keep-states' error From 7ef69fa15b0e5250bdb9570f4f81efd0fe202116 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 3 Mar 2021 14:13:55 +0100 Subject: [PATCH 07/12] * doc/tl/tl.tex: Typo reported by Florian. --- doc/tl/tl.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index 066bf1c94..39e0f1f48 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -1424,7 +1424,7 @@ $\NOT$ operator. f \EQUIV g & \equiv ((\NOT f)\AND(\NOT g))\OR(f\AND g) & \NOT(f \EQUIV g) & \equiv ((\NOT f)\AND g)\OR(f\AND\NOT g) & \NOT(f \OR g) & \equiv (\NOT f)\AND(\NOT g) \\ - f \IMPLIES g & \equiv (\NOT f) \AND g & + f \IMPLIES g & \equiv (\NOT f) \OR g & \NOT(f \IMPLIES g) & \equiv f \AND \NOT g \end{align*} From caca8728fe1fac6e342173cec7d044b706a4e026 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 15 Apr 2021 16:02:39 +0200 Subject: [PATCH 08/12] * spot/twa/twagraph.cc (remove_unused_ap): Remove unused variable. --- spot/twa/twagraph.cc | 1 - 1 file changed, 1 deletion(-) diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index d652fdaa1..960fc26d9 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -709,7 +709,6 @@ namespace spot { if (ap().empty()) return; - std::set conds; bdd all = ap_vars(); for (auto& e: g_.edges()) { From 6253885af730ef63aa3d20ad222688f9661619b3 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 19 Apr 2021 16:46:30 +0200 Subject: [PATCH 09/12] improve documentation for -x sat-minimize * bin/man/spot-x.x, bin/spot-x.cc: Improve documentation of SAT-based minimization. It was still referring to TGBA although it works for TwA. * spot/twaalgos/postproc.cc: Typo. --- bin/man/spot-x.x | 12 +++++++++--- bin/spot-x.cc | 23 ++++++++++++----------- spot/twaalgos/postproc.cc | 2 +- 3 files changed, 22 insertions(+), 15 deletions(-) diff --git a/bin/man/spot-x.x b/bin/man/spot-x.x index 69d8e35d9..f7f322a34 100644 --- a/bin/man/spot-x.x +++ b/bin/man/spot-x.x @@ -10,11 +10,17 @@ spot-x \- Common fine-tuning options and environment variables. .\" Add any additional description here [SAT\-MINIMIZE VALUES] +When the sat-minimize=K option is used to enable SAT-based +minimization of deterministic automata, a SAT solver is +used to minimize an input automaton with N states into an +output automaton with 1≤M≤N states. The parameter K specifies +how the smallest possible M should be searched. + .TP \fB1\fR -Used by default, \fB1\fR performs a binary search, checking N/2, etc. -The upper bound being N (the size of the starting automaton), the lower bound -is always 1 except when \fBsat-langmap\fR option is used. +The default, \fB1\fR, performs a binary search between 1 and N. The +lower bound can sometimes be improved when the \fBsat-langmap\fR +option is used. .TP \fB2\fR diff --git a/bin/spot-x.cc b/bin/spot-x.cc index 007e23233..feb193522 100644 --- a/bin/spot-x.cc +++ b/bin/spot-x.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013-2020 Laboratoire de Recherche et Développement +// Copyright (C) 2013-2021 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -160,11 +160,12 @@ that are weak and deterministic. The default is 1 in --high mode, else 2 in \ if the TGBA is not already deterministic. Doing so will degeneralize \ the automaton. This is disabled by default, unless sat-minimize is set.") }, { DOC("sat-minimize", - "Set it to enable SAT-based minimization of deterministic \ -TGBA. Depending on its value (from 1 to 4) it changes the algorithm \ -to perform. The default value is (1) and it proves to be the most effective \ -method. SAT-based minimization uses PicoSAT (distributed with Spot), but \ -another installed SAT-solver can be set thanks to the SPOT_SATSOLVER \ + "Set to a value between 1 and 4 to enable SAT-based minimization \ +of deterministic ω-automata. If the input has n states, a SAT solver is \ +used to find an equivalent automaton with 1≤m Date: Tue, 11 May 2021 18:25:55 +0200 Subject: [PATCH 10/12] org: add missing :exports results :results silent * doc/org/ltlfilt.org, doc/org/tut30.org, doc/org/tut31.org: Hide rm invocations used for cleanup. --- doc/org/ltlfilt.org | 2 +- doc/org/tut30.org | 2 +- doc/org/tut31.org | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/doc/org/ltlfilt.org b/doc/org/ltlfilt.org index c27853ffa..0a60479ca 100644 --- a/doc/org/ltlfilt.org +++ b/doc/org/ltlfilt.org @@ -588,7 +588,7 @@ wc -l scheck*.ltl : 4 scheck.ltl : 8 total -#+BEGIN_SRC sh +#+BEGIN_SRC sh :results silent :exports results rm -f ltlex.def ltlex.never scheck.ltl #+END_SRC diff --git a/doc/org/tut30.org b/doc/org/tut30.org index 819b147b7..e619f5881 100644 --- a/doc/org/tut30.org +++ b/doc/org/tut30.org @@ -231,7 +231,7 @@ State: 4 --END-- #+end_SRC -#+BEGIN_SRC sh :results silent +#+BEGIN_SRC sh :results silent :exports results rm -f tut30.hoa #+END_SRC diff --git a/doc/org/tut31.org b/doc/org/tut31.org index eaf39a788..4897c0415 100644 --- a/doc/org/tut31.org +++ b/doc/org/tut31.org @@ -171,7 +171,7 @@ State: 1 --END-- #+end_SRC -#+BEGIN_SRC sh :results silent +#+BEGIN_SRC sh :results silent :exports results rm -f tut31.hoa #+END_SRC From bc768a7157128dc6a8adcdee81579985ce4c9589 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 12 May 2021 11:20:37 +0200 Subject: [PATCH 11/12] Release Spot 2.9.7 * NEWS, configure.ac, doc/org/setup.org: Update for 2.9.7. --- NEWS | 7 ++++++- configure.ac | 2 +- doc/org/setup.org | 10 +++++----- 3 files changed, 12 insertions(+), 7 deletions(-) diff --git a/NEWS b/NEWS index 8622f8312..8002d12e7 100644 --- a/NEWS +++ b/NEWS @@ -1,4 +1,4 @@ -New in spot 2.9.6.dev (not yet released) +New in spot 2.9.7 (2021-05-12) Bugs fixed: @@ -8,6 +8,11 @@ New in spot 2.9.6.dev (not yet released) - autfilt --keep-states=... could incorrectly mention --mask-acc when diagnosing errors. + - Work around GraphViz issue 1931, causing spurious failures in the + test suite. + + - Miscelaneous documentation fixes. + New in spot 2.9.6 (2021-01-18) Build: diff --git a/configure.ac b/configure.ac index 201a96e4c..656e27c72 100644 --- a/configure.ac +++ b/configure.ac @@ -21,7 +21,7 @@ # along with this program. If not, see . AC_PREREQ([2.69]) -AC_INIT([spot], [2.9.6.dev], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.9.7], [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 268704e63..809788d25 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.6 -#+MACRO: LASTRELEASE 2.9.6 -#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.9.6.tar.gz][=spot-2.9.6.tar.gz=]] -#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-9-6/NEWS][summary of the changes]] -#+MACRO: LASTDATE 2021-01-18 +#+MACRO: SPOTVERSION 2.9.7 +#+MACRO: LASTRELEASE 2.9.7 +#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.9.7.tar.gz][=spot-2.9.7.tar.gz=]] +#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-9-7/NEWS][summary of the changes]] +#+MACRO: LASTDATE 2021-05-12 #+ATTR_HTML: :id spotlogo [[file:spot2.svg]] From 30e82e7b1f5c33b40f952857bbd392aa4cd11351 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 12 May 2021 15:56:02 +0200 Subject: [PATCH 12/12] Bump version to 2.9.7.dev * NEWS, configure.ac: Here. --- NEWS | 4 ++++ configure.ac | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index 8002d12e7..0ab85d0c2 100644 --- a/NEWS +++ b/NEWS @@ -1,3 +1,7 @@ +New in spot 2.9.7.dev (not yet released) + + Nothing yet. + New in spot 2.9.7 (2021-05-12) Bugs fixed: diff --git a/configure.ac b/configure.ac index 656e27c72..42a5e3627 100644 --- a/configure.ac +++ b/configure.ac @@ -21,7 +21,7 @@ # along with this program. If not, see . AC_PREREQ([2.69]) -AC_INIT([spot], [2.9.7], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.9.7.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])