- Spot-announce

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

Spot 2.8.7 released
by Alexandre Duret-Lutz 13 Mar '20

13 Mar '20

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

1 0

Spot 2.8.6 released
by Alexandre Duret-Lutz 19 Feb '20

19 Feb '20

We are happy to announce the release of Spot 2.8.6 This maintenance release containing fixes for bug discovered during the development of the future 2.9 release. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.8.6.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.6 (2020-02-19) Bugs fixed: - calling spot.translate() with two conflicting preferences like spot.translate(..., 'det', 'any') triggered a syntax error in the Python code to handle this error. - degeneralize_tba() was incorrectly not honnoring the "skip_level" optimization after creating an accepting transition; as a consequence, some correct output could be larger than necessary (but still correct). - Some formulas with Boolean sub-formulas equivalent to true or false could be translated into automata with false labels. - The HOA printer would incorrectly output the condition 'Fin(1) & Inf(2) & Fin(0)' as 'Fin(0) | Fin(1) & Inf(2)' due to a bug in the is_generalized_rabin() matching function. -- Alexandre Duret-Lutz

1 0

Spot 2.8.5 released
by Alexandre Duret-Lutz 04 Jan '20

04 Jan '20

We are happy to announce the release of Spot 2.8.5 This maintenance release contains only bug fixes. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.8.5.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.5 (2020-01-04) Bugs fixed: - ltl2tgba -B could return automata with "t" acceptance, instead of the expected Inf(0). - twa_graph::merge_edges() (a.k.a. autfilt --merge-transitions) was unaware that merging edges can sometimes transform a non-deterministic automaton into a deterministic one, causing the following unexpected diagnostic: "print_hoa(): automaton is universal despite prop_universal()==false" The kind of non-deterministic automata where this occurs is not naturally produced by any Spot algorithm, but can be found for instance in automata produced by Goal 2015-10-18. -- Alexandre Duret-Lutz

1 0

Spot 2.8.4 has been released
by Alexandre Duret-Lutz 09 Dec '19

09 Dec '19

We are happy to announce the release of Spot 2.8.4 This release contains a fix for a bug affecting complementation of Rabin-like automata. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.8.4.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.4 (2019-12-08) Bugs fixed: - The Rabin-to-Büchi conversion could misbehave when applied to Rabin-like acceptance with where some pairs have missing Inf(.) (e.g. Fin(0)|(Inf(1)&Fin(2))) and when some of the SCCs do not visit the remaining Inf(.). This indirectly caused the complementation algorithm to produce incorrect results on such inputs, causing false positives in ltlcross and autcross. - Work around a small difference between Python 3.7 and 3.8, causing spurious failures of the test suite. -- Alexandre Duret-Lutz

1 0

Spot 2.8.3 released
by Alexandre Duret-Lutz 06 Nov '19

06 Nov '19

We are happy to announce the release of Spot 2.8.3 This release mainly works around an issue in recent GraphViz releases, causing cropped automata in Jupyter notebooks. (If you do not use Spot in Jupyter notebooks, there is little point in updating.) You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.8.3.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.3 (2019-11-06) Build: - Minor portabilities improvements with C++17 deprecations. Python: - Doing "import spot.foo" will now load any spot-extra/foo.py on Python's search path. This can be used to install third-party packages that want to behave as plugins for Spot. - Work around GraphViz bug #1605 in Jupyter notebooks. https://gitlab.com/graphviz/graphviz/issues/1605 -- Alexandre Duret-Lutz

1 0

Spot 2.8.2 released
by Alexandre Duret-Lutz 28 Sep '19

28 Sep '19

We are happy to announce the release of Spot 2.8.2 This release contains many minor fixes; mostly portability issues. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.8.2.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.2 (2019-09-27) Command-line tools: - ltl2tgba and ltldo learned a --negate option. Bugs fixed: - Calling "autfilt --dualize" on an alternating automaton with transition-based acceptance and universal initial states would fail with "set_init_state() called with nonexisting state". - The numbering of nodes in the AIGER output of ltlsynt was architecture dependent. - Various compilation issues. In particular, this release is the first one that can be compiled (and pass tests) on a Raspberry PI. -- Alexandre Duret-Lutz

1 0

Spot 2.8.1 released
by Alexandre Duret-Lutz 18 Jul '19

18 Jul '19

We are happy to announce the release of Spot 2.8.1 This release one important bug fix to ltlcross, and a few other minor addition. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.8.1.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. As always, please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.8.1 (2019-07-18) Command-line tools: - genltl learned --pps-arbiter-standard and --pps-arbiter-strict. - ltlcross and autcross have learned a new option -q (--quiet) to remain quiet until an error is found. This helps for instance in scenarios where multiple instances of ltlcross/autcross are run in parallel (using "xargs -P" or "GNU Parallel", for instance). See https://spot.lrde.epita.fr/ltlcross.html#parallel for examples. Bugs fixed: - When complement() was called with an output_aborter, it could return an alternating automaton on large automata. This in turn caused ltlcross to emit errors like "remove_alternation() only works with weak alternating automata" or "product() does not support alternating automata". - Work around Emacs bug #34341 when rebuilding documentation on a system with Emacs <26.3, GNU TLS >= 3.6, and without ESS or with an obsolete org-mode installed. -- Alexandre Duret-Lutz

1 0

Spot 2.8 released
by Alexandre Duret-Lutz 10 Jul '19

10 Jul '19

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(a)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. -- Alexandre Duret-Lutz

1 0