From a266f726c647d720bb3bd98c72fcc72a95d5a986 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 7 Sep 2020 16:05:19 +0200 Subject: [PATCH 01/22] * doc/org/spot.css: Remove margin-bottom from pre.example. --- doc/org/spot.css | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/org/spot.css b/doc/org/spot.css index b4ab9c1e5..dd46b579c 100644 --- a/doc/org/spot.css +++ b/doc/org/spot.css @@ -18,7 +18,7 @@ body a{color:#008181} .outline-3 h3:before{content:"";position:absolute;z-index:-1;left:-.2em;bottom:-.05em;height:1.2em;width:1.2em;background-color:#ffe35e;border-radius:5px} pre.src{padding-top:8px;border-left-style:solid;border-color:#00adad;overflow:auto;margin-top:0;margin-bottom:0} pre.src-hoa{border-color:#d70079} -pre.example{border-left-style:solid;border-color:#d70079;margin-top:0;margin-bottom:0;position:relative;z-index:2} +pre.example{border-left-style:solid;border-color:#d70079;margin-top:0;position:relative;z-index:2} div.org-src-container+pre.example{border-top-width:1px;border-top-color:#ddd;border-top-style:dashed} div.org-src-container+div.org-src-container pre.src{border-top-width:1px;border-top-color:#ddd;border-top-style:dashed} div.org-src-container {margin-top:0;margin-bottom:0;position:relative;z-index:1} From af800182c529fc39fa450fe0dd3b49b26969d624 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 10 Sep 2020 11:22:24 +0200 Subject: [PATCH 02/22] minify SVG images if possible Fixes #422. * HACKING: mention svgo * doc/Makefile.am (dist-hook, stamp): Run svgo on produced SVGs. --- HACKING | 2 ++ doc/Makefile.am | 14 ++++++++++++-- 2 files changed, 14 insertions(+), 2 deletions(-) diff --git a/HACKING b/HACKING index 1b37af6aa..f41d7e274 100644 --- a/HACKING +++ b/HACKING @@ -53,6 +53,8 @@ only for certain operations (like releases): pandoc used during Debian packaging for the conversion of IPython notebooks to html + svgo for reducing SVG images before generating the tarball + (install with: npm install -g svgo) ltl2ba used in the generated documentation and the test suite ltl2dstar likewise ltl3dra likewise diff --git a/doc/Makefile.am b/doc/Makefile.am index 1a295ed5d..8c59630b4 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -1,5 +1,5 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2010-2011, 2013-2019 Laboratoire de Recherche et +## Copyright (C) 2010-2011, 2013-2020 Laboratoire de Recherche et ## Développement de l'Epita (LRDE). ## Copyright (C) 2003-2005 Laboratoire d'Informatique de Paris 6 ## (LIP6), département Systèmes Répartis Coopératifs (SRC), Université @@ -29,15 +29,25 @@ endif all-local: $(DOXY_STAMP) $(srcdir)/org-stamp -.PHONY: doc +.PHONY: doc svgo doc: -rm -f stamp $(MAKE) stamp +# We use SVGO only if it is available. +SVGO = if ! (svgo -v >/dev/null); then :; else svgo --disable=removeViewBox +SVGOEND = ; fi + +dist-hook: svgo +svgo: + $(SVGO) -f $(distdir)/userdoc $(SVGOEND) + + stamp: $(srcdir)/Doxyfile.in $(top_srcdir)/configure.ac $(MAKE) Doxyfile -rm -rf spot.html spot.latex $(DOXYGEN) + $(SVGO) -f spot.html $(SVGOEND) touch $@ spot.html spot.tag: stamp From 43e9050b8342a81e7bf0d82b374d8c85c1b577c8 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 10 Sep 2020 14:04:33 +0200 Subject: [PATCH 03/22] org: greatly reduce the size of satmin.svg * doc/org/satmin.tex: Use a plain background color instead of some hashed lines pattern. This reduces the size of the resulting SVG file from 1.9MB to 50kB after minification. * doc/org/satmin.org: Adjust to mention autfilt. --- doc/org/satmin.org | 3 ++- doc/org/satmin.tex | 34 +++++++++++++--------------------- 2 files changed, 15 insertions(+), 22 deletions(-) diff --git a/doc/org/satmin.org b/doc/org/satmin.org index 89c17317a..4ea80c8a0 100644 --- a/doc/org/satmin.org +++ b/doc/org/satmin.org @@ -249,7 +249,8 @@ The following figure (from our [[https://www.lrde.epita.fr/~adl/dl/adl/baarir.14 the processing chains that can be used to turn an LTL formula into a minimal DBA/DTBA/DTGBA. The blue area at the top describes =ltl2tgba -D -x sat-minimize=, while the purple area at the bottom corresponds -to =dstar2tgba -D -x stat-minimize=. +to =dstar2tgba -D -x stat-minimize= (but =autfilt= support similar +options). [[file:satmin.svg]] diff --git a/doc/org/satmin.tex b/doc/org/satmin.tex index 41d3afcb6..080f792fc 100644 --- a/doc/org/satmin.tex +++ b/doc/org/satmin.tex @@ -5,24 +5,18 @@ \usetikzlibrary{positioning} \usetikzlibrary{calc} \usetikzlibrary{shapes} -\usetikzlibrary{patterns} \usetikzlibrary{backgrounds} -\usetikzlibrary{shapes.callouts} \newcommand{\CF}{\ensuremath{\mathcal{F}}} -\newcommand{\pin}[1]{\tikz[baseline=0]\node[fill=yellow,draw,circle,thin,inner sep=0.5pt,above left] {\footnotesize #1};} - \begin{document} - +\scalebox{1.2}{ +\begin{tikzpicture}[shorten >=1pt,>=stealth',semithick,node distance=5.5mm] \tikzstyle{dstep}=[align=center,minimum height=3em] \tikzstyle{pstep}=[draw,dstep,drop shadow,fill=white] \tikzstyle{iostep}=[dstep,rounded corners=1mm] \tikzstyle{instep}=[iostep,fill=yellow!20] \tikzstyle{outstep}=[iostep,fill=green!20] \tikzstyle{errstep}=[iostep,fill=red!20] - -\scalebox{1.2}{ -\begin{tikzpicture}[shorten >=1pt,>=stealth',semithick,node distance=5.5mm] %\tikzset{callout/.style={ellipse callout, callout pointer arc=30, % callout absolute pointer={#1},fill=blue!30,draw}} %\tikzstyle{ @@ -32,7 +26,7 @@ \draw[->] (trans) -- (wdba); \node[pstep,right=of wdba.0] (simp) {simplify\\TGBA}; \draw[->] (wdba) -- node[above]{fail} (simp); -\node[instep,below=of trans,yshift=-2mm] (ltl1) {LTL\\formula}; +\node[instep,below=of trans,yshift=-4mm] (ltl1) {LTL\\formula}; \draw[->] (ltl1) -- (trans); \node[pstep,right=of simp,yshift=8mm,xshift=1mm] (degen) {degen\\to TBA}; @@ -50,7 +44,7 @@ \coordinate (turn) at ($(nottcong.-130 |- simp.0)$); \draw[->] (isdet) -- node[below right,at start]{det.} (turn); \draw[->] (tbadet2) -- node[right,pos=.6]{success} ($(tbadet2 |- turn)$); -\node[pstep,below=of tbadet.-125,yshift=-3mm] (dtbasat) {DTBA SAT\\minimization}; +\node[pstep,below=of tbadet.-125,yshift=-5mm] (dtbasat) {DTBA SAT\\minimization}; \node[pstep,below=of dtbasat,yshift=5mm] (dtgbasat) {DTGBA SAT\\minimization}; \draw[->] (turn) |- node[above left]{$m=1$} (dtbasat); \draw[->] (turn) |- node[above left]{$m>1$} (dtgbasat); @@ -61,7 +55,7 @@ \draw[->] (dtgbasat) -- (mindtgba); \draw[->] (dtbasat) -- (mindtba); -\node[pstep,below=of ltl1,yshift=-2mm,xshift=1mm] (ltl2dstar) {\texttt{ltl2dstar}\\(DRA)}; +\node[pstep,below=of ltl1,yshift=-3mm,xshift=1mm] (ltl2dstar) {\texttt{ltl2dstar}\\(DRA)}; \draw[->] (ltl1) -- ($(ltl1 |- ltl2dstar.90)$); \node[pstep,right=of ltl2dstar] (dra2dba) {attempt\\conversion\\to DBA}; \draw[->] (ltl2dstar) -- (dra2dba); @@ -77,23 +71,21 @@ \draw[->] (wdba2.160) -| node[below right,sloped]{success} (wdbaok); \begin{scope}[on background layer] -\coordinate (pt1) at ($(tbadet.north east)+(3mm,2mm)$); -\coordinate (pt2) at ($(mindtba.north east)+(3mm,0mm)$); -\coordinate (pt3) at ($(mindtgba.south east)+(0mm,-1mm)$); +\coordinate (pt1) at ($(tbadet.north east)+(3mm,3mm)$); +\coordinate (pt2) at ($(mindtba.north east)+(3mm,1mm)$); +\coordinate (pt3) at ($(mindtgba.south east)+(0mm,-2mm)$); \coordinate[xshift=1mm,yshift=1mm] (turn3) at (turn); -\path[pattern color=blue!30,pattern=north west lines] ($(trans.west |- pt1)$) |- (pt2) |- (pt3) -| (turn3) -| (pt1) -- cycle; +\path[fill=blue!30,opacity=.3,rounded corners=1mm] ($(trans.west |- pt1)$) ++ (-1mm,0) |- (pt2) -- (pt3 -| pt2) -| (turn3) -| (pt1) -- cycle; \node[below right] at ($(trans.west |- pt1)$) {\texttt{ltl2tgba}}; \coordinate[yshift=1mm,xshift=1mm] (pt4) at ($(pt2 -| turn3)$); -\coordinate[yshift=-3mm,xshift=-1mm] (pt5) at ($(dra2dba.south west)$); +\coordinate[yshift=-4mm,xshift=-1mm] (pt5) at ($(dra2dba.south west)$); \coordinate[yshift=1mm,xshift=-1mm] (pt6) at ($(dra2dba.north west)$); -\path[pattern color=blue!30!red!30,pattern=north east lines] (pt5) -| (pt4) -- ($(pt2) + (1mm,1mm)$) |- (pt6) -- cycle; -\node[above left,yshift=-1mm] at ($(pt5 -| pt4)$) {\texttt{dstar2tgba}}; +\path[fill=blue!30!red!30,opacity=.3,rounded corners=1mm] (pt5) -| (pt4) -- ($(pt2) + (1mm,1mm)$) |- (pt6) -- cycle; +\node[above left,yshift=-1mm] at ($(pt5 -| pt4)$) {\texttt{dstar2tgba}/\texttt{autfilt}}; \end{scope} - -%\node[fill=yellow,draw,ellipse callout,thin,inner sep=0.5pt,callout pointer arc=30,,yshift=6mm,callout absolute pointer={(c1)}] at (c1) {\footnotesize 1}; - +%\draw[red] (current bounding box.north west) rectangle (current bounding box.south east); \end{tikzpicture}} \end{document} %%% Local Variables: From b5c20f72f6d347d32b40f5ce11793c999e28654b Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 11 Sep 2020 10:06:48 +0200 Subject: [PATCH 04/22] i386 Debian builds need x86 builders * .gitlab-ci.yml: split the amd64/i386 debian builds so we can tag the latter with x86. --- .gitlab-ci.yml | 70 +++++++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 63 insertions(+), 7 deletions(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 11ae8fb7b..277fabbc3 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -1,5 +1,6 @@ stages: - build + - build2 - publish debian-stable-gcc: @@ -178,12 +179,10 @@ debpkg-stable: - stable script: - docker pull gitlab-registry.lrde.epita.fr/spot/buildenv/debian:stable - - docker pull gitlab-registry.lrde.epita.fr/spot/buildenv/debian-i386:stable - vol=spot-stable-$CI_COMMIT_SHA - docker volume create $vol - exitcode=0 - docker run --rm=true -v $vol:/build/result registry.lrde.epita.fr/spot-debuild:stable ./build-spot.sh $CI_COMMIT_REF_NAME -j${NBPROC-1} || exitcode=$? - - docker run --rm=true -v $vol:/build/result registry.lrde.epita.fr/spot-debuild-i386:stable ./bin-spot.sh -j${NBPROC-1} || exitcode=$? - docker run -v $vol:/build/result --name helper-$vol registry.lrde.epita.fr/spot-debuild:stable true || exitcode=$? - docker cp helper-$vol:/build/result _build_stable || exitcode=$? - docker rm helper-$vol || exitcode=$? @@ -192,6 +191,36 @@ debpkg-stable: - exit $exitcode artifacts: when: always + expire_in: 1 week + paths: + - _build_stable/ + +debpkg-stable-i386: + stage: build2 + only: + - /-deb$/ + - master + - next + - stable + tags: ["x86"] + needs: ["debpkg-stable"] + script: + - docker pull gitlab-registry.lrde.epita.fr/spot/buildenv/debian-i386:stable + - vol=spot-stable-$CI_COMMIT_SHA + - docker volume create $vol + - exitcode=0 + - docker create -v $vol:/build/result --name helper-$vol registry.lrde.epita.fr/spot-debuild-i386:stable ./bin-spot.sh -j${NBPROC-1} || exitcode=$? + - docker cp _build_stable/. helper-$vol:/build/result || exitcode=$? + - rm -rf _build_stable + - docker start -a helper-$vol || exitcode=$? + - docker cp helper-$vol:/build/result _build_stable || exitcode=$? + - docker rm helper-$vol || exitcode=$? + - docker volume rm $vol || exitcode=$? + - ls -l _build_stable + - exit $exitcode + artifacts: + when: always + expire_in: 1 week paths: - _build_stable/ @@ -206,9 +235,7 @@ debpkg-unstable: - vol=spot-unstable-$CI_COMMIT_SHA - docker volume create $vol - exitcode=0 - - docker run --rm=true -v $vol:/build/result registry.lrde.epita.fr/spot-debuild ./build-spot.sh $CI_COMMIT_REF_NAME -j${NBPROC-1} || exitcode=$? - - docker run --rm=true -v $vol:/build/result registry.lrde.epita.fr/spot-debuild-i386 ./bin-spot.sh -j${NBPROC-1} || exitcode=$? - - docker run -v $vol:/build/result --name helper-$vol registry.lrde.epita.fr/spot-debuild true || exitcode=$? + - docker run -v $vol:/build/result --name helper-$vol registry.lrde.epita.fr/spot-debuild ./build-spot.sh $CI_COMMIT_REF_NAME -j${NBPROC-1} || exitcode=$? - docker cp helper-$vol:/build/result _build_unstable || exitcode=$? - docker rm helper-$vol || exitcode=$? - docker volume rm $vol || exitcode=$? @@ -216,6 +243,34 @@ debpkg-unstable: - exit $exitcode artifacts: when: always + expire_in: 1 week + paths: + - _build_unstable/ + +debpkg-unstable-i386: + stage: build2 + only: + - /-deb$/ + - next + tags: ["x86"] + needs: ["debpkg-unstable"] + script: + - docker pull gitlab-registry.lrde.epita.fr/spot/buildenv/debian-i386 + - vol=spot-unstable-$CI_COMMIT_SHA + - docker volume create $vol + - exitcode=0 + - docker create -v $vol:/build/result --name helper-$vol registry.lrde.epita.fr/spot-debuild-i386 ./bin-spot.sh -j${NBPROC-1} || exitcode=$? + - docker cp _build_unstable/. helper-$vol:/build/result || exitcode=$? + - rm -rf _build_unstable + - docker start -a helper-$vol || exitcode=$? + - docker cp helper-$vol:/build/result _build_unstable || exitcode=$? + - docker rm helper-$vol || exitcode=$? + - docker volume rm $vol || exitcode=$? + - ls -l _build_unstable + - exit $exitcode + artifacts: + when: always + expire_in: 1 week paths: - _build_unstable/ @@ -238,6 +293,7 @@ rpm-pkg: - mv ~/rpmbuild/RPMS/x86_64/*.rpm . artifacts: when: always + expire_in: 1 week paths: - ./*.rpm @@ -261,7 +317,7 @@ publish-stable: - dput stage: publish dependencies: - - debpkg-stable + - debpkg-stable-i386 script: - cd _build_stable - ls -l @@ -277,7 +333,7 @@ publish-unstable: - dput stage: publish dependencies: - - debpkg-unstable + - debpkg-unstable-i386 script: - cd _build_unstable - ls -l From b30521351b9bf993c704aa2064cb68ce6ccc6cfa Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 13 Sep 2020 10:57:50 +0200 Subject: [PATCH 05/22] * .gitlab-ci.yml: Fix images names. --- .gitlab-ci.yml | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 277fabbc3..6ff116f55 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -182,7 +182,7 @@ debpkg-stable: - vol=spot-stable-$CI_COMMIT_SHA - docker volume create $vol - exitcode=0 - - docker run --rm=true -v $vol:/build/result registry.lrde.epita.fr/spot-debuild:stable ./build-spot.sh $CI_COMMIT_REF_NAME -j${NBPROC-1} || exitcode=$? + - docker run --rm=true -v $vol:/build/result gitlab-registry.lrde.epita.fr/spot/buildenv/debian:stable ./build-spot.sh $CI_COMMIT_REF_NAME -j${NBPROC-1} || exitcode=$? - docker run -v $vol:/build/result --name helper-$vol registry.lrde.epita.fr/spot-debuild:stable true || exitcode=$? - docker cp helper-$vol:/build/result _build_stable || exitcode=$? - docker rm helper-$vol || exitcode=$? @@ -209,7 +209,7 @@ debpkg-stable-i386: - vol=spot-stable-$CI_COMMIT_SHA - docker volume create $vol - exitcode=0 - - docker create -v $vol:/build/result --name helper-$vol registry.lrde.epita.fr/spot-debuild-i386:stable ./bin-spot.sh -j${NBPROC-1} || exitcode=$? + - docker create -v $vol:/build/result --name helper-$vol gitlab-registry.lrde.epita.fr/spot/buildenv/debian-i386:stable ./bin-spot.sh -j${NBPROC-1} || exitcode=$? - docker cp _build_stable/. helper-$vol:/build/result || exitcode=$? - rm -rf _build_stable - docker start -a helper-$vol || exitcode=$? @@ -231,11 +231,10 @@ debpkg-unstable: - next script: - docker pull gitlab-registry.lrde.epita.fr/spot/buildenv/debian - - docker pull gitlab-registry.lrde.epita.fr/spot/buildenv/debian-i386 - vol=spot-unstable-$CI_COMMIT_SHA - docker volume create $vol - exitcode=0 - - docker run -v $vol:/build/result --name helper-$vol registry.lrde.epita.fr/spot-debuild ./build-spot.sh $CI_COMMIT_REF_NAME -j${NBPROC-1} || exitcode=$? + - docker run -v $vol:/build/result --name helper-$vol gitlab-registry.lrde.epita.fr/spot/buildenv/debian ./build-spot.sh $CI_COMMIT_REF_NAME -j${NBPROC-1} || exitcode=$? - docker cp helper-$vol:/build/result _build_unstable || exitcode=$? - docker rm helper-$vol || exitcode=$? - docker volume rm $vol || exitcode=$? @@ -259,7 +258,7 @@ debpkg-unstable-i386: - vol=spot-unstable-$CI_COMMIT_SHA - docker volume create $vol - exitcode=0 - - docker create -v $vol:/build/result --name helper-$vol registry.lrde.epita.fr/spot-debuild-i386 ./bin-spot.sh -j${NBPROC-1} || exitcode=$? + - docker create -v $vol:/build/result --name helper-$vol gitlab-registry.lrde.epita.fr/spot/buildenv/debian-i386 ./bin-spot.sh -j${NBPROC-1} || exitcode=$? - docker cp _build_unstable/. helper-$vol:/build/result || exitcode=$? - rm -rf _build_unstable - docker start -a helper-$vol || exitcode=$? From d342d4c6fd28ada5bd8911de7753bee7af6f266e Mon Sep 17 00:00:00 2001 From: Jerome Dubois Date: Tue, 15 Sep 2020 15:30:42 +0200 Subject: [PATCH 06/22] python: add check for panda * tests/python/ipnbdoctest.py: Skip test if panda is not installed. --- tests/python/ipnbdoctest.py | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/tests/python/ipnbdoctest.py b/tests/python/ipnbdoctest.py index cdf4a4407..4eb120efa 100755 --- a/tests/python/ipnbdoctest.py +++ b/tests/python/ipnbdoctest.py @@ -171,6 +171,10 @@ def canonical_dict(dict, ignores): re.sub(r"(' returned non-zero exit status \d+)\.", r'\1', dict['evalue']) + if ('ename' in dict and dict['ename'] == 'ModuleNotFoundError' and + 'pandas' in dict['evalue']): + sys.exit(77) + if 'transient' in dict: del dict['transient'] if 'execution_count' in dict: From 579708543ef4ce354db553ec8a1b8d382ea6ccac Mon Sep 17 00:00:00 2001 From: Jerome Dubois Date: Wed, 16 Sep 2020 10:23:54 +0200 Subject: [PATCH 07/22] * AUTHORS: Add myself. --- AUTHORS | 1 + 1 file changed, 1 insertion(+) diff --git a/AUTHORS b/AUTHORS index bbf0a5e44..dc0092a3b 100644 --- a/AUTHORS +++ b/AUTHORS @@ -17,6 +17,7 @@ Florian Renkin Guillaume Sadegh Heikki Tauriainen Henrich Lauko +Jérôme Dubois Laurent Xu Maximilien Colange Pierre Parutto From 59124f9178fd784fa60fd830330df9d1cafcbf1c Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 15 Sep 2020 12:28:30 +0200 Subject: [PATCH 08/22] minimize_wdba: avoid memory leak * spot/twaalgos/minimize.cc: Do not look the final/non_final hash table when determinization is aborted. --- spot/twaalgos/minimize.cc | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/spot/twaalgos/minimize.cc b/spot/twaalgos/minimize.cc index f9188f0b1..49d7b7864 100644 --- a/spot/twaalgos/minimize.cc +++ b/spot/twaalgos/minimize.cc @@ -380,8 +380,8 @@ namespace spot throw std::runtime_error ("minimize_wdba() does not support alternation"); - hash_set* final = new hash_set; - hash_set* non_final = new hash_set; + hash_set* final; + hash_set* non_final; twa_graph_ptr det_a; @@ -444,6 +444,8 @@ namespace spot } } + final = new hash_set; + non_final = new hash_set; // SCC that have been marked as useless. std::vector useless(scc_count); From 23709101c52472a858501c45c98a52f2660a061d Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 23 Sep 2020 11:01:05 +0200 Subject: [PATCH 09/22] tests: replace non-portable use of sed by $PERL MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This fixes one failure reported in #428 by Étienne Renault. * tests/core/lbt.test: Here. * tests/run.in: Export PERL. --- tests/core/lbt.test | 4 ++-- tests/run.in | 5 ++++- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/tests/core/lbt.test b/tests/core/lbt.test index 7602e1945..73ecaa54c 100755 --- a/tests/core/lbt.test +++ b/tests/core/lbt.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2013, 2016, 2017, 2019 Laboratoire de Recherche et +# Copyright (C) 2013, 2016, 2017, 2019, 2020 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -99,7 +99,7 @@ test `wc -l < formulas.4` -eq 168 # Add some carriage returns to simulate MS-DOS files and # make sure our parser does not mind. -sed 's/$/\r/' formulas.2 > formulas.2ms +$PERL -pe 's/$/\r/' formulas.2 > formulas.2ms # The --csv-escape option is now obsolete and replaced by double # quotes in the format string. So eventually the first two lines # should disappear. diff --git a/tests/run.in b/tests/run.in index 77d898e72..7a2fe2a70 100755 --- a/tests/run.in +++ b/tests/run.in @@ -61,6 +61,9 @@ export top_builddir top_srcdir='@abs_top_srcdir@' export top_srcdir +PERL='@PERL@' +export PERL + # Reset those variables, as they may affect the output of DOT. SPOT_DOTEXTRA= export SPOT_DOTEXTRA @@ -108,7 +111,7 @@ case $1 in *.test) exec sh -x "$@";; *.pl) - exec @PERL@ "$@";; + exec $PERL "$@";; *python*|*jupyter*) PYTHONPATH=$pypath DYLD_LIBRARY_PATH=$modpath \ exec $PREFIXCMD "$@";; From c57a147d3d1bb0da907339366284ff92fa50151c Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 23 Sep 2020 11:06:03 +0200 Subject: [PATCH 10/22] tests: use $PERL instead of perl * tests/core/ltl2tgba2.test, tests/core/ltldo.test, tests/core/ltlfilt.test, tests/core/neverclaimread.test, tests/core/parseaut.test, tests/sanity/bin.test: Here. --- tests/core/ltl2tgba2.test | 2 +- tests/core/ltldo.test | 2 +- tests/core/ltlfilt.test | 4 ++-- tests/core/neverclaimread.test | 2 +- tests/core/parseaut.test | 4 ++-- tests/sanity/bin.test | 6 +++--- 6 files changed, 10 insertions(+), 10 deletions(-) diff --git a/tests/core/ltl2tgba2.test b/tests/core/ltl2tgba2.test index 1878e3efd..57fd57d44 100755 --- a/tests/core/ltl2tgba2.test +++ b/tests/core/ltl2tgba2.test @@ -386,7 +386,7 @@ EOF ltlfilt -Fformulas/1 --stats='%f,%f,%>' | ltl2tgba -F-/2 --stats='%<,%<, %s,%t' | ltl2tgba -D -F-/2 --stats='%<,%<,%>, %s,%t' | - perl -p -e 's/$/\r/' | + $PERL -p -e 's/$/\r/' | ltl2tgba -B -F-/2 --stats='%<,%<,%>, %s,%t' | ltl2tgba -BD -F-/2 --stats='%<,%<,%>, %s,%t' | ltl2tgba -GD -F-/2 --stats='%<,%>, %s,%t' > output diff --git a/tests/core/ltldo.test b/tests/core/ltldo.test index ce02dfb04..5027dad0c 100755 --- a/tests/core/ltldo.test +++ b/tests/core/ltldo.test @@ -169,7 +169,7 @@ grep "ltldo: failed to parse '2a'.*-n" err genltl --rv-counter=9 | ltldo ltl2tgba --stats=' print("%[up]R + %[uc]R + %[sp]R + %[sc]R - %R\n"); die if abs(%[up]R + %[uc]R + %[sp]R + %[sc]R - %R) > 0.02;' > code.pl -perl code.pl +$PERL code.pl # ltldo should not leave temporary files behind itself on errors ltldo -f a 'ltl2dstar --ltl2nba=spin:ltl2tgba@-DS' && exit 2 diff --git a/tests/core/ltlfilt.test b/tests/core/ltlfilt.test index 3d79695c7..501ae94b2 100755 --- a/tests/core/ltlfilt.test +++ b/tests/core/ltlfilt.test @@ -1,6 +1,6 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2013-2019 Laboratoire de Recherche et Développement de +# Copyright (C) 2013-2020 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -475,7 +475,7 @@ run 0 ltlfilt -p --wring -u --nnf --relabel=pnn --define in >out diff exp out run 0 ltlfilt -0 in > out -perl -i -pe 's/\0/@\n/g' out +$PERL -i -pe 's/\0/@\n/g' out cat >exp < stderrfilt diff stderrfilt expected-err # DOS-style new lines should have the same output. -perl -pi -e 's/$/\r/' input +$PERL -pi -e 's/$/\r/' input run 2 ../ikwiad -ks -XN input > stdout 2>stderr cat stderr grep input: stderr > stderrfilt diff --git a/tests/core/parseaut.test b/tests/core/parseaut.test index b4fba6d96..a4f273608 100755 --- a/tests/core/parseaut.test +++ b/tests/core/parseaut.test @@ -695,7 +695,7 @@ input:8.1-16.12: aborted input automaton EOF # DOS-style new lines should have the same output. -perl -pi -e 's/$/\r/' input +$PERL -pi -e 's/$/\r/' input autfilt --hoa input 2>stderr && exit 1 cat stderr diff stderr input.exp @@ -1135,7 +1135,7 @@ EOF diff expected input.out # DOS-style new lines should have the same output. -perl -pe -e 's/$/\r/' input +$PERL -pe -e 's/$/\r/' input autfilt --hoa input 2>stderr && exit 1 cat stderr diff stderr input.exp diff --git a/tests/sanity/bin.test b/tests/sanity/bin.test index 10aba7620..3c331020c 100644 --- a/tests/sanity/bin.test +++ b/tests/sanity/bin.test @@ -1,7 +1,7 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2017 Laboratoire de Recherche et Développement de -# l'Epita (LRDE). +# Copyright (C) 2017, 2020 Laboratoire de Recherche et Développement +# de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -102,7 +102,7 @@ do # of the document string fall right into the rmargin. ARGP_HELP_FMT=rmargin=10000 \ $top_builddir/bin/$binary --help > help-$binary.tmp - if ! perl -ne '/\n\s*\n(\s*-.*\n)/ && print("$1") && exit(1)' \ + if ! $PERL -ne '/\n\s*\n(\s*-.*\n)/ && print("$1") && exit(1)' \ -0777 help-$binary.tmp > help-err then echo "bin/$binary --help has options after blank line;" \ From 66944e866fdf4b7b00bf23b7786971009888c02c Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 23 Sep 2020 11:31:45 +0200 Subject: [PATCH 11/22] tests: fix non-portable use of sed Fixes #428, reported by Etienne Renault. * tests/core/genltl.test: Do use \? with sed. --- tests/core/genltl.test | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/tests/core/genltl.test b/tests/core/genltl.test index 271820d8d..ef596e842 100755 --- a/tests/core/genltl.test +++ b/tests/core/genltl.test @@ -24,8 +24,10 @@ set -e # Make sure the name of each pattern is correctly output by %F. opts=`genltl --help | sed -n '/=RANGE/{ s/^ *// -s/=RANGE\[\?,RANGE.*/=1,1/p -s/\[\?=RANGE.*/=1/p +s/=RANGE\[,RANGE.*/=1,1/p +s/=RANGE,RANGE.*/=1,1/p +s/\[=RANGE.*/=1/p +s/=RANGE.*/=1/p }'` res=`genltl $opts --format="--%F=%L"` test "$opts" = "$res" From a4978ed33dc57104e5e57b1263109e99cc1a5f6d Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 23 Sep 2020 11:35:11 +0200 Subject: [PATCH 12/22] Update HACKING Fixes #427 and #429. * HACKING: Mention dot2tex and update Flex. --- HACKING | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/HACKING b/HACKING index f41d7e274..6988c011b 100644 --- a/HACKING +++ b/HACKING @@ -24,7 +24,7 @@ since the generated files they produce are distributed.) GNU Autoconf >= 2.61 GNU Automake >= 1.11 GNU Libtool >= 2.4 - GNU Flex (the version seems to matters, we used 2.5.35) + GNU Flex >= 2.6 GNU Bison >= 3.0 GNU Emacs (preferably >= 24 but it may work with older versions) org-mode >= 9.1 (the version that comes bundled with your emacs @@ -59,6 +59,7 @@ only for certain operations (like releases): ltl2dstar likewise ltl3dra likewise spin likewise + dot2tex used for an example in the documentation and in one test glucose >= 3.0 likewise lbtt >= 1.2.1a used in the test suite (ltlcross is now more powerful, but additional tests do not hurt) From 5401d4c8ce5c76d9d3a817b544d6de3131fee7e1 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 23 Sep 2020 13:13:28 +0200 Subject: [PATCH 13/22] tests: fix import of libspotgen on Darwin MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Fixes #426, reported by Étienne Renault. * tests/run.in: Augment modpath. --- tests/run.in | 1 + 1 file changed, 1 insertion(+) diff --git a/tests/run.in b/tests/run.in index 7a2fe2a70..e86943b6d 100755 --- a/tests/run.in +++ b/tests/run.in @@ -26,6 +26,7 @@ # path of dependent libraries in each library). modpath='@abs_top_builddir@/python/.libs:@abs_top_builddir@/python/spot/.libs' modpath=$modpath:'@abs_top_builddir@/spot/ltsmin/.libs' +modpath=$modpath:'@abs_top_builddir@/spot/gen/.libs' modpath=$modpath:'@abs_top_builddir@/spot/.libs' modpath=$modpath:'@abs_top_builddir@/buddy/src/.libs' From ef41b6af563b62bade80fe4d41290a2fd85ece28 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 23 Sep 2020 13:25:58 +0200 Subject: [PATCH 14/22] tests: do not override DYLD_LIBRARY_PATH * tests/run.in: Here. --- tests/run.in | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/tests/run.in b/tests/run.in index e86943b6d..dd053011d 100755 --- a/tests/run.in +++ b/tests/run.in @@ -46,7 +46,8 @@ PATH="@abs_top_builddir@/bin:$PATH" export PATH test -z "$1" && - PYTHONPATH=$pypath DYLD_LIBRARY_PATH=$modpath exec $PREFIXCMD @PYTHON@ + PYTHONPATH=$pypath DYLD_LIBRARY_PATH=$modpath:$DYLD_LIBRARY_PATH \ + exec $PREFIXCMD @PYTHON@ srcdir="@srcdir@" # Reset CFLAGS, because some tests call the compiler, and we do not @@ -103,18 +104,18 @@ export srcdir case $1 in *.ipynb) - PYTHONPATH=$pypath DYLD_LIBRARY_PATH=$modpath \ + PYTHONPATH=$pypath DYLD_LIBRARY_PATH=$modpath:$DYLD_LIBRARY_PATH \ PYTHONIOENCODING=utf-8:surrogateescape \ exec $PREFIXCMD @PYTHON@ @abs_srcdir@/python/ipnbdoctest.py "$@";; *.py) - PYTHONPATH=$pypath DYLD_LIBRARY_PATH=$modpath \ + PYTHONPATH=$pypath DYLD_LIBRARY_PATH=$modpath:$DYLD_LIBRARY_PATH \ exec $PREFIXCMD @PYTHON@ "$@";; *.test) exec sh -x "$@";; *.pl) exec $PERL "$@";; *python*|*jupyter*) - PYTHONPATH=$pypath DYLD_LIBRARY_PATH=$modpath \ + PYTHONPATH=$pypath DYLD_LIBRARY_PATH=$modpath:$DYLD_LIBRARY_PATH \ exec $PREFIXCMD "$@";; *) echo "Unknown extension" >&2 From 4ca2f394e4053069402f288f0a248776a5ea1b35 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 23 Sep 2020 17:53:18 +0200 Subject: [PATCH 15/22] org: fix local export * doc/org/.dir-locals.el.in: Remove incorrect quote. --- doc/org/.dir-locals.el.in | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/org/.dir-locals.el.in b/doc/org/.dir-locals.el.in index bc56cbecf..cba9892fb 100644 --- a/doc/org/.dir-locals.el.in +++ b/doc/org/.dir-locals.el.in @@ -41,8 +41,8 @@ (shell-file-name . "@SHELL@") (ess-ask-for-ess-directory . nil) (org-export-html-postamble . nil) - (org-html-table-header-tags . - '("
" . "
")) + (org-html-table-header-tags + "
" . "
") (org-babel-default-header-args:plantuml . ((:results . "file") (:exports . "results") From 53a68f99f4a79e3c363665c20814b34e3a0d67fd Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 28 Sep 2020 17:59:55 +0200 Subject: [PATCH 16/22] org: various improvements * doc/org/spot.css: Improve style and responsiveness. * doc/org/oaut.org, doc/org/ioltl.org: Fix some ugly outputs. --- doc/org/ioltl.org | 3 +-- doc/org/oaut.org | 49 ++++++++++++++++++++++++++--------------------- doc/org/spot.css | 30 +++++++++++++++++++---------- 3 files changed, 48 insertions(+), 34 deletions(-) diff --git a/doc/org/ioltl.org b/doc/org/ioltl.org index 696a50c19..0f6193a3f 100644 --- a/doc/org/ioltl.org +++ b/doc/org/ioltl.org @@ -71,8 +71,7 @@ instance =gfa= is an atomic proposition, but =GFa= actually denotes the LTL formula =G(F(a))=. Any double-quoted string is also considered to be an atomic proposition, so if =GFa= had to be an atomic proposition, it could be written -#+HTML: "GFa" -. +@@html:@@"GFa"@@html::@@. These double-quote strings also make it possible to embed arbitrarily complex expressions that represent an atomic proposition that Spot diff --git a/doc/org/oaut.org b/doc/org/oaut.org index 810cf074b..9f872a9f9 100644 --- a/doc/org/oaut.org +++ b/doc/org/oaut.org @@ -14,7 +14,7 @@ are used to specify how to output of automata. All tools that can output automata implement the following options: #+BEGIN_SRC sh :exports results -ltl2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d' +ltl2tgba --help | sed -n 's/ *$//g;/Output format:/,/^$/p' | sed '1d;$d' #+END_SRC #+RESULTS: #+begin_example @@ -26,25 +26,25 @@ ltl2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d' 'unambiguous', 'stutter-invariant', 'stutter-sensitive-example', 'semi-determinism', or 'strength'. - -d, --dot[=1|a|A|b|B|c|C(COLOR)|e|E|f(FONT)|h|k|K|n|N|o|r|R|s|t|u|v|y|+INT| Gb) W c' -d #+END_SRC -#+RESULTS: oaut-dot1 #+begin_example digraph "(Gb | F!a) W c" { rankdir=LR @@ -438,6 +436,11 @@ This output should be processed with =dot= to be converted into a picture. For instance use =dot -Tpng= or =dot -Tpdf=. The pictures on this page are produced with =dot -Tsvg=. +#+NAME: oaut-dot1 +#+BEGIN_SRC sh :exports code :prologue export SPOT_DOTEXTRA= SPOT_DOTDEFAULT= +ltl2tgba '(Ga -> Gb) W c' -d | dot -Tsvg +#+END_SRC + #+BEGIN_SRC dot :file oaut-dot1.svg :var txt=oaut-dot1 :exports results $txt #+END_SRC @@ -445,6 +448,8 @@ $txt #+RESULTS: [[file:oaut-dot1.svg]] +However in this documentation simply omit the calls to =dot -Tsvg=. + ** Customizing the dot output This output can be customized by passing optional characters to the diff --git a/doc/org/spot.css b/doc/org/spot.css index dd46b579c..291f23e6f 100644 --- a/doc/org/spot.css +++ b/doc/org/spot.css @@ -2,20 +2,25 @@ a{color:inherit;background-color:inherit;font:inherit;text-decoration:inherit} a:hover{text-decoration:underline} /* http://paletton.com/#uid=33i0X0kz3BrkeHdpSD1C7r1FAlb */ -body{font-family:Lato, sans-serif;font-size:12pt;font-weight:normal;max-width:62em;margin:auto;padding:0 .5em} +body{font-family:Lato, sans-serif;font-size:12pt;font-weight:normal;max-width:90ch;margin:auto;padding:0 .5em} body.man{padding:0 .5em 3em .5em} body #content{padding-top:45px} body pre{background:#fbfbfb;border:none;font-family:monospace, courier} body code{font-weight:bold} body a{color:#008181} +h1{display:block;width:calc(100% - 1em);position:relative;padding:.5em} +h1::before{content:"";position:absolute;z-index:-1;background-color:#ffe35e;left:0em;bottom:0em;width:100%;height:100%;border-radius:10px;transform:skew(10deg)} #table-of-contents{font-size:80%;padding-left:0.5em;padding-right:0.5em;text-align:right;float:right;border-left:1px solid #ffd300;border-bottom:1px solid #ffd300;background:#ffe35e} #table-of-contents ul{padding-left:1em} #table-of-contents h2{font-size:100%;font-weight:normal;padding-left:0.5em;padding-right:0.5em;padding-top:0.05em;padding-bottom:0.05em} #table-of-contents #text-table-of-contents{text-align:left} #org-div-home-and-up{text-align:center;font-size:100%} -.outline-2 h2{border-bottom-style:solid;border-color:#ffe35e} -.outline-3 h3{position:relative;z-index:1} -.outline-3 h3:before{content:"";position:absolute;z-index:-1;left:-.2em;bottom:-.05em;height:1.2em;width:1.2em;background-color:#ffe35e;border-radius:5px} +.outline-2 h2{display:block;width:100%;position:relative} +.outline-2 h2::before{content:"";height:100%;width:calc(100% + 2em);position:absolute;z-index:-1;bottom:0em;left:-1em;background-color:#ffe35e;background:linear-gradient(45deg,#ffe35e 50%,transparent 75%);transform:skew(10deg);border-radius:5px;} +.outline-3 h3{display:block;width:auto;position:relative} +.outline-3 h3::before{content:"";position:absolute;z-index:-1;width:calc(100% + 2em);height:100%;left:-1em;bottom:0em;;background-color:#ffe35e;background:linear-gradient(45deg,#ffe35e 25%,transparent 50%);transform:skew(10deg);border-radius:3px} +.outline-2 h2:hover::before,.outline-3 h3:hover::before{background-color:#ffe35e} +pre{margin:1.2ex} pre.src{padding-top:8px;border-left-style:solid;border-color:#00adad;overflow:auto;margin-top:0;margin-bottom:0} pre.src-hoa{border-color:#d70079} pre.example{border-left-style:solid;border-color:#d70079;margin-top:0;position:relative;z-index:2} @@ -23,16 +28,21 @@ div.org-src-container+pre.example{border-top-width:1px;border-top-color:#ddd;bor div.org-src-container+div.org-src-container pre.src{border-top-width:1px;border-top-color:#ddd;border-top-style:dashed} div.org-src-container {margin-top:0;margin-bottom:0;position:relative;z-index:1} pre.src-text{border-left-style:solid;border-color:#d70079} -pre.src:before{border:none;border-bottom-style:solid;border-color:#00adad;top:0px;} -pre.src-python:before{content:'Python'} -pre.src-C\+\+:before{content:'C++'} -pre.src-hoa:before{content:'HOA';border-color:#d70079} +pre.src::before{border:none;border-bottom-style:solid;border-color:#00adad;top:0px;} +pre.src-python::before{content:'Python'} +pre.src-C\+\+::before{content:'C++'} +pre.src-hoa::before{content:'HOA';border-color:#d70079} img{max-width:100%} svg.org-svg{width:auto;max-width:100%} +table{margin-top:1em} table.csv-table,table.table-pre{font-family:monospace, courier} table.csv-table th{vertical-align:bottom} table.csv-table th div{text-align:center} table.csv-table th div span{text-align:left;writing-mode:vertical-lr;transform:rotate(180deg);display:inline-block;white-space:nowrap} +@media only screen and (max-width:100ch){ +#spotlogo{display:none} +.outline-2 h2::before,.outline-3 h3::before,h1.title::before{transform:none;} +} @media screen{ #table-of-contents{position:fixed;right:0em;top:0em;max-width:50%;max-height:80%;overflow:auto;z-index:10} #table-of-contents #text-table-of-contents{display:none} @@ -66,9 +76,9 @@ thead tr{background:#ffe35e} .org-hoa-header-lowercase{color:#00adad} .org-hoa-ap-number{color:#d70079} .implem{background:#fff0a6;padding:0.5ex 1ex 0.5ex 1ex;margin:1ex;border-color:#ffe35e;border-style:solid none} -.implem:before{background:#ffe35e;content:"Implementation detail";padding:.5ex;position:relative;top:0;left:0;font-weight:bold} +.implem::before{background:#ffe35e;content:"Implementation detail";padding:.5ex;position:relative;top:0;left:0;font-weight:bold} .caveat{background:#ef99c9;padding:0.5ex 1ex 0.5ex 1ex;margin:1ex;border-color:#d70079;border-style:solid none} -.caveat:before{background:#d70079;content:"Caveat";padding:.5ex;position:relative;top:0;left:0;font-weight:bold} +.caveat::before{background:#d70079;content:"Caveat";padding:.5ex;position:relative;top:0;left:0;font-weight:bold} .spotlogo{transform-origin:50% 50%;animation-duration:2s;animation-name:animspotlogo} g.spotlogobg{transform-origin:50% 50%;animation-duration:2s;animation-name:animspotlogobg} g#version{transform-origin:50% 50%;animation-duration:3s;animation-name:animspotlogover} From 7697adf645ae4c01c581a7f488d3bd046f1d8866 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 7 Oct 2020 09:45:55 +0200 Subject: [PATCH 17/22] org: work around ESS issue 1052 This was causing all our build to fail. * doc/org/init.el.in: Here. --- doc/org/init.el.in | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/doc/org/init.el.in b/doc/org/init.el.in index eec6269ac..268378b2f 100644 --- a/doc/org/init.el.in +++ b/doc/org/init.el.in @@ -54,6 +54,10 @@ (require 'org-install) (require 'hoa-mode) +; See https://github.com/emacs-ess/ESS/issues/1052 +(setq ess-gen-proc-buffer-name-function 'ess-gen-proc-buffer-name:directory) +(setq ess-use-flymake nil) + (setq org-export-htmlize-output-type 'css) (setq org-html-htmlize-output-type 'css) ; the .org-timestamp directory does not always exist, is not always From 5ea20db6b460dc5c448740ef85d388117dc2a2d6 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 17 Oct 2020 20:39:34 +0200 Subject: [PATCH 18/22] ltlsmin: fix incorrect check for dlsym error Fix #435 reported by Yann Thierry-Mieg. * spot/ltsmin/ltsmin.cc (sym): Fix incorrect check introduced by dc4a477172. --- spot/ltsmin/ltsmin.cc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/spot/ltsmin/ltsmin.cc b/spot/ltsmin/ltsmin.cc index 96b946f4c..885e9d78d 100644 --- a/spot/ltsmin/ltsmin.cc +++ b/spot/ltsmin/ltsmin.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012, 2014-2019 Laboratoire de +// Copyright (C) 2011, 2012, 2014-2020 Laboratoire de // Recherche et Développement de l'Epita (LRDE) // // This file is part of Spot, a model checking library. @@ -1047,7 +1047,7 @@ namespace spot // should not be converted to pointer-to-functions (we have to // assume they can for POSIX). *reinterpret_cast(dst) = lt_dlsym(h, name); - if (dst == nullptr) + if (*dst == nullptr) throw std::runtime_error("Failed to resolve symbol '"s + name + "' in '" + file + "'."); }; From bcd88df0fe767a39d3e04d495491921b0d1c3da1 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 8 Nov 2020 12:04:55 +0100 Subject: [PATCH 19/22] python: rename aux.py to aux_.py Fixes #437, reporeted by Yann Thierry-Mieg. * python/spot/aux.py: Rename as... * python/spot/aux_.py: ... this. * python/spot/__init__.py, python/Makefile.am: Adjust. * NEWS: Mention the change. --- NEWS | 6 +++++- python/Makefile.am | 2 +- python/spot/__init__.py | 6 ++++++ python/spot/{aux.py => aux_.py} | 7 +++++-- 4 files changed, 17 insertions(+), 4 deletions(-) rename python/spot/{aux.py => aux_.py} (93%) diff --git a/NEWS b/NEWS index 35a8b0d11..7c34cf502 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,10 @@ New in spot 2.9.4.dev (not yet released) - Nothing yet. + Bugs fixed: + + - The filename python/spot/aux.py caused a problem on Windows and + has been renamed. Existing "import spot.aux" statements should + *not* be updated. (Issue #437.) New in spot 2.9.4 (2020-09-07) diff --git a/python/Makefile.am b/python/Makefile.am index 00a176531..e3fbac6de 100644 --- a/python/Makefile.am +++ b/python/Makefile.am @@ -30,7 +30,7 @@ SWIGFLAGS = -c++ -python -py3 -O -MD EXTRA_DIST = buddy.i spot/impl.i spot/ltsmin.i spot/gen.i nobase_pyexec_PYTHON = \ spot/__init__.py \ - spot/aux.py \ + spot/aux_.py \ spot/impl.py \ spot/ltsmin.py \ spot/gen.py \ diff --git a/python/spot/__init__.py b/python/spot/__init__.py index a3f0c3b57..88d2ed9d3 100644 --- a/python/spot/__init__.py +++ b/python/spot/__init__.py @@ -47,6 +47,12 @@ for path in sys.path: from spot.impl import * +# spot.aux_ used to be called spot.aux until the filename aux.py +# caused issues on Windows. So the file is now named aux_.py, but we +# still want to import it as spot.aux, hence we add it to spot.modules +# as an alias. +import spot.aux_ as aux +sys.modules['spot.aux'] = aux from spot.aux import \ extend as _extend, \ str_to_svg as _str_to_svg, \ diff --git a/python/spot/aux.py b/python/spot/aux_.py similarity index 93% rename from python/spot/aux.py rename to python/spot/aux_.py index cd56d212b..3c6435296 100644 --- a/python/spot/aux.py +++ b/python/spot/aux_.py @@ -1,6 +1,6 @@ # -*- coding: utf-8 -*- -# Copyright (C) 2016, 2019 Laboratoire de Recherche et Développement de l'Epita -# (LRDE). +# Copyright (C) 2016, 2019-2020 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -17,6 +17,9 @@ # You should have received a copy of the GNU General Public License # along with this program. If not, see . +# This file is named "aux_.py" for compatibility with Windows' +# historical limitations, but should really be imported as "spot.aux". + """ Auxiliary functions for Spot's Python bindings """ From aecdab7ba7f15c7876173e2a17c5a9b37b6e839b Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 8 Nov 2020 14:20:17 +0100 Subject: [PATCH 20/22] * NEWS: Update for recent fixes. --- NEWS | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index 7c34cf502..e140670cd 100644 --- a/NEWS +++ b/NEWS @@ -2,9 +2,18 @@ New in spot 2.9.4.dev (not yet released) Bugs fixed: + - Fix multiple spurious test suite failures on Darwin + (Issues #426, #427, #428, #429) or when the + Pandas package was not installed. + - The filename python/spot/aux.py caused a problem on Windows and has been renamed. Existing "import spot.aux" statements should - *not* be updated. (Issue #437.) + *not* be updated. (Issue #437) + + - Fix memory leak in minimize_wdba() when determinization is aborted + because an output_aborter is passed. + + - Distribution contains unnecessary large SVG files (Issue #422) New in spot 2.9.4 (2020-09-07) From a5385bb8869ab26e6c2fa254b2b17411d2434290 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 19 Nov 2020 10:39:43 +0100 Subject: [PATCH 21/22] Release Spot 2.9.5 * configure.ac, NEWS, doc/org/setup.org: Update version. --- NEWS | 4 ++-- configure.ac | 2 +- doc/org/setup.org | 10 +++++----- 3 files changed, 8 insertions(+), 8 deletions(-) diff --git a/NEWS b/NEWS index e140670cd..500e23fe8 100644 --- a/NEWS +++ b/NEWS @@ -1,4 +1,4 @@ -New in spot 2.9.4.dev (not yet released) +New in spot 2.9.5 (2020-11-19) Bugs fixed: @@ -13,7 +13,7 @@ New in spot 2.9.4.dev (not yet released) - Fix memory leak in minimize_wdba() when determinization is aborted because an output_aborter is passed. - - Distribution contains unnecessary large SVG files (Issue #422) + - Distribution used to contain unnecessary large SVG files (Issue #422) New in spot 2.9.4 (2020-09-07) diff --git a/configure.ac b/configure.ac index d194deb9e..018d9847b 100644 --- a/configure.ac +++ b/configure.ac @@ -21,7 +21,7 @@ # along with this program. If not, see . AC_PREREQ([2.63]) -AC_INIT([spot], [2.9.4.dev], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.9.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 8a3339fb2..dc082321a 100644 --- a/doc/org/setup.org +++ b/doc/org/setup.org @@ -1,11 +1,11 @@ #+OPTIONS: H:2 num:nil toc:t html-postamble:nil ^:nil #+EMAIL: spot@lrde.epita.fr #+HTML_LINK_HOME: index.html -#+MACRO: SPOTVERSION 2.9.4 -#+MACRO: LASTRELEASE 2.9.4 -#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.9.4.tar.gz][=spot-2.9.4.tar.gz=]] -#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-9-4/NEWS][summary of the changes]] -#+MACRO: LASTDATE 2020-09-07 +#+MACRO: SPOTVERSION 2.9.5 +#+MACRO: LASTRELEASE 2.9.5 +#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.9.5.tar.gz][=spot-2.9.5.tar.gz=]] +#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-9-5/NEWS][summary of the changes]] +#+MACRO: LASTDATE 2020-11-19 #+ATTR_HTML: :id spotlogo [[file:spot2.svg]] From c5c8e8c516467557ea241c83d0fde733528e1bba Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 19 Nov 2020 10:42:46 +0100 Subject: [PATCH 22/22] * NEWS, configure.ac: Bump version. --- NEWS | 4 ++++ configure.ac | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index 500e23fe8..ad7afe992 100644 --- a/NEWS +++ b/NEWS @@ -1,3 +1,7 @@ +New in spot 2.9.5.dev (not yet released) + + Nothing yet. + New in spot 2.9.5 (2020-11-19) Bugs fixed: diff --git a/configure.ac b/configure.ac index 018d9847b..0d11d8cea 100644 --- a/configure.ac +++ b/configure.ac @@ -21,7 +21,7 @@ # along with this program. If not, see . AC_PREREQ([2.63]) -AC_INIT([spot], [2.9.5], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.9.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])