NEWS

New in spot 2.11.2  (2022-10-26)

  Command-line tools:

  - The --stats specifications %s, %e, %t for printing the number of
    (reachable) states, edges, and transitions, learned to support
    options [r], [u], [a] to indicate if only reachable, unreachable,
    or all elements should be counted.

  Library:

  - spot::reduce_parity() now has a "layered" option to force all
    transition in the same parity layer to receive the same color;
    like acd_transform() would do.

  Bugs fixed:

  - Fix pkg-config files containing @LIBSPOT_PTHREAD@ (issue #520)
  - spot::relabel_bse() was incorrectly relabeling some dependent
    Boolean subexpressions in SERE.  (Note that this had no
    consequence on automata translated from those SERE.)

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.

  - 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).

New in spot 2.10.6  (2022-05-18)

  Bugs fixed:

  - Fix compilation error on MacOS X.

  - Using -Ffile/N to read column N of a CSV file would not reset the
    /N specification for the next file.

  - make_twa_graph() will now preserve state number when copying a
    kripke_graph object.  As a consequence, print_dot() and
    print_hoa() will now use state numbers matching those of the
    kripke_graph (issue #505).

  - Fix several compilation warning introduced by newer versions
    of GCC and Clang.

New in spot 2.10.5  (2022-05-03)

  Bugs fixed:

  - reduce_parity() produced incorrect results when applied to
    automata with deleted edges.

  - An optimization of Zielonka could result in incorrect results
    in some cases.

  - ltlsynt --print-pg incorrectly solved the game in addition to
    printing it.

  - ltlsynt would fail if only one of --ins or --outs was set, and
    if it was set empty.

  - Work around a portability issue in Flex 2.6.4 preventing
    compilation on OpenBSD.

  - Do not use the seq command in test cases, it is not available
    everywhere.

  - Do not erase the previous contents of the PYTHONPATH environment
    variable when running tests, prepend to it instead.

  - Simplify Debian instructions for LTO build to work around newer
    libtool version.

  - Fix invalid read in digraph::sort_edges_of_(), currently unused in
    Spot.

New in spot 2.10.4  (2022-02-01)

  Bug fixed:

  - Fix memory leaks in Python bindings for several iteration objects.
    This occured while itering on twa_graph.out(), twa_graph.edges(),
    twa_graph.univ_dests(), kripke_graph.out(), kripke_graph.edges(),
    mark_t.sets(), scc_info.edges_of(), scc_info.inner_edges_of(), and
    on an scc_info instance.

New in spot 2.10.3  (2022-01-15)

  Bugs fixed:

  - On automata where the absence of color is not rejecting
    (e.g. co-Büchi) and where the initial state was in a rejecting
    SCC, sbacc() could output a superfluous state.  (Issue #492)

  - Compared to 2.9.8, complement() (and many functions using it) was
    slower and produced larger outputs on some automata with more than
    32 states due to an optimization of the determinization being
    unintentionally disabled.

  - The split_2step() function used to create a synthesis game could
    complain that it was unable to complement a monitor (Issue #495).

  - Work around GraphViz bug #2179 by avoiding unnecessary empty
    lines in the acceptance conditions shown in dot.

  - Fix a case where generic_accepting_run() incorrectly returns a
    cycle around a rejecting self-loop.

  - Mealy machines resulting from SAT-based minimization could differ
    on architectures with different hash tables implementations.

  - org-mode moved to GNU ELPA (Issue #496).

New in spot 2.10.2  (2021-12-03)

  Bugs fixed:

  - twa_graph::purge_dead_states() now also removes edges labeled by
    bddfalse.

  - only use sched_getcpu() and pthread_setaffinity_np() when they are
    available.

  - Using ##300 in a SERE will report that the repeatition exceeds the
    allowed value using a parse error, not as an exception.

  - spot::formula::is_literal() should be const.

New in spot 2.10.1  (2021-11-19)

  Build:

  - Python 3.5 or later is now required (unless Python bindings are
    disabled).  Python 3.5 reached end-of-life one year ago, so we
    believe support for older versions of Python will not be missed.

  Library:

  - The sbacc() function now defines the "original-states" property,
    allowing to map an output state back to its input.

  Bugs fixed:

  - Ranged repetition operators from LTL/PSL, like [*a..b],
    [->a..b] or even F[a..b] used to store and handle a and b
    as 8-bit values without overflow checks.  So for instance
       {a[*260];b} was silently interpreted as {a[*4];b}
    This version still restricts those bounds to 8 bits, but now
    diagnose overflow checks while parsing and constructing formulas.
    Also the so called "trivial simplification rules" will not be
    applied in case they would lead to an overflow.  For instance
       {a;[*150];[*50];b} is rewritten to {a;[*200];b}
    but
       {a;[*150];[*150];b} is untouched.

  - Fix a compilation error on system with glibc older than 2.18,
    where <inttypes.h> does not define some C99 macro by default when
    compiled in C++ mode.  (Such old libraries are used when compiling
    packages for conda-forge, which use CentOS 6 as building environment.)

  - Fix a link error of tests/ltsmin/modelcheck not finding BDD functions
    on some systems (observed on CentOS 6 again).

  - Fix spurious test-suite failures under newer Jupyter
    installations.  IPykernel 6.0 now captures stdout/stderr from
    subprocesses and displays them in the notebook.  The spot.ltsmin
    code that loads modules compiled with SpinS had to be rewritten to
    capture and display the output of SpinS, so that our test-cases
    can be reproduced regardless of the IPykernel version.  This fix
    was easier to do in Python 3.5.

  - Fix sevaral minor documentation errors.

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.

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.


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.

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.

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)

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.

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().

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-minimize=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
    transitons, 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) after 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.

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