From e1d0c07d4b7dfac76d433bfd002eac361ddb70d4 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 21 Nov 2016 11:09:51 +0100 Subject: [PATCH 01/10] * NEWS, configure.ac: Bump version number. --- NEWS | 4 ++++ configure.ac | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index 2e2f91cbe..7c870e1a5 100644 --- a/NEWS +++ b/NEWS @@ -1,3 +1,7 @@ +New in spot 2.2.1.dev (Not yet released) + + Nothing yet. + New in spot 2.2.1 (2016-11-21) Bug fix: diff --git a/configure.ac b/configure.ac index 1b97c65b4..c82cd40e9 100644 --- a/configure.ac +++ b/configure.ac @@ -21,7 +21,7 @@ # along with this program. If not, see . AC_PREREQ([2.61]) -AC_INIT([spot], [2.2.1], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.2.1.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]) From f868e0cea6e5d2c0f72e2408c641164df5f919dd Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 24 Nov 2016 07:31:32 +0100 Subject: [PATCH 02/10] scc_filter: remove left-over print MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Reported by František Blahoudek. * spot/twaalgos/sccfilter.cc: Remove extra print statement. * NEWS: Mention it. --- NEWS | 5 ++++- spot/twaalgos/sccfilter.cc | 1 - 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/NEWS b/NEWS index 7c870e1a5..340b218a3 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,9 @@ New in spot 2.2.1.dev (Not yet released) - Nothing yet. + Bug fixes: + + * scc_filter() had a left-over print statement that would print + "names" when copying the name of the states. New in spot 2.2.1 (2016-11-21) diff --git a/spot/twaalgos/sccfilter.cc b/spot/twaalgos/sccfilter.cc index 5eabfbc98..d88f44b19 100644 --- a/spot/twaalgos/sccfilter.cc +++ b/spot/twaalgos/sccfilter.cc @@ -334,7 +334,6 @@ namespace spot if (auto* names = aut->get_named_prop>("state-names")) { - std::cerr << "names\n"; unsigned size = names->size(); if (size > in_n) size = in_n; From 341eeb2ba1c7a349f427d29f18d76c12f20706cc Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 28 Nov 2016 16:19:05 +0100 Subject: [PATCH 03/10] strength: fix is_terminal() Fix #198. Reported by Maximilien Colange. * spot/twaalgos/strength.cc (is_terminal): Test that no accepting transition lead to a rejecting SCC. * tests/core/strength.test: Add test case. * spot/twaalgos/strength.hh, spot/twa/twa.hh, doc/org/concepts.org: Adjust documentation. * NEWS: Mention the fix. --- NEWS | 5 ++ doc/org/concepts.org | 18 ++++---- spot/twa/twa.hh | 10 ++-- spot/twaalgos/strength.cc | 11 +++++ spot/twaalgos/strength.hh | 8 +++- tests/core/strength.test | 96 +++++++++++++++++++++++++++++++++++++++ 6 files changed, 133 insertions(+), 15 deletions(-) diff --git a/NEWS b/NEWS index 340b218a3..04fb9e0eb 100644 --- a/NEWS +++ b/NEWS @@ -5,6 +5,11 @@ New in spot 2.2.1.dev (Not yet released) * scc_filter() had a left-over print statement that would print "names" when copying the name of the states. + * is_terminal() should reject automata that have accepting + transitions going into rejecting SCCs. The whole point of + being a terminal automaton is that reaching an accepting + transition guarantees that any suffix will be accepted. + New in spot 2.2.1 (2016-11-21) Bug fix: diff --git a/doc/org/concepts.org b/doc/org/concepts.org index 0e7a7f44f..54ad43fe1 100644 --- a/doc/org/concepts.org +++ b/doc/org/concepts.org @@ -990,15 +990,15 @@ better choices. There are actually several property flags that are stored into each automaton, and that can be queried or set by algorithms: -| flag name | meaning when =true= | -|---------------------+---------------------------------------------------------------------------------------| -| =state_acc= | automaton should be considered has having state-based acceptance | -| =inherently_weak= | accepting and rejecting cycles cannot be mixed in the same SCC | -| =weak= | transitions of an SCC all belong to the same acceptance sets | -| =terminal= | automaton is weak, accepting SCCs are complete and may not reach rejecting cycles | -| =deterministic= | there is at most one run *recognizing* a word, but not necessarily accepting it | -| =unambiguous= | there is at most one run *accepting* a word (but it might be recognized several time) | -| =stutter_invariant= | the property recognized by the automaton is [[https://www.lrde.epita.fr/~adl/dl/adl/michaud.15.spin.pdf][stutter-invariant]] | +| flag name | meaning when =true= | +|---------------------+----------------------------------------------------------------------------------------------| +| =state_acc= | automaton should be considered has having state-based acceptance | +| =inherently_weak= | accepting and rejecting cycles cannot be mixed in the same SCC | +| =weak= | transitions of an SCC all belong to the same acceptance sets | +| =terminal= | automaton is weak, accepting SCCs are complete, accepting edges may not go to rejecting SCCs | +| =deterministic= | there is at most one run *recognizing* a word, but not necessarily accepting it | +| =unambiguous= | there is at most one run *accepting* a word (but it might be recognized several time) | +| =stutter_invariant= | the property recognized by the automaton is [[https://www.lrde.epita.fr/~adl/dl/adl/michaud.15.spin.pdf][stutter-invariant]] | For each flag =flagname=, the =twa= class has a method =prop_flagname()= that returns the value of the flag as an instance of diff --git a/spot/twa/twa.hh b/spot/twa/twa.hh index 4ec67956e..6afe8aedb 100644 --- a/spot/twa/twa.hh +++ b/spot/twa/twa.hh @@ -1179,10 +1179,12 @@ namespace spot /// \brief Whether the automaton is terminal. /// - /// An automaton is terminal if it is weak, no non-accepting cycle - /// can be reached from an accepting cycle, and the accepting - /// strongly components are complete (i.e., any suffix is accepted - /// as soon as we enter an accepting component). + /// An automaton is terminal if it is weak, its accepting strongly + /// components are complete, and no accepting edge lead to a + /// non-accepting SCC. + /// + /// This property ensures that a word can be accepted as soon as + /// on of its prefixes move through an accepting edge. /// /// \see prop_weak() /// \see prop_inherently_weak() diff --git a/spot/twaalgos/strength.cc b/spot/twaalgos/strength.cc index 1c4fb6524..b547a0ac6 100644 --- a/spot/twaalgos/strength.cc +++ b/spot/twaalgos/strength.cc @@ -79,6 +79,17 @@ namespace spot break; } } + // A terminal automaton should accept any word that as a prefix + // leading to an accepting edge. In other words, we cannot have + // an accepting edge that goes into a rejecting SCC. + if (terminal && is_term) + for (auto& e: aut->edges()) + if (si->is_rejecting_scc(si->scc_of(e.dst)) + && aut->acc().accepting(e.acc)) + { + is_term = false; + break; + } exit: if (need_si) delete si; diff --git a/spot/twaalgos/strength.hh b/spot/twaalgos/strength.hh index dd0a426dc..a711d01e5 100644 --- a/spot/twaalgos/strength.hh +++ b/spot/twaalgos/strength.hh @@ -25,8 +25,12 @@ namespace spot { /// \brief Whether an automaton is terminal. /// - /// An automaton is terminal if it is weak, and all accepting SCCs - /// are complete. + /// An automaton is terminal if it is weak, all its accepting SCCs + /// are complete, and no accepting transitions lead to a + /// non-accepting SCC. + /// + /// This property guarantees that a word is accepted if it has some + /// prefix that reaches an accepting transition. /// /// \param aut the automaton to check /// diff --git a/tests/core/strength.test b/tests/core/strength.test index e70622877..46ea1174c 100755 --- a/tests/core/strength.test +++ b/tests/core/strength.test @@ -589,3 +589,99 @@ EOF diff out expected autfilt -q expected + + +cat >input <output + +cat >expected < Date: Mon, 28 Nov 2016 17:32:40 +0100 Subject: [PATCH 04/10] ltsmin: use any installed libltdl This should solve issue with the Debian package. * spot/ltsmin/Makefile.am: Use the LTDLINC, LTDLDEPS and LIBLTDL as documented. * NEWS: Mention the fix. --- NEWS | 5 +++++ spot/ltsmin/Makefile.am | 11 +++++++---- 2 files changed, 12 insertions(+), 4 deletions(-) diff --git a/NEWS b/NEWS index 04fb9e0eb..d57cb59e0 100644 --- a/NEWS +++ b/NEWS @@ -1,5 +1,10 @@ New in spot 2.2.1.dev (Not yet released) + Build: + + * If the system has an installed libltdl library, use it instead of + the one we distribute. + Bug fixes: * scc_filter() had a left-over print statement that would print diff --git a/spot/ltsmin/Makefile.am b/spot/ltsmin/Makefile.am index be0215a1d..4a0d949d4 100644 --- a/spot/ltsmin/Makefile.am +++ b/spot/ltsmin/Makefile.am @@ -1,6 +1,6 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2011, 2013, 2014, 2015 Laboratoire de Recherche et -## Developpement de l'Epita (LRDE). +## Copyright (C) 2011, 2013, 2014, 2015, 2016 Laboratoire de Recherche +## et Developpement de l'Epita (LRDE). ## ## This file is part of Spot, a model checking library. ## @@ -18,7 +18,7 @@ ## along with this program. If not, see . AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) \ - $(BUDDY_CPPFLAGS) -I$(top_srcdir)/ltdl + $(BUDDY_CPPFLAGS) $(LTDLINCL) AM_CXXFLAGS = $(WARNING_CXXFLAGS) ltsmindir = $(pkgincludedir)/ltsmin @@ -26,8 +26,11 @@ ltsmindir = $(pkgincludedir)/ltsmin ltsmin_HEADERS = ltsmin.hh lib_LTLIBRARIES = libspotltsmin.la +libspotltsmin_la_DEPENDENCIES = \ + $(top_builddir)/spot/libspot.la \ + $(LTDLDEPS) libspotltsmin_la_LIBADD = \ $(top_builddir)/spot/libspot.la \ - $(top_builddir)/ltdl/libltdlc.la -lpthread + $(LIBLTDL) -lpthread libspotltsmin_la_LDFLAGS = -no-undefined $(SYMBOLIC_LDFLAGS) libspotltsmin_la_SOURCES = ltsmin.cc From 2198543a7a0733656c45f6523207bcc76a59c4df Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 1 Dec 2016 15:51:55 +0100 Subject: [PATCH 05/10] parseaut: diagnose invalid acceptance terms * spot/parseaut/parseaut.yy: Add a diagnostic. * tests/core/parseaut.test: Test it. * NEWS: Document it. --- NEWS | 5 +++++ spot/parseaut/parseaut.yy | 20 +++++++++++++++----- tests/core/parseaut.test | 12 ++++++++++++ 3 files changed, 32 insertions(+), 5 deletions(-) diff --git a/NEWS b/NEWS index d57cb59e0..fdaab380a 100644 --- a/NEWS +++ b/NEWS @@ -15,6 +15,11 @@ New in spot 2.2.1.dev (Not yet released) being a terminal automaton is that reaching an accepting transition guarantees that any suffix will be accepted. + * The HOA parser incorrectly read "Acceptance: 1 Bar(0)" as a valid + way to specify "Acceptance: 1 Fin(0)" because it assumed that + everything that was not Inf was Fin. These errors are now + diagnosed. + New in spot 2.2.1 (2016-11-21) Bug fix: diff --git a/spot/parseaut/parseaut.yy b/spot/parseaut/parseaut.yy index 12a7ec517..3d83cbd19 100644 --- a/spot/parseaut/parseaut.yy +++ b/spot/parseaut/parseaut.yy @@ -867,11 +867,21 @@ acceptance-cond: IDENTIFIER '(' acc-set ')' { res.pos_acc_sets |= res.aut_or_ks->acc().mark($3); if (*$1 == "Inf") - $$ = new spot::acc_cond::acc_code - (res.aut_or_ks->acc().inf({$3})); - else - $$ = new spot::acc_cond::acc_code - (res.aut_or_ks->acc().fin({$3})); + { + $$ = new spot::acc_cond::acc_code + (res.aut_or_ks->acc().inf({$3})); + } + else if (*$1 == "Fin") + { + $$ = new spot::acc_cond::acc_code + (res.aut_or_ks->acc().fin({$3})); + } + else + { + error(@1, std::string("unknown acceptance '") + *$1 + + "', expected Fin or Inf"); + $$ = new spot::acc_cond::acc_code; + } } else { diff --git a/tests/core/parseaut.test b/tests/core/parseaut.test index 665f8cc70..a4c8769d0 100755 --- a/tests/core/parseaut.test +++ b/tests/core/parseaut.test @@ -152,11 +152,23 @@ AP: 2 "a" "b" Acceptance: 0 t --BODY-- --END-- +HOA: v1 +name: "1" +States: 1 +Start: 0 +AP: 0 +acc-name: Buchi +Acceptance: 1 Foo(0) +--BODY-- +State: 0 {0} +[t] 0 +--END-- EOF expecterr input <input < Date: Fri, 2 Dec 2016 13:39:04 +0100 Subject: [PATCH 06/10] install back the safety check of includes.test Compilation of each header file alone, as a safety check, was removed when introducing "#pragma once" because we did not have to check for possible double inclusion. However we still need to compile each header to make sure they are self-contained. * tests/sanity/includes.test: Compile each header. * tests/run.in: Export various compiler and directory flags. * spot/twaalgos/emptiness_stats.hh, spot/misc/mspool.hh, spot/misc/fixpool.hh: Include . * spot/misc/common.hh: Include . * NEWS: Mention the fixed headers. --- NEWS | 4 ++++ spot/misc/common.hh | 1 + spot/misc/fixpool.hh | 2 +- spot/misc/mspool.hh | 4 ++-- spot/twaalgos/emptiness_stats.hh | 4 ++-- tests/run.in | 9 +++++++++ tests/sanity/includes.test | 22 +++++++++++++++------- 7 files changed, 34 insertions(+), 12 deletions(-) diff --git a/NEWS b/NEWS index fdaab380a..da24bdc1b 100644 --- a/NEWS +++ b/NEWS @@ -20,6 +20,10 @@ New in spot 2.2.1.dev (Not yet released) everything that was not Inf was Fin. These errors are now diagnosed. + * Some of the installed headers (spot/misc/fixpool.hh, + spot/misc/mspool.hh, spot/twaalgos/emptiness_stats.hh) were not + self-contained. + New in spot 2.2.1 (2016-11-21) Bug fix: diff --git a/spot/misc/common.hh b/spot/misc/common.hh index cb31eefba..02515bdee 100644 --- a/spot/misc/common.hh +++ b/spot/misc/common.hh @@ -19,6 +19,7 @@ #include #include +#include #pragma once diff --git a/spot/misc/fixpool.hh b/spot/misc/fixpool.hh index 0779d7171..81c4393db 100644 --- a/spot/misc/fixpool.hh +++ b/spot/misc/fixpool.hh @@ -19,10 +19,10 @@ #pragma once +#include #include #include #include -#include namespace spot { diff --git a/spot/misc/mspool.hh b/spot/misc/mspool.hh index 600ed84e4..eb827ff27 100644 --- a/spot/misc/mspool.hh +++ b/spot/misc/mspool.hh @@ -19,11 +19,11 @@ #pragma once +#include +#include #include #include #include -#include -#include namespace spot { diff --git a/spot/twaalgos/emptiness_stats.hh b/spot/twaalgos/emptiness_stats.hh index fb8feefc7..0e52e6085 100644 --- a/spot/twaalgos/emptiness_stats.hh +++ b/spot/twaalgos/emptiness_stats.hh @@ -22,9 +22,9 @@ #pragma once -#include -#include +#include #include +#include namespace spot { diff --git a/tests/run.in b/tests/run.in index b7ae3b7ae..48c2a583c 100755 --- a/tests/run.in +++ b/tests/run.in @@ -52,6 +52,15 @@ srcdir="@srcdir@" # want to inherit parameters likes -std=c11 -fvisibility=hidden CFLAGS= export CFLAGS +CXX='@CXX@' +export CXX +CXXFLAGS='@CXXFLAGS@' +export CXXFLAGS +top_builddir='@abs_top_builddir@' +export top_builddir +top_srcdir='@abs_top_srcdir@' +export top_srcdir + case $1 in */*) diff --git a/tests/sanity/includes.test b/tests/sanity/includes.test index a37e1b3d8..bbcf29b89 100755 --- a/tests/sanity/includes.test +++ b/tests/sanity/includes.test @@ -27,7 +27,6 @@ set -e rm -f failures.inc - INCDIR=${srcdir-.}/../../spot for file in `find "$INCDIR" \( -name "${1-*}.hh" \ @@ -36,21 +35,30 @@ for file in `find "$INCDIR" \( -name "${1-*}.hh" \ if head -n 100 "$INCDIR/$file" | grep -q "[ ]*#.*pragma.* once\$"; then : - elif grep -q 'GNU Bison 2\.6' "$INCDIR/$file"; then - # Bison 2.6, 2.6.1, 2.6.2 have a bug where position.hh - # include instead of . + elif grep -q 'made by GNU Bison' "$INCDIR/$file"; then + # Those are not public headers, so we do not care continue - elif grep -q 'GNU Bison' "$INCDIR/$file"; then - : else echo "Missing, or incorrect include guard." >&2 echo "FAIL: $file" echo " $file" >> failures.inc continue fi - echo "PASS: $file" + + echo "#include " >incltest.cc + + if $CXX $CPPFLAGS -DSKIP_DEPRECATED_WARNING $CXXFLAGS \ + -I$top_builddir -I$top_srcdir -I$top_srcdir/buddy/src \ + -c incltest.cc; then + echo "PASS: $file" + else + echo "FAIL: $file" + echo " $file" >> failures.inc + fi done +rm -f incltest.cc incltest.o + if test -f failures.inc; then echo "Failed files:" cat failures.inc From 15709084b877292a8ddbb860695ad52d9c4a6cd5 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 9 Dec 2016 21:37:15 +0100 Subject: [PATCH 07/10] ltlf: ensure alive holds initially Reported by Shufang Zhu. * spot/tl/ltlf.cc, spot/tl/ltlf.hh: Fix the transltion and update the comments. * tests/core/ltlfilt.test: Adjust test cases. * NEWS: Mention the fix. * THANKS: Add Shufang Zhu. --- NEWS | 3 +++ THANKS | 1 + spot/tl/ltlf.cc | 6 +++++- spot/tl/ltlf.hh | 2 +- tests/core/ltlfilt.test | 42 ++++++++++++++++++++--------------------- 5 files changed, 31 insertions(+), 23 deletions(-) diff --git a/NEWS b/NEWS index da24bdc1b..ca895bdca 100644 --- a/NEWS +++ b/NEWS @@ -24,6 +24,9 @@ New in spot 2.2.1.dev (Not yet released) spot/misc/mspool.hh, spot/twaalgos/emptiness_stats.hh) were not self-contained. + * ltlfilt --from-ltlf should ensure that "alive" holds initially in + order to reject empty traces. + New in spot 2.2.1 (2016-11-21) Bug fix: diff --git a/THANKS b/THANKS index 99800934b..98d23b3d5 100644 --- a/THANKS +++ b/THANKS @@ -29,6 +29,7 @@ Nikos Gorogiannis Reuben Rowe Rüdiger Ehlers Silien Hong +Shufang Zhu Sonali Dutta Tomáš Babiak Valentin Iovene diff --git a/spot/tl/ltlf.cc b/spot/tl/ltlf.cc index dcdcc68bd..74532eabb 100644 --- a/spot/tl/ltlf.cc +++ b/spot/tl/ltlf.cc @@ -37,6 +37,10 @@ namespace spot // the IJCAI'13 paper by De Giacomo & Vardi has a typo. // t(a U b) should be equal to t(a) U t(b & alive). // This typo is fixed in the Memocode'14 paper by Dutta & Vardi. + // + // (However beware that the translation given in the + // Memocode'14 paper forgets to ensure that alive holds + // initially, as required in the IJCAI'13 paper.) case op::U: return formula::U(t(f[0]), formula::And({alive, t(f[1])})); case op::R: @@ -60,7 +64,7 @@ namespace spot auto al = ((*alive == '!') ? formula::Not(formula::ap(alive + 1)) : formula::ap(alive)); - return formula::And({from_ltlf_aux(f, al), + return formula::And({from_ltlf_aux(f, al), al, formula::U(al, formula::G(formula::Not(al)))}); } } diff --git a/spot/tl/ltlf.hh b/spot/tl/ltlf.hh index 385ed1c12..4235590c6 100644 --- a/spot/tl/ltlf.hh +++ b/spot/tl/ltlf.hh @@ -35,7 +35,7 @@ namespace spot /// finite word. The formula is rewritten to ensure that the /// eventualities occur during the "alive" portion. For instance /// a U b becomes - /// (a U (b & alive))&(alive U G!alive). + /// alive&(a U (b & alive))&(alive U G!alive). /// /// The \a alive argument can be used to change the name of the /// atomic property used to introduce. Additionally if \a alive is diff --git a/tests/core/ltlfilt.test b/tests/core/ltlfilt.test index 0ccaa3a36..5c24e866b 100755 --- a/tests/core/ltlfilt.test +++ b/tests/core/ltlfilt.test @@ -182,30 +182,30 @@ EOF run 0 ltlfilt --ltl formulas > formulas2 mv formulas2 formulas -checkopt --ltl --from-ltlf <in < Date: Thu, 15 Dec 2016 13:35:20 +0100 Subject: [PATCH 08/10] spotcgi: correctly kill ltl3ba on timeout * python/spot/__init__.py (automata): Do not create a session for every command, this is only needed if automata() is run with a timeout parameter. * python/ajax/spotcgi.in: Adjust exclude the main process from the process group, so that only children are killed on SIGALRM. * NEWS: Mention the bug. --- NEWS | 3 +++ python/ajax/spotcgi.in | 9 +++++---- python/spot/__init__.py | 12 ++++++++++-- 3 files changed, 18 insertions(+), 6 deletions(-) diff --git a/NEWS b/NEWS index ca895bdca..e2e42404a 100644 --- a/NEWS +++ b/NEWS @@ -27,6 +27,9 @@ New in spot 2.2.1.dev (Not yet released) * ltlfilt --from-ltlf should ensure that "alive" holds initially in order to reject empty traces. + * the on-line translator had a bug where a long ltl3ba process would + continue running even after the script had timeout'ed. + New in spot 2.2.1 (2016-11-21) Bug fix: diff --git a/python/ajax/spotcgi.in b/python/ajax/spotcgi.in index 308c5d840..baec65f70 100755 --- a/python/ajax/spotcgi.in +++ b/python/ajax/spotcgi.in @@ -164,7 +164,7 @@ def finish(kill = False): if kill: # Kill all children - os.kill(0, signal.SIGTERM) + os.killpg(child, signal.SIGTERM) # Should we prune the cache? stamp = imgdir + '/cache.stamp' now = time.time() @@ -217,7 +217,7 @@ it has been running for too long. Please try a shorter formula, or different options. If you want to benchmark big formulae it is better to install Spot on your own computer.

