We are happy to announce the release of Spot 2.8

Spot is a library of algorithms for manipulating LTL formulas and omega-automata objects (as commonly used in model checking).

This release contains code contributed by Clément Gillard and myself. A detailed list of new features is given at the end of this email.

You can find the new release here:

http://www.lrde.epita.fr/dload/spot/spot-2.8.tar.gz

See https://spot.lrde.epita.fr/ for documentation and installation instructions.

Note that since Debian 10 ("Buster") was released a few days ago, the "stable" Debian packages we distribute are now built for Buster.

As always, please direct any feedback to spot@lrde.epita.fr.

New in spot 2.8 (2019-07-10)

Command-line tools:

- autfilt learned --highlight-accepting-run=NUM to highlight some accepting run with color NUM.

- ltldo, ltlcross, and autcross are now preferring posix_spawn() over fork()+exec() when available.

- ltlcross has new options --determinize-max-states=N and --determinize-max-edges=M to restrict the use of determinization-based complementation to cases where it produces automata with at most N states and M edges. By default determinization is now attempted up to 500 states and 5000 edges. This is an improvement over the previous default where determinization-based complementation was not performed at all, unless -D was specified.

- ltlcross will now skip unnecessary cross-checks and consistency-checks (they are unnecessary when all automata could be complemented and statistics were not required).

- genaut learned --m-nba=N to generate Max Michel's NBA familly. (NBAs with N+1 states whose determinized have at least N! states.)

- Due to some new simplification of parity acceptance, the output of "ltl2tgba -P -D" is now using a minimal number of colors. This means that recurrence properties have an acceptance condition among "Inf(0)", "t", or "f", and persistance properties have an acceptance condition among "Fin(0)", "t", or "f".

- ltldo and ltlcross learned shorthands to call the tools ltl2na, ltl2nba, and ltl2ngba from Owl 19.06. Similarly, autcross learned a shorthand for Owl's dra2dpa.

Documentation:

- https://spot.lrde.epita.fr/tut90.html is a new file that explains the purpose of the spot::bdd_dict object.

Library:

- Add generic_accepting_run() as a variant of generic_emptiness_check() that returns an accepting run in an automaton with any acceptance condition.

- twa::accepting_run() and twa::intersecting_run() now work on automata using Fin in their acceptance condition.

- simulation-based reductions have learned a trick that sometimes improve transition-based output when the input is state-based. (The automaton output by 'ltl2tgba -B GFa | autfilt --small' now has 1 state instead of 2 in previous versions. Similarly, 'ltldo ltl2dstar -f 'GFa -> GFb' | autfilt --small' produces 1 state instead of 4.)

- simulation-based reductions hae learned another trick to better merge states from transiant SCCs.

- acc_cond::top_disjuncts() and acc_cond::top_conjuncts() can be used to split an acceptance condition on the top-level & or |. These methods also exist in acc_cond::acc_code.

- minimize_obligation() learned to work on very weak automata even if the formula or negated automaton are not supplied. (This allows "autfilt [-D] --small" to minimize very-weak automata whenever they are found to represent obligation properties.)

- There is a new spot::scc_and_mark_filter objet that simplifies the creation of filters to restrict spot::scc_info to some particular SCC while cutting new SCCs on given acceptance sets. This is used by spot::generic_emptiness_check() when processing SCCs recursively, and makes it easier to write similar code in Python.

- print_dot has a new option 'g', to hide edge labels. This is helpful to display automata as "graphs", e.g., when illustrating algorithms that do not care about labels.

- A new complement() function returns complemented automata with unspecified acceptance condition, allowing different algorithms to be used. The output can be alternating only if the input was alternating.

- There is a new class output_aborter that is used to specify upper bounds on the size of automata produced by some algorithms. Several functions have been changed to accept an output_aborter. This includes: * tgba_determinize() * tgba_powerset() * minimize_obligation() * minimize_wdba() * remove_alternation() * product() * the new complement() * the postprocessor class, via the "det-max-state" and "det-max-edges" options.

- SVA's first_match operator can now be used in SERE formulas and that is supported by the ltl_to_tgba_fm() translation. See doc/tl/tl.pdf for the semantics. *WARNING* Because this adds a new operator, any code that switches over the spot::op type may need a new case for op::first_match. Furthermore, the output of "randltl --psl" will be different from previous releases.

- The parser for SERE learned to recognize the ##n and ##[i:j] operators from SVA. So {##2 a ##0 b[+] ##1 c ##2 e} is another way to write {[*2];a:b[+];c;1;e}. The syntax {a ##[i:j] b} is replaced in different ways depending on the values of i, a, and b. The formula::sugar_delay() function implements this SVA operator in terms of the existing PSL operators. ##[+] and ##[*] are sugar for ##[1:$] and ##[0:$].

- The F[n:m] and G[n:m] operators introduced in Spot 2.7 now support the case where m=$.

- spot::relabel_apply() makes it easier to reverse the effect of spot::relabel() or spot::relabel_bse() on formula.

- The LTL simplifier learned the following rules: F(G(a | Fb)) = FGa | GFb (if option "favor_event_univ") G(F(a | Gb)) = GFa | FGb (if option "favor_event_univ") F(G(a & Fb) = FGa & GFb (unless option "reduce_size_strictly") G(F(a & Gb)) = GFa & FGb (unless option "reduce_size_strictly") GF(f) = GF(dnf(f)) (unless option "reduce_size_strictly") FG(f) = FG(cnf(f)) (unless option "reduce_size_strictly") (f & g) R h = f R h if h implies g (f & g) M h = f M h if h implies g (f | g) W h = f W h if g implies h (f | g) U h = f U h if g implies h Gf | F(g & eventual) = f W (g & eventual) if !f implies g Ff & G(g | universal) = f M (g | universal) if f implies !g f U (g & eventual) = F(g & eventual) if !f implies g f R (g | universal) = G(g | universal) if f implies !g

- cleanup_parity() and colorize_parity() were cleaned up a bit, resulting in fewer colors used in some cases. In particular, colorize_parity() learned that coloring transitiant edges does not require the introduction of a new color.

- A new reduce_parity() function implements and generalizes the algorithm for minimizing parity acceptance by Carton and Maceiras (Computing the Rabin index of a parity automaton, 1999). This is a better replacement for cleanup_parity() and colorize_parity(). See https://spot.lrde.epita.fr/ipynb/parity.html for examples.

- The postprocessor and translator classes are now using reduce_parity() for further simplifications.

- The code for checking recurrence/persistence properties can also use the fact the reduce_parity() with return "Inf(0)" (or "t" or "f") for deterministic automata corresponding to recurrence properties, and "Fin(0)" (or "t" or "f") for persistence properties. This can be altered with the SPOT_PR_CHECK environment variable.

Deprecation notices:

- The virtual function twa::intersecting_run() no longuer takes a second "from_other" Boolean argument. This is a backward incompatibility only for code that overrides this function in a subclass. For backward compatibility with programs that simply call this function with two argument, a non-virtual version of the function has been introduced and marked as deprecated.

- The spot::acc_cond::format() methods have been deprecated. These were used to display acceptance marks, but acceptance marks are unrelated to acceptance conditions, so it's better to simply print marks with operator<< without this extra step.

Bugs fixed:

- The gf_guarantee_to_ba() is relying on an inplace algorithm that could produce a different number of edges for the same input in two different transition order.

- A symmetry-based optimization of the LAR algorithm performed in spot::to_parity() turned out to be incorrect. The optimization has been removed. "ltlsynt --algo=lar" is the only code using this function currently.