From eeccd5804dfa919353d0fdc70fb0f7cfa8a16b65 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 17 May 2021 18:14:32 +0200 Subject: [PATCH 01/13] * spot/graph/graph.hh (chain_edges_): Typo in doc. --- spot/graph/graph.hh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spot/graph/graph.hh b/spot/graph/graph.hh index 507bc849e..d37e02acf 100644 --- a/spot/graph/graph.hh +++ b/spot/graph/graph.hh @@ -1229,7 +1229,7 @@ namespace spot /// \brief Reconstruct the chain of outgoing edges /// /// Should be called only when it is known that all edges - /// with the same destination are consecutive in the vector. + /// with the same source are consecutive in the vector. void chain_edges_() { state last_src = -1U; From 2e14eb0c02a31dc159d507d7cd1ab74c571ce5d6 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 11 Jun 2021 11:46:27 +0200 Subject: [PATCH 02/13] [buddy] typo coma -> comma * ChangeLog.1: Here. --- buddy/ChangeLog.1 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/buddy/ChangeLog.1 b/buddy/ChangeLog.1 index d81429667..3a8ffa3fa 100644 --- a/buddy/ChangeLog.1 +++ b/buddy/ChangeLog.1 @@ -369,7 +369,7 @@ examples/solitare/solitare.cxx: Include iostream. * examples/calculator/parser.y: Rename as ... * examples/calculator/parser.yxx: ... this. Remove spurious - comas in %token, %right, and %left arguments. + commas in %token, %right, and %left arguments. * examples/calculator/parser.h: Rename as ... * examples/calculator/parser_.h: ... this, because the bison rule with output parser.h (not tokens.h) from parser.y. From 773939bebef5a191d01a40e798e26753fec64daa Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 11 Jun 2021 11:46:55 +0200 Subject: [PATCH 03/13] typos: coma -> comma * ChangeLog.1, tests/core/autcross3.test, tests/core/ltl3ba.test, tests/core/ltl3dra.test, tests/core/ltlcross3.test, tests/core/ltlsynt.test, tests/sanity/style.test: Here. --- ChangeLog.1 | 2 +- tests/core/autcross3.test | 4 ++-- tests/core/ltl3ba.test | 6 +++--- tests/core/ltl3dra.test | 4 ++-- tests/core/ltlcross3.test | 4 ++-- tests/core/ltlsynt.test | 2 +- tests/sanity/style.test | 4 ++-- 7 files changed, 13 insertions(+), 13 deletions(-) diff --git a/ChangeLog.1 b/ChangeLog.1 index 178c4050e..92474b480 100644 --- a/ChangeLog.1 +++ b/ChangeLog.1 @@ -7390,7 +7390,7 @@ * src/ltlvisit/reducform.cc (reduce_form_visitor): Rename as ... (reduce_visitor): ... this. * src/ltltest/inf.cc: Adjust calls. - * src/sanity/style.test: Improve missing-space after coma detection. + * src/sanity/style.test: Improve missing-space after comma detection. 2004-05-26 Alexandre Duret-Lutz diff --git a/tests/core/autcross3.test b/tests/core/autcross3.test index 9afc50fe8..2062d7faf 100755 --- a/tests/core/autcross3.test +++ b/tests/core/autcross3.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2017 Laboratoire de Recherche et Développement de +# Copyright (C) 2017, 2021 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -24,7 +24,7 @@ set -e check_csv() { - # Make sure all lines in $1 have the same number of comas + # Make sure all lines in $1 have the same number of commas sed 's/[^,]//g' < "$1" | ( read first while read l; do diff --git a/tests/core/ltl3ba.test b/tests/core/ltl3ba.test index 105a34b7b..fdcebc926 100755 --- a/tests/core/ltl3ba.test +++ b/tests/core/ltl3ba.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2016, 2017, 2018 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). +# Copyright (C) 2016-2018, 2021 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -52,7 +52,7 @@ EOF grep _x output.csv && exit 1 -# Make sure all lines in output.csv have the same number of comas +# Make sure all lines in output.csv have the same number of commas sed 's/[^,]//g' GF(!b&XXb)' --csv='>>FILE' || : ltlsynt --algo=lar.old $opts 'FGa <-> GF(c&a)' --csv='>>FILE' || : test 6 = `wc -l < FILE` - # Make sure all lines in FILE have the same number of comas + # Make sure all lines in FILE have the same number of commas sed 's/[^,]//g' < FILE | ( read first while read l; do diff --git a/tests/sanity/style.test b/tests/sanity/style.test index 3992d29d8..7af4ed5fe 100755 --- a/tests/sanity/style.test +++ b/tests/sanity/style.test @@ -1,6 +1,6 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2009-2019 Laboratoire de Recherche et Développement de +# Copyright (C) 2009-2021 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 # (LIP6), département Systèmes Répartis Coopératifs (SRC), Université @@ -204,7 +204,7 @@ for dir in "$TOP/spot" "$TOP/bin" "$TOP/tests"; do diag 'No space after unary operators (!).' $GREP ",[^ \" %'\\\\]" $tmp && - diag 'Space after coma.' + diag 'Space after comma.' # The 'r' allows operator&& # The '.' allows &&... From 77545824ebbb2c10fabe38d96a243603ee31bf2d Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 11 Jun 2021 11:48:40 +0200 Subject: [PATCH 04/13] ltlfilt: fix a typo in the --help text * bin/ltlfilt.cc: Here. --- bin/ltlfilt.cc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/bin/ltlfilt.cc b/bin/ltlfilt.cc index 02596cde1..cc9e0f02b 100644 --- a/bin/ltlfilt.cc +++ b/bin/ltlfilt.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2020 Laboratoire de Recherche et Développement +// Copyright (C) 2012-2021 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -252,7 +252,7 @@ static const argp_option options[] = "wall-clock time elapsed in seconds (excluding parsing)", 0 }, { "%R, %[LETTERS]R", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, - "CPU time (excluding parsing), in seconds; Add LETTERS to restrict to" + "CPU time (excluding parsing), in seconds; Add LETTERS to restrict to " "(u) user time, (s) system time, (p) parent process, " "or (c) children processes.", 0 }, { "%<", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, From 487bbb63de7f30cd6c982ce011d9b1a566dce721 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 21 Jun 2021 11:42:36 +0200 Subject: [PATCH 05/13] work around a null pointer dereference error This fixes #462. * spot/twaalgos/gfguarantee.cc (do_g_f_terminal_inplace): Replace the redirect_src vector by a unique_ptr. Not only does this remove the false positive diagnostic, but it also removes the unneeded default initialization of the elements of that vector. --- spot/twaalgos/gfguarantee.cc | 36 +++++++++++++++++++++--------------- 1 file changed, 21 insertions(+), 15 deletions(-) diff --git a/spot/twaalgos/gfguarantee.cc b/spot/twaalgos/gfguarantee.cc index 730714b83..94496ee6e 100644 --- a/spot/twaalgos/gfguarantee.cc +++ b/spot/twaalgos/gfguarantee.cc @@ -188,13 +188,18 @@ namespace spot unsigned new_init = -1U; // We do two the rewrite in two passes. The first one // replays histories to detect the new source the edges - // should synchronize with. We used to have single - // loop, but replaying history on edges that have been modified - // result in different automaton depending on the edge order. - std::vector redirect_src; + // should synchronize with. The second pass do the actual + // rewrite. We used to have single loop, but replaying + // history on edges that have been modified results in + // different automata depending on the edge order. + std::unique_ptr redirect_src; if (is_det) { - redirect_src.resize(aut->edge_vector().size()); + // We use a unique_ptr instead of a resized vector to + // avoid default initializing all values. Doing so + // also removes an incorrect "null pointer dereference" + // diagnostic from g++ 11.0 (see issue #462). + redirect_src.reset(new unsigned[aut->edge_vector().size()]); for (auto& e: aut->edges()) { unsigned edge = aut->edge_number(e); @@ -268,7 +273,7 @@ namespace spot } } - // No we do the redirections. + // Now we do the redirections. // We will modify most of the edges in place, but some cases // require the addition of new edges. However we cannot add @@ -311,10 +316,10 @@ namespace spot new_init = init; continue; } - // If initial state cannot be reached from another - // state of the automaton, we can get rid of it by - // combining the edge reaching the terminal state - // with the edges leaving the initial state. + // If the initial state cannot be reached from + // another state of the automaton, we can get rid of + // it by combining the edge reaching the terminal + // state with the edges leaving the initial state. // // However if we have some histories for e.src // (which implies that the automaton is @@ -323,11 +328,12 @@ namespace spot // // One problem with those histories, is that we do // not know how much of it to replay. It's possible - // that we cannot find a matching transition (e.g. if - // the history if "b" but the choices are "!a" or "a"), - // and its also possible to that playing too much of - // history will get us back the terminal state. In both - // cases, we should try again with a smaller history. + // that we cannot find a matching transition + // (e.g. if the history if "b" but the choices are + // "!a" or "a"), and it's also possible that playing + // too much of history will get us back the terminal + // state. In both cases, we should try again with a + // smaller history. unsigned moved_init = init; bdd econd = e.cond; bool first; From bb7426c0b94a7d1349be49bde7dba39cf97aa317 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 29 Jun 2021 11:54:17 +0200 Subject: [PATCH 06/13] org: we have a conda-forge package * doc/org/install.org: Add conda instructions. --- doc/org/install.org | 22 ++++++++++++++++++++-- 1 file changed, 20 insertions(+), 2 deletions(-) diff --git a/doc/org/install.org b/doc/org/install.org index 5012d024f..97bcb7446 100644 --- a/doc/org/install.org +++ b/doc/org/install.org @@ -4,7 +4,7 @@ #+INCLUDE: setup.org #+HTML_LINK_UP: index.html -* Installing from a tarball +* Installing and compiling from a tarball :PROPERTIES: :CUSTOM_ID: tar :END: @@ -131,7 +131,25 @@ command-line tools, =python3-spot= contains the Python bindings, documentation that you can also find online. Those packages depends on =libspot= that contains the shared libraries. -* Installing from git +* Installing as a Conda package + + Spot is available as a [[https://anaconda.org/conda-forge/spot][Conda-forge package]] for Linux and OS X. + + A typical installation would go as follow: + +#+BEGIN_SRC sh + conda create --name myenv python=3.8 # adjust as desired + conda activate myenv + conda install -c conda-forge spot +#+END_SRC + + Note that this package is built automatically by the conda-forge + infrastructure, but this requires some manual trigger after each + release. Therefore there might be a delay between the moment a + release of Spot is announced, and the availability of the Conda + package. + +* Installing and compiling from git :PROPERTIES: :CUSTOM_ID: git :END: From c0c76904da69d0d851adc7d96e7a6f401d4b4b3d Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 5 Jul 2021 14:12:58 +0200 Subject: [PATCH 07/13] bitset: fix implementation of operator-() This fixes #469. * spot/misc/bitset.hh (bitset::operator-): Rewrite. I cannot follow the logic of the old implementation. * tests/python/setacc.py: Add a test case, inspired from #469. --- spot/misc/bitset.hh | 11 ++++------- tests/python/setacc.py | 16 +++++++++++++++- 2 files changed, 19 insertions(+), 8 deletions(-) diff --git a/spot/misc/bitset.hh b/spot/misc/bitset.hh index bb1693d2b..097029904 100644 --- a/spot/misc/bitset.hh +++ b/spot/misc/bitset.hh @@ -318,15 +318,12 @@ namespace spot bitset operator-() const { bitset res = *this; - unsigned carry = 0; + unsigned carry = 1; for (auto& v : res.data) { - v += carry; - if (v < carry) - carry = 2; - else - carry = 1; - v = -v; + word_t old = v; + v = ~v + carry; + carry = old == 0; } return res; } diff --git a/tests/python/setacc.py b/tests/python/setacc.py index f614d2439..f82fba37d 100644 --- a/tests/python/setacc.py +++ b/tests/python/setacc.py @@ -1,6 +1,6 @@ #!/usr/bin/python3 # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2016, 2018 Laboratoire de Recherche et Développement de +# Copyright (C) 2016, 2018, 2021 Laboratoire de Recherche et Développement de # l'EPITA. # # This file is part of Spot, a model checking library. @@ -82,3 +82,17 @@ assert v == () # FIXME: We should have a way to disable the following output, as it is not # part of HOA v1. assert acc.name() == "generalized-Streett 1 2" + + +# issue #469. This test is meaningful only if Spot is compiled with +# --enable-max-accsets=64 or more. +try: + m = spot.mark_t([33]) + assert m.lowest() == m + n = spot.mark_t([33,34]) + assert n.lowest() == m +except RuntimeError as e: + if "Too many acceptance sets used." in str(e): + pass + else: + raise e From eb3474d82b86dd3bb3574d84ee1dceaedf84e41c Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 5 Jul 2021 16:00:57 +0200 Subject: [PATCH 08/13] fix a gcc-snapshot -Wnoexcept diagnostic * spot/misc/hash.hh (ptr_hash): Add noexcept on constructor to please gcc-snapshot. --- spot/misc/hash.hh | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/spot/misc/hash.hh b/spot/misc/hash.hh index f0f55eea1..4995dab84 100644 --- a/spot/misc/hash.hh +++ b/spot/misc/hash.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2011, 2014, 2015, 2018 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2008, 2011, 2014, 2015-2018, 2021 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), // Université Pierre et Marie Curie. @@ -41,7 +41,7 @@ namespace spot // A default constructor is needed if the ptr_hash object is // stored in a const member. This occur with the clang version // installed by OS X 10.9. - ptr_hash() + ptr_hash() noexcept { } From c34192a77c29983f7553da3a54bb1e3f5d12f2b6 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 7 Jul 2021 17:20:33 +0200 Subject: [PATCH 09/13] twa_run: reduce now diagnoses rejecting runs Part of #471. * spot/twaalgos/emptiness.cc: Throw an exception if the cycle is rejecting. * spot/twaalgos/emptiness.hh: Document this behavior. * tests/python/except.py: Test it. --- spot/twaalgos/emptiness.cc | 11 +++++++++-- spot/twaalgos/emptiness.hh | 5 ++++- tests/python/except.py | 13 +++++++++++++ 3 files changed, 26 insertions(+), 3 deletions(-) diff --git a/spot/twaalgos/emptiness.cc b/spot/twaalgos/emptiness.cc index 5ca65224d..fd3319141 100644 --- a/spot/twaalgos/emptiness.cc +++ b/spot/twaalgos/emptiness.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2011-2019 Laboratoire de Recherche et +// Copyright (C) 2009, 2011-2019, 2021 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -343,8 +343,14 @@ namespace spot state_set seen; const state_set* target; }; + + [[noreturn]] static void report_rejecting_cycle() + { + throw std::runtime_error("twa_run::reduce() expects an accepting cycle"); + } } + twa_run_ptr twa_run::reduce() const { ensure_non_empty_cycle("twa_run::reduce()"); @@ -368,7 +374,8 @@ namespace spot twa_run::steps::const_iterator seg = cycle.end(); do { - assert(seg != cycle.begin()); + if (SPOT_UNLIKELY(seg == cycle.begin())) + report_rejecting_cycle(); --seg; seen_acc |= seg->acc; } diff --git a/spot/twaalgos/emptiness.hh b/spot/twaalgos/emptiness.hh index 78eb88477..47896a1d7 100644 --- a/spot/twaalgos/emptiness.hh +++ b/spot/twaalgos/emptiness.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013-2018, 2020 Laboratoire de +// Copyright (C) 2011, 2013-2018, 2020-2021 Laboratoire de // Recherche et Developpement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -419,6 +419,9 @@ namespace spot /// this fragment with fewer edges than in the original cycle. /// (This step works best in Fin-less automata.) And then trying /// to find a shorter prefix leading to any state of the cycle. + /// + /// An std::runtime_error is thrown if the run + /// to reduce is not accepting. twa_run_ptr reduce() const; /// \brief Project an accepting run diff --git a/tests/python/except.py b/tests/python/except.py index f911474e8..0f653972d 100644 --- a/tests/python/except.py +++ b/tests/python/except.py @@ -134,6 +134,19 @@ except RuntimeError as e: else: report_missing_exception() +a = spot.translate('Fa') +a = spot.to_generalized_rabin(a, False) +r = a.accepting_run() +r = r.reduce() +assert r.cycle[0].acc == spot.mark_t([1]) +r.cycle[0].acc = spot.mark_t([0]) +try: + r.reduce(); +except RuntimeError as e: + assert "expects an accepting cycle" in str(e) +else: + report_missing_exception() + f = spot.formula('GF(a | Gb)') try: spot.gf_guarantee_to_ba(f, spot._bdd_dict) From d8a75518e45c7c0ff12a85b34cf9a21afdc473dc Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 7 Jul 2021 18:00:41 +0200 Subject: [PATCH 10/13] twa: fix intersecting_run on weak automata Fixes #471, reported by Cambridge Yang. * spot/twa/twa.cc (intersecting_run): Disable the product optimization for weak automata. * tests/python/471.py: New file. * tests/Makefile.am: Add it. * NEWS: Mention the bug. --- NEWS | 6 +++++- spot/twa/twa.cc | 11 +++++++++-- tests/Makefile.am | 1 + tests/python/471.py | 28 ++++++++++++++++++++++++++++ 4 files changed, 43 insertions(+), 3 deletions(-) create mode 100644 tests/python/471.py diff --git a/NEWS b/NEWS index 0ab85d0c2..11edc1717 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,10 @@ New in spot 2.9.7.dev (not yet released) - Nothing yet. + Bugs fixed: + + - left->intersacting_run(right) could return a run with incorrect + colors (likely not corresponding to any existing transition of + left) if left was a weak automaton. New in spot 2.9.7 (2021-05-12) diff --git a/spot/twa/twa.cc b/spot/twa/twa.cc index bebcbddfa..986aeb397 100644 --- a/spot/twa/twa.cc +++ b/spot/twa/twa.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2014-2019 Laboratoire de Recherche et Developpement de -// l'EPITA (LRDE). +// Copyright (C) 2011, 2014-2019, 2021 Laboratoire de Recherche et +// Developpement 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), Université Pierre // et Marie Curie. @@ -165,7 +165,14 @@ namespace spot { const_twa_graph_ptr g1 = ensure_existential_twa_graph(self); const_twa_graph_ptr g2 = ensure_existential_twa_graph(other); + // Reset g1.prop_weak() to disable the product optimization + // for weak automata, otherwise project(g1) would be unable to + // compute the correct marks. See issue #471. It's OK to + // optimize the right part if g2 is weak. + spot::trival g1weak = g1->prop_weak(); + std::const_pointer_cast(g1)->prop_weak(false); auto run = generic_accepting_run(product(g1, g2)); + std::const_pointer_cast(g1)->prop_weak(g1weak); if (!run) return nullptr; return run->reduce()->project(g1); diff --git a/tests/Makefile.am b/tests/Makefile.am index 63d58db16..d7bfda16f 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -364,6 +364,7 @@ TESTS_ipython = \ # with a _. TESTS_python = \ python/341.py \ + python/471.py \ python/_altscc.ipynb \ python/_autparserr.ipynb \ python/_aux.ipynb \ diff --git a/tests/python/471.py b/tests/python/471.py new file mode 100644 index 000000000..6fee3a2d3 --- /dev/null +++ b/tests/python/471.py @@ -0,0 +1,28 @@ +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2021 Laboratoire de Recherche et Développement de l'Epita +# (LRDE). +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +# Test for Issue #471. + +import spot +a = spot.translate('Fa') +a = spot.to_generalized_rabin(a, False) +r1 = a.intersecting_run(a) +r2 = a.accepting_run() +assert str(r1) == str(r2) +assert a.prop_weak().is_true() From 87022c23c61b64107585cc6ea2423fa88dc8be60 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 10 Aug 2021 13:37:33 +0200 Subject: [PATCH 11/13] * NEWS: Update for 2.9.8. --- NEWS | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index 11edc1717..cef3072d9 100644 --- a/NEWS +++ b/NEWS @@ -1,10 +1,21 @@ New in spot 2.9.7.dev (not yet released) + Documentation: + + - Mention the conda-forge package. + Bugs fixed: - left->intersacting_run(right) could return a run with incorrect colors (likely not corresponding to any existing transition of - left) if left was a weak automaton. + left) if left was a weak automaton. (Issue #471) + + - Fix bitset::operator-() causing issues when Spot was configured + with more than 32 colors for instance with --enable-max-sets=64. + (Issue #469) + + - Work around some warnings from newer compilers. + New in spot 2.9.7 (2021-05-12) From db0440f1fe4f5ac7ecd3321c1767bdeb22d1951d Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 10 Aug 2021 17:37:00 +0200 Subject: [PATCH 12/13] Release Spot 2.9.8 * NEWS, configure.ac, doc/org/setup.org: Bump version to 2.9.8. --- NEWS | 2 +- configure.ac | 2 +- doc/org/setup.org | 10 +++++----- 3 files changed, 7 insertions(+), 7 deletions(-) diff --git a/NEWS b/NEWS index cef3072d9..47ef6360c 100644 --- a/NEWS +++ b/NEWS @@ -1,4 +1,4 @@ -New in spot 2.9.7.dev (not yet released) +New in spot 2.9.8 (2021-08-10) Documentation: diff --git a/configure.ac b/configure.ac index 42a5e3627..2ec872133 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.dev], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.9.8], [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 809788d25..d5c0a0bcd 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.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 +#+MACRO: SPOTVERSION 2.9.8 +#+MACRO: LASTRELEASE 2.9.8 +#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.9.8.tar.gz][=spot-2.9.8.tar.gz=]] +#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-9-8/NEWS][summary of the changes]] +#+MACRO: LASTDATE 2021-08-10 #+ATTR_HTML: :id spotlogo [[file:spot2.svg]] From 3c7a2c9b4a8d1a42de65f1504a11173b612458d3 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 10 Aug 2021 17:38:54 +0200 Subject: [PATCH 13/13] Bump version to 2.9.8.dev * NEWS, configure.ac: Here. --- NEWS | 4 ++++ configure.ac | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index 47ef6360c..f2524e32d 100644 --- a/NEWS +++ b/NEWS @@ -1,3 +1,7 @@ +New in spot 2.9.8.dev (not yet released) + + Nothing yet. + New in spot 2.9.8 (2021-08-10) Documentation: diff --git a/configure.ac b/configure.ac index 2ec872133..38db6b0a7 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.8], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.9.8.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])