From df39000d8e3c0a331b6393793399596236392a27 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 16 Jul 2020 10:31:00 +0200 Subject: [PATCH 1/5] * doc/org/setup.org: Fix 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 d94c663e7..e2864a3dd 100644 --- a/doc/org/setup.org +++ b/doc/org/setup.org @@ -5,7 +5,7 @@ #+MACRO: LASTRELEASE 2.9.1 #+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.9.1.tar.gz][=spot-2.9.1.tar.gz=]] #+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-9-1/NEWS][summary of the changes]] -#+MACRO: LASTDATE 2020-04-30 +#+MACRO: LASTDATE 2020-07-15 #+ATTR_HTML: :id spotlogo [[file:spot2.svg]] From c7774ebb55377f754440e17c2ce2dfb92f16b9e1 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 16 Jul 2020 16:45:28 +0200 Subject: [PATCH 2/5] C++20: fix warnings reported by g++ 10.1 * spot/tl/formula.hh (formula::operator bool): Mark as noexcept. * bin/common_trans.hh, bin/common_trans.cc: Use std::atomic instead of volatile. --- bin/common_trans.cc | 6 +++--- bin/common_trans.hh | 7 ++++--- spot/tl/formula.hh | 2 +- 3 files changed, 8 insertions(+), 7 deletions(-) diff --git a/bin/common_trans.cc b/bin/common_trans.cc index e3df2316b..9c1f27a15 100644 --- a/bin/common_trans.cc +++ b/bin/common_trans.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015-2019 Laboratoire de Recherche et Développement +// Copyright (C) 2015-2020 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -457,12 +457,12 @@ autproc_runner::round_automaton(spot::const_twa_graph_ptr aut, unsigned serial) filename_automaton.new_round(aut, serial); } -volatile bool timed_out = false; +std::atomic timed_out{false}; unsigned timeout_count = 0; static unsigned timeout = 0; #if ENABLE_TIMEOUT -static volatile int alarm_on = 0; +static std::atomic alarm_on{0}; static int child_pid = -1; static void diff --git a/bin/common_trans.hh b/bin/common_trans.hh index d95350abc..e01131350 100644 --- a/bin/common_trans.hh +++ b/bin/common_trans.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015-2018 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2015-2018, 2020 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -21,6 +21,7 @@ #include "common_sys.hh" #include +#include #include #include @@ -165,7 +166,7 @@ public: # define ENABLE_TIMEOUT 0 #endif -extern volatile bool timed_out; +extern std::atomic timed_out; extern unsigned timeout_count; #if ENABLE_TIMEOUT void setup_sig_handler(); diff --git a/spot/tl/formula.hh b/spot/tl/formula.hh index 8b1340aaa..57cc8f91c 100644 --- a/spot/tl/formula.hh +++ b/spot/tl/formula.hh @@ -842,7 +842,7 @@ namespace spot return ptr_ != nullptr; } - operator bool() const + operator bool() const noexcept { return ptr_ != nullptr; } From ac5a261aa5dbd5bde84076d677b232f73b0b7cb3 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 20 Jul 2020 12:10:20 +0200 Subject: [PATCH 3/5] ltlcross: fix cross-checks for automata using Fin acceptance Fixes #420 reported by Salomon Sickert. * bin/ltlcross.cc: Call determine_unknown_acceptance(). * spot/twaalgos/sccinfo.cc, spot/twaalgos/sccinfo.hh: Document that one_accepting_scc()==-1 can mean "don't know", and update determine_unknown_acceptance() to set one_acc_scc_. * tests/core/ltlcross3.test: Add test case. * NEWS: Mention the fixes. --- NEWS | 9 ++++++++- bin/ltlcross.cc | 1 + spot/twaalgos/sccinfo.cc | 10 ++++++++-- spot/twaalgos/sccinfo.hh | 9 ++++++++- tests/core/ltlcross3.test | 5 +++++ 5 files changed, 30 insertions(+), 4 deletions(-) diff --git a/NEWS b/NEWS index debc196c7..af4287184 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,13 @@ New in spot 2.9.1.dev (not yet released) - Nothing yet. + Bugs fixed: + + - ltlcross --csv=... --product=N with N>0 could output spurious + diagnosics claiming that words were rejected when evaluating + the automaton on state-space. + + - spot::scc_info::determine_unknown_acceptance() now also update the + result of spot::scc_info::one_accepting_scc(). New in spot 2.9.1 (2020-07-15) diff --git a/bin/ltlcross.cc b/bin/ltlcross.cc index fd8deb228..784f06b2f 100644 --- a/bin/ltlcross.cc +++ b/bin/ltlcross.cc @@ -1568,6 +1568,7 @@ namespace sm = new spot::scc_info(p, spot::scc_info_options::TRACK_STATES); + sm->determine_unknown_acceptance(); } catch (const std::bad_alloc&) { diff --git a/spot/twaalgos/sccinfo.cc b/spot/twaalgos/sccinfo.cc index 024051bcb..74498c49f 100644 --- a/spot/twaalgos/sccinfo.cc +++ b/spot/twaalgos/sccinfo.cc @@ -472,9 +472,15 @@ namespace spot "does not support alternating automata"); auto& node = node_[s]; if (check_scc_emptiness(s)) - node.rejecting_ = true; + { + node.rejecting_ = true; + } else - node.accepting_ = true; + { + node.accepting_ = true; + if (one_acc_scc_ < 0) + one_acc_scc_ = s; + } changed = true; } } diff --git a/spot/twaalgos/sccinfo.hh b/spot/twaalgos/sccinfo.hh index a76ca3612..0b70b29d5 100644 --- a/spot/twaalgos/sccinfo.hh +++ b/spot/twaalgos/sccinfo.hh @@ -535,7 +535,14 @@ namespace spot return node_.size(); } - /// Return the number of one accepting SCC if any, -1 otherwise. + /// \brief Return the number of one accepting SCC if any, -1 otherwise. + /// + /// If an accepting SCC has been found, return its number. + /// Otherwise return -1. Note that when the acceptance condition + /// contains Fin, -1 does not implies that all SCCs are rejecting: + /// it just means that no accepting SCC is known currently. In + /// that case, you might want to call + /// determine_unknown_acceptance() first. int one_accepting_scc() const { return one_acc_scc_; diff --git a/tests/core/ltlcross3.test b/tests/core/ltlcross3.test index 430107239..652c9f88b 100755 --- a/tests/core/ltlcross3.test +++ b/tests/core/ltlcross3.test @@ -327,6 +327,11 @@ diff foo expected # This command used to crash. Report from František Blahoudek. run 0 ltlcross --verbose --no-checks -f 'FGa' 'ltl2tgba' +# In spot 2.9 and 2.9.1 the following command used to report a bug +# that did not exist. Issue #420. +ltlcross --csv=/dev/null ltl2tgba 'ltl2tgba -D -G' --states=5 \ + -f '(G(F(((a) & (X(X(a)))) | ((!(a)) & (X(X(!(a))))))))' + # The CSV file should not talk about product if --products=0 ltlcross --color --products=0 ltl2tgba -f GFa -f FGa --csv=out.csv grep product out.csv && exit 1 From 66a6fbdcb18871e9325d5f687f1db048f0e34fe2 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 21 Jul 2020 08:22:06 +0200 Subject: [PATCH 4/5] Release Spot 2.9.2 * configure.ac, NEWS, doc/org/setup.org: Set version to 2.9.2. --- NEWS | 2 +- configure.ac | 2 +- doc/org/setup.org | 10 +++++----- 3 files changed, 7 insertions(+), 7 deletions(-) diff --git a/NEWS b/NEWS index af4287184..f812b2b9e 100644 --- a/NEWS +++ b/NEWS @@ -1,4 +1,4 @@ -New in spot 2.9.1.dev (not yet released) +New in spot 2.9.2 (2020-07-21) Bugs fixed: diff --git a/configure.ac b/configure.ac index d9fefdac2..95e889659 100644 --- a/configure.ac +++ b/configure.ac @@ -21,7 +21,7 @@ # along with this program. If not, see . AC_PREREQ([2.63]) -AC_INIT([spot], [2.9.1.dev], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.9.2], [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 e2864a3dd..5fa99eb1f 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.1 -#+MACRO: LASTRELEASE 2.9.1 -#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.9.1.tar.gz][=spot-2.9.1.tar.gz=]] -#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-9-1/NEWS][summary of the changes]] -#+MACRO: LASTDATE 2020-07-15 +#+MACRO: SPOTVERSION 2.9.2 +#+MACRO: LASTRELEASE 2.9.2 +#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.9.2.tar.gz][=spot-2.9.2.tar.gz=]] +#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-9-2/NEWS][summary of the changes]] +#+MACRO: LASTDATE 2020-07-21 #+ATTR_HTML: :id spotlogo [[file:spot2.svg]] From d61d6570acc0f104155f297d9f1e12d5b4912415 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 21 Jul 2020 08:24:52 +0200 Subject: [PATCH 5/5] * NEWS, configure.ac: Bump version to 2.9.2.dev. --- NEWS | 4 ++++ configure.ac | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index f812b2b9e..9b98a5989 100644 --- a/NEWS +++ b/NEWS @@ -1,3 +1,7 @@ +New in spot 2.9.2.dev (not yet released) + + Nothing yet. + New in spot 2.9.2 (2020-07-21) Bugs fixed: diff --git a/configure.ac b/configure.ac index 95e889659..1aaef82c2 100644 --- a/configure.ac +++ b/configure.ac @@ -21,7 +21,7 @@ # along with this program. If not, see . AC_PREREQ([2.63]) -AC_INIT([spot], [2.9.2], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.9.2.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])