Spot-announce

spot-announce@lrde.epita.fr

109 discussions

Spot 2.9.8 released (with conda-forge packages for Linux and OSX)

by Alexandre Duret-Lutz

We are happy to announce the release of Spot 2.9.8. This is a maintenance release that fixes a few bugs reported over the last three months, as well as a few warnings. New since the last version, we are now distributing Spot as a conda package (via conda-forge) for Linux and OSX. Instructions are on https://spot.lrde.epita.fr/install.html You can download the source for the new release directly from: http://www.lrde.epita.fr/dload/spot/spot-2.9.8.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. Versions from the 2.9.x branch are the last releases using C++14. We have already switched to C++17 for the development of the next major release. This release is already compatible with C++17, so those using Spot as a library should consider switching to C++17 already. Please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.9.8 (2021-08-10) Documentation: - Mention the conda-forge package. Bugs fixed: - left->intersacting_run(right) could return a run with incorrect colors (likely not corresponding to any existing transition of left) if left was a weak automaton. (Issue #471) - Fix bitset::operator-() causing issues when Spot was configured with more than 32 colors for instance with --enable-max-sets=64. (Issue #469) - Work around some warnings from newer compilers.

3 years, 11 months

Spot 2.9.7 released

by Alexandre Duret-Lutz

We are happy to announce the release of Spot 2.9.7. This is a maintenance release that fixes a handful of minor issues. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.9.7.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. Note that versions from the 2.9.x branch are the last releases using C++14. We have already switched to C++17 for the development of the next major release. This release is already compatible with C++17, so users using Spot as a library should consider switching to C++17 already. Please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.9.7 (2021-05-12) Bugs fixed: - Some formulas using ->, <->, or xor were not properly detected as purely universal or pure eventualities. - autfilt --keep-states=... could incorrectly mention --mask-acc when diagnosing errors. - Work around GraphViz issue 1931, causing spurious failures in the test suite. - Miscelaneous documentation fixes.

4 years, 2 months

Spot 2.9.6 released

by Alexandre Duret-Lutz

