We are happy to announce the release of Spot 2.11.1 Spot is a C++17 library for handling of linear-time temporal logic formulas and omega automata. It comes with a set of command-line utilities (to automate various tasks) and Python binding for easy prototyping. Some applications are model-checking and reactive synthesis. Spot 2.11 is a major release containing new features and improvements implemented over the last 11 months by Florian Rankin, Philipp Schlehuber-Caissier, Antoine Martin, and myself. A detailled list of changes is appended to this email. Spot 2.11.1 fixes a couple of build issues discovered before I had time to announce 2.11... You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.11.1.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. Please direct any feedback to <spot@lrde.epita.fr>. ⚠ Note that LRDE (EPITA's Research & Development Laboratory) had been merged with another entity into something larger that is now called LRE (EPITA's Research Laboratory). The removal of "development", is nothing to worry about: we are still continuing to develop Spot as part of our research. However a consequence is that this release contains a mix of URLs in "lre.epita.fr" (for services that have already migrated to the new name) and "lrde.epita.fr". If you find a URL ending in "lrde.epita.fr" that does not work, please try without the "d". New in spot 2.11.1 (2022-10-10) Bugs fixed: - Fix a build issue preventing the update of website (issue #516). - Fix a compilation error with clang-14 on FreeBSD (issue #515). New in spot 2.11 (2022-10-08) Build: - configure will now diagnose situations where Python bindings will be installed in a directory that is not part of Python's search path. A new configure option --with-pythondir can be used to modify this installation path. (Issue #512) - A new configure option --enable-pthread enables the compilation of Spot with -pthread, and render available the parallel version of some algorithms. If Spot is compiled with -pthread enabled, any user linking with Spot should also link with the pthread library. In order to not break existing build setups using Spot, this option is currently disabled by default in this release. We plan to turn it on by default in some future release. Third-party project using Spot may want to start linking with -pthread in prevision for this change. Command-line tools: - autfilt has a new options --aliases=drop|keep to specify if the HOA printer should attempt to preserve aliases present in the HOA input. This defaults to "keep". - autfilt has a new --to-finite option, illustrated on https://spot.lrde.epita.fr/tut12.html - ltlfilt has a new --sonf option to produce a formula's Suffix Operator Normal Form, described in [cimatti.06.fmcad]. The associated option --sonf-aps allows listing the newly introduced atomic propositions. - autcross learned a --language-complemented option to assist in the case one is testing tools that complement automata. (issue #504). - ltlsynt has a new option --tlsf that takes the filename of a TLSF specification and calls syfco (which must be installed) to convert it into an LTL formula. - ltlsynt has a new option --from-pgame that takes a parity game in extended HOA format, as used in the Synthesis Competition. - ltlsynt has a new option --hide-status to hide the REALIZABLE or UNREALIZABLE output expected by SYNTCOMP. (This line is superfluous, because the exit status of ltlsynt already indicate whether the formula is realizable or not.) - ltlsynt has a new option --dot to request GraphViz output instead of most output. This works for displaying Mealy machines, games, or AIG circuits. See https://spot.lrde.epita.fr/ltlsynt.html for examples. - genaut learned the --cyclist-trace-nba and --cyclist-proof-dba options. Those are used to generate pairs of automata that should include each other, and are used to show a regression (in speed) present in Spot 2.10.x and fixed in 2.11. - genltl learned --eil-gsi to generate a familly a function whose translation and simplification used to be very slow. In particular genltl --eil-gsi=23 | ltlfilt --from-ltlf | ltl2tgba was reported as taking 9 days. This is now instantaneous. Library: - The new function suffix_operator_normal_form() implements transformation of formulas to Suffix Operator Normal Form, described in [cimatti.06.fmcad]. - "original-classes" is a new named property similar to "original-states". It maps an each state to an unsigned integer such that if two classes are in the same class, they are expected to recognize the same language. The "original-states" should be prefered property when that integer correspond to some actual state. - tgba_determinize() learned to fill the "original-classes" property. States of the determinized automaton that correspond to the same subset of states of the original automaton belong to the same class. Filling this property is only done on demand as it inccurs a small overhead. - sbacc() learned to take the "original-classes" property into account and to preserve it. - The HOA parser and printer learned to map the synthesis-outputs property of Spot to the controllable-AP header for the Extended HOA format used in SyntComp. https://arxiv.org/abs/1912.05793 - The automaton parser learned to parse games in the PGSolver format. See the bottom of https://spot.lrde.epita.fr/ipynb/games.html for an example. - "aliases" is a new named property that is filled by the HOA parser using the list of aliases declared in the HOA file, and then used by the HOA printer on a best-effort basis. Aliases can be used to make HOA files more compact or more readable. But another possible application is to use aliases to name letters of a 2^AP alphabet, in applications where using atomic propositions is inconvenient. - print_dot() learned option "@" to display aliases, as discussed above. - to_finite() is a new function that help interpreting automata build from LTLf formula using the from_ltlf() function. It replace the previously suggested method of removing and atomic proposition and simpifying automata, that failed to deal with states without successors. See updated https://spot.lrde.epita.fr/tut12.html - the HOA parser learned to not ignore self-loops labeled with [f] and to turn any state that have colors but no outgoing transitions into a state with a [f] self-loop. This helps dealing with automata containing states without successors, as in the output of to_finite(). - purge_dead_states() will now also remove edges labeled by false (except self-loops). - When parsing formulas with a huge number of operands for an n-ary operator (for instance 'p1 | p2 | ... | p1000') the LTL parser would construct that formula two operand at a time, and the formula constructor for that operator would be responsible for inlining, sorting, deduplicating, ... all operands at each step. This resulted in a worst-than-quadratic slowdown. This is now averted in the parser by delaying the construction of such n-ary nodes until all children are known. - complement() used to always turn tautological acceptance conditions into Büchi. It now only does that if the automaton is modified. - The zielonka_tree construction was optimized using the same memoization trick that is used in ACD. Additionally it can now be run with additional options to abort when the tree as an unwanted shape, or to turn the tree into a DAG. - contains() can now take a twa as a second argument, not just a twa_graph. This allows for instance to do contains(ltl, kripke) to obtain a simple model checker (that returns true or false, without counterexample). - degeneralize() and degeneralize_tba() learned to work on generalized-co-Büchi as well. - product() learned that the product of two co-Büchi automata is a co-Büchi automaton. And product_or() learned that the "or"-product of two Büchi automata is a Büchi automaton. - spot::postprocessor has a new extra option "merge-states-min" that indicates above how many states twa_graph::merge_states() (which perform a very cheap pass to fuse states with identicall succesors) should be called before running simulation-based reductions. - A new function delay_branching_here(aut) can be used to simplify some non-deterministic branching. If two transitions (q₁,ℓ,M,q₂) and (q₁,ℓ,M,q₃) differ only by their destination state, and are the only incoming transitions of their destination states, then q₂ and q₃ can be merged (taking the union of their outgoing transitions). This is cheap function is automatically called by spot::translate() after translation of a formula to GBA, before further simplification. This was introduced to help with automata produced from formulas output by "genltl --eil-gsi" (see above). - spot::postprocessor has new configuration variable branch-post that can be used to control the use of branching-postponement (disabled by default) or delayed-branching (see above, enabled by default). See the spot-x(7) man page for details. - spot::postprocessor is now using acd_transform() by default when building parity automata. Setting option "acd=0" will revert to using "to_parity()" instead. - to_parity() has been almost entirely rewritten and is a bit faster. - When asked to build parity automata, spot::translator is now more aggressively using LTL decomposition, as done in the Generic acceptance case before paritizing the result. This results in much smaller automata in many cases. - spot::parallel_policy is an object that can be passed to some algorithm to specify how many threads can be used if Spot has been compiled with --enable-pthread. Currently, only twa_graph::merge_states() supports it. Python bindings: - The to_str() method of automata can now export a parity game into the PG-Solver format by passing option 'pg'. See https://spot.lrde.epita.fr/ipynb/games.html for an example. Deprectation notice: - spot::pg_print() has been deprecated in favor of spot::print_pg() for consistency with the rest of the API. Bugs fixed: - calling twa_graph::new_univ_edge(src, begin, end, cond, acc) could produce unexpected result if begin and end where already pointing into the universal edge vector, since the later can be reallocated during that process. - Printing an alternating automaton with print_dot() using 'u' to hide true state could produce some incorrect GraphViz output if the automaton as a true state as part of a universal group. - Due to an optimization introduces in 2.10 to parse HOA label more efficiently, the automaton parser could crash when parsing random input (not HOA) containing '[' (issue #509).