\n""") - finish(kill = True) + finish(kill=True) def run_dot(basename, ext): outname = basename + '.' + ext @@ -409,7 +409,6 @@ if output_type == 'v3': spot.unblock_signal(signal.SIGALRM) spot.unblock_signal(signal.SIGTERM) -os.setpgrp() child = os.fork() if child != 0: @@ -425,6 +424,8 @@ if child != 0: os.waitpid(child, 0) exit(0) +os.setpgrp() + # Global options utf8 = False for g in form.getlist('g'): @@ -608,7 +609,7 @@ elif translator == 'l3': g = spot.relabel(f, spot.Pnn, m) args.extend(['-f', "'" + spot.str_spin_ltl(g) + "' |"]) try: - automaton = spot.automaton(" ".join(args)) + automaton = spot.automaton(" ".join(args), no_sid=True) except RuntimeError as e: unbufprint('
{}
'.format(e)) finish() diff --git a/python/spot/__init__.py b/python/spot/__init__.py index e1b820161..5dba7a193 100644 --- a/python/spot/__init__.py +++ b/python/spot/__init__.py @@ -307,7 +307,7 @@ class formula: def automata(*sources, timeout=None, ignore_abort=True, - trust_hoa=True, debug=False): + trust_hoa=True, no_sid=False, debug=False): """Read automata from a list of sources. Parameters @@ -326,6 +326,10 @@ def automata(*sources, timeout=None, ignore_abort=True, trust_hoa : bool, optional If True (the default), supported HOA properies that cannot be easily verified are trusted. + no_sid : bool, optional + When an automaton is obtained from a subprocess, this + subprocess is started from a shell with its own session + group (the default) unless no_sid is set to True. debug : bool, optional Whether to run the parser in debug mode. @@ -386,11 +390,15 @@ def automata(*sources, timeout=None, ignore_abort=True, p = None proc = None if filename[-1] == '|': + setsid_maybe = None + if not no_sid: + setsid_maybe = os.setsid # universal_newlines for str output instead of bytes # when the pipe is read from Python (which happens # when timeout is set). proc = subprocess.Popen(filename[:-1], shell=True, - preexec_fn=os.setsid, + preexec_fn= + None if no_sid else os.setsid, universal_newlines=True, stdout=subprocess.PIPE) if timeout is None: From 574f47c366c65fb37b8a5b01aa56ba911f79eafd Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 16 Dec 2016 06:50:59 +0100 Subject: [PATCH 09/10] Release Spot 2.2.2 * 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 e2e42404a..6dc019ebd 100644 --- a/NEWS +++ b/NEWS @@ -1,4 +1,4 @@ -New in spot 2.2.1.dev (Not yet released) +New in spot 2.2.2 (2016-12-16) Build: diff --git a/configure.ac b/configure.ac index c82cd40e9..8836b60b3 100644 --- a/configure.ac +++ b/configure.ac @@ -21,7 +21,7 @@ # along with this program. If not, see . AC_PREREQ([2.61]) -AC_INIT([spot], [2.2.1.dev], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.2.2], [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 528627389..30c2ab494 100644 --- a/doc/org/setup.org +++ b/doc/org/setup.org @@ -1,8 +1,8 @@ #+OPTIONS: H:2 num:nil toc:t html-postamble:nil #+EMAIL: spot@lrde.epita.fr #+HTML_LINK_HOME: index.html -#+MACRO: SPOTVERSION 2.2.1 -#+MACRO: LASTRELEASE 2.2.1 -#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.2.1.tar.gz][=spot-2.2.1.tar.gz=]] -#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-2-1/NEWS][summary of the changes]] -#+MACRO: LASTDATE 2016-11-21 +#+MACRO: SPOTVERSION 2.2.2 +#+MACRO: LASTRELEASE 2.2.2 +#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.2.2.tar.gz][=spot-2.2.2.tar.gz=]] +#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-2-2/NEWS][summary of the changes]] +#+MACRO: LASTDATE 2016-12-16 From f8f7c9a537cd8822b3060e6a43cdf8c05eaf05f3 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 16 Dec 2016 06:58:46 +0100 Subject: [PATCH 10/10] bump version number * NEWS, configure.ac: Set version 2.2.2.dev. --- NEWS | 4 ++++ configure.ac | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index 6dc019ebd..d5a02d952 100644 --- a/NEWS +++ b/NEWS @@ -1,3 +1,7 @@ +New in spot 2.2.2.dev (not yet released) + + Nothing yet. + New in spot 2.2.2 (2016-12-16) Build: diff --git a/configure.ac b/configure.ac index 8836b60b3..d409bc0d2 100644 --- a/configure.ac +++ b/configure.ac @@ -21,7 +21,7 @@ # along with this program. If not, see . AC_PREREQ([2.61]) -AC_INIT([spot], [2.2.2], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.2.2.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])