- Spot-announce

Spot 2.10 released
by Alexandre Duret-Lutz 14 Nov '21

14 Nov '21

We are happy to announce the release of Spot 2.10 This is a major release that has been under development for 19 months. It contains new features contributed by Jérôme Dubois, Antoine Martin, Étienne Renault, Florian Renkin, Philipp Schlehuber, and myself. A summary of those changes is given at the end of this email. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.10.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.10 (2021-11-13) Build: - Spot is now built in C++17 mode, so you need at least GCC 7 or clang 5 to compile it. The current versions of all major linux distributions ship with at least GCC 7.4, so this should not be a problem. There is also an --enable-c++20 option to configure in case you want to force a build of Spot in C++20 mode. Command-line tools: - ltlsynt has been seriously overhauled, while trying to preserve backward compatibility. Below is just a summary of the main user-visible changes. Most of the new options are discussed on https://spot-dev.lrde.epita.fr/ltlsynt.html + ltlsynt now accepts only one of the --ins or --outs options to be given and will deduce the value of the other one. + ltlsynt learned --print-game-hoa to output its internal parity game in the HOA format (with an extension described below). + ltlsynt --aiger option now takes an optional argument indicating how the bdd and states are to be encoded in the aiger output. The option has to be given in the form ite|isop|both[+ud][+dc][+sub0|sub1|sub2] where the first only obligatory argument decides whether "if-then-else" ("ite") or irreducible-sum-of-products ("isop") is to be used. "both" executes both strategies and retains the smaller circuits. The additional options are for fine-tuning. "ud" also encodes the dual of the conditions and retains the smaller circuits. "dc" computes if for some inputs we do not care whether the output is high or low and try to use this information to compute a smaller circuit. "subX" indicates different strategies to find common subexpressions, with "sub0" indicating no extra computations. + ltlsynt learned --verify to check the computed strategy or aiger circuit against the specification. + ltlsynt now has a --decompose=yes|no option to specify if the specification should be decomposed into independent sub-specifications, the controllers of which can then be glued together to satisfy the input specification. (cf. [finkbeiner.21.nfm] in doc/spot.bib) + ltlsynt learned --simplify=no|bisim|bwoa|sat|bisim-sat|bwoa-sat to specifies how to simplify the synthesized controler. - ltl2tgba, autfilt, dstar2tgba, and randaut learned a --buchi option, or -b for short. This outputs Büchi automata without forcing state-based acceptance. The following aliases have also been added for consistency: --gba is an alias for --tgba, because the "t" of --tgba is never forced. --sba is an alias for -B/--ba, because -B really implies -S and that is not clear from --ba. As a consequence of the introduction of --sba, the option --sbacc (an alias for --state-based-acceptance) cannot be abbreviated as --sba anymore. - autfilt learned a --kill-states=NUM[,NUM...] option. - ltlcross, autcross, ltldo have learned shorthands for the commands of Owl 21.0. For instance running ltlcross 'owl-21 ltl2nba' ... is equivalent to running ltlcross '{owl-21 ltl2nba}owl-21 ltl2nba -f %f>%O' ... Library: - Spot now provides convenient functions to create and solve games. (twaalgos/game.hh) and some additional functions for reactive synthesis (twaalgos/synthesis.hh, twaalgos/mealy_machine.hh). - A new class called aig represent an and-inverter-graphs, and is currently used during synthesis. (twaalgos/aiger.hh) - Some new *experimental* classes, called "twacube" and "kripkecube" implement a way to store automata or Kripke structures without using BDDs as labels. Instead they use a structure called cube, that can only encode a conjunction of litterals. Avoiding BDDs (or rather, avoiding the BuDDy library) in the API for automata makes it possible to build multithreaded algorithms. /!\ Currently these classes should be considered as experimental, and their API is very likely to change in a future version. Functions like twacube_to_twa(), twa_to_twacube(), can be used to bridge between automata with BDD labels, and automata with cube labels. In addition to the previous conversion, we implemented various state-of-the-art multi-threaded emptiness-check algorithms: [bloemen.16.ppopp], [bloemen.16.hvc], [evangeslita.12.atva], [renault.13.lpar], [holzmann.11.ieee] (see doc/spot.bib). The mc_instanciator class provides an abstraction for launching, pinning, and stopping threads inside of parallel model-checking algorithms. The class ltsmin_model class, providing support for loading various models that follow ltsmin's PINS interinterface, has been adjusted and can now produce either a kripke instance, or a kripkecube instance. - The postprocessor::set_type() method can now accept options postprocessor::Buchi and postprocessor::GeneralizedBuchi. These syntaxes is more homogeneous with the rest of the supported types. Note that postprocessor::BA and postprocessor::TGBA, while still supported and not yet marked as deprecated, are best avoided in new code. postprocessor::set_type(postprocessor::TGBA) can be replaced by postprocessor::set_type(postprocessor::GeneralizedBuchi) and postprocessor::set_type(postprocessor::BA) by postprocessor::set_type(postprocessor::Buchi) postprocessor::set_pref(postprocessor::Small | postprocessor::SBAcc) Note that the old postprocessor::BA option implied state-based acceptance (and was unique in that way), but the new postprocessor::Buchi specifies Büchi acceptance without requiring state-based acceptance (something that postprocessor did not permit before). - Translations for formulas such as FGp1 & FGp2 &...& FGp32 which used to take ages are now instantaneous. (Issue #412.) - remove_fin() learned to remove more unnecessary edges by using propagate_marks_vector(), both in the general case and in the Rabin-like case. - simplify_acceptance() learned to simplify acceptence formulas of the form Inf(x)&Inf(y) or Fin(x)|Fin(y) when the presence of x always implies that of y. (Issue #406.) - simplifiy_acceptance_here() and propagate_marks_here() learned to use some patterns of the acceptance condition to remove or add (depending on the function) colors on edges. As an example, with a condition such as Inf(0) | Fin(1), an edge labeled by {0,1} can be simplied to {0}, but the oppose rewriting can be useful as well. (Issue #418.) - The parity_game class has been removed, now any twa_graph_ptr that has a "state-player" property is considered to be a game. - the "state-player" property is output by the HOA printer, and read back by the automaton parser, which means that games can be saved and loaded. - print_dot() will display states from player 1 using a diamond shape. - print_dot() learned to display automata that correspond to Mealy machines specifically. - print_dot() has a new option "i" to define id=... attributes for states (S followed by the state number), edges (E followed by the edge number), and SCCs (SCC followed by SCC number). The option "i(graphid)" will also set the id of the graph. These id attributes are useful if an automaton is converted into SVG and one needs to refer to some particular state/edge/SCC with CSS or javascript. See https://spot.lrde.epita.fr/oaut.html#SVG-and-CSS - spot::postproc has new configuration variables that define thresholds to disable some costly operation in order to speedup the processing of large automata. (Those variables are typically modified using the -x option of command-line tools, and are all documented in the spot-x(7) man page.) wdba-det-max Maximum number of additional states allowed in intermediate steps of WDBA-minimization. If the number of additional states reached in the powerset construction or in the followup products exceeds this value, WDBA-minimization is aborted. Defaults to 4096. Set to 0 to disable. This limit is ignored when -D used or when det-max-states is set. simul-max Number of states above which simulation-based reductions are skipped. Defaults to 4096. Set to 0 to disable. This also applies to the simulation-based optimization of the determinization algorithm. simul-trans-pruning For simulation-based reduction, this is the number of equivalence classes above which transition-pruning for non-deterministic automata is disabled. Defaults to 512. Set to 0 to disable. This applies to all simulation-based reduction, as well as to the simulation-based optimization of the determinization algorithm. Simulation-based reduction perform a number of BDD implication checks that is quadratic in the number of classes to implement transition pruning. dpa-simul Set to 0/1 to disable/enable simulation-based reduction performed after running a Safra-like determinization to optain a DPA. By default, it is only disabled with --low or if simul=0. dba-simul Set to 0/1 to disable/enable simulation-based reduction performed after running the powerset-like construction (enabled by option tba-det) to obtain a DBA. By default, it is only disabled with --low or if simul=0. spot::translator additionally honor the following new variables: tls-max-states Maximum number of states of automata involved in automata-based implication checks for formula simplifications. Defaults to 64. exprop When set, this causes the core LTL translation to explicitly iterate over all possible valuations of atomic propositions when considering the successors of a BDD-encoded state, instead of discovering possible successors by rewriting the BDD as a sum of product. This is enabled by default for --high, and disabled by default otherwise. When unambiguous automata are required, this option forced and cannot be disabled. (This feature is not new, but was not tunable before.) - In addition the to above new variables, the default value for ba-simul (controling how degeneralized automata are reduced) and for det-simul (simulation-based optimization of the determinization) is now equal to the default value of simul. This changes allows "-x simul=0" to disable all of "ba-simul", "dba-simul", "dpa-simul", and "det-simul" at once. - tgba_powerset() now takes an extra optional argument to specify a list of accepting sinks states if some are known. Doing so can cut the size of the powerset automaton by 2^|sinks| in favorable cases. - twa_graph::merge_edges() had its two passes swapped. Doing so improves the determinism of some automata. - twa_graph::kill_state(num) is a new method that removes the outgoing edge of some state. It can be used together with purge_dead_states() to remove selected states. - The new functions reduce_direct_sim(), reduce_direct_cosim() and reduce_iterated() (and their state based acceptance version, reduce_direct_sim_sba(), reduce_direct_cosim_sba() and reduce_iterated_sba()), are matrix-based implementation of simulation-based reductions. This new version is faster than the signature-based BDD implementation in most cases, however there are some cases it does not capture yet.. By default, the old one is used. This behavior can be changed by setting SPOT_SIMULATION_REDUCTION environment variable or using the "-x simul-method=..." option (see spot-x(7)). - The automaton parser will now recognize lines of the form #line 10 "filename" that may occur *between* the automata of an input stream to specify that error messages should be emitted as if the next automaton was read from "filename" starting on line 10. (Issue #232) - The automaton parser for HOA is now faster at parsing files where a label is used multiple times (i.e., most automata): it uses a hash table to avoid reconstructing BDDs corresponding to label that have already been parsed. This trick was already used in the never claim parser. - spot::twa_graph::merge_states() will now sort the vector of edges before attempting to detect mergeable states. When merging states with identical outgoing transitions, it will now also consider self-looping transitions has having identical destinations. Additionally, this function now returns the number of states that have been merged (and therefore removed from the automaton). - spot::zielonka_tree and spot::acd are new classes that implement the Zielonka Tree and Alternatic Cycle Decomposition, based on a paper by Casares et al. (ICALP'21). Those structures can be used to paritize any automaton, and more. The graphical rendering of ACD in Jupyter notebooks is Spot's first interactive output. See https://spot.lrde.epita.fr/ipynb/zlktree.html for more. Python: - Bindings for functions related to games. See https://spot.lrde.epita.fr/ipynb/games.html and https://spot.lrde.epita.fr/tut40.html for examples. - Bindings for functions related to synthesis and aig-circuits. See https://spot.lrde.epita.fr/ipynb/synthesis.html - spot::twa::prop_set was previously absent from the Python bindings, making it impossible to call make_twa_graph() for copying a twa. It is now available as spot.twa_prop_set (issue #453). Also for convenience, the twa_graph.__copy__() method, called by copy.copy(), will duplicate a twa_graph (issue #470). Bugs fixed: - tgba_determinize() could create parity automata using more colors than necessary. (Related to issue #298) - There were two corners cases under which sat_minimize() would return the original transition-based automaton when asked to produce state-based output without changing the acceptance condition. Deprecation notices: - twa_graph::defrag_states() and digraph::defrag_states() now take the renaming vector by reference instead of rvalue reference. The old prototype is still supported but will emit a deprecation warning.

1 0

Spot 2.9.8 released (with conda-forge packages for Linux and OSX)
by Alexandre Duret-Lutz 10 Aug '21

10 Aug '21

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.

1 0

Spot 2.9.7 released
by Alexandre Duret-Lutz 13 May '21

13 May '21

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.

1 0

Spot 2.9.6 released
by Alexandre Duret-Lutz 18 Jan '21

18 Jan '21

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.

1 0

Spot 2.9.5 released
by Alexandre Duret-Lutz 20 Nov '20

20 Nov '20

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

1 0

Spot 2.9.4 released
by Alexandre Duret-Lutz 07 Sep '20

07 Sep '20

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

1 0

Spot 2.9.3 released
by Alexandre Duret-Lutz 22 Jul '20

22 Jul '20

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

1 0

Spot 2.9.2 released
by Alexandre Duret-Lutz 21 Jul '20

21 Jul '20

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

1 0

Spot 2.9.1 released
by Alexandre Duret-Lutz 16 Jul '20

16 Jul '20

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

1 0

Spot 2.9 released
by Alexandre Duret-Lutz 30 Apr '20

30 Apr '20

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

1 0