From fd92d20fd318a14dad04480824b7fe29b65b786f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 4 Jan 2020 17:59:45 +0100 Subject: [PATCH 01/12] ipnbdoctest: attempt to restart when the kernel dies * tests/python/ipnbdoctest.py: Catch kernel deaths, wait a random number of seconds, and try again up to three times. --- tests/python/ipnbdoctest.py | 20 ++++++++++++++++++-- 1 file changed, 18 insertions(+), 2 deletions(-) diff --git a/tests/python/ipnbdoctest.py b/tests/python/ipnbdoctest.py index 26918a883..5d7d00d10 100755 --- a/tests/python/ipnbdoctest.py +++ b/tests/python/ipnbdoctest.py @@ -18,6 +18,7 @@ import time import base64 import re import pprint +import random from difflib import unified_diff as diff from collections import defaultdict @@ -324,5 +325,20 @@ def test_notebook(ipynb): if __name__ == '__main__': for ipynb in sys.argv[1:]: - print("testing %s" % ipynb) - test_notebook(ipynb) + tries=3 + while tries: + print("testing %s" % ipynb) + try: + test_notebook(ipynb) + break + except RuntimeError as e: + # If the Kernel dies, try again. It seems we have spurious + # failures when multiple instances of jupyter start in parallel. + if 'Kernel died' in str(e): + tries -= 1 + if tries: + s = random.randint(1, 5) + print("trying again in", s, "seconds...") + time.sleep(s) + else: + raise e From abab62dd3e2ed24d4456870105f289ea072557cc Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 27 Jan 2020 22:52:32 +0100 Subject: [PATCH 02/12] * doc/org/concepts.org: Typo. --- doc/org/concepts.org | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/org/concepts.org b/doc/org/concepts.org index 05cc91863..c0b2bb9b4 100644 --- a/doc/org/concepts.org +++ b/doc/org/concepts.org @@ -683,7 +683,7 @@ newer Spin releases (starting with Spin 6.2.4) use the second syntax as they help Spin to produce more precise counterexamples. Spot can read and write never claims in both syntaxes, but it cannot -parse never claim that use other features (such as variables) of the +parse never claims that use other features (such as variables) of the Promela language. * LBTT's format From e7ae3d3ae05a511ec6fb89ee7ab3f577ac74d0c9 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 3 Feb 2020 15:38:51 +0100 Subject: [PATCH 03/12] fix degeneralize_tba after accepting transition * spot/twaalgos/degen.cc (degeneralize_tba): Here. * tests/python/simstate.py: Adjust expected values. * NEWS: Mention the bug. --- NEWS | 7 ++++++- spot/twaalgos/degen.cc | 2 +- tests/python/simstate.py | 6 ++++-- 3 files changed, 11 insertions(+), 4 deletions(-) diff --git a/NEWS b/NEWS index d31ba4dff..b4f51a0d8 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,11 @@ New in spot 2.8.5.dev (not yet released) - Nothing yet. + Bugs fixed: + + - degeneralize_tba() was incorrectly not honnoring the "skip_level" + optimization after creating an accepting transition; as a + consequence, some correct output could be larger than necessary + (but still correct). New in spot 2.8.5 (2020-01-04) diff --git a/spot/twaalgos/degen.cc b/spot/twaalgos/degen.cc index 397ec33da..cbbd372bc 100644 --- a/spot/twaalgos/degen.cc +++ b/spot/twaalgos/degen.cc @@ -580,7 +580,7 @@ namespace spot { d.second = 0; // Make it go to the first level. // Skip as many levels as possible. - if (!a->acc().accepting(acc) && !skip_levels) + if (!a->acc().accepting(acc) && skip_levels) { if (use_cust_acc_orders) { diff --git a/tests/python/simstate.py b/tests/python/simstate.py index e2bf5330e..8e5e1c712 100644 --- a/tests/python/simstate.py +++ b/tests/python/simstate.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2015, 2017-2018 Laboratoire de Recherche et Développement +# Copyright (C) 2015, 2017-2018, 2020 Laboratoire de Recherche et Développement # de l'Epita # # This file is part of Spot, a model checking library. @@ -169,7 +169,9 @@ State: 11 "{₀[1#1]{₁[0#0,0#1]{₂[1#0]₂}₁}₀}" a = spot.translate('!Gp0 xor FG((p0 W Gp1) M p1)') a = spot.degeneralize_tba(a) +assert a.num_states() == 8 b = spot.simulation(a) +assert b.num_states() == 3 b.set_init_state(1) b.purge_unreachable_states() b.copy_state_names_from(a) @@ -182,7 +184,7 @@ Acceptance: 1 Inf(0) properties: trans-labels explicit-labels trans-acc complete properties: deterministic stutter-invariant --BODY-- -State: 0 "[1,8,9]" +State: 0 "[1,7]" [!1] 0 {0} [1] 0 --END--""" From cf2cfcd2fbb8bc7920c011acdb768a86c3965314 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 10 Feb 2020 11:37:58 +0100 Subject: [PATCH 04/12] _postproc_translate_options: fix syntax error * python/spot/__init__.py: Here. * tests/python/except.py: Add test. * NEWS: Mention the issue. --- NEWS | 4 ++++ python/spot/__init__.py | 4 ++-- tests/python/except.py | 11 ++++++++++- 3 files changed, 16 insertions(+), 3 deletions(-) diff --git a/NEWS b/NEWS index b4f51a0d8..2670a741f 100644 --- a/NEWS +++ b/NEWS @@ -2,6 +2,10 @@ New in spot 2.8.5.dev (not yet released) Bugs fixed: + - calling spot.translate() with two conflicting preferences like + spot.translate(..., 'det', 'any') triggered a syntax error in the + Python code to handle this error. + - degeneralize_tba() was incorrectly not honnoring the "skip_level" optimization after creating an accepting transition; as a consequence, some correct output could be larger than necessary diff --git a/python/spot/__init__.py b/python/spot/__init__.py index cb7044fdf..3b31cefbf 100644 --- a/python/spot/__init__.py +++ b/python/spot/__init__.py @@ -1,5 +1,5 @@ # -*- coding: utf-8 -*- -# Copyright (C) 2014-2019 Laboratoire de +# Copyright (C) 2014-2020 Laboratoire de # Recherche et Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -622,7 +622,7 @@ def _postproc_translate_options(obj, default_type, *args): nonlocal pref_, pref_name_ if pref_ is not None and pref_name_ != val: raise ValueError("preference cannot be both {} and {}" - .format(pref_name, val)) + .format(pref_name_, val)) elif val == 'small': pref_ = postprocessor.Small elif val == 'deterministic': diff --git a/tests/python/except.py b/tests/python/except.py index f4ece980b..926aa864d 100644 --- a/tests/python/except.py +++ b/tests/python/except.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2018, 2019 Laboratoire de Recherche et Développement de +# Copyright (C) 2018-2020 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -179,3 +179,12 @@ except RuntimeError as e: assert "requires a semi-deterministic input" in str(e) else: report_missing_exception() + +try: + spot.translate('F(G(a | !a) & ((b <-> c) W d))', 'det', 'any') +except ValueError as e: + s = str(e) + assert 'det' in s + assert 'any' in s +else: + report_missing_exception() From 9365f8de1b47476145de0ff11d995c3cfd718474 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 10 Feb 2020 12:05:36 +0100 Subject: [PATCH 05/12] relabel: do not create automata with false labels * spot/twaalgos/relabel.cc: Remove false transitions if some of the propositions are equivalent to true or false. * NEWS: Mention the bug. * tests/core/ltl2tgba2.test: Test it. --- NEWS | 3 +++ spot/twaalgos/relabel.cc | 15 +++++++++++++-- tests/core/ltl2tgba2.test | 7 ++++++- 3 files changed, 22 insertions(+), 3 deletions(-) diff --git a/NEWS b/NEWS index 2670a741f..4e1ac9873 100644 --- a/NEWS +++ b/NEWS @@ -11,6 +11,9 @@ New in spot 2.8.5.dev (not yet released) consequence, some correct output could be larger than necessary (but still correct). + - Some formulas with Boolean sub-formulas equivalent to true or + false could be translated into automata with false labels. + New in spot 2.8.5 (2020-01-04) Bugs fixed: diff --git a/spot/twaalgos/relabel.cc b/spot/twaalgos/relabel.cc index 3d09136bc..dcdc7feae 100644 --- a/spot/twaalgos/relabel.cc +++ b/spot/twaalgos/relabel.cc @@ -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. // @@ -32,6 +32,7 @@ namespace spot std::set newvars; vars.reserve(relmap->size()); bool bool_subst = false; + bool need_cleanup = false; for (auto& p: *relmap) { @@ -61,6 +62,8 @@ namespace spot bdd newb = formula_to_bdd(p.second, d, aut); bdd_setbddpair(pairs, oldv, newb); bool_subst = true; + if (newb == bddtrue || newb == bddfalse) + need_cleanup = true; } } if (!bool_subst) @@ -76,5 +79,13 @@ namespace spot for (auto v: vars) if (newvars.find(v) == newvars.end()) aut->unregister_ap(v); + + // If some of the proposition are equivalent to true or false, + // it's possible that we have introduced edges with false labels. + if (need_cleanup) + { + aut->merge_edges(); // remove any edge labeled by 0 + aut->purge_dead_states(); // remove useless states + } } } diff --git a/tests/core/ltl2tgba2.test b/tests/core/ltl2tgba2.test index 8bcf2bc71..603e7294c 100755 --- a/tests/core/ltl2tgba2.test +++ b/tests/core/ltl2tgba2.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2009-2019 Laboratoire de Recherche et Développement de +# Copyright (C) 2009-2020 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 @@ -431,3 +431,8 @@ cat >expected < c) W d))' | grep '\[f\]' && exit 1 + +: From aad5b135eff7b877062506f613d7688c648cd65b Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 15 Feb 2020 10:05:27 +0100 Subject: [PATCH 06/12] fix is_generalized_rabin() and is_generalized_streett() * spot/twa/acc.cc: Fix detection of single-pairs gen-Rabin and gen-Streett. * tests/core/randaut.test: Add test case. * NEWS: Mention this issue. --- NEWS | 4 ++++ spot/twa/acc.cc | 34 ++++++++++++++++++++++++---------- tests/core/randaut.test | 10 +++++++++- 3 files changed, 37 insertions(+), 11 deletions(-) diff --git a/NEWS b/NEWS index 4e1ac9873..857254587 100644 --- a/NEWS +++ b/NEWS @@ -14,6 +14,10 @@ New in spot 2.8.5.dev (not yet released) - Some formulas with Boolean sub-formulas equivalent to true or false could be translated into automata with false labels. + - The HOA printer would incorrectly output the condition such + 'Fin(1) & Inf(2) & Fin(0)' as 'Fin(0) | Fin(1) & Inf(2)' + due to a bug in the is_generalized_rabin() matching function. + New in spot 2.8.5 (2020-01-04) Bugs fixed: diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc index a564c4968..d11535252 100644 --- a/spot/twa/acc.cc +++ b/spot/twa/acc.cc @@ -681,14 +681,20 @@ namespace spot // generalized Rabin should start with Or, unless // it has a single pair. + bool singlepair = false; { auto topop = code_.back().sub.op; if (topop == acc_op::And) - // Probably single-pair generalized-Rabin. Shift the source - // by one position as if we had an invisible Or in front. - ++s; + { + // Probably single-pair generalized-Rabin. Shift the source + // by one position as if we had an invisible Or in front. + ++s; + singlepair = true; + } else if (topop != acc_op::Or) - return false; + { + return false; + } } // Each pair is the position of a Fin followed @@ -752,7 +758,8 @@ namespace spot } for (auto i: p) pairs.emplace_back(i.second); - return (!(seen_fin & seen_inf) + return ((!singlepair || pairs.size() == 1) + && !(seen_fin & seen_inf) && (seen_fin | seen_inf) == all_sets()); } @@ -776,14 +783,20 @@ namespace spot // generalized Streett should start with And, unless // it has a single pair. + bool singlepair = false; { auto topop = code_.back().sub.op; if (topop == acc_op::Or) - // Probably single-pair generalized-Streett. Shift the source - // by one position as if we had an invisible And in front. - ++s; + { + // Probably single-pair generalized-Streett. Shift the source + // by one position as if we had an invisible And in front. + ++s; + singlepair = true; + } else if (topop != acc_op::And) - return false; + { + return false; + } } @@ -847,7 +860,8 @@ namespace spot } for (auto i: p) pairs.emplace_back(i.second); - return (!(seen_inf & seen_fin) + return ((!singlepair || pairs.size() == 1) + && !(seen_inf & seen_fin) && (seen_inf | seen_fin) == all_sets()); } diff --git a/tests/core/randaut.test b/tests/core/randaut.test index 6707eb050..ea432ec3f 100755 --- a/tests/core/randaut.test +++ b/tests/core/randaut.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2014, 2015, 2016, 2017, 2018 Laboratoire de Recherche et +# Copyright (C) 2014-2018, 2020 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -221,4 +221,12 @@ grep 'randaut:.*end of acceptance.*invalid range' stderr randaut -Q0 1 2>stderr && exit 1 grep '0 states' stderr +# This catch a bug where 'Fin(1) & Inf(2) & Fin(0)' was +# incorrectly detected a generalized-Rabin and output a +# 'Fin(0) | Fin(1) & Inf(2)'. +randaut -Q1 -A 'Fin(1) & Inf(2) & Fin(0)' 2 > out.hoa +grep 'Acceptance:' out.hoa > out.acc +echo 'Acceptance: 3 Fin(1) & Inf(2) & Fin(0)' > out.exp +diff out.acc out.exp + : From 80b04e10b547e13f6dd193df21496a0f36ccf45b Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 15 Feb 2020 15:42:12 +0100 Subject: [PATCH 07/12] update citations of generic emptiness-check * doc/org/citing.org, doc/spot.bib: Here. --- doc/org/citing.org | 10 +++++++++- doc/spot.bib | 7 +++---- 2 files changed, 12 insertions(+), 5 deletions(-) diff --git a/doc/org/citing.org b/doc/org/citing.org index b7e5f742f..bcd322024 100644 --- a/doc/org/citing.org +++ b/doc/org/citing.org @@ -70,10 +70,18 @@ be more specific about a particular aspect of Spot. - *Reactive Synthesis from LTL Specification with Spot*, /Thibaud Michaud/, /Maximilien Colange/. - In Proc. of SYNT@CAV'18. to appear. ([[https://www.lrde.epita.fr/~max/bibtexbrowser.php?key=michaud.18.synt&bib=perso.bib][bib]] | [[https://www.lrde.epita.fr/dload/papers/michaud.18.synt.pdf][pdf]]) + In Proc. of SYNT@CAV'18. ([[https://www.lrde.epita.fr/~max/bibtexbrowser.php?key=michaud.18.synt&bib=perso.bib][bib]] | [[https://www.lrde.epita.fr/dload/papers/michaud.18.synt.pdf][pdf]]) Presents the tool [[file:ltlsynt.org][=ltlsynt=]]. +- *Generic Emptiness Check for Fun and Profit*, + /Christel Baier/, /František Blahoudek/, /Alexandre Duret-Lutz/, + /Joachim Klein/, /David Müller/, and /Jan Strejček/. + In. Proc. of ATVA'19, LNCS 11781, pp. 11781, Oct 2019. ([[https://www.lrde.epita.fr/~adl/dl/adl_bib.html#baier.19.atva][bib]] | [[https://www.lrde.epita.fr/~adl/dl/adl/baier.19.atva.pdf][pdf]] | + [[https://www.lrde.epita.fr/~adl/dl/adl/baier.19.atva.slides.mefosyloma.pdf][slides1]] | [[https://www.lrde.epita.fr/~adl/dl/adl/baier.19.atva.slides.pdf][slides2]]) + + Presents the generic emptiness-check implemented in Spot. + * Obsolete reference - *Spot: an extensible model checking library using transition-based diff --git a/doc/spot.bib b/doc/spot.bib index f777ed604..bcb1452d4 100644 --- a/doc/spot.bib +++ b/doc/spot.bib @@ -40,12 +40,11 @@ Automated Technology for Verification and Analysis (ATVA'19)}, year = {2019}, - volume = {?????}, + volume = {11781}, series = {Lecture Notes in Computer Science}, - pages = {???--???}, + pages = {445--461}, month = oct, - publisher = {Springer}, - note = {To appear} + publisher = {Springer} } @InProceedings{ beer.01.cav, From de5704049d2de88cb20e44f34531e77ca831dc52 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 16 Feb 2020 08:20:21 +0100 Subject: [PATCH 08/12] tgba_determinize: improve citations in doc * doc/spot.bib (klein.07.ciaa, redziejowski.12.fi): Add two entries. * spot/twaalgos/determinize.hh: Use them. --- doc/spot.bib | 27 +++++++++++++++++++++++++++ spot/twaalgos/determinize.hh | 20 ++++++++++---------- 2 files changed, 37 insertions(+), 10 deletions(-) diff --git a/doc/spot.bib b/doc/spot.bib index bcb1452d4..027ec695a 100644 --- a/doc/spot.bib +++ b/doc/spot.bib @@ -1,3 +1,4 @@ + @InProceedings{ babiak.12.tacas, author = {Tom{\'a}{\v{s}} Babiak and Mojm{\'i}r K{\v{r}}et{\'i}nsk{\'y} and Vojt{\v{e}}ch {\v{R}}eh{\'a}k @@ -384,6 +385,21 @@ doi = {10.4204/EPTCS.229.10} } +@InCollection{ klein.07.ciaa, + year = {2007}, + booktitle = {Proceedings of the 12th International Conference on the + Implementation and Application of Automata (CIAA'07)}, + volume = {4783}, + series = {Lecture Notes in Computer Science}, + editor = {Jan Holub and Jan Žďárek}, + doi = {10.1007/978-3-540-76336-9_7}, + title = {On-the-Fly Stuttering in the Construction of Deterministic + $\omega$-Automata}, + publisher = {Springer}, + author = {Joachim Klein and Christel Baier}, + pages = {51--61} +} + @InProceedings{ kretisnky.12.cav, author = {Jan K{\v{r}}et{\'i}nsk{\'y} and Javier Esparza}, title = {Deterministic Automata for the {(F,G)}-Fragment of {LTL}}, @@ -585,6 +601,17 @@ url = {http://www.eda.org/vfv/} } +@Article{ redziejowski.12.fi, + author = {Roman Redziejowski}, + title = {An improved construction of deterministic omega-automaton + using derivatives}, + journal = {Fundamenta Informaticae}, + year = {2012}, + volume = {119}, + number = {3-4}, + pages = {393--496} +} + @InProceedings{ renault.13.tacas, author = {Etienne Renault and Alexandre Duret-Lutz and Fabrice Kordon and Denis Poitrenaud}, diff --git a/spot/twaalgos/determinize.hh b/spot/twaalgos/determinize.hh index ab0c993a5..c588ff9aa 100644 --- a/spot/twaalgos/determinize.hh +++ b/spot/twaalgos/determinize.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016, 2019 Laboratoire de Recherche et +// Copyright (C) 2015-2016, 2019-2020 Laboratoire de Recherche et // Développement de l'Epita. // // This file is part of Spot, a model checking library. @@ -34,20 +34,20 @@ namespace spot /// The output will be a deterministic automaton using parity acceptance. /// /// This procedure is based on an algorithm by Roman Redziejowski - /// (Fundamenta Informaticae 119, 3-4 (2012)). Redziejowski's - /// algorithm is similar to Piterman's improvement of Safra's - /// algorithm, except it is presented on transition-based acceptance - /// and use simpler notations. We implement three additional - /// optimizations (they can be individually disabled) based on + /// \cite redziejowski.12.fi . Redziejowski's algorithm is similar + /// to Piterman's improvement of Safra's algorithm, except it is + /// presented on transition-based acceptance and use simpler + /// notations. We implement three additional optimizations (they + /// can be individually disabled) based on /// /// - knowledge about SCCs of the input automaton /// - knowledge about simulation relations in the input automaton /// - knowledge about stutter-invariance of the input automaton /// - /// The last optimization is an idea described by Joachim Klein & - /// Christel Baier (CIAA'07) and implemented in ltl2dstar. In fact, - /// ltl2dstar even has a finer version (letter-based stuttering) - /// that is not implemented here. + /// The last optimization is an idea implemented in + /// [`ltl2dstar`](https://www.ltl2dstar.fr) \cite klein.07.ciaa . In + /// fact, `ltl2dstar` even has a finer version (letter-based + /// stuttering) that is not implemented here. /// /// \param aut the automaton to determinize /// From 05cf6683cea965ed9607b28eb626d3e1468e036d Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 16 Feb 2020 16:08:51 +0100 Subject: [PATCH 09/12] * tests/run.in: reset some envvars to avoid spurious failures. --- tests/run.in | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/tests/run.in b/tests/run.in index e7ca121b2..77d898e72 100755 --- a/tests/run.in +++ b/tests/run.in @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2010, 2011, 2014-2016, 2018, 2019 Laboratoire de Recherche +# Copyright (C) 2010-2011, 2014-2016, 2018-2020 Laboratoire de Recherche # et Developpement 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é @@ -61,6 +61,12 @@ export top_builddir top_srcdir='@abs_top_srcdir@' export top_srcdir +# Reset those variables, as they may affect the output of DOT. +SPOT_DOTEXTRA= +export SPOT_DOTEXTRA +SPOT_DOTDEFAULT= +export SPOT_DOTDEFAULT= + SPOT_UNINSTALLED=1 export SPOT_UNINSTALLED From 00cd9b7719135dda5c852e94aefcf92d634cc034 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 19 Feb 2020 10:40:40 +0100 Subject: [PATCH 10/12] doc: add DOIs to most citations * doc/spot.bib: Here. * doc/tl/tl.tex: Fix a citation. --- doc/spot.bib | 140 +++++++++++++++++++++++++++++++++----------------- doc/tl/tl.tex | 3 +- 2 files changed, 94 insertions(+), 49 deletions(-) diff --git a/doc/spot.bib b/doc/spot.bib index 027ec695a..87259d815 100644 --- a/doc/spot.bib +++ b/doc/spot.bib @@ -12,7 +12,8 @@ publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {7214}, - pages = {95--109} + pages = {95--109}, + doi = {10.1007/978-3-642-28756-5_8} } @InProceedings{ babiak.13.spin, @@ -45,7 +46,8 @@ series = {Lecture Notes in Computer Science}, pages = {445--461}, month = oct, - publisher = {Springer} + publisher = {Springer}, + doi = {10.1007/978-3-030-31784-3_26} } @InProceedings{ beer.01.cav, @@ -61,7 +63,8 @@ pages = {363--367}, volume = {2102}, year = {2001}, - month = jul + month = jul, + doi = {10.1007/3-540-44585-4_33} } @InProceedings{ benedikt.13.tacas, @@ -75,7 +78,8 @@ series = {Lecture Notes in Computer Science}, volume = {7795}, editor = {Nir Piterman and Scott A. Smolka}, - publisher = {Springer} + publisher = {Springer}, + doi = {10.1007/978-3-642-36742-7_3} } @Article{ boker.2011.fossacs, @@ -85,7 +89,8 @@ Structures - 14th International Conference, FOSSACS 2011}, year = {2011}, pages = {184--198}, - url = {http://www.cs.huji.ac.il/~ornak/publications/fossacs11b.pdf} + url = {http://www.cs.huji.ac.il/~ornak/publications/fossacs11b.pdf}, + doi = {10.1007/978-3-642-19805-2_13} } @Article{ bruggeman.96.tcs, @@ -94,7 +99,8 @@ journal = {Theoretical Computer Science}, year = {1996}, volume = {120}, - pages = {87--98} + pages = {87--98}, + doi = {10.1007/BFb0023820} } @Article{ carton.99.ita, @@ -104,7 +110,8 @@ year = {1999}, volume = {33}, number = {6}, - pages = {495--505} + pages = {495--505}, + url = {http://www.numdam.org/item/ITA_1999__33_6_495_0/} } @InProceedings{ cerna.03.mfcs, @@ -120,7 +127,8 @@ series = {Lecture Notes in Computer Science}, address = {Bratislava, Slovak Republic}, month = aug, - publisher = {Springer-Verlag} + publisher = {Springer-Verlag}, + doi = {10.1007/978-3-540-45138-9_26} } @InProceedings{ chang.92.icalp, @@ -131,7 +139,8 @@ year = {1992}, pages = {474--486}, publisher = {Springer-Verlag}, - address = {London, UK} + address = {London, UK}, + doi = {10.1007/3-540-55719-9_97} } @InProceedings{ cichon.09.depcos, @@ -142,7 +151,8 @@ Dependability of Computer Systems}, pages = {17--24}, year = 2009, - publisher = {IEEE Computer Society} + publisher = {IEEE Computer Society}, + doi = {10.1109/DepCoS-RELCOMEX.2009.31} } @Article{ cimatti.08.tcad, @@ -155,7 +165,8 @@ volume = 27, year = 2008, date = {2009-03-20}, - url = {https://es.fbk.eu/people/tonetta/tests/tcad07/} + url = {https://es.fbk.eu/people/tonetta/tests/tcad07/}, + doi = {10.1109/TCAD.2008.2003303} } @Article{ courcoubetis.92.fmsd, @@ -166,7 +177,8 @@ journal = {Formal Methods in System Design}, pages = {275--288}, year = {1992}, - volume = {1} + volume = {1}, + doi = {10.1007/BF00121128} } @InProceedings{ couvreur.99.fm, @@ -181,7 +193,8 @@ volume = {1708}, year = {1999}, month = sep, - isbn = {3-540-66587-0} + isbn = {3-540-66587-0}, + doi = {10.1007/3-540-48119-2_16} } @InProceedings{ dax.07.atva, @@ -197,7 +210,8 @@ (ATVA'07)}, editor = {Kedar S. Namjoshi and Tomohiro Yoneda and Teruo Higashino and Yoshio Okamura}, - month = oct + month = oct, + doi = {10.1007/978-3-540-75596-8_17} } @InProceedings{ dax.09.atva, @@ -211,7 +225,8 @@ year = {2009}, volume = {5799}, series = {Lecture Notes in Computer Science}, - publisher = {Springer-Verlag} + publisher = {Springer-Verlag}, + doi = {10.1007/978-3-642-04761-9_19} } @InProceedings{ duret.11.vecos, @@ -257,7 +272,8 @@ editor = {Mark Ardis}, month = mar, year = 1998, - pages = {7--15} + pages = {7--15}, + doi = {10.1145/298595.298598} } @Book{ eisner.06.psl, @@ -265,7 +281,8 @@ title = {A Practical Introduction to {PSL}}, publisher = {Springer}, year = {2006}, - series = {Series on Integrated Circuits and Systems} + series = {Series on Integrated Circuits and Systems}, + doi = {10.1007/978-0-387-36123-9} } @InCollection{ eisner.08.hvc, @@ -280,7 +297,8 @@ pages = {164--178}, volume = {5394}, year = {2009}, - month = oct + month = oct, + doi = {10.1007/978-3-642-01702-5_17} } @InProceedings{ etessami.00.concur, @@ -301,7 +319,8 @@ \url{http://www.bell-labs.com/project/TMP/} is fixed. We fixed the bug in Spot in 2005, thanks to LBTT. See also \url{http://arxiv.org/abs/1011.4214v2} for a discussion - about this problem.} + about this problem.}, + doi = {10.1007/3-540-44618-4_13} } @Article{ etessami.00.ipl, @@ -312,7 +331,8 @@ volume = {75}, number = {6}, year = {2000}, - pages = {261--263} + pages = {261--263}, + doi = {10.1016/S0020-0190(00)00113-7} } @InProceedings{ gastin.01.cav, @@ -325,7 +345,8 @@ editor = {G. Berry and H. Comon and A. Finkel}, volume = {2102}, series = {Lecture Notes in Computer Science}, - publisher = {Springer-Verlag} + publisher = {Springer-Verlag}, + doi = {10.1007/3-540-44585-4_6} } @InProceedings{ geldenhuys.04.tacas, @@ -341,7 +362,8 @@ publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2988}, - isbn = {3-540-21299-X} + isbn = {3-540-21299-X}, + doi = {10.1007/978-3-540-24730-2_18} } @InProceedings{ geldenhuys.06.spin, @@ -353,7 +375,8 @@ pages = {53--70}, series = {Lecture Notes in Computer Science}, volume = {3925}, - publisher = {Springer} + publisher = {Springer}, + doi = {10.1007/11691617_4} } @TechReport{ holevek.04.tr, @@ -363,7 +386,8 @@ month = {September}, year = 2004, number = 03, - institution = {CESNET} + institution = {CESNET}, + url = {http://archiv.cesnet.cz/doc/techzpravy/2004/verificationresults/} } @Book{ holzmann.91.book, @@ -371,7 +395,8 @@ title = {Design and Validation of Computer Protocols}, publisher = {Prentice-Hall}, address = {Englewood Cliffs, New Jersey}, - year = {1991} + year = {1991}, + isbn = {978-0-13-539925-5} } @InProceedings{ jacobs.16.synt, @@ -408,7 +433,6 @@ year = 2012, pages = {7--22}, doi = {10.1007/978-3-642-31424-7_7}, - url = {https://doi.org/10.1007/978-3-642-31424-7_7}, isbn = {978-3-642-31424-7}, publisher = {Springer} } @@ -435,7 +459,8 @@ pages = {408--429}, volume = {2}, number = {3}, - publisher = {ACM New York, NY, USA} + publisher = {ACM New York, NY, USA}, + doi = {10.1145/377978.377993} } @Article{ kupferman.05.tcl, @@ -461,7 +486,8 @@ pages = {83--100}, volume = {345}, number = {1}, - publisher = {Elsevier} + publisher = {Elsevier}, + doi = {10.1007/978-3-540-24730-2_43} } @InProceedings{ kupferman.10.mochart, @@ -486,7 +512,8 @@ and Connection to Second Order Logic}, school = {Institute of Computer Science and Applied Mathematics Christian-Albrechts-University of Kiel}, - year = {1998} + year = {1998}, + url = {https://old.automata.rwth-aachen.de/users/loeding/diploma_loeding.pdf} } @InProceedings{ loding.99.fstts, @@ -512,7 +539,8 @@ volume = {27}, number = {3}, pages = {163--182}, - month = aug + month = aug, + doi = {10.1016/0020-0255(82)90023-8} } @InProceedings{ manna.87.podc, @@ -524,7 +552,8 @@ location = {Quebec City, Canada}, pages = {377--410}, publisher = {ACM}, - address = {New York, NY, USA} + address = {New York, NY, USA}, + doi = {10.1145/93385.93442} } @InProceedings{ michaud.15.spin, @@ -538,7 +567,8 @@ series = {Lecture Notes in Computer Science}, volume = 9232, publisher = {Springer}, - month = aug + month = aug, + doi = {10.1007/978-3-319-23404-5_7} } @InProceedings{ minato.92.sasimi, @@ -550,7 +580,7 @@ pages = {64--73}, year = {1992}, address = {Kobe, Japan}, - month = {April} + month = apr } @InProceedings{ muller.17.gandalf, @@ -576,7 +606,8 @@ numpages = {5}, volume = {4595}, series = {Lecture Notes in Computer Science}, - publisher = {Springer-Verlag} + publisher = {Springer-Verlag}, + doi = {10.1007/978-3-540-73370-6_17} } @InProceedings{ piterman.06.vmcai, @@ -590,7 +621,8 @@ publisher = {Springer}, pages = {364--380}, volume = {3855}, - series = {Lecture Notes in Computer Science} + series = {Lecture Notes in Computer Science}, + doi = {10.1007/11609773_24} } @Book{ psl.04.lrm, @@ -609,7 +641,8 @@ year = {2012}, volume = {119}, number = {3-4}, - pages = {393--496} + pages = {393--406}, + doi = {10.3233/FI-2012-744} } @InProceedings{ renault.13.tacas, @@ -637,7 +670,8 @@ year = 2007, volume = {4595}, series = {Lecture Notes in Computer Science}, - publisher = {Springer-Verlag} + publisher = {Springer-Verlag}, + doi = {10.1007/978-3-540-73370-6_11} } @InProceedings{ schneider.01.lpar, @@ -651,7 +685,8 @@ volume = {2250}, series = {Lecture Notes in Artificial Intelligence}, address = {Havana, Cuba}, - publisher = {Springer-Verlag} + publisher = {Springer-Verlag}, + doi = {10.1007/3-540-45653-8_3} } @TechReport{ schwoon.04.tr, @@ -678,7 +713,8 @@ volume = {2860}, series = {Lectures Notes in Computer Science}, month = {October}, - publisher = {Springer-Verlag} + publisher = {Springer-Verlag}, + doi = {10.1007/978-3-540-39724-3_12} } @InProceedings{ sickert.16.cav, @@ -698,7 +734,7 @@ @InProceedings{ somenzi.00.cav, author = {Fabio Somenzi and Roderick Bloem}, - title = {Efficient {B\"u}chi Automata for {LTL} Formul{\ae}}, + title = {Efficient {B\"u}chi Automata for {LTL} Formulae}, booktitle = {Proceedings of the 12th International Conference on Computer Aided Verification (CAV'00)}, pages = {247--263}, @@ -706,7 +742,8 @@ volume = {1855}, series = {Lecture Notes in Computer Science}, address = {Chicago, Illinois, USA}, - publisher = {Springer-Verlag} + publisher = {Springer-Verlag}, + doi = {10.1007/10722167_21} } @Book{ systemverilog.18.std, @@ -728,7 +765,8 @@ volume = {6418}, series = {Lecture Notes in Computer Science}, month = nov, - publisher = {Springer} + publisher = {Springer}, + doi = {10.1007/978-3-642-16612-9_33} } @TechReport{ tauriainen.00.tr, @@ -741,7 +779,8 @@ number = {A66}, year = {2000}, type = {Research Report}, - note = {Reprint of Master's thesis} + note = {Reprint of Master's thesis}, + url = {http://www.tcs.hut.fi/Publications/A66.shtml} } @TechReport{ tauriainen.03.tr, @@ -756,7 +795,8 @@ Nondeterministic Automata}, type = {Research Report}, year = {2003}, - note = {Reprint of Licentiate's thesis} + note = {Reprint of Licentiate's thesis}, + url = {http://www.tcs.hut.fi/Publications/A83.shtml} } @TechReport{ tauriainen.06.tr, @@ -768,7 +808,8 @@ title = {Automata and Linear Temporal Logic: Translations with Transition-Based Acceptance}, type = {Research Report}, - year = {2006} + year = {2006}, + url = {http://www.tcs.hut.fi/Publications/A104.shtml} } @InProceedings{ thirioux.02.fmics, @@ -783,7 +824,8 @@ editor = {Rance Cleaveland and Hubert Garavel}, year = {2002}, month = jul, - address = {M{\'a}laga, Spain} + address = {M{\'a}laga, Spain}, + doi = {10.1016/S1571-0661(04)80409-2} } @InBook{ thomas.97.chapter, @@ -793,7 +835,8 @@ editor = {Grzegorz Rozenberg and Arto Salomaa}, chapter = 7, publisher = {Springer-Verlag}, - year = {1997} + year = {1997}, + doi = {10.1007/978-3-642-59126-6_7} } @Article{ zielonka.98.tcs, @@ -804,5 +847,6 @@ volume = {200}, number = {1}, pages = {135--183}, - year = {1998} + year = {1998}, + doi = {10.1016/S0304-3975(98)00009-7} } diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index d8b7d9d24..22ecc8776 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -16,6 +16,7 @@ %\usepackage{showlabels} \usepackage{tabulary} \usepackage[numbers]{natbib} +\usepackage{doi} \usepackage{rotating} \usepackage{booktabs} \usepackage{tikz} @@ -770,7 +771,7 @@ it for output. $b$ must be a Boolean formula. \end{align*} The following adds input support for the SVA concatenation (or delay) -operator~\cite{systemverilog.04.lrm}. The simplest equivalence are +operator~\cite{systemverilog.18.std}. The simplest equivalence are that $f \DELAY{0} g$, $f \DELAY{1} g$, $f \DELAY{2} g$ mean respectively $f \FUSION g$, $f \CONCAT g$, and $f \CONCAT \1\CONCAT g$, but the delay can be a range, and $f$ can be From 39fa829340d9aae71401c5c524ee303ab2c1e1cf Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 19 Feb 2020 14:44:55 +0100 Subject: [PATCH 11/12] Release Spot 2.8.6 * NEWS, configure.ac, doc/org/setup.org: Update 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 857254587..a615aa35d 100644 --- a/NEWS +++ b/NEWS @@ -1,4 +1,4 @@ -New in spot 2.8.5.dev (not yet released) +New in spot 2.8.6 (2020-02-19) Bugs fixed: diff --git a/configure.ac b/configure.ac index b7f51b37a..327e44bf7 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.dev], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.8.6], [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 183b78a74..ad1824c80 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.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 +#+MACRO: SPOTVERSION 2.8.6 +#+MACRO: LASTRELEASE 2.8.6 +#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.8.6.tar.gz][=spot-2.8.6.tar.gz=]] +#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-8-6/NEWS][summary of the changes]] +#+MACRO: LASTDATE 2020-02-19 #+ATTR_HTML: :id spotlogo [[file:spot2.svg]] From c98f82dc36afba8850a087593a16392ad7224a04 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 19 Feb 2020 14:47:34 +0100 Subject: [PATCH 12/12] * NEWS, configure.ac: Bump version to 2.8.6.dev. --- NEWS | 4 ++++ configure.ac | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index a615aa35d..96e9a68fa 100644 --- a/NEWS +++ b/NEWS @@ -1,3 +1,7 @@ +New in spot 2.8.6.dev (not yet released) + + Nothing yet. + New in spot 2.8.6 (2020-02-19) Bugs fixed: diff --git a/configure.ac b/configure.ac index 327e44bf7..a31561efc 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.6], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.8.6.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])