From 24a48c9f1e47cd22b064350f661b219ea66280c8 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 28 Sep 2019 08:11:51 +0200 Subject: [PATCH 01/13] debian: remove -flo workaround * debian/rules: Here. --- debian/rules | 13 ------------- 1 file changed, 13 deletions(-) diff --git a/debian/rules b/debian/rules index 05adcf1d0..b4b922d7e 100755 --- a/debian/rules +++ b/debian/rules @@ -45,17 +45,6 @@ PRO2SETUP = \ PYDEFAULT=$(shell py3versions --default) PYOTHERS=$(filter-out $(PYDEFAULT), $(shell py3versions --supported)) -# There seem to be a problem with unwinding of exception handling when -# the binaries are compiled with -flto. For instance in autfilt, -# argp_parse() calls the locally defined parse_opt() that calls -# remove_ap::add_ap() (in libspot). The latter may throw an -# exception, which should be caught in main(). However If autfilt is -# compiled with -flto, the exception never traverses argp. Moving -# the try/catch block inside parse_opt() also fixes this praticular -# problem, but who knows about other exceptions? So as a workaround, -# we simply disable -flto in bin/. -FLTOWORKAROUND = perl -pi -e s/-flto// bin/Makefile - # We want to build Spot twice: once to get profile data, and a second # time to use it. override_dh_auto_configure: @@ -63,14 +52,12 @@ override_dh_auto_configure: dh_auto_configure -- $(PRO1SETUP) $(LTOSETUP) \ --disable-devel --enable-optimizations \ --disable-static PYTHON=/usr/bin/$(PYDEFAULT) - $(FLTOWORKAROUND) dh_auto_build dh_auto_test make clean dh_auto_configure -- $(PRO2SETUP) $(LTOSETUP) \ --disable-devel --enable-optimizations \ --disable-static PYTHON=/usr/bin/$(PYDEFAULT) - $(FLTOWORKAROUND) override_dh_auto_install: fix-js dh_auto_install --destdir=$(CURDIR)/debian/tmp # Reconfigure for every other supported Python3 version, From 750fcca7b7b010e8927cbca0225f72b6b4fce49e Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 28 Sep 2019 13:57:05 +0200 Subject: [PATCH 02/13] debian: use local version of require.js * debian/control (spot-doc): Depends on libjs-requirejs. * debian/rules (fix-js): Replace uses. --- debian/control | 2 +- debian/rules | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/debian/control b/debian/control index 889b5870c..c104afe24 100644 --- a/debian/control +++ b/debian/control @@ -71,7 +71,7 @@ Description: functions for generating formulas and automata in Spot Package: spot-doc Section: doc Architecture: all -Depends: ${misc:Depends}, libjs-mathjax, libjs-jquery +Depends: ${misc:Depends}, libjs-mathjax, libjs-jquery, libjs-requirejs Description: documentation for Spot HTML and PDF documentation for Spot. diff --git a/debian/rules b/debian/rules index b4b922d7e..647c49429 100755 --- a/debian/rules +++ b/debian/rules @@ -103,6 +103,7 @@ override_dh_compress: fix-js: perl -pi -e 's|http://orgmode.org/mathjax/MathJax.js|file:///usr/share/javascript/mathjax/MathJax.js|' doc/userdoc/*.html + perl -pi -e 's|https://cdnjs.cloudflare.com/ajax/libs/require.js/.*/require.min.js|file:///usr/share/javascript/requirejs/require.min.js|' tests/python/*.html perl -pi -e 's|https://cdn.mathjax.org/mathjax/.*/MathJax.js|file:///usr/share/javascript/mathjax/MathJax.js|' tests/python/*.html doc/userdoc/*.html perl -pi -e 's|https://cdnjs.cloudflare.com/ajax/libs/mathjax/.*/MathJax.js|file:///usr/share/javascript/mathjax/MathJax.js|' tests/python/*.html doc/userdoc/*.html perl -pi -e 's|https://cdnjs.cloudflare.com/ajax/libs/jquery/2.0.3/jquery.min.js|file:///usr/share/javascript/jquery/jquery.min.js|' tests/python/*.html From b28c8a5973c8776bf25abf0d8a2bae6f96005213 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 28 Sep 2019 14:00:56 +0200 Subject: [PATCH 03/13] * debian/control (libspotgen0): Fix leading spaces in description. --- debian/control | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/debian/control b/debian/control index c104afe24..d2c037129 100644 --- a/debian/control +++ b/debian/control @@ -65,8 +65,8 @@ Section: science Suggests: libspot-dev Depends: ${shlibs:Depends}, ${misc:Depends}, libspot0 (>= ${source:Version}), libspot0 (<< ${source:Version}.1~) Description: functions for generating formulas and automata in Spot - Library for generating families of formulas and automata - taken from the literature. + Library for generating families of formulas and automata + taken from the literature. Package: spot-doc Section: doc From d15ce1a77355ebd9d63ea948af320ad63a778d4c Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 28 Sep 2019 21:27:03 +0200 Subject: [PATCH 04/13] * NEWS: Fix many typos. --- NEWS | 56 ++++++++++++++++++++++++++++---------------------------- 1 file changed, 28 insertions(+), 28 deletions(-) diff --git a/NEWS b/NEWS index 6ee7113fa..bfde8915e 100644 --- a/NEWS +++ b/NEWS @@ -18,7 +18,7 @@ New in spot 2.8.2 (2019-09-27) architecture dependent. - Various compilation issues. In particular, this release is the - first one that can be compiled (as pass tests) on a Raspberry PI. + first one that can be compiled (and pass tests) on a Raspberry PI. New in spot 2.8.1 (2019-07-18) @@ -67,13 +67,13 @@ New in spot 2.8 (2019-07-10) consistency-checks (they are unnecessary when all automata could be complemented and statistics were not required). - - genaut learned --m-nba=N to generate Max Michel's NBA familly. + - genaut learned --m-nba=N to generate Max Michel's NBA family. (NBAs with N+1 states whose determinized have at least N! states.) - Due to some new simplification of parity acceptance, the output of "ltl2tgba -P -D" is now using a minimal number of colors. This means that recurrence properties have an acceptance condition - among "Inf(0)", "t", or "f", and persistance properties have an + among "Inf(0)", "t", or "f", and persistence properties have an acceptance condition among "Fin(0)", "t", or "f". - ltldo and ltlcross learned shorthands to call the tools ltl2na, @@ -100,8 +100,8 @@ New in spot 2.8 (2019-07-10) 'ltldo ltl2dstar -f 'GFa -> GFb' | autfilt --small' produces 1 state instead of 4.) - - simulation-based reductions hae learned another trick to better - merge states from transiant SCCs. + - simulation-based reductions has learned another trick to better + merge states from transient SCCs. - acc_cond::top_disjuncts() and acc_cond::top_conjuncts() can be used to split an acceptance condition on the top-level & or |. @@ -112,7 +112,7 @@ New in spot 2.8 (2019-07-10) allows "autfilt [-D] --small" to minimize very-weak automata whenever they are found to represent obligation properties.) - - There is a new spot::scc_and_mark_filter objet that simplifies the + - There is a new spot::scc_and_mark_filter object that simplifies the creation of filters to restrict spot::scc_info to some particular SCC while cutting new SCCs on given acceptance sets. This is used by spot::generic_emptiness_check() when processing SCCs @@ -180,7 +180,7 @@ New in spot 2.8 (2019-07-10) - cleanup_parity() and colorize_parity() were cleaned up a bit, resulting in fewer colors used in some cases. In particular, - colorize_parity() learned that coloring transitiant edges does not + colorize_parity() learned that coloring transient edges does not require the introduction of a new color. - A new reduce_parity() function implements and generalizes the @@ -201,7 +201,7 @@ New in spot 2.8 (2019-07-10) Deprecation notices: - - The virtual function twa::intersecting_run() no longuer takes a + - The virtual function twa::intersecting_run() no longer takes a second "from_other" Boolean argument. This is a backward incompatibility only for code that overrides this function in a subclass. For backward compatibility with programs that simply @@ -215,7 +215,7 @@ New in spot 2.8 (2019-07-10) Bugs fixed: - - The gf_guarantee_to_ba() is relying on an inplace algorithm that + - The gf_guarantee_to_ba() is relying on an in-place algorithm that could produce a different number of edges for the same input in two different transition order. @@ -240,9 +240,9 @@ New in spot 2.7.5 (2019-06-05) Bugs fixed: - - spot::translator was not applying Boolean sub-formula rewritting + - spot::translator was not applying Boolean sub-formula rewriting by default unless a spot::option_map was passed. This caused some - C++ code for translating certains formulas to be noticeably slower + C++ code for translating certain formulas to be noticeably slower than the equivalent call to the ltl2tgba binary. - The remove_ap algorithm was preserving the "terminal property" of @@ -273,7 +273,7 @@ New in spot 2.7.3 (2019-04-19) --stats would output the \r as part of the %> sequence instead of ignoring it. - - Fix serious typo in removel_alternation() causing incorrect + - Fix serious typo in remove_alternation() causing incorrect output for some VWAA. Bug introduced in Spot 2.6. Documentation: @@ -331,8 +331,8 @@ New in spot 2.7.1 (2019-02-14) - Printing Kripke structures via print_hoa() will save state names. - - kripke_graph_ptr objects now honnor any "state-names" property - when formating states. + - kripke_graph_ptr objects now honor any "state-names" property + when formatting states. Bugs fixed: @@ -353,7 +353,7 @@ New in spot 2.7.1 (2019-02-14) - The product_susp() function used to multiply an automaton with a suspendable automaton could incorrectly build transition-based - automata when multipliying two state-based automata. This caused + automata when multiplying two state-based automata. This caused ltl2tgba to emit error messages such as: "automaton has transition-based acceptance despite prop_state_acc()==true". @@ -477,7 +477,7 @@ New in spot 2.7 (2018-12-11) Note that this you were relying on the fact that Jupyter calls repr() to display returned values, you may want to call print() - explicitely if you prefer the old representation. + explicitly if you prefer the old representation. - Fix compilation under Cygwin and Alpine Linux, both choking on undefined secure_getenv(). @@ -521,7 +521,7 @@ New in spot 2.6.2 (2018-09-28) - configure --disable-doxygen would actually enable it. - - Fix several warnings emited by the development version of GCC. + - Fix several warnings emitted by the development version of GCC. New in spot 2.6.1 (2018-08-04) @@ -542,7 +542,7 @@ New in spot 2.6.1 (2018-08-04) command-line tools.) - The spot::contains(a, b) function introduced in 2.6 was testing - a⊆b instead of a⊇b as one would expect. Infortunately the + a⊆b instead of a⊇b as one would expect. Unfortunately the documentation was also matching the code, so this is a backward incompatible change, but a short-lived one. @@ -596,7 +596,7 @@ New in spot 2.6 (2018-07-04) - ./configure --enable-max-accsets=N let you specify a maximum number of acceptance sets that Spot should support. The default - is still 32, but this limit is no longer hardcoded. Larger values + is still 32, but this limit is no longer hard-coded. Larger values will cost additional memory and time. - We know distribute RPM packages for Fedora 28. See @@ -679,7 +679,7 @@ New in spot 2.6 (2018-07-04) FG(a|b)|FG(!a|Xb)|FG(a|XXb)|FG(!a|XXXb) 170(2) 8(4) 8(4) 8(5) - For 'parity' output, the 'ltl-split' optimization just separates - obligation subformulas from the rest, where a determinization is + obligation sub-formulas from the rest, where a determinization is still performed. ltl2tgba -DP ltl3dra ltl2dpa 2.5 2.6 0.2.3 18.06 @@ -746,7 +746,7 @@ New in spot 2.6 (2018-07-04) that are not used in the automaton. - spot::contains() and spot::are_equivalent() can be used to - check language containement between two automata or formulas. + check language containment between two automata or formulas. They are most welcome in Python, since we used to redefine them every now and them. Some examples are shown in https://spot.lrde.epita.fr/ipynb/contains.html @@ -758,7 +758,7 @@ New in spot 2.6 (2018-07-04) https://spot.lrde.epita.fr/ipynb/contains.html - spot::complement_semidet(aut) is a new function that returns the - complement of aut, where aut is a semideterministic automaton. The + complement of aut, where aut is a semi-deterministic automaton. The function uses the NCSB complementation algorithm proposed by F. Blahoudek, M. Heizmann, S. Schewe, J. Strejček, and MH. Tsai (TACAS'16). @@ -772,7 +772,7 @@ New in spot 2.6 (2018-07-04) spot::minimize_wdba() was changed to produce an automaton recognizing a language that includes the original one. As a consequence spot::minimize_obligation() and - spot::is_wdba_realizable() now only need one containement check + spot::is_wdba_realizable() now only need one containment check instead of two. - Slightly improved log output for the SAT-based minimization @@ -788,7 +788,7 @@ New in spot 2.6 (2018-07-04) See https://spot.lrde.epita.fr/ipynb/alternation.html for some examples. - - Strings are now implicitely converted into formulas when passed + - Strings are now implicitly converted into formulas when passed as arguments to functions that expect formulas. Previously this was done only for a few functions. @@ -800,7 +800,7 @@ New in spot 2.6 (2018-07-04) - Python *.py and *.so files are now always installed into the same directory. This was an issue on systems like Fedora that separate - plateform-specific packages from non-plateform-specific ones. + platform-specific packages from non-platform-specific ones. - print_dot() will correctly escape strings containing \n in HTML mode. @@ -818,7 +818,7 @@ New in spot 2.6 (2018-07-04) - The type spot::acc_cond::mark_t has been overhauled and uses a custom bit-vector to represent acceptance sets instead of storing everything in a "unsigned int". This change is - to accomodate configure's --enable-max-accsets=N option and + to accommodate configure's --enable-max-accsets=N option and has several effect: * The following shortcuts are deprecated: @@ -840,7 +840,7 @@ New in spot 2.6 (2018-07-04) - The output of print_dot() now include the acceptance condition. Add option "A" (supported since version 2.4) to cancel that. - - Because genltl now supports LTL pattern with two argumens, using + - Because genltl now supports LTL pattern with two arguments, using --format=%L may output two comma-separated integer. This is an issue if you used to produce CSV files using for instance: genltl --format='%F,%L,%f' ... @@ -915,7 +915,7 @@ New in spot 2.5.1 (2018-02-20) - is_generalized_rabin() had a typo that caused some non-simplified acceptance conditions like Fin(0)|(Fin(0)&Inf(1)) to be - incorrectly detecteded as generalized-Rabin 2 0 1 and then output + incorrectly detected as generalized-Rabin 2 0 1 and then output as Fin(0)|(Fin(1)&Inf(2)) instead. Likewise for is_generalized_streett From 865427c73b05b663c4c80b292c53f43fdf1f282b Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 2 Oct 2019 09:34:18 +0200 Subject: [PATCH 05/13] python: remove workaround for swig 2.0.2 * python/spot/gen.i, python/spot/impl.i, python/spot/ltsmin.i: Here. --- python/spot/gen.i | 10 ++-------- python/spot/impl.i | 7 ------- python/spot/ltsmin.i | 10 ++-------- 3 files changed, 4 insertions(+), 23 deletions(-) diff --git a/python/spot/gen.i b/python/spot/gen.i index b3cc29769..190e00b8f 100644 --- a/python/spot/gen.i +++ b/python/spot/gen.i @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// Copyright (C) 2017-2019 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -17,12 +17,6 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . -%{ - // Workaround for SWIG 2.0.2 using ptrdiff_t but not including cstddef. - // It matters with g++ 4.6. -#include -%} - %module(package="spot", director="1") gen %include "std_string.i" diff --git a/python/spot/impl.i b/python/spot/impl.i index f205270f6..131e49a76 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -20,13 +20,6 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . -%{ - // Workaround for SWIG 2.0.2 using ptrdiff_t but not including cstddef. - // It matters with g++ 4.6. -#include -%} - - %module(package="spot", director="1") impl %include "std_shared_ptr.i" diff --git a/python/spot/ltsmin.i b/python/spot/ltsmin.i index c70da47f9..3eb051f3f 100644 --- a/python/spot/ltsmin.i +++ b/python/spot/ltsmin.i @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2016, 2017 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// Copyright (C) 2016-2017, 2019 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -17,12 +17,6 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . -%{ - // Workaround for SWIG 2.0.2 using ptrdiff_t but not including cstddef. - // It matters with g++ 4.6. -#include -%} - %module(package="spot", director="1") ltsmin %include "std_string.i" From 2960b8138c6315cf3d84b15f92f0fe21623233ab Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 2 Oct 2019 13:34:44 +0200 Subject: [PATCH 06/13] "import spot.foo" may now load "spot-extra/foo.py" This is needed for tcltl. * python/spot/__init__.py: Alter __path__ to add any spot-extra/ directory we find. * NEWS: Mention this. --- NEWS | 6 ++++++ python/spot/__init__.py | 10 ++++++++++ 2 files changed, 16 insertions(+) diff --git a/NEWS b/NEWS index bfde8915e..dc5fb277f 100644 --- a/NEWS +++ b/NEWS @@ -2,6 +2,12 @@ New in spot 2.8.2.dev (not yet released) Nothing yet. + Python: + + - Doing "import spot.foo" will now load any spot-extra/foo.py on + Python's search path. This can be used to install third-party + packages that want to behave as plugins for Spot. + New in spot 2.8.2 (2019-09-27) Command-line tools: diff --git a/python/spot/__init__.py b/python/spot/__init__.py index b8400427e..738070b67 100644 --- a/python/spot/__init__.py +++ b/python/spot/__init__.py @@ -36,6 +36,16 @@ if 'SPOT_UNINSTALLED' in os.environ: # into .libs/ __path__.extend(sys.path) +# We may have third-party plugins that want to be loaded as "spot.xxx", but +# that are installed in a different $prefix. This sets things so that any +# file that looks like spot-extra/xxx.py can be loaded with "import spot.xxx". +for path in sys.path: + if path not in __path__: + path += "/spot-extra" + if os.path.isdir(path): + __path__.append(path) + + from spot.impl import * from spot.aux import \ extend as _extend, \ From e864baf6e7ffc9c13d176a4eab826bb5aaf95653 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 7 Oct 2019 20:22:24 +0200 Subject: [PATCH 07/13] * bin/ltlsynt.cc: Typo. --- bin/ltlsynt.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index 8377b79d6..e92d36f2d 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -71,7 +71,7 @@ static const argp_option options[] = " propositions", 0}, /**************************************************/ { nullptr, 0, nullptr, 0, "Fine tuning:", 10 }, - { "algo", OPT_ALGO, "ds|sd|large", 0, + { "algo", OPT_ALGO, "ds|sd|lar", 0, "choose the algorithm for synthesis:\n" " - sd: split then determinize with Safra (default)\n" " - ds: determinize (Safra) then split\n" From 9e3827317249c08dfcfe87f37cfc80ecaa70f9d0 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 17 Oct 2019 11:51:37 +0200 Subject: [PATCH 08/13] trim: avoid the soon-to-be-deprecated std::ptr_fun Reported by Etienne Renault. * spot/priv/trim.cc: Simplify with a lambda. --- spot/priv/trim.cc | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) diff --git a/spot/priv/trim.cc b/spot/priv/trim.cc index ad8dbbf64..a5f6c9c50 100644 --- a/spot/priv/trim.cc +++ b/spot/priv/trim.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2018 Laboratoire de Recherche et Developpement +// Copyright (C) 2015, 2018, 2019 Laboratoire de Recherche et Developpement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -20,7 +20,6 @@ #include "config.h" #include #include -#include #include #include @@ -29,12 +28,9 @@ namespace spot void trim(std::string& str) { - str.erase(std::find_if(str.rbegin(), str.rend(), - std::not1(std::ptr_fun - (std::isspace))).base(), + auto not_space = [](unsigned char c){ return !std::isspace(c); }; + str.erase(std::find_if(str.rbegin(), str.rend(), not_space).base(), str.end()); - str.erase(str.begin(), - std::find_if(str.begin(), str.end(), - std::not1(std::ptr_fun(std::isspace)))); + str.erase(str.begin(), std::find_if(str.begin(), str.end(), not_space)); } } From f31864488b15f775b38a900538972cd3677221fd Mon Sep 17 00:00:00 2001 From: Etienne Renault Date: Thu, 17 Oct 2019 16:45:25 +0200 Subject: [PATCH 09/13] core: random_shuffle is deprecated and not portable * tests/core/parity.cc: Here. --- tests/core/parity.cc | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/tests/core/parity.cc b/tests/core/parity.cc index 28689c41f..4cb8256ef 100644 --- a/tests/core/parity.cc +++ b/tests/core/parity.cc @@ -127,8 +127,8 @@ generate_aut(const spot::bdd_dict_ptr& current_bdd) for (auto& t: LAST_AUT->edges()) { auto nb_acc = std::rand() % (num_sets - min + 1) + min; - std::random_shuffle(cont_sets[num_sets].begin(), - cont_sets[num_sets].end()); + spot::mrandom_shuffle(cont_sets[num_sets].begin(), + cont_sets[num_sets].end()); for (auto j = 0; j < nb_acc; ++j) SET_TR(t, cont_sets[num_sets][j]); } @@ -141,8 +141,8 @@ generate_aut(const spot::bdd_dict_ptr& current_bdd) for (auto& t: LAST_AUT->edges()) { auto nb_acc = std::rand() % (num_sets - min + 1) + min; - std::random_shuffle(cont_sets[num_sets].begin(), - cont_sets[num_sets].end()); + spot::mrandom_shuffle(cont_sets[num_sets].begin(), + cont_sets[num_sets].end()); for (auto j = 0; j < nb_acc; ++j) { auto value = cont_sets[num_sets][j] * 2 + even; From 0e681ed0609a48d231ad39180acdcecedbcc5c76 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 18 Oct 2019 11:25:43 +0200 Subject: [PATCH 10/13] acc: improve diagnostics for algorithms that use too many colors * spot/twa/acc.hh (acc_cond::mark_t): Diagnose mark_t with set numbers that are too larges. * tests/python/except.py: Adjust. * tests/core/acc.cc: Remove most of asserts, as those can be disabled, and adjust expected exception. --- spot/twa/acc.hh | 5 ++++- tests/core/acc.cc | 21 ++++++++++++++++----- tests/python/except.py | 2 +- 3 files changed, 21 insertions(+), 7 deletions(-) diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index cad84f7da..7e88609ed 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -102,7 +102,10 @@ namespace spot : mark_t(_value_t::zero()) { for (iterator i = begin; i != end; ++i) - set(*i); + if (SPOT_LIKELY(*i < SPOT_MAX_ACCSETS)) + set(*i); + else + report_too_many_sets(); } /// Create a mark_t from a list of set numbers. diff --git a/tests/core/acc.cc b/tests/core/acc.cc index 91e829724..74c32fa49 100644 --- a/tests/core/acc.cc +++ b/tests/core/acc.cc @@ -53,6 +53,17 @@ static void print(const std::vector>& res) } } +static void expect(const std::exception& e, const char* prefix) +{ + if (std::strncmp(e.what(), "Too many acceptance sets used.", + strlen(prefix))) + { + std::cerr << "exception: " << e.what() << '\n'; + std::cerr << "expected: " << prefix << '\n'; + abort(); + } +} + int main() { spot::acc_cond ac(4); @@ -189,7 +200,7 @@ int main() } catch (const std::runtime_error& e) { - assert(!std::strncmp(e.what(), "Too many acceptance sets used.", 30)); + expect(e, "Too many acceptance sets used."); } #if SPOT_DEBUG @@ -204,7 +215,7 @@ int main() } catch (const std::runtime_error& e) { - assert(!std::strncmp(e.what(), "Too many acceptance sets used.", 30)); + expect(e, "Too many acceptance sets used."); } try @@ -214,17 +225,17 @@ int main() } catch (const std::runtime_error& e) { - assert(!std::strncmp(e.what(), "Too many acceptance sets used.", 30)); + expect(e, "Too many acceptance sets used."); } +#endif try { spot::acc_cond::mark_t m{spot::acc_cond::mark_t::max_accsets()}; } catch (const std::runtime_error& e) { - assert(!std::strcmp(e.what(), "bit index is out of bounds")); + expect(e, "Too many acceptance sets used."); } -#endif return 0; } diff --git a/tests/python/except.py b/tests/python/except.py index 598d70b6a..f4ece980b 100644 --- a/tests/python/except.py +++ b/tests/python/except.py @@ -169,7 +169,7 @@ else: try: m = spot.mark_t([0, n, 1]) except RuntimeError as e: - assert "bit index is out of bounds" in str(e) + assert "Too many acceptance sets used. The limit is" in str(e) else: report_missing_exception() From 44a79b1b8966fe5d618c363203ac606268c3390a Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 19 Oct 2019 15:40:00 +0200 Subject: [PATCH 11/13] work around recent GraphViz bug in SVG scaling See https://gitlab.com/graphviz/graphviz/issues/1605. * python/spot/aux.py (str_to_svg): Invert the scale parameters if they are both greater than one. --- python/spot/aux.py | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) diff --git a/python/spot/aux.py b/python/spot/aux.py index 53d787e89..cd56d212b 100644 --- a/python/spot/aux.py +++ b/python/spot/aux.py @@ -27,6 +27,7 @@ import sys import os import errno import contextlib +import re def extend(*classes): @@ -44,6 +45,21 @@ def extend(*classes): return wrap +# Work around a bug introduced in GraphViz 2.42.x, where the scale +# parameter is inverted. https://gitlab.com/graphviz/graphviz/issues/1605 +# In our case, the scale parameters should both be <= 1, so we can +# detect when that is not the case. +svgscale_regex = re.compile('transform="scale\(([\d.]+) ([\d.]+)\) rotate') + +def _gvfix(matchobj): + xs = float(matchobj.group(1)) + ys = float(matchobj.group(2)) + if xs >= 1 and ys >= 1: + xs = 1/xs + ys = 1/ys + return 'transform="scale({} {}) rotate'.format(xs, ys) + + # Add a small LRU cache so that when we display automata into a # interactive widget, we avoid some repeated calls to dot for # identical inputs. @@ -70,7 +86,8 @@ def str_to_svg(str): ret = dot.wait() if ret: raise subprocess.CalledProcessError(ret, 'dot') - return stdout.decode('utf-8') + out = stdout.decode('utf-8') + return svgscale_regex.sub(_gvfix, out) def ostream_to_svg(ostr): From 7ece49479444fd2a6b118d0e80cebb032a8e4ed4 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 6 Nov 2019 09:54:29 +0100 Subject: [PATCH 12/13] release Spot 2.8.3 * NEWS, configure.ac, doc/org/setup.org: Set version to 2.8.3. --- NEWS | 9 +++++++-- configure.ac | 2 +- doc/org/setup.org | 10 +++++----- 3 files changed, 13 insertions(+), 8 deletions(-) diff --git a/NEWS b/NEWS index dc5fb277f..bf7710b7d 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,8 @@ -New in spot 2.8.2.dev (not yet released) +New in spot 2.8.3 (2019-11-06) - Nothing yet. + Build: + + - Minor portabilities improvements with C++17 deprecations. Python: @@ -8,6 +10,9 @@ New in spot 2.8.2.dev (not yet released) Python's search path. This can be used to install third-party packages that want to behave as plugins for Spot. + - Work around GraphViz bug #1605 in Jupyter notebooks. + https://gitlab.com/graphviz/graphviz/issues/1605 + New in spot 2.8.2 (2019-09-27) Command-line tools: diff --git a/configure.ac b/configure.ac index 407cda7c3..50a992dbc 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.2.dev], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.8.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 c70f965ac..3186a4481 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.2 -#+MACRO: LASTRELEASE 2.8.2 -#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.8.2.tar.gz][=spot-2.8.2.tar.gz=]] -#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-8-2/NEWS][summary of the changes]] -#+MACRO: LASTDATE 2019-09-27 +#+MACRO: SPOTVERSION 2.8.3 +#+MACRO: LASTRELEASE 2.8.3 +#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.8.3.tar.gz][=spot-2.8.3.tar.gz=]] +#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-8-3/NEWS][summary of the changes]] +#+MACRO: LASTDATE 2019-11-06 #+ATTR_HTML: :id spotlogo [[file:spot2.svg]] From 56e08af896a0b89536eb40b669e057011aed6c9a Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 6 Nov 2019 09:56:25 +0100 Subject: [PATCH 13/13] * NEWS, configure.ac: Bump version to 2.8.3.dev. --- NEWS | 4 ++++ configure.ac | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index bf7710b7d..218a4f22e 100644 --- a/NEWS +++ b/NEWS @@ -1,3 +1,7 @@ +New in spot 2.8.3.dev (not yet released) + + Nothing yet. + New in spot 2.8.3 (2019-11-06) Build: diff --git a/configure.ac b/configure.ac index 50a992dbc..c3ea84830 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.3], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.8.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])