From 9b9c2b3c94fce6af1d1a1a684b33c2515aa66601 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 11 Dec 2019 19:46:17 +0100 Subject: [PATCH 01/10] * spot/twaalgos/compsusp.cc: Fix a warning from gcc-snapshot. --- spot/twaalgos/compsusp.cc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/spot/twaalgos/compsusp.cc b/spot/twaalgos/compsusp.cc index 36dbeb008..0d7b624ac 100644 --- a/spot/twaalgos/compsusp.cc +++ b/spot/twaalgos/compsusp.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2015, 2018 Laboratoire de Recherche et +// Copyright (C) 2012-2015, 2018, 2019 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -169,7 +169,7 @@ namespace spot // Copy all atomic propositions, except the one corresponding // to the variable v used for synchronization. int vn = bdd_var(v); - assert(dict->bdd_map[vn].type = bdd_dict::var); + assert(dict->bdd_map[vn].type == bdd_dict::var); formula vf = dict->bdd_map[vn].f; for (auto a: left->ap()) if (a != vf) From b9cac2cedb6ba72bdd79f3c90683a75bf433d459 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 12 Dec 2019 13:23:51 +0100 Subject: [PATCH 02/10] * spot/twaalgos/emptiness.cc: Fix another gcc-snapshot warning. --- spot/twaalgos/emptiness.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spot/twaalgos/emptiness.cc b/spot/twaalgos/emptiness.cc index 0f044c900..d07fd938f 100644 --- a/spot/twaalgos/emptiness.cc +++ b/spot/twaalgos/emptiness.cc @@ -848,7 +848,7 @@ namespace spot p.first->second = ns; if (names) { - assert(ns = names->size()); + assert(ns == names->size()); names->push_back(aut->format_state(next)); } } From 67b9bfda089b92bba432e342a31fdf60777b3de5 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 15 Dec 2019 16:10:05 +0100 Subject: [PATCH 03/10] tmpfile: improve error message * spot/misc/tmpfile.cc: Display strerror(errno) plus some suggestions that depend on the error. Based on a report from Shengping Shaw. * THANKS: Add reporter. * tests/core/ltlcross5.test: New file. * tests/Makefile.am: Add it. --- THANKS | 1 + spot/misc/tmpfile.cc | 26 ++++++++++++++-- tests/Makefile.am | 1 + tests/core/ltlcross5.test | 65 +++++++++++++++++++++++++++++++++++++++ 4 files changed, 91 insertions(+), 2 deletions(-) create mode 100644 tests/core/ltlcross5.test diff --git a/THANKS b/THANKS index 8fb1916d6..c3cc06999 100644 --- a/THANKS +++ b/THANKS @@ -41,6 +41,7 @@ Reuben Rowe Rüdiger Ehlers Silien Hong Simon Jantsch +Shengping Shaw Shufang Zhu Sonali Dutta Tereza Šťastná diff --git a/spot/misc/tmpfile.cc b/spot/misc/tmpfile.cc index 3f5842a98..b068d2abe 100644 --- a/spot/misc/tmpfile.cc +++ b/spot/misc/tmpfile.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2015, 2017, 2018 Laboratoire de Recherche et +// Copyright (C) 2013, 2015, 2017-2019 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -75,7 +75,29 @@ namespace spot fd = mkstemp(*name); } if (fd < 0) - throw std::runtime_error("failed to create "s + *name); + { + std::string err = ("failed to create temporary file "s + *name + + ": " + strerror(errno)); + if (errno == EACCES) + { + if (tmpdir) + err += ("\nConsider setting the SPOT_TMPDIR environment " + "variable to a writable directory."); + else + err += ("\nConsider executing this from a writable " + "directory, or setting\nthe SPOT_TMPDIR environment " + "variable to such a directory."); + } + else if (tmpdir) + { + const char* dir = + secure_getenv("SPOT_TMPDIR") ? "SPOT_TMPDIR" : "TMPDIR"; + err += ("\nNote that the directory comes from the "s + + dir + + " environment variable."); + } + throw std::runtime_error(err); + } return fd; } } diff --git a/tests/Makefile.am b/tests/Makefile.am index 309a28b58..f33ca5d2c 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -214,6 +214,7 @@ TESTS_twa = \ core/bdddict.test \ core/alternating.test \ core/ltlcross3.test \ + core/ltlcross5.test \ core/taatgba.test \ core/renault.test \ core/nondet.test \ diff --git a/tests/core/ltlcross5.test b/tests/core/ltlcross5.test new file mode 100644 index 000000000..82e9fdc89 --- /dev/null +++ b/tests/core/ltlcross5.test @@ -0,0 +1,65 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2019 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 . + +. ./defs +set -e + +unset TMPDIR +unset SPOT_TMPDIR + +mkdir foo +chmod a-w foo +cd foo +err=0 +if touch bar; then + # We are likely running as root, so we cannot detect permission + # issues. + cd .. + rm -rf foo + exit 77 +fi + +ltlcross ltl2tgba -f GFa 2>../err && err=1 +cd .. +cat err +grep 'failed to create temporary file' err || err=1 +grep 'executing this from a writable' err || err=1 +grep 'SPOT_TMPDIR' err || err=1 + +SPOT_TMPDIR=foo ltlcross ltl2tgba -f GFa 2>err && err=2 +cat err +grep 'failed to create temporary file' err || err=2 +grep 'executing this from a writable' err && err=2 +grep 'SPOT_TMPDIR' err + +chmod a+w foo +rmdir foo + +SPOT_TMPDIR=bar ltlcross ltl2tgba -f GFa 2>err && err=3 +cat err +grep 'failed to create temporary file' err +grep 'Note that the directory.*SPOT_TMPDIR ' err + +TMPDIR=bar ltlcross ltl2tgba -f GFa 2>err && err=4 +cat err +grep 'failed to create temporary file' err +grep 'Note that the directory.* TMPDIR ' err + +exit $err From 1f90e1cff97fb17557f079401463b1437bb0b344 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 26 Dec 2019 12:00:44 +0100 Subject: [PATCH 04/10] fix ltl2tgba -B not always returning Inf(0) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Reported by František Blahoudek. * spot/twaalgos/postproc.cc: Turn "t" into "Inf(0)" for BA. * tests/core/ltl2tgba.test: Add test case. * NEWS: Mention the bug. --- NEWS | 5 ++++- spot/twaalgos/postproc.cc | 11 +++++++++++ tests/core/ltl2tgba.test | 3 +++ 3 files changed, 18 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index 49c97731b..a9f71cc0a 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,9 @@ New in spot 2.8.4.dev (not yet released) - Nothing yet. + Bugs fixed: + + - ltl2tgba -B could return automata with "t" acceptance, instead + of the expected Inf(0). New in spot 2.8.4 (2019-12-08) diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc index ca639d952..6165ac834 100644 --- a/spot/twaalgos/postproc.cc +++ b/spot/twaalgos/postproc.cc @@ -163,6 +163,15 @@ namespace spot degen_lowinit_, degen_remscc_); } + static void + force_buchi(twa_graph_ptr& a) + { + assert(a->acc().is_t()); + acc_cond::mark_t m = a->set_buchi(); + for (auto& e: a->edges()) + e.acc = m; + } + twa_graph_ptr postprocessor::do_scc_filter(const twa_graph_ptr& a, bool arg) const { @@ -196,6 +205,8 @@ namespace spot tmp = SBACC_ ? do_degen(tmp) : do_degen_tba(tmp); if (SBACC_) tmp = sbacc(tmp); + if (type_ == BA && tmp->acc().is_t()) + force_buchi(tmp); if (want_parity) { reduce_parity_here(tmp, COLORED_); diff --git a/tests/core/ltl2tgba.test b/tests/core/ltl2tgba.test index ccb892f75..8417df485 100755 --- a/tests/core/ltl2tgba.test +++ b/tests/core/ltl2tgba.test @@ -292,3 +292,6 @@ test 2 = `ltl2tgba -f "$f" --low -x tls-impl=3 --stats=%s` # This is not optimal, the smallest DBA for this formula has 2 states. test 3 = `ltl2tgba -BD -f 'GF((p0 & GF!p0) | (!p0 & FGp0))' --stats=%s` + +# Some versions of Spot incorrectly returned "t" automata with -B +test "Inf(0)" = "`ltl2tgba -B 'Xb | G!b' --stats=%g`" From 383d1c003c5ca7218e0171599a220f455a528f98 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 28 Dec 2019 22:10:33 +0100 Subject: [PATCH 05/10] ltl2tgba, ltldo: fix location of --negate in --help output * bin/common_finput.cc, bin/ltl2tgba.cc, bin/ltldo.cc: Make sure --negate is listed along with input options. --- bin/common_finput.cc | 8 ++++---- bin/ltl2tgba.cc | 2 +- bin/ltldo.cc | 2 +- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/bin/common_finput.cc b/bin/common_finput.cc index 67e5a4353..a1abf5b91 100644 --- a/bin/common_finput.cc +++ b/bin/common_finput.cc @@ -37,16 +37,16 @@ static bool lenient = false; static const argp_option options[] = { { nullptr, 0, nullptr, 0, "Input options:", 1 }, - { "formula", 'f', "STRING", 0, "process the formula STRING", 1 }, + { "formula", 'f', "STRING", 0, "process the formula STRING", 0 }, { "file", 'F', "FILENAME[/COL]", 0, "process each line of FILENAME as a formula; if COL is a " "positive integer, assume a CSV file and read column COL; use " - "a negative COL to drop the first line of the CSV file", 1 }, + "a negative COL to drop the first line of the CSV file", 0 }, { "lbt-input", OPT_LBT, nullptr, 0, - "read all formulas using LBT's prefix syntax", 1 }, + "read all formulas using LBT's prefix syntax", 0 }, { "lenient", OPT_LENIENT, nullptr, 0, "parenthesized blocks that cannot be parsed as subformulas " - "are considered as atomic properties", 1 }, + "are considered as atomic properties", 0 }, { nullptr, 0, nullptr, 0, nullptr, 0 } }; diff --git a/bin/ltl2tgba.cc b/bin/ltl2tgba.cc index e24e7e856..f3de65a56 100644 --- a/bin/ltl2tgba.cc +++ b/bin/ltl2tgba.cc @@ -70,7 +70,7 @@ static const argp_option options[] = const struct argp_child children[] = { - { &finput_argp, 0, nullptr, 1 }, + { &finput_argp, 0, nullptr, 0 }, { &aoutput_argp, 0, nullptr, 0 }, { &aoutput_o_format_argp, 0, nullptr, 0 }, { &post_argp, 0, nullptr, 0 }, diff --git a/bin/ltldo.cc b/bin/ltldo.cc index f3e68c34b..fdb634450 100644 --- a/bin/ltldo.cc +++ b/bin/ltldo.cc @@ -153,7 +153,7 @@ ARGMATCH_VERIFY(errors_args, errors_types); const struct argp_child children[] = { { &hoaread_argp, 0, "Parsing of automata:", 3 }, - { &finput_argp, 0, nullptr, 1 }, + { &finput_argp, 0, nullptr, 0 }, { &trans_argp, 0, nullptr, 3 }, { &aoutput_argp, 0, nullptr, 6 }, { build_percent_list(), 0, nullptr, 7 }, From 265332dedf88c0ae0123e36dd01ef8e46a084f8e Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 31 Dec 2019 22:34:39 +0100 Subject: [PATCH 06/10] twagraph: merge_edge() can determinize automata MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Reported by František Blahoudek. * spot/twa/twagraph.cc: Reset prop_universal() if edges are merged in a non-deterministic automaton. * tests/core/det.test: Add test case. * NEWS: Mention the issue. --- NEWS | 9 +++++++++ spot/twa/twagraph.cc | 10 +++++++++- tests/core/det.test | 22 ++++++++++++++++++++++ 3 files changed, 40 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index a9f71cc0a..bfb505da0 100644 --- a/NEWS +++ b/NEWS @@ -5,6 +5,15 @@ New in spot 2.8.4.dev (not yet released) - ltl2tgba -B could return automata with "t" acceptance, instead of the expected Inf(0). + - twa_graph::merge_edges() (a.k.a. autfilt --merge-transitions) was + unaware that merging edges can sometimes transform a + non-deterministic automaton into a deterministic one, causing the + following unexpected diagnostic: + "print_hoa(): automaton is universal despite prop_universal()==false" + The kind of non-deterministic automata where this occurs is not + naturally produced by any Spot algorithm, but can be found for + instance in automata produced by Goal 2015-10-18. + New in spot 2.8.4 (2019-12-08) Bugs fixed: diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index 4c5218306..ee9fa13b9 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -148,7 +148,8 @@ namespace spot }); auto& trans = this->edge_vector(); - unsigned tend = trans.size(); + unsigned orig_size = trans.size(); + unsigned tend = orig_size; unsigned out = 0; unsigned in = 1; // Skip any leading false edge. @@ -233,6 +234,13 @@ namespace spot } g_.chain_edges_(); + + // Did we actually reduce the number of edges? + if (trans.size() != orig_size) + // Merging some edges may turn a non-deterministic automaton + // into a deterministic one. + if (prop_universal().is_false()) + prop_universal(trival::maybe()); } void twa_graph::merge_states() diff --git a/tests/core/det.test b/tests/core/det.test index f6080889f..e30f2b873 100755 --- a/tests/core/det.test +++ b/tests/core/det.test @@ -275,3 +275,25 @@ State: 1 --END-- EOF diff output expected + +# This is a syntactically non-deterministic automaton, which is +# semantically equivalent to a deterministic automaton (once +# transitions with compatible src/dst are merged). Running +# --merge-transition on this used to fail because merge_edges() would +# preserve the determism bit (or rather, the non-determinism bit). +cat >in.hoa < Date: Wed, 1 Jan 2020 16:20:28 +0100 Subject: [PATCH 07/10] bump copyright year * bin/common_setup.cc, debian/copyright: Here. --- bin/common_setup.cc | 4 ++-- debian/copyright | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/bin/common_setup.cc b/bin/common_setup.cc index dab5df571..b075bf48b 100644 --- a/bin/common_setup.cc +++ b/bin/common_setup.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2019 Laboratoire de Recherche et Développement +// Copyright (C) 2012-2020 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -35,7 +35,7 @@ display_version(FILE *stream, struct argp_state*) fputs(program_name, stream); fputs(" (" PACKAGE_NAME ") " PACKAGE_VERSION "\n\ \n\ -Copyright (C) 2019 Laboratoire de Recherche et Développement de l'Epita.\n\ +Copyright (C) 2020 Laboratoire de Recherche et Développement de l'Epita.\n\ License GPLv3+: \ GNU GPL version 3 or later .\n\ This is free software: you are free to change and redistribute it.\n\ diff --git a/debian/copyright b/debian/copyright index f292ed7d0..fb625c99e 100644 --- a/debian/copyright +++ b/debian/copyright @@ -4,7 +4,7 @@ Source: http://spot.lrde.epita.fr/dload/spot/ Files: * Copyright: 2003-2007 Laboratoire d'Informatique de Paris 6 (LIP6) - 2007-2019 Laboratoire de Recherche et Développement de l'Epita (LRDE) + 2007-2020 Laboratoire de Recherche et Développement de l'Epita (LRDE) License: GPL-3+ Spot is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by From 49bfefb46e1c8ec0f2f3195e1e9dbc91b16a6c6e Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 3 Jan 2020 15:22:05 +0100 Subject: [PATCH 08/10] ipnbdoctest: attempt to deal with buildfarm timeouts * tests/python/ipnbdoctest.py: Use shorter timeouts, and flush the shell messages without expecting them. --- tests/python/ipnbdoctest.py | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/tests/python/ipnbdoctest.py b/tests/python/ipnbdoctest.py index 20b69722f..26918a883 100755 --- a/tests/python/ipnbdoctest.py +++ b/tests/python/ipnbdoctest.py @@ -218,15 +218,15 @@ def _wait_for_ready_backport(kc): def run_cell(kc, cell): kc.execute(cell.source) - # wait for finish, maximum 30s - reply = kc.get_shell_msg(timeout=30) outs = [] while True: try: msg = kc.get_iopub_msg(timeout=1) except Empty: - break + if not kc.is_alive(): + raise RuntimeError("Kernel died") + continue msg_type = msg['msg_type'] content = msg['content'] @@ -253,6 +253,14 @@ def run_cell(kc, cell): content['output_type'] = msg_type outs.append(content) + # Flush shell channel + while True: + try: + kc.get_shell_msg(timeout=0.1) + except Empty: + if not kc.is_alive(): + raise RuntimeError("Kernel died") + break return outs @@ -268,7 +276,7 @@ def test_notebook(ipynb): kc.start_channels() try: - kc.wait_for_ready() + kc.wait_for_ready(timeout=30) except AttributeError: _wait_for_ready_backport(kc) From 68435915e79cde717ecda797ad3d743d51c65cb9 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 4 Jan 2020 14:19:10 +0100 Subject: [PATCH 09/10] Release Spot 2.8.5 * NEWS, configure.ac, doc/org/setup.org: Bump version number. --- NEWS | 2 +- configure.ac | 4 ++-- doc/org/setup.org | 10 +++++----- 3 files changed, 8 insertions(+), 8 deletions(-) diff --git a/NEWS b/NEWS index bfb505da0..4ea149b22 100644 --- a/NEWS +++ b/NEWS @@ -1,4 +1,4 @@ -New in spot 2.8.4.dev (not yet released) +New in spot 2.8.5 (2020-01-04) Bugs fixed: diff --git a/configure.ac b/configure.ac index 8782a1344..5ae7b5f05 100644 --- a/configure.ac +++ b/configure.ac @@ -1,5 +1,5 @@ # -*- coding: utf-8 -*- -# Copyright (C) 2008-2019, Laboratoire de Recherche et Développement +# Copyright (C) 2008-2020, Laboratoire de Recherche et Développement # de l'Epita (LRDE). # Copyright (C) 2003-2007 Laboratoire d'Informatique de Paris 6 # (LIP6), département Systèmes Répartis Coopératifs (SRC), Université @@ -21,7 +21,7 @@ # along with this program. If not, see . AC_PREREQ([2.63]) -AC_INIT([spot], [2.8.4.dev], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.8.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 3842728f4..183b78a74 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.8.4 -#+MACRO: LASTRELEASE 2.8.4 -#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.8.4.tar.gz][=spot-2.8.4.tar.gz=]] -#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-8-4/NEWS][summary of the changes]] -#+MACRO: LASTDATE 2019-12-08 +#+MACRO: SPOTVERSION 2.8.5 +#+MACRO: LASTRELEASE 2.8.5 +#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.8.5.tar.gz][=spot-2.8.5.tar.gz=]] +#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-8-5/NEWS][summary of the changes]] +#+MACRO: LASTDATE 2020-01-04 #+ATTR_HTML: :id spotlogo [[file:spot2.svg]] From d8ed0fb8ab45a19527bb13587e6eeeb423af2e1f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 4 Jan 2020 14:24:49 +0100 Subject: [PATCH 10/10] * NEWS, configure.ac: Bump version to 2.8.5.dev. --- NEWS | 4 ++++ configure.ac | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index 4ea149b22..d31ba4dff 100644 --- a/NEWS +++ b/NEWS @@ -1,3 +1,7 @@ +New in spot 2.8.5.dev (not yet released) + + Nothing yet. + New in spot 2.8.5 (2020-01-04) Bugs fixed: diff --git a/configure.ac b/configure.ac index 5ae7b5f05..b7f51b37a 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.8.5], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.8.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])