We are happy to announce the release of Spot 2.9.6. This is a maintenance release that fixes various issues, including a segmentation fault observed on the latest version of Alpine Linux released last week (however there is no reason why it may not occur elsewhere). It contains patches contributed by Florian Renkin, Jerome Dubois, and myself. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.9.6.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. Note that versions from the 2.9.x branch are the last releases using C++14. We have already switched to C++17 for the development of the next major release. This release is already compatible with C++17, so tools using Spot as a library should consider switching to C++17 already. Please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.9.6 (2021-01-18) Build: - Build scripts are now compatible with Autoconf 2.70 (Issue #447) and require at least Autoconf 2.69 (released in 2012). - Debian builds use updated standards. Bugs fixed: - twa_graph::merge_edges() could fail to merge two transitions if the destination transition was the first of the automaton. (Issue #441) - On non-deterministic automata, iterated_simulations() was performing an (unnecessary) second iteration even when the first one failed to reduce the automaton. (Issue #442) - When passed an incomplete automaton as input, tgba_determinize() would sometimes produce a complete automaton but incorrectly mark it as incomplete. (Related to issue #298) - gf_guarantee_to_ba(), used to translate some specific classes of subformulas, could segfault in some condition (Issue #449). - Work around some spurious test suite failures.

4 years, 6 months

Spot 2.9.5 released

by Alexandre Duret-Lutz

We are happy to announce the release of Spot 2.9.5 This is maintenance release with fixes for minor issues discovered over the last two months. If you already use 2.9.3 or later, there is no serious reason to upgrade. The release contains contributions from Jérôme Dubois and myself. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.9.5.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. Note that versions from the 2.9.x branch are the last releases using C++14. We have already switched to C++17 for the development of the next major release. This release is already compatible with C++17, so tools using Spot as a library should consider switching to C++17 already. Please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.9.5 (2020-11-19) 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) - Fix memory leak in minimize_wdba() when determinization is aborted because an output_aborter is passed. - Distribution used to contain unnecessary large SVG files (Issue #422) -- Alexandre Duret-Lutz

4 years, 8 months

Spot 2.9.4 released

by Alexandre Duret-Lutz

We are happy to announce the release of Spot 2.9.4 This is a maintenance release with very minor fixes. (If you already have 2.9.3, there is no real reason to upgrade.) The release contains contributions from Florian Renkin and myself. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.9.4.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. Note that versions from the 2.9.x branch are the last releases using C++14. We have already switched to C++17 for the development of the next major release. This release is already compatible with C++17, so tools using Spot as a library should consider switching to C++17 already. Please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.9.4 (2020-09-07) Bugs fixed: - Handle xor and <-> in a more natural way when translating LTL formulas to generic acceptance conditions. - Multiple typos in documentation, --help texts, or error messages. -- Alexandre Duret-Lutz

4 years, 10 months

Spot 2.9.3 released

by Alexandre Duret-Lutz

Yes, 2.9.2 was short-lived, as the main issue it was supposed to fix was only half-fixed... You can find the 2.9.3 release here: http://www.lrde.epita.fr/dload/spot/spot-2.9.3.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. Note that versions 2.9.x are likely to be the last releases using C++14. We plan to switch to C++17 for the next major release. The current code-base is already compatible with C++17, so tools using Spot as a library may consider switching to C++17 already. Please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.9.3 (2020-07-22) Bug fixed: - Completely fix the ltlcross issue mentioned in previous release. New in spot 2.9.2 (2020-07-21) Bugs fixed: - ltlcross --csv=... --product=N with N>0 could output spurious diagnostics claiming that words were rejected when evaluating the automaton on state-space. - spot::scc_info::determine_unknown_acceptance() now also update the result of spot::scc_info::one_accepting_scc(). -- Alexandre Duret-Lutz

4 years, 12 months

Spot 2.9.2 released

by Alexandre Duret-Lutz

Spot 2.9.2 has been released. This fixes a bug in ltlcross that was introduced in 2.9 and reported by Salomon Sickert. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.9.2.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. Note that versions 2.9.x are likely to be the last releases using C++14. We plan to switch to C++17 for the next major release. The current code-base is already compatible with C++17, so tools using Spot as a library may consider switching to C++17 already. Please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.9.2 (2020-07-21) Bugs fixed: - ltlcross --csv=... --product=N with N>0 could output spurious diagnosics claiming that words were rejected when evaluating the automaton on state-space. - spot::scc_info::determine_unknown_acceptance() now also update the result of spot::scc_info::one_accepting_scc(). -- Alexandre Duret-Lutz

4 years, 12 months

Spot 2.9.1 released

by Alexandre Duret-Lutz

We are happy to announce the release of Spot 2.9.1 This is mostly a maintenance release that fixes a couple of bugs discovered since the release of 2.9, as well as some simple portability issues. It also adds some minor features that were part of our SYNTCOMP submission (but not all patches of the SYNTCOMP submission have been merged yet). The release contains contributions from Florian Renkin and myself. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.9.1.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. Note that versions 2.9.x are likely to be the last releases using C++14. We plan to switch to C++17 for the next major release. The current code-base is already compatible with C++17, so tools using Spot as a library may consider switching to C++17 already. Please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.9.1 (2020-07-15) Command-line tools: - 'ltl2tgba -G -D' is now better at handling formulas that use '<->' and 'xor' operators at the top level. For instance ltl2tgba -D -G '(Fa & Fb & Fc & Fd) <-> GFe' now produces a 16-state automaton (instead of 31 in Spot 2.9). - Option '-x wdba-minize=N' used to accept N=0 (off), or N=1 (on). It can now take three values: 0: never attempt this optimization, 1: always try to determinize and minimize automata as WDBA, and check (if needed) that the result is correct, 2: determinize and minimize automata as WDBA only if it is known beforehand (by cheap syntactic means) that the result will be correct (e.g., the input formula is a syntactic obligation). The default is 1 in "--high" mode, 2 in "--medium" mode or in "--deterministic --low" mode, and 0 in other "--low" modes. - ltlsynt learned --algo=ps to use the default conversion to deterministic parity automata (the same as ltl2tgba -DP'max odd'). - ltlsynt now has a -x option to fine-tune the translation. See the spot-x(7) man page for detail. Unlike ltl2tgba, ltlsynt defaults to simul=0,ba-simul=0,det-simul=0,tls-impl=1,wdba-minimize=2. Library: - product_xor() and product_xnor() are two new versions of the synchronized product. They only work with operands that are deterministic automata, and build automata whose language are respectively the symmetric difference of the operands, and the complement of that. - tl_simplifier_options::keep_top_xor is a new option to keep Xor and Equiv operator that appear at the top of LTL formulas (maybe below other Boolean or X operators). This is used by the spot::translator class when creating deterministic automata with generic acceptance. - remove_fin() learned a trick to remove some superfluous transitions. Bugs fixed: - Work around undefined behavior reported by clang 10.0.0's UBsan. - spot::twa_sub_statistics was very slow at computing the number of transitions, and could overflow. It is now avoiding some costly loop of BDD operations, and storing the result using at least 64 bits. This affects the output of "ltlcross --csv" and "--stats=%t" for many tools. - simplify_acceptance() missed some patterns it should have been able to simplify. For instance Fin(0)&(Fin(1)|Fin(2)|Fin(4)) should simplify to Fin(1)|Fin(2)|Fin(4) adter adding {1,2,4} to every place where 0 occur, and then the acceptance would be renumbered to Fin(0)|Fin(1)|Fin(2). This is now fixed. - Improve ltldo diagnostics to fix spurious test-suite failure on systems with antique GNU libc. - twa_run::reduce() could reduce accepting runs incorrectly on automata using Fin in their acceptance condition. This caused issues in intersecting_run(), exclusive_run(), intersecting_word(), exclusive_word(), which all call reduce(). - ltlcross used to crash with "Too many acceptance sets used. The limit is 32." when complementing an automaton would require more acceptance sets than supported by Spot. This is now diagnosed with --verbose, but does not prevent ltlcross from continuing. - scc_info::edges_of() and scc_info::inner_edges_of() now correctly honor any filter passed to scc_info. -- Alexandre Duret-Lutz

5 years

Spot 2.9 released

by Alexandre Duret-Lutz

We are happy to announce the release of Spot 2.9 This is a major release that has been under development for 9 months. It contains new features contributed by from Florian Renkin and myself. A summary of those changes is given at the end of this email. Note that version 2.9 and the following 2.9.x minor releases are likely to be the last releases using C++14. We plan is to switch to C++17 for the next major release. The current code-base is already compatible with C++17, so tools using Spot as a library may consider switching to C++17 already. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.9.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. Please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.9 (2020-04-30) Command-line tools: - When the --check=stutter-sensitive-example option is passed to tools like ltl2tgba, autfilt, genaut, or ltldo, the produced automata are checked for stutter-invariance (as in the --check=stutter-invariant case), additionally a proof of stutter-sensitiveness is provided as two stutter-equivalent words: one accepted, and one rejected. These sample words are printed in the HOA output. % ltl2tgba --check=stutter-sensitive-example Xa | grep word: spot-accepted-word: "!a; cycle{a}" spot-rejected-word: "!a; !a; cycle{a}" - autfilt learned the --partial-degeneralize option, to remove conjunctions of Inf, or disjunctions of Fin that appears in arbitrary conditions. - ltlfilt and autfilt learned a --nth=RANGE (a.k.a. -N) option to select a range of their input formulas or automata (assuming a 1-based numbering). - When running translators, ltlcross will now display {names} when supplied. - ltlcross is now using the generic emptiness check procedure introduced in Spot 2.7, as opposed to removing Fin acceptance before using a classical emptiness check. - ltlcross learned a --save-inclusion-products=FILENAME option. Its use cases are probably quite limited. We use that to generate benchmarks for our generic emptiness check procedure. - ltlsynt --algo=lar uses the new version of to_parity() mentionned below. The old version is available via --algo=lar.old - ltlsynt learned --csv=FILENAME, to record some statistics about the duration of its different phases. - The dot printer is now automatically using rectangles with rounded corners for automata states if one state label have five or more characters. This saves space with very long labels. Use --dot=c, --dot=e, or --dot=E to force the use of Circles, Ellipses, or rEctangles. Library: - Historically, Spot only supports LTL with infinite semantics so it had automatic simplifications reducing X(1) and X(0) to 1 and 0 whenever such formulas are constructed. This caused issues for users of LTLf formulas, where it is important to distinguish a "weak next" (for which X(1)=1 but X(0)!=0) from a "strong next" (for which X(0)=0 but X(1)!=1). To accommodate this, this version introduces a new operator op::strong_X in addition to the existing op::X (whose interpretation is now weak in LTLf). The syntax for the strong next is X[!] as a reference to the PSL syntax (where the strong next is written X!). Trivial simplification rules for X are changed to just X(1) = 1 (and not X(0)=0 anymore) while we have X[!]0 = 0 The X(0)=0 and X[!]1=1 reductions are now preformed during LTL simplification, not automatically. Aside from the from_ltlf() function, the other functions of the library handle X and X[!] in the same way, since there is no difference between X and X[!] over infinite words. Operators F[n:m!] and G[n:m!] are also supported as strong variants of F[n:m] and G[n:m], but those four are only implemented as syntactic sugar. - acc_cond::acc_code::parity(bool, bool, int) was not very readable, as it was unclear to the reader what the boolean argument meant. The following sister functions can now improve readability: parity_max(is_odd, n) = parity(true, is_odd, n) parity_max_odd(n) = parity_max(true, n) parity_max_even(n) = parity_max(false, n) parity_min(is_odd, n) = parity(false, is_odd, n) parity_min_odd(n) = parity_min(true, n) parity_min_even(n) = parity_min(false, n) - partial_degeneralize() is a new function performing partial degeneralization to get rid of conjunctions of Inf terms, or disjunctions of Fin terms in acceptance conditions. - simplify_acceptance_here() and simplify_acceptance() learned to simplify subformulas like Fin(i)&Fin(j) or Inf(i)|Inf(j), or some more complex variants of those. If i is uniquely used in the acceptance condition, these become respectively Fin(i) or Inf(i), and the automaton is adjusted so that i also appears where j appeared. - acc_code::unit_propagation() is a new method for performing unit propagation in acceptance condition. E.g. Fin(0) | (Inf(0) & Inf(1)) becomes Fin(0) | Inf(1). This is now called by simplify_acceptance_here(). - propagate_marks_vector() and propagate_marks_here() are helper functions for propagating marks on the automaton: ignoring self-loops and out-of-SCC transitions, marks common to all the input transitions of a state can be pushed to all its outgoing transitions, and vice-versa. This is repeated until a fix point is reached. propagate_marks_vector() does not modify the automaton and returns a vector of the acc_cond::mark_t that should be on each transition; propagate_marks_here() actually modifies the automaton. - rabin_to_buchi_if_realizable() is a new variant of rabin_to_buchi_maybe() that converts a Rabin-like automaton into a Büchi automaton only if the resulting Büchi automaton can keep the same transition structure (where the ..._maybe() variant would modify the Rabin automaton if needed). - to_parity() has been rewritten. It now combines several strategies for paritizing automata with any acceptance condition. - relabel_bse(), used by ltlfilt --relabel-bool, is now better at dealing with n-ary operators and isolating subsets of operands that can be relabeled as a single term. - print_dot()'s default was changed to use circles for automata with fewer than 10 unamed states, ellipses for automata with up to 1000 unamed states (or named states with up to 4 characters), and rounded rectangles otherwise. Rectangles are also used for automata with acceptance bullets on states. The new "E" option can be used to force rectangles in all situations. - The generic emptiness check has been slightly improved (doing fewer recursive calls in the worst case). Backward-incompatible changes: - iar() and iar_maybe() have been moved from spot/twaalgos/rabin2parity.hh spot/twaalgos/toparity.hh and marked as deprecated, they should be replaced by to_parity(). In case the input is Rabin-like or Streett-like, to_parity() should be at least as good as iar(). - The twa_graph::is_alternating() and digraph::is_alternating() methods, deprecated in Spot 2.3.1 (2017-02-20), have been removed. Bugs fixed: - Relabeling automata could introduce false edges. Those are now removed. - Emptiness checks, and scc_info should now ignore edges labeled with false. - relabel_bse() could incorrectly relabel Boolean subformulas that had some atomic propositions in common. -- Alexandre Duret-Lutz

5 years, 2 months

Spot 2.8.7 released

by Alexandre Duret-Lutz

We are happy to announce the release of Spot 2.8.7 This maintenance release contains only bug fixes. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.8.7.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. Please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.8.7 (2019-03-13) Bugs fixed: - Building a product between two complete automata where one operand had false acceptance could create an incomplete automaton incorrectly tagged as complete, causing the print_hoa() function to raise an exception. - autfilt --uniq was not considering differences in acceptance conditions or number of states when discarding automata. - In an automaton with acceptance condition containing some Fin, and whose accepting cycle could be reduced to a self-loop in an otherwise larger SCC, the generation of an accepting run could be wrong. This could in turn cause segfaults or infinite loops while running autcross or autfilt --stats=%w. - The generic emptiness check used a suboptimal selection of "Fin" to remove, not matching the correct line in our ATVA'19 paper. This could cause superfluous recursive calls, however benchmarks have shown the difference to be insignificant in practice. - The sl(), and sl2() functions for computing the "self-loopization" of an automaton, and used for instance in algorithms for computing proof of stutter-sensitiveness (e.g., in our web application), were incorrect when applied on automata with "t" acceptance (or more generaly, any automaton where a cycle without mark is accepting). - ltlcross was not diagnosing write errors associated to options --grind=FILENAME and --save-bogus=FILENAME. -- Alexandre Duret-Lutz

5 years, 4 months

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Spot-announce