From 92369d68c633658df5d0bbbe67eab505d90bc315 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 8 Oct 2018 13:48:38 +0200 Subject: [PATCH 1/6] solve build issue on Debian unstable i386 * tests/python/_product_weak.ipynb: Split large loop in two cells. --- tests/python/_product_weak.ipynb | 45 +++++++++++++++++++++++++------- 1 file changed, 36 insertions(+), 9 deletions(-) diff --git a/tests/python/_product_weak.ipynb b/tests/python/_product_weak.ipynb index b5a233435..5defa2ef4 100644 --- a/tests/python/_product_weak.ipynb +++ b/tests/python/_product_weak.ipynb @@ -3398,7 +3398,22 @@ }, "metadata": {}, "output_type": "display_data" - }, + } + ], + "source": [ + "autslen = len(auts)\n", + "# We have trouble with Jupyter on i386, where running the full loop abort with some low-level \n", + "# exeptions from Jupyter client. \n", + "for left in auts[0:autslen//2]:\n", + " for right in auts:\n", + " display_inline(left, right, spot.product(left, right))" + ] + }, + { + "cell_type": "code", + "execution_count": 4, + "metadata": {}, + "outputs": [ { "data": { "text/html": [ @@ -6508,17 +6523,15 @@ } ], "source": [ - "for left in auts:\n", + "for left in auts[autslen//2:]:\n", " for right in auts:\n", " display_inline(left, right, spot.product(left, right))" ] }, { "cell_type": "code", - "execution_count": 4, - "metadata": { - "scrolled": false - }, + "execution_count": 5, + "metadata": {}, "outputs": [ { "data": { @@ -10137,7 +10150,21 @@ }, "metadata": {}, "output_type": "display_data" - }, + } + ], + "source": [ + "for left in auts[0:autslen//2]:\n", + " for right in auts:\n", + " display_inline(left, right, spot.product_or(left, right))" + ] + }, + { + "cell_type": "code", + "execution_count": 6, + "metadata": { + "scrolled": false + }, + "outputs": [ { "data": { "text/html": [ @@ -13363,7 +13390,7 @@ } ], "source": [ - "for left in auts:\n", + "for left in auts[autslen//2:]:\n", " for right in auts:\n", " display_inline(left, right, spot.product_or(left, right))" ] @@ -13392,7 +13419,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.6.5" + "version": "3.6.7rc1" } }, "nbformat": 4, From 68a155a818cdda6325e78ca156c42b9a5f08f0d6 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 12 Oct 2018 11:47:00 +0200 Subject: [PATCH 2/6] =?UTF-8?q?B=C3=BCchi=20translation=20should=20not=20g?= =?UTF-8?q?o=20through=20fg=5Fsafety=5Fto=5Fdca=5Fmaybe()?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Fixes #366, reported by Simon Jantsch. * spot/twaalgos/translate.cc: type_&Generic will also match if type_==BA... use type_==Generic instead. * tests/core/unambig.test: Add a test corresponding to Simon's report. * NEWS: Describe the bug. --- NEWS | 7 ++++++- spot/twaalgos/translate.cc | 3 ++- tests/core/unambig.test | 3 +++ 3 files changed, 11 insertions(+), 2 deletions(-) diff --git a/NEWS b/NEWS index b0642cf8f..7f33fbfa1 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,11 @@ New in spot 2.6.2.dev (not yet released) - Nothing yet. + Bugs fixed: + + - Running "ltl2tgba -B" on formulas of the type FG(safety) would + unexpectedly use a co-Büchi automaton as an intermediate step. + This in turn caused "ltl2tgba -U -B" to not produce unambiguous + automata. New in spot 2.6.2 (2018-09-28) diff --git a/spot/twaalgos/translate.cc b/spot/twaalgos/translate.cc index 806aa522b..a3c2a160c 100644 --- a/spot/twaalgos/translate.cc +++ b/spot/twaalgos/translate.cc @@ -322,7 +322,8 @@ namespace spot if (aut2 && ((type_ == BA) || (type_ & Parity)) && (pref_ & Deterministic)) return finalize(aut2); - if (!aut2 && (type_ & (Generic | Parity | CoBuchi))) + if (!aut2 && (type_ == Generic + || type_ & (Parity | CoBuchi))) { aut2 = fg_safety_to_dca_maybe(r, simpl_->get_dict(), sba); if (aut2 diff --git a/tests/core/unambig.test b/tests/core/unambig.test index 635ebc264..f90d6348f 100755 --- a/tests/core/unambig.test +++ b/tests/core/unambig.test @@ -26,6 +26,7 @@ for f in 'Ga' \ 'Ga | Gb' \ 'Ga | GFb' \ 'Ga | FGb' \ + 'F(Ga | Gb)' \ 'XFGa | GFb | Gc' \ '(Ga -> Gb) W c' \ 'F(a & !b & (!c W b))' \ @@ -33,6 +34,8 @@ for f in 'Ga' \ do ltl2tgba -UH "$f" | autfilt -q --is-unambiguous ltl2tgba -UH "!($f)" | autfilt -q --is-unambiguous + ltl2tgba -BUH "$f" | autfilt -q --is-unambiguous + ltl2tgba -BUH "!($f)" | autfilt -q --is-unambiguous ltl2tgba -UH "$f" | autfilt --check | grep -E 'properties:.* (unambiguous|deterministic)' ltl2tgba -UH "!($f)" | autfilt --check | From 34f9fb5d68d0f6f714017b2aec76d79454ee7316 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 12 Oct 2018 13:38:30 +0200 Subject: [PATCH 3/6] option --low should disable gf-guarantee Fixes #367. * spot/twaalgos/translate.cc, spot/twaalgos/translate.hh: Fix it. * NEWS: Mention the change. * tests/core/ltl2tgba2.test: Test this. --- NEWS | 3 +++ spot/twaalgos/translate.cc | 8 ++++++-- spot/twaalgos/translate.hh | 5 ++++- tests/core/ltl2tgba2.test | 6 ++++++ 4 files changed, 19 insertions(+), 3 deletions(-) diff --git a/NEWS b/NEWS index 7f33fbfa1..3db0ef002 100644 --- a/NEWS +++ b/NEWS @@ -7,6 +7,9 @@ New in spot 2.6.2.dev (not yet released) This in turn caused "ltl2tgba -U -B" to not produce unambiguous automata. + - ltl2tgba --low now disables the "gf-guarantee" feature, as + documented. + New in spot 2.6.2 (2018-09-28) Build: diff --git a/spot/twaalgos/translate.cc b/spot/twaalgos/translate.cc index a3c2a160c..baaa53e5f 100644 --- a/spot/twaalgos/translate.cc +++ b/spot/twaalgos/translate.cc @@ -36,7 +36,6 @@ namespace spot { comp_susp_ = early_susp_ = skel_wdba_ = skel_simul_ = 0; relabel_bool_ = tls_impl_ = -1; - gf_guarantee_ = level_ != Low; ltl_split_ = true; opt_ = opt; @@ -52,7 +51,12 @@ namespace spot skel_simul_ = opt->get("skel-simul", 1); } tls_impl_ = opt->get("tls-impl", -1); - gf_guarantee_ = opt->get("gf-guarantee", gf_guarantee_); + int gfg = opt->get("gf-guarantee", -1); + if (gfg >= 0) + { + gf_guarantee_ = !!gfg; + gf_guarantee_set_ = true; + } ltl_split_ = opt->get("ltl-split", 1); } diff --git a/spot/twaalgos/translate.hh b/spot/twaalgos/translate.hh index 7e4aadf9a..db65348dd 100644 --- a/spot/twaalgos/translate.hh +++ b/spot/twaalgos/translate.hh @@ -119,6 +119,8 @@ namespace spot delete simpl_owned_; build_simplifier(d); } + if (!gf_guarantee_set_) + gf_guarantee_ = level != Low; } /// \brief Convert \a f into an automaton. @@ -149,7 +151,8 @@ namespace spot int skel_simul_; int relabel_bool_; int tls_impl_; - bool gf_guarantee_; + bool gf_guarantee_ = true; + bool gf_guarantee_set_ = false; bool ltl_split_; const option_map* opt_; }; diff --git a/tests/core/ltl2tgba2.test b/tests/core/ltl2tgba2.test index 588e7b57e..a01e37c8e 100755 --- a/tests/core/ltl2tgba2.test +++ b/tests/core/ltl2tgba2.test @@ -381,6 +381,12 @@ ltl2tgba -Fformulas/1 --stats='%f, %s,%t' | diff formulas output +# Issue #367. +test 4 = `ltl2tgba 'GF(a<->XXa)' --stats=%s` +test 9 = `ltl2tgba --low 'GF(a<->XXa)' --stats=%s` +test 9 = `ltl2tgba -x gf-guarantee=0 'GF(a<->XXa)' --stats=%s` +test 4 = `ltl2tgba --low -x gf-guarantee=1 'GF(a<->XXa)' --stats=%s` + # Regression test for issue #357. The second formula used to # incorrectly produce 13 edges when translated after the first one # because the transition were explored in a different order. From 31bcb57648ebc757ddd4766475bc3451198737c9 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 15 Oct 2018 21:17:18 +0200 Subject: [PATCH 4/6] fix ltlfilt --accept-word and --reject-word * NEWS: Mention the issue. * bin/ltlfilt.cc: Fix test. * tests/core/acc_word.test: Test this. --- NEWS | 3 +++ bin/ltlfilt.cc | 9 ++++++++- tests/core/acc_word.test | 6 +++++- 3 files changed, 16 insertions(+), 2 deletions(-) diff --git a/NEWS b/NEWS index 3db0ef002..8a3791ef1 100644 --- a/NEWS +++ b/NEWS @@ -10,6 +10,9 @@ New in spot 2.6.2.dev (not yet released) - ltl2tgba --low now disables the "gf-guarantee" feature, as documented. + - ltlfilt's --accept-word and --reject-word options were ignored + unless used together. + New in spot 2.6.2 (2018-09-28) Build: diff --git a/bin/ltlfilt.cc b/bin/ltlfilt.cc index 460d31c13..626f59da4 100644 --- a/bin/ltlfilt.cc +++ b/bin/ltlfilt.cc @@ -83,6 +83,7 @@ enum { OPT_IGNORE_ERRORS, OPT_IMPLIED_BY, OPT_IMPLY, + OPT_LIVENESS, OPT_LTL, OPT_NEGATE, OPT_NNF, @@ -183,6 +184,8 @@ static const argp_option options[] = { "syntactic-stutter-invariant", OPT_SYNTACTIC_SI, nullptr, 0, "match stutter-invariant formulas syntactically (LTL-X or siPSL)", 0 }, { "nox", 0, nullptr, OPTION_ALIAS, nullptr, 0 }, + { "liveness", OPT_LIVENESS, nullptr, 0, + "match liveness properties", 0 }, { "safety", OPT_SAFETY, nullptr, 0, "match safety formulas (even pathological)", 0 }, { "guarantee", OPT_GUARANTEE, nullptr, 0, @@ -281,6 +284,7 @@ static bool negate = false; static bool boolean_to_isop = false; static bool unique = false; static bool psl = false; +static bool liveness = false; static bool ltl = false; static bool invert = false; static bool boolean = false; @@ -432,6 +436,9 @@ parse_opt(int key, char* arg, struct argp_state*) opt->imply = spot::formula::And({opt->imply, i}); break; } + case OPT_LIVENESS: + liveness = true; + break; case OPT_LTL: ltl = true; break; @@ -697,7 +704,7 @@ namespace { spot::twa_graph_ptr aut = nullptr; - if (!opt->acc_words.empty() && !opt->rej_words.empty()) + if (!opt->acc_words.empty() || !opt->rej_words.empty()) { aut = ltl_to_tgba_fm(f, simpl.get_dict(), true); diff --git a/tests/core/acc_word.test b/tests/core/acc_word.test index 9c8e46d64..47c09d611 100644 --- a/tests/core/acc_word.test +++ b/tests/core/acc_word.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2016, 2017 Laboratoire de Recherche et Développement +# Copyright (C) 2016, 2017, 2018 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -137,3 +137,7 @@ done ltl2tgba -G -D 'FGa' | autfilt --highlight-word='cycle{a}' 2>stderr && exit 1 test $? -eq 2 grep 'highlight-word.*Fin' stderr + + +ltlfilt -f 'GFa' --accept-word 'cycle{!a}' && exit 1 +ltlfilt -f 'GF!a' --accept-word 'cycle{!a}' From 44283adfc664959209d344514c8ca63413b72ad6 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 17 Oct 2018 09:27:22 +0200 Subject: [PATCH 5/6] Release Spot 2.6.3 * NEWS, configure.ac, doc/org/setup.org: Bump version. --- NEWS | 2 +- configure.ac | 2 +- doc/org/setup.org | 10 +++++----- 3 files changed, 7 insertions(+), 7 deletions(-) diff --git a/NEWS b/NEWS index 8a3791ef1..41fddb395 100644 --- a/NEWS +++ b/NEWS @@ -1,4 +1,4 @@ -New in spot 2.6.2.dev (not yet released) +New in spot 2.6.3 (2019-10-17) Bugs fixed: diff --git a/configure.ac b/configure.ac index 4ce96ea6e..fbff1f9b2 100644 --- a/configure.ac +++ b/configure.ac @@ -21,7 +21,7 @@ # along with this program. If not, see . AC_PREREQ([2.61]) -AC_INIT([spot], [2.6.2.dev], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.6.3], [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 3e505f3c7..5f0d58293 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 #+EMAIL: spot@lrde.epita.fr #+HTML_LINK_HOME: index.html -#+MACRO: SPOTVERSION 2.6.2 -#+MACRO: LASTRELEASE 2.6.2 -#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.6.2.tar.gz][=spot-2.6.2.tar.gz=]] -#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-6-2/NEWS][summary of the changes]] -#+MACRO: LASTDATE 2018-09-28 +#+MACRO: SPOTVERSION 2.6.3 +#+MACRO: LASTRELEASE 2.6.3 +#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.6.3.tar.gz][=spot-2.6.3.tar.gz=]] +#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-6-3/NEWS][summary of the changes]] +#+MACRO: LASTDATE 2018-10-17 #+ATTR_HTML: :id spotlogo [[file:spot2.svg]] From 1878e75ebc9522b8d3d1c859c823cfb83b1fa5b2 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 17 Oct 2018 09:34:09 +0200 Subject: [PATCH 6/6] bump version to 2.6.3.dev * NEWS, configure.ac: Here. --- NEWS | 4 ++++ configure.ac | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index 41fddb395..385cc5a39 100644 --- a/NEWS +++ b/NEWS @@ -1,3 +1,7 @@ +New in spot 2.6.3.dev (not yet released) + + Nothing yet. + New in spot 2.6.3 (2019-10-17) Bugs fixed: diff --git a/configure.ac b/configure.ac index fbff1f9b2..af25c4665 100644 --- a/configure.ac +++ b/configure.ac @@ -21,7 +21,7 @@ # along with this program. If not, see . AC_PREREQ([2.61]) -AC_INIT([spot], [2.6.3], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.6.3.